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	ffvelcdmda	$⊢ (φ \land i \in X) \to C (i) \in ℝ$
26	6	ffvelcdmda	$⊢ (φ \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	ffvelcdmda	$⊢ (φ \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	bilani	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to f \in \underset{j \in X}{⨉} [C (j), D (j))$
61	2	adantr	$⊢ (φ \land f \in \underset{j \in X}{⨉} [C (j), D (j))) \to X \in Fin$
62		simpll	$⊢ ((φ \land f \in \underset{j \in X}{⨉} [C (j), D (j))) \land i \in X) \to φ$
63	59	biimpri	$⊢ f \in \underset{j \in X}{⨉} [C (j), D (j)) \to f \in \underset{i \in X}{⨉} [C (i), D (i))$
64	63	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))$
65		simpr	$⊢ ((φ \land f \in \underset{j \in X}{⨉} [C (j), D (j))) \land i \in X) \to i \in X$
66	62 64 65 53	syl21anc	$⊢ ((φ \land f \in \underset{j \in X}{⨉} [C (j), D (j))) \land i \in X) \to {(Y (i) - f (i))}^{2} \in ℝ$
67	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}$
68	62 64 65 67	syl21anc	$⊢ ((φ \land f \in \underset{j \in X}{⨉} [C (j), D (j))) \land i \in X) \to 0 \leq {(Y (i) - f (i))}^{2}$
69	61 66 68	fsumge0	$⊢ (φ \land f \in \underset{j \in X}{⨉} [C (j), D (j))) \to 0 \leq \sum_{i \in X} {(Y (i) - f (i))}^{2}$
70	38 60 69	syl2anc	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to 0 \leq \sum_{i \in X} {(Y (i) - f (i))}^{2}$
71	54 70	resqrtcld	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to \sqrt{\sum_{i \in X} {(Y (i) - f (i))}^{2}} \in ℝ$
72	33 71	eqeltrd	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to Y dist (X) f \in ℝ$
73	26 25	resubcld	$⊢ (φ \land i \in X) \to D (i) - C (i) \in ℝ$
74	73	resqcld	$⊢ (φ \land i \in X) \to {(D (i) - C (i))}^{2} \in ℝ$
75	2 74	fsumrecl	$⊢ φ \to \sum_{i \in X} {(D (i) - C (i))}^{2} \in ℝ$
76	73	sqge0d	$⊢ (φ \land i \in X) \to 0 \leq {(D (i) - C (i))}^{2}$
77	2 74 76	fsumge0	$⊢ φ \to 0 \leq \sum_{i \in X} {(D (i) - C (i))}^{2}$
78	75 77	resqrtcld	$⊢ φ \to \sqrt{\sum_{i \in X} {(D (i) - C (i))}^{2}} \in ℝ$
79	78	adantr	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to \sqrt{\sum_{i \in X} {(D (i) - C (i))}^{2}} \in ℝ$
80	7	rpred	$⊢ φ \to E \in ℝ$
81	80	adantr	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to E \in ℝ$
82	3	adantr	$⊢ (φ \land f \in \underset{j \in X}{⨉} [C (j), D (j))) \to X \neq \emptyset$
83	74	adantlr	$⊢ ((φ \land f \in \underset{j \in X}{⨉} [C (j), D (j))) \land i \in X) \to {(D (i) - C (i))}^{2} \in ℝ$
84	38 26	sylan	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land i \in X) \to D (i) \in ℝ$
85	38 25	sylan	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land i \in X) \to C (i) \in ℝ$
86	84 85	resubcld	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land i \in X) \to D (i) - C (i) \in ℝ$
87	25	rexrd	$⊢ (φ \land i \in X) \to C (i) \in ℝ^{*}$
88	42	rexrd	$⊢ (φ \land i \in X) \to Y (i) \in ℝ^{*}$
89		2rp	$⊢ 2 \in ℝ^{+}$
90	89	a1i	$⊢ φ \to 2 \in ℝ^{+}$
91		hashnncl	$⊢ X \in Fin \to (\|X\| \in ℕ \leftrightarrow X \neq \emptyset)$
92	2 91	syl	$⊢ φ \to (\|X\| \in ℕ \leftrightarrow X \neq \emptyset)$
93	3 92	mpbird	$⊢ φ \to \|X\| \in ℕ$
94	93	nnred	$⊢ φ \to \|X\| \in ℝ$
95	93	nngt0d	$⊢ φ \to 0 < \|X\|$
96	94 95	elrpd	$⊢ φ \to \|X\| \in ℝ^{+}$
97	96	rpsqrtcld	$⊢ φ \to \sqrt{\|X\|} \in ℝ^{+}$
98	90 97	rpmulcld	$⊢ φ \to 2 \sqrt{\|X\|} \in ℝ^{+}$
99	7 98	rpdivcld	$⊢ φ \to \frac{E}{2 \sqrt{\|X\|}} \in ℝ^{+}$
100	99	rpred	$⊢ φ \to \frac{E}{2 \sqrt{\|X\|}} \in ℝ$
101	100	adantr	$⊢ (φ \land i \in X) \to \frac{E}{2 \sqrt{\|X\|}} \in ℝ$
102	42 101	resubcld	$⊢ (φ \land i \in X) \to Y (i) - (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ$
103	102	rexrd	$⊢ (φ \land i \in X) \to Y (i) - (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ^{*}$
104		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)$
105	103 88 8 104	syl3anc	$⊢ (φ \land i \in X) \to C (i) < Y (i)$
106	25 42 105	ltled	$⊢ (φ \land i \in X) \to C (i) \leq Y (i)$
107	42 101	readdcld	$⊢ (φ \land i \in X) \to Y (i) + (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ$
108	107	rexrd	$⊢ (φ \land i \in X) \to Y (i) + (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ^{*}$
109		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)$
110	88 108 9 109	syl3anc	$⊢ (φ \land i \in X) \to Y (i) < D (i)$
111	87 27 88 106 110	elicod	$⊢ (φ \land i \in X) \to Y (i) \in [C (i), D (i))$
112	38 111	sylan	$⊢ ((φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \land i \in X) \to Y (i) \in [C (i), D (i))$
113		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)$
114	85 84 112 48 113	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)$
115		0red	$⊢ (φ \land i \in X) \to 0 \in ℝ$
116	25 42 26 106 110	lelttrd	$⊢ (φ \land i \in X) \to C (i) < D (i)$
117	25 26	posdifd	$⊢ (φ \land i \in X) \to (C (i) < D (i) \leftrightarrow 0 < D (i) - C (i))$
118	116 117	mpbid	$⊢ (φ \land i \in X) \to 0 < D (i) - C (i)$
119	115 73 118	ltled	$⊢ (φ \land i \in X) \to 0 \leq D (i) - C (i)$
120	73 119	absidd	$⊢ (φ \land i \in X) \to \|D (i) - C (i)\| = D (i) - C (i)$
121	120	eqcomd	$⊢ (φ \land i \in X) \to D (i) - C (i) = \|D (i) - C (i)\|$
122	121	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)\|$
123	114 122	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)\|$
124	50 86 123	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}$
125	62 64 65 124	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}$
126	61 82 66 83 125	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}$
127	38 60 126	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}$
128	38 75	syl	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to \sum_{i \in X} {(D (i) - C (i))}^{2} \in ℝ$
129	38 77	syl	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to 0 \leq \sum_{i \in X} {(D (i) - C (i))}^{2}$
130	54 70 128 129	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}})$
131	127 130	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}}$
132	33 131	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}}$
133	80 97	rerpdivcld	$⊢ φ \to \frac{E}{\sqrt{\|X\|}} \in ℝ$
134	133	resqcld	$⊢ φ \to {(\frac{E}{\sqrt{\|X\|}})}^{2} \in ℝ$
135	134	adantr	$⊢ (φ \land i \in X) \to {(\frac{E}{\sqrt{\|X\|}})}^{2} \in ℝ$
136	26 25	jca	$⊢ (φ \land i \in X) \to (D (i) \in ℝ \land C (i) \in ℝ)$
137	107 102	jca	$⊢ (φ \land i \in X) \to (Y (i) + (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ \land Y (i) - (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ)$
138	136 137	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 ℝ))$
139		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\|}})$
140	88 108 9 139	syl3anc	$⊢ (φ \land i \in X) \to D (i) < Y (i) + (\frac{E}{2 \sqrt{\|X\|}})$
141		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)$
142	103 88 8 141	syl3anc	$⊢ (φ \land i \in X) \to Y (i) - (\frac{E}{2 \sqrt{\|X\|}}) < C (i)$
143	140 142	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))$
144		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\|}})))$
145	138 143 144	sylc	$⊢ (φ \land i \in X) \to D (i) - C (i) < Y (i) + (\frac{E}{2 \sqrt{\|X\|}}) - (Y (i) - (\frac{E}{2 \sqrt{\|X\|}}))$
146	42	recnd	$⊢ (φ \land i \in X) \to Y (i) \in ℂ$
147	101	recnd	$⊢ (φ \land i \in X) \to \frac{E}{2 \sqrt{\|X\|}} \in ℂ$
148	146 147 147	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\|}})$
149	80	recnd	$⊢ φ \to E \in ℂ$
150	97	rpcnd	$⊢ φ \to \sqrt{\|X\|} \in ℂ$
151		2cnd	$⊢ φ \to 2 \in ℂ$
152	97	rpne0d	$⊢ φ \to \sqrt{\|X\|} \neq 0$
153	90	rpne0d	$⊢ φ \to 2 \neq 0$
154	149 150 151 152 153	divdiv3d	$⊢ φ \to \frac{\frac{E}{\sqrt{\|X\|}}}{2} = \frac{E}{2 \sqrt{\|X\|}}$
155	154	eqcomd	$⊢ φ \to \frac{E}{2 \sqrt{\|X\|}} = \frac{\frac{E}{\sqrt{\|X\|}}}{2}$
156	155 155	oveq12d	$⊢ φ \to (\frac{E}{2 \sqrt{\|X\|}}) + (\frac{E}{2 \sqrt{\|X\|}}) = (\frac{\frac{E}{\sqrt{\|X\|}}}{2}) + (\frac{\frac{E}{\sqrt{\|X\|}}}{2})$
157	149 150 152	divcld	$⊢ φ \to \frac{E}{\sqrt{\|X\|}} \in ℂ$
158	157	2halvesd	$⊢ φ \to (\frac{\frac{E}{\sqrt{\|X\|}}}{2}) + (\frac{\frac{E}{\sqrt{\|X\|}}}{2}) = \frac{E}{\sqrt{\|X\|}}$
159	156 158	eqtrd	$⊢ φ \to (\frac{E}{2 \sqrt{\|X\|}}) + (\frac{E}{2 \sqrt{\|X\|}}) = \frac{E}{\sqrt{\|X\|}}$
160	159	adantr	$⊢ (φ \land i \in X) \to (\frac{E}{2 \sqrt{\|X\|}}) + (\frac{E}{2 \sqrt{\|X\|}}) = \frac{E}{\sqrt{\|X\|}}$
161	148 160	eqtrd	$⊢ (φ \land i \in X) \to Y (i) + (\frac{E}{2 \sqrt{\|X\|}}) - (Y (i) - (\frac{E}{2 \sqrt{\|X\|}})) = \frac{E}{\sqrt{\|X\|}}$
162	145 161	breqtrd	$⊢ (φ \land i \in X) \to D (i) - C (i) < \frac{E}{\sqrt{\|X\|}}$
163	133	adantr	$⊢ (φ \land i \in X) \to \frac{E}{\sqrt{\|X\|}} \in ℝ$
164		0red	$⊢ φ \to 0 \in ℝ$
165	97	rpred	$⊢ φ \to \sqrt{\|X\|} \in ℝ$
166	7	rpgt0d	$⊢ φ \to 0 < E$
167	97	rpgt0d	$⊢ φ \to 0 < \sqrt{\|X\|}$
168	80 165 166 167	divgt0d	$⊢ φ \to 0 < \frac{E}{\sqrt{\|X\|}}$
169	164 133 168	ltled	$⊢ φ \to 0 \leq \frac{E}{\sqrt{\|X\|}}$
170	169	adantr	$⊢ (φ \land i \in X) \to 0 \leq \frac{E}{\sqrt{\|X\|}}$
171		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})$
172	73 119 163 170 171	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})$
173	162 172	mpbid	$⊢ (φ \land i \in X) \to {(D (i) - C (i))}^{2} < {(\frac{E}{\sqrt{\|X\|}})}^{2}$
174	2 3 74 135 173	fsumlt	$⊢ φ \to \sum_{i \in X} {(D (i) - C (i))}^{2} < \sum_{i \in X} {(\frac{E}{\sqrt{\|X\|}})}^{2}$
175	2 135	fsumrecl	$⊢ φ \to \sum_{i \in X} {(\frac{E}{\sqrt{\|X\|}})}^{2} \in ℝ$
176	163	sqge0d	$⊢ (φ \land i \in X) \to 0 \leq {(\frac{E}{\sqrt{\|X\|}})}^{2}$
177	2 135 176	fsumge0	$⊢ φ \to 0 \leq \sum_{i \in X} {(\frac{E}{\sqrt{\|X\|}})}^{2}$
178	75 77 175 177	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}})$
179	174 178	mpbid	$⊢ φ \to \sqrt{\sum_{i \in X} {(D (i) - C (i))}^{2}} < \sqrt{\sum_{i \in X} {(\frac{E}{\sqrt{\|X\|}})}^{2}}$
180	134	recnd	$⊢ φ \to {(\frac{E}{\sqrt{\|X\|}})}^{2} \in ℂ$
181		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}$
182	2 180 181	syl2anc	$⊢ φ \to \sum_{i \in X} {(\frac{E}{\sqrt{\|X\|}})}^{2} = \|X\| {(\frac{E}{\sqrt{\|X\|}})}^{2}$
183		sqdiv	$⊢ (E \in ℂ \land \sqrt{\|X\|} \in ℂ \land \sqrt{\|X\|} \neq 0) \to {(\frac{E}{\sqrt{\|X\|}})}^{2} = \frac{E^{2}}{{\sqrt{\|X\|}}^{2}}$
184	149 150 152 183	syl3anc	$⊢ φ \to {(\frac{E}{\sqrt{\|X\|}})}^{2} = \frac{E^{2}}{{\sqrt{\|X\|}}^{2}}$
185	94	recnd	$⊢ φ \to \|X\| \in ℂ$
186		sqrtth	$⊢ \|X\| \in ℂ \to {\sqrt{\|X\|}}^{2} = \|X\|$
187	185 186	syl	$⊢ φ \to {\sqrt{\|X\|}}^{2} = \|X\|$
188	187	oveq2d	$⊢ φ \to \frac{E^{2}}{{\sqrt{\|X\|}}^{2}} = \frac{E^{2}}{\|X\|}$
189	184 188	eqtrd	$⊢ φ \to {(\frac{E}{\sqrt{\|X\|}})}^{2} = \frac{E^{2}}{\|X\|}$
190	189	oveq2d	$⊢ φ \to \|X\| {(\frac{E}{\sqrt{\|X\|}})}^{2} = \|X\| (\frac{E^{2}}{\|X\|})$
191	149	sqcld	$⊢ φ \to E^{2} \in ℂ$
192	164 95	gtned	$⊢ φ \to \|X\| \neq 0$
193	191 185 192	divcan2d	$⊢ φ \to \|X\| (\frac{E^{2}}{\|X\|}) = E^{2}$
194	182 190 193	3eqtrd	$⊢ φ \to \sum_{i \in X} {(\frac{E}{\sqrt{\|X\|}})}^{2} = E^{2}$
195	194	fveq2d	$⊢ φ \to \sqrt{\sum_{i \in X} {(\frac{E}{\sqrt{\|X\|}})}^{2}} = \sqrt{E^{2}}$
196	164 80 166	ltled	$⊢ φ \to 0 \leq E$
197		sqrtsq	$⊢ (E \in ℝ \land 0 \leq E) \to \sqrt{E^{2}} = E$
198	80 196 197	syl2anc	$⊢ φ \to \sqrt{E^{2}} = E$
199		eqidd	$⊢ φ \to E = E$
200	195 198 199	3eqtrd	$⊢ φ \to \sqrt{\sum_{i \in X} {(\frac{E}{\sqrt{\|X\|}})}^{2}} = E$
201	179 200	breqtrd	$⊢ φ \to \sqrt{\sum_{i \in X} {(D (i) - C (i))}^{2}} < E$
202	201	adantr	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to \sqrt{\sum_{i \in X} {(D (i) - C (i))}^{2}} < E$
203	72 79 81 132 202	lttrd	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to Y dist (X) f < E$
204		eqid	$⊢ dist (X) = dist (X)$
205	204	rrxmetfi	$⊢ X \in Fin \to dist (X) \in Met (ℝ^{X})$
206		metxmet	$⊢ dist (X) \in Met (ℝ^{X}) \to dist (X) \in ∞Met (ℝ^{X})$
207	2 205 206	3syl	$⊢ φ \to dist (X) \in ∞Met (ℝ^{X})$
208	207	adantr	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to dist (X) \in ∞Met (ℝ^{X})$
209	81	rexrd	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to E \in ℝ^{*}$
210	31 11	eleqtrdi	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to f \in (ℝ^{X})$
211		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)$
212	208 209 24 210 211	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)$
213	203 212	mpbird	$⊢ (φ \land f \in \underset{i \in X}{⨉} [C (i), D (i))) \to f \in (Y ball (dist (X)) E)$
214	213	ralrimiva	$⊢ φ \to \forall f \in \underset{i \in X}{⨉} [C (i), D (i)) f \in (Y ball (dist (X)) E)$
215		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)$
216	214 215	sylibr	$⊢ φ \to \underset{i \in X}{⨉} [C (i), D (i)) \subseteq Y ball (dist (X)) E$

Metamath Proof Explorer

Theorem hoiqssbllem2

Proof