itscnhlc0xyqsol

Description: Lemma for itsclc0 . Solutions of the quadratic equations for the coordinates of the intersection points of a nonhorizontal line and a circle. (Contributed by AV, 8-Feb-2023)

	Ref	Expression
Hypotheses	itscnhlc0yqe.q	$⊢ Q = A^{2} + B^{2}$
	itsclc0yqsol.d	$⊢ D = R^{2} Q - C^{2}$
Assertion	itscnhlc0xyqsol	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \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 ((X = \frac{A C + B \sqrt{D}}{Q} \land Y = \frac{B C - A \sqrt{D}}{Q}) \lor (X = \frac{A C - B \sqrt{D}}{Q} \land 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		simpl	$⊢ (A \in ℝ \land A \neq 0) \to A \in ℝ$
4	3	3anim1i	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to (A \in ℝ \land B \in ℝ \land C \in ℝ)$
5		simpr	$⊢ (A \in ℝ \land A \neq 0) \to A \neq 0$
6	5	3ad2ant1	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to A \neq 0$
7	6	orcd	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to (A \neq 0 \lor B \neq 0)$
8	4 7	jca	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0))$
9	8	3anim1i	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (((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 ℝ))$
10	1 2	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}))$
11	9 10	syl	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \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}))$
12	11	imp	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land (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})$
13		oveq2	$⊢ Y = \frac{B C - A \sqrt{D}}{Q} \to B Y = B (\frac{B C - A \sqrt{D}}{Q})$
14	13	oveq2d	$⊢ Y = \frac{B C - A \sqrt{D}}{Q} \to A X + B Y = A X + B (\frac{B C - A \sqrt{D}}{Q})$
15	14	eqeq1d	$⊢ Y = \frac{B C - A \sqrt{D}}{Q} \to (A X + B Y = C \leftrightarrow A X + B (\frac{B C - A \sqrt{D}}{Q}) = C)$
16		simp12	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B \in ℝ$
17	16	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B \in ℂ$
18		simp13	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to C \in ℝ$
19	18	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to C \in ℂ$
20	17 19	mulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B C \in ℂ$
21		simp11l	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to A \in ℝ$
22	21	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to A \in ℂ$
23		rpre	$⊢ R \in ℝ^{+} \to R \in ℝ$
24	23	adantr	$⊢ (R \in ℝ^{+} \land 0 \leq D) \to R \in ℝ$
25	24	adantl	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to R \in ℝ$
26	25	resqcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to R^{2} \in ℝ$
27		simp1l	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to A \in ℝ$
28		simp2	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to B \in ℝ$
29	1	resum2sqcl	$⊢ (A \in ℝ \land B \in ℝ) \to Q \in ℝ$
30	27 28 29	syl2anc	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to Q \in ℝ$
31	30	adantr	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q \in ℝ$
32	26 31	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to R^{2} Q \in ℝ$
33		simpl3	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to C \in ℝ$
34	33	resqcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to C^{2} \in ℝ$
35	32 34	resubcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to R^{2} Q - C^{2} \in ℝ$
36	2 35	eqeltrid	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to D \in ℝ$
37	36	3adant3	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to D \in ℝ$
38	37	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to D \in ℂ$
39	38	sqrtcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \sqrt{D} \in ℂ$
40	22 39	mulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to A \sqrt{D} \in ℂ$
41	20 40	subcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B C - A \sqrt{D} \in ℂ$
42	30	3ad2ant1	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to Q \in ℝ$
43	42	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to Q \in ℂ$
44	1	resum2sqgt0	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ) \to 0 < Q$
45	44	3adant3	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to 0 < Q$
46	45	gt0ne0d	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to Q \neq 0$
47	46	3ad2ant1	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to Q \neq 0$
48	17 41 43 47	divassd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{B (B C - A \sqrt{D})}{Q} = B (\frac{B C - A \sqrt{D}}{Q})$
49	48	eqcomd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B (\frac{B C - A \sqrt{D}}{Q}) = \frac{B (B C - A \sqrt{D})}{Q}$
50	49	oveq2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to A X + B (\frac{B C - A \sqrt{D}}{Q}) = A X + (\frac{B (B C - A \sqrt{D})}{Q})$
51	19 43 47	divcan3d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{Q C}{Q} = C$
52	51	eqcomd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to C = \frac{Q C}{Q}$
53	50 52	eqeq12d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (A X + B (\frac{B C - A \sqrt{D}}{Q}) = C \leftrightarrow A X + (\frac{B (B C - A \sqrt{D})}{Q}) = \frac{Q C}{Q})$
54	43 19	mulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to Q C \in ℂ$
55	17 41	mulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B (B C - A \sqrt{D}) \in ℂ$
56	54 55 43 47	divsubdird	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{Q C - B (B C - A \sqrt{D})}{Q} = (\frac{Q C}{Q}) - (\frac{B (B C - A \sqrt{D})}{Q})$
57	56	eqcomd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (\frac{Q C}{Q}) - (\frac{B (B C - A \sqrt{D})}{Q}) = \frac{Q C - B (B C - A \sqrt{D})}{Q}$
58	57	eqeq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to ((\frac{Q C}{Q}) - (\frac{B (B C - A \sqrt{D})}{Q}) = A X \leftrightarrow \frac{Q C - B (B C - A \sqrt{D})}{Q} = A X)$
59	54 43 47	divcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{Q C}{Q} \in ℂ$
60	55 43 47	divcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{B (B C - A \sqrt{D})}{Q} \in ℂ$
61		simp3l	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to X \in ℝ$
62	61	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to X \in ℂ$
63	22 62	mulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to A X \in ℂ$
64	59 60 63	subadd2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to ((\frac{Q C}{Q}) - (\frac{B (B C - A \sqrt{D})}{Q}) = A X \leftrightarrow A X + (\frac{B (B C - A \sqrt{D})}{Q}) = \frac{Q C}{Q})$
65		eqcom	$⊢ \frac{\frac{Q C - B (B C - A \sqrt{D})}{Q}}{A} = X \leftrightarrow X = \frac{\frac{Q C - B (B C - A \sqrt{D})}{Q}}{A}$
66	65	a1i	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (\frac{\frac{Q C - B (B C - A \sqrt{D})}{Q}}{A} = X \leftrightarrow X = \frac{\frac{Q C - B (B C - A \sqrt{D})}{Q}}{A})$
67	54 55	subcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to Q C - B (B C - A \sqrt{D}) \in ℂ$
68	67 43 47	divcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{Q C - B (B C - A \sqrt{D})}{Q} \in ℂ$
69		simp11r	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to A \neq 0$
70	68 62 22 69	divmul2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (\frac{\frac{Q C - B (B C - A \sqrt{D})}{Q}}{A} = X \leftrightarrow \frac{Q C - B (B C - A \sqrt{D})}{Q} = A X)$
71	67 43 22 47 69	divdiv1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{\frac{Q C - B (B C - A \sqrt{D})}{Q}}{A} = \frac{Q C - B (B C - A \sqrt{D})}{Q A}$
72	71	eqeq2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (X = \frac{\frac{Q C - B (B C - A \sqrt{D})}{Q}}{A} \leftrightarrow X = \frac{Q C - B (B C - A \sqrt{D})}{Q A})$
73	66 70 72	3bitr3d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (\frac{Q C - B (B C - A \sqrt{D})}{Q} = A X \leftrightarrow X = \frac{Q C - B (B C - A \sqrt{D})}{Q A})$
74	58 64 73	3bitr3d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (A X + (\frac{B (B C - A \sqrt{D})}{Q}) = \frac{Q C}{Q} \leftrightarrow X = \frac{Q C - B (B C - A \sqrt{D})}{Q A})$
75	53 74	bitrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (A X + B (\frac{B C - A \sqrt{D}}{Q}) = C \leftrightarrow X = \frac{Q C - B (B C - A \sqrt{D})}{Q A})$
76	15 75	sylan9bbr	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land Y = \frac{B C - A \sqrt{D}}{Q}) \to (A X + B Y = C \leftrightarrow X = \frac{Q C - B (B C - A \sqrt{D})}{Q A})$
77	1	oveq1i	$⊢ Q C = (A^{2} + B^{2}) C$
78	27	recnd	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to A \in ℂ$
79	78	sqcld	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to A^{2} \in ℂ$
80	28	recnd	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to B \in ℂ$
81	80	sqcld	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to B^{2} \in ℂ$
82		simp3	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to C \in ℝ$
83	82	recnd	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to C \in ℂ$
84	79 81 83	adddird	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to (A^{2} + B^{2}) C = A^{2} C + B^{2} C$
85	77 84	syl5eq	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to Q C = A^{2} C + B^{2} C$
86	85	adantr	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q C = A^{2} C + B^{2} C$
87	80	adantr	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to B \in ℂ$
88	33	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to C \in ℂ$
89	87 88	mulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to B C \in ℂ$
90	78	adantr	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to A \in ℂ$
91	36	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to D \in ℂ$
92	91	sqrtcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to \sqrt{D} \in ℂ$
93	90 92	mulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to A \sqrt{D} \in ℂ$
94	87 89 93	subdid	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to B (B C - A \sqrt{D}) = B B C - B A \sqrt{D}$
95	80 80 83	mulassd	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to B B C = B B C$
96		recn	$⊢ B \in ℝ \to B \in ℂ$
97	96	sqvald	$⊢ B \in ℝ \to B^{2} = B B$
98	97	3ad2ant2	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to B^{2} = B B$
99	98	eqcomd	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to B B = B^{2}$
100	99	oveq1d	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to B B C = B^{2} C$
101	95 100	eqtr3d	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to B B C = B^{2} C$
102	101	adantr	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to B B C = B^{2} C$
103	87 90 92	mul12d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to B A \sqrt{D} = A B \sqrt{D}$
104	102 103	oveq12d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to B B C - B A \sqrt{D} = B^{2} C - A B \sqrt{D}$
105	94 104	eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to B (B C - A \sqrt{D}) = B^{2} C - A B \sqrt{D}$
106	86 105	oveq12d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q C - B (B C - A \sqrt{D}) = A^{2} C + B^{2} C - (B^{2} C - A B \sqrt{D})$
107	90	sqcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} \in ℂ$
108	107 88	mulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C \in ℂ$
109	87	sqcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} \in ℂ$
110	109 88	mulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} C \in ℂ$
111	108 110	addcomd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C + B^{2} C = B^{2} C + A^{2} C$
112	111	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C + B^{2} C - (B^{2} C - A B \sqrt{D}) = B^{2} C + A^{2} C - (B^{2} C - A B \sqrt{D})$
113	87 92	mulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to B \sqrt{D} \in ℂ$
114	90 113	mulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to A B \sqrt{D} \in ℂ$
115	110 108 114	pnncand	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} C + A^{2} C - (B^{2} C - A B \sqrt{D}) = A^{2} C + A B \sqrt{D}$
116	106 112 115	3eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q C - B (B C - A \sqrt{D}) = A^{2} C + A B \sqrt{D}$
117	116	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{Q C - B (B C - A \sqrt{D})}{Q A} = \frac{A^{2} C + A B \sqrt{D}}{Q A}$
118	78	sqvald	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to A^{2} = A A$
119	118	oveq1d	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to A^{2} C = A A C$
120	78 78 83	mulassd	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to A A C = A A C$
121	119 120	eqtrd	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to A^{2} C = A A C$
122	121	adantr	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C = A A C$
123	122	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C + A B \sqrt{D} = A A C + A B \sqrt{D}$
124	31	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q \in ℂ$
125	124 90	mulcomd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q A = A Q$
126	123 125	oveq12d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{A^{2} C + A B \sqrt{D}}{Q A} = \frac{A A C + A B \sqrt{D}}{A Q}$
127	90 88	mulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to A C \in ℂ$
128	90 127 113	adddid	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to A (A C + B \sqrt{D}) = A A C + A B \sqrt{D}$
129	128	eqcomd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to A A C + A B \sqrt{D} = A (A C + B \sqrt{D})$
130	129	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{A A C + A B \sqrt{D}}{A Q} = \frac{A (A C + B \sqrt{D})}{A Q}$
131	127 113	addcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to A C + B \sqrt{D} \in ℂ$
132	46	adantr	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q \neq 0$
133		simpl1r	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to A \neq 0$
134	131 124 90 132 133	divcan5d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{A (A C + B \sqrt{D})}{A Q} = \frac{A C + B \sqrt{D}}{Q}$
135	130 134	eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{A A C + A B \sqrt{D}}{A Q} = \frac{A C + B \sqrt{D}}{Q}$
136	117 126 135	3eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{Q C - B (B C - A \sqrt{D})}{Q A} = \frac{A C + B \sqrt{D}}{Q}$
137	136	eqeq2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to (X = \frac{Q C - B (B C - A \sqrt{D})}{Q A} \leftrightarrow X = \frac{A C + B \sqrt{D}}{Q})$
138	137	biimpd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to (X = \frac{Q C - B (B C - A \sqrt{D})}{Q A} \to X = \frac{A C + B \sqrt{D}}{Q})$
139	138	3adant3	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (X = \frac{Q C - B (B C - A \sqrt{D})}{Q A} \to X = \frac{A C + B \sqrt{D}}{Q})$
140	139	adantr	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land Y = \frac{B C - A \sqrt{D}}{Q}) \to (X = \frac{Q C - B (B C - A \sqrt{D})}{Q A} \to X = \frac{A C + B \sqrt{D}}{Q})$
141	76 140	sylbid	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land Y = \frac{B C - A \sqrt{D}}{Q}) \to (A X + B Y = C \to X = \frac{A C + B \sqrt{D}}{Q})$
142	141	ex	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (Y = \frac{B C - A \sqrt{D}}{Q} \to (A X + B Y = C \to X = \frac{A C + B \sqrt{D}}{Q}))$
143	142	com23	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (A X + B Y = C \to (Y = \frac{B C - A \sqrt{D}}{Q} \to X = \frac{A C + B \sqrt{D}}{Q}))$
144	143	adantld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \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} \to X = \frac{A C + B \sqrt{D}}{Q}))$
145	144	imp	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land (X^{2} + Y^{2} = R^{2} \land A X + B Y = C)) \to (Y = \frac{B C - A \sqrt{D}}{Q} \to X = \frac{A C + B \sqrt{D}}{Q})$
146	145	ancrd	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land (X^{2} + Y^{2} = R^{2} \land A X + B Y = C)) \to (Y = \frac{B C - A \sqrt{D}}{Q} \to (X = \frac{A C + B \sqrt{D}}{Q} \land Y = \frac{B C - A \sqrt{D}}{Q}))$
147		oveq2	$⊢ Y = \frac{B C + A \sqrt{D}}{Q} \to B Y = B (\frac{B C + A \sqrt{D}}{Q})$
148	147	oveq2d	$⊢ Y = \frac{B C + A \sqrt{D}}{Q} \to A X + B Y = A X + B (\frac{B C + A \sqrt{D}}{Q})$
149	148	eqeq1d	$⊢ Y = \frac{B C + A \sqrt{D}}{Q} \to (A X + B Y = C \leftrightarrow A X + B (\frac{B C + A \sqrt{D}}{Q}) = C)$
150	20 40	addcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B C + A \sqrt{D} \in ℂ$
151	17 150 43 47	divassd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{B (B C + A \sqrt{D})}{Q} = B (\frac{B C + A \sqrt{D}}{Q})$
152	151	eqcomd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B (\frac{B C + A \sqrt{D}}{Q}) = \frac{B (B C + A \sqrt{D})}{Q}$
153	152	oveq2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to A X + B (\frac{B C + A \sqrt{D}}{Q}) = A X + (\frac{B (B C + A \sqrt{D})}{Q})$
154	153 52	eqeq12d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (A X + B (\frac{B C + A \sqrt{D}}{Q}) = C \leftrightarrow A X + (\frac{B (B C + A \sqrt{D})}{Q}) = \frac{Q C}{Q})$
155	17 150	mulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B (B C + A \sqrt{D}) \in ℂ$
156	54 155 43 47	divsubdird	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{Q C - B (B C + A \sqrt{D})}{Q} = (\frac{Q C}{Q}) - (\frac{B (B C + A \sqrt{D})}{Q})$
157	156	eqcomd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (\frac{Q C}{Q}) - (\frac{B (B C + A \sqrt{D})}{Q}) = \frac{Q C - B (B C + A \sqrt{D})}{Q}$
158	157	eqeq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to ((\frac{Q C}{Q}) - (\frac{B (B C + A \sqrt{D})}{Q}) = A X \leftrightarrow \frac{Q C - B (B C + A \sqrt{D})}{Q} = A X)$
159	155 43 47	divcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{B (B C + A \sqrt{D})}{Q} \in ℂ$
160	59 159 63	subadd2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to ((\frac{Q C}{Q}) - (\frac{B (B C + A \sqrt{D})}{Q}) = A X \leftrightarrow A X + (\frac{B (B C + A \sqrt{D})}{Q}) = \frac{Q C}{Q})$
161		eqcom	$⊢ \frac{\frac{Q C - B (B C + A \sqrt{D})}{Q}}{A} = X \leftrightarrow X = \frac{\frac{Q C - B (B C + A \sqrt{D})}{Q}}{A}$
162	161	a1i	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (\frac{\frac{Q C - B (B C + A \sqrt{D})}{Q}}{A} = X \leftrightarrow X = \frac{\frac{Q C - B (B C + A \sqrt{D})}{Q}}{A})$
163	54 155	subcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to Q C - B (B C + A \sqrt{D}) \in ℂ$
164	163 43 47	divcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{Q C - B (B C + A \sqrt{D})}{Q} \in ℂ$
165	164 62 22 69	divmul2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (\frac{\frac{Q C - B (B C + A \sqrt{D})}{Q}}{A} = X \leftrightarrow \frac{Q C - B (B C + A \sqrt{D})}{Q} = A X)$
166	163 43 22 47 69	divdiv1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{\frac{Q C - B (B C + A \sqrt{D})}{Q}}{A} = \frac{Q C - B (B C + A \sqrt{D})}{Q A}$
167	166	eqeq2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (X = \frac{\frac{Q C - B (B C + A \sqrt{D})}{Q}}{A} \leftrightarrow X = \frac{Q C - B (B C + A \sqrt{D})}{Q A})$
168	162 165 167	3bitr3d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (\frac{Q C - B (B C + A \sqrt{D})}{Q} = A X \leftrightarrow X = \frac{Q C - B (B C + A \sqrt{D})}{Q A})$
169	158 160 168	3bitr3d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (A X + (\frac{B (B C + A \sqrt{D})}{Q}) = \frac{Q C}{Q} \leftrightarrow X = \frac{Q C - B (B C + A \sqrt{D})}{Q A})$
170	154 169	bitrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (A X + B (\frac{B C + A \sqrt{D}}{Q}) = C \leftrightarrow X = \frac{Q C - B (B C + A \sqrt{D})}{Q A})$
171	149 170	sylan9bbr	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land Y = \frac{B C + A \sqrt{D}}{Q}) \to (A X + B Y = C \leftrightarrow X = \frac{Q C - B (B C + A \sqrt{D})}{Q A})$
172	87 89 93	adddid	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to B (B C + A \sqrt{D}) = B B C + B A \sqrt{D}$
173	102 103	oveq12d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to B B C + B A \sqrt{D} = B^{2} C + A B \sqrt{D}$
174	172 173	eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to B (B C + A \sqrt{D}) = B^{2} C + A B \sqrt{D}$
175	86 174	oveq12d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q C - B (B C + A \sqrt{D}) = A^{2} C + B^{2} C - (B^{2} C + A B \sqrt{D})$
176	111	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C + B^{2} C - (B^{2} C + A B \sqrt{D}) = B^{2} C + A^{2} C - (B^{2} C + A B \sqrt{D})$
177	110 108 114	pnpcand	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} C + A^{2} C - (B^{2} C + A B \sqrt{D}) = A^{2} C - A B \sqrt{D}$
178	175 176 177	3eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q C - B (B C + A \sqrt{D}) = A^{2} C - A B \sqrt{D}$
179	178	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{Q C - B (B C + A \sqrt{D})}{Q A} = \frac{A^{2} C - A B \sqrt{D}}{Q A}$
180	122	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C - A B \sqrt{D} = A A C - A B \sqrt{D}$
181	180 125	oveq12d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{A^{2} C - A B \sqrt{D}}{Q A} = \frac{A A C - A B \sqrt{D}}{A Q}$
182	90 127 113	subdid	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to A (A C - B \sqrt{D}) = A A C - A B \sqrt{D}$
183	182	eqcomd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to A A C - A B \sqrt{D} = A (A C - B \sqrt{D})$
184	183	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{A A C - A B \sqrt{D}}{A Q} = \frac{A (A C - B \sqrt{D})}{A Q}$
185	127 113	subcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to A C - B \sqrt{D} \in ℂ$
186	185 124 90 132 133	divcan5d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{A (A C - B \sqrt{D})}{A Q} = \frac{A C - B \sqrt{D}}{Q}$
187	184 186	eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{A A C - A B \sqrt{D}}{A Q} = \frac{A C - B \sqrt{D}}{Q}$
188	179 181 187	3eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{Q C - B (B C + A \sqrt{D})}{Q A} = \frac{A C - B \sqrt{D}}{Q}$
189	188	eqeq2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to (X = \frac{Q C - B (B C + A \sqrt{D})}{Q A} \leftrightarrow X = \frac{A C - B \sqrt{D}}{Q})$
190	189	biimpd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to (X = \frac{Q C - B (B C + A \sqrt{D})}{Q A} \to X = \frac{A C - B \sqrt{D}}{Q})$
191	190	3adant3	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (X = \frac{Q C - B (B C + A \sqrt{D})}{Q A} \to X = \frac{A C - B \sqrt{D}}{Q})$
192	191	adantr	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land Y = \frac{B C + A \sqrt{D}}{Q}) \to (X = \frac{Q C - B (B C + A \sqrt{D})}{Q A} \to X = \frac{A C - B \sqrt{D}}{Q})$
193	171 192	sylbid	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land Y = \frac{B C + A \sqrt{D}}{Q}) \to (A X + B Y = C \to X = \frac{A C - B \sqrt{D}}{Q})$
194	193	ex	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (Y = \frac{B C + A \sqrt{D}}{Q} \to (A X + B Y = C \to X = \frac{A C - B \sqrt{D}}{Q}))$
195	194	com23	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (A X + B Y = C \to (Y = \frac{B C + A \sqrt{D}}{Q} \to X = \frac{A C - B \sqrt{D}}{Q}))$
196	195	adantld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \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} \to X = \frac{A C - B \sqrt{D}}{Q}))$
197	196	imp	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land (X^{2} + Y^{2} = R^{2} \land A X + B Y = C)) \to (Y = \frac{B C + A \sqrt{D}}{Q} \to X = \frac{A C - B \sqrt{D}}{Q})$
198	197	ancrd	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land (X^{2} + Y^{2} = R^{2} \land A X + B Y = C)) \to (Y = \frac{B C + A \sqrt{D}}{Q} \to (X = \frac{A C - B \sqrt{D}}{Q} \land Y = \frac{B C + A \sqrt{D}}{Q}))$
199	146 198	orim12d	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land (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}) \to ((X = \frac{A C + B \sqrt{D}}{Q} \land Y = \frac{B C - A \sqrt{D}}{Q}) \lor (X = \frac{A C - B \sqrt{D}}{Q} \land Y = \frac{B C + A \sqrt{D}}{Q})))$
200	12 199	mpd	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land (X^{2} + Y^{2} = R^{2} \land A X + B Y = C)) \to ((X = \frac{A C + B \sqrt{D}}{Q} \land Y = \frac{B C - A \sqrt{D}}{Q}) \lor (X = \frac{A C - B \sqrt{D}}{Q} \land Y = \frac{B C + A \sqrt{D}}{Q}))$
201	200	ex	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \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 ((X = \frac{A C + B \sqrt{D}}{Q} \land Y = \frac{B C - A \sqrt{D}}{Q}) \lor (X = \frac{A C - B \sqrt{D}}{Q} \land Y = \frac{B C + A \sqrt{D}}{Q})))$

Metamath Proof Explorer

Theorem itscnhlc0xyqsol

Proof