Metamath Proof Explorer

Theorem hoiqssbllem1

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

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

Proof

Step Hyp Ref Expression
1 hoiqssbllem1.i 
 |-  F/ i ph
2 hoiqssbllem1.x 
 |-  ( ph -> X e. Fin )
3 hoiqssbllem1.n 
 |-  ( ph -> X =/= (/) )
4 hoiqssbllem1.y 
 |-  ( ph -> Y e. ( RR ^m X ) )
5 hoiqssbllem1.c 
 |-  ( ph -> C : X --> RR )
6 hoiqssbllem1.d 
 |-  ( ph -> D : X --> RR )
7 hoiqssbllem1.e 
 |-  ( ph -> E e. RR+ )
8 hoiqssbllem1.l 
 |-  ( ( ph /\ i e. X ) -> ( C ` i ) e. ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) )
9 hoiqssbllem1.r 
 |-  ( ( ph /\ i e. X ) -> ( D ` i ) e. ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) )
10 4 elexd 
 |-  ( ph -> Y e. _V )
11 elmapfn 
 |-  ( Y e. ( RR ^m X ) -> Y Fn X )
12 4 11 syl 
 |-  ( ph -> Y Fn X )
13 5 ffvelrnda 
 |-  ( ( ph /\ i e. X ) -> ( C ` i ) e. RR )
14 13 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( C ` i ) e. RR* )
15 6 ffvelrnda 
 |-  ( ( ph /\ i e. X ) -> ( D ` i ) e. RR )
16 15 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( D ` i ) e. RR* )
17 elmapi 
 |-  ( Y e. ( RR ^m X ) -> Y : X --> RR )
18 4 17 syl 
 |-  ( ph -> Y : X --> RR )
19 18 ffvelrnda 
 |-  ( ( ph /\ i e. X ) -> ( Y ` i ) e. RR )
20 19 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( Y ` i ) e. RR* )
21 2rp 
 |-  2 e. RR+
22 21 a1i 
 |-  ( ph -> 2 e. RR+ )
23 hashnncl 
 |-  ( X e. Fin -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
24 2 23 syl 
 |-  ( ph -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
25 3 24 mpbird 
 |-  ( ph -> ( # ` X ) e. NN )
26 25 nnred 
 |-  ( ph -> ( # ` X ) e. RR )
27 25 nngt0d 
 |-  ( ph -> 0 < ( # ` X ) )
28 26 27 elrpd 
 |-  ( ph -> ( # ` X ) e. RR+ )
29 28 rpsqrtcld 
 |-  ( ph -> ( sqrt ` ( # ` X ) ) e. RR+ )
30 22 29 rpmulcld 
 |-  ( ph -> ( 2 x. ( sqrt ` ( # ` X ) ) ) e. RR+ )
31 7 30 rpdivcld 
 |-  ( ph -> ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) e. RR+ )
32 31 rpred 
 |-  ( ph -> ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) e. RR )
33 32 adantr 
 |-  ( ( ph /\ i e. X ) -> ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) e. RR )
34 19 33 resubcld 
 |-  ( ( ph /\ i e. X ) -> ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR )
35 34 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR* )
36 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 ) )
37 35 20 8 36 syl3anc 
 |-  ( ( ph /\ i e. X ) -> ( C ` i ) < ( Y ` i ) )
38 13 19 37 ltled 
 |-  ( ( ph /\ i e. X ) -> ( C ` i ) <_ ( Y ` i ) )
39 19 33 readdcld 
 |-  ( ( ph /\ i e. X ) -> ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR )
40 39 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR* )
41 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 ) )
42 20 40 9 41 syl3anc 
 |-  ( ( ph /\ i e. X ) -> ( Y ` i ) < ( D ` i ) )
43 14 16 20 38 42 elicod 
 |-  ( ( ph /\ i e. X ) -> ( Y ` i ) e. ( ( C ` i ) [,) ( D ` i ) ) )
44 43 ex 
 |-  ( ph -> ( i e. X -> ( Y ` i ) e. ( ( C ` i ) [,) ( D ` i ) ) ) )
45 1 44 ralrimi 
 |-  ( ph -> A. i e. X ( Y ` i ) e. ( ( C ` i ) [,) ( D ` i ) ) )
46 10 12 45 3jca 
 |-  ( ph -> ( Y e. _V /\ Y Fn X /\ A. i e. X ( Y ` i ) e. ( ( C ` i ) [,) ( D ` i ) ) ) )
47 elixp2 
 |-  ( Y e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) <-> ( Y e. _V /\ Y Fn X /\ A. i e. X ( Y ` i ) e. ( ( C ` i ) [,) ( D ` i ) ) ) )
48 46 47 sylibr 
 |-  ( ph -> Y e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) )