# Metamath Proof Explorer

## Theorem prmrp

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

Ref Expression
Assertion prmrp ${⊢}\left({P}\in ℙ\wedge {Q}\in ℙ\right)\to \left({P}\mathrm{gcd}{Q}=1↔{P}\ne {Q}\right)$

### Proof

Step Hyp Ref Expression
1 prmz ${⊢}{Q}\in ℙ\to {Q}\in ℤ$
2 coprm ${⊢}\left({P}\in ℙ\wedge {Q}\in ℤ\right)\to \left(¬{P}\parallel {Q}↔{P}\mathrm{gcd}{Q}=1\right)$
3 1 2 sylan2 ${⊢}\left({P}\in ℙ\wedge {Q}\in ℙ\right)\to \left(¬{P}\parallel {Q}↔{P}\mathrm{gcd}{Q}=1\right)$
4 prmuz2 ${⊢}{P}\in ℙ\to {P}\in {ℤ}_{\ge 2}$
5 dvdsprm ${⊢}\left({P}\in {ℤ}_{\ge 2}\wedge {Q}\in ℙ\right)\to \left({P}\parallel {Q}↔{P}={Q}\right)$
6 4 5 sylan ${⊢}\left({P}\in ℙ\wedge {Q}\in ℙ\right)\to \left({P}\parallel {Q}↔{P}={Q}\right)$
7 6 necon3bbid ${⊢}\left({P}\in ℙ\wedge {Q}\in ℙ\right)\to \left(¬{P}\parallel {Q}↔{P}\ne {Q}\right)$
8 3 7 bitr3d ${⊢}\left({P}\in ℙ\wedge {Q}\in ℙ\right)\to \left({P}\mathrm{gcd}{Q}=1↔{P}\ne {Q}\right)$