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