BT00YB · Bertrand theorem

division_first_two_of_two_three_range

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

The two-thirds range fixes the first quotients at one and two.

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

∀ p. ∀ n. Le(p,n) → Lt(n + n,p + p + p) → ∃ x. ∃ y. DivRem(n,p,1,x) ∧ DivRem(n + n,p,2,y)

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

4 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0007 DivRem

8 occurrences

Exact expanded native-PA statement
forall p n. (exists bcf_le_gap_bdftt_lower. bcf_le_gap_bdftt_lower + (p) = n) -> (exists bcf_lt_gap_bdftt_scaled. bcf_lt_gap_bdftt_scaled + S (n + n) = (p + p) + p) -> exists r R. (((n) = (p) * (1) + (r) /\ (exists bcf_lt_gap_bdftt_left_bound. bcf_lt_gap_bdftt_left_bound + S (r) = p))) /\ (((n + n) = (p) * (2) + (R) /\ (exists bcf_lt_gap_bdftt_right_bound. bcf_lt_gap_bdftt_right_bound + S (R) = p)))

Proof neighborhood

Direct theorem prerequisites

BT0014 add_le_add_right BT0015 add_le_add_left BT000F le_trans BT001E lt_of_le_of_lt BT0002 add_comm BT00XC add_lt_cancel_left BT00Y8 division_quotient_one_of_bounds BT00Y9 division_quotient_two_of_bounds

Direct theorem dependents

BT00YE central_binom_prime_valuation_zero_two_thirds_range

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

67 script commands · 16 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 (8)
add le add rightadd le add leftle translt of le of ltadd commadd lt cancel leftdivision quotient one of boundsdivision quotient two of bounds
01Fix variables and assumptionsL1–4

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro hlower
  4. L4
    intro hscaled
02Establish hdouble_lowerL5–5

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

  1. L5
    have hdouble_lower : Le(p + p,n + n)Definitions: Le(p + p,n + n)Original native command in the exact edition
03Establish hdouble_leftL6–11

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

  1. L6
    have hdouble_left : Le(p + p,n + p)Definitions: Le(p + p,n + p)Original native command in the exact edition
  2. L7
    specialize add_le_add_right p
  3. L8
    specialize add_le_add_right n
  4. L9
    specialize add_le_add_right p
  5. L10
    apply add_le_add_right
  6. L11
    exact hlower
04Establish hshift_lowerL12–21

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

  1. L12
    have hshift_lower : Le(n + p,n + n)Definitions: Le(n + p,n + n)Original native command in the exact edition
  2. L13
    specialize add_le_add_left p
  3. L14
    specialize add_le_add_left n
  4. L15
    specialize add_le_add_left n
  5. L16
    apply add_le_add_left
  6. L17
    exact hlower
  7. L18
    specialize le_trans (p + p)
  8. L19
    specialize le_trans (n + p)
  9. L20
    specialize le_trans (n + n)
  10. L21
    apply le_trans
05Use earlier factsL22–23

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

  1. L22
    exact hdouble_left
  2. L23
    exact hshift_lower
06Establish hshift_lowerL24–29

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

  1. L24
    have hshift_lower : Le(n + p,n + n)Definitions: Le(n + p,n + n)Original native command in the exact edition
  2. L25
    specialize add_le_add_left p
  3. L26
    specialize add_le_add_left n
  4. L27
    specialize add_le_add_left n
  5. L28
    apply add_le_add_left
  6. L29
    exact hlower
07Establish hshift_strictL30–36

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

  1. L30
    have hshift_strict : Lt(n + p,p + p + p)Definitions: Lt(n + p,p + p + p)Original native command in the exact edition
  2. L31
    specialize lt_of_le_of_lt (n + p)
  3. L32
    specialize lt_of_le_of_lt (n + n)
  4. L33
    specialize lt_of_le_of_lt ((p + p) + p)
  5. L34
    apply lt_of_le_of_lt
  6. L35
    exact hshift_lower
  7. L36
    exact hscaled
08Establish hleft_commL37–39

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

  1. L37
    have hleft_comm : n + p = p + n
  2. L38
    apply add_comm
  3. L39
    rewrite hleft_comm at hshift_strict
09Establish hright_commL40–42

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

  1. L40
    have hright_comm : (p + p) + p = p + (p + p)
  2. L41
    apply add_comm
  3. L42
    rewrite hright_comm at hshift_strict
10Establish hfirst_upperL43–48

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

  1. L43
    have hfirst_upper : Lt(n,p + p)Definitions: Lt(n,p + p)Original native command in the exact edition
  2. L44
    specialize add_lt_cancel_left p
  3. L45
    specialize add_lt_cancel_left n
  4. L46
    specialize add_lt_cancel_left (p + p)
  5. L47
    apply add_lt_cancel_left
  6. L48
    exact hshift_strict
11Establish hfirstL49–54

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply division quotient one of bounds.

  1. L49
    have hfirst : ∃ r. DivRem(n,p,1,r)Definitions: DivRem(n,p,1,r)Original native command in the exact edition
  2. L50
    specialize division_quotient_one_of_bounds p
  3. L51
    specialize division_quotient_one_of_bounds n
  4. L52
    apply division_quotient_one_of_bounds
  5. L53
    exact hlower
  6. L54
    exact hfirst_upper
12Establish hsecondL55–60

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply division quotient two of bounds.

  1. L55
    have hsecond : ∃ R. DivRem(n + n,p,2,R)Definitions: DivRem(n + n,p,2,R)Original native command in the exact edition
  2. L56
    specialize division_quotient_two_of_bounds p
  3. L57
    specialize division_quotient_two_of_bounds (n + n)
  4. L58
    apply division_quotient_two_of_bounds
  5. L59
    exact hdouble_lower
  6. L60
    exact hscaled
13Separate the logical casesL61–62

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

  1. L61
    cases hfirst
  2. L62
    cases hsecond
14Construct an explicit witnessL63–64

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

  1. L63
    exists x
  2. L64
    exists x1
15Separate the logical casesL65–65

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

  1. L65
    split
16Use earlier factsL66–67

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

  1. L66
    exact hfirst_witness
  2. L67
    exact hsecond_witness

Library-wide reading audit

Original defined command ledger · 67 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro hlower
  4. 0004intro hscaled
  5. 0005have hdouble_lower : Le(p + p,n + n)
    Exact native replay linehave hdouble_lower : exists bcf_le_gap_bdftt_double_lower. bcf_le_gap_bdftt_double_lower + (p + p) = n + n
  6. 0006have hdouble_left : Le(p + p,n + p)
    Exact native replay linehave hdouble_left : exists bcf_le_gap_bdftt_double_left. bcf_le_gap_bdftt_double_left + (p + p) = n + p
  7. 0007specialize add_le_add_right p
  8. 0008specialize add_le_add_right n
  9. 0009specialize add_le_add_right p
  10. 0010apply add_le_add_right
  11. 0011exact hlower
  12. 0012have hshift_lower : Le(n + p,n + n)
    Exact native replay linehave hshift_lower : exists bcf_le_gap_bdftt_shift_lower. bcf_le_gap_bdftt_shift_lower + (n + p) = n + n
  13. 0013specialize add_le_add_left p
  14. 0014specialize add_le_add_left n
  15. 0015specialize add_le_add_left n
  16. 0016apply add_le_add_left
  17. 0017exact hlower
  18. 0018specialize le_trans (p + p)
  19. 0019specialize le_trans (n + p)
  20. 0020specialize le_trans (n + n)
  21. 0021apply le_trans
  22. 0022exact hdouble_left
  23. 0023exact hshift_lower
  24. 0024have hshift_lower : Le(n + p,n + n)
    Exact native replay linehave hshift_lower : exists bcf_le_gap_bdftt_shift_lower. bcf_le_gap_bdftt_shift_lower + (n + p) = n + n
  25. 0025specialize add_le_add_left p
  26. 0026specialize add_le_add_left n
  27. 0027specialize add_le_add_left n
  28. 0028apply add_le_add_left
  29. 0029exact hlower
  30. 0030have hshift_strict : Lt(n + p,p + p + p)
    Exact native replay linehave hshift_strict : exists bcf_lt_gap_bdftt_shift_strict. bcf_lt_gap_bdftt_shift_strict + S (n + p) = (p + p) + p
  31. 0031specialize lt_of_le_of_lt (n + p)
  32. 0032specialize lt_of_le_of_lt (n + n)
  33. 0033specialize lt_of_le_of_lt ((p + p) + p)
  34. 0034apply lt_of_le_of_lt
  35. 0035exact hshift_lower
  36. 0036exact hscaled
  37. 0037have hleft_comm : n + p = p + n
  38. 0038apply add_comm
  39. 0039rewrite hleft_comm at hshift_strict
  40. 0040have hright_comm : (p + p) + p = p + (p + p)
  41. 0041apply add_comm
  42. 0042rewrite hright_comm at hshift_strict
  43. 0043have hfirst_upper : Lt(n,p + p)
    Exact native replay linehave hfirst_upper : exists bcf_lt_gap_bdftt_upper. bcf_lt_gap_bdftt_upper + S (n) = p + p
  44. 0044specialize add_lt_cancel_left p
  45. 0045specialize add_lt_cancel_left n
  46. 0046specialize add_lt_cancel_left (p + p)
  47. 0047apply add_lt_cancel_left
  48. 0048exact hshift_strict
  49. 0049have hfirst : ∃ r. DivRem(n,p,1,r)
    Exact native replay linehave hfirst : exists r. ((n) = (p) * (1) + (r) /\ (exists bcf_lt_gap_bdftt_left_bound. bcf_lt_gap_bdftt_left_bound + S (r) = p))
  50. 0050specialize division_quotient_one_of_bounds p
  51. 0051specialize division_quotient_one_of_bounds n
  52. 0052apply division_quotient_one_of_bounds
  53. 0053exact hlower
  54. 0054exact hfirst_upper
  55. 0055have hsecond : ∃ R. DivRem(n + n,p,2,R)
    Exact native replay linehave hsecond : exists R. ((n + n) = (p) * (2) + (R) /\ (exists bcf_lt_gap_bdftt_right_bound. bcf_lt_gap_bdftt_right_bound + S (R) = p))
  56. 0056specialize division_quotient_two_of_bounds p
  57. 0057specialize division_quotient_two_of_bounds (n + n)
  58. 0058apply division_quotient_two_of_bounds
  59. 0059exact hdouble_lower
  60. 0060exact hscaled
  61. 0061cases hfirst
  62. 0062cases hsecond
  63. 0063exists x
  64. 0064exists x1
  65. 0065split
  66. 0066exact hfirst_witness
  67. 0067exact hsecond_witness