Theorem prmrp

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

	Ref	Expression
Assertion	prmrp	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( ( 𝑃 gcd 𝑄 ) = 1 ↔ 𝑃 ≠ 𝑄 ) )

Proof

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