itsclinecirc0

Description: The intersection points of a line through two different points Y and Z and a circle around the origin, using the definition of a line in a two dimensional Euclidean space. (Contributed by AV, 25-Feb-2023) (Proof shortened by AV, 16-May-2023)

	Ref	Expression
Hypotheses	itsclc0.i	$⊢ I = \{1, 2\}$
	itsclc0.e	$⊢ E = msup$
	itsclc0.p	$⊢ P = ℝ^{I}$
	itsclc0.s	$⊢ S = Sphere (E)$
	itsclc0.0	$⊢ \underset{˙}{0} = I \times \{0\}$
	itsclc0.q	$⊢ Q = A^{2} + B^{2}$
	itsclc0.d	$⊢ D = R^{2} Q - C^{2}$
	itsclinecirc0.l	$⊢ L = {Line}_{M} (E)$
	itsclinecirc0.a	$⊢ A = Y (2) - Z (2)$
	itsclinecirc0.b	$⊢ B = Z (1) - Y (1)$
	itsclinecirc0.c	$⊢ C = Y (2) Z (1) - Y (1) Z (2)$
Assertion	itsclinecirc0	$⊢ ((Y \in P \land Z \in P \land Y \neq Z) \land (R \in ℝ^{+} \land 0 \leq D)) \to ((X \in (\underset{˙}{0} S R) \land X \in (Y L Z)) \to ((X (1) = \frac{A C + B \sqrt{D}}{Q} \land X (2) = \frac{B C - A \sqrt{D}}{Q}) \lor (X (1) = \frac{A C - B \sqrt{D}}{Q} \land X (2) = \frac{B C + A \sqrt{D}}{Q})))$

Proof

