Metamath Proof Explorer

Theorem itsclc0xyqsol

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, 25-Feb-2023)

		Ref	Expression
	Hypotheses	itscnhlc0yqe.q	$⊢ Q = A^{2} + B^{2}$
		itsclc0yqsol.d	$⊢ D = R^{2} Q - C^{2}$
	Assertion	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})))$

Proof

Step	Hyp	Ref	Expression
1		itscnhlc0yqe.q	$⊢ Q = A^{2} + B^{2}$
2		itsclc0yqsol.d	$⊢ D = R^{2} Q - C^{2}$
3	1 2	itscnhlc0xyqsol	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \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	3exp	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to ((R \in ℝ^{+} \land 0 \leq D) \to ((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	4	3exp	$⊢ (A \in ℝ \land A \neq 0) \to (B \in ℝ \to (C \in ℝ \to ((R \in ℝ^{+} \land 0 \leq D) \to ((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})))))))$
6	5	expcom	$⊢ A \neq 0 \to (A \in ℝ \to (B \in ℝ \to (C \in ℝ \to ((R \in ℝ^{+} \land 0 \leq D) \to ((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}))))))))$
7	6	3impd	$⊢ A \neq 0 \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to ((R \in ℝ^{+} \land 0 \leq D) \to ((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}))))))$
8		nne	$⊢ \neg A \neq 0 \leftrightarrow A = 0$
9	1 2	itschlc0xyqsol	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land 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})))$
10	9	3exp	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to ((R \in ℝ^{+} \land 0 \leq D) \to ((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})))))$
11	10	expcom	$⊢ (A = 0 \land B \neq 0) \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to ((R \in ℝ^{+} \land 0 \leq D) \to ((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}))))))$
12	8 11	sylanb	$⊢ (\neg A \neq 0 \land B \neq 0) \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to ((R \in ℝ^{+} \land 0 \leq D) \to ((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}))))))$
13	7 12	jaoi3	$⊢ (A \neq 0 \lor B \neq 0) \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to ((R \in ℝ^{+} \land 0 \leq D) \to ((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}))))))$
14	13	impcom	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0)) \to ((R \in ℝ^{+} \land 0 \leq D) \to ((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})))))$
15	14	3imp	$⊢ (((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})))$