Proof of Theorem expnegap0
Step | Hyp | Ref
| Expression |
1 | | elnn0 9124 |
. . 3
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
2 | | nnne0 8893 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
3 | 2 | adantl 275 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → 𝑁 ≠ 0) |
4 | | nncn 8873 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
5 | 4 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℂ) |
6 | 5 | negeq0d 8209 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝑁 = 0 ↔ -𝑁 = 0)) |
7 | 6 | necon3abid 2379 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝑁 ≠ 0 ↔ ¬ -𝑁 = 0)) |
8 | 3, 7 | mpbid 146 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ¬
-𝑁 = 0) |
9 | 8 | iffalsed 3535 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) →
if(-𝑁 = 0, 1, if(0 <
-𝑁, (seq1( · ,
(ℕ × {𝐴}))‘-𝑁), (1 / (seq1( · , (ℕ ×
{𝐴}))‘--𝑁)))) = if(0 < -𝑁, (seq1( · , (ℕ
× {𝐴}))‘-𝑁), (1 / (seq1( · ,
(ℕ × {𝐴}))‘--𝑁)))) |
10 | | nnnn0 9129 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
11 | 10 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℕ0) |
12 | | nn0nlt0 9148 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ ¬ 𝑁 <
0) |
13 | 11, 12 | syl 14 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ¬
𝑁 < 0) |
14 | 11 | nn0red 9176 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ) |
15 | 14 | lt0neg1d 8421 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝑁 < 0 ↔ 0 < -𝑁)) |
16 | 13, 15 | mtbid 667 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ¬ 0
< -𝑁) |
17 | 16 | iffalsed 3535 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → if(0
< -𝑁, (seq1( · ,
(ℕ × {𝐴}))‘-𝑁), (1 / (seq1( · , (ℕ ×
{𝐴}))‘--𝑁))) = (1 / (seq1( · ,
(ℕ × {𝐴}))‘--𝑁))) |
18 | 5 | negnegd 8208 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → --𝑁 = 𝑁) |
19 | 18 | fveq2d 5498 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (seq1(
· , (ℕ × {𝐴}))‘--𝑁) = (seq1( · , (ℕ ×
{𝐴}))‘𝑁)) |
20 | 19 | oveq2d 5866 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (1 /
(seq1( · , (ℕ × {𝐴}))‘--𝑁)) = (1 / (seq1( · , (ℕ ×
{𝐴}))‘𝑁))) |
21 | 9, 17, 20 | 3eqtrd 2207 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) →
if(-𝑁 = 0, 1, if(0 <
-𝑁, (seq1( · ,
(ℕ × {𝐴}))‘-𝑁), (1 / (seq1( · , (ℕ ×
{𝐴}))‘--𝑁)))) = (1 / (seq1( · ,
(ℕ × {𝐴}))‘𝑁))) |
22 | 21 | adantlr 474 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ 𝑁 ∈ ℕ) → if(-𝑁 = 0, 1, if(0 < -𝑁, (seq1( · , (ℕ
× {𝐴}))‘-𝑁), (1 / (seq1( · ,
(ℕ × {𝐴}))‘--𝑁)))) = (1 / (seq1( · , (ℕ
× {𝐴}))‘𝑁))) |
23 | | simp1 992 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℕ) → 𝐴 ∈ ℂ) |
24 | | simp3 994 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ) |
25 | 24 | nnzd 9320 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℤ) |
26 | 25 | znegcld 9323 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℕ) → -𝑁 ∈ ℤ) |
27 | | simp2 993 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℕ) → 𝐴 # 0) |
28 | 27 | orcd 728 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℕ) → (𝐴 # 0 ∨ 0 ≤ -𝑁)) |
29 | | exp3val 10465 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ -𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ -𝑁)) → (𝐴↑-𝑁) = if(-𝑁 = 0, 1, if(0 < -𝑁, (seq1( · , (ℕ × {𝐴}))‘-𝑁), (1 / (seq1( · , (ℕ ×
{𝐴}))‘--𝑁))))) |
30 | 23, 26, 28, 29 | syl3anc 1233 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℕ) → (𝐴↑-𝑁) = if(-𝑁 = 0, 1, if(0 < -𝑁, (seq1( · , (ℕ × {𝐴}))‘-𝑁), (1 / (seq1( · , (ℕ ×
{𝐴}))‘--𝑁))))) |
31 | 30 | 3expa 1198 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ 𝑁 ∈ ℕ) → (𝐴↑-𝑁) = if(-𝑁 = 0, 1, if(0 < -𝑁, (seq1( · , (ℕ × {𝐴}))‘-𝑁), (1 / (seq1( · , (ℕ ×
{𝐴}))‘--𝑁))))) |
32 | | expnnval 10466 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) = (seq1( · , (ℕ ×
{𝐴}))‘𝑁)) |
33 | 32 | oveq2d 5866 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (1 /
(𝐴↑𝑁)) = (1 / (seq1( · , (ℕ ×
{𝐴}))‘𝑁))) |
34 | 33 | adantlr 474 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ 𝑁 ∈ ℕ) → (1 / (𝐴↑𝑁)) = (1 / (seq1( · , (ℕ ×
{𝐴}))‘𝑁))) |
35 | 22, 31, 34 | 3eqtr4d 2213 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ 𝑁 ∈ ℕ) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) |
36 | | 1div1e1 8608 |
. . . . . . 7
⊢ (1 / 1) =
1 |
37 | 36 | eqcomi 2174 |
. . . . . 6
⊢ 1 = (1 /
1) |
38 | | negeq 8099 |
. . . . . . . . 9
⊢ (𝑁 = 0 → -𝑁 = -0) |
39 | | neg0 8152 |
. . . . . . . . 9
⊢ -0 =
0 |
40 | 38, 39 | eqtrdi 2219 |
. . . . . . . 8
⊢ (𝑁 = 0 → -𝑁 = 0) |
41 | 40 | oveq2d 5866 |
. . . . . . 7
⊢ (𝑁 = 0 → (𝐴↑-𝑁) = (𝐴↑0)) |
42 | | exp0 10467 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) |
43 | 41, 42 | sylan9eqr 2225 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 = 0) → (𝐴↑-𝑁) = 1) |
44 | | oveq2 5858 |
. . . . . . . 8
⊢ (𝑁 = 0 → (𝐴↑𝑁) = (𝐴↑0)) |
45 | 44, 42 | sylan9eqr 2225 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 = 0) → (𝐴↑𝑁) = 1) |
46 | 45 | oveq2d 5866 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 = 0) → (1 / (𝐴↑𝑁)) = (1 / 1)) |
47 | 37, 43, 46 | 3eqtr4a 2229 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 = 0) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) |
48 | 47 | adantlr 474 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ 𝑁 = 0) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) |
49 | 35, 48 | jaodan 792 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℕ ∨ 𝑁 = 0)) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) |
50 | 1, 49 | sylan2b 285 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ 𝑁 ∈ ℕ0) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) |
51 | 50 | 3impa 1189 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℕ0) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) |