qndenserrnbllem

Description: n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	qndenserrnbllem.i	$⊢ φ \to I \in Fin$
	qndenserrnbllem.n	$⊢ φ \to I \neq \emptyset$
	qndenserrnbllem.x	$⊢ φ \to X \in (ℝ^{I})$
	qndenserrnbllem.d	$⊢ D = dist (I)$
	qndenserrnbllem.e	$⊢ φ \to E \in ℝ^{+}$
Assertion	qndenserrnbllem	$⊢ φ \to \exists y \in (ℚ^{I}) y \in (X ball (D) E)$

Proof

Step	Hyp	Ref	Expression
1		qndenserrnbllem.i	$⊢ φ \to I \in Fin$
2		qndenserrnbllem.n	$⊢ φ \to I \neq \emptyset$
3		qndenserrnbllem.x	$⊢ φ \to X \in (ℝ^{I})$
4		qndenserrnbllem.d	$⊢ D = dist (I)$
5		qndenserrnbllem.e	$⊢ φ \to E \in ℝ^{+}$
6		inss1	$⊢ ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})) \subseteq ℚ$
7		qex	$⊢ ℚ \in V$
8		ssexg	$⊢ (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})) \subseteq ℚ \land ℚ \in V) \to ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})) \in V$
9	6 7 8	mp2an	$⊢ ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})) \in V$
10	9	a1i	$⊢ (φ \land k \in I) \to ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})) \in V$
11		elmapi	$⊢ X \in (ℝ^{I}) \to X : I ⟶ ℝ$
12	3 11	syl	$⊢ φ \to X : I ⟶ ℝ$
13	12	adantr	$⊢ (φ \land k \in I) \to X : I ⟶ ℝ$
14		simpr	$⊢ (φ \land k \in I) \to k \in I$
15	13 14	ffvelrnd	$⊢ (φ \land k \in I) \to X (k) \in ℝ$
16	15	rexrd	$⊢ (φ \land k \in I) \to X (k) \in ℝ^{*}$
17	5	rpred	$⊢ φ \to E \in ℝ$
18	17	adantr	$⊢ (φ \land k \in I) \to E \in ℝ$
19		ne0i	$⊢ k \in I \to I \neq \emptyset$
20	19	adantl	$⊢ (φ \land k \in I) \to I \neq \emptyset$
21		hashnncl	$⊢ I \in Fin \to (\|I\| \in ℕ \leftrightarrow I \neq \emptyset)$
22	1 21	syl	$⊢ φ \to (\|I\| \in ℕ \leftrightarrow I \neq \emptyset)$
23	22	adantr	$⊢ (φ \land k \in I) \to (\|I\| \in ℕ \leftrightarrow I \neq \emptyset)$
24	20 23	mpbird	$⊢ (φ \land k \in I) \to \|I\| \in ℕ$
25	24	nnred	$⊢ (φ \land k \in I) \to \|I\| \in ℝ$
26		0red	$⊢ (φ \land k \in I) \to 0 \in ℝ$
27	24	nngt0d	$⊢ (φ \land k \in I) \to 0 < \|I\|$
28	26 25 27	ltled	$⊢ (φ \land k \in I) \to 0 \leq \|I\|$
29	25 28	resqrtcld	$⊢ (φ \land k \in I) \to \sqrt{\|I\|} \in ℝ$
30	25 27	elrpd	$⊢ (φ \land k \in I) \to \|I\| \in ℝ^{+}$
31	30	sqrtgt0d	$⊢ (φ \land k \in I) \to 0 < \sqrt{\|I\|}$
32	26 31	gtned	$⊢ (φ \land k \in I) \to \sqrt{\|I\|} \neq 0$
33	18 29 32	redivcld	$⊢ (φ \land k \in I) \to \frac{E}{\sqrt{\|I\|}} \in ℝ$
34	15 33	readdcld	$⊢ (φ \land k \in I) \to X (k) + (\frac{E}{\sqrt{\|I\|}}) \in ℝ$
35	34	rexrd	$⊢ (φ \land k \in I) \to X (k) + (\frac{E}{\sqrt{\|I\|}}) \in ℝ^{*}$
36	5	adantr	$⊢ (φ \land k \in I) \to E \in ℝ^{+}$
37	29 31	elrpd	$⊢ (φ \land k \in I) \to \sqrt{\|I\|} \in ℝ^{+}$
38	36 37	rpdivcld	$⊢ (φ \land k \in I) \to \frac{E}{\sqrt{\|I\|}} \in ℝ^{+}$
39	15 38	ltaddrpd	$⊢ (φ \land k \in I) \to X (k) < X (k) + (\frac{E}{\sqrt{\|I\|}})$
40		qbtwnxr	$⊢ (X (k) \in ℝ^{} \land X (k) + (\frac{E}{\sqrt{\|I\|}}) \in ℝ^{} \land X (k) < X (k) + (\frac{E}{\sqrt{\|I\|}})) \to \exists q \in ℚ (X (k) < q \land q < X (k) + (\frac{E}{\sqrt{\|I\|}}))$
41	16 35 39 40	syl3anc	$⊢ (φ \land k \in I) \to \exists q \in ℚ (X (k) < q \land q < X (k) + (\frac{E}{\sqrt{\|I\|}}))$
42		df-rex	$⊢ \exists q \in ℚ (X (k) < q \land q < X (k) + (\frac{E}{\sqrt{\|I\|}})) \leftrightarrow \exists q (q \in ℚ \land (X (k) < q \land q < X (k) + (\frac{E}{\sqrt{\|I\|}})))$
43	41 42	sylib	$⊢ (φ \land k \in I) \to \exists q (q \in ℚ \land (X (k) < q \land q < X (k) + (\frac{E}{\sqrt{\|I\|}})))$
44		simprl	$⊢ ((φ \land k \in I) \land (q \in ℚ \land (X (k) < q \land q < X (k) + (\frac{E}{\sqrt{\|I\|}})))) \to q \in ℚ$
45	16	adantr	$⊢ ((φ \land k \in I) \land (q \in ℚ \land (X (k) < q \land q < X (k) + (\frac{E}{\sqrt{\|I\|}})))) \to X (k) \in ℝ^{*}$
46	35	adantr	$⊢ ((φ \land k \in I) \land (q \in ℚ \land (X (k) < q \land q < X (k) + (\frac{E}{\sqrt{\|I\|}})))) \to X (k) + (\frac{E}{\sqrt{\|I\|}}) \in ℝ^{*}$
47		qre	$⊢ q \in ℚ \to q \in ℝ$
48	47	ad2antrl	$⊢ ((φ \land k \in I) \land (q \in ℚ \land (X (k) < q \land q < X (k) + (\frac{E}{\sqrt{\|I\|}})))) \to q \in ℝ$
49		simprrl	$⊢ ((φ \land k \in I) \land (q \in ℚ \land (X (k) < q \land q < X (k) + (\frac{E}{\sqrt{\|I\|}})))) \to X (k) < q$
50		simprrr	$⊢ ((φ \land k \in I) \land (q \in ℚ \land (X (k) < q \land q < X (k) + (\frac{E}{\sqrt{\|I\|}})))) \to q < X (k) + (\frac{E}{\sqrt{\|I\|}})$
51	45 46 48 49 50	eliood	$⊢ ((φ \land k \in I) \land (q \in ℚ \land (X (k) < q \land q < X (k) + (\frac{E}{\sqrt{\|I\|}})))) \to q \in (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))$
52	44 51	elind	$⊢ ((φ \land k \in I) \land (q \in ℚ \land (X (k) < q \land q < X (k) + (\frac{E}{\sqrt{\|I\|}})))) \to q \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})))$
53	52	ex	$⊢ (φ \land k \in I) \to ((q \in ℚ \land (X (k) < q \land q < X (k) + (\frac{E}{\sqrt{\|I\|}}))) \to q \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))$
54	53	eximdv	$⊢ (φ \land k \in I) \to (\exists q (q \in ℚ \land (X (k) < q \land q < X (k) + (\frac{E}{\sqrt{\|I\|}}))) \to \exists q q \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))$
55	43 54	mpd	$⊢ (φ \land k \in I) \to \exists q q \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})))$
56		n0	$⊢ ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})) \neq \emptyset \leftrightarrow \exists q q \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})))$
57	55 56	sylibr	$⊢ (φ \land k \in I) \to ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})) \neq \emptyset$
58	1 10 57	choicefi	$⊢ φ \to \exists y (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))$
59	6	a1i	$⊢ y Fn I \to ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})) \subseteq ℚ$
60	59	sseld	$⊢ y Fn I \to (y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))) \to y (k) \in ℚ)$
61	60	ralimdv	$⊢ y Fn I \to (\forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))) \to \forall k \in I y (k) \in ℚ)$
62	61	imdistani	$⊢ (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})))) \to (y Fn I \land \forall k \in I y (k) \in ℚ)$
63		ffnfv	$⊢ y : I ⟶ ℚ \leftrightarrow (y Fn I \land \forall k \in I y (k) \in ℚ)$
64	62 63	sylibr	$⊢ (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})))) \to y : I ⟶ ℚ$
65	64	adantl	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to y : I ⟶ ℚ$
66	7	a1i	$⊢ φ \to ℚ \in V$
67		elmapg	$⊢ (ℚ \in V \land I \in Fin) \to (y \in (ℚ^{I}) \leftrightarrow y : I ⟶ ℚ)$
68	66 1 67	syl2anc	$⊢ φ \to (y \in (ℚ^{I}) \leftrightarrow y : I ⟶ ℚ)$
69	68	adantr	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to (y \in (ℚ^{I}) \leftrightarrow y : I ⟶ ℚ)$
70	65 69	mpbird	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to y \in (ℚ^{I})$
71		reex	$⊢ ℝ \in V$
72	47	ssriv	$⊢ ℚ \subseteq ℝ$
73		mapss	$⊢ (ℝ \in V \land ℚ \subseteq ℝ) \to ℚ^{I} \subseteq ℝ^{I}$
74	71 72 73	mp2an	$⊢ ℚ^{I} \subseteq ℝ^{I}$
75	74	a1i	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to ℚ^{I} \subseteq ℝ^{I}$
76	75 70	sseldd	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to y \in (ℝ^{I})$
77	1	adantr	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to I \in Fin$
78	2	adantr	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to I \neq \emptyset$
79		eqid	$⊢ \|I\| = \|I\|$
80	3	adantr	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to X \in (ℝ^{I})$
81		simpll	$⊢ ((φ \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})))) \land i \in I) \to φ$
82		fveq2	$⊢ k = i \to y (k) = y (i)$
83		fveq2	$⊢ k = i \to X (k) = X (i)$
84	83	oveq1d	$⊢ k = i \to X (k) + (\frac{E}{\sqrt{\|I\|}}) = X (i) + (\frac{E}{\sqrt{\|I\|}})$
85	83 84	oveq12d	$⊢ k = i \to (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})) = (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}}))$
86	85	ineq2d	$⊢ k = i \to ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})) = ℚ \cap (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}}))$
87	82 86	eleq12d	$⊢ k = i \to (y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))) \leftrightarrow y (i) \in (ℚ \cap (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}}))))$
88	87	cbvralvw	$⊢ \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))) \leftrightarrow \forall i \in I y (i) \in (ℚ \cap (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})))$
89	88	biimpi	$⊢ \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))) \to \forall i \in I y (i) \in (ℚ \cap (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})))$
90	89	adantr	$⊢ (\forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))) \land i \in I) \to \forall i \in I y (i) \in (ℚ \cap (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})))$
91		simpr	$⊢ (\forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))) \land i \in I) \to i \in I$
92		rspa	$⊢ (\forall i \in I y (i) \in (ℚ \cap (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}}))) \land i \in I) \to y (i) \in (ℚ \cap (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})))$
93	90 91 92	syl2anc	$⊢ (\forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))) \land i \in I) \to y (i) \in (ℚ \cap (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})))$
94	93	adantll	$⊢ ((φ \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})))) \land i \in I) \to y (i) \in (ℚ \cap (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})))$
95		elinel2	$⊢ y (i) \in (ℚ \cap (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}}))) \to y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}}))$
96	94 95	syl	$⊢ ((φ \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})))) \land i \in I) \to y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}}))$
97		simpr	$⊢ ((φ \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})))) \land i \in I) \to i \in I$
98	12	ffvelrnda	$⊢ (φ \land i \in I) \to X (i) \in ℝ$
99	98	3adant2	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to X (i) \in ℝ$
100		simp2	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}}))$
101	100	elioored	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to y (i) \in ℝ$
102	99	rexrd	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to X (i) \in ℝ^{*}$
103	17	adantr	$⊢ (φ \land i \in I) \to E \in ℝ$
104	2 22	mpbird	$⊢ φ \to \|I\| \in ℕ$
105	104	nnred	$⊢ φ \to \|I\| \in ℝ$
106	105	adantr	$⊢ (φ \land i \in I) \to \|I\| \in ℝ$
107		0red	$⊢ φ \to 0 \in ℝ$
108	104	nngt0d	$⊢ φ \to 0 < \|I\|$
109	107 105 108	ltled	$⊢ φ \to 0 \leq \|I\|$
110	109	adantr	$⊢ (φ \land i \in I) \to 0 \leq \|I\|$
111	106 110	resqrtcld	$⊢ (φ \land i \in I) \to \sqrt{\|I\|} \in ℝ$
112		sqrtgt0	$⊢ (\|I\| \in ℝ \land 0 < \|I\|) \to 0 < \sqrt{\|I\|}$
113	105 108 112	syl2anc	$⊢ φ \to 0 < \sqrt{\|I\|}$
114	107 113	gtned	$⊢ φ \to \sqrt{\|I\|} \neq 0$
115	114	adantr	$⊢ (φ \land i \in I) \to \sqrt{\|I\|} \neq 0$
116	103 111 115	redivcld	$⊢ (φ \land i \in I) \to \frac{E}{\sqrt{\|I\|}} \in ℝ$
117	98 116	readdcld	$⊢ (φ \land i \in I) \to X (i) + (\frac{E}{\sqrt{\|I\|}}) \in ℝ$
118	117	rexrd	$⊢ (φ \land i \in I) \to X (i) + (\frac{E}{\sqrt{\|I\|}}) \in ℝ^{*}$
119	118	3adant2	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to X (i) + (\frac{E}{\sqrt{\|I\|}}) \in ℝ^{*}$
120		ioogtlb	$⊢ (X (i) \in ℝ^{} \land X (i) + (\frac{E}{\sqrt{\|I\|}}) \in ℝ^{} \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}}))) \to X (i) < y (i)$
121	102 119 100 120	syl3anc	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to X (i) < y (i)$
122	99 101 121	ltled	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to X (i) \leq y (i)$
123	99 101 122	abssuble0d	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to \|X (i) - y (i)\| = y (i) - X (i)$
124	117	3adant2	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to X (i) + (\frac{E}{\sqrt{\|I\|}}) \in ℝ$
125		iooltub	$⊢ (X (i) \in ℝ^{} \land X (i) + (\frac{E}{\sqrt{\|I\|}}) \in ℝ^{} \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}}))) \to y (i) < X (i) + (\frac{E}{\sqrt{\|I\|}})$
126	102 119 100 125	syl3anc	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to y (i) < X (i) + (\frac{E}{\sqrt{\|I\|}})$
127	101 124 99 126	ltsub1dd	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to y (i) - X (i) < X (i) + (\frac{E}{\sqrt{\|I\|}}) - X (i)$
128	99	recnd	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to X (i) \in ℂ$
129	105 109	resqrtcld	$⊢ φ \to \sqrt{\|I\|} \in ℝ$
130	17 129 114	redivcld	$⊢ φ \to \frac{E}{\sqrt{\|I\|}} \in ℝ$
131	130	recnd	$⊢ φ \to \frac{E}{\sqrt{\|I\|}} \in ℂ$
132	131	3ad2ant1	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to \frac{E}{\sqrt{\|I\|}} \in ℂ$
133	128 132	pncan2d	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to X (i) + (\frac{E}{\sqrt{\|I\|}}) - X (i) = \frac{E}{\sqrt{\|I\|}}$
134	127 133	breqtrd	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to y (i) - X (i) < \frac{E}{\sqrt{\|I\|}}$
135	123 134	eqbrtrd	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to \|X (i) - y (i)\| < \frac{E}{\sqrt{\|I\|}}$
136	81 96 97 135	syl3anc	$⊢ ((φ \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})))) \land i \in I) \to \|X (i) - y (i)\| < \frac{E}{\sqrt{\|I\|}}$
137	136	adantlrl	$⊢ ((φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \land i \in I) \to \|X (i) - y (i)\| < \frac{E}{\sqrt{\|I\|}}$
138	5	adantr	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to E \in ℝ^{+}$
139	105 108	elrpd	$⊢ φ \to \|I\| \in ℝ^{+}$
140	139	adantr	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to \|I\| \in ℝ^{+}$
141	140	rpsqrtcld	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to \sqrt{\|I\|} \in ℝ^{+}$
142	138 141	rpdivcld	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to \frac{E}{\sqrt{\|I\|}} \in ℝ^{+}$
143	77 78 79 80 76 137 142 4	rrndistlt	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to X D y < \sqrt{\|I\|} (\frac{E}{\sqrt{\|I\|}})$
144	138	rpcnd	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to E \in ℂ$
145	140	rpcnd	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to \|I\| \in ℂ$
146	145	sqrtcld	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to \sqrt{\|I\|} \in ℂ$
147	141	rpne0d	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to \sqrt{\|I\|} \neq 0$
148	144 146 147	divcan2d	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to \sqrt{\|I\|} (\frac{E}{\sqrt{\|I\|}}) = E$
149	143 148	breqtrd	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to X D y < E$
150	76 149	jca	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to (y \in (ℝ^{I}) \land X D y < E)$
151	4	rrxmetfi	$⊢ I \in Fin \to D \in Met (ℝ^{I})$
152	1 151	syl	$⊢ φ \to D \in Met (ℝ^{I})$
153		metxmet	$⊢ D \in Met (ℝ^{I}) \to D \in ∞Met (ℝ^{I})$
154	152 153	syl	$⊢ φ \to D \in ∞Met (ℝ^{I})$
155	17	rexrd	$⊢ φ \to E \in ℝ^{*}$
156		elbl	$⊢ (D \in ∞Met (ℝ^{I}) \land X \in (ℝ^{I}) \land E \in ℝ^{*}) \to (y \in (X ball (D) E) \leftrightarrow (y \in (ℝ^{I}) \land X D y < E))$
157	154 3 155 156	syl3anc	$⊢ φ \to (y \in (X ball (D) E) \leftrightarrow (y \in (ℝ^{I}) \land X D y < E))$
158	157	adantr	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to (y \in (X ball (D) E) \leftrightarrow (y \in (ℝ^{I}) \land X D y < E))$
159	150 158	mpbird	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to y \in (X ball (D) E)$
160	70 159	jca	$⊢ (φ \land (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}}))))) \to (y \in (ℚ^{I}) \land y \in (X ball (D) E))$
161	160	ex	$⊢ φ \to ((y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})))) \to (y \in (ℚ^{I}) \land y \in (X ball (D) E)))$
162	161	eximdv	$⊢ φ \to (\exists y (y Fn I \land \forall k \in I y (k) \in (ℚ \cap (X (k), X (k) + (\frac{E}{\sqrt{\|I\|}})))) \to \exists y (y \in (ℚ^{I}) \land y \in (X ball (D) E)))$
163	58 162	mpd	$⊢ φ \to \exists y (y \in (ℚ^{I}) \land y \in (X ball (D) E))$
164		df-rex	$⊢ \exists y \in (ℚ^{I}) y \in (X ball (D) E) \leftrightarrow \exists y (y \in (ℚ^{I}) \land y \in (X ball (D) E))$
165	163 164	sylibr	$⊢ φ \to \exists y \in (ℚ^{I}) y \in (X ball (D) E)$

Metamath Proof Explorer

Theorem qndenserrnbllem

Proof