Metamath Proof Explorer

Theorem hoiqssbllem3

Description: A n-dimensional ball contains a nonempty half-open interval with vertices with rational components. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hoiqssbllem3.x 
|- ( ph -> X e. Fin )
hoiqssbllem3.n 
|- ( ph -> X =/= (/) )
hoiqssbllem3.y 
|- ( ph -> Y e. ( RR ^m X ) )
hoiqssbllem3.e 
|- ( ph -> E e. RR+ )
Assertion hoiqssbllem3 
|- ( ph -> E. c e. ( QQ ^m X ) E. d e. ( QQ ^m X ) ( Y e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) ) )

Proof

Step Hyp Ref Expression
1 hoiqssbllem3.x 
 |-  ( ph -> X e. Fin )
2 hoiqssbllem3.n 
 |-  ( ph -> X =/= (/) )
3 hoiqssbllem3.y 
 |-  ( ph -> Y e. ( RR ^m X ) )
4 hoiqssbllem3.e 
 |-  ( ph -> E e. RR+ )
5 qex 
 |-  QQ e. _V
6 5 inex1 
 |-  ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) e. _V
7 6 a1i 
 |-  ( ( ph /\ i e. X ) -> ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) e. _V )
8 elmapi 
 |-  ( Y e. ( RR ^m X ) -> Y : X --> RR )
9 3 8 syl 
 |-  ( ph -> Y : X --> RR )
10 9 ffvelcdmda 
 |-  ( ( ph /\ i e. X ) -> ( Y ` i ) e. RR )
11 2rp 
 |-  2 e. RR+
12 11 a1i 
 |-  ( ph -> 2 e. RR+ )
13 hashnncl 
 |-  ( X e. Fin -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
14 1 13 syl 
 |-  ( ph -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
15 2 14 mpbird 
 |-  ( ph -> ( # ` X ) e. NN )
16 nnrp 
 |-  ( ( # ` X ) e. NN -> ( # ` X ) e. RR+ )
17 15 16 syl 
 |-  ( ph -> ( # ` X ) e. RR+ )
18 17 rpsqrtcld 
 |-  ( ph -> ( sqrt ` ( # ` X ) ) e. RR+ )
19 12 18 rpmulcld 
 |-  ( ph -> ( 2 x. ( sqrt ` ( # ` X ) ) ) e. RR+ )
20 4 19 rpdivcld 
 |-  ( ph -> ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) e. RR+ )
21 20 adantr 
 |-  ( ( ph /\ i e. X ) -> ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) e. RR+ )
22 10 21 ltsubrpd 
 |-  ( ( ph /\ i e. X ) -> ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) < ( Y ` i ) )
23 21 rpred 
 |-  ( ( ph /\ i e. X ) -> ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) e. RR )
24 10 23 resubcld 
 |-  ( ( ph /\ i e. X ) -> ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR )
25 24 10 ltnled 
 |-  ( ( ph /\ i e. X ) -> ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) < ( Y ` i ) <-> -. ( Y ` i ) <_ ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) )
26 22 25 mpbid 
 |-  ( ( ph /\ i e. X ) -> -. ( Y ` i ) <_ ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) )
27 24 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR* )
28 10 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( Y ` i ) e. RR* )
29 27 28 qinioo 
 |-  ( ( ph /\ i e. X ) -> ( ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) = (/) <-> ( Y ` i ) <_ ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) )
30 26 29 mtbird 
 |-  ( ( ph /\ i e. X ) -> -. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) = (/) )
31 30 neqned 
 |-  ( ( ph /\ i e. X ) -> ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) =/= (/) )
32 1 7 31 choicefi 
 |-  ( ph -> E. c ( c Fn X /\ A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) ) )
33 simpl 
 |-  ( ( c Fn X /\ A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) ) -> c Fn X )
34 nfra1 
 |-  F/ i A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) )
35 rspa 
 |-  ( ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ i e. X ) -> ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) )
36 elinel1 
 |-  ( ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) -> ( c ` i ) e. QQ )
37 35 36 syl 
 |-  ( ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ i e. X ) -> ( c ` i ) e. QQ )
38 37 ex 
 |-  ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) -> ( i e. X -> ( c ` i ) e. QQ ) )
39 34 38 ralrimi 
 |-  ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) -> A. i e. X ( c ` i ) e. QQ )
40 39 adantl 
 |-  ( ( c Fn X /\ A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) ) -> A. i e. X ( c ` i ) e. QQ )
41 33 40 jca 
 |-  ( ( c Fn X /\ A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) ) -> ( c Fn X /\ A. i e. X ( c ` i ) e. QQ ) )
42 41 adantl 
 |-  ( ( ph /\ ( c Fn X /\ A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) ) ) -> ( c Fn X /\ A. i e. X ( c ` i ) e. QQ ) )
43 ffnfv 
 |-  ( c : X --> QQ <-> ( c Fn X /\ A. i e. X ( c ` i ) e. QQ ) )
44 42 43 sylibr 
 |-  ( ( ph /\ ( c Fn X /\ A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) ) ) -> c : X --> QQ )
45 5 a1i 
 |-  ( ph -> QQ e. _V )
46 elmapg 
 |-  ( ( QQ e. _V /\ X e. Fin ) -> ( c e. ( QQ ^m X ) <-> c : X --> QQ ) )
47 45 1 46 syl2anc 
 |-  ( ph -> ( c e. ( QQ ^m X ) <-> c : X --> QQ ) )
48 47 adantr 
 |-  ( ( ph /\ ( c Fn X /\ A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) ) ) -> ( c e. ( QQ ^m X ) <-> c : X --> QQ ) )
49 44 48 mpbird 
 |-  ( ( ph /\ ( c Fn X /\ A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) ) ) -> c e. ( QQ ^m X ) )
50 simprr 
 |-  ( ( ph /\ ( c Fn X /\ A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) ) ) -> A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) )
51 49 50 jca 
 |-  ( ( ph /\ ( c Fn X /\ A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) ) ) -> ( c e. ( QQ ^m X ) /\ A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) ) )
52 51 ex 
 |-  ( ph -> ( ( c Fn X /\ A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) ) -> ( c e. ( QQ ^m X ) /\ A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) ) ) )
53 52 eximdv 
 |-  ( ph -> ( E. c ( c Fn X /\ A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) ) -> E. c ( c e. ( QQ ^m X ) /\ A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) ) ) )
54 32 53 mpd 
 |-  ( ph -> E. c ( c e. ( QQ ^m X ) /\ A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) ) )
55 df-rex 
 |-  ( E. c e. ( QQ ^m X ) A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) <-> E. c ( c e. ( QQ ^m X ) /\ A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) ) )
56 54 55 sylibr 
 |-  ( ph -> E. c e. ( QQ ^m X ) A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) )
57 5 inex1 
 |-  ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) e. _V
58 57 a1i 
 |-  ( ( ph /\ i e. X ) -> ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) e. _V )
59 10 21 ltaddrpd 
 |-  ( ( ph /\ i e. X ) -> ( Y ` i ) < ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) )
60 10 23 readdcld 
 |-  ( ( ph /\ i e. X ) -> ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR )
61 10 60 ltnled 
 |-  ( ( ph /\ i e. X ) -> ( ( Y ` i ) < ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) <-> -. ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) <_ ( Y ` i ) ) )
62 59 61 mpbid 
 |-  ( ( ph /\ i e. X ) -> -. ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) <_ ( Y ` i ) )
63 60 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) e. RR* )
64 28 63 qinioo 
 |-  ( ( ph /\ i e. X ) -> ( ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) = (/) <-> ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) <_ ( Y ` i ) ) )
65 62 64 mtbird 
 |-  ( ( ph /\ i e. X ) -> -. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) = (/) )
66 65 neqned 
 |-  ( ( ph /\ i e. X ) -> ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) =/= (/) )
67 1 58 66 choicefi 
 |-  ( ph -> E. d ( d Fn X /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) )
68 simpl 
 |-  ( ( d Fn X /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) -> d Fn X )
69 nfra1 
 |-  F/ i A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) )
70 rspa 
 |-  ( ( A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) /\ i e. X ) -> ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) )
71 elinel1 
 |-  ( ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) -> ( d ` i ) e. QQ )
