Metamath Proof Explorer

Theorem hoiqssbllem2

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

Ref Expression
Hypotheses hoiqssbllem2.i 
|- F/ i ph
hoiqssbllem2.x 
|- ( ph -> X e. Fin )
hoiqssbllem2.n 
|- ( ph -> X =/= (/) )
hoiqssbllem2.y 
|- ( ph -> Y e. ( RR ^m X ) )
hoiqssbllem2.c 
|- ( ph -> C : X --> RR )
hoiqssbllem2.d 
|- ( ph -> D : X --> RR )
hoiqssbllem2.e 
|- ( ph -> E e. RR+ )
hoiqssbllem2.l 
|- ( ( ph /\ i e. X ) -> ( C ` i ) e. ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) )
hoiqssbllem2.r 
|- ( ( ph /\ i e. X ) -> ( D ` i ) e. ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) )
Assertion hoiqssbllem2 
|- ( ph -> X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) )

Proof

Step Hyp Ref Expression
1 hoiqssbllem2.i 
 |-  F/ i ph
2 hoiqssbllem2.x 
 |-  ( ph -> X e. Fin )
3 hoiqssbllem2.n 
 |-  ( ph -> X =/= (/) )
4 hoiqssbllem2.y 
 |-  ( ph -> Y e. ( RR ^m X ) )
5 hoiqssbllem2.c 
 |-  ( ph -> C : X --> RR )
6 hoiqssbllem2.d 
 |-  ( ph -> D : X --> RR )
7 hoiqssbllem2.e 
 |-  ( ph -> E e. RR+ )
8 hoiqssbllem2.l 
 |-  ( ( ph /\ i e. X ) -> ( C ` i ) e. ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) )
9 hoiqssbllem2.r 
 |-  ( ( ph /\ i e. X ) -> ( D ` i ) e. ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) )
10 eqid 
 |-  ( RR^ ` X ) = ( RR^ ` X )
11 eqid 
 |-  ( RR ^m X ) = ( RR ^m X )
12 10 11 rrxdsfi 
 |-  ( X e. Fin -> ( dist ` ( RR^ ` X ) ) = ( g e. ( RR ^m X ) , h e. ( RR ^m X ) |-> ( sqrt ` sum_ i e. X ( ( ( g ` i ) - ( h ` i ) ) ^ 2 ) ) ) )
13 2 12 syl 
 |-  ( ph -> ( dist ` ( RR^ ` X ) ) = ( g e. ( RR ^m X ) , h e. ( RR ^m X ) |-> ( sqrt ` sum_ i e. X ( ( ( g ` i ) - ( h ` i ) ) ^ 2 ) ) ) )
14 13 adantr 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> ( dist ` ( RR^ ` X ) ) = ( g e. ( RR ^m X ) , h e. ( RR ^m X ) |-> ( sqrt ` sum_ i e. X ( ( ( g ` i ) - ( h ` i ) ) ^ 2 ) ) ) )
15 fveq1 
 |-  ( g = Y -> ( g ` i ) = ( Y ` i ) )
16 15 adantr 
 |-  ( ( g = Y /\ h = f ) -> ( g ` i ) = ( Y ` i ) )
17 fveq1 
 |-  ( h = f -> ( h ` i ) = ( f ` i ) )
18 17 adantl 
 |-  ( ( g = Y /\ h = f ) -> ( h ` i ) = ( f ` i ) )
19 16 18 oveq12d 
 |-  ( ( g = Y /\ h = f ) -> ( ( g ` i ) - ( h ` i ) ) = ( ( Y ` i ) - ( f ` i ) ) )
20 19 oveq1d 
 |-  ( ( g = Y /\ h = f ) -> ( ( ( g ` i ) - ( h ` i ) ) ^ 2 ) = ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) )
21 20 sumeq2sdv 
 |-  ( ( g = Y /\ h = f ) -> sum_ i e. X ( ( ( g ` i ) - ( h ` i ) ) ^ 2 ) = sum_ i e. X ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) )
22 21 fveq2d 
 |-  ( ( g = Y /\ h = f ) -> ( sqrt ` sum_ i e. X ( ( ( g ` i ) - ( h ` i ) ) ^ 2 ) ) = ( sqrt ` sum_ i e. X ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) ) )
23 22 adantl 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ ( g = Y /\ h = f ) ) -> ( sqrt ` sum_ i e. X ( ( ( g ` i ) - ( h ` i ) ) ^ 2 ) ) = ( sqrt ` sum_ i e. X ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) ) )
24 4 adantr 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> Y e. ( RR ^m X ) )
25 5 ffvelrnda 
 |-  ( ( ph /\ i e. X ) -> ( C ` i ) e. RR )
26 6 ffvelrnda 
 |-  ( ( ph /\ i e. X ) -> ( D ` i ) e. RR )
27 26 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( D ` i ) e. RR* )
28 1 25 27 hoissrrn2 
 |-  ( ph -> X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) C_ ( RR ^m X ) )
29 28 adantr 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) C_ ( RR ^m X ) )
30 simpr 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) )
31 29 30 sseldd 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> f e. ( RR ^m X ) )
32 fvexd 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> ( sqrt ` sum_ i e. X ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) ) e. _V )
33 14 23 24 31 32 ovmpod 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> ( Y ( dist ` ( RR^ ` X ) ) f ) = ( sqrt ` sum_ i e. X ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) ) )
34 nfcv 
 |-  F/_ i f
35 nfixp1 
 |-  F/_ i X_ i e. X ( ( C ` i ) [,) ( D ` i ) )
36 34 35 nfel 
 |-  F/ i f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) )
37 1 36 nfan 
 |-  F/ i ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) )
38 simpl 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> ph )
39 38 2 syl 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> X e. Fin )
40 elmapi 
 |-  ( Y e. ( RR ^m X ) -> Y : X --> RR )
41 4 40 syl 
 |-  ( ph -> Y : X --> RR )
42 41 ffvelrnda 
 |-  ( ( ph /\ i e. X ) -> ( Y ` i ) e. RR )
43 38 42 sylan 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> ( Y ` i ) e. RR )
44 icossre 
 |-  ( ( ( C ` i ) e. RR /\ ( D ` i ) e. RR* ) -> ( ( C ` i ) [,) ( D ` i ) ) C_ RR )
45 25 27 44 syl2anc 
 |-  ( ( ph /\ i e. X ) -> ( ( C ` i ) [,) ( D ` i ) ) C_ RR )
46 45 adantlr 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> ( ( C ` i ) [,) ( D ` i ) ) C_ RR )
47 fvixp2 
 |-  ( ( f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) /\ i e. X ) -> ( f ` i ) e. ( ( C ` i ) [,) ( D ` i ) ) )
48 47 adantll 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> ( f ` i ) e. ( ( C ` i ) [,) ( D ` i ) ) )
49 46 48 sseldd 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> ( f ` i ) e. RR )
50 43 49 resubcld 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> ( ( Y ` i ) - ( f ` i ) ) e. RR )
51 2nn0 
 |-  2 e. NN0
52 51 a1i 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> 2 e. NN0 )
53 50 52 reexpcld 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) e. RR )
54 37 39 53 fsumreclf 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> sum_ i e. X ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) e. RR )
55 fveq2 
 |-  ( i = j -> ( C ` i ) = ( C ` j ) )
56 fveq2 
 |-  ( i = j -> ( D ` i ) = ( D ` j ) )
57 55 56 oveq12d 
 |-  ( i = j -> ( ( C ` i ) [,) ( D ` i ) ) = ( ( C ` j ) [,) ( D ` j ) ) )
58 57 cbvixpv 
 |-  X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) = X_ j e. X ( ( C ` j ) [,) ( D ` j ) )
59 58 eleq2i 
 |-  ( f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) <-> f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) )
60 59 biimpi 
 |-  ( f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) -> f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) )
61 60 adantl 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) )
62 2 adantr 
 |-  ( ( ph /\ f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) ) -> X e. Fin )
63 simpll 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) ) /\ i e. X ) -> ph )
64 59 biimpri 
 |-  ( f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) -> f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) )
65 64 ad2antlr 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) ) /\ i e. X ) -> f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) )
66 simpr 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) ) /\ i e. X ) -> i e. X )
67 63 65 66 53 syl21anc 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) ) /\ i e. X ) -> ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) e. RR )
68 50 sqge0d 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> 0 <_ ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) )
69 63 65 66 68 syl21anc 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) ) /\ i e. X ) -> 0 <_ ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) )
70 62 67 69 fsumge0 
 |-  ( ( ph /\ f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) ) -> 0 <_ sum_ i e. X ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) )
71 38 61 70 syl2anc 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> 0 <_ sum_ i e. X ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) )
72 54 71 resqrtcld 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> ( sqrt ` sum_ i e. X ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) ) e. RR )
73 33 72 eqeltrd 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> ( Y ( dist ` ( RR^ ` X ) ) f ) e. RR )
74 26 25 resubcld 
 |-  ( ( ph /\ i e. X ) -> ( ( D ` i ) - ( C ` i ) ) e. RR )
75 74 resqcld 
 |-  ( ( ph /\ i e. X ) -> ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) e. RR )
76 2 75 fsumrecl 
 |-  ( ph -> sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) e. RR )
77 74 sqge0d 
 |-  ( ( ph /\ i e. X ) -> 0 <_ ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) )
78 2 75 77 fsumge0 
 |-  ( ph -> 0 <_ sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) )
79 76 78 resqrtcld 
 |-  ( ph -> ( sqrt ` sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) ) e. RR )
80 79 adantr 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> ( sqrt ` sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) ) e. RR )
81 7 rpred 
 |-  ( ph -> E e. RR )
82 81 adantr 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> E e. RR )
83 3 adantr 
 |-  ( ( ph /\ f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) ) -> X =/= (/) )
84 75 adantlr 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) ) /\ i e. X ) -> ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) e. RR )
85 38 26 sylan 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> ( D ` i ) e. RR )
86 38 25 sylan 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> ( C ` i ) e. RR )
87 85 86 resubcld 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> ( ( D ` i ) - ( C ` i ) ) e. RR )
88 25 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( C ` i ) e. RR* )
89 42 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( Y ` i ) e. RR* )
90 2rp 
 |-  2 e. RR+
91 90 a1i 
 |-  ( ph -> 2 e. RR+ )
