itsclc0xyqsolr

Description: Lemma for itsclc0 . Solutions of the quadratic equations for the coordinates of the intersection points of a (nondegenerate) line and a circle. (Contributed by AV, 2-May-2023) (Revised by AV, 14-May-2023)

	Ref	Expression
Hypotheses	itsclc0xyqsolr.q	$⊢ Q = A^{2} + B^{2}$
	itsclc0xyqsolr.d	$⊢ D = R^{2} Q - C^{2}$
Assertion	itsclc0xyqsolr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \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})) \to (X^{2} + Y^{2} = R^{2} \land A X + B Y = C))$

Proof

Step	Hyp	Ref	Expression
1		itsclc0xyqsolr.q	$⊢ Q = A^{2} + B^{2}$
2		itsclc0xyqsolr.d	$⊢ D = R^{2} Q - C^{2}$
3		recn	$⊢ A \in ℝ \to A \in ℂ$
4	3	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A \in ℂ$
5	4	3ad2ant1	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A \in ℂ$
6		recn	$⊢ C \in ℝ \to C \in ℂ$
7	6	3ad2ant3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to C \in ℂ$
8	7	3ad2ant1	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to C \in ℂ$
9	5 8	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A C \in ℂ$
10		recn	$⊢ B \in ℝ \to B \in ℂ$
11	10	3ad2ant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B \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)) \to B \in ℂ$
13		rpre	$⊢ R \in ℝ^{+} \to R \in ℝ$
14	13	adantr	$⊢ (R \in ℝ^{+} \land 0 \leq D) \to R \in ℝ$
15	14	anim2i	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (R \in ℝ^{+} \land 0 \leq D)) \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ)$
16	15	3adant2	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ)$
17	1 2	itsclc0lem3	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ) \to D \in ℝ$
18	16 17	syl	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to D \in ℝ$
19	18	recnd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to D \in ℂ$
20	19	sqrtcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \sqrt{D} \in ℂ$
21	12 20	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B \sqrt{D} \in ℂ$
22	9 21	addcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A C + B \sqrt{D} \in ℂ$
23	1	resum2sqcl	$⊢ (A \in ℝ \land B \in ℝ) \to Q \in ℝ$
24	23	3adant3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to Q \in ℝ$
25	24	recnd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to Q \in ℂ$
26	25	3ad2ant1	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q \in ℂ$
27		simp11	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A \in ℝ$
28		simp12	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B \in ℝ$
29		simp2	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (A \neq 0 \lor B \neq 0)$
30	1	resum2sqorgt0	$⊢ (A \in ℝ \land B \in ℝ \land (A \neq 0 \lor B \neq 0)) \to 0 < Q$
31	27 28 29 30	syl3anc	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to 0 < Q$
32	31	gt0ne0d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q \neq 0$
33	22 26 32	sqdivd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(\frac{A C + B \sqrt{D}}{Q})}^{2} = \frac{{(A C + B \sqrt{D})}^{2}}{Q^{2}}$
34	4 7	mulcld	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A C \in ℂ$
35	34	3ad2ant1	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A C \in ℂ$
36		binom2	$⊢ (A C \in ℂ \land B \sqrt{D} \in ℂ) \to {(A C + B \sqrt{D})}^{2} = {A C}^{2} + 2 A C B \sqrt{D} + {B \sqrt{D}}^{2}$
37	35 21 36	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(A C + B \sqrt{D})}^{2} = {A C}^{2} + 2 A C B \sqrt{D} + {B \sqrt{D}}^{2}$
38	4 7	sqmuld	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to {A C}^{2} = A^{2} C^{2}$
39	38	3ad2ant1	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {A C}^{2} = A^{2} C^{2}$
40	39	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {A C}^{2} + 2 A C B \sqrt{D} = A^{2} C^{2} + 2 A C B \sqrt{D}$
41	12 20	sqmuld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {B \sqrt{D}}^{2} = B^{2} {\sqrt{D}}^{2}$
42		simp3r	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to 0 \leq D$
43		resqrtth	$⊢ (D \in ℝ \land 0 \leq D) \to {\sqrt{D}}^{2} = D$
44	18 42 43	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {\sqrt{D}}^{2} = D$
45	44	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} {\sqrt{D}}^{2} = B^{2} D$
46	41 45	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {B \sqrt{D}}^{2} = B^{2} D$
47	40 46	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {A C}^{2} + 2 A C B \sqrt{D} + {B \sqrt{D}}^{2} = A^{2} C^{2} + 2 A C B \sqrt{D} + B^{2} D$
48	37 47	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(A C + B \sqrt{D})}^{2} = A^{2} C^{2} + 2 A C B \sqrt{D} + B^{2} D$
49	48	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{{(A C + B \sqrt{D})}^{2}}{Q^{2}} = \frac{A^{2} C^{2} + 2 A C B \sqrt{D} + B^{2} D}{Q^{2}}$
50	33 49	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(\frac{A C + B \sqrt{D}}{Q})}^{2} = \frac{A^{2} C^{2} + 2 A C B \sqrt{D} + B^{2} D}{Q^{2}}$
51	12 8	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B C \in ℂ$
52	5 20	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A \sqrt{D} \in ℂ$
53	51 52	subcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B C - A \sqrt{D} \in ℂ$
54	53 26 32	sqdivd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(\frac{B C - A \sqrt{D}}{Q})}^{2} = \frac{{(B C - A \sqrt{D})}^{2}}{Q^{2}}$
55	27	recnd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A \in ℂ$
56	55 20	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A \sqrt{D} \in ℂ$
57		binom2sub	$⊢ (B C \in ℂ \land A \sqrt{D} \in ℂ) \to {(B C - A \sqrt{D})}^{2} = {B C}^{2} - 2 B C A \sqrt{D} + {A \sqrt{D}}^{2}$
58	51 56 57	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(B C - A \sqrt{D})}^{2} = {B C}^{2} - 2 B C A \sqrt{D} + {A \sqrt{D}}^{2}$
59	11 7	sqmuld	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to {B C}^{2} = B^{2} C^{2}$
60	59	3ad2ant1	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {B C}^{2} = B^{2} C^{2}$
61	12 8 55 20	mul4d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B C A \sqrt{D} = B A C \sqrt{D}$
62	12 55	mulcomd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B A = A B$
63	62	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B A C \sqrt{D} = A B C \sqrt{D}$
64	55 12 8 20	mul4d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A B C \sqrt{D} = A C B \sqrt{D}$
65	63 64	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B A C \sqrt{D} = A C B \sqrt{D}$
66	61 65	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B C A \sqrt{D} = A C B \sqrt{D}$
67	66	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to 2 B C A \sqrt{D} = 2 A C B \sqrt{D}$
68	60 67	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {B C}^{2} - 2 B C A \sqrt{D} = B^{2} C^{2} - 2 A C B \sqrt{D}$
69	55 20	sqmuld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {A \sqrt{D}}^{2} = A^{2} {\sqrt{D}}^{2}$
70	44	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} {\sqrt{D}}^{2} = A^{2} D$
71	69 70	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {A \sqrt{D}}^{2} = A^{2} D$
72	68 71	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {B C}^{2} - 2 B C A \sqrt{D} + {A \sqrt{D}}^{2} = B^{2} C^{2} - 2 A C B \sqrt{D} + A^{2} D$
73	58 72	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(B C - A \sqrt{D})}^{2} = B^{2} C^{2} - 2 A C B \sqrt{D} + A^{2} D$
74	73	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{{(B C - A \sqrt{D})}^{2}}{Q^{2}} = \frac{B^{2} C^{2} - 2 A C B \sqrt{D} + A^{2} D}{Q^{2}}$
75	54 74	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(\frac{B C - A \sqrt{D}}{Q})}^{2} = \frac{B^{2} C^{2} - 2 A C B \sqrt{D} + A^{2} D}{Q^{2}}$
76	50 75	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(\frac{A C + B \sqrt{D}}{Q})}^{2} + {(\frac{B C - A \sqrt{D}}{Q})}^{2} = (\frac{A^{2} C^{2} + 2 A C B \sqrt{D} + B^{2} D}{Q^{2}}) + (\frac{B^{2} C^{2} - 2 A C B \sqrt{D} + A^{2} D}{Q^{2}})$
77	5	sqcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} \in ℂ$
78	8	sqcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to C^{2} \in ℂ$
79	77 78	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C^{2} \in ℂ$
80		2cnd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to 2 \in ℂ$
81	9 21	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A C B \sqrt{D} \in ℂ$
82	80 81	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to 2 A C B \sqrt{D} \in ℂ$
83	79 82	addcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C^{2} + 2 A C B \sqrt{D} \in ℂ$
84	12	sqcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} \in ℂ$
85	84 19	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} D \in ℂ$
86	83 85	addcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C^{2} + 2 A C B \sqrt{D} + B^{2} D \in ℂ$
87	84 78	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} C^{2} \in ℂ$
88	87 82	subcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} C^{2} - 2 A C B \sqrt{D} \in ℂ$
89	77 19	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} D \in ℂ$
90	88 89	addcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} C^{2} - 2 A C B \sqrt{D} + A^{2} D \in ℂ$
91	26	sqcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q^{2} \in ℂ$
92		2z	$⊢ 2 \in ℤ$
93	92	a1i	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to 2 \in ℤ$
94	26 32 93	expne0d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q^{2} \neq 0$
95	86 90 91 94	divdird	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{(A^{2} C^{2} + 2 A C B \sqrt{D}) + B^{2} D + (B^{2} C^{2} - 2 A C B \sqrt{D}) + A^{2} D}{Q^{2}} = (\frac{A^{2} C^{2} + 2 A C B \sqrt{D} + B^{2} D}{Q^{2}}) + (\frac{B^{2} C^{2} - 2 A C B \sqrt{D} + A^{2} D}{Q^{2}})$
96	83 85 88 89	add4d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (A^{2} C^{2} + 2 A C B \sqrt{D}) + B^{2} D + (B^{2} C^{2} - 2 A C B \sqrt{D}) + A^{2} D = (A^{2} C^{2} + 2 A C B \sqrt{D}) + (B^{2} C^{2} - 2 A C B \sqrt{D}) + B^{2} D + A^{2} D$
97	79 82 87	ppncand	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C^{2} + 2 A C B \sqrt{D} + (B^{2} C^{2} - 2 A C B \sqrt{D}) = A^{2} C^{2} + B^{2} C^{2}$
98	55	sqcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} \in ℂ$
99	98 84 78	adddird	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (A^{2} + B^{2}) C^{2} = A^{2} C^{2} + B^{2} C^{2}$
100	1	eqcomi	$⊢ A^{2} + B^{2} = Q$
101	100	a1i	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} + B^{2} = Q$
102	101	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (A^{2} + B^{2}) C^{2} = Q C^{2}$
103	97 99 102	3eqtr2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C^{2} + 2 A C B \sqrt{D} + (B^{2} C^{2} - 2 A C B \sqrt{D}) = Q C^{2}$
104	84 98 19	adddird	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (B^{2} + A^{2}) D = B^{2} D + A^{2} D$
105	84 98	addcomd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} + A^{2} = A^{2} + B^{2}$
106	105 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)) \to B^{2} + A^{2} = Q$
107	106	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (B^{2} + A^{2}) D = Q D$
108	104 107	eqtr3d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} D + A^{2} D = Q D$
109	103 108	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (A^{2} C^{2} + 2 A C B \sqrt{D}) + (B^{2} C^{2} - 2 A C B \sqrt{D}) + B^{2} D + A^{2} D = Q C^{2} + Q D$
110	96 109	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (A^{2} C^{2} + 2 A C B \sqrt{D}) + B^{2} D + (B^{2} C^{2} - 2 A C B \sqrt{D}) + A^{2} D = Q C^{2} + Q D$
111	110	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{(A^{2} C^{2} + 2 A C B \sqrt{D}) + B^{2} D + (B^{2} C^{2} - 2 A C B \sqrt{D}) + A^{2} D}{Q^{2}} = \frac{Q C^{2} + Q D}{Q^{2}}$
112	26 78 19	adddid	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q (C^{2} + D) = Q C^{2} + Q D$
113	112	eqcomd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q C^{2} + Q D = Q (C^{2} + D)$
114	26	sqvald	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q^{2} = Q Q$
115	113 114	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{Q C^{2} + Q D}{Q^{2}} = \frac{Q (C^{2} + D)}{Q Q}$
116	78 19	addcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to C^{2} + D \in ℂ$
117	116 26 26 32 32	divcan5d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{Q (C^{2} + D)}{Q Q} = \frac{C^{2} + D}{Q}$
118	115 117	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{Q C^{2} + Q D}{Q^{2}} = \frac{C^{2} + D}{Q}$
119	2	a1i	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to D = R^{2} Q - C^{2}$
120	119	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to C^{2} + D = C^{2} + R^{2} Q - C^{2}$
121		rpcn	$⊢ R \in ℝ^{+} \to R \in ℂ$
122	121	adantr	$⊢ (R \in ℝ^{+} \land 0 \leq D) \to R \in ℂ$
123	122	3ad2ant3	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to R \in ℂ$
124	123	sqcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to R^{2} \in ℂ$
125	124 26	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to R^{2} Q \in ℂ$
126	78 125	pncan3d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to C^{2} + R^{2} Q - C^{2} = R^{2} Q$
127	120 126	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to C^{2} + D = R^{2} Q$
128	116 124 26 32	divmul3d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (\frac{C^{2} + D}{Q} = R^{2} \leftrightarrow C^{2} + D = R^{2} Q)$
129	127 128	mpbird	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{C^{2} + D}{Q} = R^{2}$
130	118 129	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{Q C^{2} + Q D}{Q^{2}} = R^{2}$
131	111 130	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{(A^{2} C^{2} + 2 A C B \sqrt{D}) + B^{2} D + (B^{2} C^{2} - 2 A C B \sqrt{D}) + A^{2} D}{Q^{2}} = R^{2}$
132	76 95 131	3eqtr2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(\frac{A C + B \sqrt{D}}{Q})}^{2} + {(\frac{B C - A \sqrt{D}}{Q})}^{2} = R^{2}$
133	5 22 26 32	divassd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{A (A C + B \sqrt{D})}{Q} = A (\frac{A C + B \sqrt{D}}{Q})$
134	5 9 21	adddid	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A (A C + B \sqrt{D}) = A A C + A B \sqrt{D}$
135	3	adantr	$⊢ (A \in ℝ \land C \in ℝ) \to A \in ℂ$
136	6	adantl	$⊢ (A \in ℝ \land C \in ℝ) \to C \in ℂ$
137	135 135 136	mulassd	$⊢ (A \in ℝ \land C \in ℝ) \to A A C = A A C$
138	135	sqvald	$⊢ (A \in ℝ \land C \in ℝ) \to A^{2} = A A$
139	138	eqcomd	$⊢ (A \in ℝ \land C \in ℝ) \to A A = A^{2}$
140	139	oveq1d	$⊢ (A \in ℝ \land C \in ℝ) \to A A C = A^{2} C$
141	137 140	eqtr3d	$⊢ (A \in ℝ \land C \in ℝ) \to A A C = A^{2} C$
142	141	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A A C = A^{2} C$
143	142	3ad2ant1	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A A C = A^{2} C$
144	5 12 20	mulassd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A B \sqrt{D} = A B \sqrt{D}$
145	144	eqcomd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A B \sqrt{D} = A B \sqrt{D}$
146	143 145	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A A C + A B \sqrt{D} = A^{2} C + A B \sqrt{D}$
147	134 146	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A (A C + B \sqrt{D}) = A^{2} C + A B \sqrt{D}$
148	147	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{A (A C + B \sqrt{D})}{Q} = \frac{A^{2} C + A B \sqrt{D}}{Q}$
149	133 148	eqtr3d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A (\frac{A C + B \sqrt{D}}{Q}) = \frac{A^{2} C + A B \sqrt{D}}{Q}$
150	12 53 26 32	divassd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{B (B C - A \sqrt{D})}{Q} = B (\frac{B C - A \sqrt{D}}{Q})$
151	12 51 52	subdid	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B (B C - A \sqrt{D}) = B B C - B A \sqrt{D}$
152		simpl	$⊢ (B \in ℝ \land C \in ℝ) \to B \in ℝ$
153	152	recnd	$⊢ (B \in ℝ \land C \in ℝ) \to B \in ℂ$
154		simpr	$⊢ (B \in ℝ \land C \in ℝ) \to C \in ℝ$
155	154	recnd	$⊢ (B \in ℝ \land C \in ℝ) \to C \in ℂ$
156	153 153 155	mulassd	$⊢ (B \in ℝ \land C \in ℝ) \to B B C = B B C$
157	10	sqvald	$⊢ B \in ℝ \to B^{2} = B B$
158	157	eqcomd	$⊢ B \in ℝ \to B B = B^{2}$
159	158	adantr	$⊢ (B \in ℝ \land C \in ℝ) \to B B = B^{2}$
160	159	oveq1d	$⊢ (B \in ℝ \land C \in ℝ) \to B B C = B^{2} C$
161	156 160	eqtr3d	$⊢ (B \in ℝ \land C \in ℝ) \to B B C = B^{2} C$
162	161	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B B C = B^{2} C$
163	162	3ad2ant1	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B B C = B^{2} C$
164	12 5 20	mulassd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B A \sqrt{D} = B A \sqrt{D}$
165	11 4	mulcomd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B A = A B$
166	165	3ad2ant1	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B A = A B$
167	166	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B A \sqrt{D} = A B \sqrt{D}$
168	164 167	eqtr3d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B A \sqrt{D} = A B \sqrt{D}$
169	163 168	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B B C - B A \sqrt{D} = B^{2} C - A B \sqrt{D}$
170	151 169	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B (B C - A \sqrt{D}) = B^{2} C - A B \sqrt{D}$
171	170	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{B (B C - A \sqrt{D})}{Q} = \frac{B^{2} C - A B \sqrt{D}}{Q}$
172	150 171	eqtr3d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B (\frac{B C - A \sqrt{D}}{Q}) = \frac{B^{2} C - A B \sqrt{D}}{Q}$
173	149 172	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A (\frac{A C + B \sqrt{D}}{Q}) + B (\frac{B C - A \sqrt{D}}{Q}) = (\frac{A^{2} C + A B \sqrt{D}}{Q}) + (\frac{B^{2} C - A B \sqrt{D}}{Q})$
174	77 8	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C \in ℂ$
175	5 12	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A B \in ℂ$
176	175 20	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A B \sqrt{D} \in ℂ$
177	174 176	addcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C + A B \sqrt{D} \in ℂ$
178	84 8	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} C \in ℂ$
179	178 176	subcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} C - A B \sqrt{D} \in ℂ$
180	177 179 26 32	divdird	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{A^{2} C + A B \sqrt{D} + (B^{2} C - A B \sqrt{D})}{Q} = (\frac{A^{2} C + A B \sqrt{D}}{Q}) + (\frac{B^{2} C - A B \sqrt{D}}{Q})$
181	174 176 178	ppncand	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C + A B \sqrt{D} + (B^{2} C - A B \sqrt{D}) = A^{2} C + B^{2} C$
182	77 84 8	adddird	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (A^{2} + B^{2}) C = A^{2} C + B^{2} C$
183	1	a1i	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q = A^{2} + B^{2}$
184	183	eqcomd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} + B^{2} = Q$
185	184	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (A^{2} + B^{2}) C = Q C$
186	181 182 185	3eqtr2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C + A B \sqrt{D} + (B^{2} C - A B \sqrt{D}) = Q C$
187	177 179	addcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C + A B \sqrt{D} + (B^{2} C - A B \sqrt{D}) \in ℂ$
188	187 8 26 32	divmul2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (\frac{A^{2} C + A B \sqrt{D} + (B^{2} C - A B \sqrt{D})}{Q} = C \leftrightarrow A^{2} C + A B \sqrt{D} + (B^{2} C - A B \sqrt{D}) = Q C)$
189	186 188	mpbird	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{A^{2} C + A B \sqrt{D} + (B^{2} C - A B \sqrt{D})}{Q} = C$
190	173 180 189	3eqtr2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A (\frac{A C + B \sqrt{D}}{Q}) + B (\frac{B C - A \sqrt{D}}{Q}) = C$
191	132 190	jca	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to ({(\frac{A C + B \sqrt{D}}{Q})}^{2} + {(\frac{B C - A \sqrt{D}}{Q})}^{2} = R^{2} \land A (\frac{A C + B \sqrt{D}}{Q}) + B (\frac{B C - A \sqrt{D}}{Q}) = C)$
192		oveq1	$⊢ X = \frac{A C + B \sqrt{D}}{Q} \to X^{2} = {(\frac{A C + B \sqrt{D}}{Q})}^{2}$
193		oveq1	$⊢ Y = \frac{B C - A \sqrt{D}}{Q} \to Y^{2} = {(\frac{B C - A \sqrt{D}}{Q})}^{2}$
194	192 193	oveqan12d	$⊢ (X = \frac{A C + B \sqrt{D}}{Q} \land Y = \frac{B C - A \sqrt{D}}{Q}) \to X^{2} + Y^{2} = {(\frac{A C + B \sqrt{D}}{Q})}^{2} + {(\frac{B C - A \sqrt{D}}{Q})}^{2}$
195	194	eqeq1d	$⊢ (X = \frac{A C + B \sqrt{D}}{Q} \land Y = \frac{B C - A \sqrt{D}}{Q}) \to (X^{2} + Y^{2} = R^{2} \leftrightarrow {(\frac{A C + B \sqrt{D}}{Q})}^{2} + {(\frac{B C - A \sqrt{D}}{Q})}^{2} = R^{2})$
196		oveq2	$⊢ X = \frac{A C + B \sqrt{D}}{Q} \to A X = A (\frac{A C + B \sqrt{D}}{Q})$
197		oveq2	$⊢ Y = \frac{B C - A \sqrt{D}}{Q} \to B Y = B (\frac{B C - A \sqrt{D}}{Q})$
198	196 197	oveqan12d	$⊢ (X = \frac{A C + B \sqrt{D}}{Q} \land Y = \frac{B C - A \sqrt{D}}{Q}) \to A X + B Y = A (\frac{A C + B \sqrt{D}}{Q}) + B (\frac{B C - A \sqrt{D}}{Q})$
199	198	eqeq1d	$⊢ (X = \frac{A C + B \sqrt{D}}{Q} \land Y = \frac{B C - A \sqrt{D}}{Q}) \to (A X + B Y = C \leftrightarrow A (\frac{A C + B \sqrt{D}}{Q}) + B (\frac{B C - A \sqrt{D}}{Q}) = C)$
200	195 199	anbi12d	$⊢ (X = \frac{A C + B \sqrt{D}}{Q} \land Y = \frac{B C - A \sqrt{D}}{Q}) \to ((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \leftrightarrow ({(\frac{A C + B \sqrt{D}}{Q})}^{2} + {(\frac{B C - A \sqrt{D}}{Q})}^{2} = R^{2} \land A (\frac{A C + B \sqrt{D}}{Q}) + B (\frac{B C - A \sqrt{D}}{Q}) = C))$
201	191 200	syl5ibrcom	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to ((X = \frac{A C + B \sqrt{D}}{Q} \land Y = \frac{B C - A \sqrt{D}}{Q}) \to (X^{2} + Y^{2} = R^{2} \land A X + B Y = C))$
202	35 21	subcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A C - B \sqrt{D} \in ℂ$
203	202 26 32	sqdivd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(\frac{A C - B \sqrt{D}}{Q})}^{2} = \frac{{(A C - B \sqrt{D})}^{2}}{Q^{2}}$
204		binom2sub	$⊢ (A C \in ℂ \land B \sqrt{D} \in ℂ) \to {(A C - B \sqrt{D})}^{2} = {A C}^{2} - 2 A C B \sqrt{D} + {B \sqrt{D}}^{2}$
205	35 21 204	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(A C - B \sqrt{D})}^{2} = {A C}^{2} - 2 A C B \sqrt{D} + {B \sqrt{D}}^{2}$
206	39	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {A C}^{2} - 2 A C B \sqrt{D} = A^{2} C^{2} - 2 A C B \sqrt{D}$
207	206 46	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {A C}^{2} - 2 A C B \sqrt{D} + {B \sqrt{D}}^{2} = A^{2} C^{2} - 2 A C B \sqrt{D} + B^{2} D$
208	205 207	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(A C - B \sqrt{D})}^{2} = A^{2} C^{2} - 2 A C B \sqrt{D} + B^{2} D$
209	208	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{{(A C - B \sqrt{D})}^{2}}{Q^{2}} = \frac{A^{2} C^{2} - 2 A C B \sqrt{D} + B^{2} D}{Q^{2}}$
210	203 209	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(\frac{A C - B \sqrt{D}}{Q})}^{2} = \frac{A^{2} C^{2} - 2 A C B \sqrt{D} + B^{2} D}{Q^{2}}$
211	51 56	addcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B C + A \sqrt{D} \in ℂ$
212	211 26 32	sqdivd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(\frac{B C + A \sqrt{D}}{Q})}^{2} = \frac{{(B C + A \sqrt{D})}^{2}}{Q^{2}}$
213		binom2	$⊢ (B C \in ℂ \land A \sqrt{D} \in ℂ) \to {(B C + A \sqrt{D})}^{2} = {B C}^{2} + 2 B C A \sqrt{D} + {A \sqrt{D}}^{2}$
214	51 56 213	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(B C + A \sqrt{D})}^{2} = {B C}^{2} + 2 B C A \sqrt{D} + {A \sqrt{D}}^{2}$
215	60 67	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {B C}^{2} + 2 B C A \sqrt{D} = B^{2} C^{2} + 2 A C B \sqrt{D}$
216	215 71	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {B C}^{2} + 2 B C A \sqrt{D} + {A \sqrt{D}}^{2} = B^{2} C^{2} + 2 A C B \sqrt{D} + A^{2} D$
217	214 216	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(B C + A \sqrt{D})}^{2} = B^{2} C^{2} + 2 A C B \sqrt{D} + A^{2} D$
218	217	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{{(B C + A \sqrt{D})}^{2}}{Q^{2}} = \frac{B^{2} C^{2} + 2 A C B \sqrt{D} + A^{2} D}{Q^{2}}$
219	212 218	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(\frac{B C + A \sqrt{D}}{Q})}^{2} = \frac{B^{2} C^{2} + 2 A C B \sqrt{D} + A^{2} D}{Q^{2}}$
220	210 219	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(\frac{A C - B \sqrt{D}}{Q})}^{2} + {(\frac{B C + A \sqrt{D}}{Q})}^{2} = (\frac{A^{2} C^{2} - 2 A C B \sqrt{D} + B^{2} D}{Q^{2}}) + (\frac{B^{2} C^{2} + 2 A C B \sqrt{D} + A^{2} D}{Q^{2}})$
221	98 78	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C^{2} \in ℂ$
222	35 21	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A C B \sqrt{D} \in ℂ$
223	80 222	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to 2 A C B \sqrt{D} \in ℂ$
224	221 223	subcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C^{2} - 2 A C B \sqrt{D} \in ℂ$
225	224 85	addcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C^{2} - 2 A C B \sqrt{D} + B^{2} D \in ℂ$
226	87 223	addcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} C^{2} + 2 A C B \sqrt{D} \in ℂ$
227	98 19	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} D \in ℂ$
228	226 227	addcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} C^{2} + 2 A C B \sqrt{D} + A^{2} D \in ℂ$
229	225 228 91 94	divdird	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{(A^{2} C^{2} - 2 A C B \sqrt{D}) + B^{2} D + (B^{2} C^{2} + 2 A C B \sqrt{D}) + A^{2} D}{Q^{2}} = (\frac{A^{2} C^{2} - 2 A C B \sqrt{D} + B^{2} D}{Q^{2}}) + (\frac{B^{2} C^{2} + 2 A C B \sqrt{D} + A^{2} D}{Q^{2}})$
230	224 85 226 227	add4d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (A^{2} C^{2} - 2 A C B \sqrt{D}) + B^{2} D + (B^{2} C^{2} + 2 A C B \sqrt{D}) + A^{2} D = (A^{2} C^{2} - 2 A C B \sqrt{D}) + (B^{2} C^{2} + 2 A C B \sqrt{D}) + B^{2} D + A^{2} D$
231	221 223 87	nppcan3d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (A^{2} C^{2} - 2 A C B \sqrt{D}) + B^{2} C^{2} + 2 A C B \sqrt{D} = A^{2} C^{2} + B^{2} C^{2}$
232	231 99 102	3eqtr2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (A^{2} C^{2} - 2 A C B \sqrt{D}) + B^{2} C^{2} + 2 A C B \sqrt{D} = Q C^{2}$
233	232 108	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (A^{2} C^{2} - 2 A C B \sqrt{D}) + (B^{2} C^{2} + 2 A C B \sqrt{D}) + B^{2} D + A^{2} D = Q C^{2} + Q D$
234	230 233	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (A^{2} C^{2} - 2 A C B \sqrt{D}) + B^{2} D + (B^{2} C^{2} + 2 A C B \sqrt{D}) + A^{2} D = Q C^{2} + Q D$
235	234	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{(A^{2} C^{2} - 2 A C B \sqrt{D}) + B^{2} D + (B^{2} C^{2} + 2 A C B \sqrt{D}) + A^{2} D}{Q^{2}} = \frac{Q C^{2} + Q D}{Q^{2}}$
236	220 229 235	3eqtr2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(\frac{A C - B \sqrt{D}}{Q})}^{2} + {(\frac{B C + A \sqrt{D}}{Q})}^{2} = \frac{Q C^{2} + Q D}{Q^{2}}$
237	236 130	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(\frac{A C - B \sqrt{D}}{Q})}^{2} + {(\frac{B C + A \sqrt{D}}{Q})}^{2} = R^{2}$
238		simp1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A \in ℝ$
239		simp3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to C \in ℝ$
240	238 239	remulcld	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A C \in ℝ$
241	240	recnd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A C \in ℂ$
242	241	3ad2ant1	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A C \in ℂ$
243	242 21	subcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A C - B \sqrt{D} \in ℂ$
244	5 243 26 32	divassd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{A (A C - B \sqrt{D})}{Q} = A (\frac{A C - B \sqrt{D}}{Q})$
245	5 242 21	subdid	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A (A C - B \sqrt{D}) = A A C - A B \sqrt{D}$
246	143 145	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A A C - A B \sqrt{D} = A^{2} C - A B \sqrt{D}$
247	245 246	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A (A C - B \sqrt{D}) = A^{2} C - A B \sqrt{D}$
248	247	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{A (A C - B \sqrt{D})}{Q} = \frac{A^{2} C - A B \sqrt{D}}{Q}$
249	244 248	eqtr3d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A (\frac{A C - B \sqrt{D}}{Q}) = \frac{A^{2} C - A B \sqrt{D}}{Q}$
250	51 52	addcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B C + A \sqrt{D} \in ℂ$
251	12 250 26 32	divassd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{B (B C + A \sqrt{D})}{Q} = B (\frac{B C + A \sqrt{D}}{Q})$
252	12 51 52	adddid	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B (B C + A \sqrt{D}) = B B C + B A \sqrt{D}$
253	163 168	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B B C + B A \sqrt{D} = B^{2} C + A B \sqrt{D}$
254	252 253	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B (B C + A \sqrt{D}) = B^{2} C + A B \sqrt{D}$
255	254	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{B (B C + A \sqrt{D})}{Q} = \frac{B^{2} C + A B \sqrt{D}}{Q}$
256	251 255	eqtr3d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B (\frac{B C + A \sqrt{D}}{Q}) = \frac{B^{2} C + A B \sqrt{D}}{Q}$
257	249 256	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A (\frac{A C - B \sqrt{D}}{Q}) + B (\frac{B C + A \sqrt{D}}{Q}) = (\frac{A^{2} C - A B \sqrt{D}}{Q}) + (\frac{B^{2} C + A B \sqrt{D}}{Q})$
258	174 176	subcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} C - A B \sqrt{D} \in ℂ$
259	178 176	addcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} C + A B \sqrt{D} \in ℂ$
260	258 259 26 32	divdird	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{(A^{2} C - A B \sqrt{D}) + B^{2} C + A B \sqrt{D}}{Q} = (\frac{A^{2} C - A B \sqrt{D}}{Q}) + (\frac{B^{2} C + A B \sqrt{D}}{Q})$
261	174 176 178	nppcan3d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (A^{2} C - A B \sqrt{D}) + B^{2} C + A B \sqrt{D} = A^{2} C + B^{2} C$
262	261 182 185	3eqtr2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (A^{2} C - A B \sqrt{D}) + B^{2} C + A B \sqrt{D} = Q C$
263	258 259	addcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (A^{2} C - A B \sqrt{D}) + B^{2} C + A B \sqrt{D} \in ℂ$
264	263 8 26 32	divmul2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to (\frac{(A^{2} C - A B \sqrt{D}) + B^{2} C + A B \sqrt{D}}{Q} = C \leftrightarrow (A^{2} C - A B \sqrt{D}) + B^{2} C + A B \sqrt{D} = Q C)$
265	262 264	mpbird	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{(A^{2} C - A B \sqrt{D}) + B^{2} C + A B \sqrt{D}}{Q} = C$
266	257 260 265	3eqtr2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to A (\frac{A C - B \sqrt{D}}{Q}) + B (\frac{B C + A \sqrt{D}}{Q}) = C$
267	237 266	jca	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to ({(\frac{A C - B \sqrt{D}}{Q})}^{2} + {(\frac{B C + A \sqrt{D}}{Q})}^{2} = R^{2} \land A (\frac{A C - B \sqrt{D}}{Q}) + B (\frac{B C + A \sqrt{D}}{Q}) = C)$
268		oveq1	$⊢ X = \frac{A C - B \sqrt{D}}{Q} \to X^{2} = {(\frac{A C - B \sqrt{D}}{Q})}^{2}$
269		oveq1	$⊢ Y = \frac{B C + A \sqrt{D}}{Q} \to Y^{2} = {(\frac{B C + A \sqrt{D}}{Q})}^{2}$
270	268 269	oveqan12d	$⊢ (X = \frac{A C - B \sqrt{D}}{Q} \land Y = \frac{B C + A \sqrt{D}}{Q}) \to X^{2} + Y^{2} = {(\frac{A C - B \sqrt{D}}{Q})}^{2} + {(\frac{B C + A \sqrt{D}}{Q})}^{2}$
271	270	eqeq1d	$⊢ (X = \frac{A C - B \sqrt{D}}{Q} \land Y = \frac{B C + A \sqrt{D}}{Q}) \to (X^{2} + Y^{2} = R^{2} \leftrightarrow {(\frac{A C - B \sqrt{D}}{Q})}^{2} + {(\frac{B C + A \sqrt{D}}{Q})}^{2} = R^{2})$
272		oveq2	$⊢ X = \frac{A C - B \sqrt{D}}{Q} \to A X = A (\frac{A C - B \sqrt{D}}{Q})$
273		oveq2	$⊢ Y = \frac{B C + A \sqrt{D}}{Q} \to B Y = B (\frac{B C + A \sqrt{D}}{Q})$
274	272 273	oveqan12d	$⊢ (X = \frac{A C - B \sqrt{D}}{Q} \land Y = \frac{B C + A \sqrt{D}}{Q}) \to A X + B Y = A (\frac{A C - B \sqrt{D}}{Q}) + B (\frac{B C + A \sqrt{D}}{Q})$
275	274	eqeq1d	$⊢ (X = \frac{A C - B \sqrt{D}}{Q} \land Y = \frac{B C + A \sqrt{D}}{Q}) \to (A X + B Y = C \leftrightarrow A (\frac{A C - B \sqrt{D}}{Q}) + B (\frac{B C + A \sqrt{D}}{Q}) = C)$
276	271 275	anbi12d	$⊢ (X = \frac{A C - B \sqrt{D}}{Q} \land Y = \frac{B C + A \sqrt{D}}{Q}) \to ((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \leftrightarrow ({(\frac{A C - B \sqrt{D}}{Q})}^{2} + {(\frac{B C + A \sqrt{D}}{Q})}^{2} = R^{2} \land A (\frac{A C - B \sqrt{D}}{Q}) + B (\frac{B C + A \sqrt{D}}{Q}) = C))$
277	267 276	syl5ibrcom	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to ((X = \frac{A C - B \sqrt{D}}{Q} \land Y = \frac{B C + A \sqrt{D}}{Q}) \to (X^{2} + Y^{2} = R^{2} \land A X + B Y = C))$
278	201 277	jaod	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \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})) \to (X^{2} + Y^{2} = R^{2} \land A X + B Y = C))$

Metamath Proof Explorer

Theorem itsclc0xyqsolr

Proof