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