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

Metamath Proof Explorer

Theorem hoidmvlelem1

Proof