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 ffvelcdmda 
 |-  ( ( ph /\ i e. X ) -> ( C ` i ) e. RR )
26 6 ffvelcdmda 
 |-  ( ( 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 ffvelcdmda 
 |-  ( ( 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 bilani 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) )
61 2 adantr 
 |-  ( ( ph /\ f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) ) -> X e. Fin )
62 simpll 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) ) /\ i e. X ) -> ph )
63 59 biimpri 
 |-  ( f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) -> f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) )
64 63 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 ) ) )
65 simpr 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) ) /\ i e. X ) -> i e. X )
66 62 64 65 53 syl21anc 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) ) /\ i e. X ) -> ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) e. RR )
67 50 sqge0d 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> 0 <_ ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) )
68 62 64 65 67 syl21anc 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) ) /\ i e. X ) -> 0 <_ ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) )
69 61 66 68 fsumge0 
 |-  ( ( ph /\ f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) ) -> 0 <_ sum_ i e. X ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) )
70 38 60 69 syl2anc 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> 0 <_ sum_ i e. X ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) )
71 54 70 resqrtcld 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> ( sqrt ` sum_ i e. X ( ( ( Y ` i ) - ( f ` i ) ) ^ 2 ) ) e. RR )
72 33 71 eqeltrd 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> ( Y ( dist ` ( RR^ ` X ) ) f ) e. RR )
73 26 25 resubcld 
 |-  ( ( ph /\ i e. X ) -> ( ( D ` i ) - ( C ` i ) ) e. RR )
74 73 resqcld 
 |-  ( ( ph /\ i e. X ) -> ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) e. RR )
75 2 74 fsumrecl 
 |-  ( ph -> sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) e. RR )
76 73 sqge0d 
 |-  ( ( ph /\ i e. X ) -> 0 <_ ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) )
77 2 74 76 fsumge0 
 |-  ( ph -> 0 <_ sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) )
78 75 77 resqrtcld 
 |-  ( ph -> ( sqrt ` sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) ) e. RR )
79 78 adantr 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> ( sqrt ` sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) ) e. RR )
80 7 rpred 
 |-  ( ph -> E e. RR )
81 80 adantr 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> E e. RR )
82 3 adantr 
 |-  ( ( ph /\ f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) ) -> X =/= (/) )
83 74 adantlr 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( C ` j ) [,) ( D ` j ) ) ) /\ i e. X ) -> ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) e. RR )
84 38 26 sylan 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> ( D ` i ) e. RR )
85 38 25 sylan 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> ( C ` i ) e. RR )
86 84 85 resubcld 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> ( ( D ` i ) - ( C ` i ) ) e. RR )
87 25 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( C ` i ) e. RR* )
88 42 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( Y ` i ) e. RR* )
89 2rp 
 |-  2 e. RR+
90 89 a1i 
 |-  ( ph -> 2 e. RR+ )
91 hashnncl 
 |-  ( X e. Fin -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
92 2 91 syl 
 |-  ( ph -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
93 3 92 mpbird 
 |-  ( ph -> ( # ` X ) e. NN )
94 93 nnred 
 |-  ( ph -> ( # ` X ) e. RR )
95 93 nngt0d 
 |-  ( ph -> 0 < ( # ` X ) )
96 94 95 elrpd 
 |-  ( ph -> ( # ` X ) e. RR+ )
97 96 rpsqrtcld 
 |-  ( ph -> ( sqrt ` ( # ` X ) ) e. RR+ )
98 90 97 rpmulcld 
 |-  ( ph -> ( 2 x. ( sqrt ` ( # ` X ) ) ) e. RR+ )
99 7 98 rpdivcld 
 |-  ( ph -> ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) e. RR+ )
100 99 rpred 
 |-  ( ph -> ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) e. RR )
101 100 adantr 
 |-  ( ( ph /\ i e. X ) -> ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) e. RR )
102 42 101 resubcld 
 |-  ( ( ph /\ i e. X ) -> ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR )
103 102 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR* )
104 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 ) )
105 103 88 8 104 syl3anc 
 |-  ( ( ph /\ i e. X ) -> ( C ` i ) < ( Y ` i ) )
106 25 42 105 ltled 
 |-  ( ( ph /\ i e. X ) -> ( C ` i ) <_ ( Y ` i ) )
107 42 101 readdcld 
 |-  ( ( ph /\ i e. X ) -> ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR )
108 107 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR* )
109 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 ) )
110 88 108 9 109 syl3anc 
 |-  ( ( ph /\ i e. X ) -> ( Y ` i ) < ( D ` i ) )
