Theorem prmrp

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

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

Proof

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