itschlc0yqe

Description: Lemma for itsclc0 . Quadratic equation for the y-coordinate of the intersection points of a horizontal line and a circle. (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	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)$

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		oveq2	$⊢ C = B Y \to B C = B B Y$
5	4	oveq2d	$⊢ C = B Y \to 2 B C = 2 B B Y$
6	5	oveq1d	$⊢ C = B Y \to 2 B C Y = 2 B B Y Y$
7	6	negeqd	$⊢ C = B Y \to - 2 B C Y = - 2 B B Y Y$
8		oveq1	$⊢ C = B Y \to C^{2} = {B Y}^{2}$
9	7 8	oveq12d	$⊢ C = B Y \to - 2 B C Y + C^{2} = - 2 B B Y Y + {B Y}^{2}$
10	9	oveq2d	$⊢ C = B Y \to {B Y}^{2} + (- 2 B C Y) + C^{2} = {B Y}^{2} + (- 2 B B Y Y) + {B Y}^{2}$
11	10	eqcoms	$⊢ B Y = C \to {B Y}^{2} + (- 2 B C Y) + C^{2} = {B Y}^{2} + (- 2 B B Y Y) + {B Y}^{2}$
12		simp12	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to B \in ℝ$
13	12	recnd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to B \in ℂ$
14		simp3r	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to Y \in ℝ$
15	14	recnd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to Y \in ℂ$
16	13 15	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to B Y \in ℂ$
17	16	sqcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {B Y}^{2} \in ℂ$
18		2cnd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 2 \in ℂ$
19	13 16	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to B B Y \in ℂ$
20	18 19	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 2 B B Y \in ℂ$
21	20 15	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 2 B B Y Y \in ℂ$
22	21	negcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to - 2 B B Y Y \in ℂ$
23		add32r	$⊢ ({B Y}^{2} \in ℂ \land - 2 B B Y Y \in ℂ \land {B Y}^{2} \in ℂ) \to {B Y}^{2} + (- 2 B B Y Y) + {B Y}^{2} = {B Y}^{2} + {B Y}^{2} + (- 2 B B Y Y)$
24	17 22 17 23	syl3anc	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {B Y}^{2} + (- 2 B B Y Y) + {B Y}^{2} = {B Y}^{2} + {B Y}^{2} + (- 2 B B Y Y)$
25	17 17	addcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {B Y}^{2} + {B Y}^{2} \in ℂ$
26	25 21	negsubd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {B Y}^{2} + {B Y}^{2} + (- 2 B B Y Y) = {B Y}^{2} + {B Y}^{2} - 2 B B Y Y$
27	18 19 15	mulassd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 2 B B Y Y = 2 B B Y Y$
28	13 16 15	mul32d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to B B Y Y = B Y B Y$
29	16	sqvald	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {B Y}^{2} = B Y B Y$
30	28 29	eqtr4d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to B B Y Y = {B Y}^{2}$
31	30	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 2 B B Y Y = 2 {B Y}^{2}$
32	17	2timesd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 2 {B Y}^{2} = {B Y}^{2} + {B Y}^{2}$
33	27 31 32	3eqtrrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {B Y}^{2} + {B Y}^{2} = 2 B B Y Y$
34	25 33	subeq0bd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {B Y}^{2} + {B Y}^{2} - 2 B B Y Y = 0$
35	26 34	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {B Y}^{2} + {B Y}^{2} + (- 2 B B Y Y) = 0$
36	24 35	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {B Y}^{2} + (- 2 B B Y Y) + {B Y}^{2} = 0$
37	11 36	sylan9eqr	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \land B Y = C) \to {B Y}^{2} + (- 2 B C Y) + C^{2} = 0$
38	37	ex	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (B Y = C \to {B Y}^{2} + (- 2 B C Y) + C^{2} = 0)$
39		simp3l	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to X \in ℝ$
40	39	recnd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to X \in ℂ$
41	40	mul02d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 0 \cdot X = 0$
42	41	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 0 \cdot X + B Y = 0 + B Y$
43	16	addid2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 0 + B Y = B Y$
44	42 43	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 0 \cdot X + B Y = B Y$
45	44	eqeq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (0 \cdot X + B Y = C \leftrightarrow B Y = C)$
46	13	sqcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to B^{2} \in ℂ$
47	46	addid2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 0 + B^{2} = B^{2}$
48	47	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (0 + B^{2}) Y^{2} = B^{2} Y^{2}$
49	13 15	sqmuld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {B Y}^{2} = B^{2} Y^{2}$
50	48 49	eqtr4d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (0 + B^{2}) Y^{2} = {B Y}^{2}$
51		simp13	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C \in ℝ$
52	51	recnd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C \in ℂ$
53	13 52	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to B C \in ℂ$
54	18 53	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 2 B C \in ℂ$
55	54 15	mulneg1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (- 2 B C) Y = - 2 B C Y$
56		rpcn	$⊢ R \in ℝ^{+} \to R \in ℂ$
57	56	sqcld	$⊢ R \in ℝ^{+} \to R^{2} \in ℂ$
58	57	mul02d	$⊢ R \in ℝ^{+} \to 0 \cdot R^{2} = 0$
59	58	oveq2d	$⊢ R \in ℝ^{+} \to C^{2} - 0 \cdot R^{2} = C^{2} - 0$
60	59	3ad2ant2	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C^{2} - 0 \cdot R^{2} = C^{2} - 0$
61	52	sqcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C^{2} \in ℂ$
62	61	subid1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C^{2} - 0 = C^{2}$
63	60 62	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C^{2} - 0 \cdot R^{2} = C^{2}$
64	55 63	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (- 2 B C) Y + C^{2} - 0 \cdot R^{2} = - 2 B C Y + C^{2}$
65	50 64	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (0 + B^{2}) Y^{2} + (- 2 B C) Y + (C^{2} - 0 \cdot R^{2}) = {B Y}^{2} + (- 2 B C Y) + C^{2}$
66	65	eqeq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to ((0 + B^{2}) Y^{2} + (- 2 B C) Y + (C^{2} - 0 \cdot R^{2}) = 0 \leftrightarrow {B Y}^{2} + (- 2 B C Y) + C^{2} = 0)$
67	38 45 66	3imtr4d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (0 \cdot X + B Y = C \to (0 + B^{2}) Y^{2} + (- 2 B C) Y + (C^{2} - 0 \cdot R^{2}) = 0)$
68	67	3exp	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (R \in ℝ^{+} \to ((X \in ℝ \land Y \in ℝ) \to (0 \cdot X + B Y = C \to (0 + B^{2}) Y^{2} + (- 2 B C) Y + (C^{2} - 0 \cdot R^{2}) = 0)))$
69	68	3adant1r	$⊢ ((A \in ℝ \land A = 0) \land B \in ℝ \land C \in ℝ) \to (R \in ℝ^{+} \to ((X \in ℝ \land Y \in ℝ) \to (0 \cdot X + B Y = C \to (0 + B^{2}) Y^{2} + (- 2 B C) Y + (C^{2} - 0 \cdot R^{2}) = 0)))$
70	69	3imp	$⊢ (((A \in ℝ \land A = 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (0 \cdot X + B Y = C \to (0 + B^{2}) Y^{2} + (- 2 B C) Y + (C^{2} - 0 \cdot R^{2}) = 0)$
71	70	adantld	$⊢ (((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 0 \cdot X + B Y = C) \to (0 + B^{2}) Y^{2} + (- 2 B C) Y + (C^{2} - 0 \cdot R^{2}) = 0)$
72		oveq1	$⊢ A = 0 \to A X = 0 \cdot X$
73	72	oveq1d	$⊢ A = 0 \to A X + B Y = 0 \cdot X + B Y$
74	73	eqeq1d	$⊢ A = 0 \to (A X + B Y = C \leftrightarrow 0 \cdot X + B Y = C)$
75	74	anbi2d	$⊢ A = 0 \to ((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \leftrightarrow (X^{2} + Y^{2} = R^{2} \land 0 \cdot X + B Y = C))$
76		sq0i	$⊢ A = 0 \to A^{2} = 0$
77	76	oveq1d	$⊢ A = 0 \to A^{2} + B^{2} = 0 + B^{2}$
78	1 77	syl5eq	$⊢ A = 0 \to Q = 0 + B^{2}$
79	78	oveq1d	$⊢ A = 0 \to Q Y^{2} = (0 + B^{2}) Y^{2}$
80	2	oveq1i	$⊢ T Y = (- 2 B C) Y$
81	80	a1i	$⊢ A = 0 \to T Y = (- 2 B C) Y$
82	76	oveq1d	$⊢ A = 0 \to A^{2} R^{2} = 0 \cdot R^{2}$
83	82	oveq2d	$⊢ A = 0 \to C^{2} - A^{2} R^{2} = C^{2} - 0 \cdot R^{2}$
84	3 83	syl5eq	$⊢ A = 0 \to U = C^{2} - 0 \cdot R^{2}$
85	81 84	oveq12d	$⊢ A = 0 \to T Y + U = (- 2 B C) Y + C^{2} - 0 \cdot R^{2}$
86	79 85	oveq12d	$⊢ A = 0 \to Q Y^{2} + T Y + U = (0 + B^{2}) Y^{2} + (- 2 B C) Y + (C^{2} - 0 \cdot R^{2})$
87	86	eqeq1d	$⊢ A = 0 \to (Q Y^{2} + T Y + U = 0 \leftrightarrow (0 + B^{2}) Y^{2} + (- 2 B C) Y + (C^{2} - 0 \cdot R^{2}) = 0)$
88	75 87	imbi12d	$⊢ A = 0 \to (((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \to Q Y^{2} + T Y + U = 0) \leftrightarrow ((X^{2} + Y^{2} = R^{2} \land 0 \cdot X + B Y = C) \to (0 + B^{2}) Y^{2} + (- 2 B C) Y + (C^{2} - 0 \cdot R^{2}) = 0))$
89	88	adantl	$⊢ (A \in ℝ \land A = 0) \to (((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \to Q Y^{2} + T Y + U = 0) \leftrightarrow ((X^{2} + Y^{2} = R^{2} \land 0 \cdot X + B Y = C) \to (0 + B^{2}) Y^{2} + (- 2 B C) Y + (C^{2} - 0 \cdot R^{2}) = 0))$
90	89	3ad2ant1	$⊢ ((A \in ℝ \land A = 0) \land B \in ℝ \land C \in ℝ) \to (((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \to Q Y^{2} + T Y + U = 0) \leftrightarrow ((X^{2} + Y^{2} = R^{2} \land 0 \cdot X + B Y = C) \to (0 + B^{2}) Y^{2} + (- 2 B C) Y + (C^{2} - 0 \cdot R^{2}) = 0))$
91	90	3ad2ant1	$⊢ (((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) \leftrightarrow ((X^{2} + Y^{2} = R^{2} \land 0 \cdot X + B Y = C) \to (0 + B^{2}) Y^{2} + (- 2 B C) Y + (C^{2} - 0 \cdot R^{2}) = 0))$
92	71 91	mpbird	$⊢ (((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)$

Metamath Proof Explorer

Theorem itschlc0yqe

Proof