Metamath Proof Explorer

Theorem 2sphere

Description: The sphere with center M and radius R in a two dimensional Euclidean space is a circle. (Contributed by AV, 5-Feb-2023)

Ref Expression
Hypotheses 2sphere.i 
|- I = ( 0 ..^ 2 )
2sphere.e 
|- E = ( RR^ ` I )
2sphere.p 
|- P = ( RR ^m I )
2sphere.s 
|- S = ( Sphere ` E )
2sphere.c 
|- C = { p e. P | ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) = ( R ^ 2 ) }
Assertion 2sphere 
|- ( ( M e. P /\ R e. ( 0 [,) +oo ) ) -> ( M S R ) = C )

Proof

Step Hyp Ref Expression
1 2sphere.i 
 |-  I = ( 0 ..^ 2 )
2 2sphere.e 
 |-  E = ( RR^ ` I )
3 2sphere.p 
 |-  P = ( RR ^m I )
4 2sphere.s 
 |-  S = ( Sphere ` E )
5 2sphere.c 
 |-  C = { p e. P | ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) = ( R ^ 2 ) }
6 fzofi 
 |-  ( 0 ..^ 2 ) e. Fin
7 1 6 eqeltri 
 |-  I e. Fin
8 simpl 
 |-  ( ( M e. P /\ R e. ( 0 [,) +oo ) ) -> M e. P )
9 elrege0 
 |-  ( R e. ( 0 [,) +oo ) <-> ( R e. RR /\ 0 <_ R ) )
10 9 simplbi 
 |-  ( R e. ( 0 [,) +oo ) -> R e. RR )
11 10 adantl 
 |-  ( ( M e. P /\ R e. ( 0 [,) +oo ) ) -> R e. RR )
12 eqid 
 |-  ( dist ` E ) = ( dist ` E )
13 2 3 12 4 rrxsphere 
 |-  ( ( I e. Fin /\ M e. P /\ R e. RR ) -> ( M S R ) = { p e. P | ( p ( dist ` E ) M ) = R } )
14 7 8 11 13 mp3an2i 
 |-  ( ( M e. P /\ R e. ( 0 [,) +oo ) ) -> ( M S R ) = { p e. P | ( p ( dist ` E ) M ) = R } )
15 9 biimpi 
 |-  ( R e. ( 0 [,) +oo ) -> ( R e. RR /\ 0 <_ R ) )
16 15 ad2antlr 
 |-  ( ( ( M e. P /\ R e. ( 0 [,) +oo ) ) /\ p e. P ) -> ( R e. RR /\ 0 <_ R ) )
17 sqrtsq 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( sqrt ` ( R ^ 2 ) ) = R )
18 16 17 syl 
 |-  ( ( ( M e. P /\ R e. ( 0 [,) +oo ) ) /\ p e. P ) -> ( sqrt ` ( R ^ 2 ) ) = R )
