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 = { 1 , 2 }
2sphere.e
|- E = ( RR^ ` I )
2sphere.p
|- P = ( RR ^m I )
2sphere.s
|- S = ( Sphere ` E )
2sphere.c
|- C = { p e. P | ( ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 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 = { 1 , 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 ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) ) = ( R ^ 2 ) }
6 prfi
 |-  { 1 , 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 ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) ) ) = ( sqrt ` ( R ^ 2 ) ) <-> ( sqrt ` ( ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) ) ) = R ) )
20 1 3 rrx2pxel
 |-  ( p e. P -> ( p ` 1 ) e. RR )
21 20 adantl
 |-  ( ( M e. P /\ p e. P ) -> ( p ` 1 ) e. RR )
22 1 3 rrx2pxel
 |-  ( M e. P -> ( M ` 1 ) e. RR )
23 22 adantr
 |-  ( ( M e. P /\ p e. P ) -> ( M ` 1 ) e. RR )
24 21 23 resubcld
 |-  ( ( M e. P /\ p e. P ) -> ( ( p ` 1 ) - ( M ` 1 ) ) e. RR )
25 24 resqcld
 |-  ( ( M e. P /\ p e. P ) -> ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) e. RR )
26 1 3 rrx2pyel
 |-  ( p e. P -> ( p ` 2 ) e. RR )
27 26 adantl
 |-  ( ( M e. P /\ p e. P ) -> ( p ` 2 ) e. RR )
28 1 3 rrx2pyel
 |-  ( M e. P -> ( M ` 2 ) e. RR )
29 28 adantr
 |-  ( ( M e. P /\ p e. P ) -> ( M ` 2 ) e. RR )
30 27 29 resubcld
 |-  ( ( M e. P /\ p e. P ) -> ( ( p ` 2 ) - ( M ` 2 ) ) e. RR )
31 30 resqcld
 |-  ( ( M e. P /\ p e. P ) -> ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) e. RR )
32 25 31 readdcld
 |-  ( ( M e. P /\ p e. P ) -> ( ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) ) e. RR )
33 24 sqge0d
 |-  ( ( M e. P /\ p e. P ) -> 0 <_ ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) )
34 30 sqge0d
 |-  ( ( M e. P /\ p e. P ) -> 0 <_ ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) )
35 25 31 33 34 addge0d
 |-  ( ( M e. P /\ p e. P ) -> 0 <_ ( ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) ) )
36 32 35 jca
 |-  ( ( M e. P /\ p e. P ) -> ( ( ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) ) e. RR /\ 0 <_ ( ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) ) ) )
37 36 adantlr
 |-  ( ( ( M e. P /\ R e. ( 0 [,) +oo ) ) /\ p e. P ) -> ( ( ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) ) e. RR /\ 0 <_ ( ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 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 ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) ) e. RR /\ 0 <_ ( ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) ) ) /\ ( ( R ^ 2 ) e. RR /\ 0 <_ ( R ^ 2 ) ) ) -> ( ( sqrt ` ( ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) ) ) = ( sqrt ` ( R ^ 2 ) ) <-> ( ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) ) = ( R ^ 2 ) ) )
44 37 42 43 syl2anc
 |-  ( ( ( M e. P /\ R e. ( 0 [,) +oo ) ) /\ p e. P ) -> ( ( sqrt ` ( ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) ) ) = ( sqrt ` ( R ^ 2 ) ) <-> ( ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) ) = ( R ^ 2 ) ) )
45 8 anim1ci
 |-  ( ( ( M e. P /\ R e. ( 0 [,) +oo ) ) /\ p e. P ) -> ( p e. P /\ M e. P ) )
46 2nn0
 |-  2 e. NN0
47 eqid
 |-  ( EEhil ` 2 ) = ( EEhil ` 2 )
48 47 ehlval
 |-  ( 2 e. NN0 -> ( EEhil ` 2 ) = ( RR^ ` ( 1 ... 2 ) ) )
49 46 48 ax-mp
 |-  ( EEhil ` 2 ) = ( RR^ ` ( 1 ... 2 ) )
50 fz12pr
 |-  ( 1 ... 2 ) = { 1 , 2 }
51 50 1 eqtr4i
 |-  ( 1 ... 2 ) = I
52 51 fveq2i
 |-  ( RR^ ` ( 1 ... 2 ) ) = ( RR^ ` I )
53 49 52 eqtri
 |-  ( EEhil ` 2 ) = ( RR^ ` I )
54 2 53 eqtr4i
 |-  E = ( EEhil ` 2 )
55 1 oveq2i
 |-  ( RR ^m I ) = ( RR ^m { 1 , 2 } )
56 3 55 eqtri
 |-  P = ( RR ^m { 1 , 2 } )
57 54 56 12 ehl2eudisval
 |-  ( ( p e. P /\ M e. P ) -> ( p ( dist ` E ) M ) = ( sqrt ` ( ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) ) ) )
58 45 57 syl
 |-  ( ( ( M e. P /\ R e. ( 0 [,) +oo ) ) /\ p e. P ) -> ( p ( dist ` E ) M ) = ( sqrt ` ( ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) ) ) )
59 58 eqcomd
 |-  ( ( ( M e. P /\ R e. ( 0 [,) +oo ) ) /\ p e. P ) -> ( sqrt ` ( ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) ) ) = ( p ( dist ` E ) M ) )
60 59 eqeq1d
 |-  ( ( ( M e. P /\ R e. ( 0 [,) +oo ) ) /\ p e. P ) -> ( ( sqrt ` ( ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) ) ) = R <-> ( p ( dist ` E ) M ) = R ) )
61 19 44 60 3bitr3d
 |-  ( ( ( M e. P /\ R e. ( 0 [,) +oo ) ) /\ p e. P ) -> ( ( ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) ) = ( R ^ 2 ) <-> ( p ( dist ` E ) M ) = R ) )
62 61 rabbidva
 |-  ( ( M e. P /\ R e. ( 0 [,) +oo ) ) -> { p e. P | ( ( ( ( p ` 1 ) - ( M ` 1 ) ) ^ 2 ) + ( ( ( p ` 2 ) - ( M ` 2 ) ) ^ 2 ) ) = ( R ^ 2 ) } = { p e. P | ( p ( dist ` E ) M ) = R } )
63 5 62 eqtr2id
 |-  ( ( M e. P /\ R e. ( 0 [,) +oo ) ) -> { p e. P | ( p ( dist ` E ) M ) = R } = C )
64 14 63 eqtrd
 |-  ( ( M e. P /\ R e. ( 0 [,) +oo ) ) -> ( M S R ) = C )