BT0126

bertrand_upper_endpoint_factorization

Alpha body-checked · checked-use disabled

The closed upper endpoint is composite whenever 1<n.

Exact expanded PA statement

forall n p. (exists bpr_gap_bbp02_boundary_lower. bpr_gap_bbp02_boundary_lower + S (1) = n) -> ((~(p = 1) /\ forall bpr_left_bbp02_boundary_prime bpr_right_bbp02_boundary_prime. p = bpr_left_bbp02_boundary_prime * bpr_right_bbp02_boundary_prime -> bpr_left_bbp02_boundary_prime = 1 \/ bpr_right_bbp02_boundary_prime = 1)) -> p = n + n -> false

Structural proof guide

The closed upper endpoint is composite whenever 1<n.

Direct prerequisites: lt_not_le, zero_add, two_mul_eq_add_self, fixed_nontrivial_factor_not_prime. The authored body proceeds by intermediate claims (3), equality transport (1).

Proof neighborhood

Direct dependencies

BT001I lt_not_le BT0000 zero_add BT00QU two_mul_eq_add_self BT0116 fixed_nontrivial_factor_not_prime

Direct dependents

BT0127 bertrand_strict

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 p
  3. 0003intro hlower
  4. 0004intro hprime
  5. 0005intro heq
  6. 0006have hn_not_one : ~(n = 1)
  7. 0007intro hn_one
  8. 0008specialize lt_not_le 1
  9. 0009specialize lt_not_le n
  10. 0010apply lt_not_le
  11. 0011exact hlower
  12. 0012exists 0
  13. 0013rewrite hn_one
  14. 0014apply zero_add
  15. 0015have htwo_not_one : ~(2 = 1)
  16. 0016intro htwo_one
  17. 0017apply PA1
  18. 0018apply PA2
  19. 0019exact htwo_one
  20. 0020have hfactor : p = 2 * n
  21. 0021trans n + n
  22. 0022exact heq
  23. 0023symm
  24. 0024specialize two_mul_eq_add_self n
  25. 0025exact two_mul_eq_add_self
  26. 0026specialize fixed_nontrivial_factor_not_prime p
  27. 0027specialize fixed_nontrivial_factor_not_prime 2
  28. 0028specialize fixed_nontrivial_factor_not_prime n
  29. 0029apply fixed_nontrivial_factor_not_prime
  30. 0030exact hfactor
  31. 0031exact htwo_not_one
  32. 0032exact hn_not_one
  33. 0033exact hprime