PA000P

coprime_one_left

Stable checked-use theorem · independently closed

One is coprime to every natural in the expanded common-divisor relation.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

One is coprime to every natural in the expanded common-divisor relation.

Use the direct prerequisites divisor_one as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA000O divisor_one

Proof neighborhood

Direct dependencies

PA000O divisor_one

Direct dependents

PA002I bounded_beta_exclusive_recode_invariant 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 d
  3. 0003intro h1
  4. 0004intro ha
  5. 0005specialize divisor_one d
  6. 0006apply divisor_one
  7. 0007exact h1