Metamath Proof Explorer

Theorem expaddz

Description: Sum of exponents law for integer exponentiation. Proposition 10-4.2(a) of Gleason p. 135. (Contributed by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion expaddz 
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) )

Proof

Step Hyp Ref Expression
1 elznn0nn 
 |-  ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) )
2 elznn0nn 
 |-  ( M e. ZZ <-> ( M e. NN0 \/ ( M e. RR /\ -u M e. NN ) ) )
3 expadd 
 |-  ( ( A e. CC /\ M e. NN0 /\ N e. NN0 ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) )
4 3 3expia 
 |-  ( ( A e. CC /\ M e. NN0 ) -> ( N e. NN0 -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) ) )
5 4 adantlr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 ) -> ( N e. NN0 -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) ) )
6 expaddzlem 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) )
7 6 3expia 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) ) -> ( N e. NN0 -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) ) )
8 5 7 jaodan 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. NN0 \/ ( M e. RR /\ -u M e. NN ) ) ) -> ( N e. NN0 -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) ) )
9 expaddzlem 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) /\ M e. NN0 ) -> ( A ^ ( N + M ) ) = ( ( A ^ N ) x. ( A ^ M ) ) )
10 simp3 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) /\ M e. NN0 ) -> M e. NN0 )
11 10 nn0cnd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) /\ M e. NN0 ) -> M e. CC )
12 simp2l 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) /\ M e. NN0 ) -> N e. RR )
13 12 recnd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) /\ M e. NN0 ) -> N e. CC )
14 11 13 addcomd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) /\ M e. NN0 ) -> ( M + N ) = ( N + M ) )
15 14 oveq2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) /\ M e. NN0 ) -> ( A ^ ( M + N ) ) = ( A ^ ( N + M ) ) )
16 simp1l 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) /\ M e. NN0 ) -> A e. CC )
17 expcl 
 |-  ( ( A e. CC /\ M e. NN0 ) -> ( A ^ M ) e. CC )
18 16 10 17 syl2anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) /\ M e. NN0 ) -> ( A ^ M ) e. CC )
19 simp1r 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) /\ M e. NN0 ) -> A =/= 0 )
20 13 negnegd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) /\ M e. NN0 ) -> -u -u N = N )
21 simp2r 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) /\ M e. NN0 ) -> -u N e. NN )
22 21 nnnn0d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) /\ M e. NN0 ) -> -u N e. NN0 )
23 nn0negz 
 |-  ( -u N e. NN0 -> -u -u N e. ZZ )
24 22 23 syl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) /\ M e. NN0 ) -> -u -u N e. ZZ )
25 20 24 eqeltrrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) /\ M e. NN0 ) -> N e. ZZ )
26 expclz 
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) e. CC )
27 16 19 25 26 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) /\ M e. NN0 ) -> ( A ^ N ) e. CC )
28 18 27 mulcomd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) /\ M e. NN0 ) -> ( ( A ^ M ) x. ( A ^ N ) ) = ( ( A ^ N ) x. ( A ^ M ) ) )
29 9 15 28 3eqtr4d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) /\ M e. NN0 ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) )
30 29 3expia 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( M e. NN0 -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) ) )
31 30 impancom 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 ) -> ( ( N e. RR /\ -u N e. NN ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) ) )
32 simp2l 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> M e. RR )
33 32 recnd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> M e. CC )
34 simp3l 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> N e. RR )
35 34 recnd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> N e. CC )
36 33 35 negdid 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u ( M + N ) = ( -u M + -u N ) )
37 36 oveq2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ -u ( M + N ) ) = ( A ^ ( -u M + -u N ) ) )
38 simp1l 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> A e. CC )
39 simp2r 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u M e. NN )
40 39 nnnn0d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u M e. NN0 )
41 simp3r 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u N e. NN )
42 41 nnnn0d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u N e. NN0 )
43 expadd 
 |-  ( ( A e. CC /\ -u M e. NN0 /\ -u N e. NN0 ) -> ( A ^ ( -u M + -u N ) ) = ( ( A ^ -u M ) x. ( A ^ -u N ) ) )
44 38 40 42 43 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ ( -u M + -u N ) ) = ( ( A ^ -u M ) x. ( A ^ -u N ) ) )
45 37 44 eqtrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ -u ( M + N ) ) = ( ( A ^ -u M ) x. ( A ^ -u N ) ) )
46 45 oveq2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( 1 / ( A ^ -u ( M + N ) ) ) = ( 1 / ( ( A ^ -u M ) x. ( A ^ -u N ) ) ) )
47 1t1e1 
 |-  ( 1 x. 1 ) = 1
48 47 oveq1i 
 |-  ( ( 1 x. 1 ) / ( ( A ^ -u M ) x. ( A ^ -u N ) ) ) = ( 1 / ( ( A ^ -u M ) x. ( A ^ -u N ) ) )
