2sphere - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > 2sphere		Structured version Visualization version GIF version

Theorem 2sphere 50066

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

**Hypotheses**
Ref	Expression
2sphere.i	⊢ 𝐼 = (0..^2)
2sphere.e	⊢ 𝐸 = (ℝ^‘𝐼)
2sphere.p	⊢ 𝑃 = (ℝ ↑_m 𝐼)
2sphere.s	⊢ 𝑆 = (Sphere‘𝐸)
2sphere.c	⊢ 𝐶 = {𝑝 ∈ 𝑃 ∣ ((((𝑝‘0) − (𝑀‘0))↑2) + (((𝑝‘1) − (𝑀‘1))↑2)) = (𝑅↑2)}

**Assertion**
Ref	Expression
2sphere	⊢ ((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) → (𝑀𝑆𝑅) = 𝐶)

Distinct variable groups: 𝐸,𝑝 𝐼,𝑝 𝑀,𝑝 𝑃,𝑝 𝑅,𝑝 Allowed substitution hints: 𝐶(𝑝) 𝑆(𝑝)

**Proof of Theorem 2sphere**
Step	Hyp	Ref	Expression
1		2sphere.i	. . . 4 ⊢ 𝐼 = (0..^2)
2		fzofi 14144	. . . 4 ⊢ (0..^2) ∈ Fin
3	1, 2	eqeltri 2860	. . 3 ⊢ 𝐼 ∈ Fin
4		simpl 488	. . 3 ⊢ ((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) → 𝑀 ∈ 𝑃)
5		elrege0 13612	. . . . 5 ⊢ (𝑅 ∈ (0[,)+∞) ↔ (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅))
6	5	simplbi 502	. . . 4 ⊢ (𝑅 ∈ (0[,)+∞) → 𝑅 ∈ ℝ)
7	6	adantl 487	. . 3 ⊢ ((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) → 𝑅 ∈ ℝ)
8		2sphere.e	. . . 4 ⊢ 𝐸 = (ℝ^‘𝐼)
9		2sphere.p	. . . 4 ⊢ 𝑃 = (ℝ ↑_m 𝐼)
10		eqid 2763	. . . 4 ⊢ (dist‘𝐸) = (dist‘𝐸)
11		2sphere.s	. . . 4 ⊢ 𝑆 = (Sphere‘𝐸)
12	8, 9, 10, 11	rrxsphere 50065	. . 3 ⊢ ((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) → (𝑀𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (𝑝(dist‘𝐸)𝑀) = 𝑅})
13	3, 4, 7, 12	mp3an2i 1496	. 2 ⊢ ((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) → (𝑀𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (𝑝(dist‘𝐸)𝑀) = 𝑅})
14		2sphere.c	. . 3 ⊢ 𝐶 = {𝑝 ∈ 𝑃 ∣ ((((𝑝‘0) − (𝑀‘0))↑2) + (((𝑝‘1) − (𝑀‘1))↑2)) = (𝑅↑2)}
15	5	biimpi 219	. . . . . . . 8 ⊢ (𝑅 ∈ (0[,)+∞) → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅))
16	15	ad2antlr 740	. . . . . . 7 ⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅))
17		sqrtsq 15465	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (√‘(𝑅↑2)) = 𝑅)
18	16, 17	syl 18	. . . . . 6 ⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → (√‘(𝑅↑2)) = 𝑅)
19	18	eqeq2d 2774	. . . . 5 ⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → ((√‘((((𝑝‘0) − (𝑀‘0))↑2) + (((𝑝‘1) − (𝑀‘1))↑2))) = (√‘(𝑅↑2)) ↔ (√‘((((𝑝‘0) − (𝑀‘0))↑2) + (((𝑝‘1) − (𝑀‘1))↑2))) = 𝑅))
20	1, 9	rrx2pxel 50028	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘0) ∈ ℝ)
21	20	adantl 487	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → (𝑝‘0) ∈ ℝ)
22	1, 9	rrx2pxel 50028	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ 𝑃 → (𝑀‘0) ∈ ℝ)
23	22	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → (𝑀‘0) ∈ ℝ)
24	21, 23	resubcld 11771	. . . . . . . . . 10 ⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → ((𝑝‘0) − (𝑀‘0)) ∈ ℝ)
25	24	resqcld 14295	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → (((𝑝‘0) − (𝑀‘0))↑2) ∈ ℝ)
26	1, 9	rrx2pyel 50029	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℝ)
27	26	adantl 487	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → (𝑝‘1) ∈ ℝ)
28	1, 9	rrx2pyel 50029	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ 𝑃 → (𝑀‘1) ∈ ℝ)
29	28	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → (𝑀‘1) ∈ ℝ)
30	27, 29	resubcld 11771	. . . . . . . . . 10 ⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → ((𝑝‘1) − (𝑀‘1)) ∈ ℝ)
31	30	resqcld 14295	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → (((𝑝‘1) − (𝑀‘1))↑2) ∈ ℝ)
32	25, 31	readdcld 11365	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → ((((𝑝‘0) − (𝑀‘0))↑2) + (((𝑝‘1) − (𝑀‘1))↑2)) ∈ ℝ)
33	24	sqge0d 14307	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → 0 ≤ (((𝑝‘0) − (𝑀‘0))↑2))
34	30	sqge0d 14307	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → 0 ≤ (((𝑝‘1) − (𝑀‘1))↑2))
35	25, 31, 33, 34	addge0d 11919	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → 0 ≤ ((((𝑝‘0) − (𝑀‘0))↑2) + (((𝑝‘1) − (𝑀‘1))↑2)))
36	32, 35	jca 521	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → (((((𝑝‘0) − (𝑀‘0))↑2) + (((𝑝‘1) − (𝑀‘1))↑2)) ∈ ℝ ∧ 0 ≤ ((((𝑝‘0) − (𝑀‘0))↑2) + (((𝑝‘1) − (𝑀‘1))↑2))))
37	36	adantlr 728	. . . . . 6 ⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → (((((𝑝‘0) − (𝑀‘0))↑2) + (((𝑝‘1) − (𝑀‘1))↑2)) ∈ ℝ ∧ 0 ≤ ((((𝑝‘0) − (𝑀‘0))↑2) + (((𝑝‘1) − (𝑀‘1))↑2))))
38		resqcl 14294	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℝ)
39		sqge0 14306	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ → 0 ≤ (𝑅↑2))
40	38, 39	jca 521	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ → ((𝑅↑2) ∈ ℝ ∧ 0 ≤ (𝑅↑2)))
41	6, 40	syl 18	. . . . . . 7 ⊢ (𝑅 ∈ (0[,)+∞) → ((𝑅↑2) ∈ ℝ ∧ 0 ≤ (𝑅↑2)))
42	41	ad2antlr 740	. . . . . 6 ⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → ((𝑅↑2) ∈ ℝ ∧ 0 ≤ (𝑅↑2)))
43		sqrt11 15458	. . . . . 6 ⊢ (((((((𝑝‘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 596	. . . . 5 ⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → ((√‘((((𝑝‘0) − (𝑀‘0))↑2) + (((𝑝‘1) − (𝑀‘1))↑2))) = (√‘(𝑅↑2)) ↔ ((((𝑝‘0) − (𝑀‘0))↑2) + (((𝑝‘1) − (𝑀‘1))↑2)) = (𝑅↑2)))
45	4	anim1ci 628	. . . . . . . 8 ⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → (𝑝 ∈ 𝑃 ∧ 𝑀 ∈ 𝑃))
46	1	fveq2i 6911	. . . . . . . . . 10 ⊢ (ℝ^‘𝐼) = (ℝ^‘(0..^2))
47		2nn0 12650	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
48		eqid 2763	. . . . . . . . . . . 12 ⊢ (𝔼_hil‘2) = (𝔼_hil‘2)
49	48	ehlval 25765	. . . . . . . . . . 11 ⊢ (2 ∈ ℕ₀ → (𝔼_hil‘2) = (ℝ^‘(0..^2)))
50	47, 49	ax-mp 5	. . . . . . . . . 10 ⊢ (𝔼_hil‘2) = (ℝ^‘(0..^2))
51	46, 8, 50	3eqtr4i 2796	. . . . . . . . 9 ⊢ 𝐸 = (𝔼_hil‘2)
52	1	oveq2i 7454	. . . . . . . . . 10 ⊢ (ℝ ↑_m 𝐼) = (ℝ ↑_m (0..^2))
53	9, 52	eqtri 2786	. . . . . . . . 9 ⊢ 𝑃 = (ℝ ↑_m (0..^2))
54	51, 53, 10	ehl2eudisval 25774	. . . . . . . 8 ⊢ ((𝑝 ∈ 𝑃 ∧ 𝑀 ∈ 𝑃) → (𝑝(dist‘𝐸)𝑀) = (√‘((((𝑝‘0) − (𝑀‘0))↑2) + (((𝑝‘1) − (𝑀‘1))↑2))))
55	45, 54	syl 18	. . . . . . 7 ⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → (𝑝(dist‘𝐸)𝑀) = (√‘((((𝑝‘0) − (𝑀‘0))↑2) + (((𝑝‘1) − (𝑀‘1))↑2))))
56	55	eqcomd 2769	. . . . . 6 ⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → (√‘((((𝑝‘0) − (𝑀‘0))↑2) + (((𝑝‘1) − (𝑀‘1))↑2))) = (𝑝(dist‘𝐸)𝑀))
57	56	eqeq1d 2765	. . . . 5 ⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → ((√‘((((𝑝‘0) − (𝑀‘0))↑2) + (((𝑝‘1) − (𝑀‘1))↑2))) = 𝑅 ↔ (𝑝(dist‘𝐸)𝑀) = 𝑅))
58	19, 44, 57	3bitr3d 312	. . . 4 ⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → (((((𝑝‘0) − (𝑀‘0))↑2) + (((𝑝‘1) − (𝑀‘1))↑2)) = (𝑅↑2) ↔ (𝑝(dist‘𝐸)𝑀) = 𝑅))
59	58	rabbidva 3422	. . 3 ⊢ ((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) → {𝑝 ∈ 𝑃 ∣ ((((𝑝‘0) − (𝑀‘0))↑2) + (((𝑝‘1) − (𝑀‘1))↑2)) = (𝑅↑2)} = {𝑝 ∈ 𝑃 ∣ (𝑝(dist‘𝐸)𝑀) = 𝑅})
60	14, 59	eqtr2id 2811	. 2 ⊢ ((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) → {𝑝 ∈ 𝑃 ∣ (𝑝(dist‘𝐸)𝑀) = 𝑅} = 𝐶)
61	13, 60	eqtrd 2798	1 ⊢ ((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) → (𝑀𝑆𝑅) = 𝐶)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2147 {crab 3416 class class class wbr 5106 ‘cfv 6558 (class class class)co 7443 ↑_m cmap 8875 Fincfn 9001 ℝcr 11226 0cc0 11227 1c1 11228 + caddc 11230 +∞cpnf 11367 ≤ cle 11371 − cmin 11568 2c2 12424 ℕ₀cn0 12633 [,)cico 13505 ..^cfzo 13815 ↑cexp 14231 √csqrt 15429 distcds 17466 ℝ^crrx 25734 𝔼_hilcehl 25735 Spherecsph 50046

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7775 ax-inf2 9669 ax-cnex 11283 ax-resscn 11284 ax-1cn 11285 ax-icn 11286 ax-addcl 11287 ax-addrcl 11288 ax-mulcl 11289 ax-mulrcl 11290 ax-mulcom 11291 ax-addass 11292 ax-mulass 11293 ax-distr 11294 ax-i2m1 11295 ax-1ne0 11296 ax-1rid 11297 ax-rnegex 11298 ax-rrecex 11299 ax-cnre 11300 ax-pre-lttri 11301 ax-pre-lttrn 11302 ax-pre-ltadd 11303 ax-pre-mulgt0 11304 ax-pre-sup 11305 ax-addf 11306 ax-mulf 11307

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6322 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-isom 6567 df-riota 7400 df-ov 7446 df-oprab 7447 df-mpo 7448 df-of 7717 df-om 7902 df-1st 8025 df-2nd 8026 df-supp 8205 df-tpos 8271 df-frecs 8327 df-wrecs 8358 df-recs 8407 df-rdg 8446 df-1o 8504 df-2o 8505 df-er 8745 df-map 8877 df-ixp 8954 df-en 9002 df-dom 9003 df-sdom 9004 df-fin 9005 df-fsupp 9382 df-sup 9461 df-oi 9531 df-card 10047 df-pnf 11372 df-mnf 11373 df-xr 11374 df-ltxr 11375 df-le 11376 df-sub 11570 df-neg 11571 df-div 12001 df-nn 12363 df-2 12432 df-3 12433 df-4 12434 df-5 12435 df-6 12436 df-7 12437 df-8 12438 df-9 12439 df-n0 12634 df-z 12721 df-dec 12842 df-uz 12993 df-rp 13148 df-xneg 13268 df-xadd 13269 df-xmul 13270 df-ico 13509 df-icc 13510 df-fz 13667 df-fzo 13816 df-seq 14172 df-exp 14232 df-hash 14502 df-cj 15295 df-re 15296 df-im 15297 df-sqrt 15431 df-abs 15432 df-clim 15684 df-sum 15883 df-struct 17354 df-sets 17371 df-slot 17389 df-ndx 17401 df-base 17417 df-ress 17438 df-plusg 17470 df-mulr 17471 df-starv 17472 df-sca 17473 df-vsca 17474 df-ip 17475 df-tset 17476 df-ple 17477 df-ds 17479 df-unif 17480 df-hom 17481 df-cco 17482 df-0g 17641 df-gsum 17642 df-prds 17647 df-pws 17649 df-mgm 18845 df-sgrp 18937 df-mnd 18953 df-mhm 19007 df-grp 19176 df-minusg 19177 df-sbg 19178 df-subg 19362 df-ghm 19457 df-cntz 19561 df-cmn 20026 df-abl 20027 df-mgp 20391 df-rng 20405 df-ur 20438 df-ring 20491 df-cring 20492 df-oppr 20597 df-dvdsr 20617 df-unit 20618 df-invr 20648 df-dvr 20661 df-rhm 20732 df-subrng 20828 df-subrg 20852 df-drng 21012 df-field 21013 df-staf 21126 df-srng 21127 df-lmod 21167 df-lss 21237 df-sra 21478 df-rgmod 21479 df-xmet 21701 df-met 21702 df-cnfld 21709 df-refld 21941 df-dsmm 22068 df-frlm 22083 df-nm 24931 df-tng 24933 df-tcph 25520 df-rrx 25736 df-ehl 25737 df-sph 50048

This theorem is used by: 2sphere0 50067

W3C validator