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 )