BT004R

coprime_mul_left

Stable · empty-context checked

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

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

Direct prerequisites: multiple_trans, gauss_coprime_cancel. The authored body proceeds by intermediate claims (3).

Proof neighborhood

Direct dependencies

BT002C multiple_trans BT0039 gauss_coprime_cancel

Direct dependents

BT004S coprime_mul_right BT0059 beta_exclusive_accumulated_product_step BT00DH beta_product_pointwise_coprime BT00YV coprime_powers

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