Proof of Theorem expaddzaplem
Step | Hyp | Ref
| Expression |
1 | | simp1l 927 |
. . . 4
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → A ∈
ℂ) |
2 | | simp3 905 |
. . . 4
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈
ℕ0) |
3 | | expcl 8927 |
. . . 4
⊢
((A ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (A↑𝑁) ∈
ℂ) |
4 | 1, 2, 3 | syl2anc 391 |
. . 3
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (A↑𝑁) ∈
ℂ) |
5 | | simp2r 930 |
. . . . 5
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → -𝑀 ∈
ℕ) |
6 | 5 | nnnn0d 8011 |
. . . 4
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → -𝑀 ∈
ℕ0) |
7 | | expcl 8927 |
. . . 4
⊢
((A ∈ ℂ ∧ -𝑀 ∈ ℕ0) → (A↑-𝑀) ∈
ℂ) |
8 | 1, 6, 7 | syl2anc 391 |
. . 3
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (A↑-𝑀) ∈
ℂ) |
9 | | simp1r 928 |
. . . 4
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → A # 0) |
10 | 5 | nnzd 8135 |
. . . 4
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → -𝑀 ∈
ℤ) |
11 | | expap0i 8941 |
. . . 4
⊢
((A ∈ ℂ ∧
A # 0 ∧
-𝑀 ∈ ℤ) → (A↑-𝑀) # 0) |
12 | 1, 9, 10, 11 | syl3anc 1134 |
. . 3
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (A↑-𝑀) # 0) |
13 | 4, 8, 12 | divrecap2d 7551 |
. 2
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → ((A↑𝑁) / (A↑-𝑀)) = ((1 / (A↑-𝑀)) · (A↑𝑁))) |
14 | | simp2l 929 |
. . . . . . . . . . 11
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈
ℝ) |
15 | 14 | recnd 6851 |
. . . . . . . . . 10
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈
ℂ) |
16 | 15 | negnegd 7109 |
. . . . . . . . 9
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → --𝑀 = 𝑀) |
17 | | nnnegz 8024 |
. . . . . . . . . 10
⊢ (-𝑀 ∈ ℕ → --𝑀 ∈
ℤ) |
18 | 5, 17 | syl 14 |
. . . . . . . . 9
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → --𝑀 ∈
ℤ) |
19 | 16, 18 | eqeltrrd 2112 |
. . . . . . . 8
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈
ℤ) |
20 | 2 | nn0zd 8134 |
. . . . . . . 8
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈
ℤ) |
21 | 19, 20 | zaddcld 8140 |
. . . . . . 7
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (𝑀 + 𝑁) ∈
ℤ) |
22 | | expclzap 8934 |
. . . . . . 7
⊢
((A ∈ ℂ ∧
A # 0 ∧
(𝑀 + 𝑁) ∈
ℤ) → (A↑(𝑀 + 𝑁)) ∈
ℂ) |
23 | 1, 9, 21, 22 | syl3anc 1134 |
. . . . . 6
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (A↑(𝑀 + 𝑁)) ∈
ℂ) |
24 | 23 | adantr 261 |
. . . . 5
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ (𝑀 + 𝑁) ∈
ℕ0) → (A↑(𝑀 + 𝑁)) ∈
ℂ) |
25 | 8 | adantr 261 |
. . . . 5
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ (𝑀 + 𝑁) ∈
ℕ0) → (A↑-𝑀) ∈ ℂ) |
26 | 12 | adantr 261 |
. . . . 5
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ (𝑀 + 𝑁) ∈
ℕ0) → (A↑-𝑀) # 0) |
27 | 24, 25, 26 | divcanap4d 7553 |
. . . 4
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ (𝑀 + 𝑁) ∈
ℕ0) → (((A↑(𝑀 + 𝑁)) · (A↑-𝑀)) / (A↑-𝑀)) = (A↑(𝑀 + 𝑁))) |
28 | 1 | adantr 261 |
. . . . . . 7
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ (𝑀 + 𝑁) ∈
ℕ0) → A ∈ ℂ) |
29 | | simpr 103 |
. . . . . . 7
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ (𝑀 + 𝑁) ∈
ℕ0) → (𝑀 + 𝑁) ∈
ℕ0) |
30 | 6 | adantr 261 |
. . . . . . 7
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ (𝑀 + 𝑁) ∈
ℕ0) → -𝑀 ∈
ℕ0) |
31 | | expadd 8951 |
. . . . . . 7
⊢
((A ∈ ℂ ∧ (𝑀 + 𝑁) ∈
ℕ0 ∧ -𝑀 ∈
ℕ0) → (A↑((𝑀 + 𝑁) + -𝑀)) = ((A↑(𝑀 + 𝑁)) · (A↑-𝑀))) |
32 | 28, 29, 30, 31 | syl3anc 1134 |
. . . . . 6
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ (𝑀 + 𝑁) ∈
ℕ0) → (A↑((𝑀 + 𝑁) + -𝑀)) = ((A↑(𝑀 + 𝑁)) · (A↑-𝑀))) |
33 | 21 | zcnd 8137 |
. . . . . . . . . 10
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (𝑀 + 𝑁) ∈
ℂ) |
34 | 33, 15 | negsubd 7124 |
. . . . . . . . 9
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → ((𝑀 + 𝑁) + -𝑀) = ((𝑀 + 𝑁) − 𝑀)) |
35 | 2 | nn0cnd 8013 |
. . . . . . . . . 10
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈
ℂ) |
36 | 15, 35 | pncan2d 7120 |
. . . . . . . . 9
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → ((𝑀 + 𝑁) − 𝑀) = 𝑁) |
37 | 34, 36 | eqtrd 2069 |
. . . . . . . 8
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → ((𝑀 + 𝑁) + -𝑀) = 𝑁) |
38 | 37 | adantr 261 |
. . . . . . 7
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ (𝑀 + 𝑁) ∈
ℕ0) → ((𝑀 + 𝑁) + -𝑀) = 𝑁) |
39 | 38 | oveq2d 5471 |
. . . . . 6
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ (𝑀 + 𝑁) ∈
ℕ0) → (A↑((𝑀 + 𝑁) + -𝑀)) = (A↑𝑁)) |
40 | 32, 39 | eqtr3d 2071 |
. . . . 5
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ (𝑀 + 𝑁) ∈
ℕ0) → ((A↑(𝑀 + 𝑁)) · (A↑-𝑀)) = (A↑𝑁)) |
41 | 40 | oveq1d 5470 |
. . . 4
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ (𝑀 + 𝑁) ∈
ℕ0) → (((A↑(𝑀 + 𝑁)) · (A↑-𝑀)) / (A↑-𝑀)) = ((A↑𝑁) / (A↑-𝑀))) |
42 | 27, 41 | eqtr3d 2071 |
. . 3
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ (𝑀 + 𝑁) ∈
ℕ0) → (A↑(𝑀 + 𝑁)) = ((A↑𝑁) / (A↑-𝑀))) |
43 | 1 | adantr 261 |
. . . . 5
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ -(𝑀 + 𝑁) ∈
ℕ0) → A ∈ ℂ) |
44 | 9 | adantr 261 |
. . . . 5
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ -(𝑀 + 𝑁) ∈
ℕ0) → A #
0) |
45 | 33 | adantr 261 |
. . . . 5
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ -(𝑀 + 𝑁) ∈
ℕ0) → (𝑀 + 𝑁) ∈
ℂ) |
46 | | simpr 103 |
. . . . 5
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ -(𝑀 + 𝑁) ∈
ℕ0) → -(𝑀 + 𝑁) ∈
ℕ0) |
47 | | expineg2 8918 |
. . . . 5
⊢
(((A ∈ ℂ ∧
A # 0) ∧
((𝑀 + 𝑁) ∈
ℂ ∧ -(𝑀 + 𝑁) ∈
ℕ0)) → (A↑(𝑀 + 𝑁)) = (1 / (A↑-(𝑀 + 𝑁)))) |
48 | 43, 44, 45, 46, 47 | syl22anc 1135 |
. . . 4
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ -(𝑀 + 𝑁) ∈
ℕ0) → (A↑(𝑀 + 𝑁)) = (1 / (A↑-(𝑀 + 𝑁)))) |
49 | 21 | znegcld 8138 |
. . . . . . . . . 10
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → -(𝑀 + 𝑁) ∈
ℤ) |
50 | | expclzap 8934 |
. . . . . . . . . 10
⊢
((A ∈ ℂ ∧
A # 0 ∧
-(𝑀 + 𝑁) ∈
ℤ) → (A↑-(𝑀 + 𝑁)) ∈
ℂ) |
51 | 1, 9, 49, 50 | syl3anc 1134 |
. . . . . . . . 9
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (A↑-(𝑀 + 𝑁)) ∈
ℂ) |
52 | 51 | adantr 261 |
. . . . . . . 8
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ -(𝑀 + 𝑁) ∈
ℕ0) → (A↑-(𝑀 + 𝑁)) ∈
ℂ) |
53 | 4 | adantr 261 |
. . . . . . . 8
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ -(𝑀 + 𝑁) ∈
ℕ0) → (A↑𝑁) ∈ ℂ) |
54 | | expap0i 8941 |
. . . . . . . . . 10
⊢
((A ∈ ℂ ∧
A # 0 ∧
𝑁 ∈ ℤ) → (A↑𝑁) # 0) |
55 | 1, 9, 20, 54 | syl3anc 1134 |
. . . . . . . . 9
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (A↑𝑁) # 0) |
56 | 55 | adantr 261 |
. . . . . . . 8
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ -(𝑀 + 𝑁) ∈
ℕ0) → (A↑𝑁) # 0) |
57 | 52, 53, 56 | divcanap4d 7553 |
. . . . . . 7
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ -(𝑀 + 𝑁) ∈
ℕ0) → (((A↑-(𝑀 + 𝑁)) · (A↑𝑁)) / (A↑𝑁)) = (A↑-(𝑀 + 𝑁))) |
58 | 2 | adantr 261 |
. . . . . . . . . 10
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ -(𝑀 + 𝑁) ∈
ℕ0) → 𝑁 ∈
ℕ0) |
59 | | expadd 8951 |
. . . . . . . . . 10
⊢
((A ∈ ℂ ∧
-(𝑀 + 𝑁) ∈
ℕ0 ∧ 𝑁 ∈
ℕ0) → (A↑(-(𝑀 + 𝑁) + 𝑁)) = ((A↑-(𝑀 + 𝑁)) · (A↑𝑁))) |
60 | 43, 46, 58, 59 | syl3anc 1134 |
. . . . . . . . 9
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ -(𝑀 + 𝑁) ∈
ℕ0) → (A↑(-(𝑀 + 𝑁) + 𝑁)) = ((A↑-(𝑀 + 𝑁)) · (A↑𝑁))) |
61 | 15, 35 | negdi2d 7132 |
. . . . . . . . . . . . 13
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → -(𝑀 + 𝑁) = (-𝑀 − 𝑁)) |
62 | 61 | oveq1d 5470 |
. . . . . . . . . . . 12
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (-(𝑀 + 𝑁) + 𝑁) = ((-𝑀 − 𝑁) + 𝑁)) |
63 | 15 | negcld 7105 |
. . . . . . . . . . . . 13
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → -𝑀 ∈
ℂ) |
64 | 63, 35 | npcand 7122 |
. . . . . . . . . . . 12
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → ((-𝑀 − 𝑁) + 𝑁) = -𝑀) |
65 | 62, 64 | eqtrd 2069 |
. . . . . . . . . . 11
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (-(𝑀 + 𝑁) + 𝑁) = -𝑀) |
66 | 65 | adantr 261 |
. . . . . . . . . 10
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ -(𝑀 + 𝑁) ∈
ℕ0) → (-(𝑀 + 𝑁) + 𝑁) = -𝑀) |
67 | 66 | oveq2d 5471 |
. . . . . . . . 9
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ -(𝑀 + 𝑁) ∈
ℕ0) → (A↑(-(𝑀 + 𝑁) + 𝑁)) = (A↑-𝑀)) |
68 | 60, 67 | eqtr3d 2071 |
. . . . . . . 8
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ -(𝑀 + 𝑁) ∈
ℕ0) → ((A↑-(𝑀 + 𝑁)) · (A↑𝑁)) = (A↑-𝑀)) |
69 | 68 | oveq1d 5470 |
. . . . . . 7
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ -(𝑀 + 𝑁) ∈
ℕ0) → (((A↑-(𝑀 + 𝑁)) · (A↑𝑁)) / (A↑𝑁)) = ((A↑-𝑀) / (A↑𝑁))) |
70 | 57, 69 | eqtr3d 2071 |
. . . . . 6
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ -(𝑀 + 𝑁) ∈
ℕ0) → (A↑-(𝑀 + 𝑁)) = ((A↑-𝑀) / (A↑𝑁))) |
71 | 70 | oveq2d 5471 |
. . . . 5
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ -(𝑀 + 𝑁) ∈
ℕ0) → (1 / (A↑-(𝑀 + 𝑁))) = (1 / ((A↑-𝑀) / (A↑𝑁)))) |
72 | 8, 4, 12, 55 | recdivapd 7564 |
. . . . . 6
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (1 / ((A↑-𝑀) / (A↑𝑁))) = ((A↑𝑁) / (A↑-𝑀))) |
73 | 72 | adantr 261 |
. . . . 5
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ -(𝑀 + 𝑁) ∈
ℕ0) → (1 / ((A↑-𝑀) / (A↑𝑁))) = ((A↑𝑁) / (A↑-𝑀))) |
74 | 71, 73 | eqtrd 2069 |
. . . 4
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ -(𝑀 + 𝑁) ∈
ℕ0) → (1 / (A↑-(𝑀 + 𝑁))) = ((A↑𝑁) / (A↑-𝑀))) |
75 | 48, 74 | eqtrd 2069 |
. . 3
⊢
((((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) ∧ -(𝑀 + 𝑁) ∈
ℕ0) → (A↑(𝑀 + 𝑁)) = ((A↑𝑁) / (A↑-𝑀))) |
76 | | elznn0 8036 |
. . . . 5
⊢ ((𝑀 + 𝑁) ∈
ℤ ↔ ((𝑀 + 𝑁) ∈ ℝ ∧
((𝑀 + 𝑁) ∈
ℕ0 ∨ -(𝑀 + 𝑁) ∈
ℕ0))) |
77 | 76 | simprbi 260 |
. . . 4
⊢ ((𝑀 + 𝑁) ∈
ℤ → ((𝑀 + 𝑁) ∈ ℕ0
∨ -(𝑀 + 𝑁) ∈ ℕ0)) |
78 | 21, 77 | syl 14 |
. . 3
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → ((𝑀 + 𝑁) ∈
ℕ0 ∨ -(𝑀 + 𝑁) ∈
ℕ0)) |
79 | 42, 75, 78 | mpjaodan 710 |
. 2
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (A↑(𝑀 + 𝑁)) = ((A↑𝑁) / (A↑-𝑀))) |
80 | | expineg2 8918 |
. . . 4
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℂ ∧ -𝑀 ∈ ℕ0)) → (A↑𝑀) = (1 / (A↑-𝑀))) |
81 | 1, 9, 15, 6, 80 | syl22anc 1135 |
. . 3
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (A↑𝑀) = (1 / (A↑-𝑀))) |
82 | 81 | oveq1d 5470 |
. 2
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → ((A↑𝑀) · (A↑𝑁)) = ((1 / (A↑-𝑀)) · (A↑𝑁))) |
83 | 13, 79, 82 | 3eqtr4d 2079 |
1
⊢
(((A ∈ ℂ ∧
A # 0) ∧
(𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (A↑(𝑀 + 𝑁)) = ((A↑𝑀) · (A↑𝑁))) |