hoiqssbllem2

Description: The center of the n-dimensional ball belongs to the half-open interval. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	hoiqssbllem2.i	$⊢ Ⅎ i φ$
	hoiqssbllem2.x	$⊢ φ \to X \in Fin$
	hoiqssbllem2.n	$⊢ φ \to X \neq \emptyset$
	hoiqssbllem2.y	$⊢ φ \to Y \in (ℝ^{X})$
	hoiqssbllem2.c	$⊢ φ \to C : X ⟶ ℝ$
	hoiqssbllem2.d	$⊢ φ \to D : X ⟶ ℝ$
	hoiqssbllem2.e	$⊢ φ \to E \in ℝ^{+}$
	hoiqssbllem2.l	$⊢ (φ \land i \in X) \to C (i) \in (Y (i) - (\frac{E}{2 \sqrt{\|X\|}}), Y (i))$
	hoiqssbllem2.r	$⊢ (φ \land i \in X) \to D (i) \in (Y (i), Y (i) + (\frac{E}{2 \sqrt{\|X\|}}))$
Assertion	hoiqssbllem2	$⊢ φ \to \underset{i \in X}{⨉} [C (i), D (i)) \subseteq Y ball (dist (X)) E$

Proof

Step	Hyp	Ref	Expression
1		hoiqssbllem2.i	$⊢ Ⅎ i φ$
2		hoiqssbllem2.x	$⊢ φ \to X \in Fin$
3		hoiqssbllem2.n	$⊢ φ \to X \neq \emptyset$
4		hoiqssbllem2.y	$⊢ φ \to Y \in (ℝ^{X})$
5		hoiqssbllem2.c	$⊢ φ \to C : X ⟶ ℝ$
6		hoiqssbllem2.d	$⊢ φ \to D : X ⟶ ℝ$
7		hoiqssbllem2.e	$⊢ φ \to E \in ℝ^{+}$
8		hoiqssbllem2.l	$⊢ (φ \land i \in X) \to C (i) \in (Y (i) - (\frac{E}{2 \sqrt{\|X\|}}), Y (i))$
9		hoiqssbllem2.r	$⊢ (φ \land i \in X) \to D (i) \in (Y (i), Y (i) + (\frac{E}{2 \sqrt{\|X\|}}))$
10		eqid	$⊢ X = X$
11		eqid	$⊢ ℝ^{X} = ℝ^{X}$
12	10 11	rrxdsfi	$⊢ X \in Fin \to dist (X) = (g \in (ℝ^{X}), h \in (ℝ^{X}) ⟼ \sqrt{\sum_{i \in X} {(g (i) - h (i))}^{2}})$
13	2 12	syl	$⊢ φ \to dist (X) = (g \in (ℝ^{X}), h \in (ℝ^{X}) ⟼ \sqrt{\sum_{i \in X} {(g (i) - h (i))}^{2}})$
14	13	adantr	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to dist (X) = (g \in (ℝ^{X}), h \in (ℝ^{X}) ⟼ \sqrt{\sum_{i \in X} {(g (i) - h (i))}^{2}})$
15		fveq1	$⊢ g = Y \to g (i) = Y (i)$
16	15	adantr	$⊢ (g = Y \land h = f) \to g (i) = Y (i)$
17		fveq1	$⊢ h = f \to h (i) = f (i)$
18	17	adantl	$⊢ (g = Y \land h = f) \to h (i) = f (i)$
19	16 18	oveq12d	$⊢ (g = Y \land h = f) \to g (i) - h (i) = Y (i) - f (i)$
20	19	oveq1d	$⊢ (g = Y \land h = f) \to {(g (i) - h (i))}^{2} = {(Y (i) - f (i))}^{2}$
21	20	sumeq2sdv	$⊢ (g = Y \land h = f) \to \sum_{i \in X} {(g (i) - h (i))}^{2} = \sum_{i \in X} {(Y (i) - f (i))}^{2}$
22	21	fveq2d	$⊢ (g = Y \land h = f) \to \sqrt{\sum_{i \in X} {(g (i) - h (i))}^{2}} = \sqrt{\sum_{i \in X} {(Y (i) - f (i))}^{2}}$
23	22	adantl	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land (g = Y \land h = f)) \to \sqrt{\sum_{i \in X} {(g (i) - h (i))}^{2}} = \sqrt{\sum_{i \in X} {(Y (i) - f (i))}^{2}}$
24	4	adantr	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to Y \in (ℝ^{X})$
25	5	ffvelrnda	$⊢ (φ \land i \in X) \to C (i) \in ℝ$
26	6	ffvelrnda	$⊢ (φ \land i \in X) \to D (i) \in ℝ$
27	26	rexrd	$⊢ (φ \land i \in X) \to D (i) \in ℝ^{*}$
28	1 25 27	hoissrrn2	$⊢ φ \to \underset{i \in X}{⨉} [C (i), D (i)) \subseteq ℝ^{X}$
29	28	adantr	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to \underset{i \in X}{⨉} [C (i), D (i)) \subseteq ℝ^{X}$
30		simpr	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to f \in \underset{i \in X}{⨉} [C (i), D (i))$
31	29 30	sseldd	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to f \in (ℝ^{X})$
32		fvexd	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to \sqrt{\sum_{i \in X} {(Y (i) - f (i))}^{2}} \in V$
33	14 23 24 31 32	ovmpod	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to Y dist (X) f = \sqrt{\sum_{i \in X} {(Y (i) - f (i))}^{2}}$
34		nfcv	$⊢ \underline{Ⅎ} i f$
35		nfixp1	$⊢ \underline{Ⅎ} i \underset{i \in X}{⨉} [C (i), D (i))$
36	34 35	nfel	$⊢ Ⅎ i f \in \underset{i \in X}{⨉} [C (i), D (i))$
37	1 36	nfan	$⊢ Ⅎ i (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i)))$
38		simpl	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to φ$
39	38 2	syl	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to X \in Fin$
40		elmapi	$⊢ Y \in (ℝ^{X}) \to Y : X ⟶ ℝ$
41	4 40	syl	$⊢ φ \to Y : X ⟶ ℝ$
42	41	ffvelrnda	$⊢ (φ \land i \in X) \to Y (i) \in ℝ$
43	38 42	sylan	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land i \in X) \to Y (i) \in ℝ$
44		icossre	$⊢ (C (i) \in ℝ \land D (i) \in ℝ^{*}) \to [C (i), D (i)) \subseteq ℝ$
45	25 27 44	syl2anc	$⊢ (φ \land i \in X) \to [C (i), D (i)) \subseteq ℝ$
46	45	adantlr	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land i \in X) \to [C (i), D (i)) \subseteq ℝ$
47		fvixp2	$⊢ (f \in \underset{i \in X}{⨉} [C (i), D (i)) \land i \in X) \to f (i) \in [C (i), D (i))$
48	47	adantll	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land i \in X) \to f (i) \in [C (i), D (i))$
49	46 48	sseldd	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land i \in X) \to f (i) \in ℝ$
50	43 49	resubcld	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land i \in X) \to Y (i) - f (i) \in ℝ$
51		2nn0	$⊢ 2 \in ℕ_{0}$
52	51	a1i	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land i \in X) \to 2 \in ℕ_{0}$
53	50 52	reexpcld	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land i \in X) \to {(Y (i) - f (i))}^{2} \in ℝ$
54	37 39 53	fsumreclf	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to \sum_{i \in X} {(Y (i) - f (i))}^{2} \in ℝ$
55		fveq2	$⊢ i = j \to C (i) = C (j)$
56		fveq2	$⊢ i = j \to D (i) = D (j)$
57	55 56	oveq12d	$⊢ i = j \to [C (i), D (i)) = [C (j), D (j))$
58	57	cbvixpv	$⊢ \underset{i \in X}{⨉} [C (i), D (i)) = \underset{j \in X}{⨉} [C (j), D (j))$
59	58	eleq2i	$⊢ f \in \underset{i \in X}{⨉} [C (i), D (i)) \leftrightarrow f \in \underset{j \in X}{⨉} [C (j), D (j))$
60	59	biimpi	$⊢ f \in \underset{i \in X}{⨉} [C (i), D (i)) \to f \in \underset{j \in X}{⨉} [C (j), D (j))$
61	60	adantl	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to f \in \underset{j \in X}{⨉} [C (j), D (j))$
62	2	adantr	$⊢ (φ \land f \in \underset{j \in X}{⨉} [C (j), D (j))) \to X \in Fin$
63		simpll	$⊢ ((φ \land f \in \underset{j \in X}{⨉} [C (j), D (j))) \land i \in X) \to φ$
64	59	biimpri	$⊢ f \in \underset{j \in X}{⨉} [C (j), D (j)) \to f \in \underset{i \in X}{⨉} [C (i), D (i))$
65	64	ad2antlr	$⊢ ((φ \land f \in \underset{j \in X}{⨉} [C (j), D (j))) \land i \in X) \to f \in \underset{i \in X}{⨉} [C (i), D (i))$
66		simpr	$⊢ ((φ \land f \in \underset{j \in X}{⨉} [C (j), D (j))) \land i \in X) \to i \in X$
67	63 65 66 53	syl21anc	$⊢ ((φ \land f \in \underset{j \in X}{⨉} [C (j), D (j))) \land i \in X) \to {(Y (i) - f (i))}^{2} \in ℝ$
68	50	sqge0d	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land i \in X) \to 0 \leq {(Y (i) - f (i))}^{2}$
69	63 65 66 68	syl21anc	$⊢ ((φ \land f \in \underset{j \in X}{⨉} [C (j), D (j))) \land i \in X) \to 0 \leq {(Y (i) - f (i))}^{2}$
70	62 67 69	fsumge0	$⊢ (φ \land f \in \underset{j \in X}{⨉} [C (j), D (j))) \to 0 \leq \sum_{i \in X} {(Y (i) - f (i))}^{2}$
71	38 61 70	syl2anc	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to 0 \leq \sum_{i \in X} {(Y (i) - f (i))}^{2}$
72	54 71	resqrtcld	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to \sqrt{\sum_{i \in X} {(Y (i) - f (i))}^{2}} \in ℝ$
73	33 72	eqeltrd	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to Y dist (X) f \in ℝ$
74	26 25	resubcld	$⊢ (φ \land i \in X) \to D (i) - C (i) \in ℝ$
75	74	resqcld	$⊢ (φ \land i \in X) \to {(D (i) - C (i))}^{2} \in ℝ$
76	2 75	fsumrecl	$⊢ φ \to \sum_{i \in X} {(D (i) - C (i))}^{2} \in ℝ$
77	74	sqge0d	$⊢ (φ \land i \in X) \to 0 \leq {(D (i) - C (i))}^{2}$
78	2 75 77	fsumge0	$⊢ φ \to 0 \leq \sum_{i \in X} {(D (i) - C (i))}^{2}$
79	76 78	resqrtcld	$⊢ φ \to \sqrt{\sum_{i \in X} {(D (i) - C (i))}^{2}} \in ℝ$
80	79	adantr	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to \sqrt{\sum_{i \in X} {(D (i) - C (i))}^{2}} \in ℝ$
81	7	rpred	$⊢ φ \to E \in ℝ$
82	81	adantr	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to E \in ℝ$
83	3	adantr	$⊢ (φ \land f \in \underset{j \in X}{⨉} [C (j), D (j))) \to X \neq \emptyset$
84	75	adantlr	$⊢ ((φ \land f \in \underset{j \in X}{⨉} [C (j), D (j))) \land i \in X) \to {(D (i) - C (i))}^{2} \in ℝ$
85	38 26	sylan	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land i \in X) \to D (i) \in ℝ$
86	38 25	sylan	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land i \in X) \to C (i) \in ℝ$
87	85 86	resubcld	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land i \in X) \to D (i) - C (i) \in ℝ$
88	25	rexrd	$⊢ (φ \land i \in X) \to C (i) \in ℝ^{*}$
89	42	rexrd	$⊢ (φ \land i \in X) \to Y (i) \in ℝ^{*}$
90		2rp	$⊢ 2 \in ℝ^{+}$
91	90	a1i	$⊢ φ \to 2 \in ℝ^{+}$
92		hashnncl	$⊢ X \in Fin \to (\|X\| \in ℕ \leftrightarrow X \neq \emptyset)$
93	2 92	syl	$⊢ φ \to (\|X\| \in ℕ \leftrightarrow X \neq \emptyset)$
94	3 93	mpbird	$⊢ φ \to \|X\| \in ℕ$
95	94	nnred	$⊢ φ \to \|X\| \in ℝ$
96	94	nngt0d	$⊢ φ \to 0 < \|X\|$
97	95 96	elrpd	$⊢ φ \to \|X\| \in ℝ^{+}$
98	97	rpsqrtcld	$⊢ φ \to \sqrt{\|X\|} \in ℝ^{+}$
99	91 98	rpmulcld	$⊢ φ \to 2 \sqrt{\|X\|} \in ℝ^{+}$
100	7 99	rpdivcld	$⊢ φ \to \frac{E}{2 \sqrt{\|X\|}} \in ℝ^{+}$
101	100	rpred	$⊢ φ \to \frac{E}{2 \sqrt{\|X\|}} \in ℝ$
102	101	adantr	$⊢ (φ \land i \in X) \to \frac{E}{2 \sqrt{\|X\|}} \in ℝ$
103	42 102	resubcld	$⊢ (φ \land i \in X) \to Y (i) - (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ$
104	103	rexrd	$⊢ (φ \land i \in X) \to Y (i) - (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ^{*}$
105		iooltub	$⊢ (Y (i) - (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ^{} \land Y (i) \in ℝ^{} \land C (i) \in (Y (i) - (\frac{E}{2 \sqrt{\|X\|}}), Y (i))) \to C (i) < Y (i)$
106	104 89 8 105	syl3anc	$⊢ (φ \land i \in X) \to C (i) < Y (i)$
107	25 42 106	ltled	$⊢ (φ \land i \in X) \to C (i) \leq Y (i)$
108	42 102	readdcld	$⊢ (φ \land i \in X) \to Y (i) + (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ$
109	108	rexrd	$⊢ (φ \land i \in X) \to Y (i) + (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ^{*}$
110		ioogtlb	$⊢ (Y (i) \in ℝ^{} \land Y (i) + (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ^{} \land D (i) \in (Y (i), Y (i) + (\frac{E}{2 \sqrt{\|X\|}}))) \to Y (i) < D (i)$
111	89 109 9 110	syl3anc	$⊢ (φ \land i \in X) \to Y (i) < D (i)$
112	88 27 89 107 111	elicod	$⊢ (φ \land i \in X) \to Y (i) \in [C (i), D (i))$
113	38 112	sylan	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land i \in X) \to Y (i) \in [C (i), D (i))$
114		icodiamlt	$⊢ ((C (i) \in ℝ \land D (i) \in ℝ) \land (Y (i) \in [C (i), D (i)) \land f (i) \in [C (i), D (i)))) \to \|Y (i) - f (i)\| < D (i) - C (i)$
115	86 85 113 48 114	syl22anc	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land i \in X) \to \|Y (i) - f (i)\| < D (i) - C (i)$
116		0red	$⊢ (φ \land i \in X) \to 0 \in ℝ$
117	25 42 26 107 111	lelttrd	$⊢ (φ \land i \in X) \to C (i) < D (i)$
118	25 26	posdifd	$⊢ (φ \land i \in X) \to (C (i) < D (i) \leftrightarrow 0 < D (i) - C (i))$
119	117 118	mpbid	$⊢ (φ \land i \in X) \to 0 < D (i) - C (i)$
120	116 74 119	ltled	$⊢ (φ \land i \in X) \to 0 \leq D (i) - C (i)$
121	74 120	absidd	$⊢ (φ \land i \in X) \to \|D (i) - C (i)\| = D (i) - C (i)$
122	121	eqcomd	$⊢ (φ \land i \in X) \to D (i) - C (i) = \|D (i) - C (i)\|$
123	122	adantlr	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land i \in X) \to D (i) - C (i) = \|D (i) - C (i)\|$
124	115 123	breqtrd	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land i \in X) \to \|Y (i) - f (i)\| < \|D (i) - C (i)\|$
125	50 87 124	abslt2sqd	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land i \in X) \to {(Y (i) - f (i))}^{2} < {(D (i) - C (i))}^{2}$
126	63 65 66 125	syl21anc	$⊢ ((φ \land f \in \underset{j \in X}{⨉} [C (j), D (j))) \land i \in X) \to {(Y (i) - f (i))}^{2} < {(D (i) - C (i))}^{2}$
127	62 83 67 84 126	fsumlt	$⊢ (φ \land f \in \underset{j \in X}{⨉} [C (j), D (j))) \to \sum_{i \in X} {(Y (i) - f (i))}^{2} < \sum_{i \in X} {(D (i) - C (i))}^{2}$
128	38 61 127	syl2anc	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to \sum_{i \in X} {(Y (i) - f (i))}^{2} < \sum_{i \in X} {(D (i) - C (i))}^{2}$
129	38 76	syl	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to \sum_{i \in X} {(D (i) - C (i))}^{2} \in ℝ$
130	38 78	syl	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to 0 \leq \sum_{i \in X} {(D (i) - C (i))}^{2}$
131	54 71 129 130	sqrtltd	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to (\sum_{i \in X} {(Y (i) - f (i))}^{2} < \sum_{i \in X} {(D (i) - C (i))}^{2} \leftrightarrow \sqrt{\sum_{i \in X} {(Y (i) - f (i))}^{2}} < \sqrt{\sum_{i \in X} {(D (i) - C (i))}^{2}})$
132	128 131	mpbid	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to \sqrt{\sum_{i \in X} {(Y (i) - f (i))}^{2}} < \sqrt{\sum_{i \in X} {(D (i) - C (i))}^{2}}$
133	33 132	eqbrtrd	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to Y dist (X) f < \sqrt{\sum_{i \in X} {(D (i) - C (i))}^{2}}$
134	81 98	rerpdivcld	$⊢ φ \to \frac{E}{\sqrt{\|X\|}} \in ℝ$
135	134	resqcld	$⊢ φ \to {(\frac{E}{\sqrt{\|X\|}})}^{2} \in ℝ$
136	135	adantr	$⊢ (φ \land i \in X) \to {(\frac{E}{\sqrt{\|X\|}})}^{2} \in ℝ$
137	26 25	jca	$⊢ (φ \land i \in X) \to (D (i) \in ℝ \land C (i) \in ℝ)$
138	108 103	jca	$⊢ (φ \land i \in X) \to (Y (i) + (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ \land Y (i) - (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ)$
139	137 138	jca	$⊢ (φ \land i \in X) \to ((D (i) \in ℝ \land C (i) \in ℝ) \land (Y (i) + (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ \land Y (i) - (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ))$
140		iooltub	$⊢ (Y (i) \in ℝ^{} \land Y (i) + (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ^{} \land D (i) \in (Y (i), Y (i) + (\frac{E}{2 \sqrt{\|X\|}}))) \to D (i) < Y (i) + (\frac{E}{2 \sqrt{\|X\|}})$
141	89 109 9 140	syl3anc	$⊢ (φ \land i \in X) \to D (i) < Y (i) + (\frac{E}{2 \sqrt{\|X\|}})$
142		ioogtlb	$⊢ (Y (i) - (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ^{} \land Y (i) \in ℝ^{} \land C (i) \in (Y (i) - (\frac{E}{2 \sqrt{\|X\|}}), Y (i))) \to Y (i) - (\frac{E}{2 \sqrt{\|X\|}}) < C (i)$
143	104 89 8 142	syl3anc	$⊢ (φ \land i \in X) \to Y (i) - (\frac{E}{2 \sqrt{\|X\|}}) < C (i)$
144	141 143	jca	$⊢ (φ \land i \in X) \to (D (i) < Y (i) + (\frac{E}{2 \sqrt{\|X\|}}) \land Y (i) - (\frac{E}{2 \sqrt{\|X\|}}) < C (i))$
145		lt2sub	$⊢ ((D (i) \in ℝ \land C (i) \in ℝ) \land (Y (i) + (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ \land Y (i) - (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ)) \to ((D (i) < Y (i) + (\frac{E}{2 \sqrt{\|X\|}}) \land Y (i) - (\frac{E}{2 \sqrt{\|X\|}}) < C (i)) \to D (i) - C (i) < Y (i) + (\frac{E}{2 \sqrt{\|X\|}}) - (Y (i) - (\frac{E}{2 \sqrt{\|X\|}})))$
146	139 144 145	sylc	$⊢ (φ \land i \in X) \to D (i) - C (i) < Y (i) + (\frac{E}{2 \sqrt{\|X\|}}) - (Y (i) - (\frac{E}{2 \sqrt{\|X\|}}))$
147	42	recnd	$⊢ (φ \land i \in X) \to Y (i) \in ℂ$
148	102	recnd	$⊢ (φ \land i \in X) \to \frac{E}{2 \sqrt{\|X\|}} \in ℂ$
149	147 148 148	pnncand	$⊢ (φ \land i \in X) \to Y (i) + (\frac{E}{2 \sqrt{\|X\|}}) - (Y (i) - (\frac{E}{2 \sqrt{\|X\|}})) = (\frac{E}{2 \sqrt{\|X\|}}) + (\frac{E}{2 \sqrt{\|X\|}})$
150	81	recnd	$⊢ φ \to E \in ℂ$
151	98	rpcnd	$⊢ φ \to \sqrt{\|X\|} \in ℂ$
152		2cnd	$⊢ φ \to 2 \in ℂ$
153	98	rpne0d	$⊢ φ \to \sqrt{\|X\|} \neq 0$
154	91	rpne0d	$⊢ φ \to 2 \neq 0$
155	150 151 152 153 154	divdiv3d	$⊢ φ \to \frac{\frac{E}{\sqrt{\|X\|}}}{2} = \frac{E}{2 \sqrt{\|X\|}}$
156	155	eqcomd	$⊢ φ \to \frac{E}{2 \sqrt{\|X\|}} = \frac{\frac{E}{\sqrt{\|X\|}}}{2}$
157	156 156	oveq12d	$⊢ φ \to (\frac{E}{2 \sqrt{\|X\|}}) + (\frac{E}{2 \sqrt{\|X\|}}) = (\frac{\frac{E}{\sqrt{\|X\|}}}{2}) + (\frac{\frac{E}{\sqrt{\|X\|}}}{2})$
158	150 151 153	divcld	$⊢ φ \to \frac{E}{\sqrt{\|X\|}} \in ℂ$
159	158	2halvesd	$⊢ φ \to (\frac{\frac{E}{\sqrt{\|X\|}}}{2}) + (\frac{\frac{E}{\sqrt{\|X\|}}}{2}) = \frac{E}{\sqrt{\|X\|}}$
160	157 159	eqtrd	$⊢ φ \to (\frac{E}{2 \sqrt{\|X\|}}) + (\frac{E}{2 \sqrt{\|X\|}}) = \frac{E}{\sqrt{\|X\|}}$
161	160	adantr	$⊢ (φ \land i \in X) \to (\frac{E}{2 \sqrt{\|X\|}}) + (\frac{E}{2 \sqrt{\|X\|}}) = \frac{E}{\sqrt{\|X\|}}$
162	149 161	eqtrd	$⊢ (φ \land i \in X) \to Y (i) + (\frac{E}{2 \sqrt{\|X\|}}) - (Y (i) - (\frac{E}{2 \sqrt{\|X\|}})) = \frac{E}{\sqrt{\|X\|}}$
163	146 162	breqtrd	$⊢ (φ \land i \in X) \to D (i) - C (i) < \frac{E}{\sqrt{\|X\|}}$
164	134	adantr	$⊢ (φ \land i \in X) \to \frac{E}{\sqrt{\|X\|}} \in ℝ$
165		0red	$⊢ φ \to 0 \in ℝ$
166	98	rpred	$⊢ φ \to \sqrt{\|X\|} \in ℝ$
167	7	rpgt0d	$⊢ φ \to 0 < E$
168	98	rpgt0d	$⊢ φ \to 0 < \sqrt{\|X\|}$
169	81 166 167 168	divgt0d	$⊢ φ \to 0 < \frac{E}{\sqrt{\|X\|}}$
170	165 134 169	ltled	$⊢ φ \to 0 \leq \frac{E}{\sqrt{\|X\|}}$
171	170	adantr	$⊢ (φ \land i \in X) \to 0 \leq \frac{E}{\sqrt{\|X\|}}$
172		lt2sq	$⊢ ((D (i) - C (i) \in ℝ \land 0 \leq D (i) - C (i)) \land (\frac{E}{\sqrt{\|X\|}} \in ℝ \land 0 \leq \frac{E}{\sqrt{\|X\|}})) \to (D (i) - C (i) < \frac{E}{\sqrt{\|X\|}} \leftrightarrow {(D (i) - C (i))}^{2} < {(\frac{E}{\sqrt{\|X\|}})}^{2})$
173	74 120 164 171 172	syl22anc	$⊢ (φ \land i \in X) \to (D (i) - C (i) < \frac{E}{\sqrt{\|X\|}} \leftrightarrow {(D (i) - C (i))}^{2} < {(\frac{E}{\sqrt{\|X\|}})}^{2})$
174	163 173	mpbid	$⊢ (φ \land i \in X) \to {(D (i) - C (i))}^{2} < {(\frac{E}{\sqrt{\|X\|}})}^{2}$
175	2 3 75 136 174	fsumlt	$⊢ φ \to \sum_{i \in X} {(D (i) - C (i))}^{2} < \sum_{i \in X} {(\frac{E}{\sqrt{\|X\|}})}^{2}$
176	2 136	fsumrecl	$⊢ φ \to \sum_{i \in X} {(\frac{E}{\sqrt{\|X\|}})}^{2} \in ℝ$
177	164	sqge0d	$⊢ (φ \land i \in X) \to 0 \leq {(\frac{E}{\sqrt{\|X\|}})}^{2}$
178	2 136 177	fsumge0	$⊢ φ \to 0 \leq \sum_{i \in X} {(\frac{E}{\sqrt{\|X\|}})}^{2}$
179	76 78 176 178	sqrtltd	$⊢ φ \to (\sum_{i \in X} {(D (i) - C (i))}^{2} < \sum_{i \in X} {(\frac{E}{\sqrt{\|X\|}})}^{2} \leftrightarrow \sqrt{\sum_{i \in X} {(D (i) - C (i))}^{2}} < \sqrt{\sum_{i \in X} {(\frac{E}{\sqrt{\|X\|}})}^{2}})$
180	175 179	mpbid	$⊢ φ \to \sqrt{\sum_{i \in X} {(D (i) - C (i))}^{2}} < \sqrt{\sum_{i \in X} {(\frac{E}{\sqrt{\|X\|}})}^{2}}$
181	135	recnd	$⊢ φ \to {(\frac{E}{\sqrt{\|X\|}})}^{2} \in ℂ$
182		fsumconst	$⊢ (X \in Fin \land {(\frac{E}{\sqrt{\|X\|}})}^{2} \in ℂ) \to \sum_{i \in X} {(\frac{E}{\sqrt{\|X\|}})}^{2} = \|X\| {(\frac{E}{\sqrt{\|X\|}})}^{2}$
183	2 181 182	syl2anc	$⊢ φ \to \sum_{i \in X} {(\frac{E}{\sqrt{\|X\|}})}^{2} = \|X\| {(\frac{E}{\sqrt{\|X\|}})}^{2}$
184		sqdiv	$⊢ (E \in ℂ \land \sqrt{\|X\|} \in ℂ \land \sqrt{\|X\|} \neq 0) \to {(\frac{E}{\sqrt{\|X\|}})}^{2} = \frac{E^{2}}{{\sqrt{\|X\|}}^{2}}$
185	150 151 153 184	syl3anc	$⊢ φ \to {(\frac{E}{\sqrt{\|X\|}})}^{2} = \frac{E^{2}}{{\sqrt{\|X\|}}^{2}}$
186	95	recnd	$⊢ φ \to \|X\| \in ℂ$
187		sqrtth	$⊢ \|X\| \in ℂ \to {\sqrt{\|X\|}}^{2} = \|X\|$
188	186 187	syl	$⊢ φ \to {\sqrt{\|X\|}}^{2} = \|X\|$
189	188	oveq2d	$⊢ φ \to \frac{E^{2}}{{\sqrt{\|X\|}}^{2}} = \frac{E^{2}}{\|X\|}$
190	185 189	eqtrd	$⊢ φ \to {(\frac{E}{\sqrt{\|X\|}})}^{2} = \frac{E^{2}}{\|X\|}$
191	190	oveq2d	$⊢ φ \to \|X\| {(\frac{E}{\sqrt{\|X\|}})}^{2} = \|X\| (\frac{E^{2}}{\|X\|})$
192	150	sqcld	$⊢ φ \to E^{2} \in ℂ$
193	165 96	gtned	$⊢ φ \to \|X\| \neq 0$
194	192 186 193	divcan2d	$⊢ φ \to \|X\| (\frac{E^{2}}{\|X\|}) = E^{2}$
195	183 191 194	3eqtrd	$⊢ φ \to \sum_{i \in X} {(\frac{E}{\sqrt{\|X\|}})}^{2} = E^{2}$
196	195	fveq2d	$⊢ φ \to \sqrt{\sum_{i \in X} {(\frac{E}{\sqrt{\|X\|}})}^{2}} = \sqrt{E^{2}}$
197	165 81 167	ltled	$⊢ φ \to 0 \leq E$
198		sqrtsq	$⊢ (E \in ℝ \land 0 \leq E) \to \sqrt{E^{2}} = E$
199	81 197 198	syl2anc	$⊢ φ \to \sqrt{E^{2}} = E$
200		eqidd	$⊢ φ \to E = E$
201	196 199 200	3eqtrd	$⊢ φ \to \sqrt{\sum_{i \in X} {(\frac{E}{\sqrt{\|X\|}})}^{2}} = E$
202	180 201	breqtrd	$⊢ φ \to \sqrt{\sum_{i \in X} {(D (i) - C (i))}^{2}} < E$
203	202	adantr	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to \sqrt{\sum_{i \in X} {(D (i) - C (i))}^{2}} < E$
204	73 80 82 133 203	lttrd	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to Y dist (X) f < E$
205		eqid	$⊢ dist (X) = dist (X)$
206	205	rrxmetfi	$⊢ X \in Fin \to dist (X) \in Met (ℝ^{X})$
207		metxmet	$⊢ dist (X) \in Met (ℝ^{X}) \to dist (X) \in ∞Met (ℝ^{X})$
208	2 206 207	3syl	$⊢ φ \to dist (X) \in ∞Met (ℝ^{X})$
209	208	adantr	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to dist (X) \in ∞Met (ℝ^{X})$
210	82	rexrd	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to E \in ℝ^{*}$
211	31 11	eleqtrdi	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to f \in (ℝ^{X})$
212		elbl2	$⊢ ((dist (X) \in ∞Met (ℝ^{X}) \land E \in ℝ^{*}) \land (Y \in (ℝ^{X}) \land f \in (ℝ^{X}))) \to (f \in (Y ball (dist (X)) E) \leftrightarrow Y dist (X) f < E)$
213	209 210 24 211 212	syl22anc	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to (f \in (Y ball (dist (X)) E) \leftrightarrow Y dist (X) f < E)$
214	204 213	mpbird	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to f \in (Y ball (dist (X)) E)$
215	214	ralrimiva	$⊢ φ \to \forall f \in \underset{i \in X}{⨉} [C (i), D (i)) f \in (Y ball (dist (X)) E)$
216		dfss3	$⊢ \underset{i \in X}{⨉} [C (i), D (i)) \subseteq Y ball (dist (X)) E \leftrightarrow \forall f \in \underset{i \in X}{⨉} [C (i), D (i)) f \in (Y ball (dist (X)) E)$
217	215 216	sylibr	$⊢ φ \to \underset{i \in X}{⨉} [C (i), D (i)) \subseteq Y ball (dist (X)) E$

Metamath Proof Explorer

Theorem hoiqssbllem2

Proof