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 
|- ( ph -> I e. Fin )
qndenserrnbllem.n 
|- ( ph -> I =/= (/) )
qndenserrnbllem.x 
|- ( ph -> X e. ( RR ^m I ) )
qndenserrnbllem.d 
|- D = ( dist ` ( RR^ ` I ) )
qndenserrnbllem.e 
|- ( ph -> E e. RR+ )
Assertion qndenserrnbllem 
|- ( ph -> E. y e. ( QQ ^m I ) y e. ( X ( ball ` D ) E ) )

Proof

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