Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
⊢
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀)) = (ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀)) |
2 | | 0z 11388 |
. . . 4
⊢ 0 ∈
ℤ |
3 | | explecnv.3 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
4 | | ifcl 4130 |
. . . 4
⊢ ((0
∈ ℤ ∧ 𝑀
∈ ℤ) → if(𝑀
≤ 0, 0, 𝑀) ∈
ℤ) |
5 | 2, 3, 4 | sylancr 695 |
. . 3
⊢ (𝜑 → if(𝑀 ≤ 0, 0, 𝑀) ∈ ℤ) |
6 | | explecnv.5 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) |
7 | 6 | recnd 10068 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℂ) |
8 | | explecnv.4 |
. . . 4
⊢ (𝜑 → (abs‘𝐴) < 1) |
9 | 7, 8 | expcnv 14596 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) ⇝ 0) |
10 | | explecnv.1 |
. . . . . 6
⊢ 𝑍 =
(ℤ≥‘𝑀) |
11 | | fvex 6201 |
. . . . . 6
⊢
(ℤ≥‘𝑀) ∈ V |
12 | 10, 11 | eqeltri 2697 |
. . . . 5
⊢ 𝑍 ∈ V |
13 | 12 | mptex 6486 |
. . . 4
⊢ (𝑛 ∈ 𝑍 ↦ (abs‘(𝐹‘𝑛))) ∈ V |
14 | 13 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ (abs‘(𝐹‘𝑛))) ∈ V) |
15 | | nn0uz 11722 |
. . . . . . . . . . 11
⊢
ℕ0 = (ℤ≥‘0) |
16 | 10, 15 | ineq12i 3812 |
. . . . . . . . . 10
⊢ (𝑍 ∩ ℕ0) =
((ℤ≥‘𝑀) ∩
(ℤ≥‘0)) |
17 | | uzin 11720 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 0 ∈
ℤ) → ((ℤ≥‘𝑀) ∩ (ℤ≥‘0)) =
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀))) |
18 | 3, 2, 17 | sylancl 694 |
. . . . . . . . . 10
⊢ (𝜑 →
((ℤ≥‘𝑀) ∩ (ℤ≥‘0)) =
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀))) |
19 | 16, 18 | syl5req 2669 |
. . . . . . . . 9
⊢ (𝜑 →
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀)) = (𝑍 ∩
ℕ0)) |
20 | 19 | eleq2d 2687 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀)) ↔ 𝑘 ∈ (𝑍 ∩
ℕ0))) |
21 | 20 | biimpa 501 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀))) → 𝑘 ∈ (𝑍 ∩
ℕ0)) |
22 | | elin 3796 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑍 ∩ ℕ0) ↔ (𝑘 ∈ 𝑍 ∧ 𝑘 ∈
ℕ0)) |
23 | 21, 22 | sylib 208 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀))) → (𝑘 ∈ 𝑍 ∧ 𝑘 ∈
ℕ0)) |
24 | 23 | simprd 479 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀))) → 𝑘 ∈ ℕ0) |
25 | | oveq2 6658 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (𝐴↑𝑛) = (𝐴↑𝑘)) |
26 | | eqid 2622 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
↦ (𝐴↑𝑛)) = (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) |
27 | | ovex 6678 |
. . . . . 6
⊢ (𝐴↑𝑘) ∈ V |
28 | 25, 26, 27 | fvmpt 6282 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ (𝐴↑𝑛))‘𝑘) = (𝐴↑𝑘)) |
29 | 24, 28 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀))) → ((𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛))‘𝑘) = (𝐴↑𝑘)) |
30 | 6 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀))) → 𝐴 ∈ ℝ) |
31 | 30, 24 | reexpcld 13025 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀))) → (𝐴↑𝑘) ∈ ℝ) |
32 | 29, 31 | eqeltrd 2701 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀))) → ((𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛))‘𝑘) ∈ ℝ) |
33 | 23 | simpld 475 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀))) → 𝑘 ∈ 𝑍) |
34 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) |
35 | 34 | fveq2d 6195 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (abs‘(𝐹‘𝑛)) = (abs‘(𝐹‘𝑘))) |
36 | | eqid 2622 |
. . . . . 6
⊢ (𝑛 ∈ 𝑍 ↦ (abs‘(𝐹‘𝑛))) = (𝑛 ∈ 𝑍 ↦ (abs‘(𝐹‘𝑛))) |
37 | | fvex 6201 |
. . . . . 6
⊢
(abs‘(𝐹‘𝑘)) ∈ V |
38 | 35, 36, 37 | fvmpt 6282 |
. . . . 5
⊢ (𝑘 ∈ 𝑍 → ((𝑛 ∈ 𝑍 ↦ (abs‘(𝐹‘𝑛)))‘𝑘) = (abs‘(𝐹‘𝑘))) |
39 | 33, 38 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀))) → ((𝑛 ∈ 𝑍 ↦ (abs‘(𝐹‘𝑛)))‘𝑘) = (abs‘(𝐹‘𝑘))) |
40 | | explecnv.6 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
41 | 33, 40 | syldan 487 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀))) → (𝐹‘𝑘) ∈ ℂ) |
42 | 41 | abscld 14175 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀))) → (abs‘(𝐹‘𝑘)) ∈ ℝ) |
43 | 39, 42 | eqeltrd 2701 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀))) → ((𝑛 ∈ 𝑍 ↦ (abs‘(𝐹‘𝑛)))‘𝑘) ∈ ℝ) |
44 | | explecnv.7 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (abs‘(𝐹‘𝑘)) ≤ (𝐴↑𝑘)) |
45 | 33, 44 | syldan 487 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀))) → (abs‘(𝐹‘𝑘)) ≤ (𝐴↑𝑘)) |
46 | 45, 39, 29 | 3brtr4d 4685 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀))) → ((𝑛 ∈ 𝑍 ↦ (abs‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛))‘𝑘)) |
47 | 41 | absge0d 14183 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀))) → 0 ≤ (abs‘(𝐹‘𝑘))) |
48 | 47, 39 | breqtrrd 4681 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ 0, 0, 𝑀))) → 0 ≤ ((𝑛 ∈ 𝑍 ↦ (abs‘(𝐹‘𝑛)))‘𝑘)) |
49 | 1, 5, 9, 14, 32, 43, 46, 48 | climsqz2 14372 |
. 2
⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ (abs‘(𝐹‘𝑛))) ⇝ 0) |
50 | | explecnv.2 |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
51 | 38 | adantl 482 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑛 ∈ 𝑍 ↦ (abs‘(𝐹‘𝑛)))‘𝑘) = (abs‘(𝐹‘𝑘))) |
52 | 10, 3, 50, 14, 40, 51 | climabs0 14316 |
. 2
⊢ (𝜑 → (𝐹 ⇝ 0 ↔ (𝑛 ∈ 𝑍 ↦ (abs‘(𝐹‘𝑛))) ⇝ 0)) |
53 | 49, 52 | mpbird 247 |
1
⊢ (𝜑 → 𝐹 ⇝ 0) |