This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrid 
 |-  ( ( 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 ) )