BT002X

coprime_one_right

Stable · empty-context checked

Every natural is coprime to one in the expanded common-divisor relation.

Exact expanded PA statement

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

Structural proof guide

Every natural is coprime to one 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

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