itschlc0xyqsol

Description: Lemma for itsclc0 . Solutions of the quadratic equations for the coordinates of the intersection points of a horizontal 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	itschlc0xyqsol	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land 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 ((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	1 2	itschlc0xyqsol1	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land 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{C}{B} \land (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B})))$
4		orcom	$⊢ (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B}) \leftrightarrow (X = \frac{\sqrt{D}}{B} \lor X = - \frac{\sqrt{D}}{B})$
5		oveq1	$⊢ A = 0 \to A C = 0 \cdot C$
6	5	ad2antrl	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to A C = 0 \cdot C$
7	6	adantr	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to A C = 0 \cdot C$
8		simpll3	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to C \in ℝ$
9	8	recnd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to C \in ℂ$
10	9	mul02d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to 0 \cdot C = 0$
11	7 10	eqtrd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to A C = 0$
12	11	oveq1d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to A C + B \sqrt{D} = 0 + B \sqrt{D}$
13		simpll2	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B \in ℝ$
14	13	recnd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B \in ℂ$
15		rpre	$⊢ R \in ℝ^{+} \to R \in ℝ$
16	15	adantr	$⊢ (R \in ℝ^{+} \land 0 \leq D) \to R \in ℝ$
17	16	recnd	$⊢ (R \in ℝ^{+} \land 0 \leq D) \to R \in ℂ$
18	17	adantl	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to R \in ℂ$
19	18	sqcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to R^{2} \in ℂ$
20	1	resum2sqcl	$⊢ (A \in ℝ \land B \in ℝ) \to Q \in ℝ$
21	20	recnd	$⊢ (A \in ℝ \land B \in ℝ) \to Q \in ℂ$
22	21	3adant3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to Q \in ℂ$
23	22	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to Q \in ℂ$
24	23	adantr	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q \in ℂ$
25	19 24	mulcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to R^{2} Q \in ℂ$
26	9	sqcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to C^{2} \in ℂ$
27	25 26	subcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to R^{2} Q - C^{2} \in ℂ$
28	2 27	eqeltrid	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to D \in ℂ$
29	28	sqrtcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to \sqrt{D} \in ℂ$
30	14 29	mulcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B \sqrt{D} \in ℂ$
31	30	addid2d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to 0 + B \sqrt{D} = B \sqrt{D}$
32	12 31	eqtrd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to A C + B \sqrt{D} = B \sqrt{D}$
33	32	oveq1d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{A C + B \sqrt{D}}{Q} = \frac{B \sqrt{D}}{Q}$
34		sq0i	$⊢ A = 0 \to A^{2} = 0$
35	34	ad2antrl	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to A^{2} = 0$
36	35	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to A^{2} + B^{2} = 0 + B^{2}$
37		simp2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B \in ℝ$
38	37	recnd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B \in ℂ$
39	38	sqcld	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B^{2} \in ℂ$
40	39	addid2d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to 0 + B^{2} = B^{2}$
41	38	sqvald	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B^{2} = B B$
42	40 41	eqtrd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to 0 + B^{2} = B B$
43	42	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to 0 + B^{2} = B B$
44	36 43	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to A^{2} + B^{2} = B B$
45	1 44	syl5eq	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to Q = B B$
46	45	adantr	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q = B B$
47	46	oveq2d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{B \sqrt{D}}{Q} = \frac{B \sqrt{D}}{B B}$
48		simplrr	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B \neq 0$
49	29 14 14 48 48	divcan5d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{B \sqrt{D}}{B B} = \frac{\sqrt{D}}{B}$
50	47 49	eqtrd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{B \sqrt{D}}{Q} = \frac{\sqrt{D}}{B}$
51	33 50	eqtrd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{A C + B \sqrt{D}}{Q} = \frac{\sqrt{D}}{B}$
52	51	3adant3	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{A C + B \sqrt{D}}{Q} = \frac{\sqrt{D}}{B}$
53	52	adantr	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land Y = \frac{C}{B}) \to \frac{A C + B \sqrt{D}}{Q} = \frac{\sqrt{D}}{B}$
54	53	eqcomd	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land Y = \frac{C}{B}) \to \frac{\sqrt{D}}{B} = \frac{A C + B \sqrt{D}}{Q}$
55	54	eqeq2d	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land Y = \frac{C}{B}) \to (X = \frac{\sqrt{D}}{B} \leftrightarrow X = \frac{A C + B \sqrt{D}}{Q})$
56	55	biimpd	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land Y = \frac{C}{B}) \to (X = \frac{\sqrt{D}}{B} \to X = \frac{A C + B \sqrt{D}}{Q})$
57		oveq1	$⊢ A = 0 \to A \sqrt{D} = 0 \cdot \sqrt{D}$
58	57	ad2antrl	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to A \sqrt{D} = 0 \cdot \sqrt{D}$
59	58	adantr	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to A \sqrt{D} = 0 \cdot \sqrt{D}$
60	29	mul02d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to 0 \cdot \sqrt{D} = 0$
61	59 60	eqtrd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to A \sqrt{D} = 0$
62	61	oveq2d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B C - A \sqrt{D} = B C - 0$
63	14 9	mulcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B C \in ℂ$
64	63	subid1d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B C - 0 = B C$
65	62 64	eqtrd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B C - A \sqrt{D} = B C$
66	65 46	oveq12d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{B C - A \sqrt{D}}{Q} = \frac{B C}{B B}$
67	66	3adant3	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land 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}{B B}$
68	9	3adant3	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to C \in ℂ$
69	14	3adant3	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B \in ℂ$
70		simp1rr	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B \neq 0$
71	68 69 69 70 70	divcan5d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{B C}{B B} = \frac{C}{B}$
72	67 71	eqtr2d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{C}{B} = \frac{B C - A \sqrt{D}}{Q}$
73	72	eqeq2d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (Y = \frac{C}{B} \leftrightarrow Y = \frac{B C - A \sqrt{D}}{Q})$
74	73	biimpa	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land Y = \frac{C}{B}) \to Y = \frac{B C - A \sqrt{D}}{Q}$
75	56 74	jctird	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land Y = \frac{C}{B}) \to (X = \frac{\sqrt{D}}{B} \to (X = \frac{A C + B \sqrt{D}}{Q} \land Y = \frac{B C - A \sqrt{D}}{Q}))$
76	14 29	mulneg2d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B (- \sqrt{D}) = - B \sqrt{D}$
77	76	eqcomd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to - B \sqrt{D} = B (- \sqrt{D})$
78	77 46	oveq12d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{- B \sqrt{D}}{Q} = \frac{B (- \sqrt{D})}{B B}$
79	29	negcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to - \sqrt{D} \in ℂ$
80	79 14 14 48 48	divcan5d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{B (- \sqrt{D})}{B B} = \frac{- \sqrt{D}}{B}$
81	78 80	eqtrd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{- B \sqrt{D}}{Q} = \frac{- \sqrt{D}}{B}$
82	11	oveq1d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to A C - B \sqrt{D} = 0 - B \sqrt{D}$
83		df-neg	$⊢ - B \sqrt{D} = 0 - B \sqrt{D}$
84	82 83	eqtr4di	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to A C - B \sqrt{D} = - B \sqrt{D}$
85	84	oveq1d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{A C - B \sqrt{D}}{Q} = \frac{- B \sqrt{D}}{Q}$
86	29 14 48	divnegd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to - \frac{\sqrt{D}}{B} = \frac{- \sqrt{D}}{B}$
87	81 85 86	3eqtr4d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{A C - B \sqrt{D}}{Q} = - \frac{\sqrt{D}}{B}$
88	87	3adant3	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{A C - B \sqrt{D}}{Q} = - \frac{\sqrt{D}}{B}$
89	88	adantr	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land Y = \frac{C}{B}) \to \frac{A C - B \sqrt{D}}{Q} = - \frac{\sqrt{D}}{B}$
90	89	eqcomd	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land Y = \frac{C}{B}) \to - \frac{\sqrt{D}}{B} = \frac{A C - B \sqrt{D}}{Q}$
91	90	eqeq2d	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land Y = \frac{C}{B}) \to (X = - \frac{\sqrt{D}}{B} \leftrightarrow X = \frac{A C - B \sqrt{D}}{Q})$
92	91	biimpd	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land Y = \frac{C}{B}) \to (X = - \frac{\sqrt{D}}{B} \to X = \frac{A C - B \sqrt{D}}{Q})$
93	58	3ad2ant1	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to A \sqrt{D} = 0 \cdot \sqrt{D}$
94	17	3ad2ant2	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to R \in ℂ$
95	94	sqcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to R^{2} \in ℂ$
96	23	3ad2ant1	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to Q \in ℂ$
97	95 96	mulcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to R^{2} Q \in ℂ$
98		simp1l3	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to C \in ℝ$
99	98	recnd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to C \in ℂ$
100	99	sqcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to C^{2} \in ℂ$
101	97 100	subcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to R^{2} Q - C^{2} \in ℂ$
102	2 101	eqeltrid	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to D \in ℂ$
103	102	sqrtcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \sqrt{D} \in ℂ$
104	103	mul02d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to 0 \cdot \sqrt{D} = 0$
105	93 104	eqtrd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to A \sqrt{D} = 0$
106	105	oveq2d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B C + A \sqrt{D} = B C + 0$
107		simp1l2	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B \in ℝ$
108	107	recnd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B \in ℂ$
109	108 99	mulcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B C \in ℂ$
110	109	addid1d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B C + 0 = B C$
111	106 110	eqtrd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B C + A \sqrt{D} = B C$
112	45	3ad2ant1	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to Q = B B$
113	111 112	oveq12d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land 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}{B B}$
114	99 108 108 70 70	divcan5d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{B C}{B B} = \frac{C}{B}$
115	113 114	eqtr2d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{C}{B} = \frac{B C + A \sqrt{D}}{Q}$
116	115	eqeq2d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (Y = \frac{C}{B} \leftrightarrow Y = \frac{B C + A \sqrt{D}}{Q})$
117	116	biimpa	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land Y = \frac{C}{B}) \to Y = \frac{B C + A \sqrt{D}}{Q}$
118	92 117	jctird	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land Y = \frac{C}{B}) \to (X = - \frac{\sqrt{D}}{B} \to (X = \frac{A C - B \sqrt{D}}{Q} \land Y = \frac{B C + A \sqrt{D}}{Q}))$
119	75 118	orim12d	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land Y = \frac{C}{B}) \to ((X = \frac{\sqrt{D}}{B} \lor X = - \frac{\sqrt{D}}{B}) \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})))$
120	4 119	syl5bi	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land Y = \frac{C}{B}) \to ((X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B}) \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})))$
121	120	expimpd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to ((Y = \frac{C}{B} \land (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B})) \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})))$
122	3 121	syld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land 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 ((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 itschlc0xyqsol

Proof