72 70 71 syl 
 |-  ( ( A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) /\ i e. X ) -> ( d ` i ) e. QQ )
73 72 ex 
 |-  ( A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) -> ( i e. X -> ( d ` i ) e. QQ ) )
74 69 73 ralrimi 
 |-  ( A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) -> A. i e. X ( d ` i ) e. QQ )
75 74 adantl 
 |-  ( ( d Fn X /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) -> A. i e. X ( d ` i ) e. QQ )
76 68 75 jca 
 |-  ( ( d Fn X /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) -> ( d Fn X /\ A. i e. X ( d ` i ) e. QQ ) )
77 76 adantl 
 |-  ( ( ph /\ ( d Fn X /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> ( d Fn X /\ A. i e. X ( d ` i ) e. QQ ) )
78 ffnfv 
 |-  ( d : X --> QQ <-> ( d Fn X /\ A. i e. X ( d ` i ) e. QQ ) )
79 77 78 sylibr 
 |-  ( ( ph /\ ( d Fn X /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> d : X --> QQ )
80 elmapg 
 |-  ( ( QQ e. _V /\ X e. Fin ) -> ( d e. ( QQ ^m X ) <-> d : X --> QQ ) )
81 45 1 80 syl2anc 
 |-  ( ph -> ( d e. ( QQ ^m X ) <-> d : X --> QQ ) )
82 81 adantr 
 |-  ( ( ph /\ ( d Fn X /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> ( d e. ( QQ ^m X ) <-> d : X --> QQ ) )
83 79 82 mpbird 
 |-  ( ( ph /\ ( d Fn X /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> d e. ( QQ ^m X ) )
84 simprr 
 |-  ( ( ph /\ ( d Fn X /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) )
85 83 84 jca 
 |-  ( ( ph /\ ( d Fn X /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> ( d e. ( QQ ^m X ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) )
86 85 ex 
 |-  ( ph -> ( ( d Fn X /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) -> ( d e. ( QQ ^m X ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) )
87 86 eximdv 
 |-  ( ph -> ( E. d ( d Fn X /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) -> E. d ( d e. ( QQ ^m X ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) )
88 67 87 mpd 
 |-  ( ph -> E. d ( d e. ( QQ ^m X ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) )
89 df-rex 
 |-  ( E. d e. ( QQ ^m X ) A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) <-> E. d ( d e. ( QQ ^m X ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) )
90 88 89 sylibr 
 |-  ( ph -> E. d e. ( QQ ^m X ) A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) )
91 56 90 jca 
 |-  ( ph -> ( E. c e. ( QQ ^m X ) A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ E. d e. ( QQ ^m X ) A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) )
92 reeanv 
 |-  ( E. c e. ( QQ ^m X ) E. d e. ( QQ ^m X ) ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) <-> ( E. c e. ( QQ ^m X ) A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ E. d e. ( QQ ^m X ) A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) )
93 91 92 sylibr 
 |-  ( ph -> E. c e. ( QQ ^m X ) E. d e. ( QQ ^m X ) ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) )
94 nfv 
 |-  F/ i ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) )
95 34 69 nfan 
 |-  F/ i ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) )
96 94 95 nfan 
 |-  F/ i ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) )
97 1 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> X e. Fin )
98 2 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> X =/= (/) )
99 3 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> Y e. ( RR ^m X ) )
100 elmapi 
 |-  ( c e. ( QQ ^m X ) -> c : X --> QQ )
101 qssre 
 |-  QQ C_ RR
102 101 a1i 
 |-  ( c e. ( QQ ^m X ) -> QQ C_ RR )
103 100 102 fssd 
 |-  ( c e. ( QQ ^m X ) -> c : X --> RR )
104 103 adantl 
 |-  ( ( ph /\ c e. ( QQ ^m X ) ) -> c : X --> RR )
105 104 ad2antrr 
 |-  ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> c : X --> RR )
106 elmapi 
 |-  ( d e. ( QQ ^m X ) -> d : X --> QQ )
107 101 a1i 
 |-  ( d e. ( QQ ^m X ) -> QQ C_ RR )
108 106 107 fssd 
 |-  ( d e. ( QQ ^m X ) -> d : X --> RR )
109 108 ad2antlr 
 |-  ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> d : X --> RR )
110 4 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> E e. RR+ )
111 35 elin2d 
 |-  ( ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ i e. X ) -> ( c ` i ) e. ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) )
