BT00R2 · Bertrand theorem

ceil_div_six_functional

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

The two witness inequalities determine a unique ceiling quotient.

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

∀ x. ∀ e. ∀ f. CeilDivSix(x,e) → CeilDivSix(x,f) → e = f

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

PD0052 CeilDivSix

2 occurrences

In local proof propositions

PD0001 Le PD0002 Lt

8 occurrences

Exact expanded native-PA statement
forall x e f. (((exists bcs_lower_gap_functional_left. bcs_lower_gap_functional_left + (x) = 6 * (e)) /\ exists bcs_upper_gap_functional_left. bcs_upper_gap_functional_left + S (6 * (e)) = (x) + 6)) -> (((exists bcs_lower_gap_functional_right. bcs_lower_gap_functional_right + (x) = 6 * (f)) /\ exists bcs_upper_gap_functional_right. bcs_upper_gap_functional_right + S (6 * (f)) = (x) + 6)) -> e = f

Proof neighborhood

Direct theorem prerequisites

BT001H lt_trichotomy BT0014 add_le_add_right BT001L mul_le_mul_left BT001D lt_of_lt_of_le BT001B lt_irrefl_expanded

Direct theorem dependents

BT00R5 ceil_div_six_square_six_step

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

72 script commands · 17 reading checkpoints · 10 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 (5)
lt trichotomyadd le add rightmul le mul leftlt of lt of lelt irrefl expanded
01Fix variables and assumptionsL1–5

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

  1. L1
    intro x
  2. L2
    intro e
  3. L3
    intro f
  4. L4
    intro he
  5. L5
    intro hf
02Separate the logical casesL6–7

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

  1. L6
    cases he
  2. L7
    cases hf
03Use earlier factsL8–9

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

  1. L8
    specialize lt_trichotomy e
  2. L9
    specialize lt_trichotomy f
04Separate the logical casesL10–10

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

  1. L10
    cases lt_trichotomy
05Use earlier factsL11–11

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

  1. L11
    exact lt_trichotomy_left
06Separate the logical casesL12–13

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

  1. L12
    cases lt_trichotomy_right
  2. L13
    exfalso
07Establish hx6L14–19

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

  1. L14
    have hx6 : Le(x + 6,6 · e + 6)Definitions: Le(x + 6,6 · e + 6)Original native command in the exact edition
  2. L15
    specialize add_le_add_right x
  3. L16
    specialize add_le_add_right (6 * e)
  4. L17
    specialize add_le_add_right 6
  5. L18
    apply add_le_add_right
  6. L19
    exact he_left
08Establish hscaledL20–22

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

  1. L20
    have hscaled : Le(6 · S e,6 · f)Definitions: Le(6 · S e,6 · f)Original native command in the exact edition
  2. L21
    apply mul_le_mul_left
  3. L22
    exact lt_trichotomy_right_left
09Establish hsucceL23–25

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

  1. L23
    have hsucce : 6 * S e = 6 * e + 6
  2. L24
    apply PA6
  3. L25
    rewrite hsucce at hscaled
10Establish hfirstL26–32

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

  1. L26
    have hfirst : Lt(6 · f,6 · e + 6)Definitions: Lt(6 · f,6 · e + 6)Original native command in the exact edition
  2. L27
    specialize lt_of_lt_of_le (6 * f)
  3. L28
    specialize lt_of_lt_of_le (x + 6)
  4. L29
    specialize lt_of_lt_of_le (6 * e + 6)
  5. L30
    apply lt_of_lt_of_le
  6. L31
    exact hf_right
  7. L32
    exact hx6
11Establish hloopL33–42

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

  1. L33
    have hloop : Lt(6 · f,6 · f)Definitions: Lt(6 · f,6 · f)Original native command in the exact edition
  2. L34
    specialize lt_of_lt_of_le (6 * f)
  3. L35
    specialize lt_of_lt_of_le (6 * e + 6)
  4. L36
    specialize lt_of_lt_of_le (6 * f)
  5. L37
    apply lt_of_lt_of_le
  6. L38
    exact hfirst
  7. L39
    exact hscaled
  8. L40
    specialize lt_irrefl_expanded (6 * f)
  9. L41
    apply lt_irrefl_expanded
  10. L42
    exact hloop
12Separate the logical casesL43–43

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

  1. L43
    exfalso
13Establish hx6L44–49

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

  1. L44
    have hx6 : Le(x + 6,6 · f + 6)Definitions: Le(x + 6,6 · f + 6)Original native command in the exact edition
  2. L45
    specialize add_le_add_right x
  3. L46
    specialize add_le_add_right (6 * f)
  4. L47
    specialize add_le_add_right 6
  5. L48
    apply add_le_add_right
  6. L49
    exact hf_left
14Establish hscaledL50–52

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

  1. L50
    have hscaled : Le(6 · S f,6 · e)Definitions: Le(6 · S f,6 · e)Original native command in the exact edition
  2. L51
    apply mul_le_mul_left
  3. L52
    exact lt_trichotomy_right_right
15Establish hsuccfL53–55

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

  1. L53
    have hsuccf : 6 * S f = 6 * f + 6
  2. L54
    apply PA6
  3. L55
    rewrite hsuccf at hscaled
16Establish hfirstL56–62

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

  1. L56
    have hfirst : Lt(6 · e,6 · f + 6)Definitions: Lt(6 · e,6 · f + 6)Original native command in the exact edition
  2. L57
    specialize lt_of_lt_of_le (6 * e)
  3. L58
    specialize lt_of_lt_of_le (x + 6)
  4. L59
    specialize lt_of_lt_of_le (6 * f + 6)
  5. L60
    apply lt_of_lt_of_le
  6. L61
    exact he_right
  7. L62
    exact hx6
17Establish hloopL63–72

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

  1. L63
    have hloop : Lt(6 · e,6 · e)Definitions: Lt(6 · e,6 · e)Original native command in the exact edition
  2. L64
    specialize lt_of_lt_of_le (6 * e)
  3. L65
    specialize lt_of_lt_of_le (6 * f + 6)
  4. L66
    specialize lt_of_lt_of_le (6 * e)
  5. L67
    apply lt_of_lt_of_le
  6. L68
    exact hfirst
  7. L69
    exact hscaled
  8. L70
    specialize lt_irrefl_expanded (6 * e)
  9. L71
    apply lt_irrefl_expanded
  10. L72
    exact hloop

Library-wide reading audit

Original defined command ledger · 72 lines
  1. 0001intro x
  2. 0002intro e
  3. 0003intro f
  4. 0004intro he
  5. 0005intro hf
  6. 0006cases he
  7. 0007cases hf
  8. 0008specialize lt_trichotomy e
  9. 0009specialize lt_trichotomy f
  10. 0010cases lt_trichotomy
  11. 0011exact lt_trichotomy_left
  12. 0012cases lt_trichotomy_right
  13. 0013exfalso
  14. 0014have hx6 : Le(x + 6,6 · e + 6)
    Exact native replay linehave hx6 : exists k. k + (x + 6) = 6 * e + 6
  15. 0015specialize add_le_add_right x
  16. 0016specialize add_le_add_right (6 * e)
  17. 0017specialize add_le_add_right 6
  18. 0018apply add_le_add_right
  19. 0019exact he_left
  20. 0020have hscaled : Le(6 · S e,6 · f)
    Exact native replay linehave hscaled : exists k. k + 6 * S e = 6 * f
  21. 0021apply mul_le_mul_left
  22. 0022exact lt_trichotomy_right_left
  23. 0023have hsucce : 6 * S e = 6 * e + 6
  24. 0024apply PA6
  25. 0025rewrite hsucce at hscaled
  26. 0026have hfirst : Lt(6 · f,6 · e + 6)
    Exact native replay linehave hfirst : exists k. k + S (6 * f) = 6 * e + 6
  27. 0027specialize lt_of_lt_of_le (6 * f)
  28. 0028specialize lt_of_lt_of_le (x + 6)
  29. 0029specialize lt_of_lt_of_le (6 * e + 6)
  30. 0030apply lt_of_lt_of_le
  31. 0031exact hf_right
  32. 0032exact hx6
  33. 0033have hloop : Lt(6 · f,6 · f)
    Exact native replay linehave hloop : exists k. k + S (6 * f) = 6 * f
  34. 0034specialize lt_of_lt_of_le (6 * f)
  35. 0035specialize lt_of_lt_of_le (6 * e + 6)
  36. 0036specialize lt_of_lt_of_le (6 * f)
  37. 0037apply lt_of_lt_of_le
  38. 0038exact hfirst
  39. 0039exact hscaled
  40. 0040specialize lt_irrefl_expanded (6 * f)
  41. 0041apply lt_irrefl_expanded
  42. 0042exact hloop
  43. 0043exfalso
  44. 0044have hx6 : Le(x + 6,6 · f + 6)
    Exact native replay linehave hx6 : exists k. k + (x + 6) = 6 * f + 6
  45. 0045specialize add_le_add_right x
  46. 0046specialize add_le_add_right (6 * f)
  47. 0047specialize add_le_add_right 6
  48. 0048apply add_le_add_right
  49. 0049exact hf_left
  50. 0050have hscaled : Le(6 · S f,6 · e)
    Exact native replay linehave hscaled : exists k. k + 6 * S f = 6 * e
  51. 0051apply mul_le_mul_left
  52. 0052exact lt_trichotomy_right_right
  53. 0053have hsuccf : 6 * S f = 6 * f + 6
  54. 0054apply PA6
  55. 0055rewrite hsuccf at hscaled
  56. 0056have hfirst : Lt(6 · e,6 · f + 6)
    Exact native replay linehave hfirst : exists k. k + S (6 * e) = 6 * f + 6
  57. 0057specialize lt_of_lt_of_le (6 * e)
  58. 0058specialize lt_of_lt_of_le (x + 6)
  59. 0059specialize lt_of_lt_of_le (6 * f + 6)
  60. 0060apply lt_of_lt_of_le
  61. 0061exact he_right
  62. 0062exact hx6
  63. 0063have hloop : Lt(6 · e,6 · e)
    Exact native replay linehave hloop : exists k. k + S (6 * e) = 6 * e
  64. 0064specialize lt_of_lt_of_le (6 * e)
  65. 0065specialize lt_of_lt_of_le (6 * f + 6)
  66. 0066specialize lt_of_lt_of_le (6 * e)
  67. 0067apply lt_of_lt_of_le
  68. 0068exact hfirst
  69. 0069exact hscaled
  70. 0070specialize lt_irrefl_expanded (6 * e)
  71. 0071apply lt_irrefl_expanded
  72. 0072exact hloop