Metamath Proof Explorer

Theorem expaddzlem

Description: Lemma for expaddz . (Contributed by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion expaddzlem 
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) )

Proof

Step Hyp Ref Expression
1 simp1l 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> A e. CC )
2 simp3 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> N e. NN0 )
3 expcl 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( A ^ N ) e. CC )
4 1 2 3 syl2anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ N ) e. CC )
5 simp2r 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> -u M e. NN )
6 5 nnnn0d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> -u M e. NN0 )
7 expcl 
 |-  ( ( A e. CC /\ -u M e. NN0 ) -> ( A ^ -u M ) e. CC )
8 1 6 7 syl2anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ -u M ) e. CC )
9 simp1r 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> A =/= 0 )
10 5 nnzd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> -u M e. ZZ )
11 expne0i 
 |-  ( ( A e. CC /\ A =/= 0 /\ -u M e. ZZ ) -> ( A ^ -u M ) =/= 0 )
12 1 9 10 11 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ -u M ) =/= 0 )
13 4 8 12 divrec2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( ( A ^ N ) / ( A ^ -u M ) ) = ( ( 1 / ( A ^ -u M ) ) x. ( A ^ N ) ) )
14 simp2l 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> M e. RR )
15 14 recnd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> M e. CC )
16 15 negnegd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> -u -u M = M )
17 nnnegz 
 |-  ( -u M e. NN -> -u -u M e. ZZ )
18 5 17 syl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> -u -u M e. ZZ )
19 16 18 eqeltrrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> M e. ZZ )
20 2 nn0zd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> N e. ZZ )
21 19 20 zaddcld 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( M + N ) e. ZZ )
22 expclz 
 |-  ( ( A e. CC /\ A =/= 0 /\ ( M + N ) e. ZZ ) -> ( A ^ ( M + N ) ) e. CC )
23 1 9 21 22 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ ( M + N ) ) e. CC )
24 23 adantr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ ( M + N ) e. NN0 ) -> ( A ^ ( M + N ) ) e. CC )
25 8 adantr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ ( M + N ) e. NN0 ) -> ( A ^ -u M ) e. CC )
26 12 adantr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ ( M + N ) e. NN0 ) -> ( A ^ -u M ) =/= 0 )
27 24 25 26 divcan4d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ ( M + N ) e. NN0 ) -> ( ( ( A ^ ( M + N ) ) x. ( A ^ -u M ) ) / ( A ^ -u M ) ) = ( A ^ ( M + N ) ) )
28 1 adantr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ ( M + N ) e. NN0 ) -> A e. CC )
29 simpr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ ( M + N ) e. NN0 ) -> ( M + N ) e. NN0 )
30 6 adantr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ ( M + N ) e. NN0 ) -> -u M e. NN0 )
31 expadd 
 |-  ( ( A e. CC /\ ( M + N ) e. NN0 /\ -u M e. NN0 ) -> ( A ^ ( ( M + N ) + -u M ) ) = ( ( A ^ ( M + N ) ) x. ( A ^ -u M ) ) )
32 28 29 30 31 syl3anc 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ ( M + N ) e. NN0 ) -> ( A ^ ( ( M + N ) + -u M ) ) = ( ( A ^ ( M + N ) ) x. ( A ^ -u M ) ) )
33 21 zcnd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( M + N ) e. CC )
34 33 15 negsubd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( ( M + N ) + -u M ) = ( ( M + N ) - M ) )
35 2 nn0cnd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> N e. CC )
36 15 35 pncan2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( ( M + N ) - M ) = N )
37 34 36 eqtrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( ( M + N ) + -u M ) = N )
38 37 adantr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ ( M + N ) e. NN0 ) -> ( ( M + N ) + -u M ) = N )
39 38 oveq2d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ ( M + N ) e. NN0 ) -> ( A ^ ( ( M + N ) + -u M ) ) = ( A ^ N ) )
40 32 39 eqtr3d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ ( M + N ) e. NN0 ) -> ( ( A ^ ( M + N ) ) x. ( A ^ -u M ) ) = ( A ^ N ) )
41 40 oveq1d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ ( M + N ) e. NN0 ) -> ( ( ( A ^ ( M + N ) ) x. ( A ^ -u M ) ) / ( A ^ -u M ) ) = ( ( A ^ N ) / ( A ^ -u M ) ) )
42 27 41 eqtr3d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ ( M + N ) e. NN0 ) -> ( A ^ ( M + N ) ) = ( ( A ^ N ) / ( A ^ -u M ) ) )
43 1 adantr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ -u ( M + N ) e. NN0 ) -> A e. CC )
44 33 adantr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ -u ( M + N ) e. NN0 ) -> ( M + N ) e. CC )
45 simpr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ -u ( M + N ) e. NN0 ) -> -u ( M + N ) e. NN0 )
46 expneg2 
 |-  ( ( A e. CC /\ ( M + N ) e. CC /\ -u ( M + N ) e. NN0 ) -> ( A ^ ( M + N ) ) = ( 1 / ( A ^ -u ( M + N ) ) ) )
47 43 44 45 46 syl3anc 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ -u ( M + N ) e. NN0 ) -> ( A ^ ( M + N ) ) = ( 1 / ( A ^ -u ( M + N ) ) ) )
48 21 znegcld 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> -u ( M + N ) e. ZZ )
49 expclz 
 |-  ( ( A e. CC /\ A =/= 0 /\ -u ( M + N ) e. ZZ ) -> ( A ^ -u ( M + N ) ) e. CC )
50 1 9 48 49 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ -u ( M + N ) ) e. CC )
51 50 adantr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ -u ( M + N ) e. NN0 ) -> ( A ^ -u ( M + N ) ) e. CC )
52 4 adantr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ -u ( M + N ) e. NN0 ) -> ( A ^ N ) e. CC )
53 expne0i 
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) =/= 0 )
54 1 9 20 53 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ N ) =/= 0 )
55 54 adantr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ -u ( M + N ) e. NN0 ) -> ( A ^ N ) =/= 0 )
56 51 52 55 divcan4d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ -u ( M + N ) e. NN0 ) -> ( ( ( A ^ -u ( M + N ) ) x. ( A ^ N ) ) / ( A ^ N ) ) = ( A ^ -u ( M + N ) ) )
57 2 adantr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ -u ( M + N ) e. NN0 ) -> N e. NN0 )
58 expadd 
 |-  ( ( A e. CC /\ -u ( M + N ) e. NN0 /\ N e. NN0 ) -> ( A ^ ( -u ( M + N ) + N ) ) = ( ( A ^ -u ( M + N ) ) x. ( A ^ N ) ) )
59 43 45 57 58 syl3anc 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ -u ( M + N ) e. NN0 ) -> ( A ^ ( -u ( M + N ) + N ) ) = ( ( A ^ -u ( M + N ) ) x. ( A ^ N ) ) )
60 15 35 negdi2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> -u ( M + N ) = ( -u M - N ) )
61 60 oveq1d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( -u ( M + N ) + N ) = ( ( -u M - N ) + N ) )
62 15 negcld 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> -u M e. CC )
63 62 35 npcand 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( ( -u M - N ) + N ) = -u M )
64 61 63 eqtrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( -u ( M + N ) + N ) = -u M )
65 64 adantr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ -u ( M + N ) e. NN0 ) -> ( -u ( M + N ) + N ) = -u M )
66 65 oveq2d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ -u ( M + N ) e. NN0 ) -> ( A ^ ( -u ( M + N ) + N ) ) = ( A ^ -u M ) )
67 59 66 eqtr3d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ -u ( M + N ) e. NN0 ) -> ( ( A ^ -u ( M + N ) ) x. ( A ^ N ) ) = ( A ^ -u M ) )
68 67 oveq1d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ -u ( M + N ) e. NN0 ) -> ( ( ( A ^ -u ( M + N ) ) x. ( A ^ N ) ) / ( A ^ N ) ) = ( ( A ^ -u M ) / ( A ^ N ) ) )
69 56 68 eqtr3d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ -u ( M + N ) e. NN0 ) -> ( A ^ -u ( M + N ) ) = ( ( A ^ -u M ) / ( A ^ N ) ) )
70 69 oveq2d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ -u ( M + N ) e. NN0 ) -> ( 1 / ( A ^ -u ( M + N ) ) ) = ( 1 / ( ( A ^ -u M ) / ( A ^ N ) ) ) )
71 8 4 12 54 recdivd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( 1 / ( ( A ^ -u M ) / ( A ^ N ) ) ) = ( ( A ^ N ) / ( A ^ -u M ) ) )
72 71 adantr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ -u ( M + N ) e. NN0 ) -> ( 1 / ( ( A ^ -u M ) / ( A ^ N ) ) ) = ( ( A ^ N ) / ( A ^ -u M ) ) )
73 70 72 eqtrd 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ -u ( M + N ) e. NN0 ) -> ( 1 / ( A ^ -u ( M + N ) ) ) = ( ( A ^ N ) / ( A ^ -u M ) ) )
74 47 73 eqtrd 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) /\ -u ( M + N ) e. NN0 ) -> ( A ^ ( M + N ) ) = ( ( A ^ N ) / ( A ^ -u M ) ) )
75 elznn0 
 |-  ( ( M + N ) e. ZZ <-> ( ( M + N ) e. RR /\ ( ( M + N ) e. NN0 \/ -u ( M + N ) e. NN0 ) ) )
76 75 simprbi 
 |-  ( ( M + N ) e. ZZ -> ( ( M + N ) e. NN0 \/ -u ( M + N ) e. NN0 ) )
77 21 76 syl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( ( M + N ) e. NN0 \/ -u ( M + N ) e. NN0 ) )
78 42 74 77 mpjaodan 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ ( M + N ) ) = ( ( A ^ N ) / ( A ^ -u M ) ) )
79 expneg2 
 |-  ( ( A e. CC /\ M e. CC /\ -u M e. NN0 ) -> ( A ^ M ) = ( 1 / ( A ^ -u M ) ) )
80 1 15 6 79 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ M ) = ( 1 / ( A ^ -u M ) ) )
81 80 oveq1d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( ( A ^ M ) x. ( A ^ N ) ) = ( ( 1 / ( A ^ -u M ) ) x. ( A ^ N ) ) )
82 13 78 81 3eqtr4d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) )