Proof of Theorem expnegap0
Step | Hyp | Ref
| Expression |
1 | | elnn0 8183 |
. . 3
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
2 | | nnne0 7942 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
3 | 2 | adantl 262 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → 𝑁 ≠ 0) |
4 | | nncn 7922 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
5 | 4 | adantl 262 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℂ) |
6 | 5 | negeq0d 7314 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝑁 = 0 ↔ -𝑁 = 0)) |
7 | 6 | necon3abid 2244 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝑁 ≠ 0 ↔ ¬ -𝑁 = 0)) |
8 | 3, 7 | mpbid 135 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ¬
-𝑁 = 0) |
9 | 8 | iffalsed 3341 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) →
if(-𝑁 = 0, 1, if(0 <
-𝑁, (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘-𝑁), (1 /
(seq1( · , (ℕ × {𝐴}), ℂ)‘--𝑁)))) = if(0 < -𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁), (1 / (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘--𝑁)))) |
10 | | nnnn0 8188 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
11 | 10 | adantl 262 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℕ0) |
12 | | nn0nlt0 8208 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ ¬ 𝑁 <
0) |
13 | 11, 12 | syl 14 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ¬
𝑁 < 0) |
14 | 11 | nn0red 8236 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ) |
15 | 14 | lt0neg1d 7507 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝑁 < 0 ↔ 0 < -𝑁)) |
16 | 13, 15 | mtbid 597 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ¬ 0
< -𝑁) |
17 | 16 | iffalsed 3341 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → if(0
< -𝑁, (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘-𝑁), (1 /
(seq1( · , (ℕ × {𝐴}), ℂ)‘--𝑁))) = (1 / (seq1( · , (ℕ
× {𝐴}),
ℂ)‘--𝑁))) |
18 | 5 | negnegd 7313 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → --𝑁 = 𝑁) |
19 | 18 | fveq2d 5182 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (seq1(
· , (ℕ × {𝐴}), ℂ)‘--𝑁) = (seq1( · , (ℕ ×
{𝐴}), ℂ)‘𝑁)) |
20 | 19 | oveq2d 5528 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (1 /
(seq1( · , (ℕ × {𝐴}), ℂ)‘--𝑁)) = (1 / (seq1( · , (ℕ ×
{𝐴}), ℂ)‘𝑁))) |
21 | 9, 17, 20 | 3eqtrd 2076 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) →
if(-𝑁 = 0, 1, if(0 <
-𝑁, (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘-𝑁), (1 /
(seq1( · , (ℕ × {𝐴}), ℂ)‘--𝑁)))) = (1 / (seq1( · , (ℕ
× {𝐴}),
ℂ)‘𝑁))) |
22 | 21 | adantlr 446 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ 𝑁 ∈ ℕ) → if(-𝑁 = 0, 1, if(0 < -𝑁, (seq1( · , (ℕ
× {𝐴}),
ℂ)‘-𝑁), (1 /
(seq1( · , (ℕ × {𝐴}), ℂ)‘--𝑁)))) = (1 / (seq1( · , (ℕ
× {𝐴}),
ℂ)‘𝑁))) |
23 | | simp1 904 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℕ) → 𝐴 ∈ ℂ) |
24 | | simp3 906 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ) |
25 | 24 | nnzd 8359 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℤ) |
26 | 25 | znegcld 8362 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℕ) → -𝑁 ∈ ℤ) |
27 | | simp2 905 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℕ) → 𝐴 # 0) |
28 | 27 | orcd 652 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℕ) → (𝐴 # 0 ∨ 0 ≤ -𝑁)) |
29 | | expival 9257 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ -𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ -𝑁)) → (𝐴↑-𝑁) = if(-𝑁 = 0, 1, if(0 < -𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁), (1 / (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘--𝑁))))) |
30 | 23, 26, 28, 29 | syl3anc 1135 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℕ) → (𝐴↑-𝑁) = if(-𝑁 = 0, 1, if(0 < -𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁), (1 / (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘--𝑁))))) |
31 | 30 | 3expa 1104 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ 𝑁 ∈ ℕ) → (𝐴↑-𝑁) = if(-𝑁 = 0, 1, if(0 < -𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁), (1 / (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘--𝑁))))) |
32 | | expinnval 9258 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) = (seq1( · , (ℕ ×
{𝐴}), ℂ)‘𝑁)) |
33 | 32 | oveq2d 5528 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (1 /
(𝐴↑𝑁)) = (1 / (seq1( · , (ℕ ×
{𝐴}), ℂ)‘𝑁))) |
34 | 33 | adantlr 446 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ 𝑁 ∈ ℕ) → (1 / (𝐴↑𝑁)) = (1 / (seq1( · , (ℕ ×
{𝐴}), ℂ)‘𝑁))) |
35 | 22, 31, 34 | 3eqtr4d 2082 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ 𝑁 ∈ ℕ) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) |
36 | | 1div1e1 7681 |
. . . . . . 7
⊢ (1 / 1) =
1 |
37 | 36 | eqcomi 2044 |
. . . . . 6
⊢ 1 = (1 /
1) |
38 | | negeq 7204 |
. . . . . . . . 9
⊢ (𝑁 = 0 → -𝑁 = -0) |
39 | | neg0 7257 |
. . . . . . . . 9
⊢ -0 =
0 |
40 | 38, 39 | syl6eq 2088 |
. . . . . . . 8
⊢ (𝑁 = 0 → -𝑁 = 0) |
41 | 40 | oveq2d 5528 |
. . . . . . 7
⊢ (𝑁 = 0 → (𝐴↑-𝑁) = (𝐴↑0)) |
42 | | exp0 9259 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) |
43 | 41, 42 | sylan9eqr 2094 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 = 0) → (𝐴↑-𝑁) = 1) |
44 | | oveq2 5520 |
. . . . . . . 8
⊢ (𝑁 = 0 → (𝐴↑𝑁) = (𝐴↑0)) |
45 | 44, 42 | sylan9eqr 2094 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 = 0) → (𝐴↑𝑁) = 1) |
46 | 45 | oveq2d 5528 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 = 0) → (1 / (𝐴↑𝑁)) = (1 / 1)) |
47 | 37, 43, 46 | 3eqtr4a 2098 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 = 0) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) |
48 | 47 | adantlr 446 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ 𝑁 = 0) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) |
49 | 35, 48 | jaodan 710 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℕ ∨ 𝑁 = 0)) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) |
50 | 1, 49 | sylan2b 271 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ 𝑁 ∈ ℕ0) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) |
51 | 50 | 3impa 1099 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℕ0) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) |