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 A 0 M N A M + N = A M A N

Proof

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