BT00SH · Bertrand theorem

division_successor_quotient_by_bit

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

A divisibility bit is exactly the successor quotient increment.

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. ∀ q. ∀ r. ∀ z. ∀ s. ∀ bit. DivRem(n,d,q,r) → DivRem(S n,d,z,s) → bit = 1 ∧ Dvd(d,S n) ∨ bit = 0 ∧ ¬Dvd(d,S n) → z = q + bit

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 PD0007 DivRem

4 occurrences

In local proof propositions

PD0002 Lt

2 occurrences

Exact expanded native-PA statement
forall d n q r z s bit. (((n) = (d) * (q) + (r) /\ exists blsr_lt_gap_quotient_bit_old_bound. blsr_lt_gap_quotient_bit_old_bound + S (r) = (d))) -> (((S n) = (d) * (z) + (s) /\ exists blsr_lt_gap_quotient_bit_new_bound. blsr_lt_gap_quotient_bit_new_bound + S (s) = (d))) -> ((bit = 1 /\ (exists k. S n = d * k)) \/ (bit = 0 /\ ~(exists k. S n = d * k))) -> z = q + bit

Proof neighborhood

Direct theorem prerequisites

BT00SG division_remainder_successor_cases BT000L add_eq_zero_right BT000C succ_ne_zero BT001W multiple_has_zero_remainder BT001U division_remainder_unique BT001V zero_remainder_implies_multiple

Direct theorem dependents

BT00SK power_quotient_successor_pointwise_add

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

99 script commands · 28 reading checkpoints · 6 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 (6)
division remainder successor casesadd eq zero rightsucc ne zeromultiple has zero remainderdivision remainder uniquezero remainder implies multiple
01Fix variables and assumptionsL1–10

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

  1. L1
    intro d
  2. L2
    intro n
  3. L3
    intro q
  4. L4
    intro r
  5. L5
    intro z
  6. L6
    intro s
  7. L7
    intro bit
  8. L8
    intro hold
  9. L9
    intro hnew
  10. L10
    intro hbit
02Establish hcasesL11–20

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

  1. L11
    have hcases : S r = d ∧ (z = S q ∧ s = 0) ∨ Lt(S r,d) ∧ (z = q ∧ s = S r)Definitions: Lt(S r,d)Original native command in the exact edition
  2. L12
    specialize division_remainder_successor_cases d
  3. L13
    specialize division_remainder_successor_cases n
  4. L14
    specialize division_remainder_successor_cases q
  5. L15
    specialize division_remainder_successor_cases r
  6. L16
    specialize division_remainder_successor_cases z
  7. L17
    specialize division_remainder_successor_cases s
  8. L18
    apply division_remainder_successor_cases
  9. L19
    exact hold
  10. L20
    exact hnew
03Separate the logical casesL21–25

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

  1. L21
    cases hbit
  2. L22
    cases hbit_left
  3. L23
    cases hcases
  4. L24
    cases hcases_left
  5. L25
    cases hcases_left_right
04Calculate and transport equalitiesL26–30

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

  1. L26
    rewrite hbit_left_left
  2. L27
    rewrite hcases_left_right_left
  3. L28
    rewrite PA4
  4. L29
    rewrite PA3
  5. L30
    refl
05Separate the logical casesL31–32

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

  1. L31
    cases hcases_right
  2. L32
    cases hcases_right_right
06Establish hd0L33–34

Establish this local claim before using it. It is not an additional assumption.

  1. L33
    have hd0 : ~(d = 0)
  2. L34
    intro hd
07Separate the logical casesL35–36

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

  1. L35
    cases hold
  2. L36
    cases hold_right
08Calculate and transport equalitiesL37–37

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

  1. L37
    rewrite hd at hold_right_witness
09Establish hsr0L38–45

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

  1. L38
    have hsr0 : S r = 0
  2. L39
    specialize add_eq_zero_right x
  3. L40
    specialize add_eq_zero_right (S r)
  4. L41
    apply add_eq_zero_right
  5. L42
    exact hold_right_witness
  6. L43
    specialize succ_ne_zero r
  7. L44
    apply succ_ne_zero
  8. L45
    exact hsr0
