BT00RG · Bertrand theorem

double_triple_remainder_complement_budget

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

The equation 2*n=3*q+r constructively yields q+c=n and 2*n<=6*c.

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

∀ n. ∀ q. ∀ r. 2 · n = 3 · q + r → ∃ x. q + x = n ∧ Le(2 · n,6 · x)

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

PD0001 Le

1 occurrences

In local proof propositions

PD0001 Le PD0002 Lt

10 occurrences

Exact expanded native-PA statement
forall n q r. 2 * n = 3 * q + r -> exists c. ((((q) + (c) = (n)) /\ exists bqb_budget_gap_strong_result. bqb_budget_gap_strong_result + 2 * (n) = 6 * (c)))

Proof neighborhood

Direct theorem prerequisites

BT001M mul_le_mul_right BT0013 le_add_right BT000F le_trans BT000C succ_ne_zero BT00RD mul_le_cancel_left_nonzero BT0002 add_comm BT0007 mul_add BT00RE three_mul_eq_two_mul_add_self BT0003 add_assoc BT000V add_left_cancel BT0014 add_le_add_right BT001L mul_le_mul_left BT0008 mul_assoc

Direct theorem dependents

BT00RH canonical_double_triple_remainder_complement_budget

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

94 script commands · 32 reading checkpoints · 18 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 (13)
mul le mul rightle add rightle transsucc ne zeromul le cancel left nonzeroadd commmul addthree mul eq two mul add selfadd assocadd left canceladd le add rightmul le mul leftmul assoc
01Fix variables and assumptionsL1–4

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

  1. L1
    intro n
  2. L2
    intro q
  3. L3
    intro r
  4. L4
    intro hdiv
02Establish hcoeffL5–5

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

  1. L5
    have hcoeff : Lt(1,3)Definitions: Lt(1,3)Original native command in the exact edition
03Construct an explicit witnessL6–6

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

  1. L6
    exists 1
04Calculate and transport equalitiesL7–7

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

  1. L7
    norm_num
05Establish h23L8–13

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

  1. L8
    have h23 : Le(2 · q,3 · q)Definitions: Le(2 · q,3 · q)Original native command in the exact edition
  2. L9
    specialize mul_le_mul_right 2
  3. L10
    specialize mul_le_mul_right 3
  4. L11
    specialize mul_le_mul_right q
  5. L12
    apply mul_le_mul_right
  6. L13
    exact hcoeff
06Establish h3rL14–15

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

  1. L14
    have h3r : Le(3 · q,3 · q + r)Definitions: Le(3 · q,3 · q + r)Original native command in the exact edition
  2. L15
    apply le_add_right
07Establish hpreL16–22

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

  1. L16
    have hpre : Le(2 · q,3 · q + r)Definitions: Le(2 · q,3 · q + r)Original native command in the exact edition
  2. L17
    specialize le_trans (2 * q)
  3. L18
    specialize le_trans (3 * q)
  4. L19
    specialize le_trans (3 * q + r)
  5. L20
    apply le_trans
  6. L21
    exact h23
  7. L22
    exact h3r
08Establish h2nL23–25

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

  1. L23
    have h2n : Le(2 · q,2 · n)Definitions: Le(2 · q,2 · n)Original native command in the exact edition
  2. L24
    rewrite hdiv
  3. L25
    exact hpre
09Establish htwo0L26–30

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

  1. L26
    have htwo0 : ~(2 = 0)
  2. L27
    intro hzero
  3. L28
    specialize succ_ne_zero 1
  4. L29
    apply succ_ne_zero
  5. L30
    exact hzero
10Establish hqnL31–37

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

  1. L31
  2. L32
    specialize mul_le_cancel_left_nonzero 2
  3. L33
    specialize mul_le_cancel_left_nonzero q
  4. L34
    specialize mul_le_cancel_left_nonzero n
  5. L35
    apply mul_le_cancel_left_nonzero
  6. L36
    exact htwo0
  7. L37
    exact h2n
11Separate the logical casesL38–38

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

  1. L38
    cases hqn
12Establish hcompL39–42

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

  1. L39
    have hcomp : q + x = n
  2. L40
    trans x + q
  3. L41
    apply add_comm
  4. L42
    exact hqn_witness
