BT004S

coprime_mul_right

Stable · empty-context checked

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

Exact expanded PA statement

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

Structural proof guide

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

Direct prerequisites: coprime_mul_left, coprime_symm. The authored body proceeds by intermediate claims (3).

Proof neighborhood

Direct dependencies

BT004R coprime_mul_left BT002W coprime_symm

Direct dependents

BT00YU coprime_power_right

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro n
  2. 0002intro a
  3. 0003intro b
  4. 0004intro hna
  5. 0005intro hnb
  6. 0006have han : forall d. (exists x. a = d * x) -> (exists y. n = d * y) -> d = 1
  7. 0007specialize coprime_symm n
  8. 0008specialize coprime_symm a
  9. 0009apply coprime_symm
  10. 0010exact hna
  11. 0011have hbn : forall d. (exists x. b = d * x) -> (exists y. n = d * y) -> d = 1
  12. 0012specialize coprime_symm n
  13. 0013specialize coprime_symm b
  14. 0014apply coprime_symm
  15. 0015exact hnb
  16. 0016have habn : forall d. (exists x. a * b = d * x) -> (exists y. n = d * y) -> d = 1
  17. 0017specialize coprime_mul_left a
  18. 0018specialize coprime_mul_left b
  19. 0019specialize coprime_mul_left n
  20. 0020apply coprime_mul_left
  21. 0021exact han
  22. 0022exact hbn
  23. 0023specialize coprime_symm (a * b)
  24. 0024specialize coprime_symm n
  25. 0025apply coprime_symm
  26. 0026exact habn