111 87 27 88 106 110 elicod 
 |-  ( ( ph /\ i e. X ) -> ( Y ` i ) e. ( ( C ` i ) [,) ( D ` i ) ) )
112 38 111 sylan 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> ( Y ` i ) e. ( ( C ` i ) [,) ( D ` i ) ) )
113 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 ) ) )
114 85 84 112 48 113 syl22anc 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> ( abs ` ( ( Y ` i ) - ( f ` i ) ) ) < ( ( D ` i ) - ( C ` i ) ) )
115 0red 
 |-  ( ( ph /\ i e. X ) -> 0 e. RR )
116 25 42 26 106 110 lelttrd 
 |-  ( ( ph /\ i e. X ) -> ( C ` i ) < ( D ` i ) )
117 25 26 posdifd 
 |-  ( ( ph /\ i e. X ) -> ( ( C ` i ) < ( D ` i ) <-> 0 < ( ( D ` i ) - ( C ` i ) ) ) )
118 116 117 mpbid 
 |-  ( ( ph /\ i e. X ) -> 0 < ( ( D ` i ) - ( C ` i ) ) )
119 115 73 118 ltled 
 |-  ( ( ph /\ i e. X ) -> 0 <_ ( ( D ` i ) - ( C ` i ) ) )
120 73 119 absidd 
 |-  ( ( ph /\ i e. X ) -> ( abs ` ( ( D ` i ) - ( C ` i ) ) ) = ( ( D ` i ) - ( C ` i ) ) )
121 120 eqcomd 
 |-  ( ( ph /\ i e. X ) -> ( ( D ` i ) - ( C ` i ) ) = ( abs ` ( ( D ` i ) - ( C ` i ) ) ) )
122 121 adantlr 
 |-  ( ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) /\ i e. X ) -> ( ( D ` i ) - ( C ` i ) ) = ( abs ` ( ( D ` i ) - ( C ` i ) ) ) )
123 114 122 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 ) ) ) )
124 50 86 123 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 ) )
125 62 64 65 124 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 ) )
126 61 82 66 83 125 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 ) )
127 38 60 126 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 ) )
128 38 75 syl 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) e. RR )
129 38 77 syl 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> 0 <_ sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) )
130 54 70 128 129 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 ) ) ) )
131 127 130 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 ) ) )
132 33 131 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 ) ) )
133 80 97 rerpdivcld 
 |-  ( ph -> ( E / ( sqrt ` ( # ` X ) ) ) e. RR )
134 133 resqcld 
 |-  ( ph -> ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) e. RR )
135 134 adantr 
 |-  ( ( ph /\ i e. X ) -> ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) e. RR )
136 26 25 jca 
 |-  ( ( ph /\ i e. X ) -> ( ( D ` i ) e. RR /\ ( C ` i ) e. RR ) )
137 107 102 jca 
 |-  ( ( ph /\ i e. X ) -> ( ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR /\ ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR ) )
138 136 137 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 ) ) )
139 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 ) ) ) ) ) )
140 88 108 9 139 syl3anc 
 |-  ( ( ph /\ i e. X ) -> ( D ` i ) < ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) )
141 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 ) )
142 103 88 8 141 syl3anc 
 |-  ( ( ph /\ i e. X ) -> ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) < ( C ` i ) )
143 140 142 jca 
 |-  ( ( ph /\ i e. X ) -> ( ( D ` i ) < ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) /\ ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) < ( C ` i ) ) )
144 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 ) ) ) ) ) ) ) )
145 138 143 144 sylc 
 |-  ( ( ph /\ i e. X ) -> ( ( D ` i ) - ( C ` i ) ) < ( ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) - ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) )
146 42 recnd 
 |-  ( ( ph /\ i e. X ) -> ( Y ` i ) e. CC )
147 101 recnd 
 |-  ( ( ph /\ i e. X ) -> ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) e. CC )
148 146 147 147 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 ) ) ) ) ) )
149 80 recnd 
 |-  ( ph -> E e. CC )
150 97 rpcnd 
 |-  ( ph -> ( sqrt ` ( # ` X ) ) e. CC )
151 2cnd 
 |-  ( ph -> 2 e. CC )
152 97 rpne0d 
 |-  ( ph -> ( sqrt ` ( # ` X ) ) =/= 0 )
153 90 rpne0d 
 |-  ( ph -> 2 =/= 0 )
154 149 150 151 152 153 divdiv3d 
 |-  ( ph -> ( ( E / ( sqrt ` ( # ` X ) ) ) / 2 ) = ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) )
