hoidmvlelem1

Description: The supremum of U belongs to U . Step (c) in the proof of Lemma 115B of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	hoidmvlelem1.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
	hoidmvlelem1.x	$⊢ φ \to X \in Fin$
	hoidmvlelem1.y	$⊢ φ \to Y \subseteq X$
	hoidmvlelem1.z	$⊢ φ \to Z \in (X ∖ Y)$
	hoidmvlelem1.w	$⊢ W = Y \cup \{Z\}$
	hoidmvlelem1.a	$⊢ φ \to A : W ⟶ ℝ$
	hoidmvlelem1.b	$⊢ φ \to B : W ⟶ ℝ$
	hoidmvlelem1.c	$⊢ φ \to C : ℕ ⟶ ℝ^{W}$
	hoidmvlelem1.d	$⊢ φ \to D : ℕ ⟶ ℝ^{W}$
	hoidmvlelem1.r	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ$
	hoidmvlelem1.h	$⊢ H = (x \in ℝ ⟼ (c \in (ℝ^{W}) ⟼ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x)))))$
	hoidmvlelem1.g	$⊢ G = ({A ↾}_{Y}) L (Y) ({B ↾}_{Y})$
	hoidmvlelem1.e	$⊢ φ \to E \in ℝ^{+}$
	hoidmvlelem1.u	$⊢ U = \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\}$
	hoidmvlelem1.s	$⊢ S = sup (U ℝ <)$
	hoidmvlelem1.ab	$⊢ φ \to A (Z) < B (Z)$
Assertion	hoidmvlelem1	$⊢ φ \to S \in U$

Proof

