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

Metamath Proof Explorer

Theorem 2sphere

Proof