PA003O

coprime_symm

Stable checked-use theorem · independently closed

Coprimality in its expanded common-divisor form is symmetric.

Exact expanded PA statement

forall a b. (forall d. (exists x. a = d * x) -> (exists y. b = d * y) -> d = 1) -> forall c. (exists u. b = c * u) -> (exists v. a = c * v) -> c = 1

Structural proof guide

Generated structural guide

Coprimality in its expanded common-divisor form is symmetric.

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA003S prime_mod_cancel PA0082 prime_positive_bounded_product_coprime PA008K prime_range_product_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 h
  4. 0004intro c
  5. 0005intro hb
  6. 0006intro ha
  7. 0007specialize h c
  8. 0008apply h
  9. 0009exact ha
  10. 0010exact hb