BT003C · Bertrand theorem

multiple_decidable

Stable checked-use theorem · independently kernel verified

Divisibility of natural numbers is constructively decidable, including the zero divisor case.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ d. ∀ n. Dvd(d,n) ∨ ¬Dvd(d,n)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0003 Dvd

2 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall d n. (exists q. n = d * q) \/ ~(exists q. n = d * q)

Proof neighborhood

Direct theorem prerequisites

BT0004 mul_zero_left BT003A eq_decidable BT003B multiple_decidable_nonzero

Direct theorem dependents

BT00Q3 power_divides_decidable

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

29 script commands · 20 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (3)
mul zero lefteq decidablemultiple decidable nonzero
01Fix variables and assumptionsL1–2

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro d
  2. L2
    intro n
02Use earlier factsL3–4

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L3
    specialize eq_decidable d
  2. L4
    specialize eq_decidable 0
03Establish hdL5–6

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eq decidable.

  1. L5
    have hd : d = 0 \/ ~(d = 0)
  2. L6
    apply eq_decidable
04Separate the logical casesL7–7

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L7
    cases hd
05Use earlier factsL8–9

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L8
    specialize eq_decidable_before n
  2. L9
    specialize eq_decidable_before 0
06Establish hnL10–11

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eq decidable before.

  1. L10
    have hn : n = 0 \/ ~(n = 0)
  2. L11
    apply eq_decidable_before
07Separate the logical casesL12–13

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L12
    cases hn
  2. L13
    left
08Construct an explicit witnessL14–14

Supply the displayed value, then prove that it has the required property.

  1. L14
    exists 0
09Calculate and transport equalitiesL15–15

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L15
    trans 0
10Use earlier factsL16–16

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L16
    exact hn_left
11Calculate and transport equalitiesL17–18

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L17
    symm
  2. L18
    rewrite hd_left
12Use earlier factsL19–19

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L19
    apply mul_zero_left
13Separate the logical casesL20–20

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L20
    right
14Fix variables and assumptionsL21–21

Work with arbitrary variables or the premises of the current implication.

  1. L21
    intro hmultiple
15Separate the logical casesL22–22

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L22
    cases hmultiple
16Use earlier factsL23–23

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L23
    apply hn_right
17Calculate and transport equalitiesL24–24

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L24
    trans d * x
18Use earlier factsL25–25

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L25
    exact hmultiple_witness
19Calculate and transport equalitiesL26–26

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L26
    rewrite hd_left
20Use earlier factsL27–29

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L27
    apply mul_zero_left
  2. L28
    apply multiple_decidable_nonzero
  3. L29
    exact hd_right

Library-wide reading audit

Original defined command ledger · 29 lines
  1. 0001intro d
  2. 0002intro n
  3. 0003specialize eq_decidable d
  4. 0004specialize eq_decidable 0
  5. 0005have hd : d = 0 \/ ~(d = 0)
  6. 0006apply eq_decidable
  7. 0007cases hd
  8. 0008specialize eq_decidable_before n
  9. 0009specialize eq_decidable_before 0
  10. 0010have hn : n = 0 \/ ~(n = 0)
  11. 0011apply eq_decidable_before
  12. 0012cases hn
  13. 0013left
  14. 0014exists 0
  15. 0015trans 0
  16. 0016exact hn_left
  17. 0017symm
  18. 0018rewrite hd_left
  19. 0019apply mul_zero_left
  20. 0020right
  21. 0021intro hmultiple
  22. 0022cases hmultiple
  23. 0023apply hn_right
  24. 0024trans d * x
  25. 0025exact hmultiple_witness
  26. 0026rewrite hd_left
  27. 0027apply mul_zero_left
  28. 0028apply multiple_decidable_nonzero
  29. 0029exact hd_right