Step	Hyp	Ref	Expression
1		hoidmvlelem1.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
2		hoidmvlelem1.x	$⊢ φ \to X \in Fin$
3		hoidmvlelem1.y	$⊢ φ \to Y \subseteq X$
4		hoidmvlelem1.z	$⊢ φ \to Z \in (X ∖ Y)$
5		hoidmvlelem1.w	$⊢ W = Y \cup \{Z\}$
6		hoidmvlelem1.a	$⊢ φ \to A : W ⟶ ℝ$
7		hoidmvlelem1.b	$⊢ φ \to B : W ⟶ ℝ$
8		hoidmvlelem1.c	$⊢ φ \to C : ℕ ⟶ ℝ^{W}$
9		hoidmvlelem1.d	$⊢ φ \to D : ℕ ⟶ ℝ^{W}$
10		hoidmvlelem1.r	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ$
11		hoidmvlelem1.h	$⊢ H = (x \in ℝ ⟼ (c \in (ℝ^{W}) ⟼ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x)))))$
12		hoidmvlelem1.g	$⊢ G = ({A ↾}_{Y}) L (Y) ({B ↾}_{Y})$
13		hoidmvlelem1.e	$⊢ φ \to E \in ℝ^{+}$
14		hoidmvlelem1.u	$⊢ U = \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\}$
15		hoidmvlelem1.s	$⊢ S = sup (U ℝ <)$
16		hoidmvlelem1.ab	$⊢ φ \to A (Z) < B (Z)$
17	15	a1i	$⊢ φ \to S = sup (U ℝ <)$
18		snidg	$⊢ Z \in (X ∖ Y) \to Z \in \{Z\}$
19	4 18	syl	$⊢ φ \to Z \in \{Z\}$
20		elun2	$⊢ Z \in \{Z\} \to Z \in (Y \cup \{Z\})$
21	19 20	syl	$⊢ φ \to Z \in (Y \cup \{Z\})$
22	21 5	eleqtrrdi	$⊢ φ \to Z \in W$
23	6 22	ffvelrnd	$⊢ φ \to A (Z) \in ℝ$
24	7 22	ffvelrnd	$⊢ φ \to B (Z) \in ℝ$
25		ssrab2	$⊢ \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\} \subseteq [A (Z), B (Z)]$
26	14 25	eqsstri	$⊢ U \subseteq [A (Z), B (Z)]$
27	26	a1i	$⊢ φ \to U \subseteq [A (Z), B (Z)]$
28	23	leidd	$⊢ φ \to A (Z) \leq A (Z)$
29	23 24 16	ltled	$⊢ φ \to A (Z) \leq B (Z)$
30	23 24 23 28 29	eliccd	$⊢ φ \to A (Z) \in [A (Z), B (Z)]$
31	23	recnd	$⊢ φ \to A (Z) \in ℂ$
32	31	subidd	$⊢ φ \to A (Z) - A (Z) = 0$
33	32	oveq2d	$⊢ φ \to G (A (Z) - A (Z)) = G \cdot 0$
34		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
35	2 3	ssfid	$⊢ φ \to Y \in Fin$
36		ssun1	$⊢ Y \subseteq Y \cup \{Z\}$
37	36 5	sseqtrri	$⊢ Y \subseteq W$
38	37	a1i	$⊢ φ \to Y \subseteq W$
39	6 38	fssresd	$⊢ φ \to ({A ↾}_{Y}) : Y ⟶ ℝ$
40	7 38	fssresd	$⊢ φ \to ({B ↾}_{Y}) : Y ⟶ ℝ$
41	1 35 39 40	hoidmvcl	$⊢ φ \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \in [0, +∞)$
42	12 41	eqeltrid	$⊢ φ \to G \in [0, +∞)$
43	34 42	sseldi	$⊢ φ \to G \in ℝ$
44	43	recnd	$⊢ φ \to G \in ℂ$
45	44	mul01d	$⊢ φ \to G \cdot 0 = 0$
46	33 45	eqtrd	$⊢ φ \to G (A (Z) - A (Z)) = 0$
47		1red	$⊢ φ \to 1 \in ℝ$
48	13	rpred	$⊢ φ \to E \in ℝ$
49	47 48	readdcld	$⊢ φ \to 1 + E \in ℝ$
50		0red	$⊢ φ \to 0 \in ℝ$
51		0lt1	$⊢ 0 < 1$
52	51	a1i	$⊢ φ \to 0 < 1$
53	47 13	ltaddrpd	$⊢ φ \to 1 < 1 + E$
54	50 47 49 52 53	lttrd	$⊢ φ \to 0 < 1 + E$
55	50 49 54	ltled	$⊢ φ \to 0 \leq 1 + E$
56		nnex	$⊢ ℕ \in V$
57	56	a1i	$⊢ φ \to ℕ \in V$
58		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
59		snfi	$⊢ \{Z\} \in Fin$
60	59	a1i	$⊢ φ \to \{Z\} \in Fin$
61		unfi	$⊢ (Y \in Fin \land \{Z\} \in Fin) \to Y \cup \{Z\} \in Fin$
62	35 60 61	syl2anc	$⊢ φ \to Y \cup \{Z\} \in Fin$
63	5 62	eqeltrid	$⊢ φ \to W \in Fin$
64	63	adantr	$⊢ (φ \land j \in ℕ) \to W \in Fin$
65	8	ffvelrnda	$⊢ (φ \land j \in ℕ) \to C (j) \in (ℝ^{W})$
66		elmapi	$⊢ C (j) \in (ℝ^{W}) \to C (j) : W ⟶ ℝ$
67	65 66	syl	$⊢ (φ \land j \in ℕ) \to C (j) : W ⟶ ℝ$
68		eleq1w	$⊢ j = h \to (j \in Y \leftrightarrow h \in Y)$
69		fveq2	$⊢ j = h \to c (j) = c (h)$
70	69	breq1d	$⊢ j = h \to (c (j) \leq x \leftrightarrow c (h) \leq x)$
71	70 69	ifbieq1d	$⊢ j = h \to if (c (j) \leq x, c (j), x) = if (c (h) \leq x, c (h), x)$
72	68 69 71	ifbieq12d	$⊢ j = h \to if (j \in Y, c (j), if (c (j) \leq x, c (j), x)) = if (h \in Y, c (h), if (c (h) \leq x, c (h), x))$
73	72	cbvmptv	$⊢ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x))) = (h \in W ⟼ if (h \in Y, c (h), if (c (h) \leq x, c (h), x)))$
74	73	mpteq2i	$⊢ (c \in (ℝ^{W}) ⟼ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x)))) = (c \in (ℝ^{W}) ⟼ (h \in W ⟼ if (h \in Y, c (h), if (c (h) \leq x, c (h), x))))$
75	74	mpteq2i	$⊢ (x \in ℝ ⟼ (c \in (ℝ^{W}) ⟼ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x))))) = (x \in ℝ ⟼ (c \in (ℝ^{W}) ⟼ (h \in W ⟼ if (h \in Y, c (h), if (c (h) \leq x, c (h), x)))))$
76	11 75	eqtri	$⊢ H = (x \in ℝ ⟼ (c \in (ℝ^{W}) ⟼ (h \in W ⟼ if (h \in Y, c (h), if (c (h) \leq x, c (h), x)))))$
77	23	adantr	$⊢ (φ \land j \in ℕ) \to A (Z) \in ℝ$
78	9	ffvelrnda	$⊢ (φ \land j \in ℕ) \to D (j) \in (ℝ^{W})$
79		elmapi	$⊢ D (j) \in (ℝ^{W}) \to D (j) : W ⟶ ℝ$
80	78 79	syl	$⊢ (φ \land j \in ℕ) \to D (j) : W ⟶ ℝ$
81	76 77 64 80	hsphoif	$⊢ (φ \land j \in ℕ) \to H (A (Z)) (D (j)) : W ⟶ ℝ$
82	1 64 67 81	hoidmvcl	$⊢ (φ \land j \in ℕ) \to C (j) L (W) H (A (Z)) (D (j)) \in [0, +∞)$
83	58 82	sseldi	$⊢ (φ \land j \in ℕ) \to C (j) L (W) H (A (Z)) (D (j)) \in [0, +∞]$
84	83	fmpttd	$⊢ φ \to (j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j))) : ℕ ⟶ [0, +∞]$
85	57 84	sge0cl	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j)))) \in [0, +∞]$
86	57 84	sge0xrcl	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j)))) \in ℝ^{*}$
87		pnfxr	$⊢ +∞ \in ℝ^{*}$
88	87	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
89	10	rexrd	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ^{*}$
90		nfv	$⊢ Ⅎ j φ$
91	1 64 67 80	hoidmvcl	$⊢ (φ \land j \in ℕ) \to C (j) L (W) D (j) \in [0, +∞)$
92	58 91	sseldi	$⊢ (φ \land j \in ℕ) \to C (j) L (W) D (j) \in [0, +∞]$
93	4	eldifbd	$⊢ φ \to \neg Z \in Y$
94	22 93	eldifd	$⊢ φ \to Z \in (W ∖ Y)$
95	94	adantr	$⊢ (φ \land j \in ℕ) \to Z \in (W ∖ Y)$
96	1 64 95 5 77 76 67 80	hsphoidmvle	$⊢ (φ \land j \in ℕ) \to C (j) L (W) H (A (Z)) (D (j)) \leq C (j) L (W) D (j)$
97	90 57 83 92 96	sge0lempt	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j)))) \leq sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
98	10	ltpnfd	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) < +∞$
99	86 89 88 97 98	xrlelttrd	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j)))) < +∞$
100	86 88 99	xrltned	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j)))) \neq +∞$
101		ge0xrre	$⊢ (sum^((j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j)))) \in [0, +∞] \land sum^((j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j)))) \neq +∞) \to sum^((j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j)))) \in ℝ$
102	85 100 101	syl2anc	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j)))) \in ℝ$
103	57 84	sge0ge0	$⊢ φ \to 0 \leq sum^((j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j))))$
104		mulge0	$⊢ ((1 + E \in ℝ \land 0 \leq 1 + E) \land (sum^((j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j)))) \in ℝ \land 0 \leq sum^((j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j)))))) \to 0 \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j))))$
105	49 55 102 103 104	syl22anc	$⊢ φ \to 0 \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j))))$
106	46 105	eqbrtrd	$⊢ φ \to G (A (Z) - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j))))$
107	30 106	jca	$⊢ φ \to (A (Z) \in [A (Z), B (Z)] \land G (A (Z) - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j)))))$
108		oveq1	$⊢ z = A (Z) \to z - A (Z) = A (Z) - A (Z)$
109	108	oveq2d	$⊢ z = A (Z) \to G (z - A (Z)) = G (A (Z) - A (Z))$
110		fveq2	$⊢ z = A (Z) \to H (z) = H (A (Z))$
111	110	fveq1d	$⊢ z = A (Z) \to H (z) (D (j)) = H (A (Z)) (D (j))$
112	111	oveq2d	$⊢ z = A (Z) \to C (j) L (W) H (z) (D (j)) = C (j) L (W) H (A (Z)) (D (j))$
113	112	mpteq2dv	$⊢ z = A (Z) \to (j \in ℕ ⟼ C (j) L (W) H (z) (D (j))) = (j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j)))$
114	113	fveq2d	$⊢ z = A (Z) \to sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j)))) = sum^((j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j))))$
115	114	oveq2d	$⊢ z = A (Z) \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j)))) = (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j))))$
116	109 115	breq12d	$⊢ z = A (Z) \to (G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j)))) \leftrightarrow G (A (Z) - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j)))))$
117	116	elrab	$⊢ A (Z) \in \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\} \leftrightarrow (A (Z) \in [A (Z), B (Z)] \land G (A (Z) - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (A (Z)) (D (j)))))$
118	107 117	sylibr	$⊢ φ \to A (Z) \in \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\}$
119	118 14	eleqtrrdi	$⊢ φ \to A (Z) \in U$
120		ne0i	$⊢ A (Z) \in U \to U \neq \emptyset$
121	119 120	syl	$⊢ φ \to U \neq \emptyset$
122	23 24 27 121	supicc	$⊢ φ \to sup (U ℝ <) \in [A (Z), B (Z)]$
123	17 122	eqeltrd	$⊢ φ \to S \in [A (Z), B (Z)]$
124	17	oveq1d	$⊢ φ \to S - A (Z) = sup (U ℝ <) - A (Z)$
125	124	oveq2d	$⊢ φ \to G (S - A (Z)) = G (sup (U ℝ <) - A (Z))$
126	23 24	iccssred	$⊢ φ \to [A (Z), B (Z)] \subseteq ℝ$
127	27 126	sstrd	$⊢ φ \to U \subseteq ℝ$
128	23 24	jca	$⊢ φ \to (A (Z) \in ℝ \land B (Z) \in ℝ)$
129		iccsupr	$⊢ ((A (Z) \in ℝ \land B (Z) \in ℝ) \land U \subseteq [A (Z), B (Z)] \land A (Z) \in U) \to (U \subseteq ℝ \land U \neq \emptyset \land \exists y \in ℝ \forall z \in U z \leq y)$
130	128 27 119 129	syl3anc	$⊢ φ \to (U \subseteq ℝ \land U \neq \emptyset \land \exists y \in ℝ \forall z \in U z \leq y)$
131	130	simp3d	$⊢ φ \to \exists y \in ℝ \forall z \in U z \leq y$
132		eqid	$⊢ \{w \| \exists u \in U w = u - A (Z)\} = \{w \| \exists u \in U w = u - A (Z)\}$
133	127 121 131 23 132	supsubc	$⊢ φ \to sup (U ℝ <) - A (Z) = sup (\{w \| \exists u \in U w = u - A (Z)\} ℝ <)$
134	133	oveq2d	$⊢ φ \to G (sup (U ℝ <) - A (Z)) = G sup (\{w \| \exists u \in U w = u - A (Z)\} ℝ <)$
135	50	rexrd	$⊢ φ \to 0 \in ℝ^{*}$
136		icogelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land G \in [0, +∞)) \to 0 \leq G$
137	135 88 42 136	syl3anc	$⊢ φ \to 0 \leq G$
138		vex	$⊢ r \in V$
139		eqeq1	$⊢ w = r \to (w = u - A (Z) \leftrightarrow r = u - A (Z))$
140	139	rexbidv	$⊢ w = r \to (\exists u \in U w = u - A (Z) \leftrightarrow \exists u \in U r = u - A (Z))$
141	138 140	elab	$⊢ r \in \{w \| \exists u \in U w = u - A (Z)\} \leftrightarrow \exists u \in U r = u - A (Z)$
142	141	biimpi	$⊢ r \in \{w \| \exists u \in U w = u - A (Z)\} \to \exists u \in U r = u - A (Z)$
143	142	adantl	$⊢ (φ \land r \in \{w \| \exists u \in U w = u - A (Z)\}) \to \exists u \in U r = u - A (Z)$
144		nfv	$⊢ Ⅎ u φ$
145		nfcv	$⊢ \underline{Ⅎ} u r$
146		nfre1	$⊢ Ⅎ u \exists u \in U w = u - A (Z)$
147	146	nfab	$⊢ \underline{Ⅎ} u \{w \| \exists u \in U w = u - A (Z)\}$
148	145 147	nfel	$⊢ Ⅎ u r \in \{w \| \exists u \in U w = u - A (Z)\}$
149	144 148	nfan	$⊢ Ⅎ u (φ \land r \in \{w \| \exists u \in U w = u - A (Z)\})$
150		nfv	$⊢ Ⅎ u 0 \leq r$
151	23	rexrd	$⊢ φ \to A (Z) \in ℝ^{*}$
152	151	adantr	$⊢ (φ \land u \in U) \to A (Z) \in ℝ^{*}$
153	24	rexrd	$⊢ φ \to B (Z) \in ℝ^{*}$
154	153	adantr	$⊢ (φ \land u \in U) \to B (Z) \in ℝ^{*}$
155	27	sselda	$⊢ (φ \land u \in U) \to u \in [A (Z), B (Z)]$
156		iccgelb	$⊢ (A (Z) \in ℝ^{} \land B (Z) \in ℝ^{} \land u \in [A (Z), B (Z)]) \to A (Z) \leq u$
157	152 154 155 156	syl3anc	$⊢ (φ \land u \in U) \to A (Z) \leq u$
158	127	sselda	$⊢ (φ \land u \in U) \to u \in ℝ$
159	23	adantr	$⊢ (φ \land u \in U) \to A (Z) \in ℝ$
160	158 159	subge0d	$⊢ (φ \land u \in U) \to (0 \leq u - A (Z) \leftrightarrow A (Z) \leq u)$
161	157 160	mpbird	$⊢ (φ \land u \in U) \to 0 \leq u - A (Z)$
162	161	3adant3	$⊢ (φ \land u \in U \land r = u - A (Z)) \to 0 \leq u - A (Z)$
163		id	$⊢ r = u - A (Z) \to r = u - A (Z)$
164	163	eqcomd	$⊢ r = u - A (Z) \to u - A (Z) = r$
165	164	3ad2ant3	$⊢ (φ \land u \in U \land r = u - A (Z)) \to u - A (Z) = r$
166	162 165	breqtrd	$⊢ (φ \land u \in U \land r = u - A (Z)) \to 0 \leq r$
167	166	3exp	$⊢ φ \to (u \in U \to (r = u - A (Z) \to 0 \leq r))$
168	167	adantr	$⊢ (φ \land r \in \{w \| \exists u \in U w = u - A (Z)\}) \to (u \in U \to (r = u - A (Z) \to 0 \leq r))$
169	149 150 168	rexlimd	$⊢ (φ \land r \in \{w \| \exists u \in U w = u - A (Z)\}) \to (\exists u \in U r = u - A (Z) \to 0 \leq r)$
170	143 169	mpd	$⊢ (φ \land r \in \{w \| \exists u \in U w = u - A (Z)\}) \to 0 \leq r$
171	170	ralrimiva	$⊢ φ \to \forall r \in \{w \| \exists u \in U w = u - A (Z)\} 0 \leq r$
172		simp3	$⊢ (φ \land u \in U \land w = u - A (Z)) \to w = u - A (Z)$
173	158 159	resubcld	$⊢ (φ \land u \in U) \to u - A (Z) \in ℝ$
174	173	3adant3	$⊢ (φ \land u \in U \land w = u - A (Z)) \to u - A (Z) \in ℝ$
175	172 174	eqeltrd	$⊢ (φ \land u \in U \land w = u - A (Z)) \to w \in ℝ$
176	175	3exp	$⊢ φ \to (u \in U \to (w = u - A (Z) \to w \in ℝ))$
177	176	rexlimdv	$⊢ φ \to (\exists u \in U w = u - A (Z) \to w \in ℝ)$
178	177	alrimiv	$⊢ φ \to \forall w (\exists u \in U w = u - A (Z) \to w \in ℝ)$
179		abss	$⊢ \{w \| \exists u \in U w = u - A (Z)\} \subseteq ℝ \leftrightarrow \forall w (\exists u \in U w = u - A (Z) \to w \in ℝ)$
180	178 179	sylibr	$⊢ φ \to \{w \| \exists u \in U w = u - A (Z)\} \subseteq ℝ$
181	32	eqcomd	$⊢ φ \to 0 = A (Z) - A (Z)$
182		oveq1	$⊢ u = A (Z) \to u - A (Z) = A (Z) - A (Z)$
183	182	rspceeqv	$⊢ (A (Z) \in U \land 0 = A (Z) - A (Z)) \to \exists u \in U 0 = u - A (Z)$
184	119 181 183	syl2anc	$⊢ φ \to \exists u \in U 0 = u - A (Z)$
185		eqeq1	$⊢ w = 0 \to (w = u - A (Z) \leftrightarrow 0 = u - A (Z))$
186	185	rexbidv	$⊢ w = 0 \to (\exists u \in U w = u - A (Z) \leftrightarrow \exists u \in U 0 = u - A (Z))$
187	50 184 186	elabd	$⊢ φ \to 0 \in \{w \| \exists u \in U w = u - A (Z)\}$
188		ne0i	$⊢ 0 \in \{w \| \exists u \in U w = u - A (Z)\} \to \{w \| \exists u \in U w = u - A (Z)\} \neq \emptyset$
189	187 188	syl	$⊢ φ \to \{w \| \exists u \in U w = u - A (Z)\} \neq \emptyset$
190	24 23	resubcld	$⊢ φ \to B (Z) - A (Z) \in ℝ$
191		vex	$⊢ s \in V$
192		eqeq1	$⊢ w = s \to (w = u - A (Z) \leftrightarrow s = u - A (Z))$
193	192	rexbidv	$⊢ w = s \to (\exists u \in U w = u - A (Z) \leftrightarrow \exists u \in U s = u - A (Z))$
194	191 193	elab	$⊢ s \in \{w \| \exists u \in U w = u - A (Z)\} \leftrightarrow \exists u \in U s = u - A (Z)$
195	194	biimpi	$⊢ s \in \{w \| \exists u \in U w = u - A (Z)\} \to \exists u \in U s = u - A (Z)$
196	195	adantl	$⊢ (φ \land s \in \{w \| \exists u \in U w = u - A (Z)\}) \to \exists u \in U s = u - A (Z)$
197		nfcv	$⊢ \underline{Ⅎ} u s$
198	197 147	nfel	$⊢ Ⅎ u s \in \{w \| \exists u \in U w = u - A (Z)\}$
199	144 198	nfan	$⊢ Ⅎ u (φ \land s \in \{w \| \exists u \in U w = u - A (Z)\})$
200		nfv	$⊢ Ⅎ u s \leq B (Z) - A (Z)$
201		simp3	$⊢ (φ \land u \in U \land s = u - A (Z)) \to s = u - A (Z)$
202	159	3adant3	$⊢ (φ \land u \in U \land s = u - A (Z)) \to A (Z) \in ℝ$
203	24	3ad2ant1	$⊢ (φ \land u \in U \land s = u - A (Z)) \to B (Z) \in ℝ$
204	155	3adant3	$⊢ (φ \land u \in U \land s = u - A (Z)) \to u \in [A (Z), B (Z)]$
205	30	3ad2ant1	$⊢ (φ \land u \in U \land s = u - A (Z)) \to A (Z) \in [A (Z), B (Z)]$
206	202 203 204 205	iccsuble	$⊢ (φ \land u \in U \land s = u - A (Z)) \to u - A (Z) \leq B (Z) - A (Z)$
207	201 206	eqbrtrd	$⊢ (φ \land u \in U \land s = u - A (Z)) \to s \leq B (Z) - A (Z)$
208	207	3exp	$⊢ φ \to (u \in U \to (s = u - A (Z) \to s \leq B (Z) - A (Z)))$
209	208	adantr	$⊢ (φ \land s \in \{w \| \exists u \in U w = u - A (Z)\}) \to (u \in U \to (s = u - A (Z) \to s \leq B (Z) - A (Z)))$
210	199 200 209	rexlimd	$⊢ (φ \land s \in \{w \| \exists u \in U w = u - A (Z)\}) \to (\exists u \in U s = u - A (Z) \to s \leq B (Z) - A (Z))$
211	196 210	mpd	$⊢ (φ \land s \in \{w \| \exists u \in U w = u - A (Z)\}) \to s \leq B (Z) - A (Z)$
212	211	ralrimiva	$⊢ φ \to \forall s \in \{w \| \exists u \in U w = u - A (Z)\} s \leq B (Z) - A (Z)$
213		brralrspcev	$⊢ (B (Z) - A (Z) \in ℝ \land \forall s \in \{w \| \exists u \in U w = u - A (Z)\} s \leq B (Z) - A (Z)) \to \exists r \in ℝ \forall s \in \{w \| \exists u \in U w = u - A (Z)\} s \leq r$
214	190 212 213	syl2anc	$⊢ φ \to \exists r \in ℝ \forall s \in \{w \| \exists u \in U w = u - A (Z)\} s \leq r$
215		eqid	$⊢ \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} = \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\}$
216		biid	$⊢ ((G \in ℝ \land 0 \leq G \land \forall r \in \{w \| \exists u \in U w = u - A (Z)\} 0 \leq r) \land (\{w \| \exists u \in U w = u - A (Z)\} \subseteq ℝ \land \{w \| \exists u \in U w = u - A (Z)\} \neq \emptyset \land \exists r \in ℝ \forall s \in \{w \| \exists u \in U w = u - A (Z)\} s \leq r)) \leftrightarrow ((G \in ℝ \land 0 \leq G \land \forall r \in \{w \| \exists u \in U w = u - A (Z)\} 0 \leq r) \land (\{w \| \exists u \in U w = u - A (Z)\} \subseteq ℝ \land \{w \| \exists u \in U w = u - A (Z)\} \neq \emptyset \land \exists r \in ℝ \forall s \in \{w \| \exists u \in U w = u - A (Z)\} s \leq r))$
217	215 216	supmul1	$⊢ ((G \in ℝ \land 0 \leq G \land \forall r \in \{w \| \exists u \in U w = u - A (Z)\} 0 \leq r) \land (\{w \| \exists u \in U w = u - A (Z)\} \subseteq ℝ \land \{w \| \exists u \in U w = u - A (Z)\} \neq \emptyset \land \exists r \in ℝ \forall s \in \{w \| \exists u \in U w = u - A (Z)\} s \leq r)) \to G sup (\{w \| \exists u \in U w = u - A (Z)\} ℝ <) = sup (\{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} ℝ <)$
218	43 137 171 180 189 214 217	syl33anc	$⊢ φ \to G sup (\{w \| \exists u \in U w = u - A (Z)\} ℝ <) = sup (\{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} ℝ <)$
219	125 134 218	3eqtrd	$⊢ φ \to G (S - A (Z)) = sup (\{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} ℝ <)$
220		vex	$⊢ c \in V$
221		eqeq1	$⊢ v = c \to (v = G t \leftrightarrow c = G t)$
222	221	rexbidv	$⊢ v = c \to (\exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t \leftrightarrow \exists t \in \{w \| \exists u \in U w = u - A (Z)\} c = G t)$
223	220 222	elab	$⊢ c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} \leftrightarrow \exists t \in \{w \| \exists u \in U w = u - A (Z)\} c = G t$
224	223	biimpi	$⊢ c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} \to \exists t \in \{w \| \exists u \in U w = u - A (Z)\} c = G t$
225		nfv	$⊢ Ⅎ t \exists u \in U c = G (u - A (Z))$
226		vex	$⊢ t \in V$
227		eqeq1	$⊢ w = t \to (w = u - A (Z) \leftrightarrow t = u - A (Z))$
228	227	rexbidv	$⊢ w = t \to (\exists u \in U w = u - A (Z) \leftrightarrow \exists u \in U t = u - A (Z))$
229	226 228	elab	$⊢ t \in \{w \| \exists u \in U w = u - A (Z)\} \leftrightarrow \exists u \in U t = u - A (Z)$
230	229	biimpi	$⊢ t \in \{w \| \exists u \in U w = u - A (Z)\} \to \exists u \in U t = u - A (Z)$
231	230	adantr	$⊢ (t \in \{w \| \exists u \in U w = u - A (Z)\} \land c = G t) \to \exists u \in U t = u - A (Z)$
232		simpl	$⊢ (c = G t \land t = u - A (Z)) \to c = G t$
233		oveq2	$⊢ t = u - A (Z) \to G t = G (u - A (Z))$
234	233	adantl	$⊢ (c = G t \land t = u - A (Z)) \to G t = G (u - A (Z))$
235	232 234	eqtrd	$⊢ (c = G t \land t = u - A (Z)) \to c = G (u - A (Z))$
236	235	ex	$⊢ c = G t \to (t = u - A (Z) \to c = G (u - A (Z)))$
237	236	reximdv	$⊢ c = G t \to (\exists u \in U t = u - A (Z) \to \exists u \in U c = G (u - A (Z)))$
238	237	adantl	$⊢ (t \in \{w \| \exists u \in U w = u - A (Z)\} \land c = G t) \to (\exists u \in U t = u - A (Z) \to \exists u \in U c = G (u - A (Z)))$
239	231 238	mpd	$⊢ (t \in \{w \| \exists u \in U w = u - A (Z)\} \land c = G t) \to \exists u \in U c = G (u - A (Z))$
240	239	ex	$⊢ t \in \{w \| \exists u \in U w = u - A (Z)\} \to (c = G t \to \exists u \in U c = G (u - A (Z)))$
241	225 240	rexlimi	$⊢ \exists t \in \{w \| \exists u \in U w = u - A (Z)\} c = G t \to \exists u \in U c = G (u - A (Z))$
242	241	a1i	$⊢ c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} \to (\exists t \in \{w \| \exists u \in U w = u - A (Z)\} c = G t \to \exists u \in U c = G (u - A (Z)))$
243	224 242	mpd	$⊢ c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} \to \exists u \in U c = G (u - A (Z))$
244	243	adantl	$⊢ (φ \land c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\}) \to \exists u \in U c = G (u - A (Z))$
245		simp3	$⊢ (φ \land u \in U \land c = G (u - A (Z))) \to c = G (u - A (Z))$
246	43	adantr	$⊢ (φ \land u \in U) \to G \in ℝ$
247	246 173	remulcld	$⊢ (φ \land u \in U) \to G (u - A (Z)) \in ℝ$
248	49	adantr	$⊢ (φ \land u \in U) \to 1 + E \in ℝ$
249	56	a1i	$⊢ (φ \land u \in U) \to ℕ \in V$
250	64	adantlr	$⊢ ((φ \land u \in U) \land j \in ℕ) \to W \in Fin$
251	67	adantlr	$⊢ ((φ \land u \in U) \land j \in ℕ) \to C (j) : W ⟶ ℝ$
252	158	adantr	$⊢ ((φ \land u \in U) \land j \in ℕ) \to u \in ℝ$
253	80	adantlr	$⊢ ((φ \land u \in U) \land j \in ℕ) \to D (j) : W ⟶ ℝ$
254	76 252 250 253	hsphoif	$⊢ ((φ \land u \in U) \land j \in ℕ) \to H (u) (D (j)) : W ⟶ ℝ$
255	1 250 251 254	hoidmvcl	$⊢ ((φ \land u \in U) \land j \in ℕ) \to C (j) L (W) H (u) (D (j)) \in [0, +∞)$
256	58 255	sseldi	$⊢ ((φ \land u \in U) \land j \in ℕ) \to C (j) L (W) H (u) (D (j)) \in [0, +∞]$
257	256	fmpttd	$⊢ (φ \land u \in U) \to (j \in ℕ ⟼ C (j) L (W) H (u) (D (j))) : ℕ ⟶ [0, +∞]$
258	249 257	sge0cl	$⊢ (φ \land u \in U) \to sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))) \in [0, +∞]$
259	249 257	sge0xrcl	$⊢ (φ \land u \in U) \to sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))) \in ℝ^{*}$
260	87	a1i	$⊢ (φ \land u \in U) \to +∞ \in ℝ^{*}$
261	89	adantr	$⊢ (φ \land u \in U) \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ^{*}$
262		nfv	$⊢ Ⅎ j (φ \land u \in U)$
263	92	adantlr	$⊢ ((φ \land u \in U) \land j \in ℕ) \to C (j) L (W) D (j) \in [0, +∞]$
264	95	adantlr	$⊢ ((φ \land u \in U) \land j \in ℕ) \to Z \in (W ∖ Y)$
265	1 250 264 5 252 76 251 253	hsphoidmvle	$⊢ ((φ \land u \in U) \land j \in ℕ) \to C (j) L (W) H (u) (D (j)) \leq C (j) L (W) D (j)$
266	262 249 256 263 265	sge0lempt	$⊢ (φ \land u \in U) \to sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))) \leq sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
267	98	adantr	$⊢ (φ \land u \in U) \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) < +∞$
268	259 261 260 266 267	xrlelttrd	$⊢ (φ \land u \in U) \to sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))) < +∞$
269	259 260 268	xrltned	$⊢ (φ \land u \in U) \to sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))) \neq +∞$
270		ge0xrre	$⊢ (sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))) \in [0, +∞] \land sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))) \neq +∞) \to sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))) \in ℝ$
271	258 269 270	syl2anc	$⊢ (φ \land u \in U) \to sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))) \in ℝ$
272	248 271	remulcld	$⊢ (φ \land u \in U) \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))) \in ℝ$
273	126 123	sseldd	$⊢ φ \to S \in ℝ$
274	1 35 94 5 8 9 10 11 273	sge0hsphoire	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) \in ℝ$
275	49 274	remulcld	$⊢ φ \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) \in ℝ$
276	275	adantr	$⊢ (φ \land u \in U) \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) \in ℝ$
277	14	eleq2i	$⊢ u \in U \leftrightarrow u \in \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\}$
278	277	biimpi	$⊢ u \in U \to u \in \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\}$
279		oveq1	$⊢ z = u \to z - A (Z) = u - A (Z)$
280	279	oveq2d	$⊢ z = u \to G (z - A (Z)) = G (u - A (Z))$
281		fveq2	$⊢ z = u \to H (z) = H (u)$
282	281	fveq1d	$⊢ z = u \to H (z) (D (j)) = H (u) (D (j))$
283	282	oveq2d	$⊢ z = u \to C (j) L (W) H (z) (D (j)) = C (j) L (W) H (u) (D (j))$
284	283	mpteq2dv	$⊢ z = u \to (j \in ℕ ⟼ C (j) L (W) H (z) (D (j))) = (j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))$
285	284	fveq2d	$⊢ z = u \to sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j)))) = sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j))))$
286	285	oveq2d	$⊢ z = u \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j)))) = (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j))))$
287	280 286	breq12d	$⊢ z = u \to (G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j)))) \leftrightarrow G (u - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))))$
288	287	elrab	$⊢ u \in \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\} \leftrightarrow (u \in [A (Z), B (Z)] \land G (u - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))))$
289	278 288	sylib	$⊢ u \in U \to (u \in [A (Z), B (Z)] \land G (u - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))))$
290	289	simprd	$⊢ u \in U \to G (u - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j))))$
291	290	adantl	$⊢ (φ \land u \in U) \to G (u - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j))))$
292	274	adantr	$⊢ (φ \land u \in U) \to sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) \in ℝ$
293	55	adantr	$⊢ (φ \land u \in U) \to 0 \leq 1 + E$
294	273	adantr	$⊢ (φ \land j \in ℕ) \to S \in ℝ$
295	76 294 64 80	hsphoif	$⊢ (φ \land j \in ℕ) \to H (S) (D (j)) : W ⟶ ℝ$
296	1 64 67 295	hoidmvcl	$⊢ (φ \land j \in ℕ) \to C (j) L (W) H (S) (D (j)) \in [0, +∞)$
297	58 296	sseldi	$⊢ (φ \land j \in ℕ) \to C (j) L (W) H (S) (D (j)) \in [0, +∞]$
298	297	adantlr	$⊢ ((φ \land u \in U) \land j \in ℕ) \to C (j) L (W) H (S) (D (j)) \in [0, +∞]$
299	294	adantlr	$⊢ ((φ \land u \in U) \land j \in ℕ) \to S \in ℝ$
300	127	adantr	$⊢ (φ \land u \in U) \to U \subseteq ℝ$
301	121	adantr	$⊢ (φ \land u \in U) \to U \neq \emptyset$
302	131	adantr	$⊢ (φ \land u \in U) \to \exists y \in ℝ \forall z \in U z \leq y$
303		simpr	$⊢ (φ \land u \in U) \to u \in U$
304		suprub	$⊢ ((U \subseteq ℝ \land U \neq \emptyset \land \exists y \in ℝ \forall z \in U z \leq y) \land u \in U) \to u \leq sup (U ℝ <)$
305	300 301 302 303 304	syl31anc	$⊢ (φ \land u \in U) \to u \leq sup (U ℝ <)$
306	305 15	breqtrrdi	$⊢ (φ \land u \in U) \to u \leq S$
307	306	adantr	$⊢ ((φ \land u \in U) \land j \in ℕ) \to u \leq S$
308	1 250 264 5 252 299 307 76 251 253	hsphoidmvle2	$⊢ ((φ \land u \in U) \land j \in ℕ) \to C (j) L (W) H (u) (D (j)) \leq C (j) L (W) H (S) (D (j))$
309	262 249 256 298 308	sge0lempt	$⊢ (φ \land u \in U) \to sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))) \leq sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j))))$
310	271 292 248 293 309	lemul2ad	$⊢ (φ \land u \in U) \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j))))$
311	247 272 276 291 310	letrd	$⊢ (φ \land u \in U) \to G (u - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j))))$
312	311	3adant3	$⊢ (φ \land u \in U \land c = G (u - A (Z))) \to G (u - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j))))$
313	245 312	eqbrtrd	$⊢ (φ \land u \in U \land c = G (u - A (Z))) \to c \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j))))$
314	313	3exp	$⊢ φ \to (u \in U \to (c = G (u - A (Z)) \to c \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j))))))$
315	314	rexlimdv	$⊢ φ \to (\exists u \in U c = G (u - A (Z)) \to c \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))))$
316	315	adantr	$⊢ (φ \land c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\}) \to (\exists u \in U c = G (u - A (Z)) \to c \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))))$
317	244 316	mpd	$⊢ (φ \land c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\}) \to c \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j))))$
318	317	ralrimiva	$⊢ φ \to \forall c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} c \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j))))$
319	224	adantl	$⊢ (φ \land c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\}) \to \exists t \in \{w \| \exists u \in U w = u - A (Z)\} c = G t$
320		nfv	$⊢ Ⅎ t φ$
321		nfcv	$⊢ \underline{Ⅎ} t c$
322		nfre1	$⊢ Ⅎ t \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t$
323	322	nfab	$⊢ \underline{Ⅎ} t \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\}$
324	321 323	nfel	$⊢ Ⅎ t c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\}$
325	320 324	nfan	$⊢ Ⅎ t (φ \land c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\})$
326		nfv	$⊢ Ⅎ t c \in ℝ$
327	230	adantl	$⊢ (φ \land t \in \{w \| \exists u \in U w = u - A (Z)\}) \to \exists u \in U t = u - A (Z)$
328		simpr	$⊢ ((φ \land u \in U \land t = u - A (Z)) \land c = G t) \to c = G t$
329	246	3adant3	$⊢ (φ \land u \in U \land t = u - A (Z)) \to G \in ℝ$
330		simp3	$⊢ (φ \land u \in U \land t = u - A (Z)) \to t = u - A (Z)$
331	173	3adant3	$⊢ (φ \land u \in U \land t = u - A (Z)) \to u - A (Z) \in ℝ$
332	330 331	eqeltrd	$⊢ (φ \land u \in U \land t = u - A (Z)) \to t \in ℝ$
333	329 332	remulcld	$⊢ (φ \land u \in U \land t = u - A (Z)) \to G t \in ℝ$
334	333	adantr	$⊢ ((φ \land u \in U \land t = u - A (Z)) \land c = G t) \to G t \in ℝ$
335	328 334	eqeltrd	$⊢ ((φ \land u \in U \land t = u - A (Z)) \land c = G t) \to c \in ℝ$
336	335	ex	$⊢ (φ \land u \in U \land t = u - A (Z)) \to (c = G t \to c \in ℝ)$
337	336	3exp	$⊢ φ \to (u \in U \to (t = u - A (Z) \to (c = G t \to c \in ℝ)))$
338	337	rexlimdv	$⊢ φ \to (\exists u \in U t = u - A (Z) \to (c = G t \to c \in ℝ))$
339	338	adantr	$⊢ (φ \land t \in \{w \| \exists u \in U w = u - A (Z)\}) \to (\exists u \in U t = u - A (Z) \to (c = G t \to c \in ℝ))$
340	327 339	mpd	$⊢ (φ \land t \in \{w \| \exists u \in U w = u - A (Z)\}) \to (c = G t \to c \in ℝ)$
341	340	ex	$⊢ φ \to (t \in \{w \| \exists u \in U w = u - A (Z)\} \to (c = G t \to c \in ℝ))$
342	341	adantr	$⊢ (φ \land c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\}) \to (t \in \{w \| \exists u \in U w = u - A (Z)\} \to (c = G t \to c \in ℝ))$
343	325 326 342	rexlimd	$⊢ (φ \land c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\}) \to (\exists t \in \{w \| \exists u \in U w = u - A (Z)\} c = G t \to c \in ℝ)$
344	319 343	mpd	$⊢ (φ \land c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\}) \to c \in ℝ$
345	344	ralrimiva	$⊢ φ \to \forall c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} c \in ℝ$
346		dfss3	$⊢ \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} \subseteq ℝ \leftrightarrow \forall c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} c \in ℝ$
347	345 346	sylibr	$⊢ φ \to \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} \subseteq ℝ$
348	45	eqcomd	$⊢ φ \to 0 = G \cdot 0$
349		oveq2	$⊢ t = 0 \to G t = G \cdot 0$
350	349	rspceeqv	$⊢ (0 \in \{w \| \exists u \in U w = u - A (Z)\} \land 0 = G \cdot 0) \to \exists t \in \{w \| \exists u \in U w = u - A (Z)\} 0 = G t$
351	187 348 350	syl2anc	$⊢ φ \to \exists t \in \{w \| \exists u \in U w = u - A (Z)\} 0 = G t$
352		eqeq1	$⊢ v = 0 \to (v = G t \leftrightarrow 0 = G t)$
353	352	rexbidv	$⊢ v = 0 \to (\exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t \leftrightarrow \exists t \in \{w \| \exists u \in U w = u - A (Z)\} 0 = G t)$
354	50 351 353	elabd	$⊢ φ \to 0 \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\}$
355		ne0i	$⊢ 0 \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} \to \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} \neq \emptyset$
356	354 355	syl	$⊢ φ \to \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} \neq \emptyset$
357	43 190	remulcld	$⊢ φ \to G (B (Z) - A (Z)) \in ℝ$
358	190	adantr	$⊢ (φ \land u \in U) \to B (Z) - A (Z) \in ℝ$
359	137	adantr	$⊢ (φ \land u \in U) \to 0 \leq G$
360	24	adantr	$⊢ (φ \land u \in U) \to B (Z) \in ℝ$
361		iccleub	$⊢ (A (Z) \in ℝ^{} \land B (Z) \in ℝ^{} \land u \in [A (Z), B (Z)]) \to u \leq B (Z)$
362	152 154 155 361	syl3anc	$⊢ (φ \land u \in U) \to u \leq B (Z)$
363	158 360 159 362	lesub1dd	$⊢ (φ \land u \in U) \to u - A (Z) \leq B (Z) - A (Z)$
364	173 358 246 359 363	lemul2ad	$⊢ (φ \land u \in U) \to G (u - A (Z)) \leq G (B (Z) - A (Z))$
365	364	3adant3	$⊢ (φ \land u \in U \land c = G (u - A (Z))) \to G (u - A (Z)) \leq G (B (Z) - A (Z))$
366	245 365	eqbrtrd	$⊢ (φ \land u \in U \land c = G (u - A (Z))) \to c \leq G (B (Z) - A (Z))$
367	366	3exp	$⊢ φ \to (u \in U \to (c = G (u - A (Z)) \to c \leq G (B (Z) - A (Z))))$
368	367	rexlimdv	$⊢ φ \to (\exists u \in U c = G (u - A (Z)) \to c \leq G (B (Z) - A (Z)))$
369	368	adantr	$⊢ (φ \land c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\}) \to (\exists u \in U c = G (u - A (Z)) \to c \leq G (B (Z) - A (Z)))$
370	244 369	mpd	$⊢ (φ \land c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\}) \to c \leq G (B (Z) - A (Z))$
371	370	ralrimiva	$⊢ φ \to \forall c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} c \leq G (B (Z) - A (Z))$
372		brralrspcev	$⊢ (G (B (Z) - A (Z)) \in ℝ \land \forall c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} c \leq G (B (Z) - A (Z))) \to \exists y \in ℝ \forall c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} c \leq y$
373	357 371 372	syl2anc	$⊢ φ \to \exists y \in ℝ \forall c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} c \leq y$
374		suprleub	$⊢ ((\{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} \subseteq ℝ \land \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} \neq \emptyset \land \exists y \in ℝ \forall c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} c \leq y) \land (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) \in ℝ) \to (sup (\{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} ℝ <) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) \leftrightarrow \forall c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} c \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))))$
375	347 356 373 275 374	syl31anc	$⊢ φ \to (sup (\{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} ℝ <) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) \leftrightarrow \forall c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} c \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))))$
376	318 375	mpbird	$⊢ φ \to sup (\{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} ℝ <) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j))))$
377	219 376	eqbrtrd	$⊢ φ \to G (S - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j))))$
378	123 377	jca	$⊢ φ \to (S \in [A (Z), B (Z)] \land G (S - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))))$
379		oveq1	$⊢ z = S \to z - A (Z) = S - A (Z)$
380	379	oveq2d	$⊢ z = S \to G (z - A (Z)) = G (S - A (Z))$
381		fveq2	$⊢ z = S \to H (z) = H (S)$
382	381	fveq1d	$⊢ z = S \to H (z) (D (j)) = H (S) (D (j))$
383	382	oveq2d	$⊢ z = S \to C (j) L (W) H (z) (D (j)) = C (j) L (W) H (S) (D (j))$
384	383	mpteq2dv	$⊢ z = S \to (j \in ℕ ⟼ C (j) L (W) H (z) (D (j))) = (j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))$
385	384	fveq2d	$⊢ z = S \to sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j)))) = sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j))))$
386	385	oveq2d	$⊢ z = S \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j)))) = (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j))))$
387	380 386	breq12d	$⊢ z = S \to (G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j)))) \leftrightarrow G (S - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))))$
388	387	elrab	$⊢ S \in \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\} \leftrightarrow (S \in [A (Z), B (Z)] \land G (S - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))))$
389	378 388	sylibr	$⊢ φ \to S \in \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\}$
390	389 14	eleqtrrdi	$⊢ φ \to S \in U$

Metamath Proof Explorer

Theorem hoidmvlelem1

Proof