112 111 adantlr 
 |-  ( ( ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) /\ i e. X ) -> ( c ` i ) e. ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) )
113 112 adantll 
 |-  ( ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) /\ i e. X ) -> ( c ` i ) e. ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) )
114 70 elin2d 
 |-  ( ( A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) /\ i e. X ) -> ( d ` i ) e. ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) )
115 114 adantll 
 |-  ( ( ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) /\ i e. X ) -> ( d ` i ) e. ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) )
116 115 adantll 
 |-  ( ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) /\ i e. X ) -> ( d ` i ) e. ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) )
117 96 97 98 99 105 109 110 113 116 hoiqssbllem1 
 |-  ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> Y e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) )
118 simpl 
 |-  ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) )
119 fveq2 
 |-  ( i = k -> ( c ` i ) = ( c ` k ) )
120 fveq2 
 |-  ( i = k -> ( Y ` i ) = ( Y ` k ) )
121 120 oveq1d 
 |-  ( i = k -> ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) = ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) )
122 121 120 oveq12d 
 |-  ( i = k -> ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) = ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) )
123 122 ineq2d 
 |-  ( i = k -> ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) = ( QQ i^i ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) ) )
124 119 123 eleq12d 
 |-  ( i = k -> ( ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) <-> ( c ` k ) e. ( QQ i^i ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) ) ) )
125 124 cbvralvw 
 |-  ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) <-> A. k e. X ( c ` k ) e. ( QQ i^i ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) ) )
126 125 biimpi 
 |-  ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) -> A. k e. X ( c ` k ) e. ( QQ i^i ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) ) )
127 126 adantr 
 |-  ( ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) -> A. k e. X ( c ` k ) e. ( QQ i^i ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) ) )
128 fveq2 
 |-  ( i = k -> ( d ` i ) = ( d ` k ) )
129 120 oveq1d 
 |-  ( i = k -> ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) = ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) )
130 120 129 oveq12d 
 |-  ( i = k -> ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) = ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) )
131 130 ineq2d 
 |-  ( i = k -> ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) = ( QQ i^i ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) )
132 128 131 eleq12d 
 |-  ( i = k -> ( ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) <-> ( d ` k ) e. ( QQ i^i ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) )
133 132 cbvralvw 
 |-  ( A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) <-> A. k e. X ( d ` k ) e. ( QQ i^i ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) )
134 133 biimpi 
 |-  ( A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) -> A. k e. X ( d ` k ) e. ( QQ i^i ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) )