92 hashnncl 
 |-  ( X e. Fin -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
93 2 92 syl 
 |-  ( ph -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
94 3 93 mpbird 
 |-  ( ph -> ( # ` X ) e. NN )
95 94 nnred 
 |-  ( ph -> ( # ` X ) e. RR )
96 94 nngt0d 
 |-  ( ph -> 0 < ( # ` X ) )
97 95 96 elrpd 
 |-  ( ph -> ( # ` X ) e. RR+ )
98 97 rpsqrtcld 
 |-  ( ph -> ( sqrt ` ( # ` X ) ) e. RR+ )
99 91 98 rpmulcld 
 |-  ( ph -> ( 2 x. ( sqrt ` ( # ` X ) ) ) e. RR+ )
100 7 99 rpdivcld 
 |-  ( ph -> ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) e. RR+ )
101 100 rpred 
 |-  ( ph -> ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) e. RR )
102 101 adantr 
 |-  ( ( ph /\ i e. X ) -> ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) e. RR )
103 42 102 resubcld 
 |-  ( ( ph /\ i e. X ) -> ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR )
104 103 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR* )
105 iooltub 
 |-  ( ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR* /\ ( Y ` i ) e. RR* /\ ( C ` i ) e. ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) -> ( C ` i ) < ( Y ` i ) )
106 104 89 8 105 syl3anc 
 |-  ( ( ph /\ i e. X ) -> ( C ` i ) < ( Y ` i ) )
107 25 42 106 ltled 
 |-  ( ( ph /\ i e. X ) -> ( C ` i ) <_ ( Y ` i ) )
108 42 102 readdcld 
 |-  ( ( ph /\ i e. X ) -> ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR )
109 108 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR* )
110 ioogtlb 
 |-  ( ( ( Y ` i ) e. RR* /\ ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR* /\ ( D ` i ) e. ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) -> ( Y ` i ) < ( D ` i ) )
111 89 109 9 110 syl3anc 
 |-  ( ( ph /\ i e. X ) -> ( Y ` i ) < ( D ` i ) )
112 88 27 89 107 111 elicod 
 |-  ( ( ph /\ i e. X ) -> ( Y ` i ) e. ( ( C ` i ) [,) ( D ` i ) ) )
113 38 112 sylan 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> ( Y ` i ) e. ( ( C ` i ) [,) ( D ` i ) ) )
114 icodiamlt 
 |-  ( ( ( ( C ` i ) e. RR /\ ( D ` i ) e. RR ) /\ ( ( Y ` i ) e. ( ( C ` i ) [,) ( D ` i ) ) /\ ( f ` i ) e. ( ( C ` i ) [,) ( D ` i ) ) ) ) -> ( abs ` ( ( Y ` i ) - ( f ` i ) ) ) < ( ( D ` i ) - ( C ` i ) ) )
115 86 85 113 48 114 syl22anc 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> ( abs ` ( ( Y ` i ) - ( f ` i ) ) ) < ( ( D ` i ) - ( C ` i ) ) )
116 0red 
 |-  ( ( ph /\ i e. X ) -> 0 e. RR )
117 25 42 26 107 111 lelttrd 
 |-  ( ( ph /\ i e. X ) -> ( C ` i ) < ( D ` i ) )
118 25 26 posdifd 
 |-  ( ( ph /\ i e. X ) -> ( ( C ` i ) < ( D ` i ) <-> 0 < ( ( D ` i ) - ( C ` i ) ) ) )
119 117 118 mpbid 
 |-  ( ( ph /\ i e. X ) -> 0 < ( ( D ` i ) - ( C ` i ) ) )
120 116 74 119 ltled 
 |-  ( ( ph /\ i e. X ) -> 0 <_ ( ( D ` i ) - ( C ` i ) ) )
121 74 120 absidd 
 |-  ( ( ph /\ i e. X ) -> ( abs ` ( ( D ` i ) - ( C ` i ) ) ) = ( ( D ` i ) - ( C ` i ) ) )
122 121 eqcomd 
 |-  ( ( ph /\ i e. X ) -> ( ( D ` i ) - ( C ` i ) ) = ( abs ` ( ( D ` i ) - ( C ` i ) ) ) )
123 122 adantlr 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> ( ( D ` i ) - ( C ` i ) ) = ( abs ` ( ( D ` i ) - ( C ` i ) ) ) )
124 115 123 breqtrd 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> ( abs ` ( ( Y ` i ) - ( f ` i ) ) ) < ( abs ` ( ( D ` i ) - ( C ` i ) ) ) )
125 50 87 124 abslt2sqd 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) < ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) )
126 63 65 66 125 syl21anc 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) ) /\ i e. X ) -> ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) < ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) )
127 62 83 67 84 126 fsumlt 
 |-  ( ( ph /\ f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) ) -> sum_ i e. X ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) < sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) )
128 38 61 127 syl2anc 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> sum_ i e. X ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) < sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) )
129 38 76 syl 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) e. RR )
130 38 78 syl 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> 0 <_ sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) )
131 54 71 129 130 sqrtltd 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> ( sum_ i e. X ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) < sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) <-> ( sqrt ` sum_ i e. X ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) ) < ( sqrt ` sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) ) ) )
132 128 131 mpbid 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> ( sqrt ` sum_ i e. X ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) ) < ( sqrt ` sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) ) )
133 33 132 eqbrtrd 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> ( Y ( dist ` ( RR^ ` X ) ) f ) < ( sqrt ` sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) ) )
134 81 98 rerpdivcld 
 |-  ( ph -> ( E / ( sqrt ` ( # ` X ) ) ) e. RR )
