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

Metamath Proof Explorer

Theorem exp11d

Description: exp11nnd for nonzero integer exponents. (Contributed by SN, 14-Sep-2023)

Ref Expression
Hypotheses exp11d.1 
|- ( ph -> A e. RR+ )
exp11d.2 
|- ( ph -> B e. RR+ )
exp11d.3 
|- ( ph -> N e. ZZ )
exp11d.4 
|- ( ph -> N =/= 0 )
exp11d.5 
|- ( ph -> ( A ^ N ) = ( B ^ N ) )
Assertion exp11d 
|- ( ph -> A = B )

Proof

Step Hyp Ref Expression
1 exp11d.1 
 |-  ( ph -> A e. RR+ )
2 exp11d.2 
 |-  ( ph -> B e. RR+ )
3 exp11d.3 
 |-  ( ph -> N e. ZZ )
4 exp11d.4 
 |-  ( ph -> N =/= 0 )
5 exp11d.5 
 |-  ( ph -> ( A ^ N ) = ( B ^ N ) )
6 simpr 
 |-  ( ( ph /\ N = 0 ) -> N = 0 )
7 4 adantr 
 |-  ( ( ph /\ N = 0 ) -> N =/= 0 )
8 6 7 pm2.21ddne 
 |-  ( ( ph /\ N = 0 ) -> A = B )
9 1 adantr 
 |-  ( ( ph /\ N e. NN ) -> A e. RR+ )
10 2 adantr 
 |-  ( ( ph /\ N e. NN ) -> B e. RR+ )
11 simpr 
 |-  ( ( ph /\ N e. NN ) -> N e. NN )
12 5 adantr 
 |-  ( ( ph /\ N e. NN ) -> ( A ^ N ) = ( B ^ N ) )
13 9 10 11 12 exp11nnd 
 |-  ( ( ph /\ N e. NN ) -> A = B )
14 1 adantr 
 |-  ( ( ph /\ -u N e. NN ) -> A e. RR+ )
15 2 adantr 
 |-  ( ( ph /\ -u N e. NN ) -> B e. RR+ )
16 simpr 
 |-  ( ( ph /\ -u N e. NN ) -> -u N e. NN )
17 14 rpcnd 
 |-  ( ( ph /\ -u N e. NN ) -> A e. CC )
18 16 nnnn0d 
 |-  ( ( ph /\ -u N e. NN ) -> -u N e. NN0 )
19 17 18 expcld 
 |-  ( ( ph /\ -u N e. NN ) -> ( A ^ -u N ) e. CC )
20 15 rpcnd 
 |-  ( ( ph /\ -u N e. NN ) -> B e. CC )
21 20 18 expcld 
 |-  ( ( ph /\ -u N e. NN ) -> ( B ^ -u N ) e. CC )
22 14 rpne0d 
 |-  ( ( ph /\ -u N e. NN ) -> A =/= 0 )
23 16 nnzd 
 |-  ( ( ph /\ -u N e. NN ) -> -u N e. ZZ )
24 17 22 23 expne0d 
 |-  ( ( ph /\ -u N e. NN ) -> ( A ^ -u N ) =/= 0 )
25 15 rpne0d 
 |-  ( ( ph /\ -u N e. NN ) -> B =/= 0 )
26 20 25 23 expne0d 
 |-  ( ( ph /\ -u N e. NN ) -> ( B ^ -u N ) =/= 0 )
27 5 adantr 
 |-  ( ( ph /\ -u N e. NN ) -> ( A ^ N ) = ( B ^ N ) )
28 3 zcnd 
 |-  ( ph -> N e. CC )
29 28 adantr 
 |-  ( ( ph /\ -u N e. NN ) -> N e. CC )
30 expneg2 
 |-  ( ( A e. CC /\ N e. CC /\ -u N e. NN0 ) -> ( A ^ N ) = ( 1 / ( A ^ -u N ) ) )
31 17 29 18 30 syl3anc 
 |-  ( ( ph /\ -u N e. NN ) -> ( A ^ N ) = ( 1 / ( A ^ -u N ) ) )
32 expneg2 
 |-  ( ( B e. CC /\ N e. CC /\ -u N e. NN0 ) -> ( B ^ N ) = ( 1 / ( B ^ -u N ) ) )
33 20 29 18 32 syl3anc 
 |-  ( ( ph /\ -u N e. NN ) -> ( B ^ N ) = ( 1 / ( B ^ -u N ) ) )
34 27 31 33 3eqtr3d 
 |-  ( ( ph /\ -u N e. NN ) -> ( 1 / ( A ^ -u N ) ) = ( 1 / ( B ^ -u N ) ) )
35 19 21 24 26 34 rec11d 
 |-  ( ( ph /\ -u N e. NN ) -> ( A ^ -u N ) = ( B ^ -u N ) )
36 14 15 16 35 exp11nnd 
 |-  ( ( ph /\ -u N e. NN ) -> A = B )
37 elz 
 |-  ( N e. ZZ <-> ( N e. RR /\ ( N = 0 \/ N e. NN \/ -u N e. NN ) ) )
38 3 37 sylib 
 |-  ( ph -> ( N e. RR /\ ( N = 0 \/ N e. NN \/ -u N e. NN ) ) )
39 38 simprd 
 |-  ( ph -> ( N = 0 \/ N e. NN \/ -u N e. NN ) )
40 8 13 36 39 mpjao3dan 
 |-  ( ph -> A = B )