Step | Hyp | Ref
| Expression |
1 | | nfv 1921 |
. . . . . 6
⊢
Ⅎ𝑘(𝜑 ∧ 𝑖 ∈ 𝑍) |
2 | | nfra1 3145 |
. . . . . 6
⊢
Ⅎ𝑘∀𝑘 ∈ (ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1) |
3 | 1, 2 | nfan 1906 |
. . . . 5
⊢
Ⅎ𝑘((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1)) |
4 | | climrescn.z |
. . . . . . . . . 10
⊢ 𝑍 =
(ℤ≥‘𝑀) |
5 | 4 | uztrn2 12600 |
. . . . . . . . 9
⊢ ((𝑖 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → 𝑘 ∈ 𝑍) |
6 | 5 | adantll 711 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → 𝑘 ∈ 𝑍) |
7 | | climrescn.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 Fn 𝑍) |
8 | 7 | fndmd 6536 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = 𝑍) |
9 | 8 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → dom 𝐹 = 𝑍) |
10 | 6, 9 | eleqtrrd 2844 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → 𝑘 ∈ dom 𝐹) |
11 | 10 | adantlr 712 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1)) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → 𝑘 ∈ dom 𝐹) |
12 | | rspa 3133 |
. . . . . . . . 9
⊢
((∀𝑘 ∈
(ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → ((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1)) |
13 | 12 | adantll 711 |
. . . . . . . 8
⊢ (((𝑖 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1)) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → ((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1)) |
14 | 13 | simpld 495 |
. . . . . . 7
⊢ (((𝑖 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1)) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (𝐹‘𝑘) ∈ ℂ) |
15 | 14 | adantlll 715 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1)) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (𝐹‘𝑘) ∈ ℂ) |
16 | 11, 15 | jca 512 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1)) ∧ 𝑘 ∈ (ℤ≥‘𝑖)) → (𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ ℂ)) |
17 | 3, 16 | ralrimia 3429 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1)) → ∀𝑘 ∈
(ℤ≥‘𝑖)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ ℂ)) |
18 | | fnfun 6531 |
. . . . . 6
⊢ (𝐹 Fn 𝑍 → Fun 𝐹) |
19 | | ffvresb 6995 |
. . . . . 6
⊢ (Fun
𝐹 → ((𝐹 ↾
(ℤ≥‘𝑖)):(ℤ≥‘𝑖)⟶ℂ ↔
∀𝑘 ∈
(ℤ≥‘𝑖)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ ℂ))) |
20 | 7, 18, 19 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ((𝐹 ↾ (ℤ≥‘𝑖)):(ℤ≥‘𝑖)⟶ℂ ↔
∀𝑘 ∈
(ℤ≥‘𝑖)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ ℂ))) |
21 | 20 | ad2antrr 723 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1)) → ((𝐹 ↾ (ℤ≥‘𝑖)):(ℤ≥‘𝑖)⟶ℂ ↔
∀𝑘 ∈
(ℤ≥‘𝑖)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ ℂ))) |
22 | 17, 21 | mpbird 256 |
. . 3
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1)) → (𝐹 ↾ (ℤ≥‘𝑖)):(ℤ≥‘𝑖)⟶ℂ) |
23 | | breq2 5083 |
. . . . . . 7
⊢ (𝑥 = 1 → ((abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 𝑥 ↔ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1)) |
24 | 23 | anbi2d 629 |
. . . . . 6
⊢ (𝑥 = 1 → (((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 𝑥) ↔ ((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1))) |
25 | 24 | rexralbidv 3232 |
. . . . 5
⊢ (𝑥 = 1 → (∃𝑖 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 𝑥) ↔ ∃𝑖 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1))) |
26 | | climrescn.c |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ dom ⇝ ) |
27 | | climdm 15261 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘𝐹)) |
28 | 26, 27 | sylib 217 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ⇝ ( ⇝ ‘𝐹)) |
29 | | eqidd 2741 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
30 | 26, 29 | clim 15201 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ⇝ ( ⇝ ‘𝐹) ↔ (( ⇝ ‘𝐹) ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑖 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 𝑥)))) |
31 | 28, 30 | mpbid 231 |
. . . . . 6
⊢ (𝜑 → (( ⇝ ‘𝐹) ∈ ℂ ∧
∀𝑥 ∈
ℝ+ ∃𝑖 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 𝑥))) |
32 | 31 | simprd 496 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑖 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 𝑥)) |
33 | | 1rp 12733 |
. . . . . 6
⊢ 1 ∈
ℝ+ |
34 | 33 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℝ+) |
35 | 25, 32, 34 | rspcdva 3563 |
. . . 4
⊢ (𝜑 → ∃𝑖 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1)) |
36 | | climrescn.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
37 | 4 | rexuz3 15058 |
. . . . 5
⊢ (𝑀 ∈ ℤ →
(∃𝑖 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1) ↔ ∃𝑖 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1))) |
38 | 36, 37 | syl 17 |
. . . 4
⊢ (𝜑 → (∃𝑖 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1) ↔ ∃𝑖 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1))) |
39 | 35, 38 | mpbird 256 |
. . 3
⊢ (𝜑 → ∃𝑖 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑖)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1)) |
40 | 22, 39 | reximddv3 42670 |
. 2
⊢ (𝜑 → ∃𝑖 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑖)):(ℤ≥‘𝑖)⟶ℂ) |
41 | | fveq2 6771 |
. . . . 5
⊢ (𝑗 = 𝑖 → (ℤ≥‘𝑗) =
(ℤ≥‘𝑖)) |
42 | 41 | reseq2d 5890 |
. . . 4
⊢ (𝑗 = 𝑖 → (𝐹 ↾ (ℤ≥‘𝑗)) = (𝐹 ↾ (ℤ≥‘𝑖))) |
43 | 42, 41 | feq12d 6586 |
. . 3
⊢ (𝑗 = 𝑖 → ((𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℂ ↔ (𝐹 ↾
(ℤ≥‘𝑖)):(ℤ≥‘𝑖)⟶ℂ)) |
44 | 43 | cbvrexvw 3382 |
. 2
⊢
(∃𝑗 ∈
𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℂ ↔
∃𝑖 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑖)):(ℤ≥‘𝑖)⟶ℂ) |
45 | 40, 44 | sylibr 233 |
1
⊢ (𝜑 → ∃𝑗 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℂ) |