Metamath Proof Explorer

Theorem climxrre

Description: If a sequence 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 (the weaker hypothesis F e. dom ~> is probably not enough, since in principle we could have +oo e. CC and -oo e. CC ). (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses climxrre.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climxrre.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climxrre.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
climxrre.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
climxrre.c ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
Assertion climxrre ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 climxrre.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 climxrre.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 climxrre.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
4 climxrre.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
5 climxrre.c ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
6 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → 𝑀 ∈ ℤ )
7 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → 𝐹 : 𝑍 ⟶ ℝ* )
8 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → 𝐹 ⇝ 𝐴 )
9 simpr ⊢ ( ( 𝜑 ∧ +∞ ∈ ℂ ) → +∞ ∈ ℂ )
10 4 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
11 10 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ℂ ) → 𝐴 ∈ ℂ )
12 9 11 subcld ⊢ ( ( 𝜑 ∧ +∞ ∈ ℂ ) → ( +∞ − 𝐴 ) ∈ ℂ )
13 renepnf ⊢ ( 𝐴 ∈ ℝ → 𝐴 ≠ +∞ )
14 13 necomd ⊢ ( 𝐴 ∈ ℝ → +∞ ≠ 𝐴 )
15 4 14 syl ⊢ ( 𝜑 → +∞ ≠ 𝐴 )
16 15 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ℂ ) → +∞ ≠ 𝐴 )
17 9 11 16 subne0d ⊢ ( ( 𝜑 ∧ +∞ ∈ ℂ ) → ( +∞ − 𝐴 ) ≠ 0 )
18 12 17 absrpcld ⊢ ( ( 𝜑 ∧ +∞ ∈ ℂ ) → ( abs ‘ ( +∞ − 𝐴 ) ) ∈ ℝ+ )
19 18 adantr ⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → ( abs ‘ ( +∞ − 𝐴 ) ) ∈ ℝ+ )
20 simpr ⊢ ( ( 𝜑 ∧ -∞ ∈ ℂ ) → -∞ ∈ ℂ )
21 10 adantr ⊢ ( ( 𝜑 ∧ -∞ ∈ ℂ ) → 𝐴 ∈ ℂ )
22 20 21 subcld ⊢ ( ( 𝜑 ∧ -∞ ∈ ℂ ) → ( -∞ − 𝐴 ) ∈ ℂ )
23 4 adantr ⊢ ( ( 𝜑 ∧ -∞ ∈ ℂ ) → 𝐴 ∈ ℝ )
24 renemnf ⊢ ( 𝐴 ∈ ℝ → 𝐴 ≠ -∞ )
25 24 necomd ⊢ ( 𝐴 ∈ ℝ → -∞ ≠ 𝐴 )
26 23 25 syl ⊢ ( ( 𝜑 ∧ -∞ ∈ ℂ ) → -∞ ≠ 𝐴 )
27 20 21 26 subne0d ⊢ ( ( 𝜑 ∧ -∞ ∈ ℂ ) → ( -∞ − 𝐴 ) ≠ 0 )
28 22 27 absrpcld ⊢ ( ( 𝜑 ∧ -∞ ∈ ℂ ) → ( abs ‘ ( -∞ − 𝐴 ) ) ∈ ℝ+ )
29 28 adantlr ⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → ( abs ‘ ( -∞ − 𝐴 ) ) ∈ ℝ+ )
30 19 29 ifcld ⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → if ( ( abs ‘ ( +∞ − 𝐴 ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) , ( abs ‘ ( +∞ − 𝐴 ) ) , ( abs ‘ ( -∞ − 𝐴 ) ) ) ∈ ℝ+ )
31 19 rpred ⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → ( abs ‘ ( +∞ − 𝐴 ) ) ∈ ℝ )
32 29 rpred ⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → ( abs ‘ ( -∞ − 𝐴 ) ) ∈ ℝ )
33 31 32 min1d ⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → if ( ( abs ‘ ( +∞ − 𝐴 ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) , ( abs ‘ ( +∞ − 𝐴 ) ) , ( abs ‘ ( -∞ − 𝐴 ) ) ) ≤ ( abs ‘ ( +∞ − 𝐴 ) ) )
34 33 adantr ⊢ ( ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) ∧ +∞ ∈ ℂ ) → if ( ( abs ‘ ( +∞ − 𝐴 ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) , ( abs ‘ ( +∞ − 𝐴 ) ) , ( abs ‘ ( -∞ − 𝐴 ) ) ) ≤ ( abs ‘ ( +∞ − 𝐴 ) ) )
35 31 32 min2d ⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → if ( ( abs ‘ ( +∞ − 𝐴 ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) , ( abs ‘ ( +∞ − 𝐴 ) ) , ( abs ‘ ( -∞ − 𝐴 ) ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) )
36 35 adantr ⊢ ( ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → if ( ( abs ‘ ( +∞ − 𝐴 ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) , ( abs ‘ ( +∞ − 𝐴 ) ) , ( abs ‘ ( -∞ − 𝐴 ) ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) )
37 6 2 7 8 30 34 36 climxrrelem ⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ )
38 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) → 𝑀 ∈ ℤ )
39 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) → 𝐹 : 𝑍 ⟶ ℝ* )
40 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) → 𝐹 ⇝ 𝐴 )
41 18 adantr ⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) → ( abs ‘ ( +∞ − 𝐴 ) ) ∈ ℝ+ )
42 18 rpred ⊢ ( ( 𝜑 ∧ +∞ ∈ ℂ ) → ( abs ‘ ( +∞ − 𝐴 ) ) ∈ ℝ )
43 42 leidd ⊢ ( ( 𝜑 ∧ +∞ ∈ ℂ ) → ( abs ‘ ( +∞ − 𝐴 ) ) ≤ ( abs ‘ ( +∞ − 𝐴 ) ) )
44 43 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ +∞ ∈ ℂ ) → ( abs ‘ ( +∞ − 𝐴 ) ) ≤ ( abs ‘ ( +∞ − 𝐴 ) ) )
45 pm2.21 ⊢ ( ¬ -∞ ∈ ℂ → ( -∞ ∈ ℂ → ( abs ‘ ( +∞ − 𝐴 ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) ) )
46 45 imp ⊢ ( ( ¬ -∞ ∈ ℂ ∧ -∞ ∈ ℂ ) → ( abs ‘ ( +∞ − 𝐴 ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) )
47 46 adantll ⊢ ( ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → ( abs ‘ ( +∞ − 𝐴 ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) )
48 38 2 39 40 41 44 47 climxrrelem ⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ )
49 37 48 pm2.61dan ⊢ ( ( 𝜑 ∧ +∞ ∈ ℂ ) → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ )
50 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → 𝑀 ∈ ℤ )
51 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → 𝐹 : 𝑍 ⟶ ℝ* )
52 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → 𝐹 ⇝ 𝐴 )
53 28 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → ( abs ‘ ( -∞ − 𝐴 ) ) ∈ ℝ+ )
54 pm2.21 ⊢ ( ¬ +∞ ∈ ℂ → ( +∞ ∈ ℂ → ( abs ‘ ( -∞ − 𝐴 ) ) ≤ ( abs ‘ ( +∞ − 𝐴 ) ) ) )
55 54 imp ⊢ ( ( ¬ +∞ ∈ ℂ ∧ +∞ ∈ ℂ ) → ( abs ‘ ( -∞ − 𝐴 ) ) ≤ ( abs ‘ ( +∞ − 𝐴 ) ) )
56 55 ad4ant24 ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) ∧ +∞ ∈ ℂ ) → ( abs ‘ ( -∞ − 𝐴 ) ) ≤ ( abs ‘ ( +∞ − 𝐴 ) ) )
57 28 rpred ⊢ ( ( 𝜑 ∧ -∞ ∈ ℂ ) → ( abs ‘ ( -∞ − 𝐴 ) ) ∈ ℝ )
58 57 leidd ⊢ ( ( 𝜑 ∧ -∞ ∈ ℂ ) → ( abs ‘ ( -∞ − 𝐴 ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) )
59 58 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → ( abs ‘ ( -∞ − 𝐴 ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) )
60 50 2 51 52 53 56 59 climxrrelem ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ )
61 nfv ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ )
62 nfv ⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
63 nfra1 ⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ
64 62 63 nfan ⊢ Ⅎ 𝑘 ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
65 61 64 nfan ⊢ Ⅎ 𝑘 ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) )
66 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝜑 )
67 2 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
68 67 adantlr ⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
69 68 adantll ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
70 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝑍 )
71 3 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝑍 )
72 71 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → dom 𝐹 = 𝑍 )
73 70 72 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ dom 𝐹 )
74 66 69 73 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ dom 𝐹 )
75 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
76 66 69 75 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
77 rspa ⊢ ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
78 77 adantll ⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
79 78 adantll ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
80 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ¬ -∞ ∈ ℂ )
81 nelne2 ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ¬ -∞ ∈ ℂ ) → ( 𝐹 ‘ 𝑘 ) ≠ -∞ )
82 79 80 81 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ≠ -∞ )
83 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ¬ +∞ ∈ ℂ )
84 nelne2 ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ¬ +∞ ∈ ℂ ) → ( 𝐹 ‘ 𝑘 ) ≠ +∞ )
85 79 83 84 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ≠ +∞ )
86 76 82 85 xrred ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
87 74 86 jca ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) )
88 65 87 ralrimia ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) )
89 3 ffund ⊢ ( 𝜑 → Fun 𝐹 )
90 ffvresb ⊢ ( Fun 𝐹 → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) )
91 89 90 syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) )
92 91 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) )
93 88 92 mpbird ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ )
94 r19.26 ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 1 ) ↔ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 1 ) )
95 94 simplbi ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 1 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
96 95 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 1 ) ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
97 breq2 ⊢ ( 𝑥 = 1 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 1 ) )
98 97 anbi2d ⊢ ( 𝑥 = 1 → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 1 ) ) )
99 98 rexralbidv ⊢ ( 𝑥 = 1 → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 1 ) ) )
100 2 fvexi ⊢ 𝑍 ∈ V
101 100 a1i ⊢ ( 𝜑 → 𝑍 ∈ V )
102 3 101 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
103 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
104 102 103 clim ⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) ) )
105 5 104 mpbid ⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
106 105 simprd ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
107 1rp ⊢ 1 ∈ ℝ+
108 107 a1i ⊢ ( 𝜑 → 1 ∈ ℝ+ )
109 99 106 108 rspcdva ⊢ ( 𝜑 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 1 ) )
110 96 109 reximddv ⊢ ( 𝜑 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
111 2 rexuz3 ⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) )
112 1 111 syl ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) )
113 110 112 mpbird ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
114 113 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
115 93 114 reximddv ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ )
116 60 115 pm2.61dan ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ )
117 49 116 pm2.61dan ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ )