BT00RF · Bertrand theorem

ceil_div_six_le_of_upper

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

Any six-multiple upper bound also bounds the 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. ∀ c. CeilDivSix(x,e) → Le(x,6 · c) → Le(e,c)

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 PD0052 CeilDivSix

3 occurrences

In local proof propositions

PD0001 Le PD0002 Lt

4 occurrences

Exact expanded native-PA statement
forall x e c. (((exists bcs_lower_gap_upper_source. bcs_lower_gap_upper_source + (x) = 6 * (e)) /\ exists bcs_upper_gap_upper_source. bcs_upper_gap_upper_source + S (6 * (e)) = (x) + 6)) -> (exists k. k + x = 6 * c) -> exists k. k + e = c

Proof neighborhood

Direct theorem prerequisites

BT001G le_or_lt BT0014 add_le_add_right BT001L mul_le_mul_left BT001D lt_of_lt_of_le BT001B lt_irrefl_expanded

Direct theorem dependents

BT00RI floor_ceil_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

40 script commands · 11 reading checkpoints · 5 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)
le or ltadd 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 c
  4. L4
    intro he
  5. L5
    intro hxc
02Separate the logical casesL6–6

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

  1. L6
    cases he
03Use earlier factsL7–8

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

  1. L7
    specialize le_or_lt e
  2. L8
    specialize le_or_lt c
04Separate the logical casesL9–9

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

  1. L9
    cases le_or_lt
05Use earlier factsL10–10

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

  1. L10
    exact le_or_lt_left
06Separate the logical casesL11–11

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

  1. L11
    exfalso
07Establish hx6L12–17

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

  1. L12
    have hx6 : Le(x + 6,6 · c + 6)Definitions: Le(x + 6,6 · c + 6)Original native command in the exact edition
  2. L13
    specialize add_le_add_right x
  3. L14
    specialize add_le_add_right (6 * c)
  4. L15
    specialize add_le_add_right 6
  5. L16
    apply add_le_add_right
  6. L17
    exact hxc
08Establish hscaledL18–20

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

  1. L18
    have hscaled : Le(6 · S c,6 · e)Definitions: Le(6 · S c,6 · e)Original native command in the exact edition
  2. L19
    apply mul_le_mul_left
  3. L20
    exact le_or_lt_right
09Establish hsuccL21–23

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

  1. L21
    have hsucc : 6 * S c = 6 * c + 6
  2. L22
    apply PA6
  3. L23
    rewrite hsucc at hscaled
10Establish hfirstL24–30

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

  1. L24
    have hfirst : Lt(6 · e,6 · c + 6)Definitions: Lt(6 · e,6 · c + 6)Original native command in the exact edition
  2. L25
    specialize lt_of_lt_of_le (6 * e)
  3. L26
    specialize lt_of_lt_of_le (x + 6)
  4. L27
    specialize lt_of_lt_of_le (6 * c + 6)
  5. L28
    apply lt_of_lt_of_le
  6. L29
    exact he_right
  7. L30
    exact hx6
11Establish hloopL31–40

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

  1. L31
    have hloop : Lt(6 · e,6 · e)Definitions: Lt(6 · e,6 · e)Original native command in the exact edition
  2. L32
    specialize lt_of_lt_of_le (6 * e)
  3. L33
    specialize lt_of_lt_of_le (6 * c + 6)
  4. L34
    specialize lt_of_lt_of_le (6 * e)
  5. L35
    apply lt_of_lt_of_le
  6. L36
    exact hfirst
  7. L37
    exact hscaled
  8. L38
    specialize lt_irrefl_expanded (6 * e)
  9. L39
    apply lt_irrefl_expanded
  10. L40
    exact hloop

Library-wide reading audit

Original defined command ledger · 40 lines
  1. 0001intro x
  2. 0002intro e
  3. 0003intro c
  4. 0004intro he
  5. 0005intro hxc
  6. 0006cases he
  7. 0007specialize le_or_lt e
  8. 0008specialize le_or_lt c
  9. 0009cases le_or_lt
  10. 0010exact le_or_lt_left
  11. 0011exfalso
  12. 0012have hx6 : Le(x + 6,6 · c + 6)
    Exact native replay linehave hx6 : exists k. k + (x + 6) = 6 * c + 6
  13. 0013specialize add_le_add_right x
  14. 0014specialize add_le_add_right (6 * c)
  15. 0015specialize add_le_add_right 6
  16. 0016apply add_le_add_right
  17. 0017exact hxc
  18. 0018have hscaled : Le(6 · S c,6 · e)
    Exact native replay linehave hscaled : exists k. k + 6 * S c = 6 * e
  19. 0019apply mul_le_mul_left
  20. 0020exact le_or_lt_right
  21. 0021have hsucc : 6 * S c = 6 * c + 6
  22. 0022apply PA6
  23. 0023rewrite hsucc at hscaled
  24. 0024have hfirst : Lt(6 · e,6 · c + 6)
    Exact native replay linehave hfirst : exists k. k + S (6 * e) = 6 * c + 6
  25. 0025specialize lt_of_lt_of_le (6 * e)
  26. 0026specialize lt_of_lt_of_le (x + 6)
  27. 0027specialize lt_of_lt_of_le (6 * c + 6)
  28. 0028apply lt_of_lt_of_le
  29. 0029exact he_right
  30. 0030exact hx6
  31. 0031have hloop : Lt(6 · e,6 · e)
    Exact native replay linehave hloop : exists k. k + S (6 * e) = 6 * e
  32. 0032specialize lt_of_lt_of_le (6 * e)
  33. 0033specialize lt_of_lt_of_le (6 * c + 6)
  34. 0034specialize lt_of_lt_of_le (6 * e)
  35. 0035apply lt_of_lt_of_le
  36. 0036exact hfirst
  37. 0037exact hscaled
  38. 0038specialize lt_irrefl_expanded (6 * e)
  39. 0039apply lt_irrefl_expanded
  40. 0040exact hloop