BT0025

prime_two

Stable · empty-context checked

Two is prime in the expanded first-order prime predicate.

Exact expanded PA statement

~(2 = 1) /\ forall a b. 2 = a * b -> a = 1 \/ b = 1

Structural proof guide

Two is prime in the expanded first-order prime predicate.

Direct prerequisites: mul_zero_left, two_large_factors_impossible. The authored body proceeds by structural induction (4), intermediate claims (1), equality transport (2).

Proof neighborhood

Direct dependencies

BT0004 mul_zero_left BT0024 two_large_factors_impossible

Direct dependents

BT0124 bertrand_small_closed_upper

Formal native tactic body

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

  1. 0001split
  2. 0002intro h
  3. 0003have h10 : 1 = 0
  4. 0004apply PA2
  5. 0005exact h
  6. 0006apply PA1
  7. 0007exact h10
  8. 0008intro a
  9. 0009induction b
  10. 0010intro h
  11. 0011rewrite PA5 at h
  12. 0012exfalso
  13. 0013apply PA1
  14. 0014exact h
  15. 0015induction b
  16. 0016intro h
  17. 0017right
  18. 0018refl
  19. 0019induction a
  20. 0020intro h
  21. 0021specialize mul_zero_left (S (S b))
  22. 0022rewrite mul_zero_left at h
  23. 0023exfalso
  24. 0024apply PA1
  25. 0025exact h
  26. 0026induction a
  27. 0027intro h
  28. 0028left
  29. 0029refl
  30. 0030intro h
  31. 0031exfalso
  32. 0032specialize two_large_factors_impossible a
  33. 0033specialize two_large_factors_impossible b
  34. 0034apply two_large_factors_impossible
  35. 0035exact h