hoidmvlelem5

Description: The dimensional volume of a multidimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Induction step of Lemma 115B of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	hoidmvlelem5.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
	hoidmvlelem5.f	$⊢ φ \to X \in Fin$
	hoidmvlelem5.y	$⊢ φ \to Y \subseteq X$
	hoidmvlelem5.z	$⊢ φ \to Z \in (X ∖ Y)$
	hoidmvlelem5.w	$⊢ W = Y \cup \{Z\}$
	hoidmvlelem5.a	$⊢ φ \to A : W ⟶ ℝ$
	hoidmvlelem5.b	$⊢ φ \to B : W ⟶ ℝ$
	hoidmvlelem5.c	$⊢ φ \to C : ℕ ⟶ ℝ^{W}$
	hoidmvlelem5.d	$⊢ φ \to D : ℕ ⟶ ℝ^{W}$
	hoidmvlelem5.i	$⊢ φ \to \forall e \in (ℝ^{Y}) \forall f \in (ℝ^{Y}) \forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [e (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to e L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j))))$
	hoidmvlelem5.s	$⊢ φ \to \underset{k \in W}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in W}{⨉} [C (j) (k), D (j) (k))$
	hoidmvlelem5.n	$⊢ φ \to Y \neq \emptyset$
Assertion	hoidmvlelem5	$⊢ φ \to A L (W) B \leq sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$

Proof

Step	Hyp	Ref	Expression
1		hoidmvlelem5.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		hoidmvlelem5.f	$⊢ φ \to X \in Fin$
3		hoidmvlelem5.y	$⊢ φ \to Y \subseteq X$
4		hoidmvlelem5.z	$⊢ φ \to Z \in (X ∖ Y)$
5		hoidmvlelem5.w	$⊢ W = Y \cup \{Z\}$
6		hoidmvlelem5.a	$⊢ φ \to A : W ⟶ ℝ$
7		hoidmvlelem5.b	$⊢ φ \to B : W ⟶ ℝ$
8		hoidmvlelem5.c	$⊢ φ \to C : ℕ ⟶ ℝ^{W}$
9		hoidmvlelem5.d	$⊢ φ \to D : ℕ ⟶ ℝ^{W}$
10		hoidmvlelem5.i	$⊢ φ \to \forall e \in (ℝ^{Y}) \forall f \in (ℝ^{Y}) \forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [e (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to e L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j))))$
11		hoidmvlelem5.s	$⊢ φ \to \underset{k \in W}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in W}{⨉} [C (j) (k), D (j) (k))$
12		hoidmvlelem5.n	$⊢ φ \to Y \neq \emptyset$
13		nfv	$⊢ Ⅎ s φ$
14		nfre1	$⊢ Ⅎ s \exists s \in W B (s) \leq A (s)$
15	13 14	nfan	$⊢ Ⅎ s (φ \land \exists s \in W B (s) \leq A (s))$
16		ssfi	$⊢ (X \in Fin \land Y \subseteq X) \to Y \in Fin$
17	2 3 16	syl2anc	$⊢ φ \to Y \in Fin$
18		snfi	$⊢ \{Z\} \in Fin$
19	18	a1i	$⊢ φ \to \{Z\} \in Fin$
20		unfi	$⊢ (Y \in Fin \land \{Z\} \in Fin) \to Y \cup \{Z\} \in Fin$
21	17 19 20	syl2anc	$⊢ φ \to Y \cup \{Z\} \in Fin$
22	5 21	eqeltrid	$⊢ φ \to W \in Fin$
23	22	adantr	$⊢ (φ \land \exists s \in W B (s) \leq A (s)) \to W \in Fin$
24	6	adantr	$⊢ (φ \land \exists s \in W B (s) \leq A (s)) \to A : W ⟶ ℝ$
25	7	adantr	$⊢ (φ \land \exists s \in W B (s) \leq A (s)) \to B : W ⟶ ℝ$
26		simpr	$⊢ (φ \land \exists s \in W B (s) \leq A (s)) \to \exists s \in W B (s) \leq A (s)$
27	15 1 23 24 25 26	hoidmvval0	$⊢ (φ \land \exists s \in W B (s) \leq A (s)) \to A L (W) B = 0$
28		nnex	$⊢ ℕ \in V$
29	28	a1i	$⊢ φ \to ℕ \in V$
30		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
31	22	adantr	$⊢ (φ \land j \in ℕ) \to W \in Fin$
32	8	ffvelcdmda	$⊢ (φ \land j \in ℕ) \to C (j) \in (ℝ^{W})$
33		elmapi	$⊢ C (j) \in (ℝ^{W}) \to C (j) : W ⟶ ℝ$
34	32 33	syl	$⊢ (φ \land j \in ℕ) \to C (j) : W ⟶ ℝ$
35	9	ffvelcdmda	$⊢ (φ \land j \in ℕ) \to D (j) \in (ℝ^{W})$
36		elmapi	$⊢ D (j) \in (ℝ^{W}) \to D (j) : W ⟶ ℝ$
37	35 36	syl	$⊢ (φ \land j \in ℕ) \to D (j) : W ⟶ ℝ$
38	1 31 34 37	hoidmvcl	$⊢ (φ \land j \in ℕ) \to C (j) L (W) D (j) \in [0, +∞)$
39	30 38	sselid	$⊢ (φ \land j \in ℕ) \to C (j) L (W) D (j) \in [0, +∞]$
40	39	fmpttd	$⊢ φ \to (j \in ℕ ⟼ C (j) L (W) D (j)) : ℕ ⟶ [0, +∞]$
41	29 40	sge0ge0	$⊢ φ \to 0 \leq sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
42	41	adantr	$⊢ (φ \land \exists s \in W B (s) \leq A (s)) \to 0 \leq sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
43	27 42	eqbrtrd	$⊢ (φ \land \exists s \in W B (s) \leq A (s)) \to A L (W) B \leq sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
44		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
45	1 22 6 7	hoidmvcl	$⊢ φ \to A L (W) B \in [0, +∞)$
46	44 45	sselid	$⊢ φ \to A L (W) B \in ℝ^{*}$
47	46	adantr	$⊢ (φ \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞) \to A L (W) B \in ℝ^{*}$
48	29 40	sge0xrcl	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ^{*}$
49	48	adantr	$⊢ (φ \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞) \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ^{*}$
50		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
51	50 45	sselid	$⊢ φ \to A L (W) B \in ℝ$
52		ltpnf	$⊢ A L (W) B \in ℝ \to A L (W) B < +∞$
53	51 52	syl	$⊢ φ \to A L (W) B < +∞$
54	53	adantr	$⊢ (φ \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞) \to A L (W) B < +∞$
55		id	$⊢ sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞ \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞$
56	55	eqcomd	$⊢ sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞ \to +∞ = sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
57	56	adantl	$⊢ (φ \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞) \to +∞ = sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
58	54 57	breqtrd	$⊢ (φ \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞) \to A L (W) B < sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
59	47 49 58	xrltled	$⊢ (φ \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞) \to A L (W) B \leq sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
60	59	adantlr	$⊢ ((φ \land \neg \exists s \in W B (s) \leq A (s)) \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞) \to A L (W) B \leq sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
61		simpll	$⊢ ((φ \land \neg \exists s \in W B (s) \leq A (s)) \land \neg sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞) \to φ$
62		simpr	$⊢ (φ \land \neg \exists s \in W B (s) \leq A (s)) \to \neg \exists s \in W B (s) \leq A (s)$
63	6	ffvelcdmda	$⊢ (φ \land s \in W) \to A (s) \in ℝ$
64	7	ffvelcdmda	$⊢ (φ \land s \in W) \to B (s) \in ℝ$
65	63 64	ltnled	$⊢ (φ \land s \in W) \to (A (s) < B (s) \leftrightarrow \neg B (s) \leq A (s))$
66	65	ralbidva	$⊢ φ \to (\forall s \in W A (s) < B (s) \leftrightarrow \forall s \in W \neg B (s) \leq A (s))$
67		ralnex	$⊢ \forall s \in W \neg B (s) \leq A (s) \leftrightarrow \neg \exists s \in W B (s) \leq A (s)$
68	67	a1i	$⊢ φ \to (\forall s \in W \neg B (s) \leq A (s) \leftrightarrow \neg \exists s \in W B (s) \leq A (s))$
69	66 68	bitrd	$⊢ φ \to (\forall s \in W A (s) < B (s) \leftrightarrow \neg \exists s \in W B (s) \leq A (s))$
70	69	adantr	$⊢ (φ \land \neg \exists s \in W B (s) \leq A (s)) \to (\forall s \in W A (s) < B (s) \leftrightarrow \neg \exists s \in W B (s) \leq A (s))$
71	62 70	mpbird	$⊢ (φ \land \neg \exists s \in W B (s) \leq A (s)) \to \forall s \in W A (s) < B (s)$
72	71	adantr	$⊢ ((φ \land \neg \exists s \in W B (s) \leq A (s)) \land \neg sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞) \to \forall s \in W A (s) < B (s)$
73		simpr	$⊢ (φ \land \neg sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞) \to \neg sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞$
74	28	a1i	$⊢ (φ \land \neg sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞) \to ℕ \in V$
75	40	adantr	$⊢ (φ \land \neg sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞) \to (j \in ℕ ⟼ C (j) L (W) D (j)) : ℕ ⟶ [0, +∞]$
76	74 75	sge0repnf	$⊢ (φ \land \neg sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞) \to (sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ \leftrightarrow \neg sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞)$
77	73 76	mpbird	$⊢ (φ \land \neg sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞) \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ$
78	77	adantlr	$⊢ ((φ \land \neg \exists s \in W B (s) \leq A (s)) \land \neg sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞) \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ$
79		simpll	$⊢ (((φ \land \forall s \in W A (s) < B (s)) \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ) \land r \in ℝ^{+}) \to (φ \land \forall s \in W A (s) < B (s))$
80		fveq2	$⊢ j = i \to C (j) = C (i)$
81		fveq2	$⊢ j = i \to D (j) = D (i)$
82	80 81	oveq12d	$⊢ j = i \to C (j) L (W) D (j) = C (i) L (W) D (i)$
83	82	cbvmptv	$⊢ (j \in ℕ ⟼ C (j) L (W) D (j)) = (i \in ℕ ⟼ C (i) L (W) D (i))$
84	83	fveq2i	$⊢ sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = sum^((i \in ℕ ⟼ C (i) L (W) D (i)))$
85	84	eleq1i	$⊢ sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ \leftrightarrow sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ$
86	85	biimpi	$⊢ sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ \to sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ$
87	86	ad2antlr	$⊢ (((φ \land \forall s \in W A (s) < B (s)) \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ) \land r \in ℝ^{+}) \to sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ$
88		simpr	$⊢ (((φ \land \forall s \in W A (s) < B (s)) \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ) \land r \in ℝ^{+}) \to r \in ℝ^{+}$
89	2	ad3antrrr	$⊢ (((φ \land \forall s \in W A (s) < B (s)) \land sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ) \land r \in ℝ^{+}) \to X \in Fin$
90	3	ad3antrrr	$⊢ (((φ \land \forall s \in W A (s) < B (s)) \land sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ) \land r \in ℝ^{+}) \to Y \subseteq X$
91	12	ad3antrrr	$⊢ (((φ \land \forall s \in W A (s) < B (s)) \land sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ) \land r \in ℝ^{+}) \to Y \neq \emptyset$
92	4	ad3antrrr	$⊢ (((φ \land \forall s \in W A (s) < B (s)) \land sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ) \land r \in ℝ^{+}) \to Z \in (X ∖ Y)$
93	6	ad3antrrr	$⊢ (((φ \land \forall s \in W A (s) < B (s)) \land sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ) \land r \in ℝ^{+}) \to A : W ⟶ ℝ$
94	7	ad3antrrr	$⊢ (((φ \land \forall s \in W A (s) < B (s)) \land sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ) \land r \in ℝ^{+}) \to B : W ⟶ ℝ$
95		fveq2	$⊢ s = k \to A (s) = A (k)$
96		fveq2	$⊢ s = k \to B (s) = B (k)$
97	95 96	breq12d	$⊢ s = k \to (A (s) < B (s) \leftrightarrow A (k) < B (k))$
98	97	cbvralvw	$⊢ \forall s \in W A (s) < B (s) \leftrightarrow \forall k \in W A (k) < B (k)$
99	98	biimpi	$⊢ \forall s \in W A (s) < B (s) \to \forall k \in W A (k) < B (k)$
100	99	adantr	$⊢ (\forall s \in W A (s) < B (s) \land k \in W) \to \forall k \in W A (k) < B (k)$
101		simpr	$⊢ (\forall s \in W A (s) < B (s) \land k \in W) \to k \in W$
102		rspa	$⊢ (\forall k \in W A (k) < B (k) \land k \in W) \to A (k) < B (k)$
103	100 101 102	syl2anc	$⊢ (\forall s \in W A (s) < B (s) \land k \in W) \to A (k) < B (k)$
104	103	ad5ant25	$⊢ ((((φ \land \forall s \in W A (s) < B (s)) \land sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ) \land r \in ℝ^{+}) \land k \in W) \to A (k) < B (k)$
105	8	ad3antrrr	$⊢ (((φ \land \forall s \in W A (s) < B (s)) \land sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ) \land r \in ℝ^{+}) \to C : ℕ ⟶ ℝ^{W}$
106	9	ad3antrrr	$⊢ (((φ \land \forall s \in W A (s) < B (s)) \land sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ) \land r \in ℝ^{+}) \to D : ℕ ⟶ ℝ^{W}$
107	85	biimpri	$⊢ sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ$
108	107	ad2antlr	$⊢ (((φ \land \forall s \in W A (s) < B (s)) \land sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ) \land r \in ℝ^{+}) \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ$
109		fveq1	$⊢ d = c \to d (i) = c (i)$
110	109	breq1d	$⊢ d = c \to (d (i) \leq x \leftrightarrow c (i) \leq x)$
111	110 109	ifbieq1d	$⊢ d = c \to if (d (i) \leq x, d (i), x) = if (c (i) \leq x, c (i), x)$
112	109 111	ifeq12d	$⊢ d = c \to if (i \in Y, d (i), if (d (i) \leq x, d (i), x)) = if (i \in Y, c (i), if (c (i) \leq x, c (i), x))$
113	112	mpteq2dv	$⊢ d = c \to (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))) = (i \in W ⟼ if (i \in Y, c (i), if (c (i) \leq x, c (i), x)))$
114		eleq1w	$⊢ i = j \to (i \in Y \leftrightarrow j \in Y)$
115		fveq2	$⊢ i = j \to c (i) = c (j)$
116	115	breq1d	$⊢ i = j \to (c (i) \leq x \leftrightarrow c (j) \leq x)$
117	116 115	ifbieq1d	$⊢ i = j \to if (c (i) \leq x, c (i), x) = if (c (j) \leq x, c (j), x)$
118	114 115 117	ifbieq12d	$⊢ i = j \to if (i \in Y, c (i), if (c (i) \leq x, c (i), x)) = if (j \in Y, c (j), if (c (j) \leq x, c (j), x))$
119	118	cbvmptv	$⊢ (i \in W ⟼ if (i \in Y, c (i), if (c (i) \leq x, c (i), x))) = (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x)))$
120	119	a1i	$⊢ d = c \to (i \in W ⟼ if (i \in Y, c (i), if (c (i) \leq x, c (i), x))) = (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x)))$
121	113 120	eqtrd	$⊢ d = c \to (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))) = (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x)))$
122	121	cbvmptv	$⊢ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x)))) = (c \in (ℝ^{W}) ⟼ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x))))$
123	122	mpteq2i	$⊢ (x \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))))) = (x \in ℝ ⟼ (c \in (ℝ^{W}) ⟼ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x)))))$
124		eqid	$⊢ ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) = ({A ↾}_{Y}) L (Y) ({B ↾}_{Y})$
125		simpr	$⊢ (((φ \land \forall s \in W A (s) < B (s)) \land sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ) \land r \in ℝ^{+}) \to r \in ℝ^{+}$
126		oveq1	$⊢ w = z \to w - A (Z) = z - A (Z)$
127	126	oveq2d	$⊢ w = z \to (({A ↾}_{Y}) L (Y) ({B ↾}_{Y})) (w - A (Z)) = (({A ↾}_{Y}) L (Y) ({B ↾}_{Y})) (z - A (Z))$
128		breq2	$⊢ w = x \to (d (i) \leq w \leftrightarrow d (i) \leq x)$
129		eqidd	$⊢ w = x \to d (i) = d (i)$
130		id	$⊢ w = x \to w = x$
131	128 129 130	ifbieq12d	$⊢ w = x \to if (d (i) \leq w, d (i), w) = if (d (i) \leq x, d (i), x)$
132	131	ifeq2d	$⊢ w = x \to if (i \in Y, d (i), if (d (i) \leq w, d (i), w)) = if (i \in Y, d (i), if (d (i) \leq x, d (i), x))$
133	132	mpteq2dv	$⊢ w = x \to (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq w, d (i), w))) = (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x)))$
134	133	mpteq2dv	$⊢ w = x \to (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq w, d (i), w)))) = (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))))$
135	134	cbvmptv	$⊢ (w \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq w, d (i), w))))) = (x \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x)))))$
136	135	a1i	$⊢ w = z \to (w \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq w, d (i), w))))) = (x \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x)))))$
137		id	$⊢ w = z \to w = z$
138	136 137	fveq12d	$⊢ w = z \to (w \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq w, d (i), w))))) (w) = (x \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))))) (z)$
139	138	fveq1d	$⊢ w = z \to (w \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq w, d (i), w))))) (w) (D (l)) = (x \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))))) (z) (D (l))$
140	139	oveq2d	$⊢ w = z \to C (l) L (W) (w \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq w, d (i), w))))) (w) (D (l)) = C (l) L (W) (x \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))))) (z) (D (l))$
141	140	mpteq2dv	$⊢ w = z \to (l \in ℕ ⟼ C (l) L (W) (w \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq w, d (i), w))))) (w) (D (l))) = (l \in ℕ ⟼ C (l) L (W) (x \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))))) (z) (D (l)))$
142		fveq2	$⊢ l = j \to C (l) = C (j)$
143		2fveq3	$⊢ l = j \to (x \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))))) (z) (D (l)) = (x \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))))) (z) (D (j))$
144	142 143	oveq12d	$⊢ l = j \to C (l) L (W) (x \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))))) (z) (D (l)) = C (j) L (W) (x \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))))) (z) (D (j))$
145	144	cbvmptv	$⊢ (l \in ℕ ⟼ C (l) L (W) (x \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))))) (z) (D (l))) = (j \in ℕ ⟼ C (j) L (W) (x \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))))) (z) (D (j)))$
146	145	a1i	$⊢ w = z \to (l \in ℕ ⟼ C (l) L (W) (x \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))))) (z) (D (l))) = (j \in ℕ ⟼ C (j) L (W) (x \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))))) (z) (D (j)))$
147	141 146	eqtrd	$⊢ w = z \to (l \in ℕ ⟼ C (l) L (W) (w \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq w, d (i), w))))) (w) (D (l))) = (j \in ℕ ⟼ C (j) L (W) (x \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))))) (z) (D (j)))$
148	147	fveq2d	$⊢ w = z \to sum^((l \in ℕ ⟼ C (l) L (W) (w \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq w, d (i), w))))) (w) (D (l)))) = sum^((j \in ℕ ⟼ C (j) L (W) (x \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))))) (z) (D (j))))$
149	148	oveq2d	$⊢ w = z \to (1 + r) sum^((l \in ℕ ⟼ C (l) L (W) (w \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq w, d (i), w))))) (w) (D (l)))) = (1 + r) sum^((j \in ℕ ⟼ C (j) L (W) (x \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))))) (z) (D (j))))$
150	127 149	breq12d	$⊢ w = z \to ((({A ↾}_{Y}) L (Y) ({B ↾}_{Y})) (w - A (Z)) \leq (1 + r) sum^((l \in ℕ ⟼ C (l) L (W) (w \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq w, d (i), w))))) (w) (D (l)))) \leftrightarrow (({A ↾}_{Y}) L (Y) ({B ↾}_{Y})) (z - A (Z)) \leq (1 + r) sum^((j \in ℕ ⟼ C (j) L (W) (x \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))))) (z) (D (j)))))$
151	150	cbvrabv	$⊢ \{w \in [A (Z), B (Z)] \| (({A ↾}_{Y}) L (Y) ({B ↾}_{Y})) (w - A (Z)) \leq (1 + r) sum^((l \in ℕ ⟼ C (l) L (W) (w \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq w, d (i), w))))) (w) (D (l))))\} = \{z \in [A (Z), B (Z)] \| (({A ↾}_{Y}) L (Y) ({B ↾}_{Y})) (z - A (Z)) \leq (1 + r) sum^((j \in ℕ ⟼ C (j) L (W) (x \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq x, d (i), x))))) (z) (D (j))))\}$
152		eqid	$⊢ sup (\{w \in [A (Z), B (Z)] \| (({A ↾}_{Y}) L (Y) ({B ↾}_{Y})) (w - A (Z)) \leq (1 + r) sum^((l \in ℕ ⟼ C (l) L (W) (w \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq w, d (i), w))))) (w) (D (l))))\} ℝ <) = sup (\{w \in [A (Z), B (Z)] \| (({A ↾}_{Y}) L (Y) ({B ↾}_{Y})) (w - A (Z)) \leq (1 + r) sum^((l \in ℕ ⟼ C (l) L (W) (w \in ℝ ⟼ (d \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, d (i), if (d (i) \leq w, d (i), w))))) (w) (D (l))))\} ℝ <)$
153	10	ad3antrrr	$⊢ (((φ \land \forall s \in W A (s) < B (s)) \land sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ) \land r \in ℝ^{+}) \to \forall e \in (ℝ^{Y}) \forall f \in (ℝ^{Y}) \forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [e (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to e L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j))))$
154	11	ad3antrrr	$⊢ (((φ \land \forall s \in W A (s) < B (s)) \land sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ) \land r \in ℝ^{+}) \to \underset{k \in W}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in W}{⨉} [C (j) (k), D (j) (k))$
155	1 89 90 91 92 5 93 94 104 105 106 108 123 124 125 151 152 153 154	hoidmvlelem4	$⊢ (((φ \land \forall s \in W A (s) < B (s)) \land sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ) \land r \in ℝ^{+}) \to A L (W) B \leq (1 + r) sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
156	79 87 88 155	syl21anc	$⊢ (((φ \land \forall s \in W A (s) < B (s)) \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ) \land r \in ℝ^{+}) \to A L (W) B \leq (1 + r) sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
157	156	ralrimiva	$⊢ ((φ \land \forall s \in W A (s) < B (s)) \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ) \to \forall r \in ℝ^{+} A L (W) B \leq (1 + r) sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
158		nfv	$⊢ Ⅎ r ((φ \land \forall s \in W A (s) < B (s)) \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ)$
159	46	ad2antrr	$⊢ ((φ \land \forall s \in W A (s) < B (s)) \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ) \to A L (W) B \in ℝ^{*}$
160		0xr	$⊢ 0 \in ℝ^{*}$
161	160	a1i	$⊢ ((φ \land \forall s \in W A (s) < B (s)) \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ) \to 0 \in ℝ^{*}$
162		pnfxr	$⊢ +∞ \in ℝ^{*}$
163	162	a1i	$⊢ ((φ \land \forall s \in W A (s) < B (s)) \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ) \to +∞ \in ℝ^{*}$
164	48	ad2antrr	$⊢ ((φ \land \forall s \in W A (s) < B (s)) \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ) \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ^{*}$
165	41	ad2antrr	$⊢ ((φ \land \forall s \in W A (s) < B (s)) \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ) \to 0 \leq sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
166		ltpnf	$⊢ sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) < +∞$
167	166	adantl	$⊢ ((φ \land \forall s \in W A (s) < B (s)) \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ) \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) < +∞$
168	161 163 164 165 167	elicod	$⊢ ((φ \land \forall s \in W A (s) < B (s)) \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ) \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in [0, +∞)$
169	158 159 168	xralrple2	$⊢ ((φ \land \forall s \in W A (s) < B (s)) \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ) \to (A L (W) B \leq sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \leftrightarrow \forall r \in ℝ^{+} A L (W) B \leq (1 + r) sum^((j \in ℕ ⟼ C (j) L (W) D (j))))$
170	157 169	mpbird	$⊢ ((φ \land \forall s \in W A (s) < B (s)) \land sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ) \to A L (W) B \leq sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
171	61 72 78 170	syl21anc	$⊢ ((φ \land \neg \exists s \in W B (s) \leq A (s)) \land \neg sum^((j \in ℕ ⟼ C (j) L (W) D (j))) = +∞) \to A L (W) B \leq sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
172	60 171	pm2.61dan	$⊢ (φ \land \neg \exists s \in W B (s) \leq A (s)) \to A L (W) B \leq sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
173	43 172	pm2.61dan	$⊢ φ \to A L (W) B \leq sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$

Metamath Proof Explorer

Theorem hoidmvlelem5

Proof