13Establish hbalanceL43–48

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

  1. L43
    have hbalance : 2 * q + 2 * x = 3 * q + r
  2. L44
    trans 2 * (q + x)
  3. L45
    symm
  4. L46
    apply mul_add
  5. L47
    rewrite hcomp
  6. L48
    exact hdiv
14Establish hthreeqL49–50

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply three mul eq two mul add self.

  1. L49
    have hthreeq : 3 * q = 2 * q + q
  2. L50
    apply three_mul_eq_two_mul_add_self
15Establish hbalance2L51–55

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

  1. L51
    have hbalance2 : 2 * q + 2 * x = 2 * q + (q + r)
  2. L52
    trans 3 * q + r
  3. L53
    exact hbalance
  4. L54
    rewrite hthreeq
  5. L55
    apply add_assoc
16Establish hreduceL56–61

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

  1. L56
    have hreduce : 2 * x = q + r
  2. L57
    specialize add_left_cancel (2 * q)
  3. L58
    specialize add_left_cancel (2 * x)
  4. L59
    specialize add_left_cancel (q + r)
  5. L60
    apply add_left_cancel
  6. L61
    exact hbalance2
17Establish hq2cL62–62

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

  1. L62
18Construct an explicit witnessL63–63

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

  1. L63
    exists r
19Calculate and transport equalitiesL64–64

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

  1. L64
    trans q + r
20Use earlier factsL65–65

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

  1. L65
    apply add_comm
21Calculate and transport equalitiesL66–66

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

  1. L66
    symm
22Use earlier factsL67–67

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

  1. L67
    exact hreduce
23Establish hplusL68–73

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

  1. L68
    have hplus : Le(q + x,2 · x + x)Definitions: Le(q + x,2 · x + x)Original native command in the exact edition
  2. L69
    specialize add_le_add_right q
  3. L70
    specialize add_le_add_right (2 * x)
  4. L71
    specialize add_le_add_right x
  5. L72
    apply add_le_add_right
  6. L73
    exact hq2c
24Establish hthreexL74–75

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply three mul eq two mul add self.

  1. L74
    have hthreex : 3 * x = 2 * x + x
  2. L75
    apply three_mul_eq_two_mul_add_self
25Establish hn3cL76–79

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

  1. L76
  2. L77
    rewrite <- hcomp
  3. L78
    rewrite hthreex
  4. L79
    exact hplus
26Establish hscaledL80–82

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

  1. L80
    have hscaled : Le(2 · n,2 · (3 · x))Definitions: Le(2 · n,2 · (3 · x))Original native command in the exact edition
  2. L81
    apply mul_le_mul_left
  3. L82
    exact hn3c
27Establish hfactorL83–89

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

  1. L83
    have hfactor : 2 * (3 * x) = 6 * x
  2. L84
    trans (2 * 3) * x
  3. L85
    symm
  4. L86
    apply mul_assoc
  5. L87
    congr
  6. L88
    norm_num
  7. L89
    refl
28Construct an explicit witnessL90–90

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

  1. L90
    exists x
29Separate the logical casesL91–91

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

  1. L91
    split
30Use earlier factsL92–92

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

  1. L92
    exact hcomp
31Calculate and transport equalitiesL93–93

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

  1. L93
    rewrite hfactor at hscaled
32Use earlier factsL94–94

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

  1. L94
    exact hscaled

Library-wide reading audit

