MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  expaddz Unicode version

Theorem expaddz 11024
Description: Sum of exponents law for integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by Mario Carneiro, 4-Jun-2014.)
Assertion
Ref Expression
expaddz  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( M  e.  ZZ  /\  N  e.  ZZ ) )  -> 
( A ^ ( M  +  N )
)  =  ( ( A ^ M )  x.  ( A ^ N ) ) )

Proof of Theorem expaddz
StepHypRef Expression
1 elznn0nn 9916 . . 3  |-  ( N  e.  ZZ  <->  ( N  e.  NN0  \/  ( N  e.  RR  /\  -u N  e.  NN ) ) )
2 elznn0nn 9916 . . . 4  |-  ( M  e.  ZZ  <->  ( M  e.  NN0  \/  ( M  e.  RR  /\  -u M  e.  NN ) ) )
3 expadd 11022 . . . . . . . 8  |-  ( ( A  e.  CC  /\  M  e.  NN0  /\  N  e.  NN0 )  ->  ( A ^ ( M  +  N ) )  =  ( ( A ^ M )  x.  ( A ^ N ) ) )
433expia 1158 . . . . . . 7  |-  ( ( A  e.  CC  /\  M  e.  NN0 )  -> 
( N  e.  NN0  ->  ( A ^ ( M  +  N )
)  =  ( ( A ^ M )  x.  ( A ^ N ) ) ) )
54adantlr 698 . . . . . 6  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  M  e.  NN0 )  ->  ( N  e. 
NN0  ->  ( A ^
( M  +  N
) )  =  ( ( A ^ M
)  x.  ( A ^ N ) ) ) )
6 expaddzlem 11023 . . . . . . 7  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( M  e.  RR  /\  -u M  e.  NN )  /\  N  e.  NN0 )  ->  ( A ^ ( M  +  N ) )  =  ( ( A ^ M )  x.  ( A ^ N ) ) )
763expia 1158 . . . . . 6  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( M  e.  RR  /\  -u M  e.  NN ) )  -> 
( N  e.  NN0  ->  ( A ^ ( M  +  N )
)  =  ( ( A ^ M )  x.  ( A ^ N ) ) ) )
85, 7jaodan 763 . . . . 5  |-  ( ( ( 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 11023 . . . . . . . . 9  |-  ( ( ( 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 962 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  M  e.  NN0 )
1110nn0cnd 9899 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  M  e.  CC )
12 simp2l 986 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  N  e.  RR )
1312recnd 8741 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  N  e.  CC )
1411, 13addcomd 8894 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  ( M  +  N )  =  ( N  +  M ) )
1514oveq2d 5726 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  ( A ^ ( M  +  N ) )  =  ( A ^ ( N  +  M )
) )
16 simp1l 984 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  A  e.  CC )
17 expcl 10999 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  M  e.  NN0 )  -> 
( A ^ M
)  e.  CC )
1816, 10, 17syl2anc 645 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  ( A ^ M )  e.  CC )
19 simp1r 985 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  A  =/=  0 )
2013negnegd 9028 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  -u -u N  =  N )
21 simp2r 987 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  -u N  e.  NN )
2221nnnn0d 9897 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  -u N  e.  NN0 )
23 nn0negz 9936 . . . . . . . . . . . . 13  |-  ( -u N  e.  NN0  ->  -u -u N  e.  ZZ )
2422, 23syl 17 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  -u -u N  e.  ZZ )
2520, 24eqeltrrd 2328 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  N  e.  ZZ )
26 expclz 11006 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  A  =/=  0  /\  N  e.  ZZ )  ->  ( A ^ N )  e.  CC )
2716, 19, 25, 26syl3anc 1187 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  ( A ^ N )  e.  CC )
2818, 27mulcomd 8736 . . . . . . . . 9  |-  ( ( ( 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
) ) )
299, 15, 283eqtr4d 2295 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  ( A ^ ( M  +  N ) )  =  ( ( A ^ M )  x.  ( A ^ N ) ) )
30293expia 1158 . . . . . . 7  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN ) )  -> 
( M  e.  NN0  ->  ( A ^ ( M  +  N )
)  =  ( ( A ^ M )  x.  ( A ^ N ) ) ) )
3130impancom 429 . . . . . 6  |-  ( ( ( 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 986 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( M  e.  RR  /\  -u M  e.  NN )  /\  ( N  e.  RR  /\  -u N  e.  NN ) )  ->  M  e.  RR )
3332recnd 8741 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( M  e.  RR  /\  -u M  e.  NN )  /\  ( N  e.  RR  /\  -u N  e.  NN ) )  ->  M  e.  CC )
34 simp3l 988 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( M  e.  RR  /\  -u M  e.  NN )  /\  ( N  e.  RR  /\  -u N  e.  NN ) )  ->  N  e.  RR )
3534recnd 8741 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( M  e.  RR  /\  -u M  e.  NN )  /\  ( N  e.  RR  /\  -u N  e.  NN ) )  ->  N  e.  CC )
3633, 35negdid 9050 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) )
3736oveq2d 5726 . . . . . . . . . . . 12  |-  ( ( ( 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 984 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( M  e.  RR  /\  -u M  e.  NN )  /\  ( N  e.  RR  /\  -u N  e.  NN ) )  ->  A  e.  CC )
39 simp2r 987 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( M  e.  RR  /\  -u M  e.  NN )  /\  ( N  e.  RR  /\  -u N  e.  NN ) )  ->  -u M  e.  NN )
4039nnnn0d 9897 . . . . . . . . . . . . 13  |-  ( ( ( 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 989 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( M  e.  RR  /\  -u M  e.  NN )  /\  ( N  e.  RR  /\  -u N  e.  NN ) )  ->  -u N  e.  NN )
4241nnnn0d 9897 . . . . . . . . . . . . 13  |-  ( ( ( 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 11022 . . . . . . . . . . . . 13  |-  ( ( A  e.  CC  /\  -u M  e.  NN0  /\  -u N  e.  NN0 )  ->  ( A ^ ( -u M  +  -u N
) )  =  ( ( A ^ -u M
)  x.  ( A ^ -u N ) ) )
4438, 40, 42, 43syl3anc 1187 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) )
4537, 44eqtrd 2285 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) )
4645oveq2d 5726 . . . . . . . . . 10  |-  ( ( ( 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 9749 . . . . . . . . . . 11  |-  ( 1  x.  1 )  =  1
4847oveq1i 5720 . . . . . . . . . 10  |-  ( ( 1  x.  1 )  /  ( ( A ^ -u M )  x.  ( A ^ -u N ) ) )  =  ( 1  / 
( ( A ^ -u M )  x.  ( A ^ -u N ) ) )
4946, 48syl6eqr 2303 . . . . . . . . 9  |-  ( ( ( 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 10999 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  -u M  e.  NN0 )  ->  ( A ^ -u M
)  e.  CC )
5138, 40, 50syl2anc 645 . . . . . . . . . 10  |-  ( ( ( 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 985 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( M  e.  RR  /\  -u M  e.  NN )  /\  ( N  e.  RR  /\  -u N  e.  NN ) )  ->  A  =/=  0 )
5340nn0zd 9994 . . . . . . . . . . 11  |-  ( ( ( 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 11012 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  A  =/=  0  /\  -u M  e.  ZZ )  ->  ( A ^ -u M )  =/=  0 )
5538, 52, 53, 54syl3anc 1187 . . . . . . . . . 10  |-  ( ( ( 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 10999 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  -u N  e.  NN0 )  ->  ( A ^ -u N
)  e.  CC )
5738, 42, 56syl2anc 645 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( M  e.  RR  /\  -u M  e.  NN )  /\  ( N  e.  RR  /\  -u N  e.  NN ) )  -> 
( A ^ -u N
)  e.  CC )
5842nn0zd 9994 . . . . . . . . . . 11  |-  ( ( ( 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 11012 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  A  =/=  0  /\  -u N  e.  ZZ )  ->  ( A ^ -u N )  =/=  0 )
6038, 52, 58, 59syl3anc 1187 . . . . . . . . . 10  |-  ( ( ( 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 8675 . . . . . . . . . . 11  |-  1  e.  CC
62 divmuldiv 9340 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) )
6361, 61, 62mpanl12 666 . . . . . . . . . 10  |-  ( ( ( ( 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 ) ) ) )
6451, 55, 57, 60, 63syl22anc 1188 . . . . . . . . 9  |-  ( ( ( 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 ) ) ) )
6549, 64eqtr4d 2288 . . . . . . . 8  |-  ( ( ( 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 ) ) ) )
6633, 35addcld 8734 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( M  e.  RR  /\  -u M  e.  NN )  /\  ( N  e.  RR  /\  -u N  e.  NN ) )  -> 
( M  +  N
)  e.  CC )
6740, 42nn0addcld 9901 . . . . . . . . . 10  |-  ( ( ( 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 )
6836, 67eqeltrd 2327 . . . . . . . . 9  |-  ( ( ( 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 10990 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ( M  +  N
)  e.  CC  /\  -u ( M  +  N
)  e.  NN0 )  ->  ( A ^ ( M  +  N )
)  =  ( 1  /  ( A ^ -u ( M  +  N
) ) ) )
7038, 66, 68, 69syl3anc 1187 . . . . . . . 8  |-  ( ( ( 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 10990 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  M  e.  CC  /\  -u M  e.  NN0 )  ->  ( A ^ M )  =  ( 1  /  ( A ^ -u M ) ) )
7238, 33, 40, 71syl3anc 1187 . . . . . . . . 9  |-  ( ( ( 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 10990 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  N  e.  CC  /\  -u N  e.  NN0 )  ->  ( A ^ N )  =  ( 1  /  ( A ^ -u N ) ) )
7438, 35, 42, 73syl3anc 1187 . . . . . . . . 9  |-  ( ( ( 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 ) ) )
7572, 74oveq12d 5728 . . . . . . . 8  |-  ( ( ( 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 ) ) ) )
7665, 70, 753eqtr4d 2295 . . . . . . 7  |-  ( ( ( 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 ) ) )
77763expia 1158 . . . . . 6  |-  ( ( ( 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 ) ) ) )
7831, 77jaodan 763 . . . . 5  |-  ( ( ( 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 ) ) ) )
798, 78jaod 371 . . . 4  |-  ( ( ( 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 ) ) ) )
802, 79sylan2b 463 . . 3  |-  ( ( ( 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 ) ) ) )
811, 80syl5bi 210 . 2  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  M  e.  ZZ )  ->  ( N  e.  ZZ  ->  ( A ^ ( M  +  N ) )  =  ( ( A ^ M )  x.  ( A ^ N ) ) ) )
8281impr 605 1  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( M  e.  ZZ  /\  N  e.  ZZ ) )  -> 
( A ^ ( M  +  N )
)  =  ( ( A ^ M )  x.  ( A ^ N ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    \/ wo 359    /\ wa 360    /\ w3a 939    = wceq 1619    e. wcel 1621    =/= wne 2412  (class class class)co 5710   CCcc 8615   RRcr 8616   0cc0 8617   1c1 8618    + caddc 8620    x. cmul 8622   -ucneg 8918    / cdiv 9303   NNcn 9626   NN0cn0 9844   ZZcz 9903   ^cexp 10982
This theorem is referenced by:  expsub  11027  expp1z  11028  iseraltlem2  12032  iseraltlem3  12033  pcaddlem  12810  expghm  16282  aaliou3lem2  19555  aaliou3lem6  19560  dchrptlem1  20335  dchrptlem2  20336  lgseisenlem4  20423  lgsquadlem1  20425  lgsquad2lem1  20429  padicabv  20611  pellfund14  26149  rmxyadd  26172  m1expaddsub  26587
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pow 4082  ax-pr 4108  ax-un 4403  ax-cnex 8673  ax-resscn 8674  ax-1cn 8675  ax-icn 8676  ax-addcl 8677  ax-addrcl 8678  ax-mulcl 8679  ax-mulrcl 8680  ax-mulcom 8681  ax-addass 8682  ax-mulass 8683  ax-distr 8684  ax-i2m1 8685  ax-1ne0 8686  ax-1rid 8687  ax-rnegex 8688  ax-rrecex 8689  ax-cnre 8690  ax-pre-lttri 8691  ax-pre-lttrn 8692  ax-pre-ltadd 8693  ax-pre-mulgt0 8694
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-nel 2415  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2516  df-v 2729  df-sbc 2922  df-csb 3010  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-pss 3091  df-nul 3363  df-if 3471  df-pw 3532  df-sn 3550  df-pr 3551  df-tp 3552  df-op 3553  df-uni 3728  df-iun 3805  df-br 3921  df-opab 3975  df-mpt 3976  df-tr 4011  df-eprel 4198  df-id 4202  df-po 4207  df-so 4208  df-fr 4245  df-we 4247  df-ord 4288  df-on 4289  df-lim 4290  df-suc 4291  df-om 4548  df-xp 4594  df-rel 4595  df-cnv 4596  df-co 4597  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-fun 4602  df-fn 4603  df-f 4604  df-f1 4605  df-fo 4606  df-f1o 4607  df-fv 4608  df-ov 5713  df-oprab 5714  df-mpt2 5715  df-2nd 5975  df-iota 6143  df-riota 6190  df-recs 6274  df-rdg 6309  df-er 6546  df-en 6750  df-dom 6751  df-sdom 6752  df-pnf 8749  df-mnf 8750  df-xr 8751  df-ltxr 8752  df-le 8753  df-sub 8919  df-neg 8920  df-div 9304  df-n 9627  df-n0 9845  df-z 9904  df-uz 10110  df-seq 10925  df-exp 10983
  Copyright terms: Public domain W3C validator