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 ( 𝜑 → ∃ 𝑗𝑍 ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ ℝ )