Original defined command ledger · 94 lines
  1. 0001intro n
  2. 0002intro q
  3. 0003intro r
  4. 0004intro hdiv
  5. 0005have hcoeff : Lt(1,3)
    Exact native replay linehave hcoeff : exists k. k + 2 = 3
  6. 0006exists 1
  7. 0007norm_num
  8. 0008have h23 : Le(2 · q,3 · q)
    Exact native replay linehave h23 : exists k. k + 2 * q = 3 * q
  9. 0009specialize mul_le_mul_right 2
  10. 0010specialize mul_le_mul_right 3
  11. 0011specialize mul_le_mul_right q
  12. 0012apply mul_le_mul_right
  13. 0013exact hcoeff
  14. 0014have h3r : Le(3 · q,3 · q + r)
    Exact native replay linehave h3r : exists k. k + 3 * q = 3 * q + r
  15. 0015apply le_add_right
  16. 0016have hpre : Le(2 · q,3 · q + r)
    Exact native replay linehave hpre : exists k. k + 2 * q = 3 * q + r
  17. 0017specialize le_trans (2 * q)
  18. 0018specialize le_trans (3 * q)
  19. 0019specialize le_trans (3 * q + r)
  20. 0020apply le_trans
  21. 0021exact h23
  22. 0022exact h3r
  23. 0023have h2n : Le(2 · q,2 · n)
    Exact native replay linehave h2n : exists k. k + 2 * q = 2 * n
  24. 0024rewrite hdiv
  25. 0025exact hpre
  26. 0026have htwo0 : ~(2 = 0)
  27. 0027intro hzero
  28. 0028specialize succ_ne_zero 1
  29. 0029apply succ_ne_zero
  30. 0030exact hzero
  31. 0031have hqn : Le(q,n)
    Exact native replay linehave hqn : exists k. k + q = n
  32. 0032specialize mul_le_cancel_left_nonzero 2
  33. 0033specialize mul_le_cancel_left_nonzero q
  34. 0034specialize mul_le_cancel_left_nonzero n
  35. 0035apply mul_le_cancel_left_nonzero
  36. 0036exact htwo0
  37. 0037exact h2n
  38. 0038cases hqn
  39. 0039have hcomp : q + x = n
  40. 0040trans x + q
  41. 0041apply add_comm
  42. 0042exact hqn_witness
  43. 0043have hbalance : 2 * q + 2 * x = 3 * q + r
  44. 0044trans 2 * (q + x)
  45. 0045symm
  46. 0046apply mul_add
  47. 0047rewrite hcomp
  48. 0048exact hdiv
  49. 0049have hthreeq : 3 * q = 2 * q + q
  50. 0050apply three_mul_eq_two_mul_add_self
  51. 0051have hbalance2 : 2 * q + 2 * x = 2 * q + (q + r)
  52. 0052trans 3 * q + r
  53. 0053exact hbalance
  54. 0054rewrite hthreeq
  55. 0055apply add_assoc
  56. 0056have hreduce : 2 * x = q + r
  57. 0057specialize add_left_cancel (2 * q)
  58. 0058specialize add_left_cancel (2 * x)
  59. 0059specialize add_left_cancel (q + r)
  60. 0060apply add_left_cancel
  61. 0061exact hbalance2
  62. 0062have hq2c : Le(q,2 · x)
    Exact native replay linehave hq2c : exists k. k + q = 2 * x
  63. 0063exists r
  64. 0064trans q + r
  65. 0065apply add_comm
  66. 0066symm
  67. 0067exact hreduce
  68. 0068have hplus : Le(q + x,2 · x + x)
    Exact native replay linehave hplus : exists k. k + (q + x) = 2 * x + x
  69. 0069specialize add_le_add_right q
  70. 0070specialize add_le_add_right (2 * x)
  71. 0071specialize add_le_add_right x
  72. 0072apply add_le_add_right
  73. 0073exact hq2c
  74. 0074have hthreex : 3 * x = 2 * x + x
  75. 0075apply three_mul_eq_two_mul_add_self
  76. 0076have hn3c : Le(n,3 · x)
    Exact native replay linehave hn3c : exists k. k + n = 3 * x
  77. 0077rewrite <- hcomp
  78. 0078rewrite hthreex
  79. 0079exact hplus
  80. 0080have hscaled : Le(2 · n,2 · (3 · x))
    Exact native replay linehave hscaled : exists k. k + 2 * n = 2 * (3 * x)
  81. 0081apply mul_le_mul_left
  82. 0082exact hn3c
  83. 0083have hfactor : 2 * (3 * x) = 6 * x
  84. 0084trans (2 * 3) * x
  85. 0085symm
  86. 0086apply mul_assoc
  87. 0087congr
  88. 0088norm_num
  89. 0089refl
  90. 0090exists x
  91. 0091split
  92. 0092exact hcomp
  93. 0093rewrite hfactor at hscaled
  94. 0094exact hscaled