19 18 eqeq2d 
 |-  ( ( ( M e. P /\ R e. ( 0 [,) +oo ) ) /\ p e. P ) -> ( ( sqrt ` ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) ) = ( sqrt ` ( R ^ 2 ) ) <-> ( sqrt ` ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) ) = R ) )
20 1 3 rrx2pxel 
 |-  ( p e. P -> ( p ` 0 ) e. RR )
21 20 adantl 
 |-  ( ( M e. P /\ p e. P ) -> ( p ` 0 ) e. RR )
22 1 3 rrx2pxel 
 |-  ( M e. P -> ( M ` 0 ) e. RR )
23 22 adantr 
 |-  ( ( M e. P /\ p e. P ) -> ( M ` 0 ) e. RR )
24 21 23 resubcld 
 |-  ( ( M e. P /\ p e. P ) -> ( ( p ` 0 ) - ( M ` 0 ) ) e. RR )
25 24 resqcld 
 |-  ( ( M e. P /\ p e. P ) -> ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) e. RR )
26 1 3 rrx2pyel 
 |-  ( p e. P -> ( p ` 1 ) e. RR )
27 26 adantl 
 |-  ( ( M e. P /\ p e. P ) -> ( p ` 1 ) e. RR )
28 1 3 rrx2pyel 
 |-  ( M e. P -> ( M ` 1 ) e. RR )
29 28 adantr 
 |-  ( ( M e. P /\ p e. P ) -> ( M ` 1 ) e. RR )
30 27 29 resubcld 
 |-  ( ( M e. P /\ p e. P ) -> ( ( p ` 1 ) - ( M ` 1 ) ) e. RR )
31 30 resqcld 
 |-  ( ( M e. P /\ p e. P ) -> ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) e. RR )
32 25 31 readdcld 
 |-  ( ( M e. P /\ p e. P ) -> ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) e. RR )
33 24 sqge0d 
 |-  ( ( M e. P /\ p e. P ) -> 0 <_ ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) )
34 30 sqge0d 
 |-  ( ( M e. P /\ p e. P ) -> 0 <_ ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) )
35 25 31 33 34 addge0d 
 |-  ( ( M e. P /\ p e. P ) -> 0 <_ ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) )
36 32 35 jca 
 |-  ( ( M e. P /\ p e. P ) -> ( ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) e. RR /\ 0 <_ ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) ) )
37 36 adantlr 
 |-  ( ( ( M e. P /\ R e. ( 0 [,) +oo ) ) /\ p e. P ) -> ( ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) e. RR /\ 0 <_ ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) ) )
38 resqcl 
 |-  ( R e. RR -> ( R ^ 2 ) e. RR )
39 sqge0 
 |-  ( R e. RR -> 0 <_ ( R ^ 2 ) )
40 38 39 jca 
 |-  ( R e. RR -> ( ( R ^ 2 ) e. RR /\ 0 <_ ( R ^ 2 ) ) )
41 10 40 syl 
 |-  ( R e. ( 0 [,) +oo ) -> ( ( R ^ 2 ) e. RR /\ 0 <_ ( R ^ 2 ) ) )
42 41 ad2antlr 
 |-  ( ( ( M e. P /\ R e. ( 0 [,) +oo ) ) /\ p e. P ) -> ( ( R ^ 2 ) e. RR /\ 0 <_ ( R ^ 2 ) ) )
43 sqrt11 
 |-  ( ( ( ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) e. RR /\ 0 <_ ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) ) /\ ( ( R ^ 2 ) e. RR /\ 0 <_ ( R ^ 2 ) ) ) -> ( ( sqrt ` ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) ) = ( sqrt ` ( R ^ 2 ) ) <-> ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) = ( R ^ 2 ) ) )
44 37 42 43 syl2anc 
 |-  ( ( ( M e. P /\ R e. ( 0 [,) +oo ) ) /\ p e. P ) -> ( ( sqrt ` ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) ) = ( sqrt ` ( R ^ 2 ) ) <-> ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) = ( R ^ 2 ) ) )
45 8 anim1ci 
 |-  ( ( ( M e. P /\ R e. ( 0 [,) +oo ) ) /\ p e. P ) -> ( p e. P /\ M e. P ) )
46 1 fveq2i 
 |-  ( RR^ ` I ) = ( RR^ ` ( 0 ..^ 2 ) )
47 2nn0 
 |-  2 e. NN0
48 eqid 
 |-  ( EEhil ` 2 ) = ( EEhil ` 2 )
49 48 ehlval 
 |-  ( 2 e. NN0 -> ( EEhil ` 2 ) = ( RR^ ` ( 0 ..^ 2 ) ) )
50 47 49 ax-mp 
 |-  ( EEhil ` 2 ) = ( RR^ ` ( 0 ..^ 2 ) )
51 46 2 50 3eqtr4i 
 |-  E = ( EEhil ` 2 )
52 1 oveq2i 
 |-  ( RR ^m I ) = ( RR ^m ( 0 ..^ 2 ) )
53 3 52 eqtri 
 |-  P = ( RR ^m ( 0 ..^ 2 ) )
54 51 53 12 ehl2eudisval 
 |-  ( ( p e. P /\ M e. P ) -> ( p ( dist ` E ) M ) = ( sqrt ` ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) ) )
55 45 54 syl 
 |-  ( ( ( M e. P /\ R e. ( 0 [,) +oo ) ) /\ p e. P ) -> ( p ( dist ` E ) M ) = ( sqrt ` ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) ) )
56 55 eqcomd 
 |-  ( ( ( M e. P /\ R e. ( 0 [,) +oo ) ) /\ p e. P ) -> ( sqrt ` ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) ) = ( p ( dist ` E ) M ) )
57 56 eqeq1d 
 |-  ( ( ( M e. P /\ R e. ( 0 [,) +oo ) ) /\ p e. P ) -> ( ( sqrt ` ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) ) = R <-> ( p ( dist ` E ) M ) = R ) )
58 19 44 57 3bitr3d 
 |-  ( ( ( M e. P /\ R e. ( 0 [,) +oo ) ) /\ p e. P ) -> ( ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) = ( R ^ 2 ) <-> ( p ( dist ` E ) M ) = R ) )
59 58 rabbidva 
 |-  ( ( M e. P /\ R e. ( 0 [,) +oo ) ) -> { p e. P | ( ( ( ( p ` 0 ) - ( M ` 0 ) ) ^ 2 ) + ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) ) = ( R ^ 2 ) } = { p e. P | ( p ( dist ` E ) M ) = R } )
60 5 59 eqtr2id 
 |-  ( ( M e. P /\ R e. ( 0 [,) +oo ) ) -> { p e. P | ( p ( dist ` E ) M ) = R } = C )
61 14 60 eqtrd 
 |-  ( ( M e. P /\ R e. ( 0 [,) +oo ) ) -> ( M S R ) = C )