itsclc0yqsol

Description: Lemma for itsclc0 . Solutions of the quadratic equations for the y-coordinate of the intersection points of a (nondegenerate) line and a circle. (Contributed by AV, 7-Feb-2023)

	Ref	Expression
Hypotheses	itscnhlc0yqe.q	$⊢ Q = A^{2} + B^{2}$
	itsclc0yqsol.d	$⊢ D = R^{2} Q - C^{2}$
Assertion	itsclc0yqsol	$⊢ (((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 (Y = \frac{B C - A \sqrt{D}}{Q} \lor 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		eqid	$⊢ - 2 B C = - 2 B C$
4		eqid	$⊢ C^{2} - A^{2} R^{2} = C^{2} - A^{2} R^{2}$
5	1 3 4	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} + (- 2 B C) Y + (C^{2} - A^{2} R^{2}) = 0)$
6	5	3adant1r	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0)) \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} + (- 2 B C) Y + (C^{2} - A^{2} R^{2}) = 0)$
7	6	3adant2r	$⊢ (((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 Q Y^{2} + (- 2 B C) Y + (C^{2} - A^{2} R^{2}) = 0)$
8		3simpa	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (A \in ℝ \land B \in ℝ)$
9	8	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0)) \to (A \in ℝ \land B \in ℝ)$
10	1	resum2sqcl	$⊢ (A \in ℝ \land B \in ℝ) \to Q \in ℝ$
11	9 10	syl	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0)) \to Q \in ℝ$
12	11	3ad2ant1	$⊢ (((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 Q \in ℝ$
13	12	recnd	$⊢ (((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 Q \in ℂ$
14		simpr1	$⊢ (A \neq 0 \land (A \in ℝ \land B \in ℝ \land C \in ℝ)) \to A \in ℝ$
15		simpl	$⊢ (A \neq 0 \land (A \in ℝ \land B \in ℝ \land C \in ℝ)) \to A \neq 0$
16		simpr2	$⊢ (A \neq 0 \land (A \in ℝ \land B \in ℝ \land C \in ℝ)) \to B \in ℝ$
17	1	resum2sqgt0	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ) \to 0 < Q$
18	14 15 16 17	syl21anc	$⊢ (A \neq 0 \land (A \in ℝ \land B \in ℝ \land C \in ℝ)) \to 0 < Q$
19	18	ex	$⊢ A \neq 0 \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to 0 < Q)$
20		simpr2	$⊢ (B \neq 0 \land (A \in ℝ \land B \in ℝ \land C \in ℝ)) \to B \in ℝ$
21		simpl	$⊢ (B \neq 0 \land (A \in ℝ \land B \in ℝ \land C \in ℝ)) \to B \neq 0$
22		simpr1	$⊢ (B \neq 0 \land (A \in ℝ \land B \in ℝ \land C \in ℝ)) \to A \in ℝ$
23		eqid	$⊢ B^{2} + A^{2} = B^{2} + A^{2}$
24	23	resum2sqgt0	$⊢ ((B \in ℝ \land B \neq 0) \land A \in ℝ) \to 0 < B^{2} + A^{2}$
25	20 21 22 24	syl21anc	$⊢ (B \neq 0 \land (A \in ℝ \land B \in ℝ \land C \in ℝ)) \to 0 < B^{2} + A^{2}$
26		simp1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A \in ℝ$
27	26	recnd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A \in ℂ$
28	27	sqcld	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A^{2} \in ℂ$
29		simp2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B \in ℝ$
30	29	recnd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B \in ℂ$
31	30	sqcld	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B^{2} \in ℂ$
32	28 31	addcomd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A^{2} + B^{2} = B^{2} + A^{2}$
33	32	adantl	$⊢ (B \neq 0 \land (A \in ℝ \land B \in ℝ \land C \in ℝ)) \to A^{2} + B^{2} = B^{2} + A^{2}$
34	1 33	eqtrid	$⊢ (B \neq 0 \land (A \in ℝ \land B \in ℝ \land C \in ℝ)) \to Q = B^{2} + A^{2}$
35	25 34	breqtrrd	$⊢ (B \neq 0 \land (A \in ℝ \land B \in ℝ \land C \in ℝ)) \to 0 < Q$
36	35	ex	$⊢ B \neq 0 \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to 0 < Q)$
37	19 36	jaoi	$⊢ (A \neq 0 \lor B \neq 0) \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to 0 < Q)$
38	37	impcom	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0)) \to 0 < Q$
39	38	gt0ne0d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0)) \to Q \neq 0$
40	39	3ad2ant1	$⊢ (((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 Q \neq 0$
41		2cnd	$⊢ (((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 2 \in ℂ$
42		recn	$⊢ B \in ℝ \to B \in ℂ$
43	42	3ad2ant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B \in ℂ$
44	43	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0)) \to B \in ℂ$
45	44	3ad2ant1	$⊢ (((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 B \in ℂ$
46		recn	$⊢ C \in ℝ \to C \in ℂ$
47	46	3ad2ant3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to C \in ℂ$
48	47	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0)) \to C \in ℂ$
49	48	3ad2ant1	$⊢ (((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 C \in ℂ$
50	45 49	mulcld	$⊢ (((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 B C \in ℂ$
51	41 50	mulcld	$⊢ (((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 2 B C \in ℂ$
52	51	negcld	$⊢ (((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 - 2 B C \in ℂ$
53	49	sqcld	$⊢ (((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 C^{2} \in ℂ$
54		recn	$⊢ A \in ℝ \to A \in ℂ$
55	54	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A \in ℂ$
56	55	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0)) \to A \in ℂ$
57	56	3ad2ant1	$⊢ (((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 A \in ℂ$
58	57	sqcld	$⊢ (((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 A^{2} \in ℂ$
59		simpl	$⊢ (R \in ℝ^{+} \land 0 \leq D) \to R \in ℝ^{+}$
60	59	rpcnd	$⊢ (R \in ℝ^{+} \land 0 \leq D) \to R \in ℂ$
61	60	3ad2ant2	$⊢ (((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 R \in ℂ$
62	61	sqcld	$⊢ (((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 R^{2} \in ℂ$
63	58 62	mulcld	$⊢ (((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 A^{2} R^{2} \in ℂ$
64	53 63	subcld	$⊢ (((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 C^{2} - A^{2} R^{2} \in ℂ$
65		recn	$⊢ Y \in ℝ \to Y \in ℂ$
66	65	adantl	$⊢ (X \in ℝ \land Y \in ℝ) \to Y \in ℂ$
67	66	3ad2ant3	$⊢ (((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 Y \in ℂ$
68		eqidd	$⊢ (((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 {(- 2 B C)}^{2} - 4 Q (C^{2} - A^{2} R^{2}) = {(- 2 B C)}^{2} - 4 Q (C^{2} - A^{2} R^{2})$
69	13 40 52 64 67 68	quad	$⊢ (((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 (Q Y^{2} + (- 2 B C) Y + (C^{2} - A^{2} R^{2}) = 0 \leftrightarrow (Y = \frac{- (- 2 B C) + \sqrt{{(- 2 B C)}^{2} - 4 Q (C^{2} - A^{2} R^{2})}}{2 Q} \lor Y = \frac{- (- 2 B C) - \sqrt{{(- 2 B C)}^{2} - 4 Q (C^{2} - A^{2} R^{2})}}{2 Q}))$
70	54	abscld	$⊢ A \in ℝ \to \|A\| \in ℝ$
71	70	recnd	$⊢ A \in ℝ \to \|A\| \in ℂ$
72	71	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to \|A\| \in ℂ$
73	72	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0)) \to \|A\| \in ℂ$
74	73	3ad2ant1	$⊢ (((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 \|A\| \in ℂ$
75	59	rpred	$⊢ (R \in ℝ^{+} \land 0 \leq D) \to R \in ℝ$
76	75	3ad2ant2	$⊢ (((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 R \in ℝ$
77	76	resqcld	$⊢ (((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 R^{2} \in ℝ$
78	77 12	remulcld	$⊢ (((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 R^{2} Q \in ℝ$
79		simp1l3	$⊢ (((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 C \in ℝ$
80	79	resqcld	$⊢ (((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 C^{2} \in ℝ$
81	78 80	resubcld	$⊢ (((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 R^{2} Q - C^{2} \in ℝ$
82	2 81	eqeltrid	$⊢ (((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 D \in ℝ$
83	82	recnd	$⊢ (((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 D \in ℂ$
84	83	sqrtcld	$⊢ (((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 \sqrt{D} \in ℂ$
85	41 74 84	mulassd	$⊢ (((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 2 \|A\| \sqrt{D} = 2 \|A\| \sqrt{D}$
86	85	oveq2d	$⊢ (((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 2 B C + 2 \|A\| \sqrt{D} = 2 B C + 2 \|A\| \sqrt{D}$
87	51	negnegd	$⊢ (((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 - (- 2 B C) = 2 B C$
88		simpl	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0)) \to (A \in ℝ \land B \in ℝ \land C \in ℝ)$
89	88	3ad2ant1	$⊢ (((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 (A \in ℝ \land B \in ℝ \land C \in ℝ)$
90		simp2r	$⊢ (((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 0 \leq D$
91	1 3 4 2	itsclc0yqsollem2	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to \sqrt{{(- 2 B C)}^{2} - 4 Q (C^{2} - A^{2} R^{2})} = 2 \|A\| \sqrt{D}$
92	89 76 90 91	syl3anc	$⊢ (((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 \sqrt{{(- 2 B C)}^{2} - 4 Q (C^{2} - A^{2} R^{2})} = 2 \|A\| \sqrt{D}$
93	87 92	oveq12d	$⊢ (((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 - (- 2 B C) + \sqrt{{(- 2 B C)}^{2} - 4 Q (C^{2} - A^{2} R^{2})} = 2 B C + 2 \|A\| \sqrt{D}$
94	74 84	mulcld	$⊢ (((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 \|A\| \sqrt{D} \in ℂ$
95	41 50 94	adddid	$⊢ (((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 2 (B C + \|A\| \sqrt{D}) = 2 B C + 2 \|A\| \sqrt{D}$
96	86 93 95	3eqtr4d	$⊢ (((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 - (- 2 B C) + \sqrt{{(- 2 B C)}^{2} - 4 Q (C^{2} - A^{2} R^{2})} = 2 (B C + \|A\| \sqrt{D})$
97	96	oveq1d	$⊢ (((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 \frac{- (- 2 B C) + \sqrt{{(- 2 B C)}^{2} - 4 Q (C^{2} - A^{2} R^{2})}}{2 Q} = \frac{2 (B C + \|A\| \sqrt{D})}{2 Q}$
98	50 94	addcld	$⊢ (((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 B C + \|A\| \sqrt{D} \in ℂ$
99		2ne0	$⊢ 2 \neq 0$
100	99	a1i	$⊢ (((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 2 \neq 0$
101	98 13 41 40 100	divcan5d	$⊢ (((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 \frac{2 (B C + \|A\| \sqrt{D})}{2 Q} = \frac{B C + \|A\| \sqrt{D}}{Q}$
102	97 101	eqtrd	$⊢ (((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 \frac{- (- 2 B C) + \sqrt{{(- 2 B C)}^{2} - 4 Q (C^{2} - A^{2} R^{2})}}{2 Q} = \frac{B C + \|A\| \sqrt{D}}{Q}$
103	102	eqeq2d	$⊢ (((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 (Y = \frac{- (- 2 B C) + \sqrt{{(- 2 B C)}^{2} - 4 Q (C^{2} - A^{2} R^{2})}}{2 Q} \leftrightarrow Y = \frac{B C + \|A\| \sqrt{D}}{Q})$
104	85	oveq2d	$⊢ (((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 2 B C - 2 \|A\| \sqrt{D} = 2 B C - 2 \|A\| \sqrt{D}$
105	87 92	oveq12d	$⊢ (((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 - (- 2 B C) - \sqrt{{(- 2 B C)}^{2} - 4 Q (C^{2} - A^{2} R^{2})} = 2 B C - 2 \|A\| \sqrt{D}$
106	41 50 94	subdid	$⊢ (((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 2 (B C - \|A\| \sqrt{D}) = 2 B C - 2 \|A\| \sqrt{D}$
107	104 105 106	3eqtr4d	$⊢ (((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 - (- 2 B C) - \sqrt{{(- 2 B C)}^{2} - 4 Q (C^{2} - A^{2} R^{2})} = 2 (B C - \|A\| \sqrt{D})$
108	107	oveq1d	$⊢ (((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 \frac{- (- 2 B C) - \sqrt{{(- 2 B C)}^{2} - 4 Q (C^{2} - A^{2} R^{2})}}{2 Q} = \frac{2 (B C - \|A\| \sqrt{D})}{2 Q}$
109	50 94	subcld	$⊢ (((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 B C - \|A\| \sqrt{D} \in ℂ$
110	109 13 41 40 100	divcan5d	$⊢ (((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 \frac{2 (B C - \|A\| \sqrt{D})}{2 Q} = \frac{B C - \|A\| \sqrt{D}}{Q}$
111	108 110	eqtrd	$⊢ (((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 \frac{- (- 2 B C) - \sqrt{{(- 2 B C)}^{2} - 4 Q (C^{2} - A^{2} R^{2})}}{2 Q} = \frac{B C - \|A\| \sqrt{D}}{Q}$
112	111	eqeq2d	$⊢ (((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 (Y = \frac{- (- 2 B C) - \sqrt{{(- 2 B C)}^{2} - 4 Q (C^{2} - A^{2} R^{2})}}{2 Q} \leftrightarrow Y = \frac{B C - \|A\| \sqrt{D}}{Q})$
113	103 112	orbi12d	$⊢ (((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 ((Y = \frac{- (- 2 B C) + \sqrt{{(- 2 B C)}^{2} - 4 Q (C^{2} - A^{2} R^{2})}}{2 Q} \lor Y = \frac{- (- 2 B C) - \sqrt{{(- 2 B C)}^{2} - 4 Q (C^{2} - A^{2} R^{2})}}{2 Q}) \leftrightarrow (Y = \frac{B C + \|A\| \sqrt{D}}{Q} \lor Y = \frac{B C - \|A\| \sqrt{D}}{Q}))$
114	69 113	bitrd	$⊢ (((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 (Q Y^{2} + (- 2 B C) Y + (C^{2} - A^{2} R^{2}) = 0 \leftrightarrow (Y = \frac{B C + \|A\| \sqrt{D}}{Q} \lor Y = \frac{B C - \|A\| \sqrt{D}}{Q}))$
115		absid	$⊢ (A \in ℝ \land 0 \leq A) \to \|A\| = A$
116	115	ex	$⊢ A \in ℝ \to (0 \leq A \to \|A\| = A)$
117	116	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (0 \leq A \to \|A\| = A)$
118	117	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0)) \to (0 \leq A \to \|A\| = A)$
119	118	3ad2ant1	$⊢ (((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 (0 \leq A \to \|A\| = A)$
120	119	impcom	$⊢ (0 \leq A \land (((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 \|A\| = A$
121	120	oveq1d	$⊢ (0 \leq A \land (((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 \|A\| \sqrt{D} = A \sqrt{D}$
122	121	oveq2d	$⊢ (0 \leq A \land (((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 B C + \|A\| \sqrt{D} = B C + A \sqrt{D}$
123	122	oveq1d	$⊢ (0 \leq A \land (((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 \frac{B C + \|A\| \sqrt{D}}{Q} = \frac{B C + A \sqrt{D}}{Q}$
124	123	eqeq2d	$⊢ (0 \leq A \land (((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 (Y = \frac{B C + \|A\| \sqrt{D}}{Q} \leftrightarrow Y = \frac{B C + A \sqrt{D}}{Q})$
125	121	oveq2d	$⊢ (0 \leq A \land (((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 B C - \|A\| \sqrt{D} = B C - A \sqrt{D}$
126	125	oveq1d	$⊢ (0 \leq A \land (((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 \frac{B C - \|A\| \sqrt{D}}{Q} = \frac{B C - A \sqrt{D}}{Q}$
127	126	eqeq2d	$⊢ (0 \leq A \land (((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 (Y = \frac{B C - \|A\| \sqrt{D}}{Q} \leftrightarrow Y = \frac{B C - A \sqrt{D}}{Q})$
128	124 127	orbi12d	$⊢ (0 \leq A \land (((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 ((Y = \frac{B C + \|A\| \sqrt{D}}{Q} \lor Y = \frac{B C - \|A\| \sqrt{D}}{Q}) \leftrightarrow (Y = \frac{B C + A \sqrt{D}}{Q} \lor Y = \frac{B C - A \sqrt{D}}{Q}))$
129		pm1.4	$⊢ (Y = \frac{B C + A \sqrt{D}}{Q} \lor Y = \frac{B C - A \sqrt{D}}{Q}) \to (Y = \frac{B C - A \sqrt{D}}{Q} \lor Y = \frac{B C + A \sqrt{D}}{Q})$
130	128 129	biimtrdi	$⊢ (0 \leq A \land (((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 ((Y = \frac{B C + \|A\| \sqrt{D}}{Q} \lor Y = \frac{B C - \|A\| \sqrt{D}}{Q}) \to (Y = \frac{B C - A \sqrt{D}}{Q} \lor Y = \frac{B C + A \sqrt{D}}{Q}))$
131	50	adantl	$⊢ (\neg 0 \leq A \land (((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 B C \in ℂ$
132	94	adantl	$⊢ (\neg 0 \leq A \land (((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 \|A\| \sqrt{D} \in ℂ$
133	131 132	subnegd	$⊢ (\neg 0 \leq A \land (((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 B C - (- \|A\| \sqrt{D}) = B C + \|A\| \sqrt{D}$
134	74	adantl	$⊢ (\neg 0 \leq A \land (((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 \|A\| \in ℂ$
135	84	adantl	$⊢ (\neg 0 \leq A \land (((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 \sqrt{D} \in ℂ$
136	134 135	mulneg1d	$⊢ (\neg 0 \leq A \land (((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 (- \|A\|) \sqrt{D} = - \|A\| \sqrt{D}$
137	89	simp1d	$⊢ (((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 A \in ℝ$
138	137	adantl	$⊢ (\neg 0 \leq A \land (((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 A \in ℝ$
139		id	$⊢ A \in ℝ \to A \in ℝ$
140		0red	$⊢ A \in ℝ \to 0 \in ℝ$
141	139 140	ltnled	$⊢ A \in ℝ \to (A < 0 \leftrightarrow \neg 0 \leq A)$
142		ltle	$⊢ (A \in ℝ \land 0 \in ℝ) \to (A < 0 \to A \leq 0)$
143	140 142	mpdan	$⊢ A \in ℝ \to (A < 0 \to A \leq 0)$
144	141 143	sylbird	$⊢ A \in ℝ \to (\neg 0 \leq A \to A \leq 0)$
145	144	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (\neg 0 \leq A \to A \leq 0)$
146	145	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0)) \to (\neg 0 \leq A \to A \leq 0)$
147	146	3ad2ant1	$⊢ (((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 (\neg 0 \leq A \to A \leq 0)$
148	147	impcom	$⊢ (\neg 0 \leq A \land (((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 A \leq 0$
149	138 148	absnidd	$⊢ (\neg 0 \leq A \land (((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 \|A\| = - A$
150	149	negeqd	$⊢ (\neg 0 \leq A \land (((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 - \|A\| = - (- A)$
151	57	adantl	$⊢ (\neg 0 \leq A \land (((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 A \in ℂ$
152	151	negnegd	$⊢ (\neg 0 \leq A \land (((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 - (- A) = A$
153	150 152	eqtrd	$⊢ (\neg 0 \leq A \land (((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 - \|A\| = A$
154	153	oveq1d	$⊢ (\neg 0 \leq A \land (((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 (- \|A\|) \sqrt{D} = A \sqrt{D}$
155	136 154	eqtr3d	$⊢ (\neg 0 \leq A \land (((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 - \|A\| \sqrt{D} = A \sqrt{D}$
156	155	oveq2d	$⊢ (\neg 0 \leq A \land (((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 B C - (- \|A\| \sqrt{D}) = B C - A \sqrt{D}$
157	133 156	eqtr3d	$⊢ (\neg 0 \leq A \land (((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 B C + \|A\| \sqrt{D} = B C - A \sqrt{D}$
158	157	oveq1d	$⊢ (\neg 0 \leq A \land (((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 \frac{B C + \|A\| \sqrt{D}}{Q} = \frac{B C - A \sqrt{D}}{Q}$
159	158	eqeq2d	$⊢ (\neg 0 \leq A \land (((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 (Y = \frac{B C + \|A\| \sqrt{D}}{Q} \leftrightarrow Y = \frac{B C - A \sqrt{D}}{Q})$
160	131 132	negsubd	$⊢ (\neg 0 \leq A \land (((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 B C + (- \|A\| \sqrt{D}) = B C - \|A\| \sqrt{D}$
161	155	oveq2d	$⊢ (\neg 0 \leq A \land (((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 B C + (- \|A\| \sqrt{D}) = B C + A \sqrt{D}$
162	160 161	eqtr3d	$⊢ (\neg 0 \leq A \land (((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 B C - \|A\| \sqrt{D} = B C + A \sqrt{D}$
163	162	oveq1d	$⊢ (\neg 0 \leq A \land (((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 \frac{B C - \|A\| \sqrt{D}}{Q} = \frac{B C + A \sqrt{D}}{Q}$
164	163	eqeq2d	$⊢ (\neg 0 \leq A \land (((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 (Y = \frac{B C - \|A\| \sqrt{D}}{Q} \leftrightarrow Y = \frac{B C + A \sqrt{D}}{Q})$
165	159 164	orbi12d	$⊢ (\neg 0 \leq A \land (((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 ((Y = \frac{B C + \|A\| \sqrt{D}}{Q} \lor Y = \frac{B C - \|A\| \sqrt{D}}{Q}) \leftrightarrow (Y = \frac{B C - A \sqrt{D}}{Q} \lor Y = \frac{B C + A \sqrt{D}}{Q}))$
166	165	biimpd	$⊢ (\neg 0 \leq A \land (((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 ((Y = \frac{B C + \|A\| \sqrt{D}}{Q} \lor Y = \frac{B C - \|A\| \sqrt{D}}{Q}) \to (Y = \frac{B C - A \sqrt{D}}{Q} \lor Y = \frac{B C + A \sqrt{D}}{Q}))$
167	130 166	pm2.61ian	$⊢ (((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 ((Y = \frac{B C + \|A\| \sqrt{D}}{Q} \lor Y = \frac{B C - \|A\| \sqrt{D}}{Q}) \to (Y = \frac{B C - A \sqrt{D}}{Q} \lor Y = \frac{B C + A \sqrt{D}}{Q}))$
168	114 167	sylbid	$⊢ (((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 (Q Y^{2} + (- 2 B C) Y + (C^{2} - A^{2} R^{2}) = 0 \to (Y = \frac{B C - A \sqrt{D}}{Q} \lor Y = \frac{B C + A \sqrt{D}}{Q}))$
169	7 168	syld	$⊢ (((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 (Y = \frac{B C - A \sqrt{D}}{Q} \lor Y = \frac{B C + A \sqrt{D}}{Q}))$

Metamath Proof Explorer

Theorem itsclc0yqsol

Proof