135 134 resqcld 
 |-  ( ph -> ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) e. RR )
136 135 adantr 
 |-  ( ( ph /\ i e. X ) -> ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) e. RR )
137 26 25 jca 
 |-  ( ( ph /\ i e. X ) -> ( ( D ` i ) e. RR /\ ( C ` i ) e. RR ) )
138 108 103 jca 
 |-  ( ( ph /\ i e. X ) -> ( ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR /\ ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR ) )
139 137 138 jca 
 |-  ( ( ph /\ i e. X ) -> ( ( ( D ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR /\ ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR ) ) )
140 iooltub 
 |-  ( ( ( Y ` i ) e. RR* /\ ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR* /\ ( D ` i ) e. ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) -> ( D ` i ) < ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) )
141 89 109 9 140 syl3anc 
 |-  ( ( ph /\ i e. X ) -> ( D ` i ) < ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) )
142 ioogtlb 
 |-  ( ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR* /\ ( Y ` i ) e. RR* /\ ( C ` i ) e. ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) -> ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) < ( C ` i ) )
143 104 89 8 142 syl3anc 
 |-  ( ( ph /\ i e. X ) -> ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) < ( C ` i ) )
144 141 143 jca 
 |-  ( ( ph /\ i e. X ) -> ( ( D ` i ) < ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) /\ ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) < ( C ` i ) ) )
145 lt2sub 
 |-  ( ( ( ( D ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR /\ ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR ) ) -> ( ( ( D ` i ) < ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) /\ ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) < ( C ` i ) ) -> ( ( D ` i ) - ( C ` i ) ) < ( ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) - ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) )
146 139 144 145 sylc 
 |-  ( ( ph /\ i e. X ) -> ( ( D ` i ) - ( C ` i ) ) < ( ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) - ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) )
147 42 recnd 
 |-  ( ( ph /\ i e. X ) -> ( Y ` i ) e. CC )
148 102 recnd 
 |-  ( ( ph /\ i e. X ) -> ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) e. CC )
149 147 148 148 pnncand 
 |-  ( ( ph /\ i e. X ) -> ( ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) - ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) = ( ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) )
150 81 recnd 
 |-  ( ph -> E e. CC )
151 98 rpcnd 
 |-  ( ph -> ( sqrt ` ( # ` X ) ) e. CC )
152 2cnd 
 |-  ( ph -> 2 e. CC )
153 98 rpne0d 
 |-  ( ph -> ( sqrt ` ( # ` X ) ) =/= 0 )
154 91 rpne0d 
 |-  ( ph -> 2 =/= 0 )
155 150 151 152 153 154 divdiv3d 
 |-  ( ph -> ( ( E / ( sqrt ` ( # ` X ) ) ) / 2 ) = ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) )
156 155 eqcomd 
 |-  ( ph -> ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) = ( ( E / ( sqrt ` ( # ` X ) ) ) / 2 ) )
157 156 156 oveq12d 
 |-  ( ph -> ( ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) = ( ( ( E / ( sqrt ` ( # ` X ) ) ) / 2 ) + ( ( E / ( sqrt ` ( # ` X ) ) ) / 2 ) ) )
158 150 151 153 divcld 
 |-  ( ph -> ( E / ( sqrt ` ( # ` X ) ) ) e. CC )
159 158 2halvesd 
 |-  ( ph -> ( ( ( E / ( sqrt ` ( # ` X ) ) ) / 2 ) + ( ( E / ( sqrt ` ( # ` X ) ) ) / 2 ) ) = ( E / ( sqrt ` ( # ` X ) ) ) )
160 157 159 eqtrd 
 |-  ( ph -> ( ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) = ( E / ( sqrt ` ( # ` X ) ) ) )
161 160 adantr 
 |-  ( ( ph /\ i e. X ) -> ( ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) = ( E / ( sqrt ` ( # ` X ) ) ) )
162 149 161 eqtrd 
 |-  ( ( ph /\ i e. X ) -> ( ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) - ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) = ( E / ( sqrt ` ( # ` X ) ) ) )
