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

Proof

Step Hyp Ref Expression
1 2sphere.i ⊢ 𝐼 = ( 0 ..^ 2 )
2 2sphere.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3 2sphere.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4 2sphere.s ⊢ 𝑆 = ( Sphere ‘ 𝐸 )
5 2sphere.c ⊢ 𝐶 = { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) }
6 fzofi ⊢ ( 0 ..^ 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 [,) +∞ ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( √ ‘ ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ) ) = ( √ ‘ ( 𝑅 ↑ 2 ) ) ↔ ( √ ‘ ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ) ) = 𝑅 ) )
20 1 3 rrx2pxel ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 0 ) ∈ ℝ )
21 20 adantl ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 0 ) ∈ ℝ )
22 1 3 rrx2pxel ⊢ ( 𝑀 ∈ 𝑃 → ( 𝑀 ‘ 0 ) ∈ ℝ )
23 22 adantr ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( 𝑀 ‘ 0 ) ∈ ℝ )
24 21 23 resubcld ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ∈ ℝ )
25 24 resqcld ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) ∈ ℝ )
26 1 3 rrx2pyel ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℝ )
27 26 adantl ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 1 ) ∈ ℝ )
28 1 3 rrx2pyel ⊢ ( 𝑀 ∈ 𝑃 → ( 𝑀 ‘ 1 ) ∈ ℝ )
29 28 adantr ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( 𝑀 ‘ 1 ) ∈ ℝ )
30 27 29 resubcld ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ∈ ℝ )
31 30 resqcld ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ∈ ℝ )
32 25 31 readdcld ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ) ∈ ℝ )
33 24 sqge0d ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → 0 ≤ ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) )
34 30 sqge0d ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → 0 ≤ ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) )
35 25 31 33 34 addge0d ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → 0 ≤ ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ) )
36 32 35 jca ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ) ) )
37 36 adantlr ⊢ ( ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 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 ⊢ ( ( ( ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ) ) ∧ ( ( 𝑅 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝑅 ↑ 2 ) ) ) → ( ( √ ‘ ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ) ) = ( √ ‘ ( 𝑅 ↑ 2 ) ) ↔ ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
44 37 42 43 syl2anc ⊢ ( ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( √ ‘ ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ) ) = ( √ ‘ ( 𝑅 ↑ 2 ) ) ↔ ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
45 8 anim1ci ⊢ ( ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ∈ 𝑃 ∧ 𝑀 ∈ 𝑃 ) )
46 1 fveq2i ⊢ ( ℝ^ ‘ 𝐼 ) = ( ℝ^ ‘ ( 0 ..^ 2 ) )
47 2nn0 ⊢ 2 ∈ ℕ0
48 eqid ⊢ ( 𝔼hil ‘ 2 ) = ( 𝔼hil ‘ 2 )
49 48 ehlval ⊢ ( 2 ∈ ℕ0 → ( 𝔼hil ‘ 2 ) = ( ℝ^ ‘ ( 0 ..^ 2 ) ) )
50 47 49 ax-mp ⊢ ( 𝔼hil ‘ 2 ) = ( ℝ^ ‘ ( 0 ..^ 2 ) )
51 46 2 50 3eqtr4i ⊢ 𝐸 = ( 𝔼hil ‘ 2 )
52 1 oveq2i ⊢ ( ℝ ↑m 𝐼 ) = ( ℝ ↑m ( 0 ..^ 2 ) )
53 3 52 eqtri ⊢ 𝑃 = ( ℝ ↑m ( 0 ..^ 2 ) )
54 51 53 12 ehl2eudisval ⊢ ( ( 𝑝 ∈ 𝑃 ∧ 𝑀 ∈ 𝑃 ) → ( 𝑝 ( dist ‘ 𝐸 ) 𝑀 ) = ( √ ‘ ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ) ) )
55 45 54 syl ⊢ ( ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ( dist ‘ 𝐸 ) 𝑀 ) = ( √ ‘ ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ) ) )
56 55 eqcomd ⊢ ( ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) ∧ 𝑝 ∈ 𝑃 ) → ( √ ‘ ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ) ) = ( 𝑝 ( dist ‘ 𝐸 ) 𝑀 ) )
57 56 eqeq1d ⊢ ( ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( √ ‘ ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ) ) = 𝑅 ↔ ( 𝑝 ( dist ‘ 𝐸 ) 𝑀 ) = 𝑅 ) )
58 19 44 57 3bitr3d ⊢ ( ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ↔ ( 𝑝 ( dist ‘ 𝐸 ) 𝑀 ) = 𝑅 ) )
59 58 rabbidva ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑝 ‘ 0 ) − ( 𝑀 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑝 ‘ 1 ) − ( 𝑀 ‘ 1 ) ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ( dist ‘ 𝐸 ) 𝑀 ) = 𝑅 } )
60 5 59 eqtr2id ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ( dist ‘ 𝐸 ) 𝑀 ) = 𝑅 } = 𝐶 )
61 14 60 eqtrd ⊢ ( ( 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( 𝑀 𝑆 𝑅 ) = 𝐶 )