Theorem 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	⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
	itsclc0yqsol.d	⊢ 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
Assertion	itschlc0xyqsol	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		itscnhlc0yqe.q	⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
2		itsclc0yqsol.d	⊢ 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
3	1 2	itschlc0xyqsol1	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( 𝑌 = ( 𝐶 / 𝐵 ) ∧ ( 𝑋 = - ( ( √ ‘ 𝐷 ) / 𝐵 ) ∨ 𝑋 = ( ( √ ‘ 𝐷 ) / 𝐵 ) ) ) ) )
4		orcom	⊢ ( ( 𝑋 = - ( ( √ ‘ 𝐷 ) / 𝐵 ) ∨ 𝑋 = ( ( √ ‘ 𝐷 ) / 𝐵 ) ) ↔ ( 𝑋 = ( ( √ ‘ 𝐷 ) / 𝐵 ) ∨ 𝑋 = - ( ( √ ‘ 𝐷 ) / 𝐵 ) ) )
5		oveq1	⊢ ( 𝐴 = 0 → ( 𝐴 · 𝐶 ) = ( 0 · 𝐶 ) )
6	5	ad2antrl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 · 𝐶 ) = ( 0 · 𝐶 ) )
7	6	adantr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · 𝐶 ) = ( 0 · 𝐶 ) )
8		simpll3	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐶 ∈ ℝ )
9	8	recnd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐶 ∈ ℂ )
10	9	mul02d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 0 · 𝐶 ) = 0 )
11	7 10	eqtrd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · 𝐶 ) = 0 )
12	11	oveq1d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) = ( 0 + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) )
13		simpll2	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐵 ∈ ℝ )
14	13	recnd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐵 ∈ ℂ )
15		rpre	⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ )
16	15	adantr	⊢ ( ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) → 𝑅 ∈ ℝ )
17	16	recnd	⊢ ( ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) → 𝑅 ∈ ℂ )
18	17	adantl	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝑅 ∈ ℂ )
19	18	sqcld	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑅 ↑ 2 ) ∈ ℂ )
20	1	resum2sqcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝑄 ∈ ℝ )
21	20	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝑄 ∈ ℂ )
22	21	3adant3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝑄 ∈ ℂ )
23	22	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) → 𝑄 ∈ ℂ )
24	23	adantr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝑄 ∈ ℂ )
25	19 24	mulcld	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑅 ↑ 2 ) · 𝑄 ) ∈ ℂ )
26	9	sqcld	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐶 ↑ 2 ) ∈ ℂ )
27	25 26	subcld	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) ) ∈ ℂ )
28	2 27	eqeltrid	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐷 ∈ ℂ )
29	28	sqrtcld	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( √ ‘ 𝐷 ) ∈ ℂ )
30	14 29	mulcld	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · ( √ ‘ 𝐷 ) ) ∈ ℂ )
31	30	addlidd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 0 + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) = ( 𝐵 · ( √ ‘ 𝐷 ) ) )
32	12 31	eqtrd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) = ( 𝐵 · ( √ ‘ 𝐷 ) ) )
33	32	oveq1d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) = ( ( 𝐵 · ( √ ‘ 𝐷 ) ) / 𝑄 ) )
34		sq0i	⊢ ( 𝐴 = 0 → ( 𝐴 ↑ 2 ) = 0 )
35	34	ad2antrl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 ↑ 2 ) = 0 )
36	35	oveq1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 0 + ( 𝐵 ↑ 2 ) ) )
37		simp2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
38	37	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
39	38	sqcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
40	39	addlidd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 0 + ( 𝐵 ↑ 2 ) ) = ( 𝐵 ↑ 2 ) )
41	38	sqvald	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 ↑ 2 ) = ( 𝐵 · 𝐵 ) )
42	40 41	eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 0 + ( 𝐵 ↑ 2 ) ) = ( 𝐵 · 𝐵 ) )
43	42	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) → ( 0 + ( 𝐵 ↑ 2 ) ) = ( 𝐵 · 𝐵 ) )
44	36 43	eqtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐵 · 𝐵 ) )
45	1 44	eqtrid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) → 𝑄 = ( 𝐵 · 𝐵 ) )
46	45	adantr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝑄 = ( 𝐵 · 𝐵 ) )
47	46	oveq2d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · ( √ ‘ 𝐷 ) ) / 𝑄 ) = ( ( 𝐵 · ( √ ‘ 𝐷 ) ) / ( 𝐵 · 𝐵 ) ) )
48		simplrr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐵 ≠ 0 )
49	29 14 14 48 48	divcan5d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · ( √ ‘ 𝐷 ) ) / ( 𝐵 · 𝐵 ) ) = ( ( √ ‘ 𝐷 ) / 𝐵 ) )
50	47 49	eqtrd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · ( √ ‘ 𝐷 ) ) / 𝑄 ) = ( ( √ ‘ 𝐷 ) / 𝐵 ) )
51	33 50	eqtrd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) = ( ( √ ‘ 𝐷 ) / 𝐵 ) )
52	51	3adant3	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) = ( ( √ ‘ 𝐷 ) / 𝐵 ) )
53	52	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( 𝐶 / 𝐵 ) ) → ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) = ( ( √ ‘ 𝐷 ) / 𝐵 ) )
54	53	eqcomd	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( 𝐶 / 𝐵 ) ) → ( ( √ ‘ 𝐷 ) / 𝐵 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
55	54	eqeq2d	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( 𝐶 / 𝐵 ) ) → ( 𝑋 = ( ( √ ‘ 𝐷 ) / 𝐵 ) ↔ 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
56	55	biimpd	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( 𝐶 / 𝐵 ) ) → ( 𝑋 = ( ( √ ‘ 𝐷 ) / 𝐵 ) → 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
57		oveq1	⊢ ( 𝐴 = 0 → ( 𝐴 · ( √ ‘ 𝐷 ) ) = ( 0 · ( √ ‘ 𝐷 ) ) )
58	57	ad2antrl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 · ( √ ‘ 𝐷 ) ) = ( 0 · ( √ ‘ 𝐷 ) ) )
59	58	adantr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · ( √ ‘ 𝐷 ) ) = ( 0 · ( √ ‘ 𝐷 ) ) )
60	29	mul02d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 0 · ( √ ‘ 𝐷 ) ) = 0 )
61	59 60	eqtrd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · ( √ ‘ 𝐷 ) ) = 0 )
62	61	oveq2d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) = ( ( 𝐵 · 𝐶 ) − 0 ) )
63	14 9	mulcld	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
64	63	subid1d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · 𝐶 ) − 0 ) = ( 𝐵 · 𝐶 ) )
65	62 64	eqtrd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) = ( 𝐵 · 𝐶 ) )
66	65 46	oveq12d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) = ( ( 𝐵 · 𝐶 ) / ( 𝐵 · 𝐵 ) ) )
67	66	3adant3	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) = ( ( 𝐵 · 𝐶 ) / ( 𝐵 · 𝐵 ) ) )
68	9	3adant3	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐶 ∈ ℂ )
69	14	3adant3	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐵 ∈ ℂ )
70		simp1rr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐵 ≠ 0 )
71	68 69 69 70 70	divcan5d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · 𝐶 ) / ( 𝐵 · 𝐵 ) ) = ( 𝐶 / 𝐵 ) )
72	67 71	eqtr2d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐶 / 𝐵 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
73	72	eqeq2d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑌 = ( 𝐶 / 𝐵 ) ↔ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
74	73	biimpa	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( 𝐶 / 𝐵 ) ) → 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
75	56 74	jctird	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( 𝐶 / 𝐵 ) ) → ( 𝑋 = ( ( √ ‘ 𝐷 ) / 𝐵 ) → ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
76	14 29	mulneg2d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · - ( √ ‘ 𝐷 ) ) = - ( 𝐵 · ( √ ‘ 𝐷 ) ) )
77	76	eqcomd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → - ( 𝐵 · ( √ ‘ 𝐷 ) ) = ( 𝐵 · - ( √ ‘ 𝐷 ) ) )
78	77 46	oveq12d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( - ( 𝐵 · ( √ ‘ 𝐷 ) ) / 𝑄 ) = ( ( 𝐵 · - ( √ ‘ 𝐷 ) ) / ( 𝐵 · 𝐵 ) ) )
79	29	negcld	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → - ( √ ‘ 𝐷 ) ∈ ℂ )
80	79 14 14 48 48	divcan5d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · - ( √ ‘ 𝐷 ) ) / ( 𝐵 · 𝐵 ) ) = ( - ( √ ‘ 𝐷 ) / 𝐵 ) )
81	78 80	eqtrd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( - ( 𝐵 · ( √ ‘ 𝐷 ) ) / 𝑄 ) = ( - ( √ ‘ 𝐷 ) / 𝐵 ) )
82	11	oveq1d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) = ( 0 − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) )
83		df-neg	⊢ - ( 𝐵 · ( √ ‘ 𝐷 ) ) = ( 0 − ( 𝐵 · ( √ ‘ 𝐷 ) ) )
84	82 83	eqtr4di	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) = - ( 𝐵 · ( √ ‘ 𝐷 ) ) )
85	84	oveq1d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) = ( - ( 𝐵 · ( √ ‘ 𝐷 ) ) / 𝑄 ) )
86	29 14 48	divnegd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → - ( ( √ ‘ 𝐷 ) / 𝐵 ) = ( - ( √ ‘ 𝐷 ) / 𝐵 ) )
87	81 85 86	3eqtr4d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) = - ( ( √ ‘ 𝐷 ) / 𝐵 ) )
88	87	3adant3	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) = - ( ( √ ‘ 𝐷 ) / 𝐵 ) )
89	88	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( 𝐶 / 𝐵 ) ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) = - ( ( √ ‘ 𝐷 ) / 𝐵 ) )
90	89	eqcomd	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( 𝐶 / 𝐵 ) ) → - ( ( √ ‘ 𝐷 ) / 𝐵 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
91	90	eqeq2d	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( 𝐶 / 𝐵 ) ) → ( 𝑋 = - ( ( √ ‘ 𝐷 ) / 𝐵 ) ↔ 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
92	91	biimpd	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( 𝐶 / 𝐵 ) ) → ( 𝑋 = - ( ( √ ‘ 𝐷 ) / 𝐵 ) → 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
93	58	3ad2ant1	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐴 · ( √ ‘ 𝐷 ) ) = ( 0 · ( √ ‘ 𝐷 ) ) )
94	17	3ad2ant2	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑅 ∈ ℂ )
95	94	sqcld	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑅 ↑ 2 ) ∈ ℂ )
96	23	3ad2ant1	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑄 ∈ ℂ )
97	95 96	mulcld	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝑅 ↑ 2 ) · 𝑄 ) ∈ ℂ )
98		simp1l3	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐶 ∈ ℝ )
99	98	recnd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐶 ∈ ℂ )
100	99	sqcld	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐶 ↑ 2 ) ∈ ℂ )
101	97 100	subcld	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) ) ∈ ℂ )
102	2 101	eqeltrid	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐷 ∈ ℂ )
103	102	sqrtcld	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( √ ‘ 𝐷 ) ∈ ℂ )
104	103	mul02d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 0 · ( √ ‘ 𝐷 ) ) = 0 )
105	93 104	eqtrd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐴 · ( √ ‘ 𝐷 ) ) = 0 )
106	105	oveq2d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) = ( ( 𝐵 · 𝐶 ) + 0 ) )
107		simp1l2	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐵 ∈ ℝ )
108	107	recnd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐵 ∈ ℂ )
109	108 99	mulcld	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
110	109	addridd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · 𝐶 ) + 0 ) = ( 𝐵 · 𝐶 ) )
111	106 110	eqtrd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) = ( 𝐵 · 𝐶 ) )
112	45	3ad2ant1	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑄 = ( 𝐵 · 𝐵 ) )
113	111 112	oveq12d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) = ( ( 𝐵 · 𝐶 ) / ( 𝐵 · 𝐵 ) ) )
114	99 108 108 70 70	divcan5d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · 𝐶 ) / ( 𝐵 · 𝐵 ) ) = ( 𝐶 / 𝐵 ) )
115	113 114	eqtr2d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐶 / 𝐵 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
116	115	eqeq2d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑌 = ( 𝐶 / 𝐵 ) ↔ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
117	116	biimpa	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( 𝐶 / 𝐵 ) ) → 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
118	92 117	jctird	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( 𝐶 / 𝐵 ) ) → ( 𝑋 = - ( ( √ ‘ 𝐷 ) / 𝐵 ) → ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
119	75 118	orim12d	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( 𝐶 / 𝐵 ) ) → ( ( 𝑋 = ( ( √ ‘ 𝐷 ) / 𝐵 ) ∨ 𝑋 = - ( ( √ ‘ 𝐷 ) / 𝐵 ) ) → ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) )
120	4 119	biimtrid	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( 𝐶 / 𝐵 ) ) → ( ( 𝑋 = - ( ( √ ‘ 𝐷 ) / 𝐵 ) ∨ 𝑋 = ( ( √ ‘ 𝐷 ) / 𝐵 ) ) → ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) )
121	120	expimpd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝑌 = ( 𝐶 / 𝐵 ) ∧ ( 𝑋 = - ( ( √ ‘ 𝐷 ) / 𝐵 ) ∨ 𝑋 = ( ( √ ‘ 𝐷 ) / 𝐵 ) ) ) → ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) )
122	3 121	syld	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) )