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	$⊢ Ⅎ m φ$
	fnlimabslt.f	$⊢ \underline{Ⅎ} m F$
	fnlimabslt.n	$⊢ \underline{Ⅎ} x F$
	fnlimabslt.m	$⊢ φ \to M \in ℤ$
	fnlimabslt.z	$⊢ Z = ℤ_{\geq M}$
	fnlimabslt.b	$⊢ (φ \land m \in Z) \to F (m) : dom F (m) ⟶ ℝ$
	fnlimabslt.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
	fnlimabslt.g	$⊢ G = (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x))))$
	fnlimabslt.x	$⊢ φ \to X \in D$
	fnlimabslt.y	$⊢ φ \to Y \in ℝ^{+}$
Assertion	fnlimabslt	$⊢ φ \to \exists n \in Z \forall m \in ℤ_{\geq n} (F (m) (X) \in ℝ \land \|F (m) (X) - G (X)\| < Y)$

Proof

Step	Hyp	Ref	Expression
1		fnlimabslt.p	$⊢ Ⅎ m φ$
2		fnlimabslt.f	$⊢ \underline{Ⅎ} m F$
3		fnlimabslt.n	$⊢ \underline{Ⅎ} x F$
4		fnlimabslt.m	$⊢ φ \to M \in ℤ$
5		fnlimabslt.z	$⊢ Z = ℤ_{\geq M}$
6		fnlimabslt.b	$⊢ (φ \land m \in Z) \to F (m) : dom F (m) ⟶ ℝ$
7		fnlimabslt.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
8		fnlimabslt.g	$⊢ G = (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x))))$
9		fnlimabslt.x	$⊢ φ \to X \in D$
10		fnlimabslt.y	$⊢ φ \to Y \in ℝ^{+}$
11		eqid	$⊢ ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
12		nfcv	$⊢ \underline{Ⅎ} x Z$
13		nfcv	$⊢ \underline{Ⅎ} x ℤ_{\geq n}$
14		nfcv	$⊢ \underline{Ⅎ} x m$
15	3 14	nffv	$⊢ \underline{Ⅎ} x F (m)$
16	15	nfdm	$⊢ \underline{Ⅎ} x dom F (m)$
17	13 16	nfiin	$⊢ \underline{Ⅎ} x ⋂_{m \in ℤ_{\geq n}} dom F (m)$
18	12 17	nfiun	$⊢ \underline{Ⅎ} x ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
19		nfcv	$⊢ \underline{Ⅎ} y ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
20		nfv	$⊢ Ⅎ y (m \in Z ⟼ F (m) (x)) \in dom ⇝$
21		nfcv	$⊢ \underline{Ⅎ} x y$
22	15 21	nffv	$⊢ \underline{Ⅎ} x F (m) (y)$
23	12 22	nfmpt	$⊢ \underline{Ⅎ} x (m \in Z ⟼ F (m) (y))$
24		nfcv	$⊢ \underline{Ⅎ} x dom ⇝$
25	23 24	nfel	$⊢ Ⅎ x (m \in Z ⟼ F (m) (y)) \in dom ⇝$
26		fveq2	$⊢ x = y \to F (m) (x) = F (m) (y)$
27	26	mpteq2dv	$⊢ x = y \to (m \in Z ⟼ F (m) (x)) = (m \in Z ⟼ F (m) (y))$
28	27	eleq1d	$⊢ x = y \to ((m \in Z ⟼ F (m) (x)) \in dom ⇝ \leftrightarrow (m \in Z ⟼ F (m) (y)) \in dom ⇝)$
29	18 19 20 25 28	cbvrabw	$⊢ \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\} = \{y \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (y)) \in dom ⇝\}$
30		ssrab2	$⊢ \{y \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (y)) \in dom ⇝\} \subseteq ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
31	29 30	eqsstri	$⊢ \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\} \subseteq ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
32	7 31	eqsstri	$⊢ D \subseteq ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
33	32 9	sselid	$⊢ φ \to X \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
34	1 5 6 11 33	allbutfifvre	$⊢ φ \to \exists n \in Z \forall m \in ℤ_{\geq n} F (m) (X) \in ℝ$
35		nfv	$⊢ Ⅎ j φ$
36		nfcv	$⊢ \underline{Ⅎ} j (m \in Z ⟼ F (m) (X))$
37	3 7 8 9	fnlimcnv	$⊢ φ \to (m \in Z ⟼ F (m) (X)) ⇝ G (X)$
38		nfcv	$⊢ \underline{Ⅎ} l F (m) (X)$
39		nfcv	$⊢ \underline{Ⅎ} m l$
40	2 39	nffv	$⊢ \underline{Ⅎ} m F (l)$
41		nfcv	$⊢ \underline{Ⅎ} m X$
42	40 41	nffv	$⊢ \underline{Ⅎ} m F (l) (X)$
43		fveq2	$⊢ m = l \to F (m) = F (l)$
44	43	fveq1d	$⊢ m = l \to F (m) (X) = F (l) (X)$
45	38 42 44	cbvmpt	$⊢ (m \in Z ⟼ F (m) (X)) = (l \in Z ⟼ F (l) (X))$
46		fveq2	$⊢ l = j \to F (l) = F (j)$
47	46	fveq1d	$⊢ l = j \to F (l) (X) = F (j) (X)$
48		simpr	$⊢ (φ \land j \in Z) \to j \in Z$
49		fvexd	$⊢ (φ \land j \in Z) \to F (j) (X) \in V$
50	45 47 48 49	fvmptd3	$⊢ (φ \land j \in Z) \to (m \in Z ⟼ F (m) (X)) (j) = F (j) (X)$
51	35 36 5 4 37 50 10	climd	$⊢ φ \to \exists n \in Z \forall j \in ℤ_{\geq n} (F (j) (X) \in ℂ \land \|F (j) (X) - G (X)\| < Y)$
52		nfv	$⊢ Ⅎ j (F (m) (X) \in ℂ \land \|F (m) (X) - G (X)\| < Y)$
53		nfcv	$⊢ \underline{Ⅎ} m j$
54	2 53	nffv	$⊢ \underline{Ⅎ} m F (j)$
55	54 41	nffv	$⊢ \underline{Ⅎ} m F (j) (X)$
56		nfcv	$⊢ \underline{Ⅎ} m ℂ$
57	55 56	nfel	$⊢ Ⅎ m F (j) (X) \in ℂ$
58		nfcv	$⊢ \underline{Ⅎ} m abs$
59		nfcv	$⊢ \underline{Ⅎ} m -$
60		nfmpt1	$⊢ \underline{Ⅎ} m (m \in Z ⟼ F (m) (x))$
61		nfcv	$⊢ \underline{Ⅎ} m dom ⇝$
62	60 61	nfel	$⊢ Ⅎ m (m \in Z ⟼ F (m) (x)) \in dom ⇝$
63		nfcv	$⊢ \underline{Ⅎ} m Z$
64		nfii1	$⊢ \underline{Ⅎ} m ⋂_{m \in ℤ_{\geq n}} dom F (m)$
65	63 64	nfiun	$⊢ \underline{Ⅎ} m ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
66	62 65	nfrabw	$⊢ \underline{Ⅎ} m \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
67	7 66	nfcxfr	$⊢ \underline{Ⅎ} m D$
68		nfcv	$⊢ \underline{Ⅎ} m ⇝$
69	68 60	nffv	$⊢ \underline{Ⅎ} m ⇝ ((m \in Z ⟼ F (m) (x)))$
70	67 69	nfmpt	$⊢ \underline{Ⅎ} m (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x))))$
71	8 70	nfcxfr	$⊢ \underline{Ⅎ} m G$
72	71 41	nffv	$⊢ \underline{Ⅎ} m G (X)$
73	55 59 72	nfov	$⊢ \underline{Ⅎ} m (F (j) (X) - G (X))$
74	58 73	nffv	$⊢ \underline{Ⅎ} m \|F (j) (X) - G (X)\|$
75		nfcv	$⊢ \underline{Ⅎ} m <$
76		nfcv	$⊢ \underline{Ⅎ} m Y$
77	74 75 76	nfbr	$⊢ Ⅎ m \|F (j) (X) - G (X)\| < Y$
78	57 77	nfan	$⊢ Ⅎ m (F (j) (X) \in ℂ \land \|F (j) (X) - G (X)\| < Y)$
79		fveq2	$⊢ m = j \to F (m) = F (j)$
80	79	fveq1d	$⊢ m = j \to F (m) (X) = F (j) (X)$
81	80	eleq1d	$⊢ m = j \to (F (m) (X) \in ℂ \leftrightarrow F (j) (X) \in ℂ)$
82	80	fvoveq1d	$⊢ m = j \to \|F (m) (X) - G (X)\| = \|F (j) (X) - G (X)\|$
83	82	breq1d	$⊢ m = j \to (\|F (m) (X) - G (X)\| < Y \leftrightarrow \|F (j) (X) - G (X)\| < Y)$
84	81 83	anbi12d	$⊢ m = j \to ((F (m) (X) \in ℂ \land \|F (m) (X) - G (X)\| < Y) \leftrightarrow (F (j) (X) \in ℂ \land \|F (j) (X) - G (X)\| < Y))$
85	52 78 84	cbvralw	$⊢ \forall m \in ℤ_{\geq n} (F (m) (X) \in ℂ \land \|F (m) (X) - G (X)\| < Y) \leftrightarrow \forall j \in ℤ_{\geq n} (F (j) (X) \in ℂ \land \|F (j) (X) - G (X)\| < Y)$
86	85	rexbii	$⊢ \exists n \in Z \forall m \in ℤ_{\geq n} (F (m) (X) \in ℂ \land \|F (m) (X) - G (X)\| < Y) \leftrightarrow \exists n \in Z \forall j \in ℤ_{\geq n} (F (j) (X) \in ℂ \land \|F (j) (X) - G (X)\| < Y)$
87	51 86	sylibr	$⊢ φ \to \exists n \in Z \forall m \in ℤ_{\geq n} (F (m) (X) \in ℂ \land \|F (m) (X) - G (X)\| < Y)$
88		nfv	$⊢ Ⅎ m n \in Z$
89	1 88	nfan	$⊢ Ⅎ m (φ \land n \in Z)$
90		simpr	$⊢ (F (m) (X) \in ℂ \land \|F (m) (X) - G (X)\| < Y) \to \|F (m) (X) - G (X)\| < Y$
91	90	a1i	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to ((F (m) (X) \in ℂ \land \|F (m) (X) - G (X)\| < Y) \to \|F (m) (X) - G (X)\| < Y)$
92	89 91	ralimdaa	$⊢ (φ \land n \in Z) \to (\forall m \in ℤ_{\geq n} (F (m) (X) \in ℂ \land \|F (m) (X) - G (X)\| < Y) \to \forall m \in ℤ_{\geq n} \|F (m) (X) - G (X)\| < Y)$
93	92	reximdva	$⊢ φ \to (\exists n \in Z \forall m \in ℤ_{\geq n} (F (m) (X) \in ℂ \land \|F (m) (X) - G (X)\| < Y) \to \exists n \in Z \forall m \in ℤ_{\geq n} \|F (m) (X) - G (X)\| < Y)$
94	87 93	mpd	$⊢ φ \to \exists n \in Z \forall m \in ℤ_{\geq n} \|F (m) (X) - G (X)\| < Y$
95	34 94	jca	$⊢ φ \to (\exists n \in Z \forall m \in ℤ_{\geq n} F (m) (X) \in ℝ \land \exists n \in Z \forall m \in ℤ_{\geq n} \|F (m) (X) - G (X)\| < Y)$
96	5	rexanuz2	$⊢ \exists n \in Z \forall m \in ℤ_{\geq n} (F (m) (X) \in ℝ \land \|F (m) (X) - G (X)\| < Y) \leftrightarrow (\exists n \in Z \forall m \in ℤ_{\geq n} F (m) (X) \in ℝ \land \exists n \in Z \forall m \in ℤ_{\geq n} \|F (m) (X) - G (X)\| < Y)$
97	95 96	sylibr	$⊢ φ \to \exists n \in Z \forall m \in ℤ_{\geq n} (F (m) (X) \in ℝ \land \|F (m) (X) - G (X)\| < Y)$

Metamath Proof Explorer

Theorem fnlimabslt

Proof