Metamath Proof Explorer

Theorem climxrrelem

Description: If a seqence ranging over the extended reals converges w.r.t. the standard topology on the complex numbers, then there exists an upper set of the integers over which the function is real-valued. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses climxrrelem.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climxrrelem.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climxrrelem.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
climxrrelem.c ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
climxrrelem.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
climxrrelem.p ⊢ ( ( 𝜑 ∧ +∞ ∈ ℂ ) → 𝐷 ≤ ( abs ‘ ( +∞ − 𝐴 ) ) )
climxrrelem.n ⊢ ( ( 𝜑 ∧ -∞ ∈ ℂ ) → 𝐷 ≤ ( abs ‘ ( -∞ − 𝐴 ) ) )
Assertion climxrrelem ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 climxrrelem.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 climxrrelem.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 climxrrelem.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
4 climxrrelem.c ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
5 climxrrelem.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
6 climxrrelem.p ⊢ ( ( 𝜑 ∧ +∞ ∈ ℂ ) → 𝐷 ≤ ( abs ‘ ( +∞ − 𝐴 ) ) )
7 climxrrelem.n ⊢ ( ( 𝜑 ∧ -∞ ∈ ℂ ) → 𝐷 ≤ ( abs ‘ ( -∞ − 𝐴 ) ) )
8 nfv ⊢ Ⅎ 𝑘 𝜑
9 nfv ⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
10 nfra1 ⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 )
11 9 10 nfan ⊢ Ⅎ 𝑘 ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) )
12 8 11 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) )
13 2 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
14 13 adantll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
15 3 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝑍 )
16 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → dom 𝐹 = 𝑍 )
17 14 16 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ dom 𝐹 )
18 17 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ dom 𝐹 )
19 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝜑 )
20 14 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
21 rspa ⊢ ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) )
22 21 adantll ⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) )
23 22 adantll ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) )
24 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
25 24 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
26 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) = -∞ ) → 𝜑 )
27 simpr ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑘 ) = -∞ ) → ( 𝐹 ‘ 𝑘 ) = -∞ )
28 simpl ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑘 ) = -∞ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
29 27 28 eqeltrrd ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑘 ) = -∞ ) → -∞ ∈ ℂ )
30 29 adantll ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) = -∞ ) → -∞ ∈ ℂ )
31 26 30 7 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) = -∞ ) → 𝐷 ≤ ( abs ‘ ( -∞ − 𝐴 ) ) )
32 31 adantlrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑘 ) = -∞ ) → 𝐷 ≤ ( abs ‘ ( -∞ − 𝐴 ) ) )
33 fvoveq1 ⊢ ( ( 𝐹 ‘ 𝑘 ) = -∞ → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) = ( abs ‘ ( -∞ − 𝐴 ) ) )
34 33 adantl ⊢ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ∧ ( 𝐹 ‘ 𝑘 ) = -∞ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) = ( abs ‘ ( -∞ − 𝐴 ) ) )
35 simpl ⊢ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ∧ ( 𝐹 ‘ 𝑘 ) = -∞ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 )
36 34 35 eqbrtrrd ⊢ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ∧ ( 𝐹 ‘ 𝑘 ) = -∞ ) → ( abs ‘ ( -∞ − 𝐴 ) ) < 𝐷 )
37 36 adantll ⊢ ( ( ( 𝜑 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ∧ ( 𝐹 ‘ 𝑘 ) = -∞ ) → ( abs ‘ ( -∞ − 𝐴 ) ) < 𝐷 )
38 37 adantlrl ⊢ ( ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑘 ) = -∞ ) → ( abs ‘ ( -∞ − 𝐴 ) ) < 𝐷 )
39 2 fvexi ⊢ 𝑍 ∈ V
40 39 a1i ⊢ ( 𝜑 → 𝑍 ∈ V )
41 3 40 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
42 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
43 41 42 clim ⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) ) )
44 4 43 mpbid ⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
45 44 simpld ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
46 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) = -∞ ) → 𝐴 ∈ ℂ )
47 30 46 subcld ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) = -∞ ) → ( -∞ − 𝐴 ) ∈ ℂ )
48 47 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) = -∞ ) → ( abs ‘ ( -∞ − 𝐴 ) ) ∈ ℝ )
49 48 adantlrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑘 ) = -∞ ) → ( abs ‘ ( -∞ − 𝐴 ) ) ∈ ℝ )
50 5 rpred ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
51 50 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑘 ) = -∞ ) → 𝐷 ∈ ℝ )
52 49 51 ltnled ⊢ ( ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑘 ) = -∞ ) → ( ( abs ‘ ( -∞ − 𝐴 ) ) < 𝐷 ↔ ¬ 𝐷 ≤ ( abs ‘ ( -∞ − 𝐴 ) ) ) )
53 38 52 mpbid ⊢ ( ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑘 ) = -∞ ) → ¬ 𝐷 ≤ ( abs ‘ ( -∞ − 𝐴 ) ) )
54 32 53 pm2.65da ⊢ ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) → ¬ ( 𝐹 ‘ 𝑘 ) = -∞ )
55 54 3adant2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) → ¬ ( 𝐹 ‘ 𝑘 ) = -∞ )
56 55 neqned ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) → ( 𝐹 ‘ 𝑘 ) ≠ -∞ )
57 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) = +∞ ) → 𝜑 )
58 simpr ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑘 ) = +∞ ) → ( 𝐹 ‘ 𝑘 ) = +∞ )
59 simpl ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑘 ) = +∞ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
60 58 59 eqeltrrd ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑘 ) = +∞ ) → +∞ ∈ ℂ )
61 60 adantll ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) = +∞ ) → +∞ ∈ ℂ )
62 57 61 6 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) = +∞ ) → 𝐷 ≤ ( abs ‘ ( +∞ − 𝐴 ) ) )
63 62 adantlrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑘 ) = +∞ ) → 𝐷 ≤ ( abs ‘ ( +∞ − 𝐴 ) ) )
64 fvoveq1 ⊢ ( ( 𝐹 ‘ 𝑘 ) = +∞ → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) = ( abs ‘ ( +∞ − 𝐴 ) ) )
65 64 adantl ⊢ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ∧ ( 𝐹 ‘ 𝑘 ) = +∞ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) = ( abs ‘ ( +∞ − 𝐴 ) ) )
66 simpl ⊢ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ∧ ( 𝐹 ‘ 𝑘 ) = +∞ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 )
67 65 66 eqbrtrrd ⊢ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ∧ ( 𝐹 ‘ 𝑘 ) = +∞ ) → ( abs ‘ ( +∞ − 𝐴 ) ) < 𝐷 )
68 67 adantll ⊢ ( ( ( 𝜑 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ∧ ( 𝐹 ‘ 𝑘 ) = +∞ ) → ( abs ‘ ( +∞ − 𝐴 ) ) < 𝐷 )
69 68 adantlrl ⊢ ( ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑘 ) = +∞ ) → ( abs ‘ ( +∞ − 𝐴 ) ) < 𝐷 )
70 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) = +∞ ) → 𝐴 ∈ ℂ )
71 61 70 subcld ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) = +∞ ) → ( +∞ − 𝐴 ) ∈ ℂ )
72 71 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) = +∞ ) → ( abs ‘ ( +∞ − 𝐴 ) ) ∈ ℝ )
73 72 adantlrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑘 ) = +∞ ) → ( abs ‘ ( +∞ − 𝐴 ) ) ∈ ℝ )
74 50 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑘 ) = +∞ ) → 𝐷 ∈ ℝ )
75 73 74 ltnled ⊢ ( ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑘 ) = +∞ ) → ( ( abs ‘ ( +∞ − 𝐴 ) ) < 𝐷 ↔ ¬ 𝐷 ≤ ( abs ‘ ( +∞ − 𝐴 ) ) ) )
76 69 75 mpbid ⊢ ( ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑘 ) = +∞ ) → ¬ 𝐷 ≤ ( abs ‘ ( +∞ − 𝐴 ) ) )
77 63 76 pm2.65da ⊢ ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) → ¬ ( 𝐹 ‘ 𝑘 ) = +∞ )
78 77 3adant2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) → ¬ ( 𝐹 ‘ 𝑘 ) = +∞ )
79 78 neqned ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) → ( 𝐹 ‘ 𝑘 ) ≠ +∞ )
80 25 56 79 xrred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
81 19 20 23 80 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
82 18 81 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) )
83 12 82 ralrimia ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) )
84 3 ffund ⊢ ( 𝜑 → Fun 𝐹 )
85 ffvresb ⊢ ( Fun 𝐹 → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) )
86 84 85 syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) )
87 86 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) )
88 83 87 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ )
89 breq2 ⊢ ( 𝑥 = 𝐷 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) )
90 89 anbi2d ⊢ ( 𝑥 = 𝐷 → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) )
91 90 rexralbidv ⊢ ( 𝑥 = 𝐷 → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) )
92 44 simprd ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
93 91 92 5 rspcdva ⊢ ( 𝜑 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) )
94 2 rexuz3 ⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) )
95 1 94 syl ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) ) )
96 93 95 mpbird ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝐷 ) )
97 88 96 reximddv ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ )