Metamath Proof Explorer

Theorem itsclc0yqsol

Description: Lemma for itsclc0 . Solutions of the quadratic equations for the y-coordinate of the intersection points of a (nondegenerate) line and a circle. (Contributed by AV, 7-Feb-2023)

Ref Expression
Hypotheses itscnhlc0yqe.q ⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
itsclc0yqsol.d ⊢ 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
Assertion itsclc0yqsol ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )

Proof

Step Hyp Ref Expression
1 itscnhlc0yqe.q ⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
2 itsclc0yqsol.d ⊢ 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
3 eqid ⊢ - ( 2 · ( 𝐵 · 𝐶 ) ) = - ( 2 · ( 𝐵 · 𝐶 ) )
4 eqid ⊢ ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) = ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) )
5 1 3 4 itsclc0yqe ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) )
6 5 3adant1r ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) )
7 6 3adant2r ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) )
8 3simpa ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
9 8 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
10 1 resum2sqcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝑄 ∈ ℝ )
11 9 10 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) → 𝑄 ∈ ℝ )
12 11 3ad2ant1 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑄 ∈ ℝ )
13 12 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑄 ∈ ℂ )
14 simpr1 ⊢ ( ( 𝐴 ≠ 0 ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐴 ∈ ℝ )
15 simpl ⊢ ( ( 𝐴 ≠ 0 ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐴 ≠ 0 )
16 simpr2 ⊢ ( ( 𝐴 ≠ 0 ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐵 ∈ ℝ )
17 1 resum2sqgt0 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → 0 < 𝑄 )
18 14 15 16 17 syl21anc ⊢ ( ( 𝐴 ≠ 0 ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 0 < 𝑄 )
19 18 ex ⊢ ( 𝐴 ≠ 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 0 < 𝑄 ) )
20 simpr2 ⊢ ( ( 𝐵 ≠ 0 ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐵 ∈ ℝ )
21 simpl ⊢ ( ( 𝐵 ≠ 0 ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐵 ≠ 0 )
22 simpr1 ⊢ ( ( 𝐵 ≠ 0 ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐴 ∈ ℝ )
23 eqid ⊢ ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) )
24 23 resum2sqgt0 ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ∈ ℝ ) → 0 < ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) )
25 20 21 22 24 syl21anc ⊢ ( ( 𝐵 ≠ 0 ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 0 < ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) )
26 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
27 26 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℂ )
28 27 sqcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
29 simp2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
30 29 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
31 30 sqcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
32 28 31 addcomd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) )
33 32 adantl ⊢ ( ( 𝐵 ≠ 0 ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) )
34 1 33 syl5eq ⊢ ( ( 𝐵 ≠ 0 ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝑄 = ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) )
35 25 34 breqtrrd ⊢ ( ( 𝐵 ≠ 0 ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 0 < 𝑄 )
36 35 ex ⊢ ( 𝐵 ≠ 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 0 < 𝑄 ) )
37 19 36 jaoi ⊢ ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 0 < 𝑄 ) )
38 37 impcom ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) → 0 < 𝑄 )
39 38 gt0ne0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) → 𝑄 ≠ 0 )
40 39 3ad2ant1 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑄 ≠ 0 )
41 2cnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 2 ∈ ℂ )
42 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
43 42 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
44 43 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) → 𝐵 ∈ ℂ )
45 44 3ad2ant1 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐵 ∈ ℂ )
46 recn ⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
47 46 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℂ )
48 47 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) → 𝐶 ∈ ℂ )
49 48 3ad2ant1 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐶 ∈ ℂ )
50 45 49 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
51 41 50 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 2 · ( 𝐵 · 𝐶 ) ) ∈ ℂ )
52 51 negcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → - ( 2 · ( 𝐵 · 𝐶 ) ) ∈ ℂ )
53 49 sqcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐶 ↑ 2 ) ∈ ℂ )
54 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
55 54 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℂ )
56 55 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) → 𝐴 ∈ ℂ )
57 56 3ad2ant1 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐴 ∈ ℂ )
58 57 sqcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
59 simpl ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) → 𝑅 ∈ ℝ+ )
60 59 rpcnd ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) → 𝑅 ∈ ℂ )
61 60 3ad2ant2 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑅 ∈ ℂ )
62 61 sqcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑅 ↑ 2 ) ∈ ℂ )
63 58 62 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ∈ ℂ )
64 53 63 subcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ∈ ℂ )
65 recn ⊢ ( 𝑌 ∈ ℝ → 𝑌 ∈ ℂ )
66 65 adantl ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → 𝑌 ∈ ℂ )
67 66 3ad2ant3 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑌 ∈ ℂ )
68 eqidd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( 𝑄 · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) = ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( 𝑄 · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) )
69 13 40 52 64 67 68 quad ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ↔ ( 𝑌 = ( ( - - ( 2 · ( 𝐵 · 𝐶 ) ) + ( √ ‘ ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( 𝑄 · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) ) / ( 2 · 𝑄 ) ) ∨ 𝑌 = ( ( - - ( 2 · ( 𝐵 · 𝐶 ) ) − ( √ ‘ ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( 𝑄 · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) ) / ( 2 · 𝑄 ) ) ) ) )
70 54 abscld ⊢ ( 𝐴 ∈ ℝ → ( abs ‘ 𝐴 ) ∈ ℝ )
71 70 recnd ⊢ ( 𝐴 ∈ ℝ → ( abs ‘ 𝐴 ) ∈ ℂ )
72 71 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( abs ‘ 𝐴 ) ∈ ℂ )
73 72 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) → ( abs ‘ 𝐴 ) ∈ ℂ )
74 73 3ad2ant1 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( abs ‘ 𝐴 ) ∈ ℂ )
75 59 rpred ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) → 𝑅 ∈ ℝ )
76 75 3ad2ant2 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑅 ∈ ℝ )
77 76 resqcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑅 ↑ 2 ) ∈ ℝ )
78 77 12 remulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝑅 ↑ 2 ) · 𝑄 ) ∈ ℝ )
79 simp1l3 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐶 ∈ ℝ )
80 79 resqcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐶 ↑ 2 ) ∈ ℝ )
81 78 80 resubcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) ) ∈ ℝ )
82 2 81 eqeltrid ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐷 ∈ ℝ )
83 82 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐷 ∈ ℂ )
84 83 sqrtcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( √ ‘ 𝐷 ) ∈ ℂ )
85 41 74 84 mulassd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 2 · ( abs ‘ 𝐴 ) ) · ( √ ‘ 𝐷 ) ) = ( 2 · ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) )
86 85 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 2 · ( 𝐵 · 𝐶 ) ) + ( ( 2 · ( abs ‘ 𝐴 ) ) · ( √ ‘ 𝐷 ) ) ) = ( ( 2 · ( 𝐵 · 𝐶 ) ) + ( 2 · ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) ) )
87 51 negnegd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → - - ( 2 · ( 𝐵 · 𝐶 ) ) = ( 2 · ( 𝐵 · 𝐶 ) ) )
88 simpl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) )
89 88 3ad2ant1 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) )
90 simp2r ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 0 ≤ 𝐷 )
91 1 3 4 2 itsclc0yqsollem2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( √ ‘ ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( 𝑄 · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) = ( ( 2 · ( abs ‘ 𝐴 ) ) · ( √ ‘ 𝐷 ) ) )
92 89 76 90 91 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( √ ‘ ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( 𝑄 · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) = ( ( 2 · ( abs ‘ 𝐴 ) ) · ( √ ‘ 𝐷 ) ) )
93 87 92 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( - - ( 2 · ( 𝐵 · 𝐶 ) ) + ( √ ‘ ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( 𝑄 · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) ) = ( ( 2 · ( 𝐵 · 𝐶 ) ) + ( ( 2 · ( abs ‘ 𝐴 ) ) · ( √ ‘ 𝐷 ) ) ) )
94 74 84 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ∈ ℂ )
95 41 50 94 adddid ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 2 · ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) ) = ( ( 2 · ( 𝐵 · 𝐶 ) ) + ( 2 · ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) ) )
96 86 93 95 3eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( - - ( 2 · ( 𝐵 · 𝐶 ) ) + ( √ ‘ ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( 𝑄 · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) ) = ( 2 · ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) ) )
97 96 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( - - ( 2 · ( 𝐵 · 𝐶 ) ) + ( √ ‘ ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( 𝑄 · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) ) / ( 2 · 𝑄 ) ) = ( ( 2 · ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) ) / ( 2 · 𝑄 ) ) )
98 50 94 addcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) ∈ ℂ )
99 2ne0 ⊢ 2 ≠ 0
100 99 a1i ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 2 ≠ 0 )
101 98 13 41 40 100 divcan5d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 2 · ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) ) / ( 2 · 𝑄 ) ) = ( ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
102 97 101 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( - - ( 2 · ( 𝐵 · 𝐶 ) ) + ( √ ‘ ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( 𝑄 · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) ) / ( 2 · 𝑄 ) ) = ( ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
103 102 eqeq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑌 = ( ( - - ( 2 · ( 𝐵 · 𝐶 ) ) + ( √ ‘ ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( 𝑄 · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) ) / ( 2 · 𝑄 ) ) ↔ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
104 85 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 2 · ( 𝐵 · 𝐶 ) ) − ( ( 2 · ( abs ‘ 𝐴 ) ) · ( √ ‘ 𝐷 ) ) ) = ( ( 2 · ( 𝐵 · 𝐶 ) ) − ( 2 · ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) ) )
105 87 92 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( - - ( 2 · ( 𝐵 · 𝐶 ) ) − ( √ ‘ ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( 𝑄 · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) ) = ( ( 2 · ( 𝐵 · 𝐶 ) ) − ( ( 2 · ( abs ‘ 𝐴 ) ) · ( √ ‘ 𝐷 ) ) ) )
106 41 50 94 subdid ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 2 · ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) ) = ( ( 2 · ( 𝐵 · 𝐶 ) ) − ( 2 · ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) ) )
107 104 105 106 3eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( - - ( 2 · ( 𝐵 · 𝐶 ) ) − ( √ ‘ ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( 𝑄 · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) ) = ( 2 · ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) ) )
108 107 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( - - ( 2 · ( 𝐵 · 𝐶 ) ) − ( √ ‘ ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( 𝑄 · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) ) / ( 2 · 𝑄 ) ) = ( ( 2 · ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) ) / ( 2 · 𝑄 ) ) )
109 50 94 subcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) ∈ ℂ )
110 109 13 41 40 100 divcan5d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 2 · ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) ) / ( 2 · 𝑄 ) ) = ( ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
111 108 110 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( - - ( 2 · ( 𝐵 · 𝐶 ) ) − ( √ ‘ ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( 𝑄 · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) ) / ( 2 · 𝑄 ) ) = ( ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
112 111 eqeq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑌 = ( ( - - ( 2 · ( 𝐵 · 𝐶 ) ) − ( √ ‘ ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( 𝑄 · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) ) / ( 2 · 𝑄 ) ) ↔ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
113 103 112 orbi12d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝑌 = ( ( - - ( 2 · ( 𝐵 · 𝐶 ) ) + ( √ ‘ ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( 𝑄 · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) ) / ( 2 · 𝑄 ) ) ∨ 𝑌 = ( ( - - ( 2 · ( 𝐵 · 𝐶 ) ) − ( √ ‘ ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( 𝑄 · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) ) / ( 2 · 𝑄 ) ) ) ↔ ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
114 69 113 bitrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ↔ ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
115 absid ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( abs ‘ 𝐴 ) = 𝐴 )
116 115 ex ⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 → ( abs ‘ 𝐴 ) = 𝐴 ) )
117 116 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 0 ≤ 𝐴 → ( abs ‘ 𝐴 ) = 𝐴 ) )
118 117 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) → ( 0 ≤ 𝐴 → ( abs ‘ 𝐴 ) = 𝐴 ) )
119 118 3ad2ant1 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 0 ≤ 𝐴 → ( abs ‘ 𝐴 ) = 𝐴 ) )
120 119 impcom ⊢ ( ( 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( abs ‘ 𝐴 ) = 𝐴 )
121 120 oveq1d ⊢ ( ( 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) = ( 𝐴 · ( √ ‘ 𝐷 ) ) )
122 121 oveq2d ⊢ ( ( 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) = ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) )
123 122 oveq1d ⊢ ( ( 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
124 123 eqeq2d ⊢ ( ( 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↔ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
125 121 oveq2d ⊢ ( ( 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) = ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) )
126 125 oveq1d ⊢ ( ( 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
127 126 eqeq2d ⊢ ( ( 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↔ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
128 124 127 orbi12d ⊢ ( ( 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ↔ ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
129 pm1.4 ⊢ ( ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
130 128 129 syl6bi ⊢ ( ( 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
131 50 adantl ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
132 94 adantl ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ∈ ℂ )
133 131 132 subnegd ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( ( 𝐵 · 𝐶 ) − - ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) = ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) )
134 74 adantl ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( abs ‘ 𝐴 ) ∈ ℂ )
135 84 adantl ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( √ ‘ 𝐷 ) ∈ ℂ )
136 134 135 mulneg1d ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( - ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) = - ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) )
137 89 simp1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐴 ∈ ℝ )
138 137 adantl ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → 𝐴 ∈ ℝ )
139 id ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
140 0red ⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ )
141 139 140 ltnled ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < 0 ↔ ¬ 0 ≤ 𝐴 ) )
142 ltle ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐴 < 0 → 𝐴 ≤ 0 ) )
143 140 142 mpdan ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < 0 → 𝐴 ≤ 0 ) )
144 141 143 sylbird ⊢ ( 𝐴 ∈ ℝ → ( ¬ 0 ≤ 𝐴 → 𝐴 ≤ 0 ) )
145 144 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ¬ 0 ≤ 𝐴 → 𝐴 ≤ 0 ) )
146 145 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) → ( ¬ 0 ≤ 𝐴 → 𝐴 ≤ 0 ) )
147 146 3ad2ant1 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ¬ 0 ≤ 𝐴 → 𝐴 ≤ 0 ) )
148 147 impcom ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → 𝐴 ≤ 0 )
149 138 148 absnidd ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( abs ‘ 𝐴 ) = - 𝐴 )
150 149 negeqd ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → - ( abs ‘ 𝐴 ) = - - 𝐴 )
151 57 adantl ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → 𝐴 ∈ ℂ )
152 151 negnegd ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → - - 𝐴 = 𝐴 )
153 150 152 eqtrd ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → - ( abs ‘ 𝐴 ) = 𝐴 )
154 153 oveq1d ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( - ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) = ( 𝐴 · ( √ ‘ 𝐷 ) ) )
155 136 154 eqtr3d ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → - ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) = ( 𝐴 · ( √ ‘ 𝐷 ) ) )
156 155 oveq2d ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( ( 𝐵 · 𝐶 ) − - ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) = ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) )
157 133 156 eqtr3d ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) = ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) )
158 157 oveq1d ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
159 158 eqeq2d ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↔ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
160 131 132 negsubd ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( ( 𝐵 · 𝐶 ) + - ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) = ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) )
161 155 oveq2d ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( ( 𝐵 · 𝐶 ) + - ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) = ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) )
162 160 161 eqtr3d ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) = ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) )
163 162 oveq1d ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
164 163 eqeq2d ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↔ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
165 159 164 orbi12d ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ↔ ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
166 165 biimpd ⊢ ( ( ¬ 0 ≤ 𝐴 ∧ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ) → ( ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
167 130 166 pm2.61ian ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( ( abs ‘ 𝐴 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
168 114 167 sylbid ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
169 7 168 syld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )