HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem expaddt 6527
Description: Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135.
Assertion
Ref Expression
expaddt |- ((A e. CC /\ M e. NN0 /\ N e. NN0) -> (A^(M + N)) = ((A^M) x. (A^N)))
Proof of Theorem expaddt
StepHypRef Expression
1 opreq2 3954 . . . . . . . 8 |- (j = 0 -> (M + j) = (M + 0))
21opreq2d 3961 . . . . . . 7 |- (j = 0 -> (A^(M + j)) = (A^(M + 0)))
3 opreq2 3954 . . . . . . . 8 |- (j = 0 -> (A^j) = (A^0))
43opreq2d 3961 . . . . . . 7 |- (j = 0 -> ((A^M) x. (A^j)) = ((A^M) x. (A^0)))
52, 4eqeq12d 1481 . . . . . 6 |- (j = 0 -> ((A^(M + j)) = ((A^M) x. (A^j)) <-> (A^(M + 0)) = ((A^M) x. (A^0))))
65imbi2d 610 . . . . 5 |- (j = 0 -> (((A e. CC /\ M e. NN0) -> (A^(M + j)) = ((A^M) x. (A^j))) <-> ((A e. CC /\ M e. NN0) -> (A^(M + 0)) = ((A^M) x. (A^0)))))
7 opreq2 3954 . . . . . . . 8 |- (j = k -> (M + j) = (M + k))
87opreq2d 3961 . . . . . . 7 |- (j = k -> (A^(M + j)) = (A^(M + k)))
9 opreq2 3954 . . . . . . . 8 |- (j = k -> (A^j) = (A^k))
109opreq2d 3961 . . . . . . 7 |- (j = k -> ((A^M) x. (A^j)) = ((A^M) x. (A^k)))
118, 10eqeq12d 1481 . . . . . 6 |- (j = k -> ((A^(M + j)) = ((A^M) x. (A^j)) <-> (A^(M + k)) = ((A^M) x. (A^k))))
1211imbi2d 610 . . . . 5 |- (j = k -> (((A e. CC /\ M e. NN0) -> (A^(M + j)) = ((A^M) x. (A^j))) <-> ((A e. CC /\ M e. NN0) -> (A^(M + k)) = ((A^M) x. (A^k)))))
13 opreq2 3954 . . . . . . . 8 |- (j = (k + 1) -> (M + j) = (M + (k + 1)))
1413opreq2d 3961 . . . . . . 7 |- (j = (k + 1) -> (A^(M + j)) = (A^(M + (k + 1))))
15 opreq2 3954 . . . . . . . 8 |- (j = (k + 1) -> (A^j) = (A^(k + 1)))
1615opreq2d 3961 . . . . . . 7 |- (j = (k + 1) -> ((A^M) x. (A^j)) = ((A^M) x. (A^(k + 1))))
1714, 16eqeq12d 1481 . . . . . 6 |- (j = (k + 1) -> ((A^(M + j)) = ((A^M) x. (A^j)) <-> (A^(M + (k + 1))) = ((A^M) x. (A^(k + 1)))))
1817imbi2d 610 . . . . 5 |- (j = (k + 1) -> (((A e. CC /\ M e. NN0) -> (A^(M + j)) = ((A^M) x. (A^j))) <-> ((A e. CC /\ M e. NN0) -> (A^(M + (k + 1))) = ((A^M) x. (A^(k + 1))))))
19 opreq2 3954 . . . . . . . 8 |- (j = N -> (M + j) = (M + N))
2019opreq2d 3961 . . . . . . 7 |- (j = N -> (A^(M + j)) = (A^(M + N)))
21 opreq2 3954 . . . . . . . 8 |- (j = N -> (A^j) = (A^N))
2221opreq2d 3961 . . . . . . 7 |- (j = N -> ((A^M) x. (A^j)) = ((A^M) x. (A^N)))
2320, 22eqeq12d 1481 . . . . . 6 |- (j = N -> ((A^(M + j)) = ((A^M) x. (A^j)) <-> (A^(M + N)) = ((A^M) x. (A^N))))
2423imbi2d 610 . . . . 5 |- (j = N -> (((A e. CC /\ M e. NN0) -> (A^(M + j)) = ((A^M) x. (A^j))) <-> ((A e. CC /\ M e. NN0) -> (A^(M + N)) = ((A^M) x. (A^N)))))
25 expclt 6513 . . . . . . 7 |- ((A e. CC /\ M e. NN0) -> (A^M) e. CC)
26 ax1id 5254 . . . . . . 7 |- ((A^M) e. CC -> ((A^M) x. 1) = (A^M))
2725, 26syl 10 . . . . . 6 |- ((A e. CC /\ M e. NN0) -> ((A^M) x. 1) = (A^M))
28 exp0t 6503 . . . . . . . 8 |- (A e. CC -> (A^0) = 1)
2928adantr 389 . . . . . . 7 |- ((A e. CC /\ M e. NN0) -> (A^0) = 1)
3029opreq2d 3961 . . . . . 6 |- ((A e. CC /\ M e. NN0) -> ((A^M) x. (A^0)) = ((A^M) x. 1))
31 nn0cnt 6056 . . . . . . . . 9 |- (M e. NN0 -> M e. CC)
32 ax0id 5253 . . . . . . . . 9 |- (M e. CC -> (M + 0) = M)
3331, 32syl 10 . . . . . . . 8 |- (M e. NN0 -> (M + 0) = M)
3433adantl 388 . . . . . . 7 |- ((A e. CC /\ M e. NN0) -> (M + 0) = M)
3534opreq2d 3961 . . . . . 6 |- ((A e. CC /\ M e. NN0) -> (A^(M + 0)) = (A^M))
3627, 30, 353eqtr4rd 1510 . . . . 5 |- ((A e. CC /\ M e. NN0) -> (A^(M + 0)) = ((A^M) x. (A^0)))
37 ax1cn 5241 . . . . . . . . . . . . . 14 |- 1 e. CC
38 axaddass 5249 . . . . . . . . . . . . . 14 |- ((M e. CC /\ k e. CC /\ 1 e. CC) -> ((M + k) + 1) = (M + (k + 1)))
3937, 38mp3an3 902 . . . . . . . . . . . . 13 |- ((M e. CC /\ k e. CC) -> ((M + k) + 1) = (M + (k + 1)))
40 nn0cnt 6056 . . . . . . . . . . . . 13 |- (k e. NN0 -> k e. CC)
4139, 31, 40syl2an 454 . . . . . . . . . . . 12 |- ((M e. NN0 /\ k e. NN0) -> ((M + k) + 1) = (M + (k + 1)))
4241adantll 392 . . . . . . . . . . 11 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> ((M + k) + 1) = (M + (k + 1)))
4342opreq2d 3961 . . . . . . . . . 10 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (A^((M + k) + 1)) = (A^(M + (k + 1))))
44 expp1t 6506 . . . . . . . . . . 11 |- ((A e. CC /\ (M + k) e. NN0) -> (A^((M + k) + 1)) = ((A^(M + k)) x. A))
45 simpll 412 . . . . . . . . . . 11 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> A e. CC)
46 nn0addclt 6067 . . . . . . . . . . . 12 |- ((M e. NN0 /\ k e. NN0) -> (M + k) e. NN0)
4746adantll 392 . . . . . . . . . . 11 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (M + k) e. NN0)
4844, 45, 47sylanc 471 . . . . . . . . . 10 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (A^((M + k) + 1)) = ((A^(M + k)) x. A))
4943, 48eqtr3d 1501 . . . . . . . . 9 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (A^(M + (k + 1))) = ((A^(M + k)) x. A))
50 expp1t 6506 . . . . . . . . . . . 12 |- ((A e. CC /\ k e. NN0) -> (A^(k + 1)) = ((A^k) x. A))
5150adantlr 393 . . . . . . . . . . 11 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (A^(k + 1)) = ((A^k) x. A))
5251opreq2d 3961 . . . . . . . . . 10 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> ((A^M) x. (A^(k + 1))) = ((A^M) x. ((A^k) x. A)))
53 axmulass 5250 . . . . . . . . . . 11 |- (((A^M) e. CC /\ (A^k) e. CC /\ A e. CC) -> (((A^M) x. (A^k)) x. A) = ((A^M) x. ((A^k) x. A)))
5425adantr 389 . . . . . . . . . . 11 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (A^M) e. CC)
55 expclt 6513 . . . . . . . . . . . 12 |- ((A e. CC /\ k e. NN0) -> (A^k) e. CC)
5655adantlr 393 . . . . . . . . . . 11 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (A^k) e. CC)
5753, 54, 56, 45syl3anc 856 . . . . . . . . . 10 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (((A^M) x. (A^k)) x. A) = ((A^M) x. ((A^k) x. A)))
5852, 57eqtr4d 1502 . . . . . . . . 9 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> ((A^M) x. (A^