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