BT00XG · Bertrand theorem

division_double_quotient_bit

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

Doubling a dividend changes its quotient by one binary carry.

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. ∀ Q. ∀ R. DivRem(n,d,q,r) → DivRem(n + n,d,Q,R) → Q = q + q ∨ Q = S (q + q)

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

PD0007 DivRem

2 occurrences

In local proof propositions

PD0002 Lt

4 occurrences

Exact expanded native-PA statement
forall d n q r Q R. (((n) = (d) * (q) + (r) /\ (exists bcf_lt_gap_bddqb_source_bound. bcf_lt_gap_bddqb_source_bound + S (r) = d))) -> (((n + n) = (d) * (Q) + (R) /\ (exists bcf_lt_gap_bddqb_double_bound. bcf_lt_gap_bddqb_double_bound + S (R) = d))) -> (Q = q + q \/ Q = S (q + q))

Proof neighborhood

Direct theorem prerequisites

BT001G le_or_lt BT001C le_eq_or_lt BT001I lt_not_le BT000W zero_le BT0010 one_le_of_ne_zero BT00MY add_shuffle_middle BT0007 mul_add BT0003 add_assoc BT0002 add_comm BT00XB add_lt_add BT00XC add_lt_cancel_left BT001U division_remainder_unique

Direct theorem dependents

BT00XV double_quotient_carry_choice

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

133 script commands · 29 reading checkpoints · 12 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 (12)
le or ltle eq or ltlt not lezero leone le of ne zeroadd shuffle middlemul addadd assocadd commadd lt addadd lt cancel leftdivision remainder unique
01Fix variables and assumptionsL1–8

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 Q
  6. L6
    intro R
  7. L7
    intro hsource
  8. L8
    intro hdouble
02Separate the logical casesL9–10

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

  1. L9
    cases hsource
  2. L10
    cases hdouble
03Establish hdouble_eqL11–20

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

  1. L11
    have hdouble_eq : n + n = d * (q + q) + (r + r)
  2. L12
    rewrite hsource_left
  3. L13
    rewrite hsource_left
  4. L14
    trans (d * q + d * q) + (r + r)
  5. L15
    apply add_shuffle_middle
  6. L16
    congr
  7. L17
    symm
  8. L18
    apply mul_add
  9. L19
    refl
  10. L20
    specialize le_or_lt (r + r)
04Use earlier factsL21–21

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

  1. L21
    specialize le_or_lt d
05Separate the logical casesL22–22

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

  1. L22
    cases le_or_lt
06Establish hsplitL23–27

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

  1. L23
    have hsplit : r + r = d ∨ Lt(r + r,d)Definitions: Lt(r + r,d)Original native command in the exact edition
  2. L24
    specialize le_eq_or_lt (r + r)
  3. L25
    specialize le_eq_or_lt d
  4. L26
    apply le_eq_or_lt
  5. L27
    exact le_or_lt_left
07Separate the logical casesL28–28

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

  1. L28
    cases hsplit
08Establish hd0L29–37

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

  1. L29
    have hd0 : ~(d = 0)
  2. L30
    intro hd
  3. L31
    rewrite hd at hsource_right
  4. L32
    specialize lt_not_le r
  5. L33
    specialize lt_not_le 0
  6. L34
    apply lt_not_le
  7. L35
    exact hsource_right
  8. L36
    specialize zero_le r
  9. L37
    exact zero_le
09Establish hzero_boundL38–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply one le of ne zero.

  1. L38
    have hzero_bound : Lt(0,d)Definitions: Lt(0,d)Original native command in the exact edition
  2. L39
    specialize one_le_of_ne_zero d
  3. L40
    apply one_le_of_ne_zero
  4. L41
    exact hd0
10Establish hcandidate_eqL42–50

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

  1. L42
    have hcandidate_eq : n + n = d * S (q + q) + 0
  2. L43
    trans d * (q + q) + (r + r)
  3. L44
    exact hdouble_eq
  4. L45
    rewrite hsplit_left
  5. L46
    trans d * S (q + q)
  6. L47
    symm
  7. L48
    apply PA6
  8. L49
    symm
  9. L50
    apply PA3
11Establish huniqueL51–60

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

  1. L51
    have hunique : Q = S (q + q) /\ R = 0
  2. L52
    specialize division_remainder_unique d
  3. L53
    specialize division_remainder_unique (n + n)
  4. L54
    specialize division_remainder_unique Q
  5. L55
    specialize division_remainder_unique R
  6. L56
    specialize division_remainder_unique (S (q + q))
  7. L57
    specialize division_remainder_unique 0
  8. L58
    apply division_remainder_unique
  9. L59
    exact hdouble_left
  10. L60
    exact hdouble_right
12Use earlier factsL61–62

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

  1. L61
    exact hcandidate_eq
  2. L62
    exact hzero_bound
13Separate the logical casesL63–64

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

  1. L63
    cases hunique
  2. L64
    right
