Metamath Proof Explorer

Theorem prmrp

Description: Unequal prime numbers are relatively prime. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion prmrp ⊢ P ∈ ℙ ∧ Q ∈ ℙ → P gcd Q = 1 ↔ P ≠ Q

Proof

Step Hyp Ref Expression
1 prmz ⊢ Q ∈ ℙ → Q ∈ ℤ
2 coprm ⊢ P ∈ ℙ ∧ Q ∈ ℤ → ¬ P ∥ Q ↔ P gcd Q = 1
3 1 2 sylan2 ⊢ P ∈ ℙ ∧ Q ∈ ℙ → ¬ P ∥ Q ↔ P gcd Q = 1
4 prmuz2 ⊢ P ∈ ℙ → P ∈ ℤ ≥ 2
5 dvdsprm ⊢ P ∈ ℤ ≥ 2 ∧ Q ∈ ℙ → P ∥ Q ↔ P = Q
6 4 5 sylan ⊢ P ∈ ℙ ∧ Q ∈ ℙ → P ∥ Q ↔ P = Q
7 6 necon3bbid ⊢ P ∈ ℙ ∧ Q ∈ ℙ → ¬ P ∥ Q ↔ P ≠ Q
8 3 7 bitr3d ⊢ P ∈ ℙ ∧ Q ∈ ℙ → P gcd Q = 1 ↔ P ≠ Q