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 | |
|
hoiqssbllem1.x | |
||
hoiqssbllem1.n | |
||
hoiqssbllem1.y | |
||
hoiqssbllem1.c | |
||
hoiqssbllem1.d | |
||
hoiqssbllem1.e | |
||
hoiqssbllem1.l | |
||
hoiqssbllem1.r | |
||
Assertion | hoiqssbllem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hoiqssbllem1.i | |
|
2 | hoiqssbllem1.x | |
|
3 | hoiqssbllem1.n | |
|
4 | hoiqssbllem1.y | |
|
5 | hoiqssbllem1.c | |
|
6 | hoiqssbllem1.d | |
|
7 | hoiqssbllem1.e | |
|
8 | hoiqssbllem1.l | |
|
9 | hoiqssbllem1.r | |
|
10 | 4 | elexd | |
11 | elmapfn | |
|
12 | 4 11 | syl | |
13 | 5 | ffvelcdmda | |
14 | 13 | rexrd | |
15 | 6 | ffvelcdmda | |
16 | 15 | rexrd | |
17 | elmapi | |
|
18 | 4 17 | syl | |
19 | 18 | ffvelcdmda | |
20 | 19 | rexrd | |
21 | 2rp | |
|
22 | 21 | a1i | |
23 | hashnncl | |
|
24 | 2 23 | syl | |
25 | 3 24 | mpbird | |
26 | 25 | nnred | |
27 | 25 | nngt0d | |
28 | 26 27 | elrpd | |
29 | 28 | rpsqrtcld | |
30 | 22 29 | rpmulcld | |
31 | 7 30 | rpdivcld | |
32 | 31 | rpred | |
33 | 32 | adantr | |
34 | 19 33 | resubcld | |
35 | 34 | rexrd | |
36 | iooltub | |
|
37 | 35 20 8 36 | syl3anc | |
38 | 13 19 37 | ltled | |
39 | 19 33 | readdcld | |
40 | 39 | rexrd | |
41 | ioogtlb | |
|
42 | 20 40 9 41 | syl3anc | |
43 | 14 16 20 38 42 | elicod | |
44 | 43 | ex | |
45 | 1 44 | ralrimi | |
46 | 10 12 45 | 3jca | |
47 | elixp2 | |
|
48 | 46 47 | sylibr | |