BT00QD

prime_two_le

Alpha body-checked · checked-use disabled

Every prime is at least two in witness-defined order.

Exact expanded PA statement

forall p. ((~(p = 1) /\ forall frm_prime_left_bpvl_prime frm_prime_right_bpvl_prime. p = frm_prime_left_bpvl_prime * frm_prime_right_bpvl_prime -> frm_prime_left_bpvl_prime = 1 \/ frm_prime_right_bpvl_prime = 1)) -> (exists bpvl_gap_prime_two. bpvl_gap_prime_two + (2) = (p))

Structural proof guide

Every prime is at least two in witness-defined order.

Direct prerequisites: prime_is_succ_succ. The authored body proceeds by case analysis (1), intermediate claims (1), equality transport (3).

Proof neighborhood

Direct dependencies

BT00AW prime_is_succ_succ

Direct dependents

BT00QF prime_power_exponent_le

Formal native tactic body

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

  1. 0001intro p
  2. 0002intro hp
  3. 0003have hshape : exists k. p = S (S k)
  4. 0004specialize prime_is_succ_succ p
  5. 0005apply prime_is_succ_succ
  6. 0006exact hp
  7. 0007cases hshape
  8. 0008exists x
  9. 0009trans S (S x)
  10. 0010rewrite PA4
  11. 0011rewrite PA4
  12. 0012rewrite PA3
  13. 0013refl
  14. 0014symm
  15. 0015exact hshape_witness