BT0024

two_large_factors_impossible

Stable · empty-context checked

Two naturals at least two cannot multiply to two.

Exact expanded PA statement

forall a b. ~(2 = S (S a) * S (S b))

Structural proof guide

Two naturals at least two cannot multiply to two.

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

Proof neighborhood

Direct dependencies

BT0005 mul_succ_left BT001X add_eq_zero_left BT000M mul_eq_zero

Direct dependents

BT0025 prime_two

Formal native tactic body

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

  1. 0001intro a
  2. 0002intro b
  3. 0003intro h
  4. 0004specialize mul_succ_left (S a)
  5. 0005specialize mul_succ_left (S (S b))
  6. 0006rewrite mul_succ_left at h
  7. 0007rewrite PA4 at h
  8. 0008rewrite PA4 at h
  9. 0009have hzero : 0 = S a * S (S b) + b
  10. 0010apply PA2
  11. 0011apply PA2
  12. 0012exact h
  13. 0013have hzero' : S a * S (S b) + b = 0
  14. 0014symm
  15. 0015exact hzero
  16. 0016have hprod : S a * S (S b) = 0
  17. 0017apply add_eq_zero_left
  18. 0018exact hzero'
  19. 0019specialize mul_eq_zero (S a)
  20. 0020specialize mul_eq_zero (S (S b))
  21. 0021have hz : S a = 0 \/ S (S b) = 0
  22. 0022apply mul_eq_zero
  23. 0023exact hprod
  24. 0024cases hz
  25. 0025apply PA1
  26. 0026exact hz_left
  27. 0027apply PA1
  28. 0028exact hz_right