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 iφ
hoiqssbllem1.x φXFin
hoiqssbllem1.n φX
hoiqssbllem1.y φYX
hoiqssbllem1.c φC:X
hoiqssbllem1.d φD:X
hoiqssbllem1.e φE+
hoiqssbllem1.l φiXCiYiE2XYi
hoiqssbllem1.r φiXDiYiYi+E2X
Assertion hoiqssbllem1 φYiXCiDi

Proof

Step Hyp Ref Expression
1 hoiqssbllem1.i iφ
2 hoiqssbllem1.x φXFin
3 hoiqssbllem1.n φX
4 hoiqssbllem1.y φYX
5 hoiqssbllem1.c φC:X
6 hoiqssbllem1.d φD:X
7 hoiqssbllem1.e φE+
8 hoiqssbllem1.l φiXCiYiE2XYi
9 hoiqssbllem1.r φiXDiYiYi+E2X
10 4 elexd φYV
11 elmapfn YXYFnX
12 4 11 syl φYFnX
13 5 ffvelcdmda φiXCi
14 13 rexrd φiXCi*
15 6 ffvelcdmda φiXDi
16 15 rexrd φiXDi*
17 elmapi YXY:X
18 4 17 syl φY:X
19 18 ffvelcdmda φiXYi
20 19 rexrd φiXYi*
21 2rp 2+
22 21 a1i φ2+
23 hashnncl XFinXX
24 2 23 syl φXX
25 3 24 mpbird φX
26 25 nnred φX
27 25 nngt0d φ0<X
28 26 27 elrpd φX+
29 28 rpsqrtcld φX+
30 22 29 rpmulcld φ2X+
31 7 30 rpdivcld φE2X+
32 31 rpred φE2X
33 32 adantr φiXE2X
34 19 33 resubcld φiXYiE2X
35 34 rexrd φiXYiE2X*
36 iooltub YiE2X*Yi*CiYiE2XYiCi<Yi
37 35 20 8 36 syl3anc φiXCi<Yi
38 13 19 37 ltled φiXCiYi
39 19 33 readdcld φiXYi+E2X
40 39 rexrd φiXYi+E2X*
41 ioogtlb Yi*Yi+E2X*DiYiYi+E2XYi<Di
42 20 40 9 41 syl3anc φiXYi<Di
43 14 16 20 38 42 elicod φiXYiCiDi
44 43 ex φiXYiCiDi
45 1 44 ralrimi φiXYiCiDi
46 10 12 45 3jca φYVYFnXiXYiCiDi
47 elixp2 YiXCiDiYVYFnXiXYiCiDi
48 46 47 sylibr φYiXCiDi