BP0002

bertrand_window_prime_square_exceeds_double

A prime above n has square strictly larger than 2n.

Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not Stable

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.

Exact theorem in conservative defined notation

∀ n. ∀ p. Prime(p) → Lt(n,p) → Lt(n + n,p · p)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Lt(a,b) · 2Prime(p) · 1

Actual proof prerequisites

mul_lt_mul_right_nonzero · checked external prerequisitemul_comm · checked external prerequisitetwo_mul_eq_add_self · checked external prerequisiteprime_two_le · checked external prerequisitemul_le_mul_right · checked external prerequisitelt_of_lt_of_le · checked external prerequisite
Original expanded first-order statement 
forall n p. ((~(p = 1) /\ forall frm_prime_left_bpc_prime frm_prime_right_bpc_prime. p = frm_prime_left_bpc_prime * frm_prime_right_bpc_prime -> frm_prime_left_bpc_prime = 1 \/ frm_prime_right_bpc_prime = 1)) -> (exists bcf_lt_gap_bpc_lower. bcf_lt_gap_bpc_lower + S (n) = p) -> (exists bcf_lt_gap_bpc_square. bcf_lt_gap_bpc_square + S (n + n) = p * p)

Complete unchanged native tactic proof

All 42 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

42 script commands · 7 reading checkpoints · 6 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.

01Fix variables and assumptionsL1–4

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

  1. L1
    intro n
  2. L2
    intro p
  3. L3
    intro hprime
  4. L4
    intro hlower
02Establish hscaledL5–13

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

  1. L5
    have hscaled : exists q. q + S (n * 2) = p * 2
  2. L6
    specialize mul_lt_mul_right_nonzero n
  3. L7
    specialize mul_lt_mul_right_nonzero p
  4. L8
    specialize mul_lt_mul_right_nonzero 2
  5. L9
    apply mul_lt_mul_right_nonzero
  6. L10
    exact hlower
  7. L11
    intro htwozero
  8. L12
    apply PA1
  9. L13
    exact htwozero
03Establish hn_doubleL14–17

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

  1. L14
    have hn_double : n * 2 = n + n
  2. L15
    trans 2 * n
  3. L16
    apply mul_comm
  4. L17
    apply two_mul_eq_add_self
04Establish hp_doubleL18–23

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

  1. L18
    have hp_double : p * 2 = p + p
  2. L19
    trans 2 * p
  3. L20
    apply mul_comm
  4. L21
    apply two_mul_eq_add_self
  5. L22
    rewrite hn_double at hscaled
  6. L23
    rewrite hp_double at hscaled
05Establish htwoL24–27

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

  1. L24
    have htwo : exists q. q + 2 = p
  2. L25
    specialize prime_two_le p
  3. L26
    apply prime_two_le
  4. L27
    exact hprime
06Establish hsquare_boundL28–33

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

  1. L28
    have hsquare_bound : exists q. q + (2 * p) = p * p
  2. L29
    specialize mul_le_mul_right 2
  3. L30
    specialize mul_le_mul_right p
  4. L31
    specialize mul_le_mul_right p
  5. L32
    apply mul_le_mul_right
  6. L33
    exact htwo
07Establish hleftL34–42

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

  1. L34
    have hleft : 2 * p = p + p
  2. L35
    apply two_mul_eq_add_self
  3. L36
    rewrite hleft at hsquare_bound
  4. L37
    specialize lt_of_lt_of_le (n + n)
  5. L38
    specialize lt_of_lt_of_le (p + p)
  6. L39
    specialize lt_of_lt_of_le (p * p)
  7. L40
    apply lt_of_lt_of_le
  8. L41
    exact hscaled
  9. L42
    exact hsquare_bound

Library-wide reading audit

Original defined command ledger · 42 lines
  1. 0001intro n
  2. 0002intro p
  3. 0003intro hprime
  4. 0004intro hlower
  5. 0005have hscaled : exists q. q + S (n * 2) = p * 2
  6. 0006specialize mul_lt_mul_right_nonzero n
  7. 0007specialize mul_lt_mul_right_nonzero p
  8. 0008specialize mul_lt_mul_right_nonzero 2
  9. 0009apply mul_lt_mul_right_nonzero
  10. 0010exact hlower
  11. 0011intro htwozero
  12. 0012apply PA1
  13. 0013exact htwozero
  14. 0014have hn_double : n * 2 = n + n
  15. 0015trans 2 * n
  16. 0016apply mul_comm
  17. 0017apply two_mul_eq_add_self
  18. 0018have hp_double : p * 2 = p + p
  19. 0019trans 2 * p
  20. 0020apply mul_comm
  21. 0021apply two_mul_eq_add_self
  22. 0022rewrite hn_double at hscaled
  23. 0023rewrite hp_double at hscaled
  24. 0024have htwo : exists q. q + 2 = p
  25. 0025specialize prime_two_le p
  26. 0026apply prime_two_le
  27. 0027exact hprime
  28. 0028have hsquare_bound : exists q. q + (2 * p) = p * p
  29. 0029specialize mul_le_mul_right 2
  30. 0030specialize mul_le_mul_right p
  31. 0031specialize mul_le_mul_right p
  32. 0032apply mul_le_mul_right
  33. 0033exact htwo
  34. 0034have hleft : 2 * p = p + p
  35. 0035apply two_mul_eq_add_self
  36. 0036rewrite hleft at hsquare_bound
  37. 0037specialize lt_of_lt_of_le (n + n)
  38. 0038specialize lt_of_lt_of_le (p + p)
  39. 0039specialize lt_of_lt_of_le (p * p)
  40. 0040apply lt_of_lt_of_le
  41. 0041exact hscaled
  42. 0042exact hsquare_bound