135 134 adantl 
 |-  ( ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) -> A. k e. X ( d ` k ) e. ( QQ i^i ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) )
136 127 135 jca 
 |-  ( ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) -> ( A. k e. X ( c ` k ) e. ( QQ i^i ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) ) /\ A. k e. X ( d ` k ) e. ( QQ i^i ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) )
137 136 adantl 
 |-  ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> ( A. k e. X ( c ` k ) e. ( QQ i^i ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) ) /\ A. k e. X ( d ` k ) e. ( QQ i^i ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) )
138 nfv 
 |-  F/ i ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. k e. X ( c ` k ) e. ( QQ i^i ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) ) /\ A. k e. X ( d ` k ) e. ( QQ i^i ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) )
139 1 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. k e. X ( c ` k ) e. ( QQ i^i ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) ) /\ A. k e. X ( d ` k ) e. ( QQ i^i ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> X e. Fin )
140 2 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. k e. X ( c ` k ) e. ( QQ i^i ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) ) /\ A. k e. X ( d ` k ) e. ( QQ i^i ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> X =/= (/) )
141 3 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. k e. X ( c ` k ) e. ( QQ i^i ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) ) /\ A. k e. X ( d ` k ) e. ( QQ i^i ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> Y e. ( RR ^m X ) )
142 104 ad2antrr 
 |-  ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. k e. X ( c ` k ) e. ( QQ i^i ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) ) /\ A. k e. X ( d ` k ) e. ( QQ i^i ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> c : X --> RR )
143 108 ad2antlr 
 |-  ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. k e. X ( c ` k ) e. ( QQ i^i ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) ) /\ A. k e. X ( d ` k ) e. ( QQ i^i ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> d : X --> RR )
144 4 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. k e. X ( c ` k ) e. ( QQ i^i ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) ) /\ A. k e. X ( d ` k ) e. ( QQ i^i ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> E e. RR+ )
145 125 111 sylanbr 
 |-  ( ( A. k e. X ( c ` k ) e. ( QQ i^i ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) ) /\ i e. X ) -> ( c ` i ) e. ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) )
146 145 adantlr 
 |-  ( ( ( A. k e. X ( c ` k ) e. ( QQ i^i ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) ) /\ A. k e. X ( d ` k ) e. ( QQ i^i ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) /\ i e. X ) -> ( c ` i ) e. ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) )
147 146 adantll 
 |-  ( ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. k e. X ( c ` k ) e. ( QQ i^i ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) ) /\ A. k e. X ( d ` k ) e. ( QQ i^i ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) /\ i e. X ) -> ( c ` i ) e. ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) )
148 133 114 sylanbr 
 |-  ( ( A. k e. X ( d ` k ) e. ( QQ i^i ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) /\ i e. X ) -> ( d ` i ) e. ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) )
149 148 adantll 
 |-  ( ( ( A. k e. X ( c ` k ) e. ( QQ i^i ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) ) /\ A. k e. X ( d ` k ) e. ( QQ i^i ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) /\ i e. X ) -> ( d ` i ) e. ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) )
150 149 adantll 
 |-  ( ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. k e. X ( c ` k ) e. ( QQ i^i ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) ) /\ A. k e. X ( d ` k ) e. ( QQ i^i ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) /\ i e. X ) -> ( d ` i ) e. ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) )
151 138 139 140 141 142 143 144 147 150 hoiqssbllem2 
 |-  ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. k e. X ( c ` k ) e. ( QQ i^i ( ( ( Y ` k ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` k ) ) ) /\ A. k e. X ( d ` k ) e. ( QQ i^i ( ( Y ` k ) (,) ( ( Y ` k ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) )
152 118 137 151 syl2anc 
 |-  ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) )
153 117 152 jca 
 |-  ( ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) /\ ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) ) -> ( Y e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) ) )
154 153 ex 
 |-  ( ( ( ph /\ c e. ( QQ ^m X ) ) /\ d e. ( QQ ^m X ) ) -> ( ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) -> ( Y e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) ) ) )
155 154 reximdva 
 |-  ( ( ph /\ c e. ( QQ ^m X ) ) -> ( E. d e. ( QQ ^m X ) ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) -> E. d e. ( QQ ^m X ) ( Y e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) ) ) )
156 155 reximdva 
 |-  ( ph -> ( E. c e. ( QQ ^m X ) E. d e. ( QQ ^m X ) ( A. i e. X ( c ` i ) e. ( QQ i^i ( ( ( Y ` i ) - ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) (,) ( Y ` i ) ) ) /\ A. i e. X ( d ` i ) e. ( QQ i^i ( ( Y ` i ) (,) ( ( Y ` i ) + ( E / ( 2 x. ( sqrt ` ( # ` X ) ) ) ) ) ) ) ) -> E. c e. ( QQ ^m X ) E. d e. ( QQ ^m X ) ( Y e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) ) ) )
157 93 156 mpd 
 |-  ( ph -> E. c e. ( QQ ^m X ) E. d e. ( QQ ^m X ) ( Y e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( Y ( ball ` ( dist ` ( RR^ ` X ) ) ) E ) ) )