itsclquadeu

Description: Quadratic equation for the y-coordinate of the intersection points of a line and a circle. (Contributed by AV, 23-Feb-2023)

	Ref	Expression
Hypotheses	itsclquadb.q	$⊢ Q = A^{2} + B^{2}$
	itsclquadb.t	$⊢ T = - 2 B C$
	itsclquadb.u	$⊢ U = C^{2} - A^{2} R^{2}$
Assertion	itsclquadeu	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (\exists! x \in ℝ (x^{2} + Y^{2} = R^{2} \land A x + B Y = C) \leftrightarrow Q Y^{2} + T Y + U = 0)$

Proof

Step	Hyp	Ref	Expression
1		itsclquadb.q	$⊢ Q = A^{2} + B^{2}$
2		itsclquadb.t	$⊢ T = - 2 B C$
3		itsclquadb.u	$⊢ U = C^{2} - A^{2} R^{2}$
4		oveq1	$⊢ x = z \to x^{2} = z^{2}$
5	4	oveq1d	$⊢ x = z \to x^{2} + Y^{2} = z^{2} + Y^{2}$
6	5	eqeq1d	$⊢ x = z \to (x^{2} + Y^{2} = R^{2} \leftrightarrow z^{2} + Y^{2} = R^{2})$
7		oveq2	$⊢ x = z \to A x = A z$
8	7	oveq1d	$⊢ x = z \to A x + B Y = A z + B Y$
9	8	eqeq1d	$⊢ x = z \to (A x + B Y = C \leftrightarrow A z + B Y = C)$
10	6 9	anbi12d	$⊢ x = z \to ((x^{2} + Y^{2} = R^{2} \land A x + B Y = C) \leftrightarrow (z^{2} + Y^{2} = R^{2} \land A z + B Y = C))$
11	10	reu8	$⊢ \exists! x \in ℝ (x^{2} + Y^{2} = R^{2} \land A x + B Y = C) \leftrightarrow \exists x \in ℝ ((x^{2} + Y^{2} = R^{2} \land A x + B Y = C) \land \forall z \in ℝ ((z^{2} + Y^{2} = R^{2} \land A z + B Y = C) \to x = z))$
12	11	a1i	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (\exists! x \in ℝ (x^{2} + Y^{2} = R^{2} \land A x + B Y = C) \leftrightarrow \exists x \in ℝ ((x^{2} + Y^{2} = R^{2} \land A x + B Y = C) \land \forall z \in ℝ ((z^{2} + Y^{2} = R^{2} \land A z + B Y = C) \to x = z)))$
13		id	$⊢ C = A x + B Y \to C = A x + B Y$
14	13	eqcoms	$⊢ A x + B Y = C \to C = A x + B Y$
15	14	eqeq2d	$⊢ A x + B Y = C \to (A z + B Y = C \leftrightarrow A z + B Y = A x + B Y)$
16	15	adantl	$⊢ ((((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \land A x + B Y = C) \to (A z + B Y = C \leftrightarrow A z + B Y = A x + B Y)$
17		simp11l	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to A \in ℝ$
18	17	ad2antrr	$⊢ (((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \to A \in ℝ$
19		simpr	$⊢ (((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \to z \in ℝ$
20	18 19	remulcld	$⊢ (((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \to A z \in ℝ$
21	20	recnd	$⊢ (((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \to A z \in ℂ$
22	17	adantr	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \to A \in ℝ$
23		simpr	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \to x \in ℝ$
24	22 23	remulcld	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \to A x \in ℝ$
25	24	adantr	$⊢ (((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \to A x \in ℝ$
26	25	recnd	$⊢ (((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \to A x \in ℂ$
27		simp12	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to B \in ℝ$
28		simp3	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to Y \in ℝ$
29	27 28	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to B Y \in ℝ$
30	29	ad2antrr	$⊢ (((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \to B Y \in ℝ$
31	30	recnd	$⊢ (((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \to B Y \in ℂ$
32	21 26 31	addcan2d	$⊢ (((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \to (A z + B Y = A x + B Y \leftrightarrow A z = A x)$
33	19	recnd	$⊢ (((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \to z \in ℂ$
34		simplr	$⊢ (((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \to x \in ℝ$
35	34	recnd	$⊢ (((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \to x \in ℂ$
36	18	recnd	$⊢ (((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \to A \in ℂ$
37		simp11r	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to A \neq 0$
38	37	ad2antrr	$⊢ (((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \to A \neq 0$
39	33 35 36 38	mulcand	$⊢ (((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \to (A z = A x \leftrightarrow z = x)$
40		equcom	$⊢ z = x \leftrightarrow x = z$
41	40	a1i	$⊢ (((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \to (z = x \leftrightarrow x = z)$
42	32 39 41	3bitrd	$⊢ (((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \to (A z + B Y = A x + B Y \leftrightarrow x = z)$
43	42	biimpd	$⊢ (((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \to (A z + B Y = A x + B Y \to x = z)$
44	43	adantr	$⊢ ((((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \land A x + B Y = C) \to (A z + B Y = A x + B Y \to x = z)$
45	16 44	sylbid	$⊢ ((((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land z \in ℝ) \land A x + B Y = C) \to (A z + B Y = C \to x = z)$
46	45	an32s	$⊢ ((((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land A x + B Y = C) \land z \in ℝ) \to (A z + B Y = C \to x = z)$
47	46	adantld	$⊢ ((((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land A x + B Y = C) \land z \in ℝ) \to ((z^{2} + Y^{2} = R^{2} \land A z + B Y = C) \to x = z)$
48	47	ralrimiva	$⊢ (((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \land A x + B Y = C) \to \forall z \in ℝ ((z^{2} + Y^{2} = R^{2} \land A z + B Y = C) \to x = z)$
49	48	ex	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \to (A x + B Y = C \to \forall z \in ℝ ((z^{2} + Y^{2} = R^{2} \land A z + B Y = C) \to x = z))$
50	49	adantld	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \to ((x^{2} + Y^{2} = R^{2} \land A x + B Y = C) \to \forall z \in ℝ ((z^{2} + Y^{2} = R^{2} \land A z + B Y = C) \to x = z))$
51	50	pm4.71d	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \to ((x^{2} + Y^{2} = R^{2} \land A x + B Y = C) \leftrightarrow ((x^{2} + Y^{2} = R^{2} \land A x + B Y = C) \land \forall z \in ℝ ((z^{2} + Y^{2} = R^{2} \land A z + B Y = C) \to x = z)))$
52	51	bicomd	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \to (((x^{2} + Y^{2} = R^{2} \land A x + B Y = C) \land \forall z \in ℝ ((z^{2} + Y^{2} = R^{2} \land A z + B Y = C) \to x = z)) \leftrightarrow (x^{2} + Y^{2} = R^{2} \land A x + B Y = C))$
53	52	rexbidva	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (\exists x \in ℝ ((x^{2} + Y^{2} = R^{2} \land A x + B Y = C) \land \forall z \in ℝ ((z^{2} + Y^{2} = R^{2} \land A z + B Y = C) \to x = z)) \leftrightarrow \exists x \in ℝ (x^{2} + Y^{2} = R^{2} \land A x + B Y = C))$
54	1 2 3	itsclquadb	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (\exists x \in ℝ (x^{2} + Y^{2} = R^{2} \land A x + B Y = C) \leftrightarrow Q Y^{2} + T Y + U = 0)$
55	12 53 54	3bitrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (\exists! x \in ℝ (x^{2} + Y^{2} = R^{2} \land A x + B Y = C) \leftrightarrow Q Y^{2} + T Y + U = 0)$

Metamath Proof Explorer

Theorem itsclquadeu

Proof