PA003M

prime_coprime_or_divides

Stable checked-use theorem · independently closed

A prime is constructively either coprime to a natural or divides it.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

A prime is constructively either coprime to a natural or divides it.

Use the direct prerequisites gcd_exists_relational, prime_divisor_eq_one_or_self, is_gcd_one_to_coprime as previously established PA formulas.

The proof proceeds by case analysis (5), intermediate claims (4), equality transport (4).

Referenced ingredients

PA0036 gcd_exists_relational PA0003 prime_divisor_eq_one_or_self PA0037 is_gcd_one_to_coprime

Proof neighborhood

Direct dependencies

PA0036 gcd_exists_relational PA0003 prime_divisor_eq_one_or_self PA0037 is_gcd_one_to_coprime

Direct dependents

PA003N prime_not_divides_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. 0004have hg : exists g. (((exists x. p = g * x) /\ (exists y. a = g * y)) /\ forall c. (exists u. p = c * u) -> (exists v. a = c * v) -> exists w. g = c * w)
  5. 0005apply gcd_exists_relational
  6. 0006cases hg
  7. 0007have hgfull : (((exists u. p = x * u) /\ (exists v. a = x * v)) /\ forall c. (exists s. p = c * s) -> (exists t. a = c * t) -> exists w. x = c * w)
  8. 0008exact hg_witness
  9. 0009cases hg_witness
  10. 0010cases hg_witness_left
  11. 0011have hfactor : x = 1 \/ p = x
  12. 0012specialize prime_divisor_eq_one_or_self p
  13. 0013specialize prime_divisor_eq_one_or_self x
  14. 0014apply prime_divisor_eq_one_or_self
  15. 0015exact hp
  16. 0016exact hg_witness_left_left
  17. 0017cases hfactor
  18. 0018left
  19. 0019apply is_gcd_one_to_coprime
  20. 0020have hg1 : (((exists u. p = 1 * u) /\ (exists v. a = 1 * v)) /\ forall c. (exists s. p = c * s) -> (exists t. a = c * t) -> exists w. 1 = c * w)
  21. 0021rewrite <- hfactor_left
  22. 0022rewrite <- hfactor_left
  23. 0023rewrite <- hfactor_left
  24. 0024exact hgfull
  25. 0025exact hg1
  26. 0026right
  27. 0027cases hg_witness_left_right
  28. 0028exists x1
  29. 0029rewrite hfactor_right
  30. 0030exact hg_witness_left_right_witness