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 ⊢ 𝐼 = { 1 , 2 }
2sphere.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
2sphere.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
2sphere.s ⊢ 𝑆 = ( Sphere ‘ 𝐸 )
2sphere.c ⊢ 𝐶 = { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) }
Assertion 2sphere ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( 𝑀 𝑆 𝑅 ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 2sphere.i ⊢ 𝐼 = { 1 , 2 }
2 2sphere.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3 2sphere.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4 2sphere.s ⊢ 𝑆 = ( Sphere ‘ 𝐸 )
5 2sphere.c ⊢ 𝐶 = { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) }
6 prfi ⊢ { 1 , 2 } ∈ Fin
7 1 6 eqeltri ⊢ 𝐼 ∈ Fin
8 simpl ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → 𝑀 ∈ 𝑃 )
9 elrege0 ⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) ↔ ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) )
10 9 simplbi ⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) → 𝑅 ∈ ℝ )
11 10 adantl ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → 𝑅 ∈ ℝ )
12 eqid ⊢ ( dist ‘ 𝐸 ) = ( dist ‘ 𝐸 )
13 2 3 12 4 rrxsphere ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ ) → ( 𝑀 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ( dist ‘ 𝐸 ) 𝑀 ) = 𝑅 } )
14 7 8 11 13 mp3an2i ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( 𝑀 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ( dist ‘ 𝐸 ) 𝑀 ) = 𝑅 } )
15 9 biimpi ⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) → ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) )
16 15 ad2antlr ⊢ ( ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) )
17 sqrtsq ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( √ ‘ ( 𝑅 ↑ 2 ) ) = 𝑅 )
18 16 17 syl ⊢ ( ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) ∧ 𝑝 ∈ 𝑃 ) → ( √ ‘ ( 𝑅 ↑ 2 ) ) = 𝑅 )
19 18 eqeq2d ⊢ ( ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( √ ‘ ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) ) = ( √ ‘ ( 𝑅 ↑ 2 ) ) ↔ ( √ ‘ ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) ) = 𝑅 ) )
20 1 3 rrx2pxel ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℝ )
21 20 adantl ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 1 ) ∈ ℝ )
22 1 3 rrx2pxel ⊢ ( 𝑀 ∈ 𝑃 → ( 𝑀 ‘ 1 ) ∈ ℝ )
23 22 adantr ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( 𝑀 ‘ 1 ) ∈ ℝ )
24 21 23 resubcld ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ∈ ℝ )
25 24 resqcld ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ∈ ℝ )
26 1 3 rrx2pyel ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 2 ) ∈ ℝ )
27 26 adantl ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 2 ) ∈ ℝ )
28 1 3 rrx2pyel ⊢ ( 𝑀 ∈ 𝑃 → ( 𝑀 ‘ 2 ) ∈ ℝ )
29 28 adantr ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( 𝑀 ‘ 2 ) ∈ ℝ )
30 27 29 resubcld ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ∈ ℝ )
31 30 resqcld ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ∈ ℝ )
32 25 31 readdcld ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) ∈ ℝ )
33 24 sqge0d ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → 0 ≤ ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) )
34 30 sqge0d ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → 0 ≤ ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) )
35 25 31 33 34 addge0d ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → 0 ≤ ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) )
36 32 35 jca ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) ) )
37 36 adantlr ⊢ ( ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) ) )
38 resqcl ⊢ ( 𝑅 ∈ ℝ → ( 𝑅 ↑ 2 ) ∈ ℝ )
39 sqge0 ⊢ ( 𝑅 ∈ ℝ → 0 ≤ ( 𝑅 ↑ 2 ) )
40 38 39 jca ⊢ ( 𝑅 ∈ ℝ → ( ( 𝑅 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝑅 ↑ 2 ) ) )
41 10 40 syl ⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) → ( ( 𝑅 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝑅 ↑ 2 ) ) )
42 41 ad2antlr ⊢ ( ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑅 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝑅 ↑ 2 ) ) )
43 sqrt11 ⊢ ( ( ( ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) ) ∧ ( ( 𝑅 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝑅 ↑ 2 ) ) ) → ( ( √ ‘ ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) ) = ( √ ‘ ( 𝑅 ↑ 2 ) ) ↔ ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
44 37 42 43 syl2anc ⊢ ( ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( √ ‘ ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) ) = ( √ ‘ ( 𝑅 ↑ 2 ) ) ↔ ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
45 8 anim1ci ⊢ ( ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ∈ 𝑃 ∧ 𝑀 ∈ 𝑃 ) )
46 2nn0 ⊢ 2 ∈ ℕ0
47 eqid ⊢ ( 𝔼hil ‘ 2 ) = ( 𝔼hil ‘ 2 )
48 47 ehlval ⊢ ( 2 ∈ ℕ0 → ( 𝔼hil ‘ 2 ) = ( ℝ^ ‘ ( 1 ... 2 ) ) )
49 46 48 ax-mp ⊢ ( 𝔼hil ‘ 2 ) = ( ℝ^ ‘ ( 1 ... 2 ) )
50 fz12pr ⊢ ( 1 ... 2 ) = { 1 , 2 }
51 50 1 eqtr4i ⊢ ( 1 ... 2 ) = 𝐼
52 51 fveq2i ⊢ ( ℝ^ ‘ ( 1 ... 2 ) ) = ( ℝ^ ‘ 𝐼 )
53 49 52 eqtri ⊢ ( 𝔼hil ‘ 2 ) = ( ℝ^ ‘ 𝐼 )
54 2 53 eqtr4i ⊢ 𝐸 = ( 𝔼hil ‘ 2 )
55 1 oveq2i ⊢ ( ℝ ↑m 𝐼 ) = ( ℝ ↑m { 1 , 2 } )
56 3 55 eqtri ⊢ 𝑃 = ( ℝ ↑m { 1 , 2 } )
57 54 56 12 ehl2eudisval ⊢ ( ( 𝑝 ∈ 𝑃 ∧ 𝑀 ∈ 𝑃 ) → ( 𝑝 ( dist ‘ 𝐸 ) 𝑀 ) = ( √ ‘ ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) ) )
58 45 57 syl ⊢ ( ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ( dist ‘ 𝐸 ) 𝑀 ) = ( √ ‘ ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) ) )
59 58 eqcomd ⊢ ( ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) ∧ 𝑝 ∈ 𝑃 ) → ( √ ‘ ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) ) = ( 𝑝 ( dist ‘ 𝐸 ) 𝑀 ) )
60 59 eqeq1d ⊢ ( ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( √ ‘ ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) ) = 𝑅 ↔ ( 𝑝 ( dist ‘ 𝐸 ) 𝑀 ) = 𝑅 ) )
61 19 44 60 3bitr3d ⊢ ( ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ↔ ( 𝑝 ( dist ‘ 𝐸 ) 𝑀 ) = 𝑅 ) )
62 61 rabbidva ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 2 ) − ( 𝑀 ‘ 2 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ( dist ‘ 𝐸 ) 𝑀 ) = 𝑅 } )
63 5 62 eqtr2id ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ( dist ‘ 𝐸 ) 𝑀 ) = 𝑅 } = 𝐶 )
64 14 63 eqtrd ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( 𝑀 𝑆 𝑅 ) = 𝐶 )