expaddz - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > expaddz		Structured version Visualization version GIF version

Theorem expaddz 14279

Description: Sum of exponents law for integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by Mario Carneiro, 4-Jun-2014.)

**Assertion**
Ref	Expression
expaddz	⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))

**Proof of Theorem expaddz**
Step	Hyp	Ref	Expression
1		elznn0nn 12737	. . 3 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ₀ ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)))
2		elznn0nn 12737	. . . 4 ⊢ (𝑀 ∈ ℤ ↔ (𝑀 ∈ ℕ₀ ∨ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ)))
3		expadd 14277	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))
4	3	3expia 1139	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ₀) → (𝑁 ∈ ℕ₀ → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))))
5	4	adantlr 728	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝑀 ∈ ℕ₀) → (𝑁 ∈ ℕ₀ → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))))
6		expaddzlem 14278	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))
7	6	3expia 1139	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ)) → (𝑁 ∈ ℕ₀ → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))))
8	5, 7	jaodan 972	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℕ₀ ∨ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ))) → (𝑁 ∈ ℕ₀ → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))))
9		expaddzlem 14278	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → (𝐴↑(𝑁 + 𝑀)) = ((𝐴↑𝑁) · (𝐴↑𝑀)))
10		simp3 1156	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → 𝑀 ∈ ℕ₀)
11	10	nn0cnd 12699	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → 𝑀 ∈ ℂ)
12		simp2l 1218	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → 𝑁 ∈ ℝ)
13	12	recnd 11367	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → 𝑁 ∈ ℂ)
14	11, 13	addcomd 11542	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → (𝑀 + 𝑁) = (𝑁 + 𝑀))
15	14	oveq2d 7462	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → (𝐴↑(𝑀 + 𝑁)) = (𝐴↑(𝑁 + 𝑀)))
16		simp1l 1216	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → 𝐴 ∈ ℂ)
17		expcl 14252	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ₀) → (𝐴↑𝑀) ∈ ℂ)
18	16, 10, 17	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → (𝐴↑𝑀) ∈ ℂ)
19		simp1r 1217	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → 𝐴 ≠ 0)
20	13	negnegd 11690	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → - -𝑁 = 𝑁)
21		simp2r 1219	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → -𝑁 ∈ ℕ)
22	21	nnnn0d 12697	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → -𝑁 ∈ ℕ₀)
23		nn0negz 12764	. . . . . . . . . . . . 13 ⊢ ( -𝑁 ∈ ℕ₀ → - -𝑁 ∈ ℤ)
24	22, 23	syl 18	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → - -𝑁 ∈ ℤ)
25	20, 24	eqeltrrd 2865	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → 𝑁 ∈ ℤ)
26		expclz 14257	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℂ)
27	16, 19, 25, 26	syl3anc 1399	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → (𝐴↑𝑁) ∈ ℂ)
28	18, 27	mulcomd 11360	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → ((𝐴↑𝑀) · (𝐴↑𝑁)) = ((𝐴↑𝑁) · (𝐴↑𝑀)))
29	9, 15, 28	3eqtr4d 2808	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))
30	29	3expia 1139	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝑀 ∈ ℕ₀ → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))))
31	30	impancom 457	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝑀 ∈ ℕ₀) → ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))))
32		simp2l 1218	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝑀 ∈ ℝ)
33	32	recnd 11367	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝑀 ∈ ℂ)
34		simp3l 1220	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝑁 ∈ ℝ)
35	34	recnd 11367	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝑁 ∈ ℂ)
36	33, 35	negdid 11712	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -(𝑀 + 𝑁) = ( -𝑀 + -𝑁))
37	36	oveq2d 7462	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑ -(𝑀 + 𝑁)) = (𝐴↑( -𝑀 + -𝑁)))
38		simp1l 1216	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝐴 ∈ ℂ)
39		simp2r 1219	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑀 ∈ ℕ)
40	39	nnnn0d 12697	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑀 ∈ ℕ₀)
41		simp3r 1221	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑁 ∈ ℕ)
42	41	nnnn0d 12697	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑁 ∈ ℕ₀)
43		expadd 14277	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ -𝑀 ∈ ℕ₀ ∧ -𝑁 ∈ ℕ₀) → (𝐴↑( -𝑀 + -𝑁)) = ((𝐴↑ -𝑀) · (𝐴↑ -𝑁)))
44	38, 40, 42, 43	syl3anc 1399	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑( -𝑀 + -𝑁)) = ((𝐴↑ -𝑀) · (𝐴↑ -𝑁)))
45	37, 44	eqtrd 2798	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑ -(𝑀 + 𝑁)) = ((𝐴↑ -𝑀) · (𝐴↑ -𝑁)))
46	45	oveq2d 7462	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (1 / (𝐴↑ -(𝑀 + 𝑁))) = (1 / ((𝐴↑ -𝑀) · (𝐴↑ -𝑁))))
47		1t1e1 12534	. . . . . . . . . . 11 ⊢ (1 · 1) = 1
48	47	oveq1i 7456	. . . . . . . . . 10 ⊢ ((1 · 1) / ((𝐴↑ -𝑀) · (𝐴↑ -𝑁))) = (1 / ((𝐴↑ -𝑀) · (𝐴↑ -𝑁)))
49	46, 48	eqtr4di 2816	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (1 / (𝐴↑ -(𝑀 + 𝑁))) = ((1 · 1) / ((𝐴↑ -𝑀) · (𝐴↑ -𝑁))))
50		expcl 14252	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ -𝑀 ∈ ℕ₀) → (𝐴↑ -𝑀) ∈ ℂ)
51	38, 40, 50	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑ -𝑀) ∈ ℂ)
52		simp1r 1217	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝐴 ≠ 0)
53	40	nn0zd 12748	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑀 ∈ ℤ)
54		expne0i 14267	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ -𝑀 ∈ ℤ) → (𝐴↑ -𝑀) ≠ 0)
55	38, 52, 53, 54	syl3anc 1399	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑ -𝑀) ≠ 0)
56		expcl 14252	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ -𝑁 ∈ ℕ₀) → (𝐴↑ -𝑁) ∈ ℂ)
57	38, 42, 56	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑ -𝑁) ∈ ℂ)
58	42	nn0zd 12748	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑁 ∈ ℤ)
59		expne0i 14267	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ -𝑁 ∈ ℤ) → (𝐴↑ -𝑁) ≠ 0)
60	38, 52, 58, 59	syl3anc 1399	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑ -𝑁) ≠ 0)
61		ax-1cn 11288	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
62		divmuldiv 12047	. . . . . . . . . . 11 ⊢ (((1 ∈ ℂ ∧ 1 ∈ ℂ) ∧ (((𝐴↑ -𝑀) ∈ ℂ ∧ (𝐴↑ -𝑀) ≠ 0) ∧ ((𝐴↑ -𝑁) ∈ ℂ ∧ (𝐴↑ -𝑁) ≠ 0))) → ((1 / (𝐴↑ -𝑀)) · (1 / (𝐴↑ -𝑁))) = ((1 · 1) / ((𝐴↑ -𝑀) · (𝐴↑ -𝑁))))
63	61, 61, 62	mpanl12 715	. . . . . . . . . 10 ⊢ ((((𝐴↑ -𝑀) ∈ ℂ ∧ (𝐴↑ -𝑀) ≠ 0) ∧ ((𝐴↑ -𝑁) ∈ ℂ ∧ (𝐴↑ -𝑁) ≠ 0)) → ((1 / (𝐴↑ -𝑀)) · (1 / (𝐴↑ -𝑁))) = ((1 · 1) / ((𝐴↑ -𝑀) · (𝐴↑ -𝑁))))
64	51, 55, 57, 60, 63	syl22anc 852	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ((1 / (𝐴↑ -𝑀)) · (1 / (𝐴↑ -𝑁))) = ((1 · 1) / ((𝐴↑ -𝑀) · (𝐴↑ -𝑁))))
65	49, 64	eqtr4d 2801	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (1 / (𝐴↑ -(𝑀 + 𝑁))) = ((1 / (𝐴↑ -𝑀)) · (1 / (𝐴↑ -𝑁))))
66	33, 35	addcld 11358	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝑀 + 𝑁) ∈ ℂ)
67	40, 42	nn0addcld 12701	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ( -𝑀 + -𝑁) ∈ ℕ₀)
68	36, 67	eqeltrd 2864	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -(𝑀 + 𝑁) ∈ ℕ₀)
69		expneg2 14243	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (𝑀 + 𝑁) ∈ ℂ ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → (𝐴↑(𝑀 + 𝑁)) = (1 / (𝐴↑ -(𝑀 + 𝑁))))
70	38, 66, 68, 69	syl3anc 1399	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑(𝑀 + 𝑁)) = (1 / (𝐴↑ -(𝑀 + 𝑁))))
71		expneg2 14243	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ -𝑀 ∈ ℕ₀) → (𝐴↑𝑀) = (1 / (𝐴↑ -𝑀)))
72	38, 33, 40, 71	syl3anc 1399	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑𝑀) = (1 / (𝐴↑ -𝑀)))
73		expneg2 14243	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ₀) → (𝐴↑𝑁) = (1 / (𝐴↑ -𝑁)))
74	38, 35, 42, 73	syl3anc 1399	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑𝑁) = (1 / (𝐴↑ -𝑁)))
75	72, 74	oveq12d 7464	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ((𝐴↑𝑀) · (𝐴↑𝑁)) = ((1 / (𝐴↑ -𝑀)) · (1 / (𝐴↑ -𝑁))))
76	65, 70, 75	3eqtr4d 2808	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))
77	76	3expia 1139	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ)) → ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))))
78	31, 77	jaodan 972	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℕ₀ ∨ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ))) → ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))))
79	8, 78	jaod 873	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℕ₀ ∨ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ))) → ((𝑁 ∈ ℕ₀ ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))))
80	2, 79	sylan2b 606	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝑀 ∈ ℤ) → ((𝑁 ∈ ℕ₀ ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))))
81	1, 80	biimtrid 245	. 2 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝑀 ∈ ℤ) → (𝑁 ∈ ℤ → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))))
82	81	impr 460	1 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 (class class class)co 7446 ℂcc 11228 ℝcr 11229 0cc0 11230 1c1 11231 + caddc 11233 · cmul 11235 -cneg 11572 / cdiv 12003 ℕcn 12365 ℕ₀cn0 12636 ℤcz 12723 ↑cexp 14234

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778 ax-cnex 11286 ax-resscn 11287 ax-1cn 11288 ax-icn 11289 ax-addcl 11290 ax-addrcl 11291 ax-mulcl 11292 ax-mulrcl 11293 ax-mulcom 11294 ax-addass 11295 ax-mulass 11296 ax-distr 11297 ax-i2m1 11298 ax-1ne0 11299 ax-1rid 11300 ax-rnegex 11301 ax-rrecex 11302 ax-cnre 11303 ax-pre-lttri 11304 ax-pre-lttrn 11305 ax-pre-ltadd 11306 ax-pre-mulgt0 11307

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-iun 4956 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6325 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7403 df-ov 7449 df-oprab 7450 df-mpo 7451 df-om 7905 df-2nd 8029 df-frecs 8330 df-wrecs 8361 df-recs 8410 df-rdg 8449 df-er 8748 df-en 9005 df-dom 9006 df-sdom 9007 df-pnf 11375 df-mnf 11376 df-xr 11377 df-ltxr 11378 df-le 11379 df-sub 11573 df-neg 11574 df-div 12004 df-nn 12366 df-n0 12637 df-z 12724 df-uz 12996 df-seq 14175 df-exp 14235

This theorem is used by: m1expeven 14282 expsub 14283 expp1z 14284 iseraltlem2 15882 iseraltlem3 15883 pcaddlem 17098 m1expaddsub 19745 expghm 21814 aaliou3lem2 26703 aaliou3lem6 26708 dchrptlem1 27624 dchrptlem2 27625 lgseisenlem4 27738 lgsquadlem1 27740 lgsquad2lem1 27744 padicabv 27990 cos9thpiminplylem5 34501 knoppndvlem2 37570 knoppndvlem14 37582 pellfund14 44109 rmxyadd 44132

W3C validator