Step	Hyp	Ref	Expression
1		itsclc0.i	$⊢ I = \{1, 2\}$
2		itsclc0.e	$⊢ E = msup$
3		itsclc0.p	$⊢ P = ℝ^{I}$
4		itsclc0.s	$⊢ S = Sphere (E)$
5		itsclc0.0	$⊢ \underset{˙}{0} = I \times \{0\}$
6		itsclc0.q	$⊢ Q = A^{2} + B^{2}$
7		itsclc0.d	$⊢ D = R^{2} Q - C^{2}$
8		itsclinecirc0.l	$⊢ L = {Line}_{M} (E)$
9		itsclinecirc0.a	$⊢ A = Y (2) - Z (2)$
10		itsclinecirc0.b	$⊢ B = Z (1) - Y (1)$
11		itsclinecirc0.c	$⊢ C = Y (2) Z (1) - Y (1) Z (2)$
12	1 2 3 8 9 10 11	rrx2linest2	$⊢ (Y \in P \land Z \in P \land Y \neq Z) \to Y L Z = \{p \in P \| A p (1) + B p (2) = C\}$
13	12	adantr	$⊢ ((Y \in P \land Z \in P \land Y \neq Z) \land (R \in ℝ^{+} \land 0 \leq D)) \to Y L Z = \{p \in P \| A p (1) + B p (2) = C\}$
14	13	eleq2d	$⊢ ((Y \in P \land Z \in P \land Y \neq Z) \land (R \in ℝ^{+} \land 0 \leq D)) \to (X \in (Y L Z) \leftrightarrow X \in \{p \in P \| A p (1) + B p (2) = C\})$
15	14	anbi2d	$⊢ ((Y \in P \land Z \in P \land Y \neq Z) \land (R \in ℝ^{+} \land 0 \leq D)) \to ((X \in (\underset{˙}{0} S R) \land X \in (Y L Z)) \leftrightarrow (X \in (\underset{˙}{0} S R) \land X \in \{p \in P \| A p (1) + B p (2) = C\}))$
16	1 3	rrx2pyel	$⊢ Y \in P \to Y (2) \in ℝ$
17	16	3ad2ant1	$⊢ (Y \in P \land Z \in P \land Y \neq Z) \to Y (2) \in ℝ$
18	1 3	rrx2pyel	$⊢ Z \in P \to Z (2) \in ℝ$
19	18	3ad2ant2	$⊢ (Y \in P \land Z \in P \land Y \neq Z) \to Z (2) \in ℝ$
20	17 19	resubcld	$⊢ (Y \in P \land Z \in P \land Y \neq Z) \to Y (2) - Z (2) \in ℝ$
21	9 20	eqeltrid	$⊢ (Y \in P \land Z \in P \land Y \neq Z) \to A \in ℝ$
22	21	adantr	$⊢ ((Y \in P \land Z \in P \land Y \neq Z) \land (R \in ℝ^{+} \land 0 \leq D)) \to A \in ℝ$
23	1 3	rrx2pxel	$⊢ Z \in P \to Z (1) \in ℝ$
24	23	3ad2ant2	$⊢ (Y \in P \land Z \in P \land Y \neq Z) \to Z (1) \in ℝ$
25	1 3	rrx2pxel	$⊢ Y \in P \to Y (1) \in ℝ$
26	25	3ad2ant1	$⊢ (Y \in P \land Z \in P \land Y \neq Z) \to Y (1) \in ℝ$
27	24 26	resubcld	$⊢ (Y \in P \land Z \in P \land Y \neq Z) \to Z (1) - Y (1) \in ℝ$
28	10 27	eqeltrid	$⊢ (Y \in P \land Z \in P \land Y \neq Z) \to B \in ℝ$
29	28	adantr	$⊢ ((Y \in P \land Z \in P \land Y \neq Z) \land (R \in ℝ^{+} \land 0 \leq D)) \to B \in ℝ$
30	17 24	remulcld	$⊢ (Y \in P \land Z \in P \land Y \neq Z) \to Y (2) Z (1) \in ℝ$
31	26 19	remulcld	$⊢ (Y \in P \land Z \in P \land Y \neq Z) \to Y (1) Z (2) \in ℝ$
32	30 31	resubcld	$⊢ (Y \in P \land Z \in P \land Y \neq Z) \to Y (2) Z (1) - Y (1) Z (2) \in ℝ$
33	11 32	eqeltrid	$⊢ (Y \in P \land Z \in P \land Y \neq Z) \to C \in ℝ$
34	33	adantr	$⊢ ((Y \in P \land Z \in P \land Y \neq Z) \land (R \in ℝ^{+} \land 0 \leq D)) \to C \in ℝ$
35	1 3 10 9	rrx2pnedifcoorneorr	$⊢ (Y \in P \land Z \in P \land Y \neq Z) \to (B \neq 0 \lor A \neq 0)$
36	35	orcomd	$⊢ (Y \in P \land Z \in P \land Y \neq Z) \to (A \neq 0 \lor B \neq 0)$
37	36	adantr	$⊢ ((Y \in P \land Z \in P \land Y \neq Z) \land (R \in ℝ^{+} \land 0 \leq D)) \to (A \neq 0 \lor B \neq 0)$
38		simpr	$⊢ ((Y \in P \land Z \in P \land Y \neq Z) \land (R \in ℝ^{+} \land 0 \leq D)) \to (R \in ℝ^{+} \land 0 \leq D)$
39		eqid	$⊢ \{p \in P \| A p (1) + B p (2) = C\} = \{p \in P \| A p (1) + B p (2) = C\}$
40	1 2 3 4 5 6 7 39	itsclc0	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to ((X \in (\underset{˙}{0} S R) \land X \in \{p \in P \| A p (1) + B p (2) = C\}) \to ((X (1) = \frac{A C + B \sqrt{D}}{Q} \land X (2) = \frac{B C - A \sqrt{D}}{Q}) \lor (X (1) = \frac{A C - B \sqrt{D}}{Q} \land X (2) = \frac{B C + A \sqrt{D}}{Q})))$
41	22 29 34 37 38 40	syl311anc	$⊢ ((Y \in P \land Z \in P \land Y \neq Z) \land (R \in ℝ^{+} \land 0 \leq D)) \to ((X \in (\underset{˙}{0} S R) \land X \in \{p \in P \| A p (1) + B p (2) = C\}) \to ((X (1) = \frac{A C + B \sqrt{D}}{Q} \land X (2) = \frac{B C - A \sqrt{D}}{Q}) \lor (X (1) = \frac{A C - B \sqrt{D}}{Q} \land X (2) = \frac{B C + A \sqrt{D}}{Q})))$
42	15 41	sylbid	$⊢ ((Y \in P \land Z \in P \land Y \neq Z) \land (R \in ℝ^{+} \land 0 \leq D)) \to ((X \in (\underset{˙}{0} S R) \land X \in (Y L Z)) \to ((X (1) = \frac{A C + B \sqrt{D}}{Q} \land X (2) = \frac{B C - A \sqrt{D}}{Q}) \lor (X (1) = \frac{A C - B \sqrt{D}}{Q} \land X (2) = \frac{B C + A \sqrt{D}}{Q})))$

Metamath Proof Explorer

Theorem itsclinecirc0

Proof