Metamath Proof Explorer

Theorem fnlimabslt

Description: A sequence of function values, approximates the corresponding limit function value, all but finitely many times. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses fnlimabslt.p ⊢ Ⅎ 𝑚 𝜑
fnlimabslt.f ⊢ Ⅎ 𝑚 𝐹
fnlimabslt.n ⊢ Ⅎ 𝑥 𝐹
fnlimabslt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
fnlimabslt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
fnlimabslt.b ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
fnlimabslt.d ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
fnlimabslt.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
fnlimabslt.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
fnlimabslt.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
Assertion fnlimabslt ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) )

Proof

Step Hyp Ref Expression
1 fnlimabslt.p ⊢ Ⅎ 𝑚 𝜑
2 fnlimabslt.f ⊢ Ⅎ 𝑚 𝐹
3 fnlimabslt.n ⊢ Ⅎ 𝑥 𝐹
4 fnlimabslt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5 fnlimabslt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
6 fnlimabslt.b ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
7 fnlimabslt.d ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
8 fnlimabslt.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
9 fnlimabslt.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
10 fnlimabslt.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
11 eqid ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
12 nfcv ⊢ Ⅎ 𝑥 𝑍
13 nfcv ⊢ Ⅎ 𝑥 ( ℤ≥ ‘ 𝑛 )
14 nfcv ⊢ Ⅎ 𝑥 𝑚
15 3 14 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑚 )
16 15 nfdm ⊢ Ⅎ 𝑥 dom ( 𝐹 ‘ 𝑚 )
17 13 16 nfiin ⊢ Ⅎ 𝑥 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
18 12 17 nfiun ⊢ Ⅎ 𝑥 ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
19 nfcv ⊢ Ⅎ 𝑦 ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
20 nfv ⊢ Ⅎ 𝑦 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝
21 nfcv ⊢ Ⅎ 𝑥 𝑦
22 15 21 nffv ⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 )
23 12 22 nfmpt ⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) )
24 nfcv ⊢ Ⅎ 𝑥 dom ⇝
25 23 24 nfel ⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝
26 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) )
27 26 mpteq2dv ⊢ ( 𝑥 = 𝑦 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) )
28 27 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ ↔ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ ) )
29 18 19 20 25 28 cbvrabw ⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } = { 𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ }
30 ssrab2 ⊢ { 𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
31 29 30 eqsstri ⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
32 7 31 eqsstri ⊢ 𝐷 ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
33 32 9 sselid ⊢ ( 𝜑 → 𝑋 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
34 1 5 6 11 33 allbutfifvre ⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℝ )
35 nfv ⊢ Ⅎ 𝑗 𝜑
36 nfcv ⊢ Ⅎ 𝑗 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) )
37 3 7 8 9 fnlimcnv ⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ⇝ ( 𝐺 ‘ 𝑋 ) )
38 nfcv ⊢ Ⅎ 𝑙 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 )
39 nfcv ⊢ Ⅎ 𝑚 𝑙
40 2 39 nffv ⊢ Ⅎ 𝑚 ( 𝐹 ‘ 𝑙 )
41 nfcv ⊢ Ⅎ 𝑚 𝑋
42 40 41 nffv ⊢ Ⅎ 𝑚 ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑋 )
43 fveq2 ⊢ ( 𝑚 = 𝑙 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑙 ) )
44 43 fveq1d ⊢ ( 𝑚 = 𝑙 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑋 ) )
45 38 42 44 cbvmpt ⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) = ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑋 ) )
46 fveq2 ⊢ ( 𝑙 = 𝑗 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑗 ) )
47 46 fveq1d ⊢ ( 𝑙 = 𝑗 → ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) )
48 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝑍 )
49 fvexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) ∈ V )
50 45 47 48 49 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) )
51 35 36 5 4 37 50 10 climd ⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) )
52 nfv ⊢ Ⅎ 𝑗 ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 )
53 nfcv ⊢ Ⅎ 𝑚 𝑗
54 2 53 nffv ⊢ Ⅎ 𝑚 ( 𝐹 ‘ 𝑗 )
55 54 41 nffv ⊢ Ⅎ 𝑚 ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 )
56 nfcv ⊢ Ⅎ 𝑚 ℂ
57 55 56 nfel ⊢ Ⅎ 𝑚 ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) ∈ ℂ
58 nfcv ⊢ Ⅎ 𝑚 abs
59 nfcv ⊢ Ⅎ 𝑚 −
60 nfmpt1 ⊢ Ⅎ 𝑚 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
61 nfcv ⊢ Ⅎ 𝑚 dom ⇝
62 60 61 nfel ⊢ Ⅎ 𝑚 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝
63 nfcv ⊢ Ⅎ 𝑚 𝑍
64 nfii1 ⊢ Ⅎ 𝑚 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
65 63 64 nfiun ⊢ Ⅎ 𝑚 ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
66 62 65 nfrabw ⊢ Ⅎ 𝑚 { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
67 7 66 nfcxfr ⊢ Ⅎ 𝑚 𝐷
68 nfcv ⊢ Ⅎ 𝑚 ⇝
69 68 60 nffv ⊢ Ⅎ 𝑚 ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
70 67 69 nfmpt ⊢ Ⅎ 𝑚 ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
71 8 70 nfcxfr ⊢ Ⅎ 𝑚 𝐺
72 71 41 nffv ⊢ Ⅎ 𝑚 ( 𝐺 ‘ 𝑋 )
73 55 59 72 nfov ⊢ Ⅎ 𝑚 ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) )
74 58 73 nffv ⊢ Ⅎ 𝑚 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) )
75 nfcv ⊢ Ⅎ 𝑚 <
76 nfcv ⊢ Ⅎ 𝑚 𝑌
77 74 75 76 nfbr ⊢ Ⅎ 𝑚 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌
78 57 77 nfan ⊢ Ⅎ 𝑚 ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 )
79 fveq2 ⊢ ( 𝑚 = 𝑗 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑗 ) )
80 79 fveq1d ⊢ ( 𝑚 = 𝑗 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) )
81 80 eleq1d ⊢ ( 𝑚 = 𝑗 → ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℂ ↔ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) ∈ ℂ ) )
82 80 fvoveq1d ⊢ ( 𝑚 = 𝑗 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) )
83 82 breq1d ⊢ ( 𝑚 = 𝑗 → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) )
84 81 83 anbi12d ⊢ ( 𝑚 = 𝑗 → ( ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) ↔ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) ) )
85 52 78 84 cbvralw ⊢ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) )
86 85 rexbii ⊢ ( ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) ↔ ∃ 𝑛 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) )
87 51 86 sylibr ⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) )
88 nfv ⊢ Ⅎ 𝑚 𝑛 ∈ 𝑍
89 1 88 nfan ⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑛 ∈ 𝑍 )
90 simpr ⊢ ( ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 )
91 90 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) )
92 89 91 ralimdaa ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) )
93 92 reximdva ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) )
94 87 93 mpd ⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 )
95 34 94 jca ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℝ ∧ ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) )
96 5 rexanuz2 ⊢ ( ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) ↔ ( ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℝ ∧ ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) )
97 95 96 sylibr ⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑌 ) )