hoiqssbllem1

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

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

Proof

Step	Hyp	Ref	Expression
1		hoiqssbllem1.i	$⊢ Ⅎ i φ$
2		hoiqssbllem1.x	$⊢ φ \to X \in Fin$
3		hoiqssbllem1.n	$⊢ φ \to X \neq \emptyset$
4		hoiqssbllem1.y	$⊢ φ \to Y \in (ℝ^{X})$
5		hoiqssbllem1.c	$⊢ φ \to C : X ⟶ ℝ$
6		hoiqssbllem1.d	$⊢ φ \to D : X ⟶ ℝ$
7		hoiqssbllem1.e	$⊢ φ \to E \in ℝ^{+}$
8		hoiqssbllem1.l	$⊢ (φ \land i \in X) \to C (i) \in (Y (i) - (\frac{E}{2 \sqrt{\|X\|}}), Y (i))$
9		hoiqssbllem1.r	$⊢ (φ \land i \in X) \to D (i) \in (Y (i), Y (i) + (\frac{E}{2 \sqrt{\|X\|}}))$
10	4	elexd	$⊢ φ \to Y \in V$
11		elmapfn	$⊢ Y \in (ℝ^{X}) \to Y Fn X$
12	4 11	syl	$⊢ φ \to Y Fn X$
13	5	ffvelrnda	$⊢ (φ \land i \in X) \to C (i) \in ℝ$
14	13	rexrd	$⊢ (φ \land i \in X) \to C (i) \in ℝ^{*}$
15	6	ffvelrnda	$⊢ (φ \land i \in X) \to D (i) \in ℝ$
16	15	rexrd	$⊢ (φ \land i \in X) \to D (i) \in ℝ^{*}$
17		elmapi	$⊢ Y \in (ℝ^{X}) \to Y : X ⟶ ℝ$
18	4 17	syl	$⊢ φ \to Y : X ⟶ ℝ$
19	18	ffvelrnda	$⊢ (φ \land i \in X) \to Y (i) \in ℝ$
20	19	rexrd	$⊢ (φ \land i \in X) \to Y (i) \in ℝ^{*}$
21		2rp	$⊢ 2 \in ℝ^{+}$
22	21	a1i	$⊢ φ \to 2 \in ℝ^{+}$
23		hashnncl	$⊢ X \in Fin \to (\|X\| \in ℕ \leftrightarrow X \neq \emptyset)$
24	2 23	syl	$⊢ φ \to (\|X\| \in ℕ \leftrightarrow X \neq \emptyset)$
25	3 24	mpbird	$⊢ φ \to \|X\| \in ℕ$
26	25	nnred	$⊢ φ \to \|X\| \in ℝ$
27	25	nngt0d	$⊢ φ \to 0 < \|X\|$
28	26 27	elrpd	$⊢ φ \to \|X\| \in ℝ^{+}$
29	28	rpsqrtcld	$⊢ φ \to \sqrt{\|X\|} \in ℝ^{+}$
30	22 29	rpmulcld	$⊢ φ \to 2 \sqrt{\|X\|} \in ℝ^{+}$
31	7 30	rpdivcld	$⊢ φ \to \frac{E}{2 \sqrt{\|X\|}} \in ℝ^{+}$
32	31	rpred	$⊢ φ \to \frac{E}{2 \sqrt{\|X\|}} \in ℝ$
33	32	adantr	$⊢ (φ \land i \in X) \to \frac{E}{2 \sqrt{\|X\|}} \in ℝ$
34	19 33	resubcld	$⊢ (φ \land i \in X) \to Y (i) - (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ$
35	34	rexrd	$⊢ (φ \land i \in X) \to Y (i) - (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ^{*}$
36		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)$
37	35 20 8 36	syl3anc	$⊢ (φ \land i \in X) \to C (i) < Y (i)$
38	13 19 37	ltled	$⊢ (φ \land i \in X) \to C (i) \leq Y (i)$
39	19 33	readdcld	$⊢ (φ \land i \in X) \to Y (i) + (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ$
40	39	rexrd	$⊢ (φ \land i \in X) \to Y (i) + (\frac{E}{2 \sqrt{\|X\|}}) \in ℝ^{*}$
41		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)$
42	20 40 9 41	syl3anc	$⊢ (φ \land i \in X) \to Y (i) < D (i)$
43	14 16 20 38 42	elicod	$⊢ (φ \land i \in X) \to Y (i) \in [C (i), D (i))$
44	43	ex	$⊢ φ \to (i \in X \to Y (i) \in [C (i), D (i)))$
45	1 44	ralrimi	$⊢ φ \to \forall i \in X Y (i) \in [C (i), D (i))$
46	10 12 45	3jca	$⊢ φ \to (Y \in V \land Y Fn X \land \forall i \in X Y (i) \in [C (i), D (i)))$
47		elixp2	$⊢ Y \in \underset{i \in X}{⨉} [C (i), D (i)) \leftrightarrow (Y \in V \land Y Fn X \land \forall i \in X Y (i) \in [C (i), D (i)))$
48	46 47	sylibr	$⊢ φ \to Y \in \underset{i \in X}{⨉} [C (i), D (i))$

Metamath Proof Explorer

Theorem hoiqssbllem1

Proof