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	ffvelcdmd	$⊢ (φ \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	birani	$⊢ (\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\|}})))$
90		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$
91		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\|}})))$
92	89 90 91	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\|}})))$
93	92	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\|}})))$
94		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\|}}))$
95	93 94	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\|}}))$
96		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$
97	12	ffvelcdmda	$⊢ (φ \land i \in I) \to X (i) \in ℝ$
98	97	3adant2	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to X (i) \in ℝ$
99		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\|}}))$
100	99	elioored	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to y (i) \in ℝ$
101	98	rexrd	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to X (i) \in ℝ^{*}$
102	17	adantr	$⊢ (φ \land i \in I) \to E \in ℝ$
103	2 22	mpbird	$⊢ φ \to \|I\| \in ℕ$
104	103	nnred	$⊢ φ \to \|I\| \in ℝ$
105	104	adantr	$⊢ (φ \land i \in I) \to \|I\| \in ℝ$
106		0red	$⊢ φ \to 0 \in ℝ$
107	103	nngt0d	$⊢ φ \to 0 < \|I\|$
108	106 104 107	ltled	$⊢ φ \to 0 \leq \|I\|$
109	108	adantr	$⊢ (φ \land i \in I) \to 0 \leq \|I\|$
110	105 109	resqrtcld	$⊢ (φ \land i \in I) \to \sqrt{\|I\|} \in ℝ$
111		sqrtgt0	$⊢ (\|I\| \in ℝ \land 0 < \|I\|) \to 0 < \sqrt{\|I\|}$
112	104 107 111	syl2anc	$⊢ φ \to 0 < \sqrt{\|I\|}$
113	106 112	gtned	$⊢ φ \to \sqrt{\|I\|} \neq 0$
114	113	adantr	$⊢ (φ \land i \in I) \to \sqrt{\|I\|} \neq 0$
115	102 110 114	redivcld	$⊢ (φ \land i \in I) \to \frac{E}{\sqrt{\|I\|}} \in ℝ$
116	97 115	readdcld	$⊢ (φ \land i \in I) \to X (i) + (\frac{E}{\sqrt{\|I\|}}) \in ℝ$
117	116	rexrd	$⊢ (φ \land i \in I) \to X (i) + (\frac{E}{\sqrt{\|I\|}}) \in ℝ^{*}$
118	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 ℝ^{*}$
119		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)$
120	101 118 99 119	syl3anc	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to X (i) < y (i)$
121	98 100 120	ltled	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to X (i) \leq y (i)$
122	98 100 121	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)$
123	116	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 ℝ$
124		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\|}})$
125	101 118 99 124	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\|}})$
126	100 123 98 125	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)$
127	98	recnd	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to X (i) \in ℂ$
128	104 108	resqrtcld	$⊢ φ \to \sqrt{\|I\|} \in ℝ$
129	17 128 113	redivcld	$⊢ φ \to \frac{E}{\sqrt{\|I\|}} \in ℝ$
130	129	recnd	$⊢ φ \to \frac{E}{\sqrt{\|I\|}} \in ℂ$
131	130	3ad2ant1	$⊢ (φ \land y (i) \in (X (i), X (i) + (\frac{E}{\sqrt{\|I\|}})) \land i \in I) \to \frac{E}{\sqrt{\|I\|}} \in ℂ$
132	127 131	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\|}}$
133	126 132	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\|}}$
134	122 133	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\|}}$
135	81 95 96 134	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\|}}$
136	135	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\|}}$
137	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 ℝ^{+}$
138	104 107	elrpd	$⊢ φ \to \|I\| \in ℝ^{+}$
139	138	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 ℝ^{+}$
140	139	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 ℝ^{+}$
141	137 140	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 ℝ^{+}$
142	77 78 79 80 76 136 141 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\|}})$
143	137	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 ℂ$
144	139	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 ℂ$
145	144	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 ℂ$
146	140	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$
147	143 145 146	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$
148	142 147	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$
149	76 148	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)$
150	4	rrxmetfi	$⊢ I \in Fin \to D \in Met (ℝ^{I})$
151	1 150	syl	$⊢ φ \to D \in Met (ℝ^{I})$
152		metxmet	$⊢ D \in Met (ℝ^{I}) \to D \in ∞Met (ℝ^{I})$
153	151 152	syl	$⊢ φ \to D \in ∞Met (ℝ^{I})$
154	17	rexrd	$⊢ φ \to E \in ℝ^{*}$
155		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))$
156	153 3 154 155	syl3anc	$⊢ φ \to (y \in (X ball (D) E) \leftrightarrow (y \in (ℝ^{I}) \land X D y < E))$
157	156	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))$
158	149 157	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)$
159	70 158	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))$
160	159	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)))$
161	160	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)))$
162	58 161	mpd	$⊢ φ \to \exists y (y \in (ℚ^{I}) \land y \in (X ball (D) E))$
163		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))$
164	162 163	sylibr	$⊢ φ \to \exists y \in (ℚ^{I}) y \in (X ball (D) E)$

Metamath Proof Explorer

Theorem qndenserrnbllem

Proof