14Use earlier factsL65–65

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

  1. L65
    exact hunique_left
15Establish huniqueL66–75

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

  1. L66
    have hunique : Q = q + q /\ R = r + r
  2. L67
    specialize division_remainder_unique d
  3. L68
    specialize division_remainder_unique (n + n)
  4. L69
    specialize division_remainder_unique Q
  5. L70
    specialize division_remainder_unique R
  6. L71
    specialize division_remainder_unique (q + q)
  7. L72
    specialize division_remainder_unique (r + r)
  8. L73
    apply division_remainder_unique
  9. L74
    exact hdouble_left
  10. L75
    exact hdouble_right
16Use earlier factsL76–77

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

  1. L76
    exact hdouble_eq
  2. L77
    exact hsplit_right
17Separate the logical casesL78–79

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

  1. L78
    cases hunique
  2. L79
    left
18Use earlier factsL80–80

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

  1. L80
    exact hunique_left
19Separate the logical casesL81–81

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

  1. L81
    cases le_or_lt_right
20Establish hrrL82–91

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

  1. L82
    have hrr : r + r = d + S x
  2. L83
    trans x + S d
  3. L84
    symm
  4. L85
    exact le_or_lt_right_witness
  5. L86
    trans S (x + d)
  6. L87
    apply PA4
  7. L88
    trans S (d + x)
  8. L89
    congr
  9. L90
    apply add_comm
  10. L91
    symm
21Use earlier factsL92–92

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

  1. L92
    apply PA4
22Establish hsum_ltL93–101

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

  1. L93
    have hsum_lt : Lt(r + r,d + d)Definitions: Lt(r + r,d + d)Original native command in the exact edition
  2. L94
    specialize add_lt_add r
  3. L95
    specialize add_lt_add d
  4. L96
    specialize add_lt_add r
  5. L97
    specialize add_lt_add d
  6. L98
    apply add_lt_add
  7. L99
    exact hsource_right
  8. L100
    exact hsource_right
  9. L101
    rewrite hrr at hsum_lt
23Establish hcarry_boundL102–107

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add lt cancel left.

  1. L102
    have hcarry_bound : Lt(S x,d)Definitions: Lt(S x,d)Original native command in the exact edition
  2. L103
    specialize add_lt_cancel_left d
  3. L104
    specialize add_lt_cancel_left (S x)
  4. L105
    specialize add_lt_cancel_left d
  5. L106
    apply add_lt_cancel_left
  6. L107
    exact hsum_lt
24Establish hcandidate_eqL108–117

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

  1. L108
    have hcandidate_eq : n + n = d * S (q + q) + S x
  2. L109
    trans d * (q + q) + (r + r)
  3. L110
    exact hdouble_eq
  4. L111
    rewrite hrr
  5. L112
    trans (d * (q + q) + d) + S x
  6. L113
    symm
  7. L114
    apply add_assoc
  8. L115
    congr
  9. L116
    symm
  10. L117
    apply PA6
25Calculate and transport equalitiesL118–118

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

  1. L118
    refl
26Establish huniqueL119–128

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

  1. L119
    have hunique : Q = S (q + q) /\ R = S x
  2. L120
    specialize division_remainder_unique d
  3. L121
    specialize division_remainder_unique (n + n)
  4. L122
    specialize division_remainder_unique Q
  5. L123
    specialize division_remainder_unique R
  6. L124
    specialize division_remainder_unique (S (q + q))
  7. L125
    specialize division_remainder_unique (S x)
  8. L126
    apply division_remainder_unique
  9. L127
    exact hdouble_left
  10. L128
    exact hdouble_right
27Use earlier factsL129–130

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

  1. L129
    exact hcandidate_eq
  2. L130
    exact hcarry_bound
28Separate the logical casesL131–132

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

  1. L131
    cases hunique
  2. L132
    right
29Use earlier factsL133–133

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

  1. L133
    exact hunique_left

Library-wide reading audit

