Metamath Proof Explorer


Theorem 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 φIFin
qndenserrnbllem.n φI
qndenserrnbllem.x φXI
qndenserrnbllem.d D=distmsup
qndenserrnbllem.e φE+
Assertion qndenserrnbllem φyIyXballDE

Proof

Step Hyp Ref Expression
1 qndenserrnbllem.i φIFin
2 qndenserrnbllem.n φI
3 qndenserrnbllem.x φXI
4 qndenserrnbllem.d D=distmsup
5 qndenserrnbllem.e φE+
6 inss1 XkXk+EI
7 qex V
8 ssexg XkXk+EIVXkXk+EIV
9 6 7 8 mp2an XkXk+EIV
10 9 a1i φkIXkXk+EIV
11 elmapi XIX:I
12 3 11 syl φX:I
13 12 adantr φkIX:I
14 simpr φkIkI
15 13 14 ffvelrnd φkIXk
16 15 rexrd φkIXk*
17 5 rpred φE
18 17 adantr φkIE
19 ne0i kII
20 19 adantl φkII
21 hashnncl IFinII
22 1 21 syl φII
23 22 adantr φkIII
24 20 23 mpbird φkII
25 24 nnred φkII
26 0red φkI0
27 24 nngt0d φkI0<I
28 26 25 27 ltled φkI0I
29 25 28 resqrtcld φkII
30 25 27 elrpd φkII+
31 30 sqrtgt0d φkI0<I
32 26 31 gtned φkII0
33 18 29 32 redivcld φkIEI
34 15 33 readdcld φkIXk+EI
35 34 rexrd φkIXk+EI*
36 5 adantr φkIE+
37 29 31 elrpd φkII+
38 36 37 rpdivcld φkIEI+
39 15 38 ltaddrpd φkIXk<Xk+EI
40 qbtwnxr Xk*Xk+EI*Xk<Xk+EIqXk<qq<Xk+EI
41 16 35 39 40 syl3anc φkIqXk<qq<Xk+EI
42 df-rex qXk<qq<Xk+EIqqXk<qq<Xk+EI
43 41 42 sylib φkIqqXk<qq<Xk+EI
44 simprl φkIqXk<qq<Xk+EIq
45 16 adantr φkIqXk<qq<Xk+EIXk*
46 35 adantr φkIqXk<qq<Xk+EIXk+EI*
47 qre qq
48 47 ad2antrl φkIqXk<qq<Xk+EIq
49 simprrl φkIqXk<qq<Xk+EIXk<q
50 simprrr φkIqXk<qq<Xk+EIq<Xk+EI
51 45 46 48 49 50 eliood φkIqXk<qq<Xk+EIqXkXk+EI
52 44 51 elind φkIqXk<qq<Xk+EIqXkXk+EI
53 52 ex φkIqXk<qq<Xk+EIqXkXk+EI
54 53 eximdv φkIqqXk<qq<Xk+EIqqXkXk+EI
55 43 54 mpd φkIqqXkXk+EI
56 n0 XkXk+EIqqXkXk+EI
57 55 56 sylibr φkIXkXk+EI
58 1 10 57 choicefi φyyFnIkIykXkXk+EI
59 6 a1i yFnIXkXk+EI
60 59 sseld yFnIykXkXk+EIyk
61 60 ralimdv yFnIkIykXkXk+EIkIyk
62 61 imdistani yFnIkIykXkXk+EIyFnIkIyk
63 ffnfv y:IyFnIkIyk
64 62 63 sylibr yFnIkIykXkXk+EIy:I
65 64 adantl φyFnIkIykXkXk+EIy:I
66 7 a1i φV
67 elmapg VIFinyIy:I
68 66 1 67 syl2anc φyIy:I
69 68 adantr φyFnIkIykXkXk+EIyIy:I
70 65 69 mpbird φyFnIkIykXkXk+EIyI
71 reex V
72 47 ssriv
73 mapss VII
74 71 72 73 mp2an II
75 74 a1i φyFnIkIykXkXk+EIII
76 75 70 sseldd φyFnIkIykXkXk+EIyI
77 1 adantr φyFnIkIykXkXk+EIIFin
78 2 adantr φyFnIkIykXkXk+EII
79 eqid I=I
80 3 adantr φyFnIkIykXkXk+EIXI
81 simpll φkIykXkXk+EIiIφ
82 fveq2 k=iyk=yi
83 fveq2 k=iXk=Xi
84 83 oveq1d k=iXk+EI=Xi+EI
85 83 84 oveq12d k=iXkXk+EI=XiXi+EI
86 85 ineq2d k=iXkXk+EI=XiXi+EI
87 82 86 eleq12d k=iykXkXk+EIyiXiXi+EI
88 87 cbvralvw kIykXkXk+EIiIyiXiXi+EI
89 88 biimpi kIykXkXk+EIiIyiXiXi+EI
90 89 adantr kIykXkXk+EIiIiIyiXiXi+EI
91 simpr kIykXkXk+EIiIiI
92 rspa iIyiXiXi+EIiIyiXiXi+EI
93 90 91 92 syl2anc kIykXkXk+EIiIyiXiXi+EI
94 93 adantll φkIykXkXk+EIiIyiXiXi+EI
95 elinel2 yiXiXi+EIyiXiXi+EI
96 94 95 syl φkIykXkXk+EIiIyiXiXi+EI
97 simpr φkIykXkXk+EIiIiI
98 12 ffvelrnda φiIXi
99 98 3adant2 φyiXiXi+EIiIXi
100 simp2 φyiXiXi+EIiIyiXiXi+EI
101 100 elioored φyiXiXi+EIiIyi
102 99 rexrd φyiXiXi+EIiIXi*
103 17 adantr φiIE
104 2 22 mpbird φI
105 104 nnred φI
106 105 adantr φiII
107 0red φ0
108 104 nngt0d φ0<I
109 107 105 108 ltled φ0I
110 109 adantr φiI0I
111 106 110 resqrtcld φiII
112 sqrtgt0 I0<I0<I
113 105 108 112 syl2anc φ0<I
114 107 113 gtned φI0
115 114 adantr φiII0
116 103 111 115 redivcld φiIEI
117 98 116 readdcld φiIXi+EI
118 117 rexrd φiIXi+EI*
119 118 3adant2 φyiXiXi+EIiIXi+EI*
120 ioogtlb Xi*Xi+EI*yiXiXi+EIXi<yi
121 102 119 100 120 syl3anc φyiXiXi+EIiIXi<yi
122 99 101 121 ltled φyiXiXi+EIiIXiyi
123 99 101 122 abssuble0d φyiXiXi+EIiIXiyi=yiXi
124 117 3adant2 φyiXiXi+EIiIXi+EI
125 iooltub Xi*Xi+EI*yiXiXi+EIyi<Xi+EI
126 102 119 100 125 syl3anc φyiXiXi+EIiIyi<Xi+EI
127 101 124 99 126 ltsub1dd φyiXiXi+EIiIyiXi<Xi+EI-Xi
128 99 recnd φyiXiXi+EIiIXi
129 105 109 resqrtcld φI
130 17 129 114 redivcld φEI
131 130 recnd φEI
132 131 3ad2ant1 φyiXiXi+EIiIEI
133 128 132 pncan2d φyiXiXi+EIiIXi+EI-Xi=EI
134 127 133 breqtrd φyiXiXi+EIiIyiXi<EI
135 123 134 eqbrtrd φyiXiXi+EIiIXiyi<EI
136 81 96 97 135 syl3anc φkIykXkXk+EIiIXiyi<EI
137 136 adantlrl φyFnIkIykXkXk+EIiIXiyi<EI
138 5 adantr φyFnIkIykXkXk+EIE+
139 105 108 elrpd φI+
140 139 adantr φyFnIkIykXkXk+EII+
141 140 rpsqrtcld φyFnIkIykXkXk+EII+
142 138 141 rpdivcld φyFnIkIykXkXk+EIEI+
143 77 78 79 80 76 137 142 4 rrndistlt φyFnIkIykXkXk+EIXDy<IEI
144 138 rpcnd φyFnIkIykXkXk+EIE
145 140 rpcnd φyFnIkIykXkXk+EII
146 145 sqrtcld φyFnIkIykXkXk+EII
147 141 rpne0d φyFnIkIykXkXk+EII0
148 144 146 147 divcan2d φyFnIkIykXkXk+EIIEI=E
149 143 148 breqtrd φyFnIkIykXkXk+EIXDy<E
150 76 149 jca φyFnIkIykXkXk+EIyIXDy<E
151 4 rrxmetfi IFinDMetI
152 1 151 syl φDMetI
153 metxmet DMetID∞MetI
154 152 153 syl φD∞MetI
155 17 rexrd φE*
156 elbl D∞MetIXIE*yXballDEyIXDy<E
157 154 3 155 156 syl3anc φyXballDEyIXDy<E
158 157 adantr φyFnIkIykXkXk+EIyXballDEyIXDy<E
159 150 158 mpbird φyFnIkIykXkXk+EIyXballDE
160 70 159 jca φyFnIkIykXkXk+EIyIyXballDE
161 160 ex φyFnIkIykXkXk+EIyIyXballDE
162 161 eximdv φyyFnIkIykXkXk+EIyyIyXballDE
163 58 162 mpd φyyIyXballDE
164 df-rex yIyXballDEyyIyXballDE
165 163 164 sylibr φyIyXballDE