BT002Y

coprime_one_left

Stable · empty-context checked

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

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

Direct prerequisites: divisor_one. The authored body proceeds by direct introduction and elimination.

Proof neighborhood

Direct dependencies

BT002E divisor_one

Direct dependents

BT005C bounded_beta_exclusive_recode_invariant BT00DH beta_product_pointwise_coprime BT00VE primorial_interval_pairwise_coprime BT00YV coprime_powers BT00YW prime_contribution_prefix_pairwise_coprime

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