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 14229

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 12688	. . 3 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ₀ ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)))
2		elznn0nn 12688	. . . 4 ⊢ (𝑀 ∈ ℤ ↔ (𝑀 ∈ ℕ₀ ∨ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ)))
3		expadd 14227	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))
4	3	3expia 1139	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ₀) → (𝑁 ∈ ℕ₀ → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))))
5	4	adantlr 728	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝑀 ∈ ℕ₀) → (𝑁 ∈ ℕ₀ → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))))
6		expaddzlem 14228	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))
7	6	3expia 1139	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ)) → (𝑁 ∈ ℕ₀ → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))))
8	5, 7	jaodan 972	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℕ₀ ∨ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ))) → (𝑁 ∈ ℕ₀ → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))))
9		expaddzlem 14228	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → (𝐴↑(𝑁 + 𝑀)) = ((𝐴↑𝑁) · (𝐴↑𝑀)))
10		simp3 1156	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → 𝑀 ∈ ℕ₀)
11	10	nn0cnd 12650	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → 𝑀 ∈ ℂ)
12		simp2l 1218	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → 𝑁 ∈ ℝ)
13	12	recnd 11318	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → 𝑁 ∈ ℂ)
14	11, 13	addcomd 11493	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → (𝑀 + 𝑁) = (𝑁 + 𝑀))
15	14	oveq2d 7428	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → (𝐴↑(𝑀 + 𝑁)) = (𝐴↑(𝑁 + 𝑀)))
16		simp1l 1216	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → 𝐴 ∈ ℂ)
17		expcl 14202	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ₀) → (𝐴↑𝑀) ∈ ℂ)
18	16, 10, 17	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → (𝐴↑𝑀) ∈ ℂ)
19		simp1r 1217	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → 𝐴 ≠ 0)
20	13	negnegd 11641	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → --𝑁 = 𝑁)
21		simp2r 1219	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → -𝑁 ∈ ℕ)
22	21	nnnn0d 12648	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → -𝑁 ∈ ℕ₀)
23		nn0negz 12715	. . . . . . . . . . . . 13 ⊢ (-𝑁 ∈ ℕ₀ → --𝑁 ∈ ℤ)
24	22, 23	syl 18	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → --𝑁 ∈ ℤ)
25	20, 24	eqeltrrd 2862	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → 𝑁 ∈ ℤ)
26		expclz 14207	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℂ)
27	16, 19, 25, 26	syl3anc 1398	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → (𝐴↑𝑁) ∈ ℂ)
28	18, 27	mulcomd 11311	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → ((𝐴↑𝑀) · (𝐴↑𝑁)) = ((𝐴↑𝑁) · (𝐴↑𝑀)))
29	9, 15, 28	3eqtr4d 2806	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ₀) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))
30	29	3expia 1139	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝑀 ∈ ℕ₀ → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))))
31	30	impancom 457	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝑀 ∈ ℕ₀) → ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))))
32		simp2l 1218	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝑀 ∈ ℝ)
33	32	recnd 11318	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝑀 ∈ ℂ)
34		simp3l 1220	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝑁 ∈ ℝ)
35	34	recnd 11318	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝑁 ∈ ℂ)
36	33, 35	negdid 11663	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -(𝑀 + 𝑁) = (-𝑀 + -𝑁))
37	36	oveq2d 7428	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑-(𝑀 + 𝑁)) = (𝐴↑(-𝑀 + -𝑁)))
38		simp1l 1216	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝐴 ∈ ℂ)
39		simp2r 1219	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑀 ∈ ℕ)
40	39	nnnn0d 12648	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑀 ∈ ℕ₀)
41		simp3r 1221	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑁 ∈ ℕ)
42	41	nnnn0d 12648	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑁 ∈ ℕ₀)
43		expadd 14227	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ -𝑀 ∈ ℕ₀ ∧ -𝑁 ∈ ℕ₀) → (𝐴↑(-𝑀 + -𝑁)) = ((𝐴↑-𝑀) · (𝐴↑-𝑁)))
44	38, 40, 42, 43	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑(-𝑀 + -𝑁)) = ((𝐴↑-𝑀) · (𝐴↑-𝑁)))
45	37, 44	eqtrd 2796	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑-(𝑀 + 𝑁)) = ((𝐴↑-𝑀) · (𝐴↑-𝑁)))
46	45	oveq2d 7428	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (1 / (𝐴↑-(𝑀 + 𝑁))) = (1 / ((𝐴↑-𝑀) · (𝐴↑-𝑁))))
47		1t1e1 12485	. . . . . . . . . . 11 ⊢ (1 · 1) = 1
48	47	oveq1i 7422	. . . . . . . . . 10 ⊢ ((1 · 1) / ((𝐴↑-𝑀) · (𝐴↑-𝑁))) = (1 / ((𝐴↑-𝑀) · (𝐴↑-𝑁)))
49	46, 48	eqtr4di 2814	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (1 / (𝐴↑-(𝑀 + 𝑁))) = ((1 · 1) / ((𝐴↑-𝑀) · (𝐴↑-𝑁))))
50		expcl 14202	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ -𝑀 ∈ ℕ₀) → (𝐴↑-𝑀) ∈ ℂ)
51	38, 40, 50	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑-𝑀) ∈ ℂ)
52		simp1r 1217	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝐴 ≠ 0)
53	40	nn0zd 12699	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑀 ∈ ℤ)
54		expne0i 14217	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ -𝑀 ∈ ℤ) → (𝐴↑-𝑀) ≠ 0)
55	38, 52, 53, 54	syl3anc 1398	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑-𝑀) ≠ 0)
56		expcl 14202	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ -𝑁 ∈ ℕ₀) → (𝐴↑-𝑁) ∈ ℂ)
57	38, 42, 56	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑-𝑁) ∈ ℂ)
58	42	nn0zd 12699	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑁 ∈ ℤ)
59		expne0i 14217	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ -𝑁 ∈ ℤ) → (𝐴↑-𝑁) ≠ 0)
60	38, 52, 58, 59	syl3anc 1398	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑-𝑁) ≠ 0)
61		ax-1cn 11239	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
62		divmuldiv 11998	. . . . . . . . . . 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 2799	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (1 / (𝐴↑-(𝑀 + 𝑁))) = ((1 / (𝐴↑-𝑀)) · (1 / (𝐴↑-𝑁))))
66	33, 35	addcld 11309	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝑀 + 𝑁) ∈ ℂ)
67	40, 42	nn0addcld 12652	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (-𝑀 + -𝑁) ∈ ℕ₀)
68	36, 67	eqeltrd 2861	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -(𝑀 + 𝑁) ∈ ℕ₀)
69		expneg2 14193	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (𝑀 + 𝑁) ∈ ℂ ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → (𝐴↑(𝑀 + 𝑁)) = (1 / (𝐴↑-(𝑀 + 𝑁))))
70	38, 66, 68, 69	syl3anc 1398	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑(𝑀 + 𝑁)) = (1 / (𝐴↑-(𝑀 + 𝑁))))
71		expneg2 14193	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ -𝑀 ∈ ℕ₀) → (𝐴↑𝑀) = (1 / (𝐴↑-𝑀)))
72	38, 33, 40, 71	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑𝑀) = (1 / (𝐴↑-𝑀)))
73		expneg2 14193	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ₀) → (𝐴↑𝑁) = (1 / (𝐴↑-𝑁)))
74	38, 35, 42, 73	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑𝑁) = (1 / (𝐴↑-𝑁)))
75	72, 74	oveq12d 7430	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ((𝐴↑𝑀) · (𝐴↑𝑁)) = ((1 / (𝐴↑-𝑀)) · (1 / (𝐴↑-𝑁))))
76	65, 70, 75	3eqtr4d 2806	. . . . . . 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 2145 ≠ wne 2956 (class class class)co 7412 ℂcc 11179 ℝcr 11180 0cc0 11181 1c1 11182 + caddc 11184 · cmul 11186 -cneg 11523 / cdiv 11954 ℕcn 12316 ℕ₀cn0 12587 ℤcz 12674 ↑cexp 14184

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 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258

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 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7867 df-2nd 7991 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-er 8701 df-en 8958 df-dom 8959 df-sdom 8960 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-div 11955 df-nn 12317 df-n0 12588 df-z 12675 df-uz 12947 df-seq 14125 df-exp 14185

This theorem is used by: m1expeven 14232 expsub 14233 expp1z 14234 iseraltlem2 15830 iseraltlem3 15831 pcaddlem 17046 m1expaddsub 19692 expghm 21761 aaliou3lem2 26652 aaliou3lem6 26657 dchrptlem1 27573 dchrptlem2 27574 lgseisenlem4 27687 lgsquadlem1 27689 lgsquad2lem1 27693 padicabv 27939 cos9thpiminplylem5 34400 knoppndvlem2 37349 knoppndvlem14 37361 pellfund14 43858 rmxyadd 43881

W3C validator