itsclc0b

Description: The intersection points of a (nondegenerate) line through two points and a circle around the origin. (Contributed by AV, 2-May-2023) (Revised by AV, 14-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}$
	itsclc0.l	$⊢ L = \{p \in P \| A p (1) + B p (2) = C\}$
Assertion	itsclc0b	$⊢ ((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 L) \leftrightarrow (X \in P \land ((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		itsclc0.l	$⊢ L = \{p \in P \| A p (1) + B p (2) = C\}$
9		rprege0	$⊢ R \in ℝ^{+} \to (R \in ℝ \land 0 \leq R)$
10		elrege0	$⊢ R \in [0, +∞) \leftrightarrow (R \in ℝ \land 0 \leq R)$
11	9 10	sylibr	$⊢ R \in ℝ^{+} \to R \in [0, +∞)$
12	11	adantr	$⊢ (R \in ℝ^{+} \land 0 \leq D) \to R \in [0, +∞)$
13	12	3ad2ant3	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to R \in [0, +∞)$
14		eqid	$⊢ \{p \in P \| {p (1)}^{2} + {p (2)}^{2} = R^{2}\} = \{p \in P \| {p (1)}^{2} + {p (2)}^{2} = R^{2}\}$
15	1 2 3 4 5 14	2sphere0	$⊢ R \in [0, +∞) \to \underset{˙}{0} S R = \{p \in P \| {p (1)}^{2} + {p (2)}^{2} = R^{2}\}$
16	15	eleq2d	$⊢ R \in [0, +∞) \to (X \in (\underset{˙}{0} S R) \leftrightarrow X \in \{p \in P \| {p (1)}^{2} + {p (2)}^{2} = R^{2}\})$
17	13 16	syl	$⊢ ((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) \leftrightarrow X \in \{p \in P \| {p (1)}^{2} + {p (2)}^{2} = R^{2}\})$
18		fveq1	$⊢ p = X \to p (1) = X (1)$
19	18	oveq2d	$⊢ p = X \to A p (1) = A X (1)$
20		fveq1	$⊢ p = X \to p (2) = X (2)$
21	20	oveq2d	$⊢ p = X \to B p (2) = B X (2)$
22	19 21	oveq12d	$⊢ p = X \to A p (1) + B p (2) = A X (1) + B X (2)$
23	22	eqeq1d	$⊢ p = X \to (A p (1) + B p (2) = C \leftrightarrow A X (1) + B X (2) = C)$
24	23 8	elrab2	$⊢ X \in L \leftrightarrow (X \in P \land A X (1) + B X (2) = C)$
25	24	a1i	$⊢ ((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 L \leftrightarrow (X \in P \land A X (1) + B X (2) = C))$
26	17 25	anbi12d	$⊢ ((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 L) \leftrightarrow (X \in \{p \in P \| {p (1)}^{2} + {p (2)}^{2} = R^{2}\} \land (X \in P \land A X (1) + B X (2) = C)))$
27	18	oveq1d	$⊢ p = X \to {p (1)}^{2} = {X (1)}^{2}$
28	20	oveq1d	$⊢ p = X \to {p (2)}^{2} = {X (2)}^{2}$
29	27 28	oveq12d	$⊢ p = X \to {p (1)}^{2} + {p (2)}^{2} = {X (1)}^{2} + {X (2)}^{2}$
30	29	eqeq1d	$⊢ p = X \to ({p (1)}^{2} + {p (2)}^{2} = R^{2} \leftrightarrow {X (1)}^{2} + {X (2)}^{2} = R^{2})$
31	30	elrab	$⊢ X \in \{p \in P \| {p (1)}^{2} + {p (2)}^{2} = R^{2}\} \leftrightarrow (X \in P \land {X (1)}^{2} + {X (2)}^{2} = R^{2})$
32	31	anbi1i	$⊢ (X \in \{p \in P \| {p (1)}^{2} + {p (2)}^{2} = R^{2}\} \land (X \in P \land A X (1) + B X (2) = C)) \leftrightarrow ((X \in P \land {X (1)}^{2} + {X (2)}^{2} = R^{2}) \land (X \in P \land A X (1) + B X (2) = C))$
33		anandi	$⊢ (X \in P \land ({X (1)}^{2} + {X (2)}^{2} = R^{2} \land A X (1) + B X (2) = C)) \leftrightarrow ((X \in P \land {X (1)}^{2} + {X (2)}^{2} = R^{2}) \land (X \in P \land A X (1) + B X (2) = C))$
34		simpl1	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \land X \in P) \to (A \in ℝ \land B \in ℝ \land C \in ℝ)$
35		simpl2	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \land X \in P) \to (A \neq 0 \lor B \neq 0)$
36		simpl3l	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \land X \in P) \to R \in ℝ^{+}$
37		simpl3r	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \land X \in P) \to 0 \leq D$
38	1 3	rrx2pxel	$⊢ X \in P \to X (1) \in ℝ$
39	1 3	rrx2pyel	$⊢ X \in P \to X (2) \in ℝ$
40	38 39	jca	$⊢ X \in P \to (X (1) \in ℝ \land X (2) \in ℝ)$
41	40	adantl	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \land X \in P) \to (X (1) \in ℝ \land X (2) \in ℝ)$
42	36 37 41	jca31	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \land X \in P) \to ((R \in ℝ^{+} \land 0 \leq D) \land (X (1) \in ℝ \land X (2) \in ℝ))$
43	6 7	itsclc0xyqsolb	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0)) \land ((R \in ℝ^{+} \land 0 \leq D) \land (X (1) \in ℝ \land X (2) \in ℝ))) \to (({X (1)}^{2} + {X (2)}^{2} = R^{2} \land A X (1) + B X (2) = C) \leftrightarrow ((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})))$
44	34 35 42 43	syl21anc	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \land X \in P) \to (({X (1)}^{2} + {X (2)}^{2} = R^{2} \land A X (1) + B X (2) = C) \leftrightarrow ((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})))$
45	44	pm5.32da	$⊢ ((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 P \land ({X (1)}^{2} + {X (2)}^{2} = R^{2} \land A X (1) + B X (2) = C)) \leftrightarrow (X \in P \land ((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}))))$
46	33 45	bitr3id	$⊢ ((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 P \land {X (1)}^{2} + {X (2)}^{2} = R^{2}) \land (X \in P \land A X (1) + B X (2) = C)) \leftrightarrow (X \in P \land ((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}))))$
47	32 46	bitrid	$⊢ ((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 \{p \in P \| {p (1)}^{2} + {p (2)}^{2} = R^{2}\} \land (X \in P \land A X (1) + B X (2) = C)) \leftrightarrow (X \in P \land ((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}))))$
48	26 47	bitrd	$⊢ ((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 L) \leftrightarrow (X \in P \land ((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 itsclc0b

Proof