itscnhlc0yqe

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

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		recn	$⊢ A \in ℝ \to A \in ℂ$
5	4	adantr	$⊢ (A \in ℝ \land A \neq 0) \to A \in ℂ$
6	5	3ad2ant1	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to A \in ℂ$
7	6	3ad2ant1	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A \in ℂ$
8		simp2	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to B \in ℝ$
9	8	3ad2ant1	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to B \in ℝ$
10		simpr	$⊢ (X \in ℝ \land Y \in ℝ) \to Y \in ℝ$
11	10	3ad2ant3	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to Y \in ℝ$
12	9 11	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to B Y \in ℝ$
13	12	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to B Y \in ℂ$
14		recn	$⊢ X \in ℝ \to X \in ℂ$
15	14	adantr	$⊢ (X \in ℝ \land Y \in ℝ) \to X \in ℂ$
16	15	3ad2ant3	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to X \in ℂ$
17		simp3	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to C \in ℝ$
18	17	recnd	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to C \in ℂ$
19	18	3ad2ant1	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C \in ℂ$
20		simp11r	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A \neq 0$
21	7 13 16 19 20	lineq	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (A X + B Y = C \leftrightarrow X = \frac{C - B Y}{A})$
22	21	anbi2d	$⊢ (((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) \leftrightarrow (X^{2} + Y^{2} = R^{2} \land X = \frac{C - B Y}{A}))$
23		oveq1	$⊢ X = \frac{C - B Y}{A} \to X^{2} = {(\frac{C - B Y}{A})}^{2}$
24	23	oveq1d	$⊢ X = \frac{C - B Y}{A} \to X^{2} + Y^{2} = {(\frac{C - B Y}{A})}^{2} + Y^{2}$
25	24	eqeq1d	$⊢ X = \frac{C - B Y}{A} \to (X^{2} + Y^{2} = R^{2} \leftrightarrow {(\frac{C - B Y}{A})}^{2} + Y^{2} = R^{2})$
26	25	biimpac	$⊢ (X^{2} + Y^{2} = R^{2} \land X = \frac{C - B Y}{A}) \to {(\frac{C - B Y}{A})}^{2} + Y^{2} = R^{2}$
27		simpl	$⊢ (A \in ℝ \land A \neq 0) \to A \in ℝ$
28	27	3ad2ant1	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to A \in ℝ$
29	28	resqcld	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to A^{2} \in ℝ$
30	29	recnd	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to A^{2} \in ℂ$
31	30	3ad2ant1	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A^{2} \in ℂ$
32	17	3ad2ant1	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C \in ℝ$
33	32 12	resubcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C - B Y \in ℝ$
34	28	3ad2ant1	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A \in ℝ$
35	33 34 20	redivcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to \frac{C - B Y}{A} \in ℝ$
36	35	resqcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {(\frac{C - B Y}{A})}^{2} \in ℝ$
37	36	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {(\frac{C - B Y}{A})}^{2} \in ℂ$
38	10	resqcld	$⊢ (X \in ℝ \land Y \in ℝ) \to Y^{2} \in ℝ$
39	38	recnd	$⊢ (X \in ℝ \land Y \in ℝ) \to Y^{2} \in ℂ$
40	39	3ad2ant3	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to Y^{2} \in ℂ$
41	31 37 40	adddid	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A^{2} ({(\frac{C - B Y}{A})}^{2} + Y^{2}) = A^{2} {(\frac{C - B Y}{A})}^{2} + A^{2} Y^{2}$
42	33	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C - B Y \in ℂ$
43	27	recnd	$⊢ (A \in ℝ \land A \neq 0) \to A \in ℂ$
44	43	3ad2ant1	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to A \in ℂ$
45	44	3ad2ant1	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A \in ℂ$
46	42 45 20	sqdivd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {(\frac{C - B Y}{A})}^{2} = \frac{{(C - B Y)}^{2}}{A^{2}}$
47	46	oveq2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A^{2} {(\frac{C - B Y}{A})}^{2} = A^{2} (\frac{{(C - B Y)}^{2}}{A^{2}})$
48	33	resqcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {(C - B Y)}^{2} \in ℝ$
49	48	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {(C - B Y)}^{2} \in ℂ$
50	27	resqcld	$⊢ (A \in ℝ \land A \neq 0) \to A^{2} \in ℝ$
51	50	recnd	$⊢ (A \in ℝ \land A \neq 0) \to A^{2} \in ℂ$
52	51	3ad2ant1	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to A^{2} \in ℂ$
53	52	3ad2ant1	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A^{2} \in ℂ$
54		sqne0	$⊢ A \in ℂ \to (A^{2} \neq 0 \leftrightarrow A \neq 0)$
55	4 54	syl	$⊢ A \in ℝ \to (A^{2} \neq 0 \leftrightarrow A \neq 0)$
56	55	biimpar	$⊢ (A \in ℝ \land A \neq 0) \to A^{2} \neq 0$
57	56	3ad2ant1	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to A^{2} \neq 0$
58	57	3ad2ant1	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A^{2} \neq 0$
59	49 53 58	divcan2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A^{2} (\frac{{(C - B Y)}^{2}}{A^{2}}) = {(C - B Y)}^{2}$
60	47 59	eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A^{2} {(\frac{C - B Y}{A})}^{2} = {(C - B Y)}^{2}$
61	60	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A^{2} {(\frac{C - B Y}{A})}^{2} + A^{2} Y^{2} = {(C - B Y)}^{2} + A^{2} Y^{2}$
62	41 61	eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A^{2} ({(\frac{C - B Y}{A})}^{2} + Y^{2}) = {(C - B Y)}^{2} + A^{2} Y^{2}$
63	62	eqeq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (A^{2} ({(\frac{C - B Y}{A})}^{2} + Y^{2}) = A^{2} R^{2} \leftrightarrow {(C - B Y)}^{2} + A^{2} Y^{2} = A^{2} R^{2})$
64	11	resqcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to Y^{2} \in ℝ$
65	36 64	readdcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {(\frac{C - B Y}{A})}^{2} + Y^{2} \in ℝ$
66	65	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {(\frac{C - B Y}{A})}^{2} + Y^{2} \in ℂ$
67		rpre	$⊢ R \in ℝ^{+} \to R \in ℝ$
68	67	resqcld	$⊢ R \in ℝ^{+} \to R^{2} \in ℝ$
69	68	recnd	$⊢ R \in ℝ^{+} \to R^{2} \in ℂ$
70	69	3ad2ant2	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to R^{2} \in ℂ$
71	50	3ad2ant1	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to A^{2} \in ℝ$
72	71	3ad2ant1	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A^{2} \in ℝ$
73	72	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A^{2} \in ℂ$
74	66 70 73 58	mulcand	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (A^{2} ({(\frac{C - B Y}{A})}^{2} + Y^{2}) = A^{2} R^{2} \leftrightarrow {(\frac{C - B Y}{A})}^{2} + Y^{2} = R^{2})$
75		binom2sub	$⊢ (C \in ℂ \land B Y \in ℂ) \to {(C - B Y)}^{2} = C^{2} - 2 C B Y + {B Y}^{2}$
76	19 13 75	syl2anc	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {(C - B Y)}^{2} = C^{2} - 2 C B Y + {B Y}^{2}$
77	76	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {(C - B Y)}^{2} + A^{2} Y^{2} = (C^{2} - 2 C B Y) + {B Y}^{2} + A^{2} Y^{2}$
78	77	eqeq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to ({(C - B Y)}^{2} + A^{2} Y^{2} = A^{2} R^{2} \leftrightarrow (C^{2} - 2 C B Y) + {B Y}^{2} + A^{2} Y^{2} = A^{2} R^{2})$
79	17	resqcld	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to C^{2} \in ℝ$
80	79	3ad2ant1	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C^{2} \in ℝ$
81		2re	$⊢ 2 \in ℝ$
82	81	a1i	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 2 \in ℝ$
83	32 12	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C B Y \in ℝ$
84	82 83	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 2 C B Y \in ℝ$
85	80 84	resubcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C^{2} - 2 C B Y \in ℝ$
86	12	resqcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {B Y}^{2} \in ℝ$
87	85 86	readdcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C^{2} - 2 C B Y + {B Y}^{2} \in ℝ$
88	72 64	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A^{2} Y^{2} \in ℝ$
89	87 88	readdcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (C^{2} - 2 C B Y) + {B Y}^{2} + A^{2} Y^{2} \in ℝ$
90	89	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (C^{2} - 2 C B Y) + {B Y}^{2} + A^{2} Y^{2} \in ℂ$
91	68	3ad2ant2	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to R^{2} \in ℝ$
92	72 91	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A^{2} R^{2} \in ℝ$
93	92	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A^{2} R^{2} \in ℂ$
94	90 93 93	subcan2ad	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to ((C^{2} - 2 C B Y + {B Y}^{2}) + A^{2} Y^{2} - A^{2} R^{2} = A^{2} R^{2} - A^{2} R^{2} \leftrightarrow (C^{2} - 2 C B Y) + {B Y}^{2} + A^{2} Y^{2} = A^{2} R^{2})$
95	85	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C^{2} - 2 C B Y \in ℂ$
96	86	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {B Y}^{2} \in ℂ$
97	88	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A^{2} Y^{2} \in ℂ$
98	95 96 97	addassd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (C^{2} - 2 C B Y) + {B Y}^{2} + A^{2} Y^{2} = (C^{2} - 2 C B Y) + {B Y}^{2} + A^{2} Y^{2}$
99	32	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C \in ℂ$
100	8	recnd	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to B \in ℂ$
101	100	3ad2ant1	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to B \in ℂ$
102	11	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to Y \in ℂ$
103	99 101 102	mulassd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C B Y = C B Y$
104	18 100	mulcomd	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to C B = B C$
105	104	3ad2ant1	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C B = B C$
106	105	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C B Y = B C Y$
107	103 106	eqtr3d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C B Y = B C Y$
108	107	oveq2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 2 C B Y = 2 B C Y$
109	82	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 2 \in ℂ$
110	8 17	remulcld	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to B C \in ℝ$
111	110	3ad2ant1	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to B C \in ℝ$
112	111	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to B C \in ℂ$
113	109 112 102	mulassd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 2 B C Y = 2 B C Y$
114	108 113	eqtr4d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 2 C B Y = 2 B C Y$
115	114	oveq2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C^{2} - 2 C B Y = C^{2} - 2 B C Y$
116	101 102	sqmuld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {B Y}^{2} = B^{2} Y^{2}$
117	116	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {B Y}^{2} + A^{2} Y^{2} = B^{2} Y^{2} + A^{2} Y^{2}$
118	9	resqcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to B^{2} \in ℝ$
119	118	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to B^{2} \in ℂ$
120	34	resqcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A^{2} \in ℝ$
121	120	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A^{2} \in ℂ$
122	64	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to Y^{2} \in ℂ$
123	119 121 122	adddird	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (B^{2} + A^{2}) Y^{2} = B^{2} Y^{2} + A^{2} Y^{2}$
124	117 123	eqtr4d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to {B Y}^{2} + A^{2} Y^{2} = (B^{2} + A^{2}) Y^{2}$
125	115 124	oveq12d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (C^{2} - 2 C B Y) + {B Y}^{2} + A^{2} Y^{2} = C^{2} - 2 B C Y + (B^{2} + A^{2}) Y^{2}$
126	98 125	eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (C^{2} - 2 C B Y) + {B Y}^{2} + A^{2} Y^{2} = C^{2} - 2 B C Y + (B^{2} + A^{2}) Y^{2}$
127	126	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (C^{2} - 2 C B Y + {B Y}^{2}) + A^{2} Y^{2} - A^{2} R^{2} = (C^{2} - 2 B C Y) + (B^{2} + A^{2}) Y^{2} - A^{2} R^{2}$
128	80	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C^{2} \in ℂ$
129	8	resqcld	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to B^{2} \in ℝ$
130	129 71	readdcld	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to B^{2} + A^{2} \in ℝ$
131	130	3ad2ant1	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to B^{2} + A^{2} \in ℝ$
132	131 64	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (B^{2} + A^{2}) Y^{2} \in ℝ$
133	9 32	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to B C \in ℝ$
134	82 133	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 2 B C \in ℝ$
135	134 11	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 2 B C Y \in ℝ$
136	132 135	resubcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (B^{2} + A^{2}) Y^{2} - 2 B C Y \in ℝ$
137	136	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (B^{2} + A^{2}) Y^{2} - 2 B C Y \in ℂ$
138	135	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 2 B C Y \in ℂ$
139	132	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (B^{2} + A^{2}) Y^{2} \in ℂ$
140	128 138 139	subadd23d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C^{2} - 2 B C Y + (B^{2} + A^{2}) Y^{2} = C^{2} + (B^{2} + A^{2}) Y^{2} - 2 B C Y$
141	128 137 140	comraddd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C^{2} - 2 B C Y + (B^{2} + A^{2}) Y^{2} = (B^{2} + A^{2}) Y^{2} - 2 B C Y + C^{2}$
142	141	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (C^{2} - 2 B C Y) + (B^{2} + A^{2}) Y^{2} - A^{2} R^{2} = ((B^{2} + A^{2}) Y^{2} - 2 B C Y) + C^{2} - A^{2} R^{2}$
143	137 128 93	addsubassd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to ((B^{2} + A^{2}) Y^{2} - 2 B C Y) + C^{2} - A^{2} R^{2} = ((B^{2} + A^{2}) Y^{2} - 2 B C Y) + C^{2} - A^{2} R^{2}$
144	139 138	negsubd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (B^{2} + A^{2}) Y^{2} + (- 2 B C Y) = (B^{2} + A^{2}) Y^{2} - 2 B C Y$
145	144	eqcomd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (B^{2} + A^{2}) Y^{2} - 2 B C Y = (B^{2} + A^{2}) Y^{2} + (- 2 B C Y)$
146	145	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to ((B^{2} + A^{2}) Y^{2} - 2 B C Y) + C^{2} - A^{2} R^{2} = (B^{2} + A^{2}) Y^{2} + (- 2 B C Y) + (C^{2} - A^{2} R^{2})$
147	135	renegcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to - 2 B C Y \in ℝ$
148	147	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to - 2 B C Y \in ℂ$
149	80 92	resubcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C^{2} - A^{2} R^{2} \in ℝ$
150	149	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to C^{2} - A^{2} R^{2} \in ℂ$
151	139 148 150	addassd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (B^{2} + A^{2}) Y^{2} + (- 2 B C Y) + (C^{2} - A^{2} R^{2}) = (B^{2} + A^{2}) Y^{2} + (- 2 B C Y) + (C^{2} - A^{2} R^{2})$
152	143 146 151	3eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to ((B^{2} + A^{2}) Y^{2} - 2 B C Y) + C^{2} - A^{2} R^{2} = (B^{2} + A^{2}) Y^{2} + (- 2 B C Y) + (C^{2} - A^{2} R^{2})$
153	127 142 152	3eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (C^{2} - 2 C B Y + {B Y}^{2}) + A^{2} Y^{2} - A^{2} R^{2} = (B^{2} + A^{2}) Y^{2} + (- 2 B C Y) + (C^{2} - A^{2} R^{2})$
154	93	subidd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to A^{2} R^{2} - A^{2} R^{2} = 0$
155	153 154	eqeq12d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to ((C^{2} - 2 C B Y + {B Y}^{2}) + A^{2} Y^{2} - A^{2} R^{2} = A^{2} R^{2} - A^{2} R^{2} \leftrightarrow (B^{2} + A^{2}) Y^{2} + (- 2 B C Y) + (C^{2} - A^{2} R^{2}) = 0)$
156	78 94 155	3bitr2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to ({(C - B Y)}^{2} + A^{2} Y^{2} = A^{2} R^{2} \leftrightarrow (B^{2} + A^{2}) Y^{2} + (- 2 B C Y) + (C^{2} - A^{2} R^{2}) = 0)$
157	63 74 156	3bitr3d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to ({(\frac{C - B Y}{A})}^{2} + Y^{2} = R^{2} \leftrightarrow (B^{2} + A^{2}) Y^{2} + (- 2 B C Y) + (C^{2} - A^{2} R^{2}) = 0)$
158	1	a1i	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to Q = A^{2} + B^{2}$
159	121 119 158	comraddd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to Q = B^{2} + A^{2}$
160	159	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to Q Y^{2} = (B^{2} + A^{2}) Y^{2}$
161	2	a1i	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to T = - 2 B C$
162	161	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to T Y = (- 2 B C) Y$
163	134	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to 2 B C \in ℂ$
164	163 102	mulneg1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (- 2 B C) Y = - 2 B C Y$
165	162 164	eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to T Y = - 2 B C Y$
166	3	a1i	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to U = C^{2} - A^{2} R^{2}$
167	165 166	oveq12d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to T Y + U = (- 2 B C Y) + C^{2} - A^{2} R^{2}$
168	160 167	oveq12d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to Q Y^{2} + T Y + U = (B^{2} + A^{2}) Y^{2} + (- 2 B C Y) + (C^{2} - A^{2} R^{2})$
169	168	eqcomd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to (B^{2} + A^{2}) Y^{2} + (- 2 B C Y) + (C^{2} - A^{2} R^{2}) = Q Y^{2} + T Y + U$
170	169	eqeq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to ((B^{2} + A^{2}) Y^{2} + (- 2 B C Y) + (C^{2} - A^{2} R^{2}) = 0 \leftrightarrow Q Y^{2} + T Y + U = 0)$
171	170	biimpd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to ((B^{2} + A^{2}) Y^{2} + (- 2 B C Y) + (C^{2} - A^{2} R^{2}) = 0 \to Q Y^{2} + T Y + U = 0)$
172	157 171	sylbid	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (X \in ℝ \land Y \in ℝ)) \to ({(\frac{C - B Y}{A})}^{2} + Y^{2} = R^{2} \to Q Y^{2} + T Y + U = 0)$
173	26 172	syl5	$⊢ (((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 X = \frac{C - B Y}{A}) \to Q Y^{2} + T Y + U = 0)$
174	22 173	sylbid	$⊢ (((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)$

Metamath Proof Explorer

Theorem itscnhlc0yqe

Proof