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

Theorem expaddz 11894
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 10650 . . 3  |-  ( N  e.  ZZ  <->  ( N  e.  NN0  \/  ( N  e.  RR  /\  -u N  e.  NN ) ) )
2 elznn0nn 10650 . . . 4  |-  ( M  e.  ZZ  <->  ( M  e.  NN0  \/  ( M  e.  RR  /\  -u M  e.  NN ) ) )
3 expadd 11892 . . . . . . . 8  |-  ( ( A  e.  CC  /\  M  e.  NN0  /\  N  e.  NN0 )  ->  ( A ^ ( M  +  N ) )  =  ( ( A ^ M )  x.  ( A ^ N ) ) )
433expia 1184 . . . . . . 7  |-  ( ( A  e.  CC  /\  M  e.  NN0 )  -> 
( N  e.  NN0  ->  ( A ^ ( M  +  N )
)  =  ( ( A ^ M )  x.  ( A ^ N ) ) ) )
54adantlr 709 . . . . . 6  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  M  e.  NN0 )  ->  ( N  e. 
NN0  ->  ( A ^
( M  +  N
) )  =  ( ( A ^ M
)  x.  ( A ^ N ) ) ) )
6 expaddzlem 11893 . . . . . . 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 1184 . . . . . 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 778 . . . . 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 11893 . . . . . . . . 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 985 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  M  e.  NN0 )
1110nn0cnd 10628 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  M  e.  CC )
12 simp2l 1009 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  N  e.  RR )
1312recnd 9402 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  N  e.  CC )
1411, 13addcomd 9561 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  ( M  +  N )  =  ( N  +  M ) )
1514oveq2d 6098 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  ( A ^ ( M  +  N ) )  =  ( A ^ ( N  +  M )
) )
16 simp1l 1007 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  A  e.  CC )
17 expcl 11869 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  M  e.  NN0 )  -> 
( A ^ M
)  e.  CC )
1816, 10, 17syl2anc 656 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  ( A ^ M )  e.  CC )
19 simp1r 1008 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  A  =/=  0 )
2013negnegd 9700 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  -u -u N  =  N )
21 simp2r 1010 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  -u N  e.  NN )
2221nnnn0d 10626 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  -u N  e.  NN0 )
23 nn0negz 10673 . . . . . . . . . . . . 13  |-  ( -u N  e.  NN0  ->  -u -u N  e.  ZZ )
2422, 23syl 16 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  -u -u N  e.  ZZ )
2520, 24eqeltrrd 2510 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  N  e.  ZZ )
26 expclz 11876 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  A  =/=  0  /\  N  e.  ZZ )  ->  ( A ^ N )  e.  CC )
2716, 19, 25, 26syl3anc 1213 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( N  e.  RR  /\  -u N  e.  NN )  /\  M  e.  NN0 )  ->  ( A ^ N )  e.  CC )
2818, 27mulcomd 9397 . . . . . . . . 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 2477 . . . . . . . 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 1184 . . . . . . 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 438 . . . . . 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 1009 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( M  e.  RR  /\  -u M  e.  NN )  /\  ( N  e.  RR  /\  -u N  e.  NN ) )  ->  M  e.  RR )
3332recnd 9402 . . . . . . . . . . . . . 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 1011 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( M  e.  RR  /\  -u M  e.  NN )  /\  ( N  e.  RR  /\  -u N  e.  NN ) )  ->  N  e.  RR )
3534recnd 9402 . . . . . . . . . . . . . 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 9722 . . . . . . . . . . . . 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 6098 . . . . . . . . . . . 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 1007 . . . . . . . . . . . . 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 1010 . . . . . . . . . . . . . 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 10626 . . . . . . . . . . . . 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 1012 . . . . . . . . . . . . . 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 10626 . . . . . . . . . . . . 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 11892 . . . . . . . . . . . . 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 1213 . . . . . . . . . . . 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 2467 . . . . . . . . . . 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 6098 . . . . . . . . . 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 10459 . . . . . . . . . . 11  |-  ( 1  x.  1 )  =  1
4847oveq1i 6092 . . . . . . . . . 10  |-  ( ( 1  x.  1 )  /  ( ( A ^ -u M )  x.  ( A ^ -u N ) ) )  =  ( 1  / 
( ( A ^ -u M )  x.  ( A ^ -u N ) ) )
4946, 48syl6eqr 2485 . . . . . . . . 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 11869 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  -u M  e.  NN0 )  ->  ( A ^ -u M
)  e.  CC )
5138, 40, 50syl2anc 656 . . . . . . . . . 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 1008 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( M  e.  RR  /\  -u M  e.  NN )  /\  ( N  e.  RR  /\  -u N  e.  NN ) )  ->  A  =/=  0 )
5340nn0zd 10735 . . . . . . . . . . 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 11882 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  A  =/=  0  /\  -u M  e.  ZZ )  ->  ( A ^ -u M )  =/=  0 )
5538, 52, 53, 54syl3anc 1213 . . . . . . . . . 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 11869 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  -u N  e.  NN0 )  ->  ( A ^ -u N
)  e.  CC )
5738, 42, 56syl2anc 656 . . . . . . . . . 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 10735 . . . . . . . . . . 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 11882 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  A  =/=  0  /\  -u N  e.  ZZ )  ->  ( A ^ -u N )  =/=  0 )
6038, 52, 58, 59syl3anc 1213 . . . . . . . . . 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 9330 . . . . . . . . . . 11  |-  1  e.  CC
62 divmuldiv 10021 . . . . . . . . . . 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 677 . . . . . . . . . 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 1214 . . . . . . . . 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 2470 . . . . . . . 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 9395 . . . . . . . . 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 10630 . . . . . . . . . 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 2509 . . . . . . . . 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 11860 . . . . . . . . 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 1213 . . . . . . . 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 11860 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  M  e.  CC  /\  -u M  e.  NN0 )  ->  ( A ^ M )  =  ( 1  /  ( A ^ -u M ) ) )
7238, 33, 40, 71syl3anc 1213 . . . . . . . . 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 11860 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  N  e.  CC  /\  -u N  e.  NN0 )  ->  ( A ^ N )  =  ( 1  /  ( A ^ -u N ) ) )
7438, 35, 42, 73syl3anc 1213 . . . . . . . . 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 6100 . . . . . . . 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 2477 . . . . . . 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 1184 . . . . . 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 778 . . . . 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 380 . . . 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 472 . . 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 217 . 2  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  M  e.  ZZ )  ->  ( N  e.  ZZ  ->  ( A ^ ( M  +  N ) )  =  ( ( A ^ M )  x.  ( A ^ N ) ) ) )
8281impr 616 1  |-  ( ( ( A  e.  CC  /\  A  =/=  0 )  /\  ( M  e.  ZZ  /\  N  e.  ZZ ) )  -> 
( A ^ ( M  +  N )
)  =  ( ( A ^ M )  x.  ( A ^ N ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368    /\ wa 369    /\ w3a 960    = wceq 1364    e. wcel 1757    =/= wne 2598  (class class class)co 6082   CCcc 9270   RRcr 9271   0cc0 9272   1c1 9273    + caddc 9275    x. cmul 9277   -ucneg 9586    / cdiv 9983   NNcn 10312   NN0cn0 10569   ZZcz 10636   ^cexp 11851
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363  ax-cnex 9328  ax-resscn 9329  ax-1cn 9330  ax-icn 9331  ax-addcl 9332  ax-addrcl 9333  ax-mulcl 9334  ax-mulrcl 9335  ax-mulcom 9336  ax-addass 9337  ax-mulass 9338  ax-distr 9339  ax-i2m1 9340  ax-1ne0 9341  ax-1rid 9342  ax-rnegex 9343  ax-rrecex 9344  ax-cnre 9345  ax-pre-lttri 9346  ax-pre-lttrn 9347  ax-pre-ltadd 9348  ax-pre-mulgt0 9349
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-pss 3334  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-tp 3872  df-op 3874  df-uni 4082  df-iun 4163  df-br 4283  df-opab 4341  df-mpt 4342  df-tr 4376  df-eprel 4621  df-id 4625  df-po 4630  df-so 4631  df-fr 4668  df-we 4670  df-ord 4711  df-on 4712  df-lim 4713  df-suc 4714  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-riota 6041  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-om 6468  df-2nd 6569  df-recs 6820  df-rdg 6854  df-er 7091  df-en 7301  df-dom 7302  df-sdom 7303  df-pnf 9410  df-mnf 9411  df-xr 9412  df-ltxr 9413  df-le 9414  df-sub 9587  df-neg 9588  df-div 9984  df-nn 10313  df-n0 10570  df-z 10637  df-uz 10852  df-seq 11793  df-exp 11852
This theorem is referenced by:  expsub  11897  expp1z  11898  iseraltlem2  13146  iseraltlem3  13147  pcaddlem  13935  m1expaddsub  15986  expghm  17767  expghmOLD  17768  aaliou3lem2  21696  aaliou3lem6  21701  dchrptlem1  22490  dchrptlem2  22491  lgseisenlem4  22578  lgsquadlem1  22580  lgsquad2lem1  22584  padicabv  22766  m1expevenALT  26957  pellfund14  29086  rmxyadd  29109
  Copyright terms: Public domain W3C validator