155 154 eqcomd 
 |-  ( ph -> ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) = ( ( E / ( sqrt ` ( # ` X ) ) ) / 2 ) )
156 155 155 oveq12d 
 |-  ( ph -> ( ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) = ( ( ( E / ( sqrt ` ( # ` X ) ) ) / 2 ) + ( ( E / ( sqrt ` ( # ` X ) ) ) / 2 ) ) )
157 149 150 152 divcld 
 |-  ( ph -> ( E / ( sqrt ` ( # ` X ) ) ) e. CC )
158 157 2halvesd 
 |-  ( ph -> ( ( ( E / ( sqrt ` ( # ` X ) ) ) / 2 ) + ( ( E / ( sqrt ` ( # ` X ) ) ) / 2 ) ) = ( E / ( sqrt ` ( # ` X ) ) ) )
159 156 158 eqtrd 
 |-  ( ph -> ( ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) = ( E / ( sqrt ` ( # ` X ) ) ) )
160 159 adantr 
 |-  ( ( ph /\ i e. X ) -> ( ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) = ( E / ( sqrt ` ( # ` X ) ) ) )
161 148 160 eqtrd 
 |-  ( ( ph /\ i e. X ) -> ( ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) - ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) = ( E / ( sqrt ` ( # ` X ) ) ) )
162 145 161 breqtrd 
 |-  ( ( ph /\ i e. X ) -> ( ( D ` i ) - ( C ` i ) ) < ( E / ( sqrt ` ( # ` X ) ) ) )
163 133 adantr 
 |-  ( ( ph /\ i e. X ) -> ( E / ( sqrt ` ( # ` X ) ) ) e. RR )
164 0red 
 |-  ( ph -> 0 e. RR )
165 97 rpred 
 |-  ( ph -> ( sqrt ` ( # ` X ) ) e. RR )
166 7 rpgt0d 
 |-  ( ph -> 0 < E )
167 97 rpgt0d 
 |-  ( ph -> 0 < ( sqrt ` ( # ` X ) ) )
168 80 165 166 167 divgt0d 
 |-  ( ph -> 0 < ( E / ( sqrt ` ( # ` X ) ) ) )
169 164 133 168 ltled 
 |-  ( ph -> 0 <_ ( E / ( sqrt ` ( # ` X ) ) ) )
170 169 adantr 
 |-  ( ( ph /\ i e. X ) -> 0 <_ ( E / ( sqrt ` ( # ` X ) ) ) )
171 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 ) ) )
172 73 119 163 170 171 syl22anc 
 |-  ( ( ph /\ i e. X ) -> ( ( ( D ` i ) - ( C ` i ) ) < ( E / ( sqrt ` ( # ` X ) ) ) <-> ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) < ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) ) )
173 162 172 mpbid 
 |-  ( ( ph /\ i e. X ) -> ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) < ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) )
174 2 3 74 135 173 fsumlt 
 |-  ( ph -> sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) < sum_ i e. X ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) )
175 2 135 fsumrecl 
 |-  ( ph -> sum_ i e. X ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) e. RR )
176 163 sqge0d 
 |-  ( ( ph /\ i e. X ) -> 0 <_ ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) )
177 2 135 176 fsumge0 
 |-  ( ph -> 0 <_ sum_ i e. X ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) )
178 75 77 175 177 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 ) ) ) )
179 174 178 mpbid 
 |-  ( ph -> ( sqrt ` sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) ) < ( sqrt ` sum_ i e. X ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) ) )
180 134 recnd 
 |-  ( ph -> ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) e. CC )
181 fsumconst 
 |-  ( ( X e. Fin /\ ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) e. CC ) -> sum_ i e. X ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) = ( ( # ` X ) x. ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) ) )
182 2 180 181 syl2anc 
 |-  ( ph -> sum_ i e. X ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) = ( ( # ` X ) x. ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) ) )
183 sqdiv 
 |-  ( ( E e. CC /\ ( sqrt ` ( # ` X ) ) e. CC /\ ( sqrt ` ( # ` X ) ) =/= 0 ) -> ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) = ( ( E ^ 2 ) / ( ( sqrt ` ( # ` X ) ) ^ 2 ) ) )
