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	ffvelcdmd	$⊢ φ \to A (Z) \in ℝ$
24	7 22	ffvelcdmd	$⊢ φ \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	sselid	$⊢ φ \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	ffvelcdmda	$⊢ (φ \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	ffvelcdmda	$⊢ (φ \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	sselid	$⊢ (φ \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	sselid	$⊢ (φ \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	abssdv	$⊢ φ \to \{w \| \exists u \in U w = u - A (Z)\} \subseteq ℝ$
179	32	eqcomd	$⊢ φ \to 0 = A (Z) - A (Z)$
180		oveq1	$⊢ u = A (Z) \to u - A (Z) = A (Z) - A (Z)$
181	180	rspceeqv	$⊢ (A (Z) \in U \land 0 = A (Z) - A (Z)) \to \exists u \in U 0 = u - A (Z)$
182	119 179 181	syl2anc	$⊢ φ \to \exists u \in U 0 = u - A (Z)$
183		eqeq1	$⊢ w = 0 \to (w = u - A (Z) \leftrightarrow 0 = u - A (Z))$
184	183	rexbidv	$⊢ w = 0 \to (\exists u \in U w = u - A (Z) \leftrightarrow \exists u \in U 0 = u - A (Z))$
185	50 182 184	elabd	$⊢ φ \to 0 \in \{w \| \exists u \in U w = u - A (Z)\}$
186		ne0i	$⊢ 0 \in \{w \| \exists u \in U w = u - A (Z)\} \to \{w \| \exists u \in U w = u - A (Z)\} \neq \emptyset$
187	185 186	syl	$⊢ φ \to \{w \| \exists u \in U w = u - A (Z)\} \neq \emptyset$
188	24 23	resubcld	$⊢ φ \to B (Z) - A (Z) \in ℝ$
189		vex	$⊢ s \in V$
190		eqeq1	$⊢ w = s \to (w = u - A (Z) \leftrightarrow s = u - A (Z))$
191	190	rexbidv	$⊢ w = s \to (\exists u \in U w = u - A (Z) \leftrightarrow \exists u \in U s = u - A (Z))$
192	189 191	elab	$⊢ s \in \{w \| \exists u \in U w = u - A (Z)\} \leftrightarrow \exists u \in U s = u - A (Z)$
193	192	biimpi	$⊢ s \in \{w \| \exists u \in U w = u - A (Z)\} \to \exists u \in U s = u - A (Z)$
194	193	adantl	$⊢ (φ \land s \in \{w \| \exists u \in U w = u - A (Z)\}) \to \exists u \in U s = u - A (Z)$
195		nfcv	$⊢ \underline{Ⅎ} u s$
196	195 147	nfel	$⊢ Ⅎ u s \in \{w \| \exists u \in U w = u - A (Z)\}$
197	144 196	nfan	$⊢ Ⅎ u (φ \land s \in \{w \| \exists u \in U w = u - A (Z)\})$
198		nfv	$⊢ Ⅎ u s \leq B (Z) - A (Z)$
199		simp3	$⊢ (φ \land u \in U \land s = u - A (Z)) \to s = u - A (Z)$
200	159	3adant3	$⊢ (φ \land u \in U \land s = u - A (Z)) \to A (Z) \in ℝ$
201	24	3ad2ant1	$⊢ (φ \land u \in U \land s = u - A (Z)) \to B (Z) \in ℝ$
202	155	3adant3	$⊢ (φ \land u \in U \land s = u - A (Z)) \to u \in [A (Z), B (Z)]$
203	30	3ad2ant1	$⊢ (φ \land u \in U \land s = u - A (Z)) \to A (Z) \in [A (Z), B (Z)]$
204	200 201 202 203	iccsuble	$⊢ (φ \land u \in U \land s = u - A (Z)) \to u - A (Z) \leq B (Z) - A (Z)$
205	199 204	eqbrtrd	$⊢ (φ \land u \in U \land s = u - A (Z)) \to s \leq B (Z) - A (Z)$
206	205	3exp	$⊢ φ \to (u \in U \to (s = u - A (Z) \to s \leq B (Z) - A (Z)))$
207	206	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)))$
208	197 198 207	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))$
209	194 208	mpd	$⊢ (φ \land s \in \{w \| \exists u \in U w = u - A (Z)\}) \to s \leq B (Z) - A (Z)$
210	209	ralrimiva	$⊢ φ \to \forall s \in \{w \| \exists u \in U w = u - A (Z)\} s \leq B (Z) - A (Z)$
211		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$
212	188 210 211	syl2anc	$⊢ φ \to \exists r \in ℝ \forall s \in \{w \| \exists u \in U w = u - A (Z)\} s \leq r$
213		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\}$
214		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))$
215	213 214	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\} ℝ <)$
216	43 137 171 178 187 212 215	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\} ℝ <)$
217	125 134 216	3eqtrd	$⊢ φ \to G (S - A (Z)) = sup (\{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} ℝ <)$
218		vex	$⊢ c \in V$
219		eqeq1	$⊢ v = c \to (v = G t \leftrightarrow c = G t)$
220	219	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)$
221	218 220	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$
222	221	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$
223		nfv	$⊢ Ⅎ t \exists u \in U c = G (u - A (Z))$
224		vex	$⊢ t \in V$
225		eqeq1	$⊢ w = t \to (w = u - A (Z) \leftrightarrow t = u - A (Z))$
226	225	rexbidv	$⊢ w = t \to (\exists u \in U w = u - A (Z) \leftrightarrow \exists u \in U t = u - A (Z))$
227	224 226	elab	$⊢ t \in \{w \| \exists u \in U w = u - A (Z)\} \leftrightarrow \exists u \in U t = u - A (Z)$
228	227	biimpi	$⊢ t \in \{w \| \exists u \in U w = u - A (Z)\} \to \exists u \in U t = u - A (Z)$
229	228	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)$
230		simpl	$⊢ (c = G t \land t = u - A (Z)) \to c = G t$
231		oveq2	$⊢ t = u - A (Z) \to G t = G (u - A (Z))$
232	231	adantl	$⊢ (c = G t \land t = u - A (Z)) \to G t = G (u - A (Z))$
233	230 232	eqtrd	$⊢ (c = G t \land t = u - A (Z)) \to c = G (u - A (Z))$
234	233	ex	$⊢ c = G t \to (t = u - A (Z) \to c = G (u - A (Z)))$
235	234	reximdv	$⊢ c = G t \to (\exists u \in U t = u - A (Z) \to \exists u \in U c = G (u - A (Z)))$
236	235	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)))$
237	229 236	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))$
238	237	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)))$
239	223 238	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))$
240	222 239	syl	$⊢ 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))$
241	240	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))$
242		simp3	$⊢ (φ \land u \in U \land c = G (u - A (Z))) \to c = G (u - A (Z))$
243	43	adantr	$⊢ (φ \land u \in U) \to G \in ℝ$
244	243 173	remulcld	$⊢ (φ \land u \in U) \to G (u - A (Z)) \in ℝ$
245	49	adantr	$⊢ (φ \land u \in U) \to 1 + E \in ℝ$
246	56	a1i	$⊢ (φ \land u \in U) \to ℕ \in V$
247	64	adantlr	$⊢ ((φ \land u \in U) \land j \in ℕ) \to W \in Fin$
248	67	adantlr	$⊢ ((φ \land u \in U) \land j \in ℕ) \to C (j) : W ⟶ ℝ$
249	158	adantr	$⊢ ((φ \land u \in U) \land j \in ℕ) \to u \in ℝ$
250	80	adantlr	$⊢ ((φ \land u \in U) \land j \in ℕ) \to D (j) : W ⟶ ℝ$
251	76 249 247 250	hsphoif	$⊢ ((φ \land u \in U) \land j \in ℕ) \to H (u) (D (j)) : W ⟶ ℝ$
252	1 247 248 251	hoidmvcl	$⊢ ((φ \land u \in U) \land j \in ℕ) \to C (j) L (W) H (u) (D (j)) \in [0, +∞)$
253	58 252	sselid	$⊢ ((φ \land u \in U) \land j \in ℕ) \to C (j) L (W) H (u) (D (j)) \in [0, +∞]$
254	253	fmpttd	$⊢ (φ \land u \in U) \to (j \in ℕ ⟼ C (j) L (W) H (u) (D (j))) : ℕ ⟶ [0, +∞]$
255	246 254	sge0cl	$⊢ (φ \land u \in U) \to sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))) \in [0, +∞]$
256	246 254	sge0xrcl	$⊢ (φ \land u \in U) \to sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))) \in ℝ^{*}$
257	87	a1i	$⊢ (φ \land u \in U) \to +∞ \in ℝ^{*}$
258	89	adantr	$⊢ (φ \land u \in U) \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ^{*}$
259		nfv	$⊢ Ⅎ j (φ \land u \in U)$
260	92	adantlr	$⊢ ((φ \land u \in U) \land j \in ℕ) \to C (j) L (W) D (j) \in [0, +∞]$
261	95	adantlr	$⊢ ((φ \land u \in U) \land j \in ℕ) \to Z \in (W ∖ Y)$
262	1 247 261 5 249 76 248 250	hsphoidmvle	$⊢ ((φ \land u \in U) \land j \in ℕ) \to C (j) L (W) H (u) (D (j)) \leq C (j) L (W) D (j)$
263	259 246 253 260 262	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)))$
264	98	adantr	$⊢ (φ \land u \in U) \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) < +∞$
265	256 258 257 263 264	xrlelttrd	$⊢ (φ \land u \in U) \to sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))) < +∞$
266	256 257 265	xrltned	$⊢ (φ \land u \in U) \to sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))) \neq +∞$
267		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 ℝ$
268	255 266 267	syl2anc	$⊢ (φ \land u \in U) \to sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))) \in ℝ$
269	245 268	remulcld	$⊢ (φ \land u \in U) \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))) \in ℝ$
270	126 123	sseldd	$⊢ φ \to S \in ℝ$
271	1 35 94 5 8 9 10 11 270	sge0hsphoire	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) \in ℝ$
272	49 271	remulcld	$⊢ φ \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) \in ℝ$
273	272	adantr	$⊢ (φ \land u \in U) \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) \in ℝ$
274	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))))\}$
275	274	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))))\}$
276		oveq1	$⊢ z = u \to z - A (Z) = u - A (Z)$
277	276	oveq2d	$⊢ z = u \to G (z - A (Z)) = G (u - A (Z))$
278		fveq2	$⊢ z = u \to H (z) = H (u)$
279	278	fveq1d	$⊢ z = u \to H (z) (D (j)) = H (u) (D (j))$
280	279	oveq2d	$⊢ z = u \to C (j) L (W) H (z) (D (j)) = C (j) L (W) H (u) (D (j))$
281	280	mpteq2dv	$⊢ z = u \to (j \in ℕ ⟼ C (j) L (W) H (z) (D (j))) = (j \in ℕ ⟼ C (j) L (W) H (u) (D (j)))$
282	281	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))))$
283	282	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))))$
284	277 283	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)))))$
285	284	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)))))$
286	275 285	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)))))$
287	286	simprd	$⊢ u \in U \to G (u - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j))))$
288	287	adantl	$⊢ (φ \land u \in U) \to G (u - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (u) (D (j))))$
289	271	adantr	$⊢ (φ \land u \in U) \to sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) \in ℝ$
290	55	adantr	$⊢ (φ \land u \in U) \to 0 \leq 1 + E$
291	270	adantr	$⊢ (φ \land j \in ℕ) \to S \in ℝ$
292	76 291 64 80	hsphoif	$⊢ (φ \land j \in ℕ) \to H (S) (D (j)) : W ⟶ ℝ$
293	1 64 67 292	hoidmvcl	$⊢ (φ \land j \in ℕ) \to C (j) L (W) H (S) (D (j)) \in [0, +∞)$
294	58 293	sselid	$⊢ (φ \land j \in ℕ) \to C (j) L (W) H (S) (D (j)) \in [0, +∞]$
295	294	adantlr	$⊢ ((φ \land u \in U) \land j \in ℕ) \to C (j) L (W) H (S) (D (j)) \in [0, +∞]$
296	291	adantlr	$⊢ ((φ \land u \in U) \land j \in ℕ) \to S \in ℝ$
297	127	adantr	$⊢ (φ \land u \in U) \to U \subseteq ℝ$
298	121	adantr	$⊢ (φ \land u \in U) \to U \neq \emptyset$
299	131	adantr	$⊢ (φ \land u \in U) \to \exists y \in ℝ \forall z \in U z \leq y$
300		simpr	$⊢ (φ \land u \in U) \to u \in U$
301		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 ℝ <)$
302	297 298 299 300 301	syl31anc	$⊢ (φ \land u \in U) \to u \leq sup (U ℝ <)$
303	302 15	breqtrrdi	$⊢ (φ \land u \in U) \to u \leq S$
304	303	adantr	$⊢ ((φ \land u \in U) \land j \in ℕ) \to u \leq S$
305	1 247 261 5 249 296 304 76 248 250	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))$
306	259 246 253 295 305	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))))$
307	268 289 245 290 306	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))))$
308	244 269 273 288 307	letrd	$⊢ (φ \land u \in U) \to G (u - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j))))$
309	308	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))))$
310	242 309	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))))$
311	310	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))))))$
312	311	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)))))$
313	312	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)))))$
314	241 313	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))))$
315	314	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))))$
316	222	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$
317		nfv	$⊢ Ⅎ t φ$
318		nfcv	$⊢ \underline{Ⅎ} t c$
319		nfre1	$⊢ Ⅎ t \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t$
320	319	nfab	$⊢ \underline{Ⅎ} t \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\}$
321	318 320	nfel	$⊢ Ⅎ t c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\}$
322	317 321	nfan	$⊢ Ⅎ t (φ \land c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\})$
323		nfv	$⊢ Ⅎ t c \in ℝ$
324	228	adantl	$⊢ (φ \land t \in \{w \| \exists u \in U w = u - A (Z)\}) \to \exists u \in U t = u - A (Z)$
325		simpr	$⊢ ((φ \land u \in U \land t = u - A (Z)) \land c = G t) \to c = G t$
326	243	3adant3	$⊢ (φ \land u \in U \land t = u - A (Z)) \to G \in ℝ$
327		simp3	$⊢ (φ \land u \in U \land t = u - A (Z)) \to t = u - A (Z)$
328	173	3adant3	$⊢ (φ \land u \in U \land t = u - A (Z)) \to u - A (Z) \in ℝ$
329	327 328	eqeltrd	$⊢ (φ \land u \in U \land t = u - A (Z)) \to t \in ℝ$
330	326 329	remulcld	$⊢ (φ \land u \in U \land t = u - A (Z)) \to G t \in ℝ$
331	330	adantr	$⊢ ((φ \land u \in U \land t = u - A (Z)) \land c = G t) \to G t \in ℝ$
332	325 331	eqeltrd	$⊢ ((φ \land u \in U \land t = u - A (Z)) \land c = G t) \to c \in ℝ$
333	332	ex	$⊢ (φ \land u \in U \land t = u - A (Z)) \to (c = G t \to c \in ℝ)$
334	333	3exp	$⊢ φ \to (u \in U \to (t = u - A (Z) \to (c = G t \to c \in ℝ)))$
335	334	rexlimdv	$⊢ φ \to (\exists u \in U t = u - A (Z) \to (c = G t \to c \in ℝ))$
336	335	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 ℝ))$
337	324 336	mpd	$⊢ (φ \land t \in \{w \| \exists u \in U w = u - A (Z)\}) \to (c = G t \to c \in ℝ)$
338	337	ex	$⊢ φ \to (t \in \{w \| \exists u \in U w = u - A (Z)\} \to (c = G t \to c \in ℝ))$
339	338	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 ℝ))$
340	322 323 339	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 ℝ)$
341	316 340	mpd	$⊢ (φ \land c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\}) \to c \in ℝ$
342	341	ralrimiva	$⊢ φ \to \forall c \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} c \in ℝ$
343		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 ℝ$
344	342 343	sylibr	$⊢ φ \to \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} \subseteq ℝ$
345	45	eqcomd	$⊢ φ \to 0 = G \cdot 0$
346		oveq2	$⊢ t = 0 \to G t = G \cdot 0$
347	346	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$
348	185 345 347	syl2anc	$⊢ φ \to \exists t \in \{w \| \exists u \in U w = u - A (Z)\} 0 = G t$
349		eqeq1	$⊢ v = 0 \to (v = G t \leftrightarrow 0 = G t)$
350	349	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)$
351	50 348 350	elabd	$⊢ φ \to 0 \in \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\}$
352		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$
353	351 352	syl	$⊢ φ \to \{v \| \exists t \in \{w \| \exists u \in U w = u - A (Z)\} v = G t\} \neq \emptyset$
354	43 188	remulcld	$⊢ φ \to G (B (Z) - A (Z)) \in ℝ$
355	188	adantr	$⊢ (φ \land u \in U) \to B (Z) - A (Z) \in ℝ$
356	137	adantr	$⊢ (φ \land u \in U) \to 0 \leq G$
357	24	adantr	$⊢ (φ \land u \in U) \to B (Z) \in ℝ$
358		iccleub	$⊢ (A (Z) \in ℝ^{} \land B (Z) \in ℝ^{} \land u \in [A (Z), B (Z)]) \to u \leq B (Z)$
359	152 154 155 358	syl3anc	$⊢ (φ \land u \in U) \to u \leq B (Z)$
360	158 357 159 359	lesub1dd	$⊢ (φ \land u \in U) \to u - A (Z) \leq B (Z) - A (Z)$
361	173 355 243 356 360	lemul2ad	$⊢ (φ \land u \in U) \to G (u - A (Z)) \leq G (B (Z) - A (Z))$
362	361	3adant3	$⊢ (φ \land u \in U \land c = G (u - A (Z))) \to G (u - A (Z)) \leq G (B (Z) - A (Z))$
363	242 362	eqbrtrd	$⊢ (φ \land u \in U \land c = G (u - A (Z))) \to c \leq G (B (Z) - A (Z))$
364	363	3exp	$⊢ φ \to (u \in U \to (c = G (u - A (Z)) \to c \leq G (B (Z) - A (Z))))$
365	364	rexlimdv	$⊢ φ \to (\exists u \in U c = G (u - A (Z)) \to c \leq G (B (Z) - A (Z)))$
366	365	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)))$
367	241 366	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))$
368	367	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))$
369		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$
370	354 368 369	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$
371		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)))))$
372	344 353 370 272 371	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)))))$
373	315 372	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))))$
374	217 373	eqbrtrd	$⊢ φ \to G (S - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j))))$
375	123 374	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)))))$
376		oveq1	$⊢ z = S \to z - A (Z) = S - A (Z)$
377	376	oveq2d	$⊢ z = S \to G (z - A (Z)) = G (S - A (Z))$
378		fveq2	$⊢ z = S \to H (z) = H (S)$
379	378	fveq1d	$⊢ z = S \to H (z) (D (j)) = H (S) (D (j))$
380	379	oveq2d	$⊢ z = S \to C (j) L (W) H (z) (D (j)) = C (j) L (W) H (S) (D (j))$
381	380	mpteq2dv	$⊢ z = S \to (j \in ℕ ⟼ C (j) L (W) H (z) (D (j))) = (j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))$
382	381	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))))$
383	382	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))))$
384	377 383	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)))))$
385	384	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)))))$
386	375 385	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))))\}$
387	386 14	eleqtrrdi	$⊢ φ \to S \in U$

Metamath Proof Explorer

Theorem hoidmvlelem1

Proof