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 = I$
	2sphere.p	$⊢ P = ℝ^{I}$
	2sphere.s	$⊢ S = Sphere (E)$
	2sphere.c	$⊢ C = \{p \in P \| {(p (1) - M (1))}^{2} + {(p (2) - M (2))}^{2} = R^{2}\}$
Assertion	2sphere	$⊢ (M \in P \land R \in [0, +∞)) \to M S R = C$

Proof

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

Metamath Proof Explorer

Theorem 2sphere

Proof