This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem expaddzlem

Description: Lemma for expaddz . (Contributed by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion expaddzlem ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 simp1l ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
2 simp3 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
3 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
4 1 2 3 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
5 simp2r ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → - 𝑀 ∈ ℕ )
6 5 nnnn0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → - 𝑀 ∈ ℕ0 )
7 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ - 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝑀 ) ∈ ℂ )
8 1 6 7 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝑀 ) ∈ ℂ )
9 simp1r ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ≠ 0 )
10 5 nnzd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → - 𝑀 ∈ ℤ )
11 expne0i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ - 𝑀 ∈ ℤ ) → ( 𝐴 ↑ - 𝑀 ) ≠ 0 )
12 1 9 10 11 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝑀 ) ≠ 0 )
13 4 8 12 divrec2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ - 𝑀 ) ) = ( ( 1 / ( 𝐴 ↑ - 𝑀 ) ) · ( 𝐴 ↑ 𝑁 ) ) )
14 simp2l ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → 𝑀 ∈ ℝ )
15 14 recnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → 𝑀 ∈ ℂ )
16 15 negnegd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → - - 𝑀 = 𝑀 )
17 nnnegz ⊢ ( - 𝑀 ∈ ℕ → - - 𝑀 ∈ ℤ )
18 5 17 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → - - 𝑀 ∈ ℤ )
19 16 18 eqeltrrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → 𝑀 ∈ ℤ )
20 2 nn0zd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
21 19 20 zaddcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
22 expclz ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ) → ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) ∈ ℂ )
23 1 9 21 22 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) ∈ ℂ )
24 23 adantr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) ∈ ℂ )
25 8 adantr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ - 𝑀 ) ∈ ℂ )
26 12 adantr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ - 𝑀 ) ≠ 0 )
27 24 25 26 divcan4d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) · ( 𝐴 ↑ - 𝑀 ) ) / ( 𝐴 ↑ - 𝑀 ) ) = ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) )
28 1 adantr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → 𝐴 ∈ ℂ )
29 simpr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝑀 + 𝑁 ) ∈ ℕ0 )
30 6 adantr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → - 𝑀 ∈ ℕ0 )
31 expadd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ∧ - 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( ( 𝑀 + 𝑁 ) + - 𝑀 ) ) = ( ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) · ( 𝐴 ↑ - 𝑀 ) ) )
32 28 29 30 31 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( ( 𝑀 + 𝑁 ) + - 𝑀 ) ) = ( ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) · ( 𝐴 ↑ - 𝑀 ) ) )
33 21 zcnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 + 𝑁 ) ∈ ℂ )
34 33 15 negsubd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) + - 𝑀 ) = ( ( 𝑀 + 𝑁 ) − 𝑀 ) )
35 2 nn0cnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
36 15 35 pncan2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) − 𝑀 ) = 𝑁 )
37 34 36 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) + - 𝑀 ) = 𝑁 )
38 37 adantr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) + - 𝑀 ) = 𝑁 )
39 38 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( ( 𝑀 + 𝑁 ) + - 𝑀 ) ) = ( 𝐴 ↑ 𝑁 ) )
40 32 39 eqtr3d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) · ( 𝐴 ↑ - 𝑀 ) ) = ( 𝐴 ↑ 𝑁 ) )
41 40 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) · ( 𝐴 ↑ - 𝑀 ) ) / ( 𝐴 ↑ - 𝑀 ) ) = ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ - 𝑀 ) ) )
42 27 41 eqtr3d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) = ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ - 𝑀 ) ) )
43 1 adantr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → 𝐴 ∈ ℂ )
44 33 adantr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝑀 + 𝑁 ) ∈ ℂ )
45 simpr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → - ( 𝑀 + 𝑁 ) ∈ ℕ0 )
46 expneg2 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 + 𝑁 ) ∈ ℂ ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) = ( 1 / ( 𝐴 ↑ - ( 𝑀 + 𝑁 ) ) ) )
47 43 44 45 46 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) = ( 1 / ( 𝐴 ↑ - ( 𝑀 + 𝑁 ) ) ) )
48 21 znegcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → - ( 𝑀 + 𝑁 ) ∈ ℤ )
49 expclz ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ - ( 𝑀 + 𝑁 ) ∈ ℤ ) → ( 𝐴 ↑ - ( 𝑀 + 𝑁 ) ) ∈ ℂ )
50 1 9 48 49 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ - ( 𝑀 + 𝑁 ) ) ∈ ℂ )
51 50 adantr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ - ( 𝑀 + 𝑁 ) ) ∈ ℂ )
52 4 adantr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
53 expne0i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ≠ 0 )
54 1 9 20 53 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ≠ 0 )
55 54 adantr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ≠ 0 )
56 51 52 55 divcan4d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( ( 𝐴 ↑ - ( 𝑀 + 𝑁 ) ) · ( 𝐴 ↑ 𝑁 ) ) / ( 𝐴 ↑ 𝑁 ) ) = ( 𝐴 ↑ - ( 𝑀 + 𝑁 ) ) )
57 2 adantr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
58 expadd ⊢ ( ( 𝐴 ∈ ℂ ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ ( - ( 𝑀 + 𝑁 ) + 𝑁 ) ) = ( ( 𝐴 ↑ - ( 𝑀 + 𝑁 ) ) · ( 𝐴 ↑ 𝑁 ) ) )
59 43 45 57 58 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( - ( 𝑀 + 𝑁 ) + 𝑁 ) ) = ( ( 𝐴 ↑ - ( 𝑀 + 𝑁 ) ) · ( 𝐴 ↑ 𝑁 ) ) )
60 15 35 negdi2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → - ( 𝑀 + 𝑁 ) = ( - 𝑀 − 𝑁 ) )
61 60 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( - ( 𝑀 + 𝑁 ) + 𝑁 ) = ( ( - 𝑀 − 𝑁 ) + 𝑁 ) )
62 15 negcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → - 𝑀 ∈ ℂ )
63 62 35 npcand ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( - 𝑀 − 𝑁 ) + 𝑁 ) = - 𝑀 )
64 61 63 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( - ( 𝑀 + 𝑁 ) + 𝑁 ) = - 𝑀 )
65 64 adantr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( - ( 𝑀 + 𝑁 ) + 𝑁 ) = - 𝑀 )
66 65 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( - ( 𝑀 + 𝑁 ) + 𝑁 ) ) = ( 𝐴 ↑ - 𝑀 ) )
67 59 66 eqtr3d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( 𝐴 ↑ - ( 𝑀 + 𝑁 ) ) · ( 𝐴 ↑ 𝑁 ) ) = ( 𝐴 ↑ - 𝑀 ) )
68 67 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( ( 𝐴 ↑ - ( 𝑀 + 𝑁 ) ) · ( 𝐴 ↑ 𝑁 ) ) / ( 𝐴 ↑ 𝑁 ) ) = ( ( 𝐴 ↑ - 𝑀 ) / ( 𝐴 ↑ 𝑁 ) ) )
69 56 68 eqtr3d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ - ( 𝑀 + 𝑁 ) ) = ( ( 𝐴 ↑ - 𝑀 ) / ( 𝐴 ↑ 𝑁 ) ) )
70 69 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 1 / ( 𝐴 ↑ - ( 𝑀 + 𝑁 ) ) ) = ( 1 / ( ( 𝐴 ↑ - 𝑀 ) / ( 𝐴 ↑ 𝑁 ) ) ) )
71 8 4 12 54 recdivd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 1 / ( ( 𝐴 ↑ - 𝑀 ) / ( 𝐴 ↑ 𝑁 ) ) ) = ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ - 𝑀 ) ) )
72 71 adantr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 1 / ( ( 𝐴 ↑ - 𝑀 ) / ( 𝐴 ↑ 𝑁 ) ) ) = ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ - 𝑀 ) ) )
73 70 72 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 1 / ( 𝐴 ↑ - ( 𝑀 + 𝑁 ) ) ) = ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ - 𝑀 ) ) )
74 47 73 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) = ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ - 𝑀 ) ) )
75 elznn0 ⊢ ( ( 𝑀 + 𝑁 ) ∈ ℤ ↔ ( ( 𝑀 + 𝑁 ) ∈ ℝ ∧ ( ( 𝑀 + 𝑁 ) ∈ ℕ0 ∨ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ) )
76 75 simprbi ⊢ ( ( 𝑀 + 𝑁 ) ∈ ℤ → ( ( 𝑀 + 𝑁 ) ∈ ℕ0 ∨ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) )
77 21 76 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) ∈ ℕ0 ∨ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) )
78 42 74 77 mpjaodan ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) = ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ - 𝑀 ) ) )
79 expneg2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ - 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑀 ) = ( 1 / ( 𝐴 ↑ - 𝑀 ) ) )
80 1 15 6 79 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑀 ) = ( 1 / ( 𝐴 ↑ - 𝑀 ) ) )
81 80 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑁 ) ) = ( ( 1 / ( 𝐴 ↑ - 𝑀 ) ) · ( 𝐴 ↑ 𝑁 ) ) )
82 13 78 81 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑁 ) ) )