Metamath Proof Explorer

Theorem prmexpb

Description: Two positive prime powers are equal iff the primes and the powers are equal. (Contributed by Paul Chapman, 30-Nov-2012)

Ref Expression
Assertion prmexpb 
|- ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) ) -> ( ( P ^ M ) = ( Q ^ N ) <-> ( P = Q /\ M = N ) ) )

Proof

Step Hyp Ref Expression
1 prmz 
 |-  ( P e. Prime -> P e. ZZ )
2 1 adantr 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> P e. ZZ )
3 2 3ad2ant1 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) /\ ( P ^ M ) = ( Q ^ N ) ) -> P e. ZZ )
4 simp2l 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) /\ ( P ^ M ) = ( Q ^ N ) ) -> M e. NN )
5 iddvdsexp 
 |-  ( ( P e. ZZ /\ M e. NN ) -> P || ( P ^ M ) )
6 3 4 5 syl2anc 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) /\ ( P ^ M ) = ( Q ^ N ) ) -> P || ( P ^ M ) )
7 breq2 
 |-  ( ( P ^ M ) = ( Q ^ N ) -> ( P || ( P ^ M ) <-> P || ( Q ^ N ) ) )
8 7 3ad2ant3 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) /\ ( P ^ M ) = ( Q ^ N ) ) -> ( P || ( P ^ M ) <-> P || ( Q ^ N ) ) )
9 simp1l 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) /\ ( P ^ M ) = ( Q ^ N ) ) -> P e. Prime )
10 simp1r 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) /\ ( P ^ M ) = ( Q ^ N ) ) -> Q e. Prime )
11 simp2r 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) /\ ( P ^ M ) = ( Q ^ N ) ) -> N e. NN )
12 prmdvdsexpb 
 |-  ( ( P e. Prime /\ Q e. Prime /\ N e. NN ) -> ( P || ( Q ^ N ) <-> P = Q ) )
13 9 10 11 12 syl3anc 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) /\ ( P ^ M ) = ( Q ^ N ) ) -> ( P || ( Q ^ N ) <-> P = Q ) )
14 8 13 bitrd 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) /\ ( P ^ M ) = ( Q ^ N ) ) -> ( P || ( P ^ M ) <-> P = Q ) )
15 6 14 mpbid 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) /\ ( P ^ M ) = ( Q ^ N ) ) -> P = Q )
16 3 zred 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) /\ ( P ^ M ) = ( Q ^ N ) ) -> P e. RR )
17 4 nnzd 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) /\ ( P ^ M ) = ( Q ^ N ) ) -> M e. ZZ )
18 11 nnzd 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) /\ ( P ^ M ) = ( Q ^ N ) ) -> N e. ZZ )
19 prmgt1 
 |-  ( P e. Prime -> 1 < P )
20 19 ad2antrr 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) ) -> 1 < P )
21 20 3adant3 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) /\ ( P ^ M ) = ( Q ^ N ) ) -> 1 < P )
22 simp3 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) /\ ( P ^ M ) = ( Q ^ N ) ) -> ( P ^ M ) = ( Q ^ N ) )
23 15 oveq1d 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) /\ ( P ^ M ) = ( Q ^ N ) ) -> ( P ^ N ) = ( Q ^ N ) )
24 22 23 eqtr4d 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) /\ ( P ^ M ) = ( Q ^ N ) ) -> ( P ^ M ) = ( P ^ N ) )
25 16 17 18 21 24 expcand 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) /\ ( P ^ M ) = ( Q ^ N ) ) -> M = N )
26 15 25 jca 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) /\ ( P ^ M ) = ( Q ^ N ) ) -> ( P = Q /\ M = N ) )
27 26 3expia 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) ) -> ( ( P ^ M ) = ( Q ^ N ) -> ( P = Q /\ M = N ) ) )
28 oveq12 
 |-  ( ( P = Q /\ M = N ) -> ( P ^ M ) = ( Q ^ N ) )
29 27 28 impbid1 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) ) -> ( ( P ^ M ) = ( Q ^ N ) <-> ( P = Q /\ M = N ) ) )