163 146 162 breqtrd 
 |-  ( ( ph /\ i e. X ) -> ( ( D ` i ) - ( C ` i ) ) < ( E / ( sqrt ` ( # ` X ) ) ) )
164 134 adantr 
 |-  ( ( ph /\ i e. X ) -> ( E / ( sqrt ` ( # ` X ) ) ) e. RR )
165 0red 
 |-  ( ph -> 0 e. RR )
166 98 rpred 
 |-  ( ph -> ( sqrt ` ( # ` X ) ) e. RR )
167 7 rpgt0d 
 |-  ( ph -> 0 < E )
168 98 rpgt0d 
 |-  ( ph -> 0 < ( sqrt ` ( # ` X ) ) )
169 81 166 167 168 divgt0d 
 |-  ( ph -> 0 < ( E / ( sqrt ` ( # ` X ) ) ) )
170 165 134 169 ltled 
 |-  ( ph -> 0 <_ ( E / ( sqrt ` ( # ` X ) ) ) )
171 170 adantr 
 |-  ( ( ph /\ i e. X ) -> 0 <_ ( E / ( sqrt ` ( # ` X ) ) ) )
172 lt2sq 
 |-  ( ( ( ( ( D ` i ) - ( C ` i ) ) e. RR /\ 0 <_ ( ( D ` i ) - ( C ` i ) ) ) /\ ( ( E / ( sqrt ` ( # ` X ) ) ) e. RR /\ 0 <_ ( E / ( sqrt ` ( # ` X ) ) ) ) ) -> ( ( ( D ` i ) - ( C ` i ) ) < ( E / ( sqrt ` ( # ` X ) ) ) <-> ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) < ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) ) )
173 74 120 164 171 172 syl22anc 
 |-  ( ( ph /\ i e. X ) -> ( ( ( D ` i ) - ( C ` i ) ) < ( E / ( sqrt ` ( # ` X ) ) ) <-> ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) < ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) ) )
174 163 173 mpbid 
 |-  ( ( ph /\ i e. X ) -> ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) < ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) )
175 2 3 75 136 174 fsumlt 
 |-  ( ph -> sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) < sum_ i e. X ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) )
176 2 136 fsumrecl 
 |-  ( ph -> sum_ i e. X ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) e. RR )
177 164 sqge0d 
 |-  ( ( ph /\ i e. X ) -> 0 <_ ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) )
178 2 136 177 fsumge0 
 |-  ( ph -> 0 <_ sum_ i e. X ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) )
179 76 78 176 178 sqrtltd 
 |-  ( ph -> ( sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) < sum_ i e. X ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) <-> ( sqrt ` sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) ) < ( sqrt ` sum_ i e. X ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) ) ) )
180 175 179 mpbid 
 |-  ( ph -> ( sqrt ` sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) ) < ( sqrt ` sum_ i e. X ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) ) )
181 135 recnd 
 |-  ( ph -> ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) e. CC )
182 fsumconst 
 |-  ( ( X e. Fin /\ ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) e. CC ) -> sum_ i e. X ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) = ( ( # ` X ) x. ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) ) )
183 2 181 182 syl2anc 
 |-  ( ph -> sum_ i e. X ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) = ( ( # ` X ) x. ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) ) )
184 sqdiv 
 |-  ( ( E e. CC /\ ( sqrt ` ( # ` X ) ) e. CC /\ ( sqrt ` ( # ` X ) ) =/= 0 ) -> ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) = ( ( E ^ 2 ) / ( ( sqrt ` ( # ` X ) ) ^ 2 ) ) )
185 150 151 153 184 syl3anc 
 |-  ( ph -> ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) = ( ( E ^ 2 ) / ( ( sqrt ` ( # ` X ) ) ^ 2 ) ) )
