itscnhlinecirc02p

Description: Intersection of a nonhorizontal line with a circle: A nonhorizontal line passing through a point within a circle around the origin intersects the circle at exactly two different points. (Contributed by AV, 28-Jan-2023)

	Ref	Expression
Hypotheses	itscnhlinecirc02p.i	$⊢ I = (0 ..^2)$
	itscnhlinecirc02p.e	$⊢ E = I$
	itscnhlinecirc02p.p	$⊢ P = ℝ^{I}$
	itscnhlinecirc02p.s	$⊢ S = Sphere (E)$
	itscnhlinecirc02p.0	$⊢ \underset{˙}{0} = I \times \{0\}$
	itscnhlinecirc02p.l	$⊢ L = {Line}_{M} (E)$
	itscnhlinecirc02p.d	$⊢ D = dist (E)$
Assertion	itscnhlinecirc02p	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to \exists! s \in 𝒫 ℝ (\|s\| = 2 \land \forall y \in s \exists! x \in ℝ (⟨“ x y ”⟩ \in (\underset{˙}{0} S R) \land ⟨“ x y ”⟩ \in (X L Y)))$

Proof

Step	Hyp	Ref	Expression
1		itscnhlinecirc02p.i	$⊢ I = (0 ..^2)$
2		itscnhlinecirc02p.e	$⊢ E = I$
3		itscnhlinecirc02p.p	$⊢ P = ℝ^{I}$
4		itscnhlinecirc02p.s	$⊢ S = Sphere (E)$
5		itscnhlinecirc02p.0	$⊢ \underset{˙}{0} = I \times \{0\}$
6		itscnhlinecirc02p.l	$⊢ L = {Line}_{M} (E)$
7		itscnhlinecirc02p.d	$⊢ D = dist (E)$
8	1 2 3 4 5 6 7	itscnhlinecirc02plem3	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to 0 < {(- 2 (Y (0) - X (0)) (X (1) Y (0) - X (0) Y (1)))}^{2} - 4 ({(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) ({(X (1) Y (0) - X (0) Y (1))}^{2} - {(X (1) - Y (1))}^{2} R^{2})$
9	1 3	rrx2pyel	$⊢ X \in P \to X (1) \in ℝ$
10	9	3ad2ant1	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to X (1) \in ℝ$
11	10	adantr	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to X (1) \in ℝ$
12	1 3	rrx2pyel	$⊢ Y \in P \to Y (1) \in ℝ$
13	12	3ad2ant2	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to Y (1) \in ℝ$
14	13	adantr	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to Y (1) \in ℝ$
15	11 14	resubcld	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to X (1) - Y (1) \in ℝ$
16	15	resqcld	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to {(X (1) - Y (1))}^{2} \in ℝ$
17	1 3	rrx2pxel	$⊢ Y \in P \to Y (0) \in ℝ$
18	17	3ad2ant2	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to Y (0) \in ℝ$
19	18	adantr	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to Y (0) \in ℝ$
20	1 3	rrx2pxel	$⊢ X \in P \to X (0) \in ℝ$
21	20	3ad2ant1	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to X (0) \in ℝ$
22	21	adantr	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to X (0) \in ℝ$
23	19 22	resubcld	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to Y (0) - X (0) \in ℝ$
24	23	resqcld	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to {(Y (0) - X (0))}^{2} \in ℝ$
25	16 24	readdcld	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to {(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2} \in ℝ$
26	10 13	resubcld	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to X (1) - Y (1) \in ℝ$
27	26	resqcld	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to {(X (1) - Y (1))}^{2} \in ℝ$
28	18 21	resubcld	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to Y (0) - X (0) \in ℝ$
29	28	resqcld	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to {(Y (0) - X (0))}^{2} \in ℝ$
30	10	recnd	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to X (1) \in ℂ$
31	13	recnd	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to Y (1) \in ℂ$
32		simp3	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to X (1) \neq Y (1)$
33	30 31 32	subne0d	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to X (1) - Y (1) \neq 0$
34	26 33	sqgt0d	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to 0 < {(X (1) - Y (1))}^{2}$
35	28	sqge0d	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to 0 \leq {(Y (0) - X (0))}^{2}$
36	27 29 34 35	addgtge0d	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to 0 < {(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}$
37	36	gt0ne0d	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to {(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2} \neq 0$
38	37	adantr	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to {(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2} \neq 0$
39		2re	$⊢ 2 \in ℝ$
40	39	a1i	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to 2 \in ℝ$
41	11 19	remulcld	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to X (1) Y (0) \in ℝ$
42	22 14	remulcld	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to X (0) Y (1) \in ℝ$
43	41 42	resubcld	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to X (1) Y (0) - X (0) Y (1) \in ℝ$
44	23 43	remulcld	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to (Y (0) - X (0)) (X (1) Y (0) - X (0) Y (1)) \in ℝ$
45	40 44	remulcld	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to 2 (Y (0) - X (0)) (X (1) Y (0) - X (0) Y (1)) \in ℝ$
46	45	renegcld	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to - 2 (Y (0) - X (0)) (X (1) Y (0) - X (0) Y (1)) \in ℝ$
47	43	resqcld	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to {(X (1) Y (0) - X (0) Y (1))}^{2} \in ℝ$
48		rpre	$⊢ R \in ℝ^{+} \to R \in ℝ$
49	48	ad2antrl	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to R \in ℝ$
50	49	resqcld	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to R^{2} \in ℝ$
51	16 50	remulcld	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to {(X (1) - Y (1))}^{2} R^{2} \in ℝ$
52	47 51	resubcld	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to {(X (1) Y (0) - X (0) Y (1))}^{2} - {(X (1) - Y (1))}^{2} R^{2} \in ℝ$
53		eqidd	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to {(- 2 (Y (0) - X (0)) (X (1) Y (0) - X (0) Y (1)))}^{2} - 4 ({(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) ({(X (1) Y (0) - X (0) Y (1))}^{2} - {(X (1) - Y (1))}^{2} R^{2}) = {(- 2 (Y (0) - X (0)) (X (1) Y (0) - X (0) Y (1)))}^{2} - 4 ({(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) ({(X (1) Y (0) - X (0) Y (1))}^{2} - {(X (1) - Y (1))}^{2} R^{2})$
54	25 38 46 52 53	requad2	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to (\exists! s \in 𝒫 ℝ (\|s\| = 2 \land \forall y \in s ({(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) y^{2} + (- 2 (Y (0) - X (0)) (X (1) Y (0) - X (0) Y (1))) y + ({(X (1) Y (0) - X (0) Y (1))}^{2} - {(X (1) - Y (1))}^{2} R^{2}) = 0) \leftrightarrow 0 < {(- 2 (Y (0) - X (0)) (X (1) Y (0) - X (0) Y (1)))}^{2} - 4 ({(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) ({(X (1) Y (0) - X (0) Y (1))}^{2} - {(X (1) - Y (1))}^{2} R^{2}))$
55	8 54	mpbird	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to \exists! s \in 𝒫 ℝ (\|s\| = 2 \land \forall y \in s ({(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) y^{2} + (- 2 (Y (0) - X (0)) (X (1) Y (0) - X (0) Y (1))) y + ({(X (1) Y (0) - X (0) Y (1))}^{2} - {(X (1) - Y (1))}^{2} R^{2}) = 0)$
56		0xr	$⊢ 0 \in ℝ^{*}$
57	56	a1i	$⊢ R \in ℝ^{+} \to 0 \in ℝ^{*}$
58		pnfxr	$⊢ +∞ \in ℝ^{*}$
59	58	a1i	$⊢ R \in ℝ^{+} \to +∞ \in ℝ^{*}$
60		rpxr	$⊢ R \in ℝ^{+} \to R \in ℝ^{*}$
61		rpge0	$⊢ R \in ℝ^{+} \to 0 \leq R$
62	48	ltpnfd	$⊢ R \in ℝ^{+} \to R < +∞$
63	57 59 60 61 62	elicod	$⊢ R \in ℝ^{+} \to R \in [0, +∞)$
64		eqid	$⊢ \{p \in P \| {p (0)}^{2} + {p (1)}^{2} = R^{2}\} = \{p \in P \| {p (0)}^{2} + {p (1)}^{2} = R^{2}\}$
65	1 2 3 4 5 64	2sphere0	$⊢ R \in [0, +∞) \to \underset{˙}{0} S R = \{p \in P \| {p (0)}^{2} + {p (1)}^{2} = R^{2}\}$
66	63 65	syl	$⊢ R \in ℝ^{+} \to \underset{˙}{0} S R = \{p \in P \| {p (0)}^{2} + {p (1)}^{2} = R^{2}\}$
67	66	ad2antrl	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to \underset{˙}{0} S R = \{p \in P \| {p (0)}^{2} + {p (1)}^{2} = R^{2}\}$
68	67	ad2antrr	$⊢ ((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \to \underset{˙}{0} S R = \{p \in P \| {p (0)}^{2} + {p (1)}^{2} = R^{2}\}$
69	68	ad2antrr	$⊢ ((((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \land x \in ℝ) \to \underset{˙}{0} S R = \{p \in P \| {p (0)}^{2} + {p (1)}^{2} = R^{2}\}$
70	69	eleq2d	$⊢ ((((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \land x \in ℝ) \to (⟨“ x y ”⟩ \in (\underset{˙}{0} S R) \leftrightarrow ⟨“ x y ”⟩ \in \{p \in P \| {p (0)}^{2} + {p (1)}^{2} = R^{2}\})$
71		fveq1	$⊢ p = ⟨“ x y ”⟩ \to p (0) = ⟨“ x y ”⟩ (0)$
72	71	oveq1d	$⊢ p = ⟨“ x y ”⟩ \to {p (0)}^{2} = {⟨“ x y ”⟩ (0)}^{2}$
73		fveq1	$⊢ p = ⟨“ x y ”⟩ \to p (1) = ⟨“ x y ”⟩ (1)$
74	73	oveq1d	$⊢ p = ⟨“ x y ”⟩ \to {p (1)}^{2} = {⟨“ x y ”⟩ (1)}^{2}$
75	72 74	oveq12d	$⊢ p = ⟨“ x y ”⟩ \to {p (0)}^{2} + {p (1)}^{2} = {⟨“ x y ”⟩ (0)}^{2} + {⟨“ x y ”⟩ (1)}^{2}$
76	75	eqeq1d	$⊢ p = ⟨“ x y ”⟩ \to ({p (0)}^{2} + {p (1)}^{2} = R^{2} \leftrightarrow {⟨“ x y ”⟩ (0)}^{2} + {⟨“ x y ”⟩ (1)}^{2} = R^{2})$
77	76	elrab	$⊢ ⟨“ x y ”⟩ \in \{p \in P \| {p (0)}^{2} + {p (1)}^{2} = R^{2}\} \leftrightarrow (⟨“ x y ”⟩ \in P \land {⟨“ x y ”⟩ (0)}^{2} + {⟨“ x y ”⟩ (1)}^{2} = R^{2})$
78	77	a1i	$⊢ ((((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \land x \in ℝ) \to (⟨“ x y ”⟩ \in \{p \in P \| {p (0)}^{2} + {p (1)}^{2} = R^{2}\} \leftrightarrow (⟨“ x y ”⟩ \in P \land {⟨“ x y ”⟩ (0)}^{2} + {⟨“ x y ”⟩ (1)}^{2} = R^{2}))$
79		simpr	$⊢ ((((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \land x \in ℝ) \to x \in ℝ$
80		elpwi	$⊢ s \in 𝒫 ℝ \to s \subseteq ℝ$
81	80	ad4antlr	$⊢ ((((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \land x \in ℝ) \to s \subseteq ℝ$
82		simplr	$⊢ ((((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \land x \in ℝ) \to y \in s$
83	81 82	sseldd	$⊢ ((((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \land x \in ℝ) \to y \in ℝ$
84		s2fv0	$⊢ x \in ℝ \to ⟨“ x y ”⟩ (0) = x$
85	84	oveq1d	$⊢ x \in ℝ \to {⟨“ x y ”⟩ (0)}^{2} = x^{2}$
86		s2fv1	$⊢ y \in ℝ \to ⟨“ x y ”⟩ (1) = y$
87	86	oveq1d	$⊢ y \in ℝ \to {⟨“ x y ”⟩ (1)}^{2} = y^{2}$
88	85 87	oveqan12d	$⊢ (x \in ℝ \land y \in ℝ) \to {⟨“ x y ”⟩ (0)}^{2} + {⟨“ x y ”⟩ (1)}^{2} = x^{2} + y^{2}$
89	88	eqeq1d	$⊢ (x \in ℝ \land y \in ℝ) \to ({⟨“ x y ”⟩ (0)}^{2} + {⟨“ x y ”⟩ (1)}^{2} = R^{2} \leftrightarrow x^{2} + y^{2} = R^{2})$
90	89	anbi2d	$⊢ (x \in ℝ \land y \in ℝ) \to ((⟨“ x y ”⟩ \in P \land {⟨“ x y ”⟩ (0)}^{2} + {⟨“ x y ”⟩ (1)}^{2} = R^{2}) \leftrightarrow (⟨“ x y ”⟩ \in P \land x^{2} + y^{2} = R^{2}))$
91	79 83 90	syl2anc	$⊢ ((((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \land x \in ℝ) \to ((⟨“ x y ”⟩ \in P \land {⟨“ x y ”⟩ (0)}^{2} + {⟨“ x y ”⟩ (1)}^{2} = R^{2}) \leftrightarrow (⟨“ x y ”⟩ \in P \land x^{2} + y^{2} = R^{2}))$
92	70 78 91	3bitrd	$⊢ ((((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \land x \in ℝ) \to (⟨“ x y ”⟩ \in (\underset{˙}{0} S R) \leftrightarrow (⟨“ x y ”⟩ \in P \land x^{2} + y^{2} = R^{2}))$
93		simp1	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to X \in P$
94		simp2	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to Y \in P$
95		fveq1	$⊢ X = Y \to X (1) = Y (1)$
96	95	a1i	$⊢ (X \in P \land Y \in P) \to (X = Y \to X (1) = Y (1))$
97	96	necon3d	$⊢ (X \in P \land Y \in P) \to (X (1) \neq Y (1) \to X \neq Y)$
98	97	3impia	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to X \neq Y$
99	93 94 98	3jca	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to (X \in P \land Y \in P \land X \neq Y)$
100	99	ad3antrrr	$⊢ ((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \to (X \in P \land Y \in P \land X \neq Y)$
101	100	ad2antrr	$⊢ ((((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \land x \in ℝ) \to (X \in P \land Y \in P \land X \neq Y)$
102		eqid	$⊢ X (1) - Y (1) = X (1) - Y (1)$
103		eqid	$⊢ Y (0) - X (0) = Y (0) - X (0)$
104		eqid	$⊢ X (1) Y (0) - X (0) Y (1) = X (1) Y (0) - X (0) Y (1)$
105	1 2 3 6 102 103 104	rrx2linest2	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X L Y = \{p \in P \| (X (1) - Y (1)) p (0) + (Y (0) - X (0)) p (1) = X (1) Y (0) - X (0) Y (1)\}$
106	101 105	syl	$⊢ ((((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \land x \in ℝ) \to X L Y = \{p \in P \| (X (1) - Y (1)) p (0) + (Y (0) - X (0)) p (1) = X (1) Y (0) - X (0) Y (1)\}$
107	106	eleq2d	$⊢ ((((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \land x \in ℝ) \to (⟨“ x y ”⟩ \in (X L Y) \leftrightarrow ⟨“ x y ”⟩ \in \{p \in P \| (X (1) - Y (1)) p (0) + (Y (0) - X (0)) p (1) = X (1) Y (0) - X (0) Y (1)\})$
108	71	oveq2d	$⊢ p = ⟨“ x y ”⟩ \to (X (1) - Y (1)) p (0) = (X (1) - Y (1)) ⟨“ x y ”⟩ (0)$
109	73	oveq2d	$⊢ p = ⟨“ x y ”⟩ \to (Y (0) - X (0)) p (1) = (Y (0) - X (0)) ⟨“ x y ”⟩ (1)$
110	108 109	oveq12d	$⊢ p = ⟨“ x y ”⟩ \to (X (1) - Y (1)) p (0) + (Y (0) - X (0)) p (1) = (X (1) - Y (1)) ⟨“ x y ”⟩ (0) + (Y (0) - X (0)) ⟨“ x y ”⟩ (1)$
111	110	eqeq1d	$⊢ p = ⟨“ x y ”⟩ \to ((X (1) - Y (1)) p (0) + (Y (0) - X (0)) p (1) = X (1) Y (0) - X (0) Y (1) \leftrightarrow (X (1) - Y (1)) ⟨“ x y ”⟩ (0) + (Y (0) - X (0)) ⟨“ x y ”⟩ (1) = X (1) Y (0) - X (0) Y (1))$
112	111	elrab	$⊢ ⟨“ x y ”⟩ \in \{p \in P \| (X (1) - Y (1)) p (0) + (Y (0) - X (0)) p (1) = X (1) Y (0) - X (0) Y (1)\} \leftrightarrow (⟨“ x y ”⟩ \in P \land (X (1) - Y (1)) ⟨“ x y ”⟩ (0) + (Y (0) - X (0)) ⟨“ x y ”⟩ (1) = X (1) Y (0) - X (0) Y (1))$
113	84	oveq2d	$⊢ x \in ℝ \to (X (1) - Y (1)) ⟨“ x y ”⟩ (0) = (X (1) - Y (1)) x$
114	86	oveq2d	$⊢ y \in ℝ \to (Y (0) - X (0)) ⟨“ x y ”⟩ (1) = (Y (0) - X (0)) y$
115	113 114	oveqan12d	$⊢ (x \in ℝ \land y \in ℝ) \to (X (1) - Y (1)) ⟨“ x y ”⟩ (0) + (Y (0) - X (0)) ⟨“ x y ”⟩ (1) = (X (1) - Y (1)) x + (Y (0) - X (0)) y$
116	115	eqeq1d	$⊢ (x \in ℝ \land y \in ℝ) \to ((X (1) - Y (1)) ⟨“ x y ”⟩ (0) + (Y (0) - X (0)) ⟨“ x y ”⟩ (1) = X (1) Y (0) - X (0) Y (1) \leftrightarrow (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1))$
117	116	anbi2d	$⊢ (x \in ℝ \land y \in ℝ) \to ((⟨“ x y ”⟩ \in P \land (X (1) - Y (1)) ⟨“ x y ”⟩ (0) + (Y (0) - X (0)) ⟨“ x y ”⟩ (1) = X (1) Y (0) - X (0) Y (1)) \leftrightarrow (⟨“ x y ”⟩ \in P \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1)))$
118	112 117	bitrid	$⊢ (x \in ℝ \land y \in ℝ) \to (⟨“ x y ”⟩ \in \{p \in P \| (X (1) - Y (1)) p (0) + (Y (0) - X (0)) p (1) = X (1) Y (0) - X (0) Y (1)\} \leftrightarrow (⟨“ x y ”⟩ \in P \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1)))$
119	79 83 118	syl2anc	$⊢ ((((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \land x \in ℝ) \to (⟨“ x y ”⟩ \in \{p \in P \| (X (1) - Y (1)) p (0) + (Y (0) - X (0)) p (1) = X (1) Y (0) - X (0) Y (1)\} \leftrightarrow (⟨“ x y ”⟩ \in P \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1)))$
120	107 119	bitrd	$⊢ ((((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \land x \in ℝ) \to (⟨“ x y ”⟩ \in (X L Y) \leftrightarrow (⟨“ x y ”⟩ \in P \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1)))$
121	92 120	anbi12d	$⊢ ((((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \land x \in ℝ) \to ((⟨“ x y ”⟩ \in (\underset{˙}{0} S R) \land ⟨“ x y ”⟩ \in (X L Y)) \leftrightarrow ((⟨“ x y ”⟩ \in P \land x^{2} + y^{2} = R^{2}) \land (⟨“ x y ”⟩ \in P \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1))))$
122	121	reubidva	$⊢ (((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \to (\exists! x \in ℝ (⟨“ x y ”⟩ \in (\underset{˙}{0} S R) \land ⟨“ x y ”⟩ \in (X L Y)) \leftrightarrow \exists! x \in ℝ ((⟨“ x y ”⟩ \in P \land x^{2} + y^{2} = R^{2}) \land (⟨“ x y ”⟩ \in P \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1))))$
123		elelpwi	$⊢ (y \in s \land s \in 𝒫 ℝ) \to y \in ℝ$
124	1 3	prelrrx2	$⊢ (x \in ℝ \land y \in ℝ) \to ⟨“ x y ”⟩ \in P$
125	124	ancoms	$⊢ (y \in ℝ \land x \in ℝ) \to ⟨“ x y ”⟩ \in P$
126	125	biantrurd	$⊢ (y \in ℝ \land x \in ℝ) \to (x^{2} + y^{2} = R^{2} \leftrightarrow (⟨“ x y ”⟩ \in P \land x^{2} + y^{2} = R^{2}))$
127	126	bicomd	$⊢ (y \in ℝ \land x \in ℝ) \to ((⟨“ x y ”⟩ \in P \land x^{2} + y^{2} = R^{2}) \leftrightarrow x^{2} + y^{2} = R^{2})$
128	125	biantrurd	$⊢ (y \in ℝ \land x \in ℝ) \to ((X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1) \leftrightarrow (⟨“ x y ”⟩ \in P \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1)))$
129	128	bicomd	$⊢ (y \in ℝ \land x \in ℝ) \to ((⟨“ x y ”⟩ \in P \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1)) \leftrightarrow (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1))$
130	127 129	anbi12d	$⊢ (y \in ℝ \land x \in ℝ) \to (((⟨“ x y ”⟩ \in P \land x^{2} + y^{2} = R^{2}) \land (⟨“ x y ”⟩ \in P \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1))) \leftrightarrow (x^{2} + y^{2} = R^{2} \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1)))$
131	130	reubidva	$⊢ y \in ℝ \to (\exists! x \in ℝ ((⟨“ x y ”⟩ \in P \land x^{2} + y^{2} = R^{2}) \land (⟨“ x y ”⟩ \in P \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1))) \leftrightarrow \exists! x \in ℝ (x^{2} + y^{2} = R^{2} \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1)))$
132	123 131	syl	$⊢ (y \in s \land s \in 𝒫 ℝ) \to (\exists! x \in ℝ ((⟨“ x y ”⟩ \in P \land x^{2} + y^{2} = R^{2}) \land (⟨“ x y ”⟩ \in P \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1))) \leftrightarrow \exists! x \in ℝ (x^{2} + y^{2} = R^{2} \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1)))$
133	132	expcom	$⊢ s \in 𝒫 ℝ \to (y \in s \to (\exists! x \in ℝ ((⟨“ x y ”⟩ \in P \land x^{2} + y^{2} = R^{2}) \land (⟨“ x y ”⟩ \in P \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1))) \leftrightarrow \exists! x \in ℝ (x^{2} + y^{2} = R^{2} \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1))))$
134	133	ad2antlr	$⊢ ((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \to (y \in s \to (\exists! x \in ℝ ((⟨“ x y ”⟩ \in P \land x^{2} + y^{2} = R^{2}) \land (⟨“ x y ”⟩ \in P \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1))) \leftrightarrow \exists! x \in ℝ (x^{2} + y^{2} = R^{2} \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1))))$
135	134	imp	$⊢ (((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \to (\exists! x \in ℝ ((⟨“ x y ”⟩ \in P \land x^{2} + y^{2} = R^{2}) \land (⟨“ x y ”⟩ \in P \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1))) \leftrightarrow \exists! x \in ℝ (x^{2} + y^{2} = R^{2} \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1)))$
136	26 33	jca	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to (X (1) - Y (1) \in ℝ \land X (1) - Y (1) \neq 0)$
137	136	adantr	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to (X (1) - Y (1) \in ℝ \land X (1) - Y (1) \neq 0)$
138	137	ad3antrrr	$⊢ (((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \to (X (1) - Y (1) \in ℝ \land X (1) - Y (1) \neq 0)$
139	19	ad3antrrr	$⊢ (((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \to Y (0) \in ℝ$
140	22	ad3antrrr	$⊢ (((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \to X (0) \in ℝ$
141	139 140	resubcld	$⊢ (((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \to Y (0) - X (0) \in ℝ$
142	11	ad3antrrr	$⊢ (((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \to X (1) \in ℝ$
143	142 139	remulcld	$⊢ (((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \to X (1) Y (0) \in ℝ$
144	14	ad3antrrr	$⊢ (((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \to Y (1) \in ℝ$
145	140 144	remulcld	$⊢ (((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \to X (0) Y (1) \in ℝ$
146	143 145	resubcld	$⊢ (((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \to X (1) Y (0) - X (0) Y (1) \in ℝ$
147		simplrl	$⊢ (((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \to R \in ℝ^{+}$
148	147	ad2antrr	$⊢ (((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \to R \in ℝ^{+}$
149	123	expcom	$⊢ s \in 𝒫 ℝ \to (y \in s \to y \in ℝ)$
150	149	ad2antlr	$⊢ ((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \to (y \in s \to y \in ℝ)$
151	150	imp	$⊢ (((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \to y \in ℝ$
152		eqid	$⊢ {(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2} = {(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}$
153		eqid	$⊢ - 2 (Y (0) - X (0)) (X (1) Y (0) - X (0) Y (1)) = - 2 (Y (0) - X (0)) (X (1) Y (0) - X (0) Y (1))$
154		eqid	$⊢ {(X (1) Y (0) - X (0) Y (1))}^{2} - {(X (1) - Y (1))}^{2} R^{2} = {(X (1) Y (0) - X (0) Y (1))}^{2} - {(X (1) - Y (1))}^{2} R^{2}$
155	152 153 154	itsclquadeu	$⊢ (((X (1) - Y (1) \in ℝ \land X (1) - Y (1) \neq 0) \land Y (0) - X (0) \in ℝ \land X (1) Y (0) - X (0) Y (1) \in ℝ) \land R \in ℝ^{+} \land y \in ℝ) \to (\exists! x \in ℝ (x^{2} + y^{2} = R^{2} \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1)) \leftrightarrow ({(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) y^{2} + (- 2 (Y (0) - X (0)) (X (1) Y (0) - X (0) Y (1))) y + ({(X (1) Y (0) - X (0) Y (1))}^{2} - {(X (1) - Y (1))}^{2} R^{2}) = 0)$
156	138 141 146 148 151 155	syl311anc	$⊢ (((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \to (\exists! x \in ℝ (x^{2} + y^{2} = R^{2} \land (X (1) - Y (1)) x + (Y (0) - X (0)) y = X (1) Y (0) - X (0) Y (1)) \leftrightarrow ({(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) y^{2} + (- 2 (Y (0) - X (0)) (X (1) Y (0) - X (0) Y (1))) y + ({(X (1) Y (0) - X (0) Y (1))}^{2} - {(X (1) - Y (1))}^{2} R^{2}) = 0)$
157	122 135 156	3bitrd	$⊢ (((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \land y \in s) \to (\exists! x \in ℝ (⟨“ x y ”⟩ \in (\underset{˙}{0} S R) \land ⟨“ x y ”⟩ \in (X L Y)) \leftrightarrow ({(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) y^{2} + (- 2 (Y (0) - X (0)) (X (1) Y (0) - X (0) Y (1))) y + ({(X (1) Y (0) - X (0) Y (1))}^{2} - {(X (1) - Y (1))}^{2} R^{2}) = 0)$
158	157	ralbidva	$⊢ ((((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \land \|s\| = 2) \to (\forall y \in s \exists! x \in ℝ (⟨“ x y ”⟩ \in (\underset{˙}{0} S R) \land ⟨“ x y ”⟩ \in (X L Y)) \leftrightarrow \forall y \in s ({(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) y^{2} + (- 2 (Y (0) - X (0)) (X (1) Y (0) - X (0) Y (1))) y + ({(X (1) Y (0) - X (0) Y (1))}^{2} - {(X (1) - Y (1))}^{2} R^{2}) = 0)$
159	158	pm5.32da	$⊢ (((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \land s \in 𝒫 ℝ) \to ((\|s\| = 2 \land \forall y \in s \exists! x \in ℝ (⟨“ x y ”⟩ \in (\underset{˙}{0} S R) \land ⟨“ x y ”⟩ \in (X L Y))) \leftrightarrow (\|s\| = 2 \land \forall y \in s ({(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) y^{2} + (- 2 (Y (0) - X (0)) (X (1) Y (0) - X (0) Y (1))) y + ({(X (1) Y (0) - X (0) Y (1))}^{2} - {(X (1) - Y (1))}^{2} R^{2}) = 0))$
160	159	reubidva	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to (\exists! s \in 𝒫 ℝ (\|s\| = 2 \land \forall y \in s \exists! x \in ℝ (⟨“ x y ”⟩ \in (\underset{˙}{0} S R) \land ⟨“ x y ”⟩ \in (X L Y))) \leftrightarrow \exists! s \in 𝒫 ℝ (\|s\| = 2 \land \forall y \in s ({(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) y^{2} + (- 2 (Y (0) - X (0)) (X (1) Y (0) - X (0) Y (1))) y + ({(X (1) Y (0) - X (0) Y (1))}^{2} - {(X (1) - Y (1))}^{2} R^{2}) = 0))$
161	55 160	mpbird	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to \exists! s \in 𝒫 ℝ (\|s\| = 2 \land \forall y \in s \exists! x \in ℝ (⟨“ x y ”⟩ \in (\underset{˙}{0} S R) \land ⟨“ x y ”⟩ \in (X L Y)))$

Metamath Proof Explorer

Theorem itscnhlinecirc02p

Proof