BT0020

mul_eq_one_components

Stable · empty-context checked

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

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

Direct prerequisites: mul_zero_left, add_eq_zero_right, one_mul. The authored body proceeds by structural induction (2), intermediate claims (2), equality transport (8).

Proof neighborhood

Direct dependencies

BT0004 mul_zero_left BT000L add_eq_zero_right BT0009 one_mul

Direct dependents

BT002E divisor_one BT002F multiple_antisymm BT006N prime_three BT00RL prime_power_valuation_one_zero

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. 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