Description: The sphere with center M and radius R in a generalized real Euclidean space of finite dimension. Remark: this theorem holds also for the degenerate case R < 0 (negative radius): in this case, ( M S R ) is empty. (Contributed by AV, 5-Feb-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rrxspheres.e | |
|
rrxspheres.p | |
||
rrxspheres.d | |
||
rrxspheres.s | |
||
Assertion | rrxsphere | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rrxspheres.e | |
|
2 | rrxspheres.p | |
|
3 | rrxspheres.d | |
|
4 | rrxspheres.s | |
|
5 | 1 | fvexi | |
6 | id | |
|
7 | eqid | |
|
8 | 6 1 7 | rrxbasefi | |
9 | 2 8 | eqtr4id | |
10 | 9 | eleq2d | |
11 | 10 | biimpa | |
12 | 11 | 3adant3 | |
13 | 12 | adantl | |
14 | rexr | |
|
15 | 14 | 3ad2ant3 | |
16 | 15 | anim2i | |
17 | 16 | ancomd | |
18 | elxrge0 | |
|
19 | 17 18 | sylibr | |
20 | 7 4 3 | sphere | |
21 | 5 13 19 20 | mp3an2i | |
22 | simp1 | |
|
23 | 22 1 7 | rrxbasefi | |
24 | 23 2 | eqtr4di | |
25 | 24 | adantl | |
26 | 25 | rabeqdv | |
27 | 21 26 | eqtrd | |
28 | 27 | ex | |
29 | 7 4 3 | spheres | |
30 | 5 29 | ax-mp | |
31 | fvex | |
|
32 | 31 | rabex | |
33 | 30 32 | dmmpo | |
34 | 0xr | |
|
35 | pnfxr | |
|
36 | 34 35 | pm3.2i | |
37 | elicc1 | |
|
38 | 36 37 | mp1i | |
39 | simp2 | |
|
40 | 38 39 | syl6bi | |
41 | 40 | con3d | |
42 | 41 | imp | |
43 | 42 | intnand | |
44 | ndmovg | |
|
45 | 33 43 44 | sylancr | |
46 | 1 | fveq2i | |
47 | 3 46 | eqtri | |
48 | 47 | rrxmetfi | |
49 | 48 | 3ad2ant1 | |
50 | 49 | adantr | |
51 | 2 | fveq2i | |
52 | 50 51 | eleqtrrdi | |
53 | simpr | |
|
54 | simp2 | |
|
55 | 54 | adantr | |
56 | metge0 | |
|
57 | 52 53 55 56 | syl3anc | |
58 | breq2 | |
|
59 | 57 58 | syl5ibcom | |
60 | 59 | con3d | |
61 | 60 | impancom | |
62 | 61 | imp | |
63 | 62 | ralrimiva | |
64 | eqcom | |
|
65 | rabeq0 | |
|
66 | 64 65 | bitri | |
67 | 63 66 | sylibr | |
68 | 45 67 | eqtrd | |
69 | 68 | expcom | |
70 | 28 69 | pm2.61i | |