itsclc0

Description: The intersection points of a line L and a circle around the origin. (Contributed by AV, 25-Feb-2023)

	Ref	Expression
Hypotheses	itsclc0.i	$⊢ I = \{1, 2\}$
	itsclc0.e	$⊢ E = I$
	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	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 L) \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 = I$
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		3simpa	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0))$
33	32	adantr	$⊢ (((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 ℝ) \land (A \neq 0 \lor B \neq 0))$
34		simpl3	$⊢ (((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)$
35	1 3	rrx2pxel	$⊢ X \in P \to X (1) \in ℝ$
36	1 3	rrx2pyel	$⊢ X \in P \to X (2) \in ℝ$
37	35 36	jca	$⊢ X \in P \to (X (1) \in ℝ \land X (2) \in ℝ)$
38	37	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 ℝ)$
39	6 7	itsclc0xyqsol	$⊢ (((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) \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})))$
40	33 34 38 39	syl3anc	$⊢ (((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) \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	40	expcomd	$⊢ (((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 X (1) + B X (2) = C \to ({X (1)}^{2} + {X (2)}^{2} = R^{2} \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	41	expimpd	$⊢ ((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 A X (1) + B X (2) = C) \to ({X (1)}^{2} + {X (2)}^{2} = R^{2} \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}))))$
43	42	com23	$⊢ ((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 (1)}^{2} + {X (2)}^{2} = R^{2} \to ((X \in P \land A X (1) + B X (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}))))$
44	43	adantld	$⊢ ((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}) \to ((X \in P \land A X (1) + B X (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}))))$
45	31 44	biimtrid	$⊢ ((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}\} \to ((X \in P \land A X (1) + B X (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}))))$
46	45	impd	$⊢ ((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)) \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})))$
47	26 46	sylbid	$⊢ ((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) \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 itsclc0

Proof