BT002F

multiple_antisymm

Stable · empty-context checked

Mutual divisibility is antisymmetric over natural numbers.

Exact expanded PA statement

forall a b. (exists x. b = a * x) -> (exists y. a = b * y) -> a = b

Structural proof guide

Mutual divisibility is antisymmetric over natural numbers.

Direct prerequisites: zero_or_succ, mul_zero_left, mul_assoc, mul_one, mul_left_cancel_nonzero, mul_eq_one_components. The authored body proceeds by case analysis (5), intermediate claims (4), equality transport (5).

Proof neighborhood

Direct dependencies

BT000Q zero_or_succ BT0004 mul_zero_left BT0008 mul_assoc BT000A mul_one BT0022 mul_left_cancel_nonzero BT0020 mul_eq_one_components

Direct dependents

BT0105 prime_contribution_product_eq

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 hab
  4. 0004intro hba
  5. 0005cases hab
  6. 0006cases hba
  7. 0007specialize zero_or_succ a
  8. 0008cases zero_or_succ
  9. 0009rewrite zero_or_succ_left
  10. 0010rewrite zero_or_succ_left at hab_witness
  11. 0011specialize mul_zero_left x
  12. 0012rewrite mul_zero_left at hab_witness
  13. 0013symm
  14. 0014exact hab_witness
  15. 0015cases zero_or_succ_right
  16. 0016have ha : ~(a = 0)
  17. 0017intro ha0
  18. 0018rewrite zero_or_succ_right_witness at ha0
  19. 0019apply PA1
  20. 0020exact ha0
  21. 0021have hcycle : a = a * (x * x1)
  22. 0022trans b * x1
  23. 0023exact hba_witness
  24. 0024trans (a * x) * x1
  25. 0025congr
  26. 0026exact hab_witness
  27. 0027refl
  28. 0028apply mul_assoc
  29. 0029specialize mul_left_cancel_nonzero a
  30. 0030specialize mul_left_cancel_nonzero 1
  31. 0031specialize mul_left_cancel_nonzero (x * x1)
  32. 0032have hunit : 1 = x * x1
  33. 0033apply mul_left_cancel_nonzero
  34. 0034exact ha
  35. 0035specialize mul_one a
  36. 0036trans a
  37. 0037apply mul_one
  38. 0038exact hcycle
  39. 0039specialize mul_eq_one_components x
  40. 0040specialize mul_eq_one_components x1
  41. 0041have hparts : x = 1 /\ x1 = 1
  42. 0042apply mul_eq_one_components
  43. 0043symm
  44. 0044exact hunit
  45. 0045cases hparts
  46. 0046symm
  47. 0047trans a * x
  48. 0048exact hab_witness
  49. 0049rewrite hparts_left
  50. 0050apply mul_one