Theorem prmdvdsexpb

Description: A prime divides a positive power of another iff they are equal. (Contributed by Paul Chapman, 30-Nov-2012) (Revised by Mario Carneiro, 24-Feb-2014)

	Ref	Expression
Assertion	prmdvdsexpb	$$⊢\left(P\in \mathbb{P}\wedge Q\in \mathbb{P}\wedge N\in \mathbb{N}\right)\to \left(P\parallel Q^N\leftrightarrow P=Q\right)$$

Proof

Step	Hyp	Ref	Expression
1		prmz	$$⊢Q\in \mathbb{P}\to Q\in \mathbb{Z}$$
2		prmdvdsexp	$$⊢\left(P\in \mathbb{P}\wedge Q\in \mathbb{Z}\wedge N\in \mathbb{N}\right)\to \left(P\parallel Q^N\leftrightarrow P\parallel Q\right)$$
3	1 2	syl3an2	$$⊢\left(P\in \mathbb{P}\wedge Q\in \mathbb{P}\wedge N\in \mathbb{N}\right)\to \left(P\parallel Q^N\leftrightarrow P\parallel Q\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	3adant3	$$⊢\left(P\in \mathbb{P}\wedge Q\in \mathbb{P}\wedge N\in \mathbb{N}\right)\to \left(P\parallel Q\leftrightarrow P=Q\right)$$
8	3 7	bitrd	$$⊢\left(P\in \mathbb{P}\wedge Q\in \mathbb{P}\wedge N\in \mathbb{N}\right)\to \left(P\parallel Q^N\leftrightarrow P=Q\right)$$