PA003N

prime_not_divides_coprime

Stable checked-use theorem · independently closed

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

Generated structural guide

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

Use the direct prerequisites prime_coprime_or_divides as previously established PA formulas.

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

Referenced ingredients

PA003M prime_coprime_or_divides

Proof neighborhood

Direct dependencies

PA003M prime_coprime_or_divides

Direct dependents

PA003S prime_mod_cancel PA0062 prime_mod_inverse PA0082 prime_positive_bounded_product_coprime PA008K prime_range_product_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 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