49 46 48 eqtr4di 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( 1 / ( A ^ -u ( M + N ) ) ) = ( ( 1 x. 1 ) / ( ( A ^ -u M ) x. ( A ^ -u N ) ) ) )
50 expcl 
 |-  ( ( A e. CC /\ -u M e. NN0 ) -> ( A ^ -u M ) e. CC )
51 38 40 50 syl2anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ -u M ) e. CC )
52 simp1r 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> A =/= 0 )
53 40 nn0zd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u M e. ZZ )
54 expne0i 
 |-  ( ( A e. CC /\ A =/= 0 /\ -u M e. ZZ ) -> ( A ^ -u M ) =/= 0 )
55 38 52 53 54 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ -u M ) =/= 0 )
56 expcl 
 |-  ( ( A e. CC /\ -u N e. NN0 ) -> ( A ^ -u N ) e. CC )
57 38 42 56 syl2anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ -u N ) e. CC )
58 42 nn0zd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u N e. ZZ )
59 expne0i 
 |-  ( ( A e. CC /\ A =/= 0 /\ -u N e. ZZ ) -> ( A ^ -u N ) =/= 0 )
60 38 52 58 59 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ -u N ) =/= 0 )
61 ax-1cn 
 |-  1 e. CC
62 divmuldiv 
 |-  ( ( ( 1 e. CC /\ 1 e. CC ) /\ ( ( ( A ^ -u M ) e. CC /\ ( A ^ -u M ) =/= 0 ) /\ ( ( A ^ -u N ) e. CC /\ ( A ^ -u N ) =/= 0 ) ) ) -> ( ( 1 / ( A ^ -u M ) ) x. ( 1 / ( A ^ -u N ) ) ) = ( ( 1 x. 1 ) / ( ( A ^ -u M ) x. ( A ^ -u N ) ) ) )
63 61 61 62 mpanl12 
 |-  ( ( ( ( A ^ -u M ) e. CC /\ ( A ^ -u M ) =/= 0 ) /\ ( ( A ^ -u N ) e. CC /\ ( A ^ -u N ) =/= 0 ) ) -> ( ( 1 / ( A ^ -u M ) ) x. ( 1 / ( A ^ -u N ) ) ) = ( ( 1 x. 1 ) / ( ( A ^ -u M ) x. ( A ^ -u N ) ) ) )
64 51 55 57 60 63 syl22anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( ( 1 / ( A ^ -u M ) ) x. ( 1 / ( A ^ -u N ) ) ) = ( ( 1 x. 1 ) / ( ( A ^ -u M ) x. ( A ^ -u N ) ) ) )
65 49 64 eqtr4d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( 1 / ( A ^ -u ( M + N ) ) ) = ( ( 1 / ( A ^ -u M ) ) x. ( 1 / ( A ^ -u N ) ) ) )
66 33 35 addcld 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( M + N ) e. CC )
67 40 42 nn0addcld 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( -u M + -u N ) e. NN0 )
68 36 67 eqeltrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u ( M + N ) e. NN0 )
69 expneg2 
 |-  ( ( A e. CC /\ ( M + N ) e. CC /\ -u ( M + N ) e. NN0 ) -> ( A ^ ( M + N ) ) = ( 1 / ( A ^ -u ( M + N ) ) ) )
70 38 66 68 69 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ ( M + N ) ) = ( 1 / ( A ^ -u ( M + N ) ) ) )
71 expneg2 
 |-  ( ( A e. CC /\ M e. CC /\ -u M e. NN0 ) -> ( A ^ M ) = ( 1 / ( A ^ -u M ) ) )
72 38 33 40 71 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ M ) = ( 1 / ( A ^ -u M ) ) )
73 expneg2 
 |-  ( ( A e. CC /\ N e. CC /\ -u N e. NN0 ) -> ( A ^ N ) = ( 1 / ( A ^ -u N ) ) )
74 38 35 42 73 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ N ) = ( 1 / ( A ^ -u N ) ) )
75 72 74 oveq12d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( ( A ^ M ) x. ( A ^ N ) ) = ( ( 1 / ( A ^ -u M ) ) x. ( 1 / ( A ^ -u N ) ) ) )
76 65 70 75 3eqtr4d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) )
77 76 3expia 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) ) -> ( ( N e. RR /\ -u N e. NN ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) ) )
78 31 77 jaodan 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. NN0 \/ ( M e. RR /\ -u M e. NN ) ) ) -> ( ( N e. RR /\ -u N e. NN ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) ) )
79 8 78 jaod 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. NN0 \/ ( M e. RR /\ -u M e. NN ) ) ) -> ( ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) ) )
80 2 79 sylan2b 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. ZZ ) -> ( ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) ) )
81 1 80 syl5bi 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. ZZ ) -> ( N e. ZZ -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) ) )
82 81 impr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) )