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 = \{1, 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)$
	itscnhlinecirc02p.z	$⊢ Z = \{⟨1, x⟩, ⟨2, y⟩\}$
Assertion	itscnhlinecirc02p	$⊢ ((X \in P \land Y \in P \land X (2) \neq Y (2)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to \exists! s \in 𝒫 ℝ (\|s\| = 2 \land \forall y \in s \exists! x \in ℝ (Z \in (\underset{˙}{0} S R) \land Z \in (X L Y)))$

Proof

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

Metamath Proof Explorer

Theorem itscnhlinecirc02p

Proof