184 149 150 152 183 syl3anc 
 |-  ( ph -> ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) = ( ( E ^ 2 ) / ( ( sqrt ` ( # ` X ) ) ^ 2 ) ) )
185 94 recnd 
 |-  ( ph -> ( # ` X ) e. CC )
186 sqrtth 
 |-  ( ( # ` X ) e. CC -> ( ( sqrt ` ( # ` X ) ) ^ 2 ) = ( # ` X ) )
187 185 186 syl 
 |-  ( ph -> ( ( sqrt ` ( # ` X ) ) ^ 2 ) = ( # ` X ) )
188 187 oveq2d 
 |-  ( ph -> ( ( E ^ 2 ) / ( ( sqrt ` ( # ` X ) ) ^ 2 ) ) = ( ( E ^ 2 ) / ( # ` X ) ) )
189 184 188 eqtrd 
 |-  ( ph -> ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) = ( ( E ^ 2 ) / ( # ` X ) ) )
190 189 oveq2d 
 |-  ( ph -> ( ( # ` X ) x. ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) ) = ( ( # ` X ) x. ( ( E ^ 2 ) / ( # ` X ) ) ) )
191 149 sqcld 
 |-  ( ph -> ( E ^ 2 ) e. CC )
192 164 95 gtned 
 |-  ( ph -> ( # ` X ) =/= 0 )
193 191 185 192 divcan2d 
 |-  ( ph -> ( ( # ` X ) x. ( ( E ^ 2 ) / ( # ` X ) ) ) = ( E ^ 2 ) )
194 182 190 193 3eqtrd 
 |-  ( ph -> sum_ i e. X ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) = ( E ^ 2 ) )
195 194 fveq2d 
 |-  ( ph -> ( sqrt ` sum_ i e. X ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) ) = ( sqrt ` ( E ^ 2 ) ) )
196 164 80 166 ltled 
 |-  ( ph -> 0 <_ E )
197 sqrtsq 
 |-  ( ( E e. RR /\ 0 <_ E ) -> ( sqrt ` ( E ^ 2 ) ) = E )
198 80 196 197 syl2anc 
 |-  ( ph -> ( sqrt ` ( E ^ 2 ) ) = E )
199 eqidd 
 |-  ( ph -> E = E )
200 195 198 199 3eqtrd 
 |-  ( ph -> ( sqrt ` sum_ i e. X ( ( E / ( sqrt ` ( # ` X ) ) ) ^ 2 ) ) = E )
201 179 200 breqtrd 
 |-  ( ph -> ( sqrt ` sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) ) < E )
202 201 adantr 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> ( sqrt ` sum_ i e. X ( ( ( D ` i ) - ( C ` i ) ) ^ 2 ) ) < E )
203 72 79 81 132 202 lttrd 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> ( Y ( dist ` ( RR^ ` X ) ) f ) < E )
204 eqid 
 |-  ( dist ` ( RR^ ` X ) ) = ( dist ` ( RR^ ` X ) )
205 204 rrxmetfi 
 |-  ( X e. Fin -> ( dist ` ( RR^ ` X ) ) e. ( Met ` ( RR ^m X ) ) )
206 metxmet 
 |-  ( ( dist ` ( RR^ ` X ) ) e. ( Met ` ( RR ^m X ) ) -> ( dist ` ( RR^ ` X ) ) e. ( *Met ` ( RR ^m X ) ) )
207 2 205 206 3syl 
 |-  ( ph -> ( dist ` ( RR^ ` X ) ) e. ( *Met ` ( RR ^m X ) ) )
208 207 adantr 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> ( dist ` ( RR^ ` X ) ) e. ( *Met ` ( RR ^m X ) ) )
209 81 rexrd 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> E e. RR* )
210 31 11 eleqtrdi 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> f e. ( RR ^m X ) )
211 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 ) )
212 208 209 24 210 211 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 ) )
213 203 212 mpbird 
 |-  ( ( ph /\ f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) ) -> f e. ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) )
214 213 ralrimiva 
 |-  ( ph -> A. f e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) f e. ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) )
215 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 ) )
216 214 215 sylibr 
 |-  ( ph -> X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) )