Step | Hyp | Ref
| Expression |
1 | | climxrre.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
2 | 1 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) → 𝑀 ∈ ℤ) |
3 | | climxrre.z |
. . . 4
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | | climxrre.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) |
5 | 4 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) → 𝐹:𝑍⟶ℝ*) |
6 | | climxrre.c |
. . . . 5
⊢ (𝜑 → 𝐹 ⇝ 𝐴) |
7 | 6 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) → 𝐹 ⇝ 𝐴) |
8 | | simpr 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ +∞ ∈ ℂ)
→ +∞ ∈ ℂ) |
9 | | climxrre.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) |
10 | 9 | recnd 10890 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) |
11 | 10 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ +∞ ∈ ℂ)
→ 𝐴 ∈
ℂ) |
12 | 8, 11 | subcld 11218 |
. . . . . . 7
⊢ ((𝜑 ∧ +∞ ∈ ℂ)
→ (+∞ − 𝐴)
∈ ℂ) |
13 | | renepnf 10910 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞) |
14 | 13 | necomd 2999 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → +∞
≠ 𝐴) |
15 | 9, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → +∞ ≠ 𝐴) |
16 | 15 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ +∞ ∈ ℂ)
→ +∞ ≠ 𝐴) |
17 | 8, 11, 16 | subne0d 11227 |
. . . . . . 7
⊢ ((𝜑 ∧ +∞ ∈ ℂ)
→ (+∞ − 𝐴)
≠ 0) |
18 | 12, 17 | absrpcld 15044 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ℂ)
→ (abs‘(+∞ − 𝐴)) ∈
ℝ+) |
19 | 18 | adantr 484 |
. . . . 5
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) → (abs‘(+∞ − 𝐴)) ∈
ℝ+) |
20 | | simpr 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ -∞ ∈ ℂ)
→ -∞ ∈ ℂ) |
21 | 10 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ -∞ ∈ ℂ)
→ 𝐴 ∈
ℂ) |
22 | 20, 21 | subcld 11218 |
. . . . . . 7
⊢ ((𝜑 ∧ -∞ ∈ ℂ)
→ (-∞ − 𝐴)
∈ ℂ) |
23 | 9 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ -∞ ∈ ℂ)
→ 𝐴 ∈
ℝ) |
24 | | renemnf 10911 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞) |
25 | 24 | necomd 2999 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → -∞
≠ 𝐴) |
26 | 23, 25 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ -∞ ∈ ℂ)
→ -∞ ≠ 𝐴) |
27 | 20, 21, 26 | subne0d 11227 |
. . . . . . 7
⊢ ((𝜑 ∧ -∞ ∈ ℂ)
→ (-∞ − 𝐴)
≠ 0) |
28 | 22, 27 | absrpcld 15044 |
. . . . . 6
⊢ ((𝜑 ∧ -∞ ∈ ℂ)
→ (abs‘(-∞ − 𝐴)) ∈
ℝ+) |
29 | 28 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) → (abs‘(-∞ − 𝐴)) ∈
ℝ+) |
30 | 19, 29 | ifcld 4501 |
. . . 4
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) → if((abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞
− 𝐴)),
(abs‘(+∞ − 𝐴)), (abs‘(-∞ − 𝐴))) ∈
ℝ+) |
31 | 19 | rpred 12657 |
. . . . . 6
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) → (abs‘(+∞ − 𝐴)) ∈
ℝ) |
32 | 29 | rpred 12657 |
. . . . . 6
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) → (abs‘(-∞ − 𝐴)) ∈
ℝ) |
33 | 31, 32 | min1d 42732 |
. . . . 5
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) → if((abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞
− 𝐴)),
(abs‘(+∞ − 𝐴)), (abs‘(-∞ − 𝐴))) ≤ (abs‘(+∞
− 𝐴))) |
34 | 33 | adantr 484 |
. . . 4
⊢ ((((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) ∧ +∞ ∈ ℂ) →
if((abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴)), (abs‘(+∞ −
𝐴)), (abs‘(-∞
− 𝐴))) ≤
(abs‘(+∞ − 𝐴))) |
35 | 31, 32 | min2d 42733 |
. . . . 5
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) → if((abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞
− 𝐴)),
(abs‘(+∞ − 𝐴)), (abs‘(-∞ − 𝐴))) ≤ (abs‘(-∞
− 𝐴))) |
36 | 35 | adantr 484 |
. . . 4
⊢ ((((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) ∧ -∞ ∈ ℂ) →
if((abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴)), (abs‘(+∞ −
𝐴)), (abs‘(-∞
− 𝐴))) ≤
(abs‘(-∞ − 𝐴))) |
37 | 2, 3, 5, 7, 30, 34, 36 | climxrrelem 43010 |
. . 3
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) → ∃𝑗 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ) |
38 | 1 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ ¬ -∞ ∈ ℂ) → 𝑀 ∈ ℤ) |
39 | 4 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ ¬ -∞ ∈ ℂ) → 𝐹:𝑍⟶ℝ*) |
40 | 6 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ ¬ -∞ ∈ ℂ) → 𝐹 ⇝ 𝐴) |
41 | 18 | adantr 484 |
. . . 4
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ ¬ -∞ ∈ ℂ) → (abs‘(+∞ − 𝐴)) ∈
ℝ+) |
42 | 18 | rpred 12657 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ℂ)
→ (abs‘(+∞ − 𝐴)) ∈ ℝ) |
43 | 42 | leidd 11427 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ℂ)
→ (abs‘(+∞ − 𝐴)) ≤ (abs‘(+∞ − 𝐴))) |
44 | 43 | ad2antrr 726 |
. . . 4
⊢ ((((𝜑 ∧ +∞ ∈ ℂ)
∧ ¬ -∞ ∈ ℂ) ∧ +∞ ∈ ℂ) →
(abs‘(+∞ − 𝐴)) ≤ (abs‘(+∞ − 𝐴))) |
45 | | pm2.21 123 |
. . . . . 6
⊢ (¬
-∞ ∈ ℂ → (-∞ ∈ ℂ →
(abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴)))) |
46 | 45 | imp 410 |
. . . . 5
⊢ ((¬
-∞ ∈ ℂ ∧ -∞ ∈ ℂ) →
(abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴))) |
47 | 46 | adantll 714 |
. . . 4
⊢ ((((𝜑 ∧ +∞ ∈ ℂ)
∧ ¬ -∞ ∈ ℂ) ∧ -∞ ∈ ℂ) →
(abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴))) |
48 | 38, 3, 39, 40, 41, 44, 47 | climxrrelem 43010 |
. . 3
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ ¬ -∞ ∈ ℂ) → ∃𝑗 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ) |
49 | 37, 48 | pm2.61dan 813 |
. 2
⊢ ((𝜑 ∧ +∞ ∈ ℂ)
→ ∃𝑗 ∈
𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ) |
50 | 1 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ -∞ ∈ ℂ) → 𝑀 ∈ ℤ) |
51 | 4 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ -∞ ∈ ℂ) → 𝐹:𝑍⟶ℝ*) |
52 | 6 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ -∞ ∈ ℂ) → 𝐹 ⇝ 𝐴) |
53 | 28 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ -∞ ∈ ℂ) → (abs‘(-∞ −
𝐴)) ∈
ℝ+) |
54 | | pm2.21 123 |
. . . . . 6
⊢ (¬
+∞ ∈ ℂ → (+∞ ∈ ℂ →
(abs‘(-∞ − 𝐴)) ≤ (abs‘(+∞ − 𝐴)))) |
55 | 54 | imp 410 |
. . . . 5
⊢ ((¬
+∞ ∈ ℂ ∧ +∞ ∈ ℂ) →
(abs‘(-∞ − 𝐴)) ≤ (abs‘(+∞ − 𝐴))) |
56 | 55 | ad4ant24 754 |
. . . 4
⊢ ((((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ -∞ ∈ ℂ) ∧ +∞ ∈ ℂ) →
(abs‘(-∞ − 𝐴)) ≤ (abs‘(+∞ − 𝐴))) |
57 | 28 | rpred 12657 |
. . . . . 6
⊢ ((𝜑 ∧ -∞ ∈ ℂ)
→ (abs‘(-∞ − 𝐴)) ∈ ℝ) |
58 | 57 | leidd 11427 |
. . . . 5
⊢ ((𝜑 ∧ -∞ ∈ ℂ)
→ (abs‘(-∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴))) |
59 | 58 | ad4ant13 751 |
. . . 4
⊢ ((((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ -∞ ∈ ℂ) ∧ -∞ ∈ ℂ) →
(abs‘(-∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴))) |
60 | 50, 3, 51, 52, 53, 56, 59 | climxrrelem 43010 |
. . 3
⊢ (((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ -∞ ∈ ℂ) → ∃𝑗 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ) |
61 | | nfv 1922 |
. . . . . . 7
⊢
Ⅎ𝑘((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ ¬ -∞ ∈ ℂ) |
62 | | nfv 1922 |
. . . . . . . 8
⊢
Ⅎ𝑘 𝑗 ∈ 𝑍 |
63 | | nfra1 3143 |
. . . . . . . 8
⊢
Ⅎ𝑘∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ |
64 | 62, 63 | nfan 1907 |
. . . . . . 7
⊢
Ⅎ𝑘(𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) |
65 | 61, 64 | nfan 1907 |
. . . . . 6
⊢
Ⅎ𝑘(((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) |
66 | | simp-4l 783 |
. . . . . . . 8
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝜑) |
67 | 3 | uztrn2 12486 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
68 | 67 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
69 | 68 | adantll 714 |
. . . . . . . 8
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
70 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ 𝑍) |
71 | 4 | fdmd 6577 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝐹 = 𝑍) |
72 | 71 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → dom 𝐹 = 𝑍) |
73 | 70, 72 | eleqtrrd 2843 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ dom 𝐹) |
74 | 66, 69, 73 | syl2anc 587 |
. . . . . . 7
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ dom 𝐹) |
75 | 4 | ffvelrnda 6925 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈
ℝ*) |
76 | 66, 69, 75 | syl2anc 587 |
. . . . . . . 8
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈
ℝ*) |
77 | | rspa 3131 |
. . . . . . . . . . 11
⊢
((∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈ ℂ) |
78 | 77 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈ ℂ) |
79 | 78 | adantll 714 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈ ℂ) |
80 | | simpllr 776 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ¬ -∞ ∈
ℂ) |
81 | | nelne2 3042 |
. . . . . . . . 9
⊢ (((𝐹‘𝑘) ∈ ℂ ∧ ¬ -∞ ∈
ℂ) → (𝐹‘𝑘) ≠ -∞) |
82 | 79, 80, 81 | syl2anc 587 |
. . . . . . . 8
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ≠ -∞) |
83 | | simp-4r 784 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ¬ +∞ ∈
ℂ) |
84 | | nelne2 3042 |
. . . . . . . . 9
⊢ (((𝐹‘𝑘) ∈ ℂ ∧ ¬ +∞ ∈
ℂ) → (𝐹‘𝑘) ≠ +∞) |
85 | 79, 83, 84 | syl2anc 587 |
. . . . . . . 8
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ≠ +∞) |
86 | 76, 82, 85 | xrred 42624 |
. . . . . . 7
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈ ℝ) |
87 | 74, 86 | jca 515 |
. . . . . 6
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ ℝ)) |
88 | 65, 87 | ralrimia 3421 |
. . . . 5
⊢ ((((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) → ∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ ℝ)) |
89 | 4 | ffund 6570 |
. . . . . . 7
⊢ (𝜑 → Fun 𝐹) |
90 | | ffvresb 6962 |
. . . . . . 7
⊢ (Fun
𝐹 → ((𝐹 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ ↔
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ ℝ))) |
91 | 89, 90 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ ↔
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ ℝ))) |
92 | 91 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) → ((𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ ↔
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ ℝ))) |
93 | 88, 92 | mpbird 260 |
. . . 4
⊢ ((((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) → (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ) |
94 | | r19.26 3095 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 1) ↔ (∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 1)) |
95 | 94 | simplbi 501 |
. . . . . . . 8
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 1) → ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) |
96 | 95 | ad2antll 729 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 1))) → ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) |
97 | | breq2 5073 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → ((abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥 ↔ (abs‘((𝐹‘𝑘) − 𝐴)) < 1)) |
98 | 97 | anbi2d 632 |
. . . . . . . . 9
⊢ (𝑥 = 1 → (((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥) ↔ ((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 1))) |
99 | 98 | rexralbidv 3230 |
. . . . . . . 8
⊢ (𝑥 = 1 → (∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 1))) |
100 | 3 | fvexi 6752 |
. . . . . . . . . . . . 13
⊢ 𝑍 ∈ V |
101 | 100 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑍 ∈ V) |
102 | 4, 101 | fexd 7064 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ V) |
103 | | eqidd 2740 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
104 | 102, 103 | clim 15087 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥)))) |
105 | 6, 104 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥))) |
106 | 105 | simprd 499 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥)) |
107 | | 1rp 12619 |
. . . . . . . . 9
⊢ 1 ∈
ℝ+ |
108 | 107 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ+) |
109 | 99, 106, 108 | rspcdva 3554 |
. . . . . . 7
⊢ (𝜑 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 1)) |
110 | 96, 109 | reximddv 3204 |
. . . . . 6
⊢ (𝜑 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) |
111 | 3 | rexuz3 14944 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ →
(∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) |
112 | 1, 111 | syl 17 |
. . . . . 6
⊢ (𝜑 → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) |
113 | 110, 112 | mpbird 260 |
. . . . 5
⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) |
114 | 113 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ ¬ -∞ ∈ ℂ) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) |
115 | 93, 114 | reximddv 3204 |
. . 3
⊢ (((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ ¬ -∞ ∈ ℂ) → ∃𝑗 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ) |
116 | 60, 115 | pm2.61dan 813 |
. 2
⊢ ((𝜑 ∧ ¬ +∞ ∈
ℂ) → ∃𝑗
∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ) |
117 | 49, 116 | pm2.61dan 813 |
1
⊢ (𝜑 → ∃𝑗 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ) |