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