Metamath Proof Explorer

Theorem itsclc0xyqsolb

Description: Lemma for itsclc0 . Solutions of the quadratic equations for the coordinates of the intersection points of a (nondegenerate) line and a circle. (Contributed by AV, 2-May-2023) (Revised by AV, 14-May-2023)

		Ref	Expression
	Hypotheses	itsclc0xyqsolr.q	$⊢ Q = A^{2} + B^{2}$
		itsclc0xyqsolr.d	$⊢ D = R^{2} Q - C^{2}$
	Assertion	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 \in ℝ \land Y \in ℝ))) \to ((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \leftrightarrow ((X = \frac{A C + B \sqrt{D}}{Q} \land Y = \frac{B C - A \sqrt{D}}{Q}) \lor (X = \frac{A C - B \sqrt{D}}{Q} \land Y = \frac{B C + A \sqrt{D}}{Q})))$

Proof

Step	Hyp	Ref	Expression
1		itsclc0xyqsolr.q	$⊢ Q = A^{2} + B^{2}$
2		itsclc0xyqsolr.d	$⊢ D = R^{2} Q - C^{2}$
3	1 2	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 \in ℝ \land Y \in ℝ)) \to ((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \to ((X = \frac{A C + B \sqrt{D}}{Q} \land Y = \frac{B C - A \sqrt{D}}{Q}) \lor (X = \frac{A C - B \sqrt{D}}{Q} \land Y = \frac{B C + A \sqrt{D}}{Q})))$
4	3	3expb	$⊢ (((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 ℝ \land Y \in ℝ))) \to ((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \to ((X = \frac{A C + B \sqrt{D}}{Q} \land Y = \frac{B C - A \sqrt{D}}{Q}) \lor (X = \frac{A C - B \sqrt{D}}{Q} \land Y = \frac{B C + A \sqrt{D}}{Q})))$
5		simpl	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0)) \to (A \in ℝ \land B \in ℝ \land C \in ℝ)$
6		simpr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0)) \to (A \neq 0 \lor B \neq 0)$
7		simpl	$⊢ ((R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (R \in ℝ^{+} \land 0 \leq D)$
8	1 2	itsclc0xyqsolr	$⊢ ((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 = \frac{A C + B \sqrt{D}}{Q} \land Y = \frac{B C - A \sqrt{D}}{Q}) \lor (X = \frac{A C - B \sqrt{D}}{Q} \land Y = \frac{B C + A \sqrt{D}}{Q})) \to (X^{2} + Y^{2} = R^{2} \land A X + B Y = C))$
9	5 6 7 8	syl2an3an	$⊢ (((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 ℝ \land Y \in ℝ))) \to (((X = \frac{A C + B \sqrt{D}}{Q} \land Y = \frac{B C - A \sqrt{D}}{Q}) \lor (X = \frac{A C - B \sqrt{D}}{Q} \land Y = \frac{B C + A \sqrt{D}}{Q})) \to (X^{2} + Y^{2} = R^{2} \land A X + B Y = C))$
10	4 9	impbid	$⊢ (((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 ℝ \land Y \in ℝ))) \to ((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \leftrightarrow ((X = \frac{A C + B \sqrt{D}}{Q} \land Y = \frac{B C - A \sqrt{D}}{Q}) \lor (X = \frac{A C - B \sqrt{D}}{Q} \land Y = \frac{B C + A \sqrt{D}}{Q})))$