expaddzlem - Metamath Proof Explorer

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

Theorem expaddzlem 14252

Description: Lemma for expaddz 14253. (Contributed by Mario Carneiro, 4-Jun-2014.)

**Assertion**
Ref	Expression
expaddzlem	⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))

**Proof of Theorem expaddzlem**
Step	Hyp	Ref	Expression
1		simp1l 1216	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → 𝐴 ∈ ℂ)
2		simp3 1156	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → 𝑁 ∈ ℕ₀)
3		expcl 14226	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → (𝐴↑𝑁) ∈ ℂ)
4	1, 2, 3	syl2anc 596	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → (𝐴↑𝑁) ∈ ℂ)
5		simp2r 1219	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → -𝑀 ∈ ℕ)
6	5	nnnn0d 12671	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → -𝑀 ∈ ℕ₀)
7		expcl 14226	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ -𝑀 ∈ ℕ₀) → (𝐴↑ -𝑀) ∈ ℂ)
8	1, 6, 7	syl2anc 596	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → (𝐴↑ -𝑀) ∈ ℂ)
9		simp1r 1217	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → 𝐴 ≠ 0)
10	5	nnzd 12723	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → -𝑀 ∈ ℤ)
11		expne0i 14241	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ -𝑀 ∈ ℤ) → (𝐴↑ -𝑀) ≠ 0)
12	1, 9, 10, 11	syl3anc 1398	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → (𝐴↑ -𝑀) ≠ 0)
13	4, 8, 12	divrec2d 12101	. 2 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → ((𝐴↑𝑁) / (𝐴↑ -𝑀)) = ((1 / (𝐴↑ -𝑀)) · (𝐴↑𝑁)))
14		simp2l 1218	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → 𝑀 ∈ ℝ)
15	14	recnd 11341	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → 𝑀 ∈ ℂ)
16	15	negnegd 11664	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → - -𝑀 = 𝑀)
17		nnnegz 12700	. . . . . . . . . 10 ⊢ ( -𝑀 ∈ ℕ → - -𝑀 ∈ ℤ)
18	5, 17	syl 18	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → - -𝑀 ∈ ℤ)
19	16, 18	eqeltrrd 2861	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → 𝑀 ∈ ℤ)
20	2	nn0zd 12722	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → 𝑁 ∈ ℤ)
21	19, 20	zaddcld 12811	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → (𝑀 + 𝑁) ∈ ℤ)
22		expclz 14231	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ (𝑀 + 𝑁) ∈ ℤ) → (𝐴↑(𝑀 + 𝑁)) ∈ ℂ)
23	1, 9, 21, 22	syl3anc 1398	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → (𝐴↑(𝑀 + 𝑁)) ∈ ℂ)
24	23	adantr 486	. . . . 5 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ (𝑀 + 𝑁) ∈ ℕ₀) → (𝐴↑(𝑀 + 𝑁)) ∈ ℂ)
25	8	adantr 486	. . . . 5 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ (𝑀 + 𝑁) ∈ ℕ₀) → (𝐴↑ -𝑀) ∈ ℂ)
26	12	adantr 486	. . . . 5 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ (𝑀 + 𝑁) ∈ ℕ₀) → (𝐴↑ -𝑀) ≠ 0)
27	24, 25, 26	divcan4d 12103	. . . 4 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ (𝑀 + 𝑁) ∈ ℕ₀) → (((𝐴↑(𝑀 + 𝑁)) · (𝐴↑ -𝑀)) / (𝐴↑ -𝑀)) = (𝐴↑(𝑀 + 𝑁)))
28	1	adantr 486	. . . . . . 7 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ (𝑀 + 𝑁) ∈ ℕ₀) → 𝐴 ∈ ℂ)
29		simpr 490	. . . . . . 7 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ (𝑀 + 𝑁) ∈ ℕ₀) → (𝑀 + 𝑁) ∈ ℕ₀)
30	6	adantr 486	. . . . . . 7 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ (𝑀 + 𝑁) ∈ ℕ₀) → -𝑀 ∈ ℕ₀)
31		expadd 14251	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (𝑀 + 𝑁) ∈ ℕ₀ ∧ -𝑀 ∈ ℕ₀) → (𝐴↑((𝑀 + 𝑁) + -𝑀)) = ((𝐴↑(𝑀 + 𝑁)) · (𝐴↑ -𝑀)))
32	28, 29, 30, 31	syl3anc 1398	. . . . . 6 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ (𝑀 + 𝑁) ∈ ℕ₀) → (𝐴↑((𝑀 + 𝑁) + -𝑀)) = ((𝐴↑(𝑀 + 𝑁)) · (𝐴↑ -𝑀)))
33	21	zcnd 12808	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → (𝑀 + 𝑁) ∈ ℂ)
34	33, 15	negsubd 11679	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → ((𝑀 + 𝑁) + -𝑀) = ((𝑀 + 𝑁) − 𝑀))
35	2	nn0cnd 12673	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → 𝑁 ∈ ℂ)
36	15, 35	pncan2d 11675	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → ((𝑀 + 𝑁) − 𝑀) = 𝑁)
37	34, 36	eqtrd 2795	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → ((𝑀 + 𝑁) + -𝑀) = 𝑁)
38	37	adantr 486	. . . . . . 7 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ (𝑀 + 𝑁) ∈ ℕ₀) → ((𝑀 + 𝑁) + -𝑀) = 𝑁)
39	38	oveq2d 7437	. . . . . 6 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ (𝑀 + 𝑁) ∈ ℕ₀) → (𝐴↑((𝑀 + 𝑁) + -𝑀)) = (𝐴↑𝑁))
40	32, 39	eqtr3d 2797	. . . . 5 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ (𝑀 + 𝑁) ∈ ℕ₀) → ((𝐴↑(𝑀 + 𝑁)) · (𝐴↑ -𝑀)) = (𝐴↑𝑁))
41	40	oveq1d 7436	. . . 4 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ (𝑀 + 𝑁) ∈ ℕ₀) → (((𝐴↑(𝑀 + 𝑁)) · (𝐴↑ -𝑀)) / (𝐴↑ -𝑀)) = ((𝐴↑𝑁) / (𝐴↑ -𝑀)))
42	27, 41	eqtr3d 2797	. . 3 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ (𝑀 + 𝑁) ∈ ℕ₀) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑁) / (𝐴↑ -𝑀)))
43	1	adantr 486	. . . . 5 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → 𝐴 ∈ ℂ)
44	33	adantr 486	. . . . 5 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → (𝑀 + 𝑁) ∈ ℂ)
45		simpr 490	. . . . 5 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → -(𝑀 + 𝑁) ∈ ℕ₀)
46		expneg2 14217	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (𝑀 + 𝑁) ∈ ℂ ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → (𝐴↑(𝑀 + 𝑁)) = (1 / (𝐴↑ -(𝑀 + 𝑁))))
47	43, 44, 45, 46	syl3anc 1398	. . . 4 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → (𝐴↑(𝑀 + 𝑁)) = (1 / (𝐴↑ -(𝑀 + 𝑁))))
48	21	znegcld 12809	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → -(𝑀 + 𝑁) ∈ ℤ)
49		expclz 14231	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ -(𝑀 + 𝑁) ∈ ℤ) → (𝐴↑ -(𝑀 + 𝑁)) ∈ ℂ)
50	1, 9, 48, 49	syl3anc 1398	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → (𝐴↑ -(𝑀 + 𝑁)) ∈ ℂ)
51	50	adantr 486	. . . . . . 7 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → (𝐴↑ -(𝑀 + 𝑁)) ∈ ℂ)
52	4	adantr 486	. . . . . . 7 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → (𝐴↑𝑁) ∈ ℂ)
53		expne0i 14241	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ≠ 0)
54	1, 9, 20, 53	syl3anc 1398	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → (𝐴↑𝑁) ≠ 0)
55	54	adantr 486	. . . . . . 7 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → (𝐴↑𝑁) ≠ 0)
56	51, 52, 55	divcan4d 12103	. . . . . 6 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → (((𝐴↑ -(𝑀 + 𝑁)) · (𝐴↑𝑁)) / (𝐴↑𝑁)) = (𝐴↑ -(𝑀 + 𝑁)))
57	2	adantr 486	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → 𝑁 ∈ ℕ₀)
58		expadd 14251	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ -(𝑀 + 𝑁) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝐴↑( -(𝑀 + 𝑁) + 𝑁)) = ((𝐴↑ -(𝑀 + 𝑁)) · (𝐴↑𝑁)))
59	43, 45, 57, 58	syl3anc 1398	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → (𝐴↑( -(𝑀 + 𝑁) + 𝑁)) = ((𝐴↑ -(𝑀 + 𝑁)) · (𝐴↑𝑁)))
60	15	negcld 11660	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → -𝑀 ∈ ℂ)
61	15, 35	negdi2d 11687	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → -(𝑀 + 𝑁) = ( -𝑀 − 𝑁))
62	60, 35, 61	mvrrsubd 11733	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → ( -(𝑀 + 𝑁) + 𝑁) = -𝑀)
63	62	adantr 486	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → ( -(𝑀 + 𝑁) + 𝑁) = -𝑀)
64	63	oveq2d 7437	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → (𝐴↑( -(𝑀 + 𝑁) + 𝑁)) = (𝐴↑ -𝑀))
65	59, 64	eqtr3d 2797	. . . . . . 7 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → ((𝐴↑ -(𝑀 + 𝑁)) · (𝐴↑𝑁)) = (𝐴↑ -𝑀))
66	65	oveq1d 7436	. . . . . 6 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → (((𝐴↑ -(𝑀 + 𝑁)) · (𝐴↑𝑁)) / (𝐴↑𝑁)) = ((𝐴↑ -𝑀) / (𝐴↑𝑁)))
67	56, 66	eqtr3d 2797	. . . . 5 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → (𝐴↑ -(𝑀 + 𝑁)) = ((𝐴↑ -𝑀) / (𝐴↑𝑁)))
68	67	oveq2d 7437	. . . 4 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → (1 / (𝐴↑ -(𝑀 + 𝑁))) = (1 / ((𝐴↑ -𝑀) / (𝐴↑𝑁))))
69	8, 4, 12, 54	recdivd 12114	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → (1 / ((𝐴↑ -𝑀) / (𝐴↑𝑁))) = ((𝐴↑𝑁) / (𝐴↑ -𝑀)))
70	69	adantr 486	. . . 4 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → (1 / ((𝐴↑ -𝑀) / (𝐴↑𝑁))) = ((𝐴↑𝑁) / (𝐴↑ -𝑀)))
71	47, 68, 70	3eqtrd 2799	. . 3 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) ∧ -(𝑀 + 𝑁) ∈ ℕ₀) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑁) / (𝐴↑ -𝑀)))
72		elznn0 12712	. . . . 5 ⊢ ((𝑀 + 𝑁) ∈ ℤ ↔ ((𝑀 + 𝑁) ∈ ℝ ∧ ((𝑀 + 𝑁) ∈ ℕ₀ ∨ -(𝑀 + 𝑁) ∈ ℕ₀)))
73	72	simprbi 503	. . . 4 ⊢ ((𝑀 + 𝑁) ∈ ℤ → ((𝑀 + 𝑁) ∈ ℕ₀ ∨ -(𝑀 + 𝑁) ∈ ℕ₀))
74	21, 73	syl 18	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → ((𝑀 + 𝑁) ∈ ℕ₀ ∨ -(𝑀 + 𝑁) ∈ ℕ₀))
75	42, 71, 74	mpjaodan 973	. 2 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑁) / (𝐴↑ -𝑀)))
76		expneg2 14217	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ -𝑀 ∈ ℕ₀) → (𝐴↑𝑀) = (1 / (𝐴↑ -𝑀)))
77	1, 15, 6, 76	syl3anc 1398	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → (𝐴↑𝑀) = (1 / (𝐴↑ -𝑀)))
78	77	oveq1d 7436	. 2 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → ((𝐴↑𝑀) · (𝐴↑𝑁)) = ((1 / (𝐴↑ -𝑀)) · (𝐴↑𝑁)))
79	13, 75, 78	3eqtr4d 2805	1 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ₀) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 (class class class)co 7421 ℂcc 11202 ℝcr 11203 0cc0 11204 1c1 11205 + caddc 11207 · cmul 11209 − cmin 11545 -cneg 11546 / cdiv 11977 ℕcn 12339 ℕ₀cn0 12610 ℤcz 12697 ↑cexp 14208

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-cnex 11260 ax-resscn 11261 ax-1cn 11262 ax-icn 11263 ax-addcl 11264 ax-addrcl 11265 ax-mulcl 11266 ax-mulrcl 11267 ax-mulcom 11268 ax-addass 11269 ax-mulass 11270 ax-distr 11271 ax-i2m1 11272 ax-1ne0 11273 ax-1rid 11274 ax-rnegex 11275 ax-rrecex 11276 ax-cnre 11277 ax-pre-lttri 11278 ax-pre-lttrn 11279 ax-pre-ltadd 11280 ax-pre-mulgt0 11281

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-om 7879 df-2nd 8003 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-er 8721 df-en 8978 df-dom 8979 df-sdom 8980 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352 df-le 11353 df-sub 11547 df-neg 11548 df-div 11978 df-nn 12340 df-n0 12611 df-z 12698 df-uz 12970 df-seq 14149 df-exp 14209

This theorem is used by: expaddz 14253

W3C validator