BT008R

prime_not_divides_coprime

Stable · empty-context checked

A prime not dividing a natural is coprime to that natural.

Exact expanded PA statement

forall p a. (~(p = 1) /\ forall c e. p = c * e -> c = 1 \/ e = 1) -> ~(exists k. a = p * k) -> forall d. (exists x. p = d * x) -> (exists y. a = d * y) -> d = 1

Structural proof guide

A prime not dividing a natural is coprime to that natural.

Direct prerequisites: prime_coprime_or_divides. The authored body proceeds by case analysis (1), intermediate claims (1).

Proof neighborhood

Direct dependencies

BT008Q prime_coprime_or_divides

Direct dependents

BT008S distinct_primes_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 p
  2. 0002intro a
  3. 0003intro hp
  4. 0004intro hnot
  5. 0005specialize prime_coprime_or_divides p
  6. 0006specialize prime_coprime_or_divides a
  7. 0007have hsplit : (forall d. (exists x. p = d * x) -> (exists y. a = d * y) -> d = 1) \/ exists k. a = p * k
  8. 0008apply prime_coprime_or_divides
  9. 0009exact hp
  10. 0010cases hsplit
  11. 0011exact hsplit_left
  12. 0012exfalso
  13. 0013apply hnot
  14. 0014exact hsplit_right