Metamath Proof Explorer

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 addid2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 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 addid2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 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 syl5eq ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 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 addid1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 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 syl5bi ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( 𝐶 / 𝐵 ) ) → ( ( 𝑋 = - ( ( √ ‘ 𝐷 ) / 𝐵 ) ∨ 𝑋 = ( ( √ ‘ 𝐷 ) / 𝐵 ) ) → ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) )
121 120 expimpd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝑌 = ( 𝐶 / 𝐵 ) ∧ ( 𝑋 = - ( ( √ ‘ 𝐷 ) / 𝐵 ) ∨ 𝑋 = ( ( √ ‘ 𝐷 ) / 𝐵 ) ) ) → ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) )
122 3 121 syld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) )