Theorem prmdvdsexpr

Description: If a prime divides a nonnegative power of another, then they are equal. (Contributed by Mario Carneiro, 16-Jan-2015)

	Ref	Expression
Assertion	prmdvdsexpr	|- ( ( P e. Prime /\ Q e. Prime /\ N e. NN0 ) -> ( P || ( Q ^ N ) -> P = Q ) )

Proof

Step	Hyp	Ref	Expression
1		elnn0	|- ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2		prmdvdsexpb	|- ( ( P e. Prime /\ Q e. Prime /\ N e. NN ) -> ( P || ( Q ^ N ) <-> P = Q ) )
3	2	biimpd	|- ( ( P e. Prime /\ Q e. Prime /\ N e. NN ) -> ( P || ( Q ^ N ) -> P = Q ) )
4	3	3expia	|- ( ( P e. Prime /\ Q e. Prime ) -> ( N e. NN -> ( P || ( Q ^ N ) -> P = Q ) ) )
5		prmnn	|- ( Q e. Prime -> Q e. NN )
6	5	adantl	|- ( ( P e. Prime /\ Q e. Prime ) -> Q e. NN )
7	6	nncnd	|- ( ( P e. Prime /\ Q e. Prime ) -> Q e. CC )
8	7	exp0d	|- ( ( P e. Prime /\ Q e. Prime ) -> ( Q ^ 0 ) = 1 )
9	8	breq2d	|- ( ( P e. Prime /\ Q e. Prime ) -> ( P || ( Q ^ 0 ) <-> P || 1 ) )
10		nprmdvds1	|- ( P e. Prime -> -. P || 1 )
11	10	pm2.21d	|- ( P e. Prime -> ( P || 1 -> P = Q ) )
12	11	adantr	|- ( ( P e. Prime /\ Q e. Prime ) -> ( P || 1 -> P = Q ) )
13	9 12	sylbid	|- ( ( P e. Prime /\ Q e. Prime ) -> ( P || ( Q ^ 0 ) -> P = Q ) )
14		oveq2	|- ( N = 0 -> ( Q ^ N ) = ( Q ^ 0 ) )
15	14	breq2d	|- ( N = 0 -> ( P || ( Q ^ N ) <-> P || ( Q ^ 0 ) ) )
16	15	imbi1d	|- ( N = 0 -> ( ( P || ( Q ^ N ) -> P = Q ) <-> ( P || ( Q ^ 0 ) -> P = Q ) ) )
17	13 16	syl5ibrcom	|- ( ( P e. Prime /\ Q e. Prime ) -> ( N = 0 -> ( P || ( Q ^ N ) -> P = Q ) ) )
18	4 17	jaod	|- ( ( P e. Prime /\ Q e. Prime ) -> ( ( N e. NN \/ N = 0 ) -> ( P || ( Q ^ N ) -> P = Q ) ) )
19	1 18	syl5bi	|- ( ( P e. Prime /\ Q e. Prime ) -> ( N e. NN0 -> ( P || ( Q ^ N ) -> P = Q ) ) )
20	19	3impia	|- ( ( P e. Prime /\ Q e. Prime /\ N e. NN0 ) -> ( P || ( Q ^ N ) -> P = Q ) )