Description: The sphere around the origin .0. (see rrx0 ) with radius R in a two dimensional Euclidean space is a circle. (Contributed by AV, 5-Feb-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 2sphere.i | |
|
2sphere.e | |
||
2sphere.p | |
||
2sphere.s | |
||
2sphere0.0 | |
||
2sphere0.c | |
||
Assertion | 2sphere0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2sphere.i | |
|
2 | 2sphere.e | |
|
3 | 2sphere.p | |
|
4 | 2sphere.s | |
|
5 | 2sphere0.0 | |
|
6 | 2sphere0.c | |
|
7 | prex | |
|
8 | 1 7 | eqeltri | |
9 | 5 3 | rrx0el | |
10 | 8 9 | ax-mp | |
11 | eqid | |
|
12 | 1 2 3 4 11 | 2sphere | |
13 | 10 12 | mpan | |
14 | 5 | fveq1i | |
15 | c0ex | |
|
16 | 1ex | |
|
17 | 16 | prid1 | |
18 | 17 1 | eleqtrri | |
19 | fvconst2g | |
|
20 | 15 18 19 | mp2an | |
21 | 14 20 | eqtri | |
22 | 21 | a1i | |
23 | 22 | oveq2d | |
24 | 1 3 | rrx2pxel | |
25 | 24 | recnd | |
26 | 25 | subid1d | |
27 | 23 26 | eqtrd | |
28 | 27 | oveq1d | |
29 | 5 | fveq1i | |
30 | 2ex | |
|
31 | 30 | prid2 | |
32 | 31 1 | eleqtrri | |
33 | fvconst2g | |
|
34 | 15 32 33 | mp2an | |
35 | 29 34 | eqtri | |
36 | 35 | a1i | |
37 | 36 | oveq2d | |
38 | 1 3 | rrx2pyel | |
39 | 38 | recnd | |
40 | 39 | subid1d | |
41 | 37 40 | eqtrd | |
42 | 41 | oveq1d | |
43 | 28 42 | oveq12d | |
44 | 43 | eqeq1d | |
45 | 44 | adantl | |
46 | 45 | rabbidva | |
47 | 46 6 | eqtr4di | |
48 | 13 47 | eqtrd | |