Proof of Theorem expaddz
Step | Hyp | Ref
| Expression |
1 | | elznn0nn 12190 |
. . 3
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨
(𝑁 ∈ ℝ ∧
-𝑁 ∈
ℕ))) |
2 | | elznn0nn 12190 |
. . . 4
⊢ (𝑀 ∈ ℤ ↔ (𝑀 ∈ ℕ0 ∨
(𝑀 ∈ ℝ ∧
-𝑀 ∈
ℕ))) |
3 | | expadd 13677 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))) |
4 | 3 | 3expia 1123 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
→ (𝑁 ∈
ℕ0 → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))) |
5 | 4 | adantlr 715 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝑀 ∈ ℕ0) → (𝑁 ∈ ℕ0
→ (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))) |
6 | | expaddzlem 13678 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0)
→ (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))) |
7 | 6 | 3expia 1123 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ)) → (𝑁 ∈ ℕ0
→ (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))) |
8 | 5, 7 | jaodan 958 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℕ0 ∨
(𝑀 ∈ ℝ ∧
-𝑀 ∈ ℕ))) →
(𝑁 ∈
ℕ0 → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))) |
9 | | expaddzlem 13678 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ0)
→ (𝐴↑(𝑁 + 𝑀)) = ((𝐴↑𝑁) · (𝐴↑𝑀))) |
10 | | simp3 1140 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ0)
→ 𝑀 ∈
ℕ0) |
11 | 10 | nn0cnd 12152 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ0)
→ 𝑀 ∈
ℂ) |
12 | | simp2l 1201 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ0)
→ 𝑁 ∈
ℝ) |
13 | 12 | recnd 10861 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ0)
→ 𝑁 ∈
ℂ) |
14 | 11, 13 | addcomd 11034 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ0)
→ (𝑀 + 𝑁) = (𝑁 + 𝑀)) |
15 | 14 | oveq2d 7229 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ0)
→ (𝐴↑(𝑀 + 𝑁)) = (𝐴↑(𝑁 + 𝑀))) |
16 | | simp1l 1199 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ0)
→ 𝐴 ∈
ℂ) |
17 | | expcl 13653 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
→ (𝐴↑𝑀) ∈
ℂ) |
18 | 16, 10, 17 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ0)
→ (𝐴↑𝑀) ∈
ℂ) |
19 | | simp1r 1200 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ0)
→ 𝐴 ≠
0) |
20 | 13 | negnegd 11180 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ0)
→ --𝑁 = 𝑁) |
21 | | simp2r 1202 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ0)
→ -𝑁 ∈
ℕ) |
22 | 21 | nnnn0d 12150 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ0)
→ -𝑁 ∈
ℕ0) |
23 | | nn0negz 12215 |
. . . . . . . . . . . . 13
⊢ (-𝑁 ∈ ℕ0
→ --𝑁 ∈
ℤ) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ0)
→ --𝑁 ∈
ℤ) |
25 | 20, 24 | eqeltrrd 2839 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ0)
→ 𝑁 ∈
ℤ) |
26 | | expclz 13660 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℂ) |
27 | 16, 19, 25, 26 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ0)
→ (𝐴↑𝑁) ∈
ℂ) |
28 | 18, 27 | mulcomd 10854 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ0)
→ ((𝐴↑𝑀) · (𝐴↑𝑁)) = ((𝐴↑𝑁) · (𝐴↑𝑀))) |
29 | 9, 15, 28 | 3eqtr4d 2787 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑀 ∈ ℕ0)
→ (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))) |
30 | 29 | 3expia 1123 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝑀 ∈ ℕ0
→ (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))) |
31 | 30 | impancom 455 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝑀 ∈ ℕ0) → ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))) |
32 | | simp2l 1201 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝑀 ∈
ℝ) |
33 | 32 | recnd 10861 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝑀 ∈
ℂ) |
34 | | simp3l 1203 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝑁 ∈
ℝ) |
35 | 34 | recnd 10861 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝑁 ∈
ℂ) |
36 | 33, 35 | negdid 11202 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -(𝑀 + 𝑁) = (-𝑀 + -𝑁)) |
37 | 36 | oveq2d 7229 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑-(𝑀 + 𝑁)) = (𝐴↑(-𝑀 + -𝑁))) |
38 | | simp1l 1199 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝐴 ∈
ℂ) |
39 | | simp2r 1202 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑀 ∈
ℕ) |
40 | 39 | nnnn0d 12150 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑀 ∈
ℕ0) |
41 | | simp3r 1204 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑁 ∈
ℕ) |
42 | 41 | nnnn0d 12150 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑁 ∈
ℕ0) |
43 | | expadd 13677 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ -𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0) → (𝐴↑(-𝑀 + -𝑁)) = ((𝐴↑-𝑀) · (𝐴↑-𝑁))) |
44 | 38, 40, 42, 43 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑(-𝑀 + -𝑁)) = ((𝐴↑-𝑀) · (𝐴↑-𝑁))) |
45 | 37, 44 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑-(𝑀 + 𝑁)) = ((𝐴↑-𝑀) · (𝐴↑-𝑁))) |
46 | 45 | oveq2d 7229 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (1 /
(𝐴↑-(𝑀 + 𝑁))) = (1 / ((𝐴↑-𝑀) · (𝐴↑-𝑁)))) |
47 | | 1t1e1 11992 |
. . . . . . . . . . 11
⊢ (1
· 1) = 1 |
48 | 47 | oveq1i 7223 |
. . . . . . . . . 10
⊢ ((1
· 1) / ((𝐴↑-𝑀) · (𝐴↑-𝑁))) = (1 / ((𝐴↑-𝑀) · (𝐴↑-𝑁))) |
49 | 46, 48 | eqtr4di 2796 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (1 /
(𝐴↑-(𝑀 + 𝑁))) = ((1 · 1) / ((𝐴↑-𝑀) · (𝐴↑-𝑁)))) |
50 | | expcl 13653 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ -𝑀 ∈ ℕ0)
→ (𝐴↑-𝑀) ∈
ℂ) |
51 | 38, 40, 50 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑-𝑀) ∈ ℂ) |
52 | | simp1r 1200 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝐴 ≠ 0) |
53 | 40 | nn0zd 12280 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑀 ∈
ℤ) |
54 | | expne0i 13667 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ -𝑀 ∈ ℤ) → (𝐴↑-𝑀) ≠ 0) |
55 | 38, 52, 53, 54 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑-𝑀) ≠ 0) |
56 | | expcl 13653 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ -𝑁 ∈ ℕ0)
→ (𝐴↑-𝑁) ∈
ℂ) |
57 | 38, 42, 56 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑-𝑁) ∈ ℂ) |
58 | 42 | nn0zd 12280 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑁 ∈
ℤ) |
59 | | expne0i 13667 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ -𝑁 ∈ ℤ) → (𝐴↑-𝑁) ≠ 0) |
60 | 38, 52, 58, 59 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑-𝑁) ≠ 0) |
61 | | ax-1cn 10787 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
62 | | divmuldiv 11532 |
. . . . . . . . . . 11
⊢ (((1
∈ ℂ ∧ 1 ∈ ℂ) ∧ (((𝐴↑-𝑀) ∈ ℂ ∧ (𝐴↑-𝑀) ≠ 0) ∧ ((𝐴↑-𝑁) ∈ ℂ ∧ (𝐴↑-𝑁) ≠ 0))) → ((1 / (𝐴↑-𝑀)) · (1 / (𝐴↑-𝑁))) = ((1 · 1) / ((𝐴↑-𝑀) · (𝐴↑-𝑁)))) |
63 | 61, 61, 62 | mpanl12 702 |
. . . . . . . . . 10
⊢ ((((𝐴↑-𝑀) ∈ ℂ ∧ (𝐴↑-𝑀) ≠ 0) ∧ ((𝐴↑-𝑁) ∈ ℂ ∧ (𝐴↑-𝑁) ≠ 0)) → ((1 / (𝐴↑-𝑀)) · (1 / (𝐴↑-𝑁))) = ((1 · 1) / ((𝐴↑-𝑀) · (𝐴↑-𝑁)))) |
64 | 51, 55, 57, 60, 63 | syl22anc 839 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ((1 /
(𝐴↑-𝑀)) · (1 / (𝐴↑-𝑁))) = ((1 · 1) / ((𝐴↑-𝑀) · (𝐴↑-𝑁)))) |
65 | 49, 64 | eqtr4d 2780 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (1 /
(𝐴↑-(𝑀 + 𝑁))) = ((1 / (𝐴↑-𝑀)) · (1 / (𝐴↑-𝑁)))) |
66 | 33, 35 | addcld 10852 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝑀 + 𝑁) ∈ ℂ) |
67 | 40, 42 | nn0addcld 12154 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (-𝑀 + -𝑁) ∈
ℕ0) |
68 | 36, 67 | eqeltrd 2838 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -(𝑀 + 𝑁) ∈
ℕ0) |
69 | | expneg2 13644 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ (𝑀 + 𝑁) ∈ ℂ ∧ -(𝑀 + 𝑁) ∈ ℕ0) → (𝐴↑(𝑀 + 𝑁)) = (1 / (𝐴↑-(𝑀 + 𝑁)))) |
70 | 38, 66, 68, 69 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑(𝑀 + 𝑁)) = (1 / (𝐴↑-(𝑀 + 𝑁)))) |
71 | | expneg2 13644 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ -𝑀 ∈ ℕ0)
→ (𝐴↑𝑀) = (1 / (𝐴↑-𝑀))) |
72 | 38, 33, 40, 71 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑𝑀) = (1 / (𝐴↑-𝑀))) |
73 | | expneg2 13644 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0)
→ (𝐴↑𝑁) = (1 / (𝐴↑-𝑁))) |
74 | 38, 35, 42, 73 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑𝑁) = (1 / (𝐴↑-𝑁))) |
75 | 72, 74 | oveq12d 7231 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ((𝐴↑𝑀) · (𝐴↑𝑁)) = ((1 / (𝐴↑-𝑀)) · (1 / (𝐴↑-𝑁)))) |
76 | 65, 70, 75 | 3eqtr4d 2787 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))) |
77 | 76 | 3expia 1123 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ)) → ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))) |
78 | 31, 77 | jaodan 958 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℕ0 ∨
(𝑀 ∈ ℝ ∧
-𝑀 ∈ ℕ))) →
((𝑁 ∈ ℝ ∧
-𝑁 ∈ ℕ) →
(𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))) |
79 | 8, 78 | jaod 859 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℕ0 ∨
(𝑀 ∈ ℝ ∧
-𝑀 ∈ ℕ))) →
((𝑁 ∈
ℕ0 ∨ (𝑁
∈ ℝ ∧ -𝑁
∈ ℕ)) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))) |
80 | 2, 79 | sylan2b 597 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝑀 ∈ ℤ) → ((𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))) |
81 | 1, 80 | syl5bi 245 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝑀 ∈ ℤ) → (𝑁 ∈ ℤ → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))) |
82 | 81 | impr 458 |
1
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))) |