PA001T

coprime_mul_left

Stable checked-use theorem · independently closed

Coprimality with a fixed right operand is closed under multiplication on the left.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

Coprimality with a fixed right operand is closed under multiplication on the left.

Use the direct prerequisites multiple_trans, gauss_coprime_cancel as previously established PA formulas.

The proof proceeds by intermediate claims (3).

Referenced ingredients

PA0018 multiple_trans PA001P gauss_coprime_cancel

Proof neighborhood

Direct dependencies

PA0018 multiple_trans PA001P gauss_coprime_cancel

Direct dependents

PA001U beta_exclusive_accumulated_product_step PA0081 beta_product_pointwise_coprime

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. 0002intro b
  3. 0003intro n
  4. 0004intro han
  5. 0005intro hbn
  6. 0006intro d
  7. 0007intro hab
  8. 0008intro hdn
  9. 0009have hda : forall e. (exists u. d = e * u) -> (exists v. a = e * v) -> e = 1
  10. 0010intro e
  11. 0011intro hed
  12. 0012intro hea
  13. 0013have hen : exists q. n = e * q
  14. 0014specialize multiple_trans d
  15. 0015specialize multiple_trans e
  16. 0016specialize multiple_trans n
  17. 0017apply multiple_trans
  18. 0018exact hdn
  19. 0019exact hed
  20. 0020specialize han e
  21. 0021apply han
  22. 0022exact hea
  23. 0023exact hen
  24. 0024have hdb : exists w. b = d * w
  25. 0025specialize gauss_coprime_cancel d
  26. 0026specialize gauss_coprime_cancel a
  27. 0027specialize gauss_coprime_cancel b
  28. 0028apply gauss_coprime_cancel
  29. 0029exact hda
  30. 0030exact hab
  31. 0031specialize hbn d
  32. 0032apply hbn
  33. 0033exact hdb
  34. 0034exact hdn