BT003B · Bertrand theorem

multiple_decidable_nonzero

Stable checked-use theorem · independently kernel verified

Divisibility by a nonzero natural is constructively decidable.

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. ¬d = 0 → 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

PD0002 Lt PD0007 DivRem

2 occurrences

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

Proof neighborhood

Direct theorem prerequisites

BT003A eq_decidable BT001P division_remainder_exists BT001W multiple_has_zero_remainder BT001U division_remainder_unique

Direct theorem dependents

BT003C multiple_decidable BT003E factor_search_up_to

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

40 script commands · 18 reading checkpoints · 4 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 (4)
eq decidabledivision remainder existsmultiple has zero remainderdivision remainder unique
01Fix variables and assumptionsL1–3

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

  1. L1
    intro d
  2. L2
    intro n
  3. L3
    intro hd
02Establish hdivL4–6

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply division remainder exists.

  1. L4
    have hdiv : ∃ q. ∃ r. DivRem(n,d,q,r)Definitions: DivRem(n,d,q,r)Original native command in the exact edition
  2. L5
    apply division_remainder_exists
  3. L6
    exact hd
03Separate the logical casesL7–9

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

  1. L7
    cases hdiv
  2. L8
    cases hdiv_witness
  3. L9
    cases hdiv_witness_witness
04Use earlier factsL10–11

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

  1. L10
    specialize eq_decidable x1
  2. L11
    specialize eq_decidable 0
05Establish hrL12–13

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

  1. L12
    have hr : x1 = 0 \/ ~(x1 = 0)
  2. L13
    apply eq_decidable
06Separate the logical casesL14–15

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

  1. L14
    cases hr
  2. L15
    left
07Construct an explicit witnessL16–16

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

  1. L16
    exists x
08Calculate and transport equalitiesL17–18

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

  1. L17
    rewrite hr_left at hdiv_witness_witness_left
  2. L18
    rewrite PA3 at hdiv_witness_witness_left
09Use earlier factsL19–19

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

  1. L19
    exact hdiv_witness_witness_left
10Separate the logical casesL20–20

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

  1. L20
    right
11Fix variables and assumptionsL21–21

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

  1. L21
    intro hmul
12Establish hzeroL22–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply multiple has zero remainder.

  1. L22
    have hzero : ∃ q. ∃ r. n = d · q + r ∧ r = 0 ∧ Lt(r,d)Definitions: Lt(r,d)Original native command in the exact edition
  2. L23
    apply multiple_has_zero_remainder
  3. L24
    exact hd
  4. L25
    exact hmul
13Separate the logical casesL26–29

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

  1. L26
    cases hzero
  2. L27
    cases hzero_witness
  3. L28
    cases hzero_witness_witness
  4. L29
    cases hzero_witness_witness_left
14Establish huniqL30–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply division remainder unique.

  1. L30
    have huniq : x = x2 /\ x1 = x3
  2. L31
    apply division_remainder_unique
  3. L32
    exact hdiv_witness_witness_left
  4. L33
    exact hdiv_witness_witness_right
  5. L34
    exact hzero_witness_witness_left_left
  6. L35
    exact hzero_witness_witness_right
15Separate the logical casesL36–36

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

  1. L36
    cases huniq
16Use earlier factsL37–37

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

  1. L37
    apply hr_right
17Calculate and transport equalitiesL38–38

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

  1. L38
    trans x3
18Use earlier factsL39–40

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

  1. L39
    exact huniq_right
  2. L40
    exact hzero_witness_witness_left_right

Library-wide reading audit

Original defined command ledger · 40 lines
  1. 0001intro d
  2. 0002intro n
  3. 0003intro hd
  4. 0004have hdiv : ∃ q. ∃ r. DivRem(n,d,q,r)
    Exact native replay linehave hdiv : exists q r. n = d * q + r /\ S r <= d
  5. 0005apply division_remainder_exists
  6. 0006exact hd
  7. 0007cases hdiv
  8. 0008cases hdiv_witness
  9. 0009cases hdiv_witness_witness
  10. 0010specialize eq_decidable x1
  11. 0011specialize eq_decidable 0
  12. 0012have hr : x1 = 0 \/ ~(x1 = 0)
  13. 0013apply eq_decidable
  14. 0014cases hr
  15. 0015left
  16. 0016exists x
  17. 0017rewrite hr_left at hdiv_witness_witness_left
  18. 0018rewrite PA3 at hdiv_witness_witness_left
  19. 0019exact hdiv_witness_witness_left
  20. 0020right
  21. 0021intro hmul
  22. 0022have hzero : ∃ q. ∃ r. n = d · q + r ∧ r = 0 ∧ Lt(r,d)
    Exact native replay linehave hzero : exists q r. ((n = d * q + r /\ r = 0) /\ S r <= d)
  23. 0023apply multiple_has_zero_remainder
  24. 0024exact hd
  25. 0025exact hmul
  26. 0026cases hzero
  27. 0027cases hzero_witness
  28. 0028cases hzero_witness_witness
  29. 0029cases hzero_witness_witness_left
  30. 0030have huniq : x = x2 /\ x1 = x3
  31. 0031apply division_remainder_unique
  32. 0032exact hdiv_witness_witness_left
  33. 0033exact hdiv_witness_witness_right
  34. 0034exact hzero_witness_witness_left_left
  35. 0035exact hzero_witness_witness_right
  36. 0036cases huniq
  37. 0037apply hr_right
  38. 0038trans x3
  39. 0039exact huniq_right
  40. 0040exact hzero_witness_witness_left_right