hoidmvlelem2

Description: This is the contradiction proven in step (d) in the proof of Lemma 115B of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	hoidmvlelem2.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
	hoidmvlelem2.x	$⊢ φ \to X \in Fin$
	hoidmvlelem2.y	$⊢ φ \to Y \subseteq X$
	hoidmvlelem2.z	$⊢ φ \to Z \in (X ∖ Y)$
	hoidmvlelem2.w	$⊢ W = Y \cup \{Z\}$
	hoidmvlelem2.a	$⊢ φ \to A : W ⟶ ℝ$
	hoidmvlelem2.b	$⊢ φ \to B : W ⟶ ℝ$
	hoidmvlelem2.c	$⊢ φ \to C : ℕ ⟶ ℝ^{W}$
	hoidmvlelem2.f	$⊢ F = (y \in Y ⟼ 0)$
	hoidmvlelem2.j	$⊢ J = (j \in ℕ ⟼ if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F))$
	hoidmvlelem2.d	$⊢ φ \to D : ℕ ⟶ ℝ^{W}$
	hoidmvlelem2.k	$⊢ K = (j \in ℕ ⟼ if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F))$
	hoidmvlelem2.r	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ$
	hoidmvlelem2.h	$⊢ H = (x \in ℝ ⟼ (c \in (ℝ^{W}) ⟼ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x)))))$
	hoidmvlelem2.g	$⊢ G = ({A ↾}_{Y}) L (Y) ({B ↾}_{Y})$
	hoidmvlelem2.e	$⊢ φ \to E \in ℝ^{+}$
	hoidmvlelem2.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))))\}$
	hoidmvlelem2.su	$⊢ φ \to S \in U$
	hoidmvlelem2.sb	$⊢ φ \to S < B (Z)$
	hoidmvlelem2.p	$⊢ P = (j \in ℕ ⟼ J (j) L (Y) K (j))$
	hoidmvlelem2.m	$⊢ φ \to M \in ℕ$
	hoidmvlelem2.le	$⊢ φ \to G \leq (1 + E) \sum_{j = 1}^{M} P (j)$
	hoidmvlelem2.O	$⊢ O = ran (i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} ⟼ D (i) (Z))$
	hoidmvlelem2.v	$⊢ V = \{B (Z)\} \cup O$
	hoidmvlelem2.q	$⊢ Q = inf (V ℝ <)$
Assertion	hoidmvlelem2	$⊢ φ \to \exists u \in U S < u$

Proof

Step	Hyp	Ref	Expression
1		hoidmvlelem2.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		hoidmvlelem2.x	$⊢ φ \to X \in Fin$
3		hoidmvlelem2.y	$⊢ φ \to Y \subseteq X$
4		hoidmvlelem2.z	$⊢ φ \to Z \in (X ∖ Y)$
5		hoidmvlelem2.w	$⊢ W = Y \cup \{Z\}$
6		hoidmvlelem2.a	$⊢ φ \to A : W ⟶ ℝ$
7		hoidmvlelem2.b	$⊢ φ \to B : W ⟶ ℝ$
8		hoidmvlelem2.c	$⊢ φ \to C : ℕ ⟶ ℝ^{W}$
9		hoidmvlelem2.f	$⊢ F = (y \in Y ⟼ 0)$
10		hoidmvlelem2.j	$⊢ J = (j \in ℕ ⟼ if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F))$
11		hoidmvlelem2.d	$⊢ φ \to D : ℕ ⟶ ℝ^{W}$
12		hoidmvlelem2.k	$⊢ K = (j \in ℕ ⟼ if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F))$
13		hoidmvlelem2.r	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ$
14		hoidmvlelem2.h	$⊢ H = (x \in ℝ ⟼ (c \in (ℝ^{W}) ⟼ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x)))))$
15		hoidmvlelem2.g	$⊢ G = ({A ↾}_{Y}) L (Y) ({B ↾}_{Y})$
16		hoidmvlelem2.e	$⊢ φ \to E \in ℝ^{+}$
17		hoidmvlelem2.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))))\}$
18		hoidmvlelem2.su	$⊢ φ \to S \in U$
19		hoidmvlelem2.sb	$⊢ φ \to S < B (Z)$
20		hoidmvlelem2.p	$⊢ P = (j \in ℕ ⟼ J (j) L (Y) K (j))$
21		hoidmvlelem2.m	$⊢ φ \to M \in ℕ$
22		hoidmvlelem2.le	$⊢ φ \to G \leq (1 + E) \sum_{j = 1}^{M} P (j)$
23		hoidmvlelem2.O	$⊢ O = ran (i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} ⟼ D (i) (Z))$
24		hoidmvlelem2.v	$⊢ V = \{B (Z)\} \cup O$
25		hoidmvlelem2.q	$⊢ Q = inf (V ℝ <)$
26		snidg	$⊢ Z \in (X ∖ Y) \to Z \in \{Z\}$
27	4 26	syl	$⊢ φ \to Z \in \{Z\}$
28		elun2	$⊢ Z \in \{Z\} \to Z \in (Y \cup \{Z\})$
29	27 28	syl	$⊢ φ \to Z \in (Y \cup \{Z\})$
30	29 5	eleqtrrdi	$⊢ φ \to Z \in W$
31	6 30	ffvelcdmd	$⊢ φ \to A (Z) \in ℝ$
32	7 30	ffvelcdmd	$⊢ φ \to B (Z) \in ℝ$
33	32	snssd	$⊢ φ \to \{B (Z)\} \subseteq ℝ$
34		nfv	$⊢ Ⅎ i φ$
35		eqid	$⊢ (i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} ⟼ D (i) (Z)) = (i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} ⟼ D (i) (Z))$
36		simpl	$⊢ (φ \land i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\}) \to φ$
37		fz1ssnn	$⊢ (1 \dots M) \subseteq ℕ$
38		elrabi	$⊢ i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} \to i \in (1 \dots M)$
39	37 38	sselid	$⊢ i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} \to i \in ℕ$
40	39	adantl	$⊢ (φ \land i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\}) \to i \in ℕ$
41		eleq1w	$⊢ j = i \to (j \in ℕ \leftrightarrow i \in ℕ)$
42	41	anbi2d	$⊢ j = i \to ((φ \land j \in ℕ) \leftrightarrow (φ \land i \in ℕ))$
43		fveq2	$⊢ j = i \to D (j) = D (i)$
44	43	fveq1d	$⊢ j = i \to D (j) (Z) = D (i) (Z)$
45	44	eleq1d	$⊢ j = i \to (D (j) (Z) \in ℝ \leftrightarrow D (i) (Z) \in ℝ)$
46	42 45	imbi12d	$⊢ j = i \to (((φ \land j \in ℕ) \to D (j) (Z) \in ℝ) \leftrightarrow ((φ \land i \in ℕ) \to D (i) (Z) \in ℝ))$
47	11	ffvelcdmda	$⊢ (φ \land j \in ℕ) \to D (j) \in (ℝ^{W})$
48		elmapi	$⊢ D (j) \in (ℝ^{W}) \to D (j) : W ⟶ ℝ$
49	47 48	syl	$⊢ (φ \land j \in ℕ) \to D (j) : W ⟶ ℝ$
50	30	adantr	$⊢ (φ \land j \in ℕ) \to Z \in W$
51	49 50	ffvelcdmd	$⊢ (φ \land j \in ℕ) \to D (j) (Z) \in ℝ$
52	46 51	chvarvv	$⊢ (φ \land i \in ℕ) \to D (i) (Z) \in ℝ$
53	36 40 52	syl2anc	$⊢ (φ \land i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\}) \to D (i) (Z) \in ℝ$
54	34 35 53	rnmptssd	$⊢ φ \to ran (i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} ⟼ D (i) (Z)) \subseteq ℝ$
55	23 54	eqsstrid	$⊢ φ \to O \subseteq ℝ$
56	33 55	unssd	$⊢ φ \to \{B (Z)\} \cup O \subseteq ℝ$
57	24 56	eqsstrid	$⊢ φ \to V \subseteq ℝ$
58		ltso	$⊢ < Or ℝ$
59	58	a1i	$⊢ φ \to < Or ℝ$
60		snfi	$⊢ \{B (Z)\} \in Fin$
61	60	a1i	$⊢ φ \to \{B (Z)\} \in Fin$
62		fzfi	$⊢ (1 \dots M) \in Fin$
63		rabfi	$⊢ (1 \dots M) \in Fin \to \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} \in Fin$
64	62 63	ax-mp	$⊢ \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} \in Fin$
65	64	a1i	$⊢ φ \to \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} \in Fin$
66	35	rnmptfi	$⊢ \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} \in Fin \to ran (i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} ⟼ D (i) (Z)) \in Fin$
67	65 66	syl	$⊢ φ \to ran (i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} ⟼ D (i) (Z)) \in Fin$
68	23 67	eqeltrid	$⊢ φ \to O \in Fin$
69		unfi	$⊢ (\{B (Z)\} \in Fin \land O \in Fin) \to \{B (Z)\} \cup O \in Fin$
70	61 68 69	syl2anc	$⊢ φ \to \{B (Z)\} \cup O \in Fin$
71	24 70	eqeltrid	$⊢ φ \to V \in Fin$
72		fvex	$⊢ B (Z) \in V$
73	72	snid	$⊢ B (Z) \in \{B (Z)\}$
74		elun1	$⊢ B (Z) \in \{B (Z)\} \to B (Z) \in (\{B (Z)\} \cup O)$
75	73 74	ax-mp	$⊢ B (Z) \in (\{B (Z)\} \cup O)$
76	24	eqcomi	$⊢ \{B (Z)\} \cup O = V$
77	75 76	eleqtri	$⊢ B (Z) \in V$
78	77	a1i	$⊢ φ \to B (Z) \in V$
79		ne0i	$⊢ B (Z) \in V \to V \neq \emptyset$
80	78 79	syl	$⊢ φ \to V \neq \emptyset$
81		fiinfcl	$⊢ (< Or ℝ \land (V \in Fin \land V \neq \emptyset \land V \subseteq ℝ)) \to inf (V ℝ <) \in V$
82	59 71 80 57 81	syl13anc	$⊢ φ \to inf (V ℝ <) \in V$
83	25 82	eqeltrid	$⊢ φ \to Q \in V$
84	57 83	sseldd	$⊢ φ \to Q \in ℝ$
85		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)]$
86	17 85	eqsstri	$⊢ U \subseteq [A (Z), B (Z)]$
87	86	a1i	$⊢ φ \to U \subseteq [A (Z), B (Z)]$
88	31 32	iccssred	$⊢ φ \to [A (Z), B (Z)] \subseteq ℝ$
89	87 88	sstrd	$⊢ φ \to U \subseteq ℝ$
90	89 18	sseldd	$⊢ φ \to S \in ℝ$
91	31	rexrd	$⊢ φ \to A (Z) \in ℝ^{*}$
92	32	rexrd	$⊢ φ \to B (Z) \in ℝ^{*}$
93	86 18	sselid	$⊢ φ \to S \in [A (Z), B (Z)]$
94		iccgelb	$⊢ (A (Z) \in ℝ^{} \land B (Z) \in ℝ^{} \land S \in [A (Z), B (Z)]) \to A (Z) \leq S$
95	91 92 93 94	syl3anc	$⊢ φ \to A (Z) \leq S$
96	19	adantr	$⊢ (φ \land x = B (Z)) \to S < B (Z)$
97		id	$⊢ x = B (Z) \to x = B (Z)$
98	97	eqcomd	$⊢ x = B (Z) \to B (Z) = x$
99	98	adantl	$⊢ (φ \land x = B (Z)) \to B (Z) = x$
100	96 99	breqtrd	$⊢ (φ \land x = B (Z)) \to S < x$
101	100	adantlr	$⊢ ((φ \land x \in V) \land x = B (Z)) \to S < x$
102		simpll	$⊢ ((φ \land x \in V) \land \neg x = B (Z)) \to φ$
103		id	$⊢ x \in V \to x \in V$
104	103 24	eleqtrdi	$⊢ x \in V \to x \in (\{B (Z)\} \cup O)$
105	104	adantr	$⊢ (x \in V \land \neg x = B (Z)) \to x \in (\{B (Z)\} \cup O)$
106		elsni	$⊢ x \in \{B (Z)\} \to x = B (Z)$
107	106	con3i	$⊢ \neg x = B (Z) \to \neg x \in \{B (Z)\}$
108	107	adantl	$⊢ (x \in V \land \neg x = B (Z)) \to \neg x \in \{B (Z)\}$
109		elunnel1	$⊢ (x \in (\{B (Z)\} \cup O) \land \neg x \in \{B (Z)\}) \to x \in O$
110	105 108 109	syl2anc	$⊢ (x \in V \land \neg x = B (Z)) \to x \in O$
111	110	adantll	$⊢ ((φ \land x \in V) \land \neg x = B (Z)) \to x \in O$
112		id	$⊢ x \in O \to x \in O$
113	112 23	eleqtrdi	$⊢ x \in O \to x \in ran (i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} ⟼ D (i) (Z))$
114		vex	$⊢ x \in V$
115	35	elrnmpt	$⊢ x \in V \to (x \in ran (i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} ⟼ D (i) (Z)) \leftrightarrow \exists i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} x = D (i) (Z))$
116	114 115	ax-mp	$⊢ x \in ran (i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} ⟼ D (i) (Z)) \leftrightarrow \exists i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} x = D (i) (Z)$
117	113 116	sylib	$⊢ x \in O \to \exists i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} x = D (i) (Z)$
118	117	adantl	$⊢ (φ \land x \in O) \to \exists i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} x = D (i) (Z)$
119		fveq2	$⊢ j = i \to C (j) = C (i)$
120	119	fveq1d	$⊢ j = i \to C (j) (Z) = C (i) (Z)$
121	120	eleq1d	$⊢ j = i \to (C (j) (Z) \in ℝ \leftrightarrow C (i) (Z) \in ℝ)$
122	42 121	imbi12d	$⊢ j = i \to (((φ \land j \in ℕ) \to C (j) (Z) \in ℝ) \leftrightarrow ((φ \land i \in ℕ) \to C (i) (Z) \in ℝ))$
123	8	ffvelcdmda	$⊢ (φ \land j \in ℕ) \to C (j) \in (ℝ^{W})$
124		elmapi	$⊢ C (j) \in (ℝ^{W}) \to C (j) : W ⟶ ℝ$
125	123 124	syl	$⊢ (φ \land j \in ℕ) \to C (j) : W ⟶ ℝ$
126	125 50	ffvelcdmd	$⊢ (φ \land j \in ℕ) \to C (j) (Z) \in ℝ$
127	122 126	chvarvv	$⊢ (φ \land i \in ℕ) \to C (i) (Z) \in ℝ$
128	127	rexrd	$⊢ (φ \land i \in ℕ) \to C (i) (Z) \in ℝ^{*}$
129	36 40 128	syl2anc	$⊢ (φ \land i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\}) \to C (i) (Z) \in ℝ^{*}$
130	52	rexrd	$⊢ (φ \land i \in ℕ) \to D (i) (Z) \in ℝ^{*}$
131	36 40 130	syl2anc	$⊢ (φ \land i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\}) \to D (i) (Z) \in ℝ^{*}$
132	120 44	oveq12d	$⊢ j = i \to [C (j) (Z), D (j) (Z)) = [C (i) (Z), D (i) (Z))$
133	132	eleq2d	$⊢ j = i \to (S \in [C (j) (Z), D (j) (Z)) \leftrightarrow S \in [C (i) (Z), D (i) (Z)))$
134	133	elrab	$⊢ i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} \leftrightarrow (i \in (1 \dots M) \land S \in [C (i) (Z), D (i) (Z)))$
135	134	biimpi	$⊢ i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} \to (i \in (1 \dots M) \land S \in [C (i) (Z), D (i) (Z)))$
136	135	simprd	$⊢ i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} \to S \in [C (i) (Z), D (i) (Z))$
137	136	adantl	$⊢ (φ \land i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\}) \to S \in [C (i) (Z), D (i) (Z))$
138		icoltub	$⊢ (C (i) (Z) \in ℝ^{} \land D (i) (Z) \in ℝ^{} \land S \in [C (i) (Z), D (i) (Z))) \to S < D (i) (Z)$
139	129 131 137 138	syl3anc	$⊢ (φ \land i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\}) \to S < D (i) (Z)$
140	139	3adant3	$⊢ (φ \land i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} \land x = D (i) (Z)) \to S < D (i) (Z)$
141		id	$⊢ x = D (i) (Z) \to x = D (i) (Z)$
142	141	eqcomd	$⊢ x = D (i) (Z) \to D (i) (Z) = x$
143	142	3ad2ant3	$⊢ (φ \land i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} \land x = D (i) (Z)) \to D (i) (Z) = x$
144	140 143	breqtrd	$⊢ (φ \land i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} \land x = D (i) (Z)) \to S < x$
145	144	3exp	$⊢ φ \to (i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} \to (x = D (i) (Z) \to S < x))$
146	145	adantr	$⊢ (φ \land x \in O) \to (i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} \to (x = D (i) (Z) \to S < x))$
147	146	rexlimdv	$⊢ (φ \land x \in O) \to (\exists i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} x = D (i) (Z) \to S < x)$
148	118 147	mpd	$⊢ (φ \land x \in O) \to S < x$
149	102 111 148	syl2anc	$⊢ ((φ \land x \in V) \land \neg x = B (Z)) \to S < x$
150	101 149	pm2.61dan	$⊢ (φ \land x \in V) \to S < x$
151	150	ralrimiva	$⊢ φ \to \forall x \in V S < x$
152		breq2	$⊢ x = inf (V ℝ <) \to (S < x \leftrightarrow S < inf (V ℝ <))$
153	152	rspcva	$⊢ (inf (V ℝ <) \in V \land \forall x \in V S < x) \to S < inf (V ℝ <)$
154	82 151 153	syl2anc	$⊢ φ \to S < inf (V ℝ <)$
155	25	eqcomi	$⊢ inf (V ℝ <) = Q$
156	155	a1i	$⊢ φ \to inf (V ℝ <) = Q$
157	154 156	breqtrd	$⊢ φ \to S < Q$
158	31 90 84 95 157	lelttrd	$⊢ φ \to A (Z) < Q$
159	31 84 158	ltled	$⊢ φ \to A (Z) \leq Q$
160		fiminre	$⊢ (V \subseteq ℝ \land V \in Fin \land V \neq \emptyset) \to \exists x \in V \forall y \in V x \leq y$
161	57 71 80 160	syl3anc	$⊢ φ \to \exists x \in V \forall y \in V x \leq y$
162		lbinfle	$⊢ (V \subseteq ℝ \land \exists x \in V \forall y \in V x \leq y \land B (Z) \in V) \to inf (V ℝ <) \leq B (Z)$
163	57 161 78 162	syl3anc	$⊢ φ \to inf (V ℝ <) \leq B (Z)$
164	25 163	eqbrtrid	$⊢ φ \to Q \leq B (Z)$
165	31 32 84 159 164	eliccd	$⊢ φ \to Q \in [A (Z), B (Z)]$
166	84	recnd	$⊢ φ \to Q \in ℂ$
167	90	recnd	$⊢ φ \to S \in ℂ$
168	31	recnd	$⊢ φ \to A (Z) \in ℂ$
169	166 167 168	npncand	$⊢ φ \to (Q - S) + S - A (Z) = Q - A (Z)$
170	169	eqcomd	$⊢ φ \to Q - A (Z) = (Q - S) + S - A (Z)$
171	170	oveq2d	$⊢ φ \to G (Q - A (Z)) = G ((Q - S) + S - A (Z))$
172		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
173	2 3	ssfid	$⊢ φ \to Y \in Fin$
174		ssun1	$⊢ Y \subseteq Y \cup \{Z\}$
175	174 5	sseqtrri	$⊢ Y \subseteq W$
176	175	a1i	$⊢ φ \to Y \subseteq W$
177	6 176	fssresd	$⊢ φ \to ({A ↾}_{Y}) : Y ⟶ ℝ$
178	7 176	fssresd	$⊢ φ \to ({B ↾}_{Y}) : Y ⟶ ℝ$
179	1 173 177 178	hoidmvcl	$⊢ φ \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \in [0, +∞)$
180	15 179	eqeltrid	$⊢ φ \to G \in [0, +∞)$
181	172 180	sselid	$⊢ φ \to G \in ℝ$
182	181	recnd	$⊢ φ \to G \in ℂ$
183	166 167	subcld	$⊢ φ \to Q - S \in ℂ$
184	167 168	subcld	$⊢ φ \to S - A (Z) \in ℂ$
185	182 183 184	adddid	$⊢ φ \to G ((Q - S) + S - A (Z)) = G (Q - S) + G (S - A (Z))$
186	182 183	mulcld	$⊢ φ \to G (Q - S) \in ℂ$
187	182 184	mulcld	$⊢ φ \to G (S - A (Z)) \in ℂ$
188	186 187	addcomd	$⊢ φ \to G (Q - S) + G (S - A (Z)) = G (S - A (Z)) + G (Q - S)$
189	171 185 188	3eqtrd	$⊢ φ \to G (Q - A (Z)) = G (S - A (Z)) + G (Q - S)$
190	84 90	jca	$⊢ φ \to (Q \in ℝ \land S \in ℝ)$
191		resubcl	$⊢ (Q \in ℝ \land S \in ℝ) \to Q - S \in ℝ$
192	190 191	syl	$⊢ φ \to Q - S \in ℝ$
193	181 192	jca	$⊢ φ \to (G \in ℝ \land Q - S \in ℝ)$
194		remulcl	$⊢ (G \in ℝ \land Q - S \in ℝ) \to G (Q - S) \in ℝ$
195	193 194	syl	$⊢ φ \to G (Q - S) \in ℝ$
196	90 31	jca	$⊢ φ \to (S \in ℝ \land A (Z) \in ℝ)$
197		resubcl	$⊢ (S \in ℝ \land A (Z) \in ℝ) \to S - A (Z) \in ℝ$
198	196 197	syl	$⊢ φ \to S - A (Z) \in ℝ$
199	181 198	jca	$⊢ φ \to (G \in ℝ \land S - A (Z) \in ℝ)$
200		remulcl	$⊢ (G \in ℝ \land S - A (Z) \in ℝ) \to G (S - A (Z)) \in ℝ$
201	199 200	syl	$⊢ φ \to G (S - A (Z)) \in ℝ$
202	195 201	jca	$⊢ φ \to (G (Q - S) \in ℝ \land G (S - A (Z)) \in ℝ)$
203		readdcl	$⊢ (G (Q - S) \in ℝ \land G (S - A (Z)) \in ℝ) \to G (Q - S) + G (S - A (Z)) \in ℝ$
204	202 203	syl	$⊢ φ \to G (Q - S) + G (S - A (Z)) \in ℝ$
205	188 204	eqeltrrd	$⊢ φ \to G (S - A (Z)) + G (Q - S) \in ℝ$
206		1red	$⊢ φ \to 1 \in ℝ$
207	16	rpred	$⊢ φ \to E \in ℝ$
208	206 207	readdcld	$⊢ φ \to 1 + E \in ℝ$
209	4	eldifbd	$⊢ φ \to \neg Z \in Y$
210	30 209	eldifd	$⊢ φ \to Z \in (W ∖ Y)$
211	1 173 210 5 8 11 13 14 90	sge0hsphoire	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) \in ℝ$
212	208 211	remulcld	$⊢ φ \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) \in ℝ$
213		fzfid	$⊢ φ \to (1 \dots M) \in Fin$
214	192	adantr	$⊢ (φ \land j \in (1 \dots M)) \to Q - S \in ℝ$
215		simpl	$⊢ (φ \land j \in (1 \dots M)) \to φ$
216		elfznn	$⊢ j \in (1 \dots M) \to j \in ℕ$
217	216	adantl	$⊢ (φ \land j \in (1 \dots M)) \to j \in ℕ$
218		id	$⊢ j \in ℕ \to j \in ℕ$
219		ovexd	$⊢ j \in ℕ \to J (j) L (Y) K (j) \in V$
220	20	fvmpt2	$⊢ (j \in ℕ \land J (j) L (Y) K (j) \in V) \to P (j) = J (j) L (Y) K (j)$
221	218 219 220	syl2anc	$⊢ j \in ℕ \to P (j) = J (j) L (Y) K (j)$
222	221	adantl	$⊢ (φ \land j \in ℕ) \to P (j) = J (j) L (Y) K (j)$
223	173	adantr	$⊢ (φ \land j \in ℕ) \to Y \in Fin$
224	175	a1i	$⊢ (φ \land j \in ℕ) \to Y \subseteq W$
225	125 224	fssresd	$⊢ (φ \land j \in ℕ) \to ({C (j) ↾}_{Y}) : Y ⟶ ℝ$
226	225	adantr	$⊢ ((φ \land j \in ℕ) \land S \in [C (j) (Z), D (j) (Z))) \to ({C (j) ↾}_{Y}) : Y ⟶ ℝ$
227		iftrue	$⊢ S \in [C (j) (Z), D (j) (Z)) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) = {C (j) ↾}_{Y}$
228	227	adantl	$⊢ ((φ \land j \in ℕ) \land S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) = {C (j) ↾}_{Y}$
229	228	feq1d	$⊢ ((φ \land j \in ℕ) \land S \in [C (j) (Z), D (j) (Z))) \to (if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) : Y ⟶ ℝ \leftrightarrow ({C (j) ↾}_{Y}) : Y ⟶ ℝ)$
230	226 229	mpbird	$⊢ ((φ \land j \in ℕ) \land S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) : Y ⟶ ℝ$
231		0red	$⊢ (φ \land y \in Y) \to 0 \in ℝ$
232	231 9	fmptd	$⊢ φ \to F : Y ⟶ ℝ$
233	232	ad2antrr	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to F : Y ⟶ ℝ$
234		iffalse	$⊢ \neg S \in [C (j) (Z), D (j) (Z)) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) = F$
235	234	adantl	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) = F$
236	235	feq1d	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to (if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) : Y ⟶ ℝ \leftrightarrow F : Y ⟶ ℝ)$
237	233 236	mpbird	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) : Y ⟶ ℝ$
238	230 237	pm2.61dan	$⊢ (φ \land j \in ℕ) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) : Y ⟶ ℝ$
239		simpr	$⊢ (φ \land j \in ℕ) \to j \in ℕ$
240		fvex	$⊢ C (j) \in V$
241	240	resex	$⊢ {C (j) ↾}_{Y} \in V$
242	241	a1i	$⊢ φ \to {C (j) ↾}_{Y} \in V$
243	2 3	ssexd	$⊢ φ \to Y \in V$
244		mptexg	$⊢ Y \in V \to (y \in Y ⟼ 0) \in V$
245	243 244	syl	$⊢ φ \to (y \in Y ⟼ 0) \in V$
246	9 245	eqeltrid	$⊢ φ \to F \in V$
247	242 246	ifcld	$⊢ φ \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) \in V$
248	247	adantr	$⊢ (φ \land j \in ℕ) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) \in V$
249	10	fvmpt2	$⊢ (j \in ℕ \land if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) \in V) \to J (j) = if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F)$
250	239 248 249	syl2anc	$⊢ (φ \land j \in ℕ) \to J (j) = if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F)$
251	250	feq1d	$⊢ (φ \land j \in ℕ) \to (J (j) : Y ⟶ ℝ \leftrightarrow if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) : Y ⟶ ℝ)$
252	238 251	mpbird	$⊢ (φ \land j \in ℕ) \to J (j) : Y ⟶ ℝ$
253	49 224	fssresd	$⊢ (φ \land j \in ℕ) \to ({D (j) ↾}_{Y}) : Y ⟶ ℝ$
254	253	adantr	$⊢ ((φ \land j \in ℕ) \land S \in [C (j) (Z), D (j) (Z))) \to ({D (j) ↾}_{Y}) : Y ⟶ ℝ$
255		iftrue	$⊢ S \in [C (j) (Z), D (j) (Z)) \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) = {D (j) ↾}_{Y}$
256	255	adantl	$⊢ ((φ \land j \in ℕ) \land S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) = {D (j) ↾}_{Y}$
257	256	feq1d	$⊢ ((φ \land j \in ℕ) \land S \in [C (j) (Z), D (j) (Z))) \to (if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) : Y ⟶ ℝ \leftrightarrow ({D (j) ↾}_{Y}) : Y ⟶ ℝ)$
258	254 257	mpbird	$⊢ ((φ \land j \in ℕ) \land S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) : Y ⟶ ℝ$
259		iffalse	$⊢ \neg S \in [C (j) (Z), D (j) (Z)) \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) = F$
260	259	adantl	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) = F$
261	260	feq1d	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to (if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) : Y ⟶ ℝ \leftrightarrow F : Y ⟶ ℝ)$
262	233 261	mpbird	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) : Y ⟶ ℝ$
263	258 262	pm2.61dan	$⊢ (φ \land j \in ℕ) \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) : Y ⟶ ℝ$
264		fvex	$⊢ D (j) \in V$
265	264	resex	$⊢ {D (j) ↾}_{Y} \in V$
266	265	a1i	$⊢ φ \to {D (j) ↾}_{Y} \in V$
267	266 246	ifcld	$⊢ φ \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) \in V$
268	267	adantr	$⊢ (φ \land j \in ℕ) \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) \in V$
269	12	fvmpt2	$⊢ (j \in ℕ \land if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) \in V) \to K (j) = if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F)$
270	239 268 269	syl2anc	$⊢ (φ \land j \in ℕ) \to K (j) = if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F)$
271	270	feq1d	$⊢ (φ \land j \in ℕ) \to (K (j) : Y ⟶ ℝ \leftrightarrow if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) : Y ⟶ ℝ)$
272	263 271	mpbird	$⊢ (φ \land j \in ℕ) \to K (j) : Y ⟶ ℝ$
273	1 223 252 272	hoidmvcl	$⊢ (φ \land j \in ℕ) \to J (j) L (Y) K (j) \in [0, +∞)$
274	222 273	eqeltrd	$⊢ (φ \land j \in ℕ) \to P (j) \in [0, +∞)$
275	172 274	sselid	$⊢ (φ \land j \in ℕ) \to P (j) \in ℝ$
276	215 217 275	syl2anc	$⊢ (φ \land j \in (1 \dots M)) \to P (j) \in ℝ$
277	214 276	remulcld	$⊢ (φ \land j \in (1 \dots M)) \to (Q - S) P (j) \in ℝ$
278	213 277	fsumrecl	$⊢ φ \to \sum_{j = 1}^{M} (Q - S) P (j) \in ℝ$
279	208 278	remulcld	$⊢ φ \to (1 + E) \sum_{j = 1}^{M} (Q - S) P (j) \in ℝ$
280	212 279	readdcld	$⊢ φ \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) + (1 + E) \sum_{j = 1}^{M} (Q - S) P (j) \in ℝ$
281	1 173 210 5 8 11 13 14 84	sge0hsphoire	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) H (Q) (D (j)))) \in ℝ$
282	208 281	remulcld	$⊢ φ \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (Q) (D (j)))) \in ℝ$
283	18 17	eleqtrdi	$⊢ φ \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))))\}$
284		oveq1	$⊢ z = S \to z - A (Z) = S - A (Z)$
285	284	oveq2d	$⊢ z = S \to G (z - A (Z)) = G (S - A (Z))$
286		fveq2	$⊢ z = S \to H (z) = H (S)$
287	286	fveq1d	$⊢ z = S \to H (z) (D (j)) = H (S) (D (j))$
288	287	oveq2d	$⊢ z = S \to C (j) L (W) H (z) (D (j)) = C (j) L (W) H (S) (D (j))$
289	288	mpteq2dv	$⊢ z = S \to (j \in ℕ ⟼ C (j) L (W) H (z) (D (j))) = (j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))$
290	289	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))))$
291	290	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))))$
292	285 291	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)))))$
293	292	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)))))$
294	283 293	sylib	$⊢ φ \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)))))$
295	294	simprd	$⊢ φ \to G (S - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j))))$
296	213 276	fsumrecl	$⊢ φ \to \sum_{j = 1}^{M} P (j) \in ℝ$
297	208 296	remulcld	$⊢ φ \to (1 + E) \sum_{j = 1}^{M} P (j) \in ℝ$
298		0red	$⊢ φ \to 0 \in ℝ$
299	90 84	posdifd	$⊢ φ \to (S < Q \leftrightarrow 0 < Q - S)$
300	157 299	mpbid	$⊢ φ \to 0 < Q - S$
301	298 192 300	ltled	$⊢ φ \to 0 \leq Q - S$
302	181 297 192 301 22	lemul1ad	$⊢ φ \to G (Q - S) \leq (1 + E) \sum_{j = 1}^{M} P (j) (Q - S)$
303	208	recnd	$⊢ φ \to 1 + E \in ℂ$
304	296	recnd	$⊢ φ \to \sum_{j = 1}^{M} P (j) \in ℂ$
305	303 304 183	mulassd	$⊢ φ \to (1 + E) \sum_{j = 1}^{M} P (j) (Q - S) = (1 + E) \sum_{j = 1}^{M} P (j) (Q - S)$
306	276	recnd	$⊢ (φ \land j \in (1 \dots M)) \to P (j) \in ℂ$
307	213 183 306	fsummulc1	$⊢ φ \to \sum_{j = 1}^{M} P (j) (Q - S) = \sum_{j = 1}^{M} P (j) (Q - S)$
308	183	adantr	$⊢ (φ \land j \in (1 \dots M)) \to Q - S \in ℂ$
309	306 308	mulcomd	$⊢ (φ \land j \in (1 \dots M)) \to P (j) (Q - S) = (Q - S) P (j)$
310	309	sumeq2dv	$⊢ φ \to \sum_{j = 1}^{M} P (j) (Q - S) = \sum_{j = 1}^{M} (Q - S) P (j)$
311	307 310	eqtrd	$⊢ φ \to \sum_{j = 1}^{M} P (j) (Q - S) = \sum_{j = 1}^{M} (Q - S) P (j)$
312	311	oveq2d	$⊢ φ \to (1 + E) \sum_{j = 1}^{M} P (j) (Q - S) = (1 + E) \sum_{j = 1}^{M} (Q - S) P (j)$
313	305 312	eqtrd	$⊢ φ \to (1 + E) \sum_{j = 1}^{M} P (j) (Q - S) = (1 + E) \sum_{j = 1}^{M} (Q - S) P (j)$
314	302 313	breqtrd	$⊢ φ \to G (Q - S) \leq (1 + E) \sum_{j = 1}^{M} (Q - S) P (j)$
315	201 195 212 279 295 314	le2addd	$⊢ φ \to G (S - A (Z)) + G (Q - S) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) + (1 + E) \sum_{j = 1}^{M} (Q - S) P (j)$
316		nnsplit	$⊢ M \in ℕ \to ℕ = (1 \dots M) \cup ℤ_{\geq (M + 1)}$
317	21 316	syl	$⊢ φ \to ℕ = (1 \dots M) \cup ℤ_{\geq (M + 1)}$
318		uncom	$⊢ (1 \dots M) \cup ℤ_{\geq (M + 1)} = ℤ_{\geq (M + 1)} \cup (1 \dots M)$
319	318	a1i	$⊢ φ \to (1 \dots M) \cup ℤ_{\geq (M + 1)} = ℤ_{\geq (M + 1)} \cup (1 \dots M)$
320	317 319	eqtr2d	$⊢ φ \to ℤ_{\geq (M + 1)} \cup (1 \dots M) = ℕ$
321	320	eqcomd	$⊢ φ \to ℕ = ℤ_{\geq (M + 1)} \cup (1 \dots M)$
322	321	mpteq1d	$⊢ φ \to (j \in ℕ ⟼ C (j) L (W) H (S) (D (j))) = (j \in (ℤ_{\geq (M + 1)} \cup (1 \dots M)) ⟼ C (j) L (W) H (S) (D (j)))$
323	322	fveq2d	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) = sum^((j \in (ℤ_{\geq (M + 1)} \cup (1 \dots M)) ⟼ C (j) L (W) H (S) (D (j))))$
324		nfv	$⊢ Ⅎ j φ$
325		fvexd	$⊢ φ \to ℤ_{\geq (M + 1)} \in V$
326		ovexd	$⊢ φ \to (1 \dots M) \in V$
327		incom	$⊢ ℤ_{\geq (M + 1)} \cap (1 \dots M) = (1 \dots M) \cap ℤ_{\geq (M + 1)}$
328		nnuzdisj	$⊢ (1 \dots M) \cap ℤ_{\geq (M + 1)} = \emptyset$
329	327 328	eqtri	$⊢ ℤ_{\geq (M + 1)} \cap (1 \dots M) = \emptyset$
330	329	a1i	$⊢ φ \to ℤ_{\geq (M + 1)} \cap (1 \dots M) = \emptyset$
331		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
332		ssid	$⊢ [0, +∞) \subseteq [0, +∞)$
333		simpl	$⊢ (φ \land j \in ℤ_{\geq (M + 1)}) \to φ$
334	21	peano2nnd	$⊢ φ \to M + 1 \in ℕ$
335		uznnssnn	$⊢ M + 1 \in ℕ \to ℤ_{\geq (M + 1)} \subseteq ℕ$
336	334 335	syl	$⊢ φ \to ℤ_{\geq (M + 1)} \subseteq ℕ$
337	336	adantr	$⊢ (φ \land j \in ℤ_{\geq (M + 1)}) \to ℤ_{\geq (M + 1)} \subseteq ℕ$
338		simpr	$⊢ (φ \land j \in ℤ_{\geq (M + 1)}) \to j \in ℤ_{\geq (M + 1)}$
339	337 338	sseldd	$⊢ (φ \land j \in ℤ_{\geq (M + 1)}) \to j \in ℕ$
340		snfi	$⊢ \{Z\} \in Fin$
341	340	a1i	$⊢ φ \to \{Z\} \in Fin$
342		unfi	$⊢ (Y \in Fin \land \{Z\} \in Fin) \to Y \cup \{Z\} \in Fin$
343	173 341 342	syl2anc	$⊢ φ \to Y \cup \{Z\} \in Fin$
344	5 343	eqeltrid	$⊢ φ \to W \in Fin$
345	344	adantr	$⊢ (φ \land j \in ℕ) \to W \in Fin$
346		eleq1w	$⊢ j = l \to (j \in Y \leftrightarrow l \in Y)$
347		fveq2	$⊢ j = l \to c (j) = c (l)$
348	347	breq1d	$⊢ j = l \to (c (j) \leq x \leftrightarrow c (l) \leq x)$
349	348 347	ifbieq1d	$⊢ j = l \to if (c (j) \leq x, c (j), x) = if (c (l) \leq x, c (l), x)$
350	346 347 349	ifbieq12d	$⊢ j = l \to if (j \in Y, c (j), if (c (j) \leq x, c (j), x)) = if (l \in Y, c (l), if (c (l) \leq x, c (l), x))$
351	350	cbvmptv	$⊢ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x))) = (l \in W ⟼ if (l \in Y, c (l), if (c (l) \leq x, c (l), x)))$
352	351	mpteq2i	$⊢ (c \in (ℝ^{W}) ⟼ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x)))) = (c \in (ℝ^{W}) ⟼ (l \in W ⟼ if (l \in Y, c (l), if (c (l) \leq x, c (l), x))))$
353	352	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}) ⟼ (l \in W ⟼ if (l \in Y, c (l), if (c (l) \leq x, c (l), x)))))$
354	14 353	eqtri	$⊢ H = (x \in ℝ ⟼ (c \in (ℝ^{W}) ⟼ (l \in W ⟼ if (l \in Y, c (l), if (c (l) \leq x, c (l), x)))))$
355	90	adantr	$⊢ (φ \land j \in ℕ) \to S \in ℝ$
356	354 355 345 49	hsphoif	$⊢ (φ \land j \in ℕ) \to H (S) (D (j)) : W ⟶ ℝ$
357	1 345 125 356	hoidmvcl	$⊢ (φ \land j \in ℕ) \to C (j) L (W) H (S) (D (j)) \in [0, +∞)$
358	333 339 357	syl2anc	$⊢ (φ \land j \in ℤ_{\geq (M + 1)}) \to C (j) L (W) H (S) (D (j)) \in [0, +∞)$
359	332 358	sselid	$⊢ (φ \land j \in ℤ_{\geq (M + 1)}) \to C (j) L (W) H (S) (D (j)) \in [0, +∞)$
360	331 359	sselid	$⊢ (φ \land j \in ℤ_{\geq (M + 1)}) \to C (j) L (W) H (S) (D (j)) \in [0, +∞]$
361	215 217 357	syl2anc	$⊢ (φ \land j \in (1 \dots M)) \to C (j) L (W) H (S) (D (j)) \in [0, +∞)$
362	331 361	sselid	$⊢ (φ \land j \in (1 \dots M)) \to C (j) L (W) H (S) (D (j)) \in [0, +∞]$
363	324 325 326 330 360 362	sge0splitmpt	$⊢ φ \to sum^((j \in (ℤ_{\geq (M + 1)} \cup (1 \dots M)) ⟼ C (j) L (W) H (S) (D (j)))) = sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) +_{𝑒} sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j))))$
364		nnex	$⊢ ℕ \in V$
365	364	a1i	$⊢ φ \to ℕ \in V$
366	331 357	sselid	$⊢ (φ \land j \in ℕ) \to C (j) L (W) H (S) (D (j)) \in [0, +∞]$
367	324 365 366 211 336	sge0ssrempt	$⊢ φ \to sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) \in ℝ$
368	37	a1i	$⊢ φ \to (1 \dots M) \subseteq ℕ$
369	324 365 366 211 368	sge0ssrempt	$⊢ φ \to sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j)))) \in ℝ$
370		rexadd	$⊢ (sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) \in ℝ \land sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j)))) \in ℝ) \to sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) +_{𝑒} sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j)))) = sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j))))$
371	367 369 370	syl2anc	$⊢ φ \to sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) +_{𝑒} sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j)))) = sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j))))$
372	323 363 371	3eqtrd	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) = sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j))))$
373	372	oveq2d	$⊢ φ \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) = (1 + E) (sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j)))))$
374	373	oveq1d	$⊢ φ \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) + (1 + E) \sum_{j = 1}^{M} (Q - S) P (j) = (1 + E) (sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j))))) + (1 + E) \sum_{j = 1}^{M} (Q - S) P (j)$
375	372 211	eqeltrrd	$⊢ φ \to sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j)))) \in ℝ$
376	375	recnd	$⊢ φ \to sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j)))) \in ℂ$
377	278	recnd	$⊢ φ \to \sum_{j = 1}^{M} (Q - S) P (j) \in ℂ$
378	303 376 377	adddid	$⊢ φ \to (1 + E) (sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j)))) + \sum_{j = 1}^{M} (Q - S) P (j)) = (1 + E) (sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j))))) + (1 + E) \sum_{j = 1}^{M} (Q - S) P (j)$
379	378	eqcomd	$⊢ φ \to (1 + E) (sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j))))) + (1 + E) \sum_{j = 1}^{M} (Q - S) P (j) = (1 + E) (sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j)))) + \sum_{j = 1}^{M} (Q - S) P (j))$
380	367	recnd	$⊢ φ \to sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) \in ℂ$
381	369	recnd	$⊢ φ \to sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j)))) \in ℂ$
382	380 381 377	addassd	$⊢ φ \to sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j)))) + \sum_{j = 1}^{M} (Q - S) P (j) = sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j)))) + \sum_{j = 1}^{M} (Q - S) P (j)$
383	213 361	sge0fsummpt	$⊢ φ \to sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j)))) = \sum_{j = 1}^{M} (C (j) L (W) H (S) (D (j)))$
384	383	oveq1d	$⊢ φ \to sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j)))) + \sum_{j = 1}^{M} (Q - S) P (j) = \sum_{j = 1}^{M} (C (j) L (W) H (S) (D (j))) + \sum_{j = 1}^{M} (Q - S) P (j)$
385		ax-resscn	$⊢ ℝ \subseteq ℂ$
386	172 385	sstri	$⊢ [0, +∞) \subseteq ℂ$
387	386 357	sselid	$⊢ (φ \land j \in ℕ) \to C (j) L (W) H (S) (D (j)) \in ℂ$
388	215 217 387	syl2anc	$⊢ (φ \land j \in (1 \dots M)) \to C (j) L (W) H (S) (D (j)) \in ℂ$
389	192	adantr	$⊢ (φ \land j \in ℕ) \to Q - S \in ℝ$
390	389 275	remulcld	$⊢ (φ \land j \in ℕ) \to (Q - S) P (j) \in ℝ$
391	390	recnd	$⊢ (φ \land j \in ℕ) \to (Q - S) P (j) \in ℂ$
392	217 391	syldan	$⊢ (φ \land j \in (1 \dots M)) \to (Q - S) P (j) \in ℂ$
393	213 388 392	fsumadd	$⊢ φ \to \sum_{j = 1}^{M} ((C (j) L (W) H (S) (D (j))) + (Q - S) P (j)) = \sum_{j = 1}^{M} (C (j) L (W) H (S) (D (j))) + \sum_{j = 1}^{M} (Q - S) P (j)$
394	393	eqcomd	$⊢ φ \to \sum_{j = 1}^{M} (C (j) L (W) H (S) (D (j))) + \sum_{j = 1}^{M} (Q - S) P (j) = \sum_{j = 1}^{M} ((C (j) L (W) H (S) (D (j))) + (Q - S) P (j))$
395	384 394	eqtrd	$⊢ φ \to sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j)))) + \sum_{j = 1}^{M} (Q - S) P (j) = \sum_{j = 1}^{M} ((C (j) L (W) H (S) (D (j))) + (Q - S) P (j))$
396	395	oveq2d	$⊢ φ \to sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j)))) + \sum_{j = 1}^{M} (Q - S) P (j) = sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + \sum_{j = 1}^{M} ((C (j) L (W) H (S) (D (j))) + (Q - S) P (j))$
397	382 396	eqtrd	$⊢ φ \to sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j)))) + \sum_{j = 1}^{M} (Q - S) P (j) = sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + \sum_{j = 1}^{M} ((C (j) L (W) H (S) (D (j))) + (Q - S) P (j))$
398	397	oveq2d	$⊢ φ \to (1 + E) (sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (S) (D (j)))) + \sum_{j = 1}^{M} (Q - S) P (j)) = (1 + E) (sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + \sum_{j = 1}^{M} ((C (j) L (W) H (S) (D (j))) + (Q - S) P (j)))$
399	374 379 398	3eqtrd	$⊢ φ \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) + (1 + E) \sum_{j = 1}^{M} (Q - S) P (j) = (1 + E) (sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + \sum_{j = 1}^{M} ((C (j) L (W) H (S) (D (j))) + (Q - S) P (j)))$
400	172 357	sselid	$⊢ (φ \land j \in ℕ) \to C (j) L (W) H (S) (D (j)) \in ℝ$
401	400 390	readdcld	$⊢ (φ \land j \in ℕ) \to (C (j) L (W) H (S) (D (j))) + (Q - S) P (j) \in ℝ$
402	215 217 401	syl2anc	$⊢ (φ \land j \in (1 \dots M)) \to (C (j) L (W) H (S) (D (j))) + (Q - S) P (j) \in ℝ$
403	213 402	fsumrecl	$⊢ φ \to \sum_{j = 1}^{M} ((C (j) L (W) H (S) (D (j))) + (Q - S) P (j)) \in ℝ$
404	367 403	readdcld	$⊢ φ \to sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + \sum_{j = 1}^{M} ((C (j) L (W) H (S) (D (j))) + (Q - S) P (j)) \in ℝ$
405		0le1	$⊢ 0 \leq 1$
406	405	a1i	$⊢ φ \to 0 \leq 1$
407	16	rpge0d	$⊢ φ \to 0 \leq E$
408	206 207 406 407	addge0d	$⊢ φ \to 0 \leq 1 + E$
409	84	adantr	$⊢ (φ \land j \in ℕ) \to Q \in ℝ$
410	354 409 345 49	hsphoif	$⊢ (φ \land j \in ℕ) \to H (Q) (D (j)) : W ⟶ ℝ$
411	1 345 125 410	hoidmvcl	$⊢ (φ \land j \in ℕ) \to C (j) L (W) H (Q) (D (j)) \in [0, +∞)$
412	331 411	sselid	$⊢ (φ \land j \in ℕ) \to C (j) L (W) H (Q) (D (j)) \in [0, +∞]$
413	324 365 412 281 336	sge0ssrempt	$⊢ φ \to sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (Q) (D (j)))) \in ℝ$
414	172 411	sselid	$⊢ (φ \land j \in ℕ) \to C (j) L (W) H (Q) (D (j)) \in ℝ$
415	215 217 414	syl2anc	$⊢ (φ \land j \in (1 \dots M)) \to C (j) L (W) H (Q) (D (j)) \in ℝ$
416	213 415	fsumrecl	$⊢ φ \to \sum_{j = 1}^{M} (C (j) L (W) H (Q) (D (j))) \in ℝ$
417	333 339 412	syl2anc	$⊢ (φ \land j \in ℤ_{\geq (M + 1)}) \to C (j) L (W) H (Q) (D (j)) \in [0, +∞]$
418	210	adantr	$⊢ (φ \land j \in ℕ) \to Z \in (W ∖ Y)$
419	90 84 157	ltled	$⊢ φ \to S \leq Q$
420	419	adantr	$⊢ (φ \land j \in ℕ) \to S \leq Q$
421	1 345 418 5 355 409 420 354 125 49	hsphoidmvle2	$⊢ (φ \land j \in ℕ) \to C (j) L (W) H (S) (D (j)) \leq C (j) L (W) H (Q) (D (j))$
422	333 339 421	syl2anc	$⊢ (φ \land j \in ℤ_{\geq (M + 1)}) \to C (j) L (W) H (S) (D (j)) \leq C (j) L (W) H (Q) (D (j))$
423	324 325 360 417 422	sge0lempt	$⊢ φ \to sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) \leq sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (Q) (D (j))))$
424	215	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) = 0) \to φ$
425	217	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) = 0) \to j \in ℕ$
426		simpr	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) = 0) \to P (j) = 0$
427		oveq2	$⊢ P (j) = 0 \to (Q - S) P (j) = (Q - S) \cdot 0$
428	427	adantl	$⊢ ((φ \land j \in ℕ) \land P (j) = 0) \to (Q - S) P (j) = (Q - S) \cdot 0$
429	183	mul01d	$⊢ φ \to (Q - S) \cdot 0 = 0$
430	429	ad2antrr	$⊢ ((φ \land j \in ℕ) \land P (j) = 0) \to (Q - S) \cdot 0 = 0$
431	428 430	eqtrd	$⊢ ((φ \land j \in ℕ) \land P (j) = 0) \to (Q - S) P (j) = 0$
432	431	oveq2d	$⊢ ((φ \land j \in ℕ) \land P (j) = 0) \to (C (j) L (W) H (S) (D (j))) + (Q - S) P (j) = (C (j) L (W) H (S) (D (j))) + 0$
433	387	addridd	$⊢ (φ \land j \in ℕ) \to (C (j) L (W) H (S) (D (j))) + 0 = C (j) L (W) H (S) (D (j))$
434	433	adantr	$⊢ ((φ \land j \in ℕ) \land P (j) = 0) \to (C (j) L (W) H (S) (D (j))) + 0 = C (j) L (W) H (S) (D (j))$
435	432 434	eqtrd	$⊢ ((φ \land j \in ℕ) \land P (j) = 0) \to (C (j) L (W) H (S) (D (j))) + (Q - S) P (j) = C (j) L (W) H (S) (D (j))$
436	421	adantr	$⊢ ((φ \land j \in ℕ) \land P (j) = 0) \to C (j) L (W) H (S) (D (j)) \leq C (j) L (W) H (Q) (D (j))$
437	435 436	eqbrtrd	$⊢ ((φ \land j \in ℕ) \land P (j) = 0) \to (C (j) L (W) H (S) (D (j))) + (Q - S) P (j) \leq C (j) L (W) H (Q) (D (j))$
438	424 425 426 437	syl21anc	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) = 0) \to (C (j) L (W) H (S) (D (j))) + (Q - S) P (j) \leq C (j) L (W) H (Q) (D (j))$
439		simpl	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P (j) = 0) \to (φ \land j \in (1 \dots M))$
440		neqne	$⊢ \neg P (j) = 0 \to P (j) \neq 0$
441	440	adantl	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P (j) = 0) \to P (j) \neq 0$
442	402	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to (C (j) L (W) H (S) (D (j))) + (Q - S) P (j) \in ℝ$
443	215	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to φ$
444	217	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to j \in ℕ$
445		simpr	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to P (j) \neq 0$
446	4	adantr	$⊢ (φ \land j \in ℕ) \to Z \in (X ∖ Y)$
447	209	adantr	$⊢ (φ \land j \in ℕ) \to \neg Z \in Y$
448		eqid	$⊢ \prod_{k \in Y} vol ([C (j) (k), H (S) (D (j)) (k))) = \prod_{k \in Y} vol ([C (j) (k), H (S) (D (j)) (k)))$
449	1 223 446 447 5 125 356 448	hoiprodp1	$⊢ (φ \land j \in ℕ) \to C (j) L (W) H (S) (D (j)) = \prod_{k \in Y} vol ([C (j) (k), H (S) (D (j)) (k))) vol ([C (j) (Z), H (S) (D (j)) (Z)))$
450	449	adantr	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to C (j) L (W) H (S) (D (j)) = \prod_{k \in Y} vol ([C (j) (k), H (S) (D (j)) (k))) vol ([C (j) (Z), H (S) (D (j)) (Z)))$
451	222	adantr	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to P (j) = J (j) L (Y) K (j)$
452	223	adantr	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to Y \in Fin$
453	222	adantr	$⊢ ((φ \land j \in ℕ) \land Y = \emptyset) \to P (j) = J (j) L (Y) K (j)$
454		fveq2	$⊢ Y = \emptyset \to L (Y) = L (\emptyset)$
455	454	oveqd	$⊢ Y = \emptyset \to J (j) L (Y) K (j) = J (j) L (\emptyset) K (j)$
456	455	adantl	$⊢ ((φ \land j \in ℕ) \land Y = \emptyset) \to J (j) L (Y) K (j) = J (j) L (\emptyset) K (j)$
457	252	adantr	$⊢ ((φ \land j \in ℕ) \land Y = \emptyset) \to J (j) : Y ⟶ ℝ$
458		id	$⊢ Y = \emptyset \to Y = \emptyset$
459	458	eqcomd	$⊢ Y = \emptyset \to \emptyset = Y$
460	459	adantl	$⊢ ((φ \land j \in ℕ) \land Y = \emptyset) \to \emptyset = Y$
461	460	feq2d	$⊢ ((φ \land j \in ℕ) \land Y = \emptyset) \to (J (j) : \emptyset ⟶ ℝ \leftrightarrow J (j) : Y ⟶ ℝ)$
462	457 461	mpbird	$⊢ ((φ \land j \in ℕ) \land Y = \emptyset) \to J (j) : \emptyset ⟶ ℝ$
463	272	adantr	$⊢ ((φ \land j \in ℕ) \land Y = \emptyset) \to K (j) : Y ⟶ ℝ$
464	460	feq2d	$⊢ ((φ \land j \in ℕ) \land Y = \emptyset) \to (K (j) : \emptyset ⟶ ℝ \leftrightarrow K (j) : Y ⟶ ℝ)$
465	463 464	mpbird	$⊢ ((φ \land j \in ℕ) \land Y = \emptyset) \to K (j) : \emptyset ⟶ ℝ$
466	1 462 465	hoidmv0val	$⊢ ((φ \land j \in ℕ) \land Y = \emptyset) \to J (j) L (\emptyset) K (j) = 0$
467	453 456 466	3eqtrd	$⊢ ((φ \land j \in ℕ) \land Y = \emptyset) \to P (j) = 0$
468	467	adantlr	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land Y = \emptyset) \to P (j) = 0$
469		neneq	$⊢ P (j) \neq 0 \to \neg P (j) = 0$
470	469	ad2antlr	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land Y = \emptyset) \to \neg P (j) = 0$
471	468 470	pm2.65da	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to \neg Y = \emptyset$
472	471	neqned	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to Y \neq \emptyset$
473	252	adantr	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to J (j) : Y ⟶ ℝ$
474	272	adantr	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to K (j) : Y ⟶ ℝ$
475	1 452 472 473 474	hoidmvn0val	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to J (j) L (Y) K (j) = \prod_{k \in Y} vol ([J (j) (k), K (j) (k)))$
476	250	adantr	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to J (j) = if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F)$
477	222	adantr	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to P (j) = J (j) L (Y) K (j)$
478	250	adantr	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to J (j) = if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F)$
479	478 235	eqtrd	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to J (j) = F$
480	270	adantr	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to K (j) = if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F)$
481	480 260	eqtrd	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to K (j) = F$
482	479 481	oveq12d	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to J (j) L (Y) K (j) = F L (Y) F$
483	1 173 232	hoidmvval0b	$⊢ φ \to F L (Y) F = 0$
484	483	ad2antrr	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to F L (Y) F = 0$
485	477 482 484	3eqtrd	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to P (j) = 0$
486	485	adantlr	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land \neg S \in [C (j) (Z), D (j) (Z))) \to P (j) = 0$
487	469	ad2antlr	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land \neg S \in [C (j) (Z), D (j) (Z))) \to \neg P (j) = 0$
488	486 487	condan	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to S \in [C (j) (Z), D (j) (Z))$
489	488	iftrued	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) = {C (j) ↾}_{Y}$
490	476 489	eqtrd	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to J (j) = {C (j) ↾}_{Y}$
491	490	fveq1d	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to J (j) (k) = ({C (j) ↾}_{Y}) (k)$
492	491	adantr	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land k \in Y) \to J (j) (k) = ({C (j) ↾}_{Y}) (k)$
493		fvres	$⊢ k \in Y \to ({C (j) ↾}_{Y}) (k) = C (j) (k)$
494	493	adantl	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land k \in Y) \to ({C (j) ↾}_{Y}) (k) = C (j) (k)$
495	492 494	eqtrd	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land k \in Y) \to J (j) (k) = C (j) (k)$
496	270	adantr	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to K (j) = if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F)$
497	488 255	syl	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) = {D (j) ↾}_{Y}$
498	496 497	eqtrd	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to K (j) = {D (j) ↾}_{Y}$
499	498	fveq1d	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to K (j) (k) = ({D (j) ↾}_{Y}) (k)$
500	499	adantr	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land k \in Y) \to K (j) (k) = ({D (j) ↾}_{Y}) (k)$
501		fvres	$⊢ k \in Y \to ({D (j) ↾}_{Y}) (k) = D (j) (k)$
502	501	adantl	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land k \in Y) \to ({D (j) ↾}_{Y}) (k) = D (j) (k)$
503	500 502	eqtrd	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land k \in Y) \to K (j) (k) = D (j) (k)$
504	495 503	oveq12d	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land k \in Y) \to [J (j) (k), K (j) (k)) = [C (j) (k), D (j) (k))$
505	504	fveq2d	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land k \in Y) \to vol ([J (j) (k), K (j) (k))) = vol ([C (j) (k), D (j) (k)))$
506	505	prodeq2dv	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to \prod_{k \in Y} vol ([J (j) (k), K (j) (k))) = \prod_{k \in Y} vol ([C (j) (k), D (j) (k)))$
507	475 506	eqtrd	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to J (j) L (Y) K (j) = \prod_{k \in Y} vol ([C (j) (k), D (j) (k)))$
508	355	adantr	$⊢ ((φ \land j \in ℕ) \land k \in Y) \to S \in ℝ$
509	345	adantr	$⊢ ((φ \land j \in ℕ) \land k \in Y) \to W \in Fin$
510	49	adantr	$⊢ ((φ \land j \in ℕ) \land k \in Y) \to D (j) : W ⟶ ℝ$
511		elun1	$⊢ k \in Y \to k \in (Y \cup \{Z\})$
512	511 5	eleqtrrdi	$⊢ k \in Y \to k \in W$
513	512	adantl	$⊢ ((φ \land j \in ℕ) \land k \in Y) \to k \in W$
514	354 508 509 510 513	hsphoival	$⊢ ((φ \land j \in ℕ) \land k \in Y) \to H (S) (D (j)) (k) = if (k \in Y, D (j) (k), if (D (j) (k) \leq S, D (j) (k), S))$
515		iftrue	$⊢ k \in Y \to if (k \in Y, D (j) (k), if (D (j) (k) \leq S, D (j) (k), S)) = D (j) (k)$
516	515	adantl	$⊢ ((φ \land j \in ℕ) \land k \in Y) \to if (k \in Y, D (j) (k), if (D (j) (k) \leq S, D (j) (k), S)) = D (j) (k)$
517	514 516	eqtrd	$⊢ ((φ \land j \in ℕ) \land k \in Y) \to H (S) (D (j)) (k) = D (j) (k)$
518	517	oveq2d	$⊢ ((φ \land j \in ℕ) \land k \in Y) \to [C (j) (k), H (S) (D (j)) (k)) = [C (j) (k), D (j) (k))$
519	518	fveq2d	$⊢ ((φ \land j \in ℕ) \land k \in Y) \to vol ([C (j) (k), H (S) (D (j)) (k))) = vol ([C (j) (k), D (j) (k)))$
520	519	prodeq2dv	$⊢ (φ \land j \in ℕ) \to \prod_{k \in Y} vol ([C (j) (k), H (S) (D (j)) (k))) = \prod_{k \in Y} vol ([C (j) (k), D (j) (k)))$
521	520	eqcomd	$⊢ (φ \land j \in ℕ) \to \prod_{k \in Y} vol ([C (j) (k), D (j) (k))) = \prod_{k \in Y} vol ([C (j) (k), H (S) (D (j)) (k)))$
522	521	adantr	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to \prod_{k \in Y} vol ([C (j) (k), D (j) (k))) = \prod_{k \in Y} vol ([C (j) (k), H (S) (D (j)) (k)))$
523	451 507 522	3eqtrrd	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to \prod_{k \in Y} vol ([C (j) (k), H (S) (D (j)) (k))) = P (j)$
524	354 355 345 49 50	hsphoival	$⊢ (φ \land j \in ℕ) \to H (S) (D (j)) (Z) = if (Z \in Y, D (j) (Z), if (D (j) (Z) \leq S, D (j) (Z), S))$
525	209	iffalsed	$⊢ φ \to if (Z \in Y, D (j) (Z), if (D (j) (Z) \leq S, D (j) (Z), S)) = if (D (j) (Z) \leq S, D (j) (Z), S)$
526	525	adantr	$⊢ (φ \land j \in ℕ) \to if (Z \in Y, D (j) (Z), if (D (j) (Z) \leq S, D (j) (Z), S)) = if (D (j) (Z) \leq S, D (j) (Z), S)$
527	524 526	eqtrd	$⊢ (φ \land j \in ℕ) \to H (S) (D (j)) (Z) = if (D (j) (Z) \leq S, D (j) (Z), S)$
528	527	oveq2d	$⊢ (φ \land j \in ℕ) \to [C (j) (Z), H (S) (D (j)) (Z)) = [C (j) (Z), if (D (j) (Z) \leq S, D (j) (Z), S))$
529	528	adantr	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to [C (j) (Z), H (S) (D (j)) (Z)) = [C (j) (Z), if (D (j) (Z) \leq S, D (j) (Z), S))$
530	126	rexrd	$⊢ (φ \land j \in ℕ) \to C (j) (Z) \in ℝ^{*}$
531	530	adantr	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to C (j) (Z) \in ℝ^{*}$
532	51	rexrd	$⊢ (φ \land j \in ℕ) \to D (j) (Z) \in ℝ^{*}$
533	532	adantr	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to D (j) (Z) \in ℝ^{*}$
534		icoltub	$⊢ (C (j) (Z) \in ℝ^{} \land D (j) (Z) \in ℝ^{} \land S \in [C (j) (Z), D (j) (Z))) \to S < D (j) (Z)$
535	531 533 488 534	syl3anc	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to S < D (j) (Z)$
536	355	adantr	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to S \in ℝ$
537	51	adantr	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to D (j) (Z) \in ℝ$
538	536 537	ltnled	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to (S < D (j) (Z) \leftrightarrow \neg D (j) (Z) \leq S)$
539	535 538	mpbid	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to \neg D (j) (Z) \leq S$
540	539	iffalsed	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to if (D (j) (Z) \leq S, D (j) (Z), S) = S$
541	540	oveq2d	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to [C (j) (Z), if (D (j) (Z) \leq S, D (j) (Z), S)) = [C (j) (Z), S)$
542	529 541	eqtrd	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to [C (j) (Z), H (S) (D (j)) (Z)) = [C (j) (Z), S)$
543	542	fveq2d	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to vol ([C (j) (Z), H (S) (D (j)) (Z))) = vol ([C (j) (Z), S))$
544		volico	$⊢ (C (j) (Z) \in ℝ \land S \in ℝ) \to vol ([C (j) (Z), S)) = if (C (j) (Z) < S, S - C (j) (Z), 0)$
545	126 536 544	syl2an	$⊢ ((φ \land j \in ℕ) \land ((φ \land j \in ℕ) \land P (j) \neq 0)) \to vol ([C (j) (Z), S)) = if (C (j) (Z) < S, S - C (j) (Z), 0)$
546	545	anabss5	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to vol ([C (j) (Z), S)) = if (C (j) (Z) < S, S - C (j) (Z), 0)$
547		iftrue	$⊢ C (j) (Z) < S \to if (C (j) (Z) < S, S - C (j) (Z), 0) = S - C (j) (Z)$
548	547	adantl	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land C (j) (Z) < S) \to if (C (j) (Z) < S, S - C (j) (Z), 0) = S - C (j) (Z)$
549		iffalse	$⊢ \neg C (j) (Z) < S \to if (C (j) (Z) < S, S - C (j) (Z), 0) = 0$
550	549	adantl	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land \neg C (j) (Z) < S) \to if (C (j) (Z) < S, S - C (j) (Z), 0) = 0$
551		simpll	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land \neg C (j) (Z) < S) \to (φ \land j \in ℕ)$
552		icogelb	$⊢ (C (j) (Z) \in ℝ^{} \land D (j) (Z) \in ℝ^{} \land S \in [C (j) (Z), D (j) (Z))) \to C (j) (Z) \leq S$
553	531 533 488 552	syl3anc	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to C (j) (Z) \leq S$
554	553	adantr	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land \neg C (j) (Z) < S) \to C (j) (Z) \leq S$
555		simpr	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land \neg C (j) (Z) < S) \to \neg C (j) (Z) < S$
556	554 555	jca	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land \neg C (j) (Z) < S) \to (C (j) (Z) \leq S \land \neg C (j) (Z) < S)$
557	551 126	syl	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land \neg C (j) (Z) < S) \to C (j) (Z) \in ℝ$
558	551 355	syl	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land \neg C (j) (Z) < S) \to S \in ℝ$
559	557 558	eqleltd	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land \neg C (j) (Z) < S) \to (C (j) (Z) = S \leftrightarrow (C (j) (Z) \leq S \land \neg C (j) (Z) < S))$
560	556 559	mpbird	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land \neg C (j) (Z) < S) \to C (j) (Z) = S$
561		id	$⊢ C (j) (Z) = S \to C (j) (Z) = S$
562	561	eqcomd	$⊢ C (j) (Z) = S \to S = C (j) (Z)$
563	562	oveq1d	$⊢ C (j) (Z) = S \to S - C (j) (Z) = C (j) (Z) - C (j) (Z)$
564	563	adantl	$⊢ ((φ \land j \in ℕ) \land C (j) (Z) = S) \to S - C (j) (Z) = C (j) (Z) - C (j) (Z)$
565	385 126	sselid	$⊢ (φ \land j \in ℕ) \to C (j) (Z) \in ℂ$
566	565	subidd	$⊢ (φ \land j \in ℕ) \to C (j) (Z) - C (j) (Z) = 0$
567	566	adantr	$⊢ ((φ \land j \in ℕ) \land C (j) (Z) = S) \to C (j) (Z) - C (j) (Z) = 0$
568	564 567	eqtr2d	$⊢ ((φ \land j \in ℕ) \land C (j) (Z) = S) \to 0 = S - C (j) (Z)$
569	551 560 568	syl2anc	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land \neg C (j) (Z) < S) \to 0 = S - C (j) (Z)$
570	550 569	eqtrd	$⊢ (((φ \land j \in ℕ) \land P (j) \neq 0) \land \neg C (j) (Z) < S) \to if (C (j) (Z) < S, S - C (j) (Z), 0) = S - C (j) (Z)$
571	548 570	pm2.61dan	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to if (C (j) (Z) < S, S - C (j) (Z), 0) = S - C (j) (Z)$
572	543 546 571	3eqtrd	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to vol ([C (j) (Z), H (S) (D (j)) (Z))) = S - C (j) (Z)$
573	523 572	oveq12d	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to \prod_{k \in Y} vol ([C (j) (k), H (S) (D (j)) (k))) vol ([C (j) (Z), H (S) (D (j)) (Z))) = P (j) (S - C (j) (Z))$
574	386 274	sselid	$⊢ (φ \land j \in ℕ) \to P (j) \in ℂ$
575	355 126	resubcld	$⊢ (φ \land j \in ℕ) \to S - C (j) (Z) \in ℝ$
576	575	recnd	$⊢ (φ \land j \in ℕ) \to S - C (j) (Z) \in ℂ$
577	574 576	mulcomd	$⊢ (φ \land j \in ℕ) \to P (j) (S - C (j) (Z)) = (S - C (j) (Z)) P (j)$
578	577	adantr	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to P (j) (S - C (j) (Z)) = (S - C (j) (Z)) P (j)$
579	450 573 578	3eqtrd	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to C (j) L (W) H (S) (D (j)) = (S - C (j) (Z)) P (j)$
580	579	oveq1d	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to (C (j) L (W) H (S) (D (j))) + (Q - S) P (j) = (S - C (j) (Z)) P (j) + (Q - S) P (j)$
581	183	adantr	$⊢ (φ \land j \in ℕ) \to Q - S \in ℂ$
582	576 581 574	adddird	$⊢ (φ \land j \in ℕ) \to ((S - C (j) (Z)) + Q - S) P (j) = (S - C (j) (Z)) P (j) + (Q - S) P (j)$
583	582	eqcomd	$⊢ (φ \land j \in ℕ) \to (S - C (j) (Z)) P (j) + (Q - S) P (j) = ((S - C (j) (Z)) + Q - S) P (j)$
584	583	adantr	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to (S - C (j) (Z)) P (j) + (Q - S) P (j) = ((S - C (j) (Z)) + Q - S) P (j)$
585	576 581	addcomd	$⊢ (φ \land j \in ℕ) \to (S - C (j) (Z)) + Q - S = (Q - S) + S - C (j) (Z)$
586	166	adantr	$⊢ (φ \land j \in ℕ) \to Q \in ℂ$
587	167	adantr	$⊢ (φ \land j \in ℕ) \to S \in ℂ$
588	586 587 565	npncand	$⊢ (φ \land j \in ℕ) \to (Q - S) + S - C (j) (Z) = Q - C (j) (Z)$
589	585 588	eqtrd	$⊢ (φ \land j \in ℕ) \to (S - C (j) (Z)) + Q - S = Q - C (j) (Z)$
590	589	oveq1d	$⊢ (φ \land j \in ℕ) \to ((S - C (j) (Z)) + Q - S) P (j) = (Q - C (j) (Z)) P (j)$
591	590	adantr	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to ((S - C (j) (Z)) + Q - S) P (j) = (Q - C (j) (Z)) P (j)$
592	580 584 591	3eqtrd	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to (C (j) L (W) H (S) (D (j))) + (Q - S) P (j) = (Q - C (j) (Z)) P (j)$
593	443 444 445 592	syl21anc	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to (C (j) L (W) H (S) (D (j))) + (Q - S) P (j) = (Q - C (j) (Z)) P (j)$
594		eqid	$⊢ \prod_{k \in Y} vol ([C (j) (k), H (Q) (D (j)) (k))) = \prod_{k \in Y} vol ([C (j) (k), H (Q) (D (j)) (k)))$
595	1 223 50 447 5 125 410 594	hoiprodp1	$⊢ (φ \land j \in ℕ) \to C (j) L (W) H (Q) (D (j)) = \prod_{k \in Y} vol ([C (j) (k), H (Q) (D (j)) (k))) vol ([C (j) (Z), H (Q) (D (j)) (Z)))$
596	215 217 595	syl2anc	$⊢ (φ \land j \in (1 \dots M)) \to C (j) L (W) H (Q) (D (j)) = \prod_{k \in Y} vol ([C (j) (k), H (Q) (D (j)) (k))) vol ([C (j) (Z), H (Q) (D (j)) (Z)))$
597	596	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to C (j) L (W) H (Q) (D (j)) = \prod_{k \in Y} vol ([C (j) (k), H (Q) (D (j)) (k))) vol ([C (j) (Z), H (Q) (D (j)) (Z)))$
598	507	eqcomd	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to \prod_{k \in Y} vol ([C (j) (k), D (j) (k))) = J (j) L (Y) K (j)$
599	409	adantr	$⊢ ((φ \land j \in ℕ) \land k \in Y) \to Q \in ℝ$
600	354 599 509 510 513	hsphoival	$⊢ ((φ \land j \in ℕ) \land k \in Y) \to H (Q) (D (j)) (k) = if (k \in Y, D (j) (k), if (D (j) (k) \leq Q, D (j) (k), Q))$
601		iftrue	$⊢ k \in Y \to if (k \in Y, D (j) (k), if (D (j) (k) \leq Q, D (j) (k), Q)) = D (j) (k)$
602	601	adantl	$⊢ ((φ \land j \in ℕ) \land k \in Y) \to if (k \in Y, D (j) (k), if (D (j) (k) \leq Q, D (j) (k), Q)) = D (j) (k)$
603	600 602	eqtrd	$⊢ ((φ \land j \in ℕ) \land k \in Y) \to H (Q) (D (j)) (k) = D (j) (k)$
604	603	oveq2d	$⊢ ((φ \land j \in ℕ) \land k \in Y) \to [C (j) (k), H (Q) (D (j)) (k)) = [C (j) (k), D (j) (k))$
605	604	fveq2d	$⊢ ((φ \land j \in ℕ) \land k \in Y) \to vol ([C (j) (k), H (Q) (D (j)) (k))) = vol ([C (j) (k), D (j) (k)))$
606	605	prodeq2dv	$⊢ (φ \land j \in ℕ) \to \prod_{k \in Y} vol ([C (j) (k), H (Q) (D (j)) (k))) = \prod_{k \in Y} vol ([C (j) (k), D (j) (k)))$
607	606	adantr	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to \prod_{k \in Y} vol ([C (j) (k), H (Q) (D (j)) (k))) = \prod_{k \in Y} vol ([C (j) (k), D (j) (k)))$
608	598 607 451	3eqtr4d	$⊢ ((φ \land j \in ℕ) \land P (j) \neq 0) \to \prod_{k \in Y} vol ([C (j) (k), H (Q) (D (j)) (k))) = P (j)$
609	443 444 445 608	syl21anc	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to \prod_{k \in Y} vol ([C (j) (k), H (Q) (D (j)) (k))) = P (j)$
610	354 409 345 49 50	hsphoival	$⊢ (φ \land j \in ℕ) \to H (Q) (D (j)) (Z) = if (Z \in Y, D (j) (Z), if (D (j) (Z) \leq Q, D (j) (Z), Q))$
611	217 610	syldan	$⊢ (φ \land j \in (1 \dots M)) \to H (Q) (D (j)) (Z) = if (Z \in Y, D (j) (Z), if (D (j) (Z) \leq Q, D (j) (Z), Q))$
612	611	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to H (Q) (D (j)) (Z) = if (Z \in Y, D (j) (Z), if (D (j) (Z) \leq Q, D (j) (Z), Q))$
613	209	iffalsed	$⊢ φ \to if (Z \in Y, D (j) (Z), if (D (j) (Z) \leq Q, D (j) (Z), Q)) = if (D (j) (Z) \leq Q, D (j) (Z), Q)$
614	613	ad2antrr	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to if (Z \in Y, D (j) (Z), if (D (j) (Z) \leq Q, D (j) (Z), Q)) = if (D (j) (Z) \leq Q, D (j) (Z), Q)$
615	217 51	syldan	$⊢ (φ \land j \in (1 \dots M)) \to D (j) (Z) \in ℝ$
616	615	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land D (j) (Z) = Q) \to D (j) (Z) \in ℝ$
617		simpr	$⊢ ((φ \land j \in (1 \dots M)) \land D (j) (Z) = Q) \to D (j) (Z) = Q$
618	616 617	eqled	$⊢ ((φ \land j \in (1 \dots M)) \land D (j) (Z) = Q) \to D (j) (Z) \leq Q$
619	618	iftrued	$⊢ ((φ \land j \in (1 \dots M)) \land D (j) (Z) = Q) \to if (D (j) (Z) \leq Q, D (j) (Z), Q) = D (j) (Z)$
620	619 617	eqtrd	$⊢ ((φ \land j \in (1 \dots M)) \land D (j) (Z) = Q) \to if (D (j) (Z) \leq Q, D (j) (Z), Q) = Q$
621	620	adantlr	$⊢ (((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \land D (j) (Z) = Q) \to if (D (j) (Z) \leq Q, D (j) (Z), Q) = Q$
622	84	adantr	$⊢ (φ \land j \in (1 \dots M)) \to Q \in ℝ$
623	622	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land \neg D (j) (Z) = Q) \to Q \in ℝ$
624	623	adantlr	$⊢ (((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \land \neg D (j) (Z) = Q) \to Q \in ℝ$
625	615	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land \neg D (j) (Z) = Q) \to D (j) (Z) \in ℝ$
626	625	adantlr	$⊢ (((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \land \neg D (j) (Z) = Q) \to D (j) (Z) \in ℝ$
627	25	a1i	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to Q = inf (V ℝ <)$
628	443 57	syl	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to V \subseteq ℝ$
629	161	ad2antrr	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to \exists x \in V \forall y \in V x \leq y$
630		simplr	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to j \in (1 \dots M)$
631	216 488	sylanl2	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to S \in [C (j) (Z), D (j) (Z))$
632	630 631	jca	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to (j \in (1 \dots M) \land S \in [C (j) (Z), D (j) (Z)))$
633		rabid	$⊢ j \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} \leftrightarrow (j \in (1 \dots M) \land S \in [C (j) (Z), D (j) (Z)))$
634	632 633	sylibr	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to j \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\}$
635		eqidd	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to D (j) (Z) = D (j) (Z)$
636		fveq2	$⊢ i = j \to D (i) = D (j)$
637	636	fveq1d	$⊢ i = j \to D (i) (Z) = D (j) (Z)$
638	637	eqeq2d	$⊢ i = j \to (D (j) (Z) = D (i) (Z) \leftrightarrow D (j) (Z) = D (j) (Z))$
639	638	rspcev	$⊢ (j \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} \land D (j) (Z) = D (j) (Z)) \to \exists i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} D (j) (Z) = D (i) (Z)$
640	634 635 639	syl2anc	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to \exists i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} D (j) (Z) = D (i) (Z)$
641		fvexd	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to D (j) (Z) \in V$
642	35 640 641	elrnmptd	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to D (j) (Z) \in ran (i \in \{j \in (1 \dots M) \| S \in [C (j) (Z), D (j) (Z))\} ⟼ D (i) (Z))$
643	642 23	eleqtrrdi	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to D (j) (Z) \in O$
644		elun2	$⊢ D (j) (Z) \in O \to D (j) (Z) \in (\{B (Z)\} \cup O)$
645	643 644	syl	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to D (j) (Z) \in (\{B (Z)\} \cup O)$
646	76	a1i	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to \{B (Z)\} \cup O = V$
647	645 646	eleqtrd	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to D (j) (Z) \in V$
648		lbinfle	$⊢ (V \subseteq ℝ \land \exists x \in V \forall y \in V x \leq y \land D (j) (Z) \in V) \to inf (V ℝ <) \leq D (j) (Z)$
649	628 629 647 648	syl3anc	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to inf (V ℝ <) \leq D (j) (Z)$
650	627 649	eqbrtrd	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to Q \leq D (j) (Z)$
651	650	adantr	$⊢ (((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \land \neg D (j) (Z) = Q) \to Q \leq D (j) (Z)$
652		neqne	$⊢ \neg D (j) (Z) = Q \to D (j) (Z) \neq Q$
653	652	adantl	$⊢ (((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \land \neg D (j) (Z) = Q) \to D (j) (Z) \neq Q$
654	624 626 651 653	leneltd	$⊢ (((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \land \neg D (j) (Z) = Q) \to Q < D (j) (Z)$
655	624 626	ltnled	$⊢ (((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \land \neg D (j) (Z) = Q) \to (Q < D (j) (Z) \leftrightarrow \neg D (j) (Z) \leq Q)$
656	654 655	mpbid	$⊢ (((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \land \neg D (j) (Z) = Q) \to \neg D (j) (Z) \leq Q$
657	656	iffalsed	$⊢ (((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \land \neg D (j) (Z) = Q) \to if (D (j) (Z) \leq Q, D (j) (Z), Q) = Q$
658	621 657	pm2.61dan	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to if (D (j) (Z) \leq Q, D (j) (Z), Q) = Q$
659	612 614 658	3eqtrd	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to H (Q) (D (j)) (Z) = Q$
660	659	oveq2d	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to [C (j) (Z), H (Q) (D (j)) (Z)) = [C (j) (Z), Q)$
661	660	fveq2d	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to vol ([C (j) (Z), H (Q) (D (j)) (Z))) = vol ([C (j) (Z), Q))$
662	215 217 126	syl2anc	$⊢ (φ \land j \in (1 \dots M)) \to C (j) (Z) \in ℝ$
663	662	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to C (j) (Z) \in ℝ$
664	443 84	syl	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to Q \in ℝ$
665		volico	$⊢ (C (j) (Z) \in ℝ \land Q \in ℝ) \to vol ([C (j) (Z), Q)) = if (C (j) (Z) < Q, Q - C (j) (Z), 0)$
666	663 664 665	syl2anc	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to vol ([C (j) (Z), Q)) = if (C (j) (Z) < Q, Q - C (j) (Z), 0)$
667	443 90	syl	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to S \in ℝ$
668	443 444 445 553	syl21anc	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to C (j) (Z) \leq S$
669	443 157	syl	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to S < Q$
670	663 667 664 668 669	lelttrd	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to C (j) (Z) < Q$
671	670	iftrued	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to if (C (j) (Z) < Q, Q - C (j) (Z), 0) = Q - C (j) (Z)$
672	661 666 671	3eqtrd	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to vol ([C (j) (Z), H (Q) (D (j)) (Z))) = Q - C (j) (Z)$
673	609 672	oveq12d	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to \prod_{k \in Y} vol ([C (j) (k), H (Q) (D (j)) (k))) vol ([C (j) (Z), H (Q) (D (j)) (Z))) = P (j) (Q - C (j) (Z))$
674	215 166	syl	$⊢ (φ \land j \in (1 \dots M)) \to Q \in ℂ$
675	385 662	sselid	$⊢ (φ \land j \in (1 \dots M)) \to C (j) (Z) \in ℂ$
676	674 675	subcld	$⊢ (φ \land j \in (1 \dots M)) \to Q - C (j) (Z) \in ℂ$
677	306 676	mulcomd	$⊢ (φ \land j \in (1 \dots M)) \to P (j) (Q - C (j) (Z)) = (Q - C (j) (Z)) P (j)$
678	677	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to P (j) (Q - C (j) (Z)) = (Q - C (j) (Z)) P (j)$
679	597 673 678	3eqtrd	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to C (j) L (W) H (Q) (D (j)) = (Q - C (j) (Z)) P (j)$
680	593 679	eqtr4d	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to (C (j) L (W) H (S) (D (j))) + (Q - S) P (j) = C (j) L (W) H (Q) (D (j))$
681	442 680	eqled	$⊢ ((φ \land j \in (1 \dots M)) \land P (j) \neq 0) \to (C (j) L (W) H (S) (D (j))) + (Q - S) P (j) \leq C (j) L (W) H (Q) (D (j))$
682	439 441 681	syl2anc	$⊢ ((φ \land j \in (1 \dots M)) \land \neg P (j) = 0) \to (C (j) L (W) H (S) (D (j))) + (Q - S) P (j) \leq C (j) L (W) H (Q) (D (j))$
683	438 682	pm2.61dan	$⊢ (φ \land j \in (1 \dots M)) \to (C (j) L (W) H (S) (D (j))) + (Q - S) P (j) \leq C (j) L (W) H (Q) (D (j))$
684	213 402 415 683	fsumle	$⊢ φ \to \sum_{j = 1}^{M} ((C (j) L (W) H (S) (D (j))) + (Q - S) P (j)) \leq \sum_{j = 1}^{M} (C (j) L (W) H (Q) (D (j)))$
685	367 403 413 416 423 684	le2addd	$⊢ φ \to sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + \sum_{j = 1}^{M} ((C (j) L (W) H (S) (D (j))) + (Q - S) P (j)) \leq sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (Q) (D (j)))) + \sum_{j = 1}^{M} (C (j) L (W) H (Q) (D (j)))$
686	321	mpteq1d	$⊢ φ \to (j \in ℕ ⟼ C (j) L (W) H (Q) (D (j))) = (j \in (ℤ_{\geq (M + 1)} \cup (1 \dots M)) ⟼ C (j) L (W) H (Q) (D (j)))$
687	686	fveq2d	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) H (Q) (D (j)))) = sum^((j \in (ℤ_{\geq (M + 1)} \cup (1 \dots M)) ⟼ C (j) L (W) H (Q) (D (j))))$
688	217 412	syldan	$⊢ (φ \land j \in (1 \dots M)) \to C (j) L (W) H (Q) (D (j)) \in [0, +∞]$
689	324 325 326 330 417 688	sge0splitmpt	$⊢ φ \to sum^((j \in (ℤ_{\geq (M + 1)} \cup (1 \dots M)) ⟼ C (j) L (W) H (Q) (D (j)))) = sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (Q) (D (j)))) +_{𝑒} sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (Q) (D (j))))$
690	687 689	eqtrd	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) H (Q) (D (j)))) = sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (Q) (D (j)))) +_{𝑒} sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (Q) (D (j))))$
691	215 217 411	syl2anc	$⊢ (φ \land j \in (1 \dots M)) \to C (j) L (W) H (Q) (D (j)) \in [0, +∞)$
692	213 691	sge0fsummpt	$⊢ φ \to sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (Q) (D (j)))) = \sum_{j = 1}^{M} (C (j) L (W) H (Q) (D (j)))$
693	692 416	eqeltrd	$⊢ φ \to sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (Q) (D (j)))) \in ℝ$
694		rexadd	$⊢ (sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (Q) (D (j)))) \in ℝ \land sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (Q) (D (j)))) \in ℝ) \to sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (Q) (D (j)))) +_{𝑒} sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (Q) (D (j)))) = sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (Q) (D (j)))) + sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (Q) (D (j))))$
695	413 693 694	syl2anc	$⊢ φ \to sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (Q) (D (j)))) +_{𝑒} sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (Q) (D (j)))) = sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (Q) (D (j)))) + sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (Q) (D (j))))$
696	692	oveq2d	$⊢ φ \to sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (Q) (D (j)))) + sum^((j \in (1 \dots M) ⟼ C (j) L (W) H (Q) (D (j)))) = sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (Q) (D (j)))) + \sum_{j = 1}^{M} (C (j) L (W) H (Q) (D (j)))$
697	690 695 696	3eqtrrd	$⊢ φ \to sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (Q) (D (j)))) + \sum_{j = 1}^{M} (C (j) L (W) H (Q) (D (j))) = sum^((j \in ℕ ⟼ C (j) L (W) H (Q) (D (j))))$
698	685 697	breqtrd	$⊢ φ \to sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + \sum_{j = 1}^{M} ((C (j) L (W) H (S) (D (j))) + (Q - S) P (j)) \leq sum^((j \in ℕ ⟼ C (j) L (W) H (Q) (D (j))))$
699	404 281 208 408 698	lemul2ad	$⊢ φ \to (1 + E) (sum^((j \in ℤ_{\geq (M + 1)} ⟼ C (j) L (W) H (S) (D (j)))) + \sum_{j = 1}^{M} ((C (j) L (W) H (S) (D (j))) + (Q - S) P (j))) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (Q) (D (j))))$
700	399 699	eqbrtrd	$⊢ φ \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (S) (D (j)))) + (1 + E) \sum_{j = 1}^{M} (Q - S) P (j) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (Q) (D (j))))$
701	205 280 282 315 700	letrd	$⊢ φ \to G (S - A (Z)) + G (Q - S) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (Q) (D (j))))$
702	189 701	eqbrtrd	$⊢ φ \to G (Q - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (Q) (D (j))))$
703	165 702	jca	$⊢ φ \to (Q \in [A (Z), B (Z)] \land G (Q - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (Q) (D (j)))))$
704		oveq1	$⊢ z = Q \to z - A (Z) = Q - A (Z)$
705	704	oveq2d	$⊢ z = Q \to G (z - A (Z)) = G (Q - A (Z))$
706		fveq2	$⊢ z = Q \to H (z) = H (Q)$
707	706	fveq1d	$⊢ z = Q \to H (z) (D (j)) = H (Q) (D (j))$
708	707	oveq2d	$⊢ z = Q \to C (j) L (W) H (z) (D (j)) = C (j) L (W) H (Q) (D (j))$
709	708	mpteq2dv	$⊢ z = Q \to (j \in ℕ ⟼ C (j) L (W) H (z) (D (j))) = (j \in ℕ ⟼ C (j) L (W) H (Q) (D (j)))$
710	709	fveq2d	$⊢ z = Q \to sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j)))) = sum^((j \in ℕ ⟼ C (j) L (W) H (Q) (D (j))))$
711	710	oveq2d	$⊢ z = Q \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j)))) = (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (Q) (D (j))))$
712	705 711	breq12d	$⊢ z = Q \to (G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j)))) \leftrightarrow G (Q - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (Q) (D (j)))))$
713	712	elrab	$⊢ Q \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 (Q \in [A (Z), B (Z)] \land G (Q - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (Q) (D (j)))))$
714	703 713	sylibr	$⊢ φ \to Q \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))))\}$
715	714 17	eleqtrrdi	$⊢ φ \to Q \in U$
716		breq2	$⊢ u = Q \to (S < u \leftrightarrow S < Q)$
717	716	rspcev	$⊢ (Q \in U \land S < Q) \to \exists u \in U S < u$
718	715 157 717	syl2anc	$⊢ φ \to \exists u \in U S < u$

Metamath Proof Explorer

Theorem hoidmvlelem2

Proof