BT0127

bertrand_strict

Alpha body-checked · checked-use disabled

Every n greater than one has a prime strictly below n+n.

Exact expanded PA statement

forall n. (exists h. h + S 1 = n) -> exists p. ((~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1) /\ ((exists u. u + S n = p) /\ (exists v. v + S p = n + n)))

Structural proof guide

Every n greater than one has a prime strictly below n+n.

Direct prerequisites: add_eq_zero_right, bertrand_closed_upper, le_eq_or_lt, bertrand_upper_endpoint_factorization. The authored body proceeds by case analysis (5), intermediate claims (4), equality transport (1).

Proof neighborhood

Direct dependencies

BT000L add_eq_zero_right BT0125 bertrand_closed_upper BT001C le_eq_or_lt BT0126 bertrand_upper_endpoint_factorization

Direct dependents

none

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro n
  2. 0002intro hlower
  3. 0003have hn_nonzero : ~(n = 0)
  4. 0004intro hn_zero
  5. 0005cases hlower
  6. 0006rewrite hn_zero at hlower_witness
  7. 0007have htwo_zero : 2 = 0
  8. 0008specialize add_eq_zero_right x
  9. 0009specialize add_eq_zero_right 2
  10. 0010apply add_eq_zero_right
  11. 0011exact hlower_witness
  12. 0012apply PA1
  13. 0013exact htwo_zero
  14. 0014have hclosed : exists x. ((~(x = 1) /\ forall bpr_left_bbp02_closed_prime bpr_right_bbp02_closed_prime. x = bpr_left_bbp02_closed_prime * bpr_right_bbp02_closed_prime -> bpr_left_bbp02_closed_prime = 1 \/ bpr_right_bbp02_closed_prime = 1)) /\ ((exists bpr_gap_bbp02_closed_lower. bpr_gap_bbp02_closed_lower + S (n) = x) /\ (exists bpr_le_gap_bbp02_closed_upper. bpr_le_gap_bbp02_closed_upper + (x) = (n + n)))
  15. 0015specialize bertrand_closed_upper n
  16. 0016apply bertrand_closed_upper
  17. 0017exact hn_nonzero
  18. 0018cases hclosed
  19. 0019cases hclosed_witness
  20. 0020cases hclosed_witness_right
  21. 0021have hsplit : x = n + n \/ (exists v. v + S x = n + n)
  22. 0022specialize le_eq_or_lt x
  23. 0023specialize le_eq_or_lt (n + n)
  24. 0024apply le_eq_or_lt
  25. 0025exact hclosed_witness_right_right
  26. 0026cases hsplit
  27. 0027exfalso
  28. 0028specialize bertrand_upper_endpoint_factorization n
  29. 0029specialize bertrand_upper_endpoint_factorization x
  30. 0030apply bertrand_upper_endpoint_factorization
  31. 0031exact hlower
  32. 0032exact hclosed_witness_left
  33. 0033exact hsplit_left
  34. 0034exists x
  35. 0035split
  36. 0036exact hclosed_witness_left
  37. 0037split
  38. 0038exact hclosed_witness_right_left
  39. 0039exact hsplit_right