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

Metamath Proof Explorer

Theorem expmulz

Description: Product of exponents law for integer exponentiation. Proposition 10-4.2(b) of Gleason p. 135. (Contributed by Mario Carneiro, 7-Jul-2014)

Ref Expression
Assertion expmulz ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 elznn0nn ⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )
2 elznn0nn ⊢ ( 𝑀 ∈ ℤ ↔ ( 𝑀 ∈ ℕ0 ∨ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ) )
3 expmul ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) )
4 3 3expia ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 ∈ ℕ0 → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) ) )
5 4 adantlr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 ∈ ℕ0 → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) ) )
6 simp2l ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → 𝑀 ∈ ℝ )
7 6 recnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → 𝑀 ∈ ℂ )
8 simp3 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
9 8 nn0cnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
10 7 9 mulneg1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( - 𝑀 · 𝑁 ) = - ( 𝑀 · 𝑁 ) )
11 10 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ ( - 𝑀 · 𝑁 ) ) = ( 𝐴 ↑ - ( 𝑀 · 𝑁 ) ) )
12 simp1l ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
13 simp2r ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → - 𝑀 ∈ ℕ )
14 13 nnnn0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → - 𝑀 ∈ ℕ0 )
15 expmul ⊢ ( ( 𝐴 ∈ ℂ ∧ - 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ ( - 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ - 𝑀 ) ↑ 𝑁 ) )
16 12 14 8 15 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ ( - 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ - 𝑀 ) ↑ 𝑁 ) )
17 11 16 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ - ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ - 𝑀 ) ↑ 𝑁 ) )
18 17 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 1 / ( 𝐴 ↑ - ( 𝑀 · 𝑁 ) ) ) = ( 1 / ( ( 𝐴 ↑ - 𝑀 ) ↑ 𝑁 ) ) )
19 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ - 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝑀 ) ∈ ℂ )
20 12 14 19 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝑀 ) ∈ ℂ )
21 simp1r ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ≠ 0 )
22 13 nnzd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → - 𝑀 ∈ ℤ )
23 expne0i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ - 𝑀 ∈ ℤ ) → ( 𝐴 ↑ - 𝑀 ) ≠ 0 )
24 12 21 22 23 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝑀 ) ≠ 0 )
25 8 nn0zd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
26 exprec ⊢ ( ( ( 𝐴 ↑ - 𝑀 ) ∈ ℂ ∧ ( 𝐴 ↑ - 𝑀 ) ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ( 1 / ( 𝐴 ↑ - 𝑀 ) ) ↑ 𝑁 ) = ( 1 / ( ( 𝐴 ↑ - 𝑀 ) ↑ 𝑁 ) ) )
27 20 24 25 26 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 1 / ( 𝐴 ↑ - 𝑀 ) ) ↑ 𝑁 ) = ( 1 / ( ( 𝐴 ↑ - 𝑀 ) ↑ 𝑁 ) ) )
28 18 27 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 1 / ( 𝐴 ↑ - ( 𝑀 · 𝑁 ) ) ) = ( ( 1 / ( 𝐴 ↑ - 𝑀 ) ) ↑ 𝑁 ) )
29 7 9 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 · 𝑁 ) ∈ ℂ )
30 14 8 nn0mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( - 𝑀 · 𝑁 ) ∈ ℕ0 )
31 10 30 eqeltrrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → - ( 𝑀 · 𝑁 ) ∈ ℕ0 )
32 expneg2 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 · 𝑁 ) ∈ ℂ ∧ - ( 𝑀 · 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( 1 / ( 𝐴 ↑ - ( 𝑀 · 𝑁 ) ) ) )
33 12 29 31 32 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( 1 / ( 𝐴 ↑ - ( 𝑀 · 𝑁 ) ) ) )
34 expneg2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ - 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑀 ) = ( 1 / ( 𝐴 ↑ - 𝑀 ) ) )
35 12 7 14 34 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑀 ) = ( 1 / ( 𝐴 ↑ - 𝑀 ) ) )
36 35 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) = ( ( 1 / ( 𝐴 ↑ - 𝑀 ) ) ↑ 𝑁 ) )
37 28 33 36 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) )
38 37 3expia ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ) → ( 𝑁 ∈ ℕ0 → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) ) )
39 5 38 jaodan ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℕ0 ∨ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ) ) → ( 𝑁 ∈ ℕ0 → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) ) )
40 simp2 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝑀 ∈ ℕ0 )
41 40 nn0cnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝑀 ∈ ℂ )
42 simp3l ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝑁 ∈ ℝ )
43 42 recnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝑁 ∈ ℂ )
44 41 43 mulneg2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝑀 · - 𝑁 ) = - ( 𝑀 · 𝑁 ) )
45 44 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ ( 𝑀 · - 𝑁 ) ) = ( 𝐴 ↑ - ( 𝑀 · 𝑁 ) ) )
46 simp1l ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝐴 ∈ ℂ )
47 simp3r ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - 𝑁 ∈ ℕ )
48 47 nnnn0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - 𝑁 ∈ ℕ0 )
49 expmul ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · - 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) ↑ - 𝑁 ) )
50 46 40 48 49 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ ( 𝑀 · - 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) ↑ - 𝑁 ) )
51 45 50 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ - ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) ↑ - 𝑁 ) )
52 51 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 1 / ( 𝐴 ↑ - ( 𝑀 · 𝑁 ) ) ) = ( 1 / ( ( 𝐴 ↑ 𝑀 ) ↑ - 𝑁 ) ) )
53 41 43 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝑀 · 𝑁 ) ∈ ℂ )
54 40 48 nn0mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝑀 · - 𝑁 ) ∈ ℕ0 )
55 44 54 eqeltrrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - ( 𝑀 · 𝑁 ) ∈ ℕ0 )
56 46 53 55 32 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( 1 / ( 𝐴 ↑ - ( 𝑀 · 𝑁 ) ) ) )
57 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑀 ) ∈ ℂ )
58 46 40 57 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ 𝑀 ) ∈ ℂ )
59 expneg2 ⊢ ( ( ( 𝐴 ↑ 𝑀 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) = ( 1 / ( ( 𝐴 ↑ 𝑀 ) ↑ - 𝑁 ) ) )
60 58 43 48 59 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) = ( 1 / ( ( 𝐴 ↑ 𝑀 ) ↑ - 𝑁 ) ) )
61 52 56 60 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) )
62 61 3expia ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) ) )
63 simp1l ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝐴 ∈ ℂ )
64 simp2l ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝑀 ∈ ℝ )
65 64 recnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝑀 ∈ ℂ )
66 simp2r ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - 𝑀 ∈ ℕ )
67 66 nnnn0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - 𝑀 ∈ ℕ0 )
68 63 65 67 34 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ 𝑀 ) = ( 1 / ( 𝐴 ↑ - 𝑀 ) ) )
69 68 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) = ( ( 1 / ( 𝐴 ↑ - 𝑀 ) ) ↑ 𝑁 ) )
70 63 67 19 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ - 𝑀 ) ∈ ℂ )
71 simp1r ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝐴 ≠ 0 )
72 66 nnzd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - 𝑀 ∈ ℤ )
73 63 71 72 23 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ - 𝑀 ) ≠ 0 )
74 70 73 reccld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 1 / ( 𝐴 ↑ - 𝑀 ) ) ∈ ℂ )
75 simp3l ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝑁 ∈ ℝ )
76 75 recnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝑁 ∈ ℂ )
77 simp3r ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - 𝑁 ∈ ℕ )
78 77 nnnn0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - 𝑁 ∈ ℕ0 )
79 expneg2 ⊢ ( ( ( 1 / ( 𝐴 ↑ - 𝑀 ) ) ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( ( 1 / ( 𝐴 ↑ - 𝑀 ) ) ↑ 𝑁 ) = ( 1 / ( ( 1 / ( 𝐴 ↑ - 𝑀 ) ) ↑ - 𝑁 ) ) )
80 74 76 78 79 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( 1 / ( 𝐴 ↑ - 𝑀 ) ) ↑ 𝑁 ) = ( 1 / ( ( 1 / ( 𝐴 ↑ - 𝑀 ) ) ↑ - 𝑁 ) ) )
81 77 nnzd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - 𝑁 ∈ ℤ )
82 exprec ⊢ ( ( ( 𝐴 ↑ - 𝑀 ) ∈ ℂ ∧ ( 𝐴 ↑ - 𝑀 ) ≠ 0 ∧ - 𝑁 ∈ ℤ ) → ( ( 1 / ( 𝐴 ↑ - 𝑀 ) ) ↑ - 𝑁 ) = ( 1 / ( ( 𝐴 ↑ - 𝑀 ) ↑ - 𝑁 ) ) )
83 70 73 81 82 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( 1 / ( 𝐴 ↑ - 𝑀 ) ) ↑ - 𝑁 ) = ( 1 / ( ( 𝐴 ↑ - 𝑀 ) ↑ - 𝑁 ) ) )
84 83 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 1 / ( ( 1 / ( 𝐴 ↑ - 𝑀 ) ) ↑ - 𝑁 ) ) = ( 1 / ( 1 / ( ( 𝐴 ↑ - 𝑀 ) ↑ - 𝑁 ) ) ) )
85 expcl ⊢ ( ( ( 𝐴 ↑ - 𝑀 ) ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( ( 𝐴 ↑ - 𝑀 ) ↑ - 𝑁 ) ∈ ℂ )
86 70 78 85 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( 𝐴 ↑ - 𝑀 ) ↑ - 𝑁 ) ∈ ℂ )
87 expne0i ⊢ ( ( ( 𝐴 ↑ - 𝑀 ) ∈ ℂ ∧ ( 𝐴 ↑ - 𝑀 ) ≠ 0 ∧ - 𝑁 ∈ ℤ ) → ( ( 𝐴 ↑ - 𝑀 ) ↑ - 𝑁 ) ≠ 0 )
88 70 73 81 87 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( 𝐴 ↑ - 𝑀 ) ↑ - 𝑁 ) ≠ 0 )
89 86 88 recrecd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 1 / ( 1 / ( ( 𝐴 ↑ - 𝑀 ) ↑ - 𝑁 ) ) ) = ( ( 𝐴 ↑ - 𝑀 ) ↑ - 𝑁 ) )
90 expmul ⊢ ( ( 𝐴 ∈ ℂ ∧ - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ ( - 𝑀 · - 𝑁 ) ) = ( ( 𝐴 ↑ - 𝑀 ) ↑ - 𝑁 ) )
91 63 67 78 90 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ ( - 𝑀 · - 𝑁 ) ) = ( ( 𝐴 ↑ - 𝑀 ) ↑ - 𝑁 ) )
92 65 76 mul2negd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( - 𝑀 · - 𝑁 ) = ( 𝑀 · 𝑁 ) )
93 92 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ ( - 𝑀 · - 𝑁 ) ) = ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) )
94 91 93 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( 𝐴 ↑ - 𝑀 ) ↑ - 𝑁 ) = ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) )
95 84 89 94 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 1 / ( ( 1 / ( 𝐴 ↑ - 𝑀 ) ) ↑ - 𝑁 ) ) = ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) )
96 69 80 95 3eqtrrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) )
97 96 3expia ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ) → ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) ) )
98 62 97 jaodan ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℕ0 ∨ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ) ) → ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) ) )
99 39 98 jaod ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℕ0 ∨ ( 𝑀 ∈ ℝ ∧ - 𝑀 ∈ ℕ ) ) ) → ( ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) ) )
100 2 99 sylan2b ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℤ ) → ( ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) ) )
101 1 100 biimtrid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℤ ) → ( 𝑁 ∈ ℤ → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) ) )
102 101 impr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) )