BT008S

distinct_primes_coprime

Stable · empty-context checked

Distinct primes are coprime in the expanded common-divisor relation.

Exact expanded PA statement

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

Structural proof guide

Distinct primes are coprime in the expanded common-divisor relation.

Direct prerequisites: prime_divisor_eq_one_or_self, prime_not_divides_coprime. The authored body proceeds by case analysis (2), intermediate claims (2).

Proof neighborhood

Direct dependencies

BT003M prime_divisor_eq_one_or_self BT008R prime_not_divides_coprime

Direct dependents

BT00VE primorial_interval_pairwise_coprime 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 p
  2. 0002intro q
  3. 0003intro hp
  4. 0004intro hq
  5. 0005intro hpq
  6. 0006have hnot : ~(exists k. q = p * k)
  7. 0007intro hdiv
  8. 0008specialize prime_divisor_eq_one_or_self q
  9. 0009specialize prime_divisor_eq_one_or_self p
  10. 0010have hfactor : p = 1 \/ q = p
  11. 0011apply prime_divisor_eq_one_or_self
  12. 0012exact hq
  13. 0013exact hdiv
  14. 0014cases hfactor
  15. 0015cases hp
  16. 0016apply hp_left
  17. 0017exact hfactor_left
  18. 0018apply hpq
  19. 0019symm
  20. 0020exact hfactor_right
  21. 0021specialize prime_not_divides_coprime p
  22. 0022specialize prime_not_divides_coprime q
  23. 0023apply prime_not_divides_coprime
  24. 0024exact hp
  25. 0025exact hnot