| 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 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ +∞ ∈ ℂ)
→ +∞ ∈ ℂ) |
| 9 | | climxrre.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 10 | 9 | recnd 11289 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 11 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ +∞ ∈ ℂ)
→ 𝐴 ∈
ℂ) |
| 12 | 8, 11 | subcld 11620 |
. . . . . . 7
⊢ ((𝜑 ∧ +∞ ∈ ℂ)
→ (+∞ − 𝐴)
∈ ℂ) |
| 13 | | renepnf 11309 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞) |
| 14 | 13 | necomd 2996 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → +∞
≠ 𝐴) |
| 15 | 9, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → +∞ ≠ 𝐴) |
| 16 | 15 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ +∞ ∈ ℂ)
→ +∞ ≠ 𝐴) |
| 17 | 8, 11, 16 | subne0d 11629 |
. . . . . . 7
⊢ ((𝜑 ∧ +∞ ∈ ℂ)
→ (+∞ − 𝐴)
≠ 0) |
| 18 | 12, 17 | absrpcld 15487 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ℂ)
→ (abs‘(+∞ − 𝐴)) ∈
ℝ+) |
| 19 | 18 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) → (abs‘(+∞ − 𝐴)) ∈
ℝ+) |
| 20 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ -∞ ∈ ℂ)
→ -∞ ∈ ℂ) |
| 21 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ -∞ ∈ ℂ)
→ 𝐴 ∈
ℂ) |
| 22 | 20, 21 | subcld 11620 |
. . . . . . 7
⊢ ((𝜑 ∧ -∞ ∈ ℂ)
→ (-∞ − 𝐴)
∈ ℂ) |
| 23 | 9 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ -∞ ∈ ℂ)
→ 𝐴 ∈
ℝ) |
| 24 | | renemnf 11310 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞) |
| 25 | 24 | necomd 2996 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → -∞
≠ 𝐴) |
| 26 | 23, 25 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ -∞ ∈ ℂ)
→ -∞ ≠ 𝐴) |
| 27 | 20, 21, 26 | subne0d 11629 |
. . . . . . 7
⊢ ((𝜑 ∧ -∞ ∈ ℂ)
→ (-∞ − 𝐴)
≠ 0) |
| 28 | 22, 27 | absrpcld 15487 |
. . . . . 6
⊢ ((𝜑 ∧ -∞ ∈ ℂ)
→ (abs‘(-∞ − 𝐴)) ∈
ℝ+) |
| 29 | 28 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) → (abs‘(-∞ − 𝐴)) ∈
ℝ+) |
| 30 | 19, 29 | ifcld 4572 |
. . . 4
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) → if((abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞
− 𝐴)),
(abs‘(+∞ − 𝐴)), (abs‘(-∞ − 𝐴))) ∈
ℝ+) |
| 31 | 19 | rpred 13077 |
. . . . . 6
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) → (abs‘(+∞ − 𝐴)) ∈
ℝ) |
| 32 | 29 | rpred 13077 |
. . . . . 6
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) → (abs‘(-∞ − 𝐴)) ∈
ℝ) |
| 33 | 31, 32 | min1d 45483 |
. . . . 5
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) → if((abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞
− 𝐴)),
(abs‘(+∞ − 𝐴)), (abs‘(-∞ − 𝐴))) ≤ (abs‘(+∞
− 𝐴))) |
| 34 | 33 | adantr 480 |
. . . 4
⊢ ((((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) ∧ +∞ ∈ ℂ) →
if((abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴)), (abs‘(+∞ −
𝐴)), (abs‘(-∞
− 𝐴))) ≤
(abs‘(+∞ − 𝐴))) |
| 35 | 31, 32 | min2d 45484 |
. . . . 5
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) → if((abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞
− 𝐴)),
(abs‘(+∞ − 𝐴)), (abs‘(-∞ − 𝐴))) ≤ (abs‘(-∞
− 𝐴))) |
| 36 | 35 | adantr 480 |
. . . 4
⊢ ((((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) ∧ -∞ ∈ ℂ) →
if((abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴)), (abs‘(+∞ −
𝐴)), (abs‘(-∞
− 𝐴))) ≤
(abs‘(-∞ − 𝐴))) |
| 37 | 2, 3, 5, 7, 30, 34, 36 | climxrrelem 45764 |
. . 3
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ -∞ ∈ ℂ) → ∃𝑗 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ) |
| 38 | 1 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ ¬ -∞ ∈ ℂ) → 𝑀 ∈ ℤ) |
| 39 | 4 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ ¬ -∞ ∈ ℂ) → 𝐹:𝑍⟶ℝ*) |
| 40 | 6 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ ¬ -∞ ∈ ℂ) → 𝐹 ⇝ 𝐴) |
| 41 | 18 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ +∞ ∈ ℂ)
∧ ¬ -∞ ∈ ℂ) → (abs‘(+∞ − 𝐴)) ∈
ℝ+) |
| 42 | 18 | rpred 13077 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ℂ)
→ (abs‘(+∞ − 𝐴)) ∈ ℝ) |
| 43 | 42 | leidd 11829 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ℂ)
→ (abs‘(+∞ − 𝐴)) ≤ (abs‘(+∞ − 𝐴))) |
| 44 | 43 | ad2antrr 726 |
. . . 4
⊢ ((((𝜑 ∧ +∞ ∈ ℂ)
∧ ¬ -∞ ∈ ℂ) ∧ +∞ ∈ ℂ) →
(abs‘(+∞ − 𝐴)) ≤ (abs‘(+∞ − 𝐴))) |
| 45 | | pm2.21 123 |
. . . . . 6
⊢ (¬
-∞ ∈ ℂ → (-∞ ∈ ℂ →
(abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴)))) |
| 46 | 45 | imp 406 |
. . . . 5
⊢ ((¬
-∞ ∈ ℂ ∧ -∞ ∈ ℂ) →
(abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴))) |
| 47 | 46 | adantll 714 |
. . . 4
⊢ ((((𝜑 ∧ +∞ ∈ ℂ)
∧ ¬ -∞ ∈ ℂ) ∧ -∞ ∈ ℂ) →
(abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴))) |
| 48 | 38, 3, 39, 40, 41, 44, 47 | climxrrelem 45764 |
. . 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 406 |
. . . . 5
⊢ ((¬
+∞ ∈ ℂ ∧ +∞ ∈ ℂ) →
(abs‘(-∞ − 𝐴)) ≤ (abs‘(+∞ − 𝐴))) |
| 56 | 55 | ad4ant24 754 |
. . . 4
⊢ ((((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ -∞ ∈ ℂ) ∧ +∞ ∈ ℂ) →
(abs‘(-∞ − 𝐴)) ≤ (abs‘(+∞ − 𝐴))) |
| 57 | 28 | rpred 13077 |
. . . . . 6
⊢ ((𝜑 ∧ -∞ ∈ ℂ)
→ (abs‘(-∞ − 𝐴)) ∈ ℝ) |
| 58 | 57 | leidd 11829 |
. . . . 5
⊢ ((𝜑 ∧ -∞ ∈ ℂ)
→ (abs‘(-∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴))) |
| 59 | 58 | ad4ant13 751 |
. . . 4
⊢ ((((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ -∞ ∈ ℂ) ∧ -∞ ∈ ℂ) →
(abs‘(-∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴))) |
| 60 | 50, 3, 51, 52, 53, 56, 59 | climxrrelem 45764 |
. . 3
⊢ (((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ -∞ ∈ ℂ) → ∃𝑗 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ) |
| 61 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑘((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ ¬ -∞ ∈ ℂ) |
| 62 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑘 𝑗 ∈ 𝑍 |
| 63 | | nfra1 3284 |
. . . . . . . 8
⊢
Ⅎ𝑘∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ |
| 64 | 62, 63 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑘(𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) |
| 65 | 61, 64 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑘(((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) |
| 66 | | simp-4l 783 |
. . . . . . . 8
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝜑) |
| 67 | 3 | uztrn2 12897 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
| 68 | 67 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
| 69 | 68 | adantll 714 |
. . . . . . . 8
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
| 70 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ 𝑍) |
| 71 | 4 | fdmd 6746 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝐹 = 𝑍) |
| 72 | 71 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → dom 𝐹 = 𝑍) |
| 73 | 70, 72 | eleqtrrd 2844 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ dom 𝐹) |
| 74 | 66, 69, 73 | syl2anc 584 |
. . . . . . 7
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ dom 𝐹) |
| 75 | 4 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈
ℝ*) |
| 76 | 66, 69, 75 | syl2anc 584 |
. . . . . . . 8
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈
ℝ*) |
| 77 | | rspa 3248 |
. . . . . . . . . . 11
⊢
((∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈ ℂ) |
| 78 | 77 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈ ℂ) |
| 79 | 78 | adantll 714 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈ ℂ) |
| 80 | | simpllr 776 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ¬ -∞ ∈
ℂ) |
| 81 | | nelne2 3040 |
. . . . . . . . 9
⊢ (((𝐹‘𝑘) ∈ ℂ ∧ ¬ -∞ ∈
ℂ) → (𝐹‘𝑘) ≠ -∞) |
| 82 | 79, 80, 81 | syl2anc 584 |
. . . . . . . 8
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ≠ -∞) |
| 83 | | simp-4r 784 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ¬ +∞ ∈
ℂ) |
| 84 | | nelne2 3040 |
. . . . . . . . 9
⊢ (((𝐹‘𝑘) ∈ ℂ ∧ ¬ +∞ ∈
ℂ) → (𝐹‘𝑘) ≠ +∞) |
| 85 | 79, 83, 84 | syl2anc 584 |
. . . . . . . 8
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ≠ +∞) |
| 86 | 76, 82, 85 | xrred 45376 |
. . . . . . 7
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈ ℝ) |
| 87 | 74, 86 | jca 511 |
. . . . . 6
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ ℝ)) |
| 88 | 65, 87 | ralrimia 3258 |
. . . . 5
⊢ ((((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) → ∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ ℝ)) |
| 89 | 4 | ffund 6740 |
. . . . . . 7
⊢ (𝜑 → Fun 𝐹) |
| 90 | | ffvresb 7145 |
. . . . . . 7
⊢ (Fun
𝐹 → ((𝐹 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ ↔
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ ℝ))) |
| 91 | 89, 90 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ ↔
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ ℝ))) |
| 92 | 91 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) → ((𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ ↔
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ ℝ))) |
| 93 | 88, 92 | mpbird 257 |
. . . 4
⊢ ((((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) → (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ) |
| 94 | | r19.26 3111 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 1) ↔ (∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 1)) |
| 95 | 94 | simplbi 497 |
. . . . . . . 8
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 1) → ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) |
| 96 | 95 | ad2antll 729 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 1))) → ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) |
| 97 | | breq2 5147 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → ((abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥 ↔ (abs‘((𝐹‘𝑘) − 𝐴)) < 1)) |
| 98 | 97 | anbi2d 630 |
. . . . . . . . 9
⊢ (𝑥 = 1 → (((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥) ↔ ((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 1))) |
| 99 | 98 | rexralbidv 3223 |
. . . . . . . 8
⊢ (𝑥 = 1 → (∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 1))) |
| 100 | 3 | fvexi 6920 |
. . . . . . . . . . . . 13
⊢ 𝑍 ∈ V |
| 101 | 100 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑍 ∈ V) |
| 102 | 4, 101 | fexd 7247 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ V) |
| 103 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
| 104 | 102, 103 | clim 15530 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥)))) |
| 105 | 6, 104 | mpbid 232 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥))) |
| 106 | 105 | simprd 495 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥)) |
| 107 | | 1rp 13038 |
. . . . . . . . 9
⊢ 1 ∈
ℝ+ |
| 108 | 107 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ+) |
| 109 | 99, 106, 108 | rspcdva 3623 |
. . . . . . 7
⊢ (𝜑 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 1)) |
| 110 | 96, 109 | reximddv 3171 |
. . . . . 6
⊢ (𝜑 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) |
| 111 | 3 | rexuz3 15387 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ →
(∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) |
| 112 | 1, 111 | syl 17 |
. . . . . 6
⊢ (𝜑 → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ)) |
| 113 | 110, 112 | mpbird 257 |
. . . . 5
⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) |
| 114 | 113 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ ¬ -∞ ∈ ℂ) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℂ) |
| 115 | 93, 114 | reximddv 3171 |
. . 3
⊢ (((𝜑 ∧ ¬ +∞ ∈
ℂ) ∧ ¬ -∞ ∈ ℂ) → ∃𝑗 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ) |
| 116 | 60, 115 | pm2.61dan 813 |
. 2
⊢ ((𝜑 ∧ ¬ +∞ ∈
ℂ) → ∃𝑗
∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ) |
| 117 | 49, 116 | pm2.61dan 813 |
1
⊢ (𝜑 → ∃𝑗 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ) |