186 95 recnd 
 |-  ( ph -> ( # ` X ) e. CC )
187 sqrtth 
 |-  ( ( # ` X ) e. CC -> ( ( sqrt ` ( # ` X ) ) ^ 2 ) = ( # ` X ) )
188 186 187 syl 
 |-  ( ph -> ( ( sqrt ` ( # ` X ) ) ^ 2 ) = ( # ` X ) )
189 188 oveq2d 
 |-  ( ph -> ( ( E ^ 2 ) / ( ( sqrt ` ( # ` X ) ) ^ 2 ) ) = ( ( E ^ 2 ) / ( # ` X ) ) )
190 185 189 eqtrd 
 |-  ( ph -> ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) = ( ( E ^ 2 ) / ( # ` X ) ) )
191 190 oveq2d 
 |-  ( ph -> ( ( # ` X ) x. ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) ) = ( ( # ` X ) x. ( ( E ^ 2 ) / ( # ` X ) ) ) )
192 150 sqcld 
 |-  ( ph -> ( E ^ 2 ) e. CC )
193 165 96 gtned 
 |-  ( ph -> ( # ` X ) =/= 0 )
194 192 186 193 divcan2d 
 |-  ( ph -> ( ( # ` X ) x. ( ( E ^ 2 ) / ( # ` X ) ) ) = ( E ^ 2 ) )
195 183 191 194 3eqtrd 
 |-  ( ph -> sum_ i e. X ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) = ( E ^ 2 ) )
196 195 fveq2d 
 |-  ( ph -> ( sqrt ` sum_ i e. X ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) ) = ( sqrt ` ( E ^ 2 ) ) )
197 165 81 167 ltled 
 |-  ( ph -> 0 <_ E )
198 sqrtsq 
 |-  ( ( E e. RR /\ 0 <_ E ) -> ( sqrt ` ( E ^ 2 ) ) = E )
199 81 197 198 syl2anc 
 |-  ( ph -> ( sqrt ` ( E ^ 2 ) ) = E )
200 eqidd 
 |-  ( ph -> E = E )
201 196 199 200 3eqtrd 
 |-  ( ph -> ( sqrt ` sum_ i e. X ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) ) = E )
202 180 201 breqtrd 
 |-  ( ph -> ( sqrt ` sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) ) < E )
203 202 adantr 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> ( sqrt ` sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) ) < E )
204 73 80 82 133 203 lttrd 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> ( Y ( dist ` ( RR^ ` X ) ) f ) < E )
205 eqid 
 |-  ( dist ` ( RR^ ` X ) ) = ( dist ` ( RR^ ` X ) )
206 205 rrxmetfi 
 |-  ( X e. Fin -> ( dist ` ( RR^ ` X ) ) e. ( Met ` ( RR ^m X ) ) )
207 metxmet 
 |-  ( ( dist ` ( RR^ ` X ) ) e. ( Met ` ( RR ^m X ) ) -> ( dist ` ( RR^ ` X ) ) e. ( *Met ` ( RR ^m X ) ) )
208 2 206 207 3syl 
 |-  ( ph -> ( dist ` ( RR^ ` X ) ) e. ( *Met ` ( RR ^m X ) ) )
209 208 adantr 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> ( dist ` ( RR^ ` X ) ) e. ( *Met ` ( RR ^m X ) ) )
210 82 rexrd 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> E e. RR* )
211 31 11 eleqtrdi 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> f e. ( RR ^m X ) )
212 elbl2 
 |-  ( ( ( ( dist ` ( RR^ ` X ) ) e. ( *Met ` ( RR ^m X ) ) /\ E e. RR* ) /\ ( Y e. ( RR ^m X ) /\ f e. ( RR ^m X ) ) ) -> ( f e. ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) <-> ( Y ( dist ` ( RR^ ` X ) ) f ) < E ) )
213 209 210 24 211 212 syl22anc 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> ( f e. ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) <-> ( Y ( dist ` ( RR^ ` X ) ) f ) < E ) )
214 204 213 mpbird 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> f e. ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) )
215 214 ralrimiva 
 |-  ( ph -> A. f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) f e. ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) )
216 dfss3 
 |-  ( X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) <-> A. f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) f e. ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) )
217 215 216 sylibr 
 |-  ( ph -> X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) )