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 ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) = ( ( 𝐴𝑀 ) · ( 𝐴𝑁 ) ) )

Proof

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