smflimlem4

Description: Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of Fremlin1 p. 38 . This lemma proves one-side of the double inclusion for the proof that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by D . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smflimlem4.1	$⊢ φ \to M \in ℤ$
	smflimlem4.2	$⊢ Z = ℤ_{\geq M}$
	smflimlem4.3	$⊢ φ \to S \in SAlg$
	smflimlem4.4	$⊢ φ \to F : Z ⟶ SMblFn (S)$
	smflimlem4.5	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
	smflimlem4.6	$⊢ G = (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x))))$
	smflimlem4.7	$⊢ φ \to A \in ℝ$
	smflimlem4.8	$⊢ P = (m \in Z, k \in ℕ ⟼ \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\})$
	smflimlem4.9	$⊢ H = (m \in Z, k \in ℕ ⟼ C (m P k))$
	smflimlem4.10	$⊢ I = ⋂_{k \in ℕ} ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k)$
	smflimlem4.11	$⊢ (φ \land r \in ran P) \to C (r) \in r$
Assertion	smflimlem4	$⊢ φ \to D \cap I \subseteq \{x \in D \| G (x) \leq A\}$

Proof

Step	Hyp	Ref	Expression
1		smflimlem4.1	$⊢ φ \to M \in ℤ$
2		smflimlem4.2	$⊢ Z = ℤ_{\geq M}$
3		smflimlem4.3	$⊢ φ \to S \in SAlg$
4		smflimlem4.4	$⊢ φ \to F : Z ⟶ SMblFn (S)$
5		smflimlem4.5	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
6		smflimlem4.6	$⊢ G = (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x))))$
7		smflimlem4.7	$⊢ φ \to A \in ℝ$
8		smflimlem4.8	$⊢ P = (m \in Z, k \in ℕ ⟼ \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\})$
9		smflimlem4.9	$⊢ H = (m \in Z, k \in ℕ ⟼ C (m P k))$
10		smflimlem4.10	$⊢ I = ⋂_{k \in ℕ} ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k)$
11		smflimlem4.11	$⊢ (φ \land r \in ran P) \to C (r) \in r$
12		inss1	$⊢ D \cap I \subseteq D$
13	12	a1i	$⊢ φ \to D \cap I \subseteq D$
14	13	sselda	$⊢ (φ \land x \in (D \cap I)) \to x \in D$
15	6	a1i	$⊢ φ \to G = (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x))))$
16		nfv	$⊢ Ⅎ m (φ \land x \in D)$
17		nfcv	$⊢ \underline{Ⅎ} m F$
18		nfcv	$⊢ \underline{Ⅎ} z F$
19	3	adantr	$⊢ (φ \land m \in Z) \to S \in SAlg$
20	4	ffvelrnda	$⊢ (φ \land m \in Z) \to F (m) \in SMblFn (S)$
21		eqid	$⊢ dom F (m) = dom F (m)$
22	19 20 21	smff	$⊢ (φ \land m \in Z) \to F (m) : dom F (m) ⟶ ℝ$
23	22	adantlr	$⊢ ((φ \land x \in D) \land m \in Z) \to F (m) : dom F (m) ⟶ ℝ$
24		fveq2	$⊢ x = z \to F (m) (x) = F (m) (z)$
25	24	mpteq2dv	$⊢ x = z \to (m \in Z ⟼ F (m) (x)) = (m \in Z ⟼ F (m) (z))$
26	25	eleq1d	$⊢ x = z \to ((m \in Z ⟼ F (m) (x)) \in dom ⇝ \leftrightarrow (m \in Z ⟼ F (m) (z)) \in dom ⇝)$
27	26	cbvrabv	$⊢ \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\} = \{z \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (z)) \in dom ⇝\}$
28	5 27	eqtri	$⊢ D = \{z \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (z)) \in dom ⇝\}$
29		simpr	$⊢ (φ \land x \in D) \to x \in D$
30	16 17 18 2 23 28 29	fnlimfvre	$⊢ (φ \land x \in D) \to ⇝ ((m \in Z ⟼ F (m) (x))) \in ℝ$
31	30	elexd	$⊢ (φ \land x \in D) \to ⇝ ((m \in Z ⟼ F (m) (x))) \in V$
32	15 31	fvmpt2d	$⊢ (φ \land x \in D) \to G (x) = ⇝ ((m \in Z ⟼ F (m) (x)))$
33	32 30	eqeltrd	$⊢ (φ \land x \in D) \to G (x) \in ℝ$
34	14 33	syldan	$⊢ (φ \land x \in (D \cap I)) \to G (x) \in ℝ$
35	34	adantr	$⊢ ((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \to G (x) \in ℝ$
36	7	adantr	$⊢ (φ \land y \in ℝ^{+}) \to A \in ℝ$
37		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
38	37	adantl	$⊢ (φ \land y \in ℝ^{+}) \to y \in ℝ$
39	36 38	readdcld	$⊢ (φ \land y \in ℝ^{+}) \to A + y \in ℝ$
40	39	adantlr	$⊢ ((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \to A + y \in ℝ$
41		nfv	$⊢ Ⅎ m ((φ \land x \in (D \cap I)) \land y \in ℝ^{+})$
42		rphalfcl	$⊢ y \in ℝ^{+} \to \frac{y}{2} \in ℝ^{+}$
43		rpgtrecnn	$⊢ \frac{y}{2} \in ℝ^{+} \to \exists k \in ℕ \frac{1}{k} < \frac{y}{2}$
44	42 43	syl	$⊢ y \in ℝ^{+} \to \exists k \in ℕ \frac{1}{k} < \frac{y}{2}$
45	44	adantl	$⊢ ((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \to \exists k \in ℕ \frac{1}{k} < \frac{y}{2}$
46	3	ad4antr	$⊢ ((((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land k \in ℕ) \land \frac{1}{k} < \frac{y}{2}) \to S \in SAlg$
47	20	adantlr	$⊢ ((φ \land x \in (D \cap I)) \land m \in Z) \to F (m) \in SMblFn (S)$
48	47	ad5ant15	$⊢ (((((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land k \in ℕ) \land \frac{1}{k} < \frac{y}{2}) \land m \in Z) \to F (m) \in SMblFn (S)$
49	7	adantr	$⊢ (φ \land x \in (D \cap I)) \to A \in ℝ$
50	49	ad3antrrr	$⊢ ((((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land k \in ℕ) \land \frac{1}{k} < \frac{y}{2}) \to A \in ℝ$
51		nfcv	$⊢ \underline{Ⅎ} k Z$
52		nfcv	$⊢ \underline{Ⅎ} j Z$
53		nfcv	$⊢ \underline{Ⅎ} j \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\}$
54		nfcv	$⊢ \underline{Ⅎ} k \{s \in S \| \{z \in dom F (m) \| F (m) (z) < A + (\frac{1}{j})\} = s \cap dom F (m)\}$
55	24	breq1d	$⊢ x = z \to (F (m) (x) < A + (\frac{1}{k}) \leftrightarrow F (m) (z) < A + (\frac{1}{k}))$
56	55	cbvrabv	$⊢ \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = \{z \in dom F (m) \| F (m) (z) < A + (\frac{1}{k})\}$
57	56	a1i	$⊢ k = j \to \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = \{z \in dom F (m) \| F (m) (z) < A + (\frac{1}{k})\}$
58		oveq2	$⊢ k = j \to \frac{1}{k} = \frac{1}{j}$
59	58	oveq2d	$⊢ k = j \to A + (\frac{1}{k}) = A + (\frac{1}{j})$
60	59	breq2d	$⊢ k = j \to (F (m) (z) < A + (\frac{1}{k}) \leftrightarrow F (m) (z) < A + (\frac{1}{j}))$
61	60	rabbidv	$⊢ k = j \to \{z \in dom F (m) \| F (m) (z) < A + (\frac{1}{k})\} = \{z \in dom F (m) \| F (m) (z) < A + (\frac{1}{j})\}$
62	57 61	eqtrd	$⊢ k = j \to \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = \{z \in dom F (m) \| F (m) (z) < A + (\frac{1}{j})\}$
63	62	eqeq1d	$⊢ k = j \to (\{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m) \leftrightarrow \{z \in dom F (m) \| F (m) (z) < A + (\frac{1}{j})\} = s \cap dom F (m))$
64	63	rabbidv	$⊢ k = j \to \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} = \{s \in S \| \{z \in dom F (m) \| F (m) (z) < A + (\frac{1}{j})\} = s \cap dom F (m)\}$
65	51 52 53 54 64	cbvmpo2	$⊢ (m \in Z, k \in ℕ ⟼ \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\}) = (m \in Z, j \in ℕ ⟼ \{s \in S \| \{z \in dom F (m) \| F (m) (z) < A + (\frac{1}{j})\} = s \cap dom F (m)\})$
66	8 65	eqtri	$⊢ P = (m \in Z, j \in ℕ ⟼ \{s \in S \| \{z \in dom F (m) \| F (m) (z) < A + (\frac{1}{j})\} = s \cap dom F (m)\})$
67		nfcv	$⊢ \underline{Ⅎ} j C (m P k)$
68		nfcv	$⊢ \underline{Ⅎ} k C (m P j)$
69		oveq2	$⊢ k = j \to m P k = m P j$
70	69	fveq2d	$⊢ k = j \to C (m P k) = C (m P j)$
71	51 52 67 68 70	cbvmpo2	$⊢ (m \in Z, k \in ℕ ⟼ C (m P k)) = (m \in Z, j \in ℕ ⟼ C (m P j))$
72	9 71	eqtri	$⊢ H = (m \in Z, j \in ℕ ⟼ C (m P j))$
73		simpll	$⊢ ((k = j \land n \in Z) \land m \in ℤ_{\geq n}) \to k = j$
74	73	oveq2d	$⊢ ((k = j \land n \in Z) \land m \in ℤ_{\geq n}) \to m H k = m H j$
75	74	iineq2dv	$⊢ (k = j \land n \in Z) \to ⋂_{m \in ℤ_{\geq n}} (m H k) = ⋂_{m \in ℤ_{\geq n}} (m H j)$
76	75	iuneq2dv	$⊢ k = j \to ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k) = ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H j)$
77	76	cbviinv	$⊢ ⋂_{k \in ℕ} ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k) = ⋂_{j \in ℕ} ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H j)$
78	10 77	eqtri	$⊢ I = ⋂_{j \in ℕ} ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H j)$
79	11	adantlr	$⊢ ((φ \land x \in (D \cap I)) \land r \in ran P) \to C (r) \in r$
80	79	ad5ant15	$⊢ (((((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land k \in ℕ) \land \frac{1}{k} < \frac{y}{2}) \land r \in ran P) \to C (r) \in r$
81		simp-4r	$⊢ ((((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land k \in ℕ) \land \frac{1}{k} < \frac{y}{2}) \to x \in (D \cap I)$
82		simplr	$⊢ ((((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land k \in ℕ) \land \frac{1}{k} < \frac{y}{2}) \to k \in ℕ$
83	42	ad3antlr	$⊢ ((((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land k \in ℕ) \land \frac{1}{k} < \frac{y}{2}) \to \frac{y}{2} \in ℝ^{+}$
84		simpr	$⊢ ((((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land k \in ℕ) \land \frac{1}{k} < \frac{y}{2}) \to \frac{1}{k} < \frac{y}{2}$
85	2 46 48 28 50 66 72 78 80 81 82 83 84	smflimlem3	$⊢ ((((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land k \in ℕ) \land \frac{1}{k} < \frac{y}{2}) \to \exists m \in Z \forall i \in ℤ_{\geq m} (x \in dom F (i) \land F (i) (x) < A + (\frac{y}{2}))$
86	85	rexlimdva2	$⊢ ((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \to (\exists k \in ℕ \frac{1}{k} < \frac{y}{2} \to \exists m \in Z \forall i \in ℤ_{\geq m} (x \in dom F (i) \land F (i) (x) < A + (\frac{y}{2})))$
87	45 86	mpd	$⊢ ((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \to \exists m \in Z \forall i \in ℤ_{\geq m} (x \in dom F (i) \land F (i) (x) < A + (\frac{y}{2}))$
88		nfv	$⊢ Ⅎ i ((φ \land x \in (D \cap I)) \land y \in ℝ^{+})$
89		nfcv	$⊢ \underline{Ⅎ} i F$
90		nfcv	$⊢ \underline{Ⅎ} x F$
91	1	ad2antrr	$⊢ ((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \to M \in ℤ$
92		eleq1w	$⊢ m = i \to (m \in Z \leftrightarrow i \in Z)$
93	92	anbi2d	$⊢ m = i \to ((φ \land m \in Z) \leftrightarrow (φ \land i \in Z))$
94		fveq2	$⊢ m = i \to F (m) = F (i)$
95	94	dmeqd	$⊢ m = i \to dom F (m) = dom F (i)$
96	94 95	feq12d	$⊢ m = i \to (F (m) : dom F (m) ⟶ ℝ \leftrightarrow F (i) : dom F (i) ⟶ ℝ)$
97	93 96	imbi12d	$⊢ m = i \to (((φ \land m \in Z) \to F (m) : dom F (m) ⟶ ℝ) \leftrightarrow ((φ \land i \in Z) \to F (i) : dom F (i) ⟶ ℝ))$
98	97 22	chvarvv	$⊢ (φ \land i \in Z) \to F (i) : dom F (i) ⟶ ℝ$
99	98	ad4ant14	$⊢ (((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land i \in Z) \to F (i) : dom F (i) ⟶ ℝ$
100		fveq2	$⊢ m = l \to F (m) = F (l)$
101	100	dmeqd	$⊢ m = l \to dom F (m) = dom F (l)$
102	101	cbviinv	$⊢ ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋂_{l \in ℤ_{\geq n}} dom F (l)$
103	102	a1i	$⊢ n \in Z \to ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋂_{l \in ℤ_{\geq n}} dom F (l)$
104	103	iuneq2i	$⊢ ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋃_{n \in Z} ⋂_{l \in ℤ_{\geq n}} dom F (l)$
105		fveq2	$⊢ n = m \to ℤ_{\geq n} = ℤ_{\geq m}$
106	105	iineq1d	$⊢ n = m \to ⋂_{l \in ℤ_{\geq n}} dom F (l) = ⋂_{l \in ℤ_{\geq m}} dom F (l)$
107		fveq2	$⊢ l = i \to F (l) = F (i)$
108	107	dmeqd	$⊢ l = i \to dom F (l) = dom F (i)$
109	108	cbviinv	$⊢ ⋂_{l \in ℤ_{\geq m}} dom F (l) = ⋂_{i \in ℤ_{\geq m}} dom F (i)$
110	109	a1i	$⊢ n = m \to ⋂_{l \in ℤ_{\geq m}} dom F (l) = ⋂_{i \in ℤ_{\geq m}} dom F (i)$
111	106 110	eqtrd	$⊢ n = m \to ⋂_{l \in ℤ_{\geq n}} dom F (l) = ⋂_{i \in ℤ_{\geq m}} dom F (i)$
112	111	cbviunv	$⊢ ⋃_{n \in Z} ⋂_{l \in ℤ_{\geq n}} dom F (l) = ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} dom F (i)$
113	104 112	eqtri	$⊢ ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} dom F (i)$
114	113	rabeqi	$⊢ \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\} = \{x \in ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} dom F (i) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
115		fveq2	$⊢ i = m \to F (i) = F (m)$
116	115	fveq1d	$⊢ i = m \to F (i) (x) = F (m) (x)$
117	116	cbvmptv	$⊢ (i \in Z ⟼ F (i) (x)) = (m \in Z ⟼ F (m) (x))$
118	117	eqcomi	$⊢ (m \in Z ⟼ F (m) (x)) = (i \in Z ⟼ F (i) (x))$
119	118	eleq1i	$⊢ (m \in Z ⟼ F (m) (x)) \in dom ⇝ \leftrightarrow (i \in Z ⟼ F (i) (x)) \in dom ⇝$
120	119	rabbii	$⊢ \{x \in ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} dom F (i) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\} = \{x \in ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} dom F (i) \| (i \in Z ⟼ F (i) (x)) \in dom ⇝\}$
121	5 114 120	3eqtri	$⊢ D = \{x \in ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} dom F (i) \| (i \in Z ⟼ F (i) (x)) \in dom ⇝\}$
122	118	fveq2i	$⊢ ⇝ ((m \in Z ⟼ F (m) (x))) = ⇝ ((i \in Z ⟼ F (i) (x)))$
123	122	mpteq2i	$⊢ (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x)))) = (x \in D ⟼ ⇝ ((i \in Z ⟼ F (i) (x))))$
124	6 123	eqtri	$⊢ G = (x \in D ⟼ ⇝ ((i \in Z ⟼ F (i) (x))))$
125	14	adantr	$⊢ ((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \to x \in D$
126	42	adantl	$⊢ ((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \to \frac{y}{2} \in ℝ^{+}$
127	88 89 90 91 2 99 121 124 125 126	fnlimabslt	$⊢ ((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \to \exists m \in Z \forall i \in ℤ_{\geq m} (F (i) (x) \in ℝ \land \|F (i) (x) - G (x)\| < \frac{y}{2})$
128	35	adantr	$⊢ (((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land F (i) (x) \in ℝ) \to G (x) \in ℝ$
129		simpr	$⊢ (((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land F (i) (x) \in ℝ) \to F (i) (x) \in ℝ$
130	128 129	resubcld	$⊢ (((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land F (i) (x) \in ℝ) \to G (x) - F (i) (x) \in ℝ$
131	130	adantrr	$⊢ (((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land (F (i) (x) \in ℝ \land \|F (i) (x) - G (x)\| < \frac{y}{2})) \to G (x) - F (i) (x) \in ℝ$
132	130	recnd	$⊢ (((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land F (i) (x) \in ℝ) \to G (x) - F (i) (x) \in ℂ$
133	132	abscld	$⊢ (((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land F (i) (x) \in ℝ) \to \|G (x) - F (i) (x)\| \in ℝ$
134	133	adantrr	$⊢ (((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land (F (i) (x) \in ℝ \land \|F (i) (x) - G (x)\| < \frac{y}{2})) \to \|G (x) - F (i) (x)\| \in ℝ$
135	37	rehalfcld	$⊢ y \in ℝ^{+} \to \frac{y}{2} \in ℝ$
136	135	ad2antlr	$⊢ (((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land (F (i) (x) \in ℝ \land \|F (i) (x) - G (x)\| < \frac{y}{2})) \to \frac{y}{2} \in ℝ$
137	131	leabsd	$⊢ (((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land (F (i) (x) \in ℝ \land \|F (i) (x) - G (x)\| < \frac{y}{2})) \to G (x) - F (i) (x) \leq \|G (x) - F (i) (x)\|$
138	34	recnd	$⊢ (φ \land x \in (D \cap I)) \to G (x) \in ℂ$
139	138	adantr	$⊢ ((φ \land x \in (D \cap I)) \land F (i) (x) \in ℝ) \to G (x) \in ℂ$
140		recn	$⊢ F (i) (x) \in ℝ \to F (i) (x) \in ℂ$
141	140	adantl	$⊢ ((φ \land x \in (D \cap I)) \land F (i) (x) \in ℝ) \to F (i) (x) \in ℂ$
142	139 141	abssubd	$⊢ ((φ \land x \in (D \cap I)) \land F (i) (x) \in ℝ) \to \|G (x) - F (i) (x)\| = \|F (i) (x) - G (x)\|$
143	142	adantrr	$⊢ ((φ \land x \in (D \cap I)) \land (F (i) (x) \in ℝ \land \|F (i) (x) - G (x)\| < \frac{y}{2})) \to \|G (x) - F (i) (x)\| = \|F (i) (x) - G (x)\|$
144		simprr	$⊢ ((φ \land x \in (D \cap I)) \land (F (i) (x) \in ℝ \land \|F (i) (x) - G (x)\| < \frac{y}{2})) \to \|F (i) (x) - G (x)\| < \frac{y}{2}$
145	143 144	eqbrtrd	$⊢ ((φ \land x \in (D \cap I)) \land (F (i) (x) \in ℝ \land \|F (i) (x) - G (x)\| < \frac{y}{2})) \to \|G (x) - F (i) (x)\| < \frac{y}{2}$
146	145	adantlr	$⊢ (((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land (F (i) (x) \in ℝ \land \|F (i) (x) - G (x)\| < \frac{y}{2})) \to \|G (x) - F (i) (x)\| < \frac{y}{2}$
147	131 134 136 137 146	lelttrd	$⊢ (((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land (F (i) (x) \in ℝ \land \|F (i) (x) - G (x)\| < \frac{y}{2})) \to G (x) - F (i) (x) < \frac{y}{2}$
148	35	adantr	$⊢ (((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land (F (i) (x) \in ℝ \land \|F (i) (x) - G (x)\| < \frac{y}{2})) \to G (x) \in ℝ$
149		simprl	$⊢ (((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land (F (i) (x) \in ℝ \land \|F (i) (x) - G (x)\| < \frac{y}{2})) \to F (i) (x) \in ℝ$
150	148 149 136	ltsubadd2d	$⊢ (((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land (F (i) (x) \in ℝ \land \|F (i) (x) - G (x)\| < \frac{y}{2})) \to (G (x) - F (i) (x) < \frac{y}{2} \leftrightarrow G (x) < F (i) (x) + (\frac{y}{2}))$
151	147 150	mpbid	$⊢ (((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land (F (i) (x) \in ℝ \land \|F (i) (x) - G (x)\| < \frac{y}{2})) \to G (x) < F (i) (x) + (\frac{y}{2})$
152	151	ex	$⊢ ((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \to ((F (i) (x) \in ℝ \land \|F (i) (x) - G (x)\| < \frac{y}{2}) \to G (x) < F (i) (x) + (\frac{y}{2}))$
153	152	ad2antrr	$⊢ ((((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land m \in Z) \land i \in ℤ_{\geq m}) \to ((F (i) (x) \in ℝ \land \|F (i) (x) - G (x)\| < \frac{y}{2}) \to G (x) < F (i) (x) + (\frac{y}{2}))$
154	153	ralimdva	$⊢ (((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land m \in Z) \to (\forall i \in ℤ_{\geq m} (F (i) (x) \in ℝ \land \|F (i) (x) - G (x)\| < \frac{y}{2}) \to \forall i \in ℤ_{\geq m} G (x) < F (i) (x) + (\frac{y}{2}))$
155	154	ex	$⊢ ((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \to (m \in Z \to (\forall i \in ℤ_{\geq m} (F (i) (x) \in ℝ \land \|F (i) (x) - G (x)\| < \frac{y}{2}) \to \forall i \in ℤ_{\geq m} G (x) < F (i) (x) + (\frac{y}{2})))$
156	41 155	reximdai	$⊢ ((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \to (\exists m \in Z \forall i \in ℤ_{\geq m} (F (i) (x) \in ℝ \land \|F (i) (x) - G (x)\| < \frac{y}{2}) \to \exists m \in Z \forall i \in ℤ_{\geq m} G (x) < F (i) (x) + (\frac{y}{2}))$
157	127 156	mpd	$⊢ ((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \to \exists m \in Z \forall i \in ℤ_{\geq m} G (x) < F (i) (x) + (\frac{y}{2})$
158	115	dmeqd	$⊢ i = m \to dom F (i) = dom F (m)$
159	158	eleq2d	$⊢ i = m \to (x \in dom F (i) \leftrightarrow x \in dom F (m))$
160	116	breq1d	$⊢ i = m \to (F (i) (x) < A + (\frac{y}{2}) \leftrightarrow F (m) (x) < A + (\frac{y}{2}))$
161	159 160	anbi12d	$⊢ i = m \to ((x \in dom F (i) \land F (i) (x) < A + (\frac{y}{2})) \leftrightarrow (x \in dom F (m) \land F (m) (x) < A + (\frac{y}{2})))$
162	116	oveq1d	$⊢ i = m \to F (i) (x) + (\frac{y}{2}) = F (m) (x) + (\frac{y}{2})$
163	162	breq2d	$⊢ i = m \to (G (x) < F (i) (x) + (\frac{y}{2}) \leftrightarrow G (x) < F (m) (x) + (\frac{y}{2}))$
164	41 2 87 157 161 163	rexanuz3	$⊢ ((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \to \exists m \in Z ((x \in dom F (m) \land F (m) (x) < A + (\frac{y}{2})) \land G (x) < F (m) (x) + (\frac{y}{2}))$
165		df-3an	$⊢ (x \in dom F (m) \land F (m) (x) < A + (\frac{y}{2}) \land G (x) < F (m) (x) + (\frac{y}{2})) \leftrightarrow ((x \in dom F (m) \land F (m) (x) < A + (\frac{y}{2})) \land G (x) < F (m) (x) + (\frac{y}{2}))$
166		3ancomb	$⊢ (x \in dom F (m) \land F (m) (x) < A + (\frac{y}{2}) \land G (x) < F (m) (x) + (\frac{y}{2})) \leftrightarrow (x \in dom F (m) \land G (x) < F (m) (x) + (\frac{y}{2}) \land F (m) (x) < A + (\frac{y}{2}))$
167	165 166	bitr3i	$⊢ ((x \in dom F (m) \land F (m) (x) < A + (\frac{y}{2})) \land G (x) < F (m) (x) + (\frac{y}{2})) \leftrightarrow (x \in dom F (m) \land G (x) < F (m) (x) + (\frac{y}{2}) \land F (m) (x) < A + (\frac{y}{2}))$
168	167	rexbii	$⊢ \exists m \in Z ((x \in dom F (m) \land F (m) (x) < A + (\frac{y}{2})) \land G (x) < F (m) (x) + (\frac{y}{2})) \leftrightarrow \exists m \in Z (x \in dom F (m) \land G (x) < F (m) (x) + (\frac{y}{2}) \land F (m) (x) < A + (\frac{y}{2}))$
169	164 168	sylib	$⊢ ((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \to \exists m \in Z (x \in dom F (m) \land G (x) < F (m) (x) + (\frac{y}{2}) \land F (m) (x) < A + (\frac{y}{2}))$
170	35	ad2antrr	$⊢ ((((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land m \in Z) \land (x \in dom F (m) \land G (x) < F (m) (x) + (\frac{y}{2}) \land F (m) (x) < A + (\frac{y}{2}))) \to G (x) \in ℝ$
171	22	3adant3	$⊢ (φ \land m \in Z \land x \in dom F (m)) \to F (m) : dom F (m) ⟶ ℝ$
172		simp3	$⊢ (φ \land m \in Z \land x \in dom F (m)) \to x \in dom F (m)$
173	171 172	ffvelrnd	$⊢ (φ \land m \in Z \land x \in dom F (m)) \to F (m) (x) \in ℝ$
174	173	ad4ant134	$⊢ (((φ \land y \in ℝ^{+}) \land m \in Z) \land x \in dom F (m)) \to F (m) (x) \in ℝ$
175		simpllr	$⊢ (((φ \land y \in ℝ^{+}) \land m \in Z) \land x \in dom F (m)) \to y \in ℝ^{+}$
176	175 135	syl	$⊢ (((φ \land y \in ℝ^{+}) \land m \in Z) \land x \in dom F (m)) \to \frac{y}{2} \in ℝ$
177	174 176	readdcld	$⊢ (((φ \land y \in ℝ^{+}) \land m \in Z) \land x \in dom F (m)) \to F (m) (x) + (\frac{y}{2}) \in ℝ$
178	177	adantl3r	$⊢ ((((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land m \in Z) \land x \in dom F (m)) \to F (m) (x) + (\frac{y}{2}) \in ℝ$
179	178	3ad2antr1	$⊢ ((((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land m \in Z) \land (x \in dom F (m) \land G (x) < F (m) (x) + (\frac{y}{2}) \land F (m) (x) < A + (\frac{y}{2}))) \to F (m) (x) + (\frac{y}{2}) \in ℝ$
180		rehalfcl	$⊢ y \in ℝ \to \frac{y}{2} \in ℝ$
181	38 180	syl	$⊢ (φ \land y \in ℝ^{+}) \to \frac{y}{2} \in ℝ$
182	36 181	jca	$⊢ (φ \land y \in ℝ^{+}) \to (A \in ℝ \land \frac{y}{2} \in ℝ)$
183		readdcl	$⊢ (A \in ℝ \land \frac{y}{2} \in ℝ) \to A + (\frac{y}{2}) \in ℝ$
184	182 183	syl	$⊢ (φ \land y \in ℝ^{+}) \to A + (\frac{y}{2}) \in ℝ$
185	184 181	readdcld	$⊢ (φ \land y \in ℝ^{+}) \to A + (\frac{y}{2}) + (\frac{y}{2}) \in ℝ$
186	185	ad5ant13	$⊢ ((((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land m \in Z) \land (x \in dom F (m) \land G (x) < F (m) (x) + (\frac{y}{2}) \land F (m) (x) < A + (\frac{y}{2}))) \to A + (\frac{y}{2}) + (\frac{y}{2}) \in ℝ$
187		simpr2	$⊢ ((((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land m \in Z) \land (x \in dom F (m) \land G (x) < F (m) (x) + (\frac{y}{2}) \land F (m) (x) < A + (\frac{y}{2}))) \to G (x) < F (m) (x) + (\frac{y}{2})$
188	174	adantrr	$⊢ (((φ \land y \in ℝ^{+}) \land m \in Z) \land (x \in dom F (m) \land F (m) (x) < A + (\frac{y}{2}))) \to F (m) (x) \in ℝ$
189	184	ad2antrr	$⊢ (((φ \land y \in ℝ^{+}) \land m \in Z) \land (x \in dom F (m) \land F (m) (x) < A + (\frac{y}{2}))) \to A + (\frac{y}{2}) \in ℝ$
190	176	adantrr	$⊢ (((φ \land y \in ℝ^{+}) \land m \in Z) \land (x \in dom F (m) \land F (m) (x) < A + (\frac{y}{2}))) \to \frac{y}{2} \in ℝ$
191		simprr	$⊢ (((φ \land y \in ℝ^{+}) \land m \in Z) \land (x \in dom F (m) \land F (m) (x) < A + (\frac{y}{2}))) \to F (m) (x) < A + (\frac{y}{2})$
192	188 189 190 191	ltadd1dd	$⊢ (((φ \land y \in ℝ^{+}) \land m \in Z) \land (x \in dom F (m) \land F (m) (x) < A + (\frac{y}{2}))) \to F (m) (x) + (\frac{y}{2}) < A + (\frac{y}{2}) + (\frac{y}{2})$
193	192	adantl3r	$⊢ ((((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land m \in Z) \land (x \in dom F (m) \land F (m) (x) < A + (\frac{y}{2}))) \to F (m) (x) + (\frac{y}{2}) < A + (\frac{y}{2}) + (\frac{y}{2})$
194	193	3adantr2	$⊢ ((((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land m \in Z) \land (x \in dom F (m) \land G (x) < F (m) (x) + (\frac{y}{2}) \land F (m) (x) < A + (\frac{y}{2}))) \to F (m) (x) + (\frac{y}{2}) < A + (\frac{y}{2}) + (\frac{y}{2})$
195	170 179 186 187 194	lttrd	$⊢ ((((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land m \in Z) \land (x \in dom F (m) \land G (x) < F (m) (x) + (\frac{y}{2}) \land F (m) (x) < A + (\frac{y}{2}))) \to G (x) < A + (\frac{y}{2}) + (\frac{y}{2})$
196	36	recnd	$⊢ (φ \land y \in ℝ^{+}) \to A \in ℂ$
197	181	recnd	$⊢ (φ \land y \in ℝ^{+}) \to \frac{y}{2} \in ℂ$
198	196 197 197	addassd	$⊢ (φ \land y \in ℝ^{+}) \to A + (\frac{y}{2}) + (\frac{y}{2}) = A + (\frac{y}{2}) + (\frac{y}{2})$
199	37	recnd	$⊢ y \in ℝ^{+} \to y \in ℂ$
200		2halves	$⊢ y \in ℂ \to (\frac{y}{2}) + (\frac{y}{2}) = y$
201	199 200	syl	$⊢ y \in ℝ^{+} \to (\frac{y}{2}) + (\frac{y}{2}) = y$
202	201	oveq2d	$⊢ y \in ℝ^{+} \to A + (\frac{y}{2}) + (\frac{y}{2}) = A + y$
203	202	adantl	$⊢ (φ \land y \in ℝ^{+}) \to A + (\frac{y}{2}) + (\frac{y}{2}) = A + y$
204	198 203	eqtrd	$⊢ (φ \land y \in ℝ^{+}) \to A + (\frac{y}{2}) + (\frac{y}{2}) = A + y$
205	204	ad5ant13	$⊢ ((((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land m \in Z) \land (x \in dom F (m) \land G (x) < F (m) (x) + (\frac{y}{2}) \land F (m) (x) < A + (\frac{y}{2}))) \to A + (\frac{y}{2}) + (\frac{y}{2}) = A + y$
206	195 205	breqtrd	$⊢ ((((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \land m \in Z) \land (x \in dom F (m) \land G (x) < F (m) (x) + (\frac{y}{2}) \land F (m) (x) < A + (\frac{y}{2}))) \to G (x) < A + y$
207	206	rexlimdva2	$⊢ ((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \to (\exists m \in Z (x \in dom F (m) \land G (x) < F (m) (x) + (\frac{y}{2}) \land F (m) (x) < A + (\frac{y}{2})) \to G (x) < A + y)$
208	169 207	mpd	$⊢ ((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \to G (x) < A + y$
209	35 40 208	ltled	$⊢ ((φ \land x \in (D \cap I)) \land y \in ℝ^{+}) \to G (x) \leq A + y$
210	209	ralrimiva	$⊢ (φ \land x \in (D \cap I)) \to \forall y \in ℝ^{+} G (x) \leq A + y$
211		alrple	$⊢ (G (x) \in ℝ \land A \in ℝ) \to (G (x) \leq A \leftrightarrow \forall y \in ℝ^{+} G (x) \leq A + y)$
212	34 49 211	syl2anc	$⊢ (φ \land x \in (D \cap I)) \to (G (x) \leq A \leftrightarrow \forall y \in ℝ^{+} G (x) \leq A + y)$
213	210 212	mpbird	$⊢ (φ \land x \in (D \cap I)) \to G (x) \leq A$
214	13 213	ssrabdv	$⊢ φ \to D \cap I \subseteq \{x \in D \| G (x) \leq A\}$

Metamath Proof Explorer

Theorem smflimlem4

Proof