itsclc0yqe

Description: Lemma for itsclc0 . Quadratic equation for the y-coordinate of the intersection points of an arbitrary line and a circle. This theorem holds even for degenerate lines ( A = B = 0 ). (Contributed by AV, 25-Feb-2023)

	Ref	Expression
Hypotheses	itscnhlc0yqe.q	$⊢ Q = A^{2} + B^{2}$
	itscnhlc0yqe.t	$⊢ T = - 2 B C$
	itscnhlc0yqe.u	$⊢ U = C^{2} - A^{2} R^{2}$
Assertion	itsclc0yqe	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to ((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \to Q Y^{2} + T Y + U = 0)$

Proof

Step	Hyp	Ref	Expression
1		itscnhlc0yqe.q	$⊢ Q = A^{2} + B^{2}$
2		itscnhlc0yqe.t	$⊢ T = - 2 B C$
3		itscnhlc0yqe.u	$⊢ U = C^{2} - A^{2} R^{2}$
4		simp11	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A \in ℝ$
5	4	anim1i	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \land A = 0) \to (A \in ℝ \land A = 0)$
6	5	ancoms	$⊢ (A = 0 \land ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ))) \to (A \in ℝ \land A = 0)$
7		simpr12	$⊢ (A = 0 \land ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ))) \to B \in ℝ$
8		simpr13	$⊢ (A = 0 \land ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ))) \to C \in ℝ$
9		simpr2	$⊢ (A = 0 \land ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ))) \to R \in ℝ^{+}$
10		simpr3	$⊢ (A = 0 \land ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ))) \to (X \in ℝ \land Y \in ℝ)$
11	1 2 3	itschlc0yqe	$⊢ (((A \in ℝ \land A = 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to ((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \to Q Y^{2} + T Y + U = 0)$
12	6 7 8 9 10 11	syl311anc	$⊢ (A = 0 \land ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ))) \to ((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \to Q Y^{2} + T Y + U = 0)$
13	12	ex	$⊢ A = 0 \to (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to ((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \to Q Y^{2} + T Y + U = 0))$
14	4	anim1i	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \land A \neq 0) \to (A \in ℝ \land A \neq 0)$
15	14	ancoms	$⊢ (A \neq 0 \land ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ))) \to (A \in ℝ \land A \neq 0)$
16		simpr12	$⊢ (A \neq 0 \land ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ))) \to B \in ℝ$
17		simpr13	$⊢ (A \neq 0 \land ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ))) \to C \in ℝ$
18		simpr2	$⊢ (A \neq 0 \land ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ))) \to R \in ℝ^{+}$
19		simpr3	$⊢ (A \neq 0 \land ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ))) \to (X \in ℝ \land Y \in ℝ)$
20	1 2 3	itscnhlc0yqe	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to ((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \to Q Y^{2} + T Y + U = 0)$
21	15 16 17 18 19 20	syl311anc	$⊢ (A \neq 0 \land ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ))) \to ((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \to Q Y^{2} + T Y + U = 0)$
22	21	ex	$⊢ A \neq 0 \to (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to ((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \to Q Y^{2} + T Y + U = 0))$
23	13 22	pm2.61ine	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to ((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \to Q Y^{2} + T Y + U = 0)$

Metamath Proof Explorer

Theorem itsclc0yqe

Proof