PA0037

is_gcd_one_to_coprime

Stable checked-use theorem · independently closed

A relational gcd witness one implies expanded coprimality.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

A relational gcd witness one implies expanded coprimality.

Use the direct prerequisites divisor_one as previously established PA formulas.

The proof proceeds by case analysis (1), intermediate claims (1).

Referenced ingredients

PA000O divisor_one

Proof neighborhood

Direct dependencies

PA000O divisor_one

Direct dependents

PA0038 euclid_prime_dvd_product PA003M prime_coprime_or_divides

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 hg
  4. 0004intro c
  5. 0005intro ha
  6. 0006intro hb
  7. 0007cases hg
  8. 0008specialize hg_right c
  9. 0009have hd : exists w. 1 = c * w
  10. 0010apply hg_right
  11. 0011exact ha
  12. 0012exact hb
  13. 0013specialize divisor_one c
  14. 0014apply divisor_one
  15. 0015exact hd