Original defined command ledger · 133 lines
  1. 0001intro d
  2. 0002intro n
  3. 0003intro q
  4. 0004intro r
  5. 0005intro Q
  6. 0006intro R
  7. 0007intro hsource
  8. 0008intro hdouble
  9. 0009cases hsource
  10. 0010cases hdouble
  11. 0011have hdouble_eq : n + n = d * (q + q) + (r + r)
  12. 0012rewrite hsource_left
  13. 0013rewrite hsource_left
  14. 0014trans (d * q + d * q) + (r + r)
  15. 0015apply add_shuffle_middle
  16. 0016congr
  17. 0017symm
  18. 0018apply mul_add
  19. 0019refl
  20. 0020specialize le_or_lt (r + r)
  21. 0021specialize le_or_lt d
  22. 0022cases le_or_lt
  23. 0023have hsplit : r + r = d ∨ Lt(r + r,d)
    Exact native replay linehave hsplit : r + r = d \/ exists k. k + S (r + r) = d
  24. 0024specialize le_eq_or_lt (r + r)
  25. 0025specialize le_eq_or_lt d
  26. 0026apply le_eq_or_lt
  27. 0027exact le_or_lt_left
  28. 0028cases hsplit
  29. 0029have hd0 : ~(d = 0)
  30. 0030intro hd
  31. 0031rewrite hd at hsource_right
  32. 0032specialize lt_not_le r
  33. 0033specialize lt_not_le 0
  34. 0034apply lt_not_le
  35. 0035exact hsource_right
  36. 0036specialize zero_le r
  37. 0037exact zero_le
  38. 0038have hzero_bound : Lt(0,d)
    Exact native replay linehave hzero_bound : exists k. k + S 0 = d
  39. 0039specialize one_le_of_ne_zero d
  40. 0040apply one_le_of_ne_zero
  41. 0041exact hd0
  42. 0042have hcandidate_eq : n + n = d * S (q + q) + 0
  43. 0043trans d * (q + q) + (r + r)
  44. 0044exact hdouble_eq
  45. 0045rewrite hsplit_left
  46. 0046trans d * S (q + q)
  47. 0047symm
  48. 0048apply PA6
  49. 0049symm
  50. 0050apply PA3
  51. 0051have hunique : Q = S (q + q) /\ R = 0
  52. 0052specialize division_remainder_unique d
  53. 0053specialize division_remainder_unique (n + n)
  54. 0054specialize division_remainder_unique Q
  55. 0055specialize division_remainder_unique R
  56. 0056specialize division_remainder_unique (S (q + q))
  57. 0057specialize division_remainder_unique 0
  58. 0058apply division_remainder_unique
  59. 0059exact hdouble_left
  60. 0060exact hdouble_right
  61. 0061exact hcandidate_eq
  62. 0062exact hzero_bound
  63. 0063cases hunique
  64. 0064right
  65. 0065exact hunique_left
  66. 0066have hunique : Q = q + q /\ R = r + r
  67. 0067specialize division_remainder_unique d
  68. 0068specialize division_remainder_unique (n + n)
  69. 0069specialize division_remainder_unique Q
  70. 0070specialize division_remainder_unique R
  71. 0071specialize division_remainder_unique (q + q)
  72. 0072specialize division_remainder_unique (r + r)
  73. 0073apply division_remainder_unique
  74. 0074exact hdouble_left
  75. 0075exact hdouble_right
  76. 0076exact hdouble_eq
  77. 0077exact hsplit_right
  78. 0078cases hunique
  79. 0079left
  80. 0080exact hunique_left
  81. 0081cases le_or_lt_right
  82. 0082have hrr : r + r = d + S x
  83. 0083trans x + S d
  84. 0084symm
  85. 0085exact le_or_lt_right_witness
  86. 0086trans S (x + d)
  87. 0087apply PA4
  88. 0088trans S (d + x)
  89. 0089congr
  90. 0090apply add_comm
  91. 0091symm
  92. 0092apply PA4
  93. 0093have hsum_lt : Lt(r + r,d + d)
    Exact native replay linehave hsum_lt : exists k. k + S (r + r) = d + d
  94. 0094specialize add_lt_add r
  95. 0095specialize add_lt_add d
  96. 0096specialize add_lt_add r
  97. 0097specialize add_lt_add d
  98. 0098apply add_lt_add
  99. 0099exact hsource_right
  100. 0100exact hsource_right
  101. 0101rewrite hrr at hsum_lt
  102. 0102have hcarry_bound : Lt(S x,d)
    Exact native replay linehave hcarry_bound : exists k. k + S (S x) = d
  103. 0103specialize add_lt_cancel_left d
  104. 0104specialize add_lt_cancel_left (S x)
  105. 0105specialize add_lt_cancel_left d
  106. 0106apply add_lt_cancel_left
  107. 0107exact hsum_lt
  108. 0108have hcandidate_eq : n + n = d * S (q + q) + S x
  109. 0109trans d * (q + q) + (r + r)
  110. 0110exact hdouble_eq
  111. 0111rewrite hrr
  112. 0112trans (d * (q + q) + d) + S x
  113. 0113symm
  114. 0114apply add_assoc
  115. 0115congr
  116. 0116symm
  117. 0117apply PA6
  118. 0118refl
  119. 0119have hunique : Q = S (q + q) /\ R = S x
  120. 0120specialize division_remainder_unique d
  121. 0121specialize division_remainder_unique (n + n)
  122. 0122specialize division_remainder_unique Q
  123. 0123specialize division_remainder_unique R
  124. 0124specialize division_remainder_unique (S (q + q))
  125. 0125specialize division_remainder_unique (S x)
  126. 0126apply division_remainder_unique
  127. 0127exact hdouble_left
  128. 0128exact hdouble_right
  129. 0129exact hcandidate_eq
  130. 0130exact hcarry_bound
  131. 0131cases hunique
  132. 0132right
  133. 0133exact hunique_left