PA000N

mul_eq_one_components

Stable checked-use theorem · independently closed

A product is one only when both natural factors are one.

Exact expanded PA statement

forall a b. a * b = 1 -> a = 1 /\ b = 1

Structural proof guide

Generated structural guide

A product is one only when both natural factors are one.

Use the direct prerequisites mul_zero_left, add_eq_zero_right, one_mul as previously established PA formulas.

The proof proceeds by structural induction (2), intermediate claims (2), equality transport (8).

Referenced ingredients

PA000D mul_zero_left PA0004 add_eq_zero_right PA000M one_mul

Proof neighborhood

Direct dependencies

PA000D mul_zero_left PA0004 add_eq_zero_right PA000M one_mul

Direct dependents

PA000O divisor_one

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  1. 0001intro a
  2. 0002induction a
  3. 0003intro b
  4. 0004intro h
  5. 0005specialize mul_zero_left b
  6. 0006rewrite mul_zero_left at h
  7. 0007exfalso
  8. 0008apply PA1
  9. 0009symm
  10. 0010exact h
  11. 0011intro b
  12. 0012induction b
  13. 0013intro h
  14. 0014rewrite PA5 at h
  15. 0015exfalso
  16. 0016apply PA1
  17. 0017symm
  18. 0018exact h
  19. 0019intro h
  20. 0020rewrite PA6 at h
  21. 0021rewrite PA4 at h
  22. 0022have hz : S a * b + a = 0
  23. 0023apply PA2
  24. 0024exact h
  25. 0025specialize add_eq_zero_right (S a * b)
  26. 0026specialize add_eq_zero_right a
  27. 0027have ha0 : a = 0
  28. 0028apply add_eq_zero_right
  29. 0029exact hz
  30. 0030split
  31. 0031congr
  32. 0032exact ha0
  33. 0033rewrite ha0 at hz
  34. 0034rewrite ha0 at hz
  35. 0035rewrite PA3 at hz
  36. 0036specialize one_mul b
  37. 0037rewrite one_mul at hz
  38. 0038congr
  39. 0039exact hz