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	|- ( ( P e. Prime /\ Q e. Prime /\ N e. NN ) -> ( P || ( Q ^ N ) <-> P = Q ) )

Proof

Step	Hyp	Ref	Expression
1		prmz	|- ( Q e. Prime -> Q e. ZZ )
2		prmdvdsexp	|- ( ( P e. Prime /\ Q e. ZZ /\ N e. NN ) -> ( P || ( Q ^ N ) <-> P || Q ) )
3	1 2	syl3an2	|- ( ( P e. Prime /\ Q e. Prime /\ N e. NN ) -> ( P || ( Q ^ N ) <-> P || Q ) )
4		prmuz2	|- ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
5		dvdsprm	|- ( ( P e. ( ZZ>= ` 2 ) /\ Q e. Prime ) -> ( P || Q <-> P = Q ) )
6	4 5	sylan	|- ( ( P e. Prime /\ Q e. Prime ) -> ( P || Q <-> P = Q ) )
7	6	3adant3	|- ( ( P e. Prime /\ Q e. Prime /\ N e. NN ) -> ( P || Q <-> P = Q ) )
8	3 7	bitrd	|- ( ( P e. Prime /\ Q e. Prime /\ N e. NN ) -> ( P || ( Q ^ N ) <-> P = Q ) )