10Establish hzeroL46–51

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

  1. L46
    have hzero : ∃ q0. ∃ r0. S n = d · q0 + r0 ∧ r0 = 0 ∧ Lt(r0,d)Definitions: Lt(r0,d)Original native command in the exact edition
  2. L47
    specialize multiple_has_zero_remainder d
  3. L48
    specialize multiple_has_zero_remainder (S n)
  4. L49
    apply multiple_has_zero_remainder
  5. L50
    exact hd0
  6. L51
    exact hbit_left_right
11Separate the logical casesL52–55

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

  1. L52
    cases hzero
  2. L53
    cases hzero_witness
  3. L54
    cases hzero_witness_witness
  4. L55
    cases hzero_witness_witness_left
12Establish huniqueL56–56

Establish this local claim before using it. It is not an additional assumption.

  1. L56
    have hunique : z = x /\ s = x1
13Separate the logical casesL57–57

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

  1. L57
    cases hnew
14Use earlier factsL58–67

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

  1. L58
    specialize division_remainder_unique d
  2. L59
    specialize division_remainder_unique (S n)
  3. L60
    specialize division_remainder_unique z
  4. L61
    specialize division_remainder_unique s
  5. L62
    specialize division_remainder_unique x
  6. L63
    specialize division_remainder_unique x1
  7. L64
    apply division_remainder_unique
  8. L65
    exact hnew_left
  9. L66
    exact hnew_right
  10. L67
    exact hzero_witness_witness_left_left
15Use earlier factsL68–68

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

  1. L68
    exact hzero_witness_witness_right
16Separate the logical casesL69–69

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

  1. L69
    cases hunique
17Establish hs0L70–73

Establish this local claim before using it. It is not an additional assumption.

  1. L70
    have hs0 : s = 0
  2. L71
    trans x1
  3. L72
    exact hunique_right
  4. L73
    exact hzero_witness_witness_left_right
18Separate the logical casesL74–74

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

  1. L74
    exfalso
19Use earlier factsL75–76

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

  1. L75
    specialize succ_ne_zero r
  2. L76
    apply succ_ne_zero
20Calculate and transport equalitiesL77–78

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

  1. L77
    trans s
  2. L78
    symm
21Use earlier factsL79–80

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

  1. L79
    exact hcases_right_right_right
  2. L80
    exact hs0
22Separate the logical casesL81–85

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

  1. L81
    cases hbit_right
  2. L82
    cases hcases
  3. L83
    cases hcases_left
  4. L84
    cases hcases_left_right
  5. L85
    exfalso
23Use earlier factsL86–86

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

  1. L86
    apply hbit_right_right
24Separate the logical casesL87–87

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

  1. L87
    cases hnew
25Calculate and transport equalitiesL88–88

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

  1. L88
    rewrite hcases_left_right_right at hnew_left
26Use earlier factsL89–93

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

  1. L89
    specialize zero_remainder_implies_multiple d
  2. L90
    specialize zero_remainder_implies_multiple (S n)
  3. L91
    specialize zero_remainder_implies_multiple z
  4. L92
    apply zero_remainder_implies_multiple
  5. L93
    exact hnew_left
27Separate the logical casesL94–95

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

  1. L94
    cases hcases_right
  2. L95
    cases hcases_right_right
28Calculate and transport equalitiesL96–99

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

  1. L96
    rewrite hbit_right_left
  2. L97
    rewrite hcases_right_right_left
  3. L98
    rewrite PA3
  4. L99
    refl

Library-wide reading audit

Original defined command ledger · 99 lines
  1. 0001intro d
  2. 0002intro n
  3. 0003intro q
  4. 0004intro r
  5. 0005intro z
  6. 0006intro s
  7. 0007intro bit
  8. 0008intro hold
  9. 0009intro hnew
  10. 0010intro hbit
  11. 0011have hcases : S r = d ∧ (z = S q ∧ s = 0) ∨ Lt(S r,d) ∧ (z = q ∧ s = S r)
    Exact native replay linehave hcases : ((S r = d /\ (z = S q /\ s = 0)) \/ ((exists blsr_lt_gap_quotient_bit_cases_no_carry. blsr_lt_gap_quotient_bit_cases_no_carry + S (S r) = (d)) /\ (z = q /\ s = S r)))
  12. 0012specialize division_remainder_successor_cases d
  13. 0013specialize division_remainder_successor_cases n
  14. 0014specialize division_remainder_successor_cases q
  15. 0015specialize division_remainder_successor_cases r
  16. 0016specialize division_remainder_successor_cases z
  17. 0017specialize division_remainder_successor_cases s
  18. 0018apply division_remainder_successor_cases
  19. 0019exact hold
  20. 0020exact hnew
  21. 0021cases hbit
  22. 0022cases hbit_left
  23. 0023cases hcases
  24. 0024cases hcases_left
  25. 0025cases hcases_left_right
  26. 0026rewrite hbit_left_left
  27. 0027rewrite hcases_left_right_left
  28. 0028rewrite PA4
  29. 0029rewrite PA3
  30. 0030refl
  31. 0031cases hcases_right
  32. 0032cases hcases_right_right
  33. 0033have hd0 : ~(d = 0)
  34. 0034intro hd
  35. 0035cases hold
  36. 0036cases hold_right
  37. 0037rewrite hd at hold_right_witness
  38. 0038have hsr0 : S r = 0
  39. 0039specialize add_eq_zero_right x
  40. 0040specialize add_eq_zero_right (S r)
  41. 0041apply add_eq_zero_right
  42. 0042exact hold_right_witness
  43. 0043specialize succ_ne_zero r
  44. 0044apply succ_ne_zero
  45. 0045exact hsr0
  46. 0046have hzero : ∃ q0. ∃ r0. S n = d · q0 + r0 ∧ r0 = 0 ∧ Lt(r0,d)
    Exact native replay linehave hzero : exists q0 r0. ((S n = d * q0 + r0 /\ r0 = 0) /\ exists gap. gap + S r0 = d)
  47. 0047specialize multiple_has_zero_remainder d
  48. 0048specialize multiple_has_zero_remainder (S n)
  49. 0049apply multiple_has_zero_remainder
  50. 0050exact hd0
  51. 0051exact hbit_left_right
  52. 0052cases hzero
  53. 0053cases hzero_witness
  54. 0054cases hzero_witness_witness
  55. 0055cases hzero_witness_witness_left
  56. 0056have hunique : z = x /\ s = x1
  57. 0057cases hnew
  58. 0058specialize division_remainder_unique d
  59. 0059specialize division_remainder_unique (S n)
  60. 0060specialize division_remainder_unique z
  61. 0061specialize division_remainder_unique s
  62. 0062specialize division_remainder_unique x
  63. 0063specialize division_remainder_unique x1
  64. 0064apply division_remainder_unique
  65. 0065exact hnew_left
  66. 0066exact hnew_right
  67. 0067exact hzero_witness_witness_left_left
  68. 0068exact hzero_witness_witness_right
  69. 0069cases hunique
  70. 0070have hs0 : s = 0
  71. 0071trans x1
  72. 0072exact hunique_right
  73. 0073exact hzero_witness_witness_left_right
  74. 0074exfalso
  75. 0075specialize succ_ne_zero r
  76. 0076apply succ_ne_zero
  77. 0077trans s
  78. 0078symm
  79. 0079exact hcases_right_right_right
  80. 0080exact hs0
  81. 0081cases hbit_right
  82. 0082cases hcases
  83. 0083cases hcases_left
  84. 0084cases hcases_left_right
  85. 0085exfalso
  86. 0086apply hbit_right_right
  87. 0087cases hnew
  88. 0088rewrite hcases_left_right_right at hnew_left
  89. 0089specialize zero_remainder_implies_multiple d
  90. 0090specialize zero_remainder_implies_multiple (S n)
  91. 0091specialize zero_remainder_implies_multiple z
  92. 0092apply zero_remainder_implies_multiple
  93. 0093exact hnew_left
  94. 0094cases hcases_right
  95. 0095cases hcases_right_right
  96. 0096rewrite hbit_right_left
  97. 0097rewrite hcases_right_right_left
  98. 0098rewrite PA3
  99. 0099refl