Metamath Proof Explorer


Theorem itsclquadb

Description: Quadratic equation for the y-coordinate of the intersection points of a line and a circle. (Contributed by AV, 22-Feb-2023)

Ref Expression
Hypotheses itsclquadb.q 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
itsclquadb.t 𝑇 = - ( 2 · ( 𝐵 · 𝐶 ) )
itsclquadb.u 𝑈 = ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) )
Assertion itsclquadb ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ∃ 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ↔ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) )

Proof

Step Hyp Ref Expression
1 itsclquadb.q 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
2 itsclquadb.t 𝑇 = - ( 2 · ( 𝐵 · 𝐶 ) )
3 itsclquadb.u 𝑈 = ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) )
4 simpl1 ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) )
5 simp2 ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → 𝑅 ∈ ℝ+ )
6 5 adantr ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → 𝑅 ∈ ℝ+ )
7 simp3 ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → 𝑌 ∈ ℝ )
8 7 anim1ci ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ℝ ∧ 𝑌 ∈ ℝ ) )
9 1 2 3 itscnhlc0yqe ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑥 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) )
10 4 6 8 9 syl3anc ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) )
11 10 rexlimdva ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ∃ 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) )
12 simp3 ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
13 12 3ad2ant1 ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → 𝐶 ∈ ℝ )
14 simp2 ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
15 14 3ad2ant1 ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → 𝐵 ∈ ℝ )
16 15 7 remulcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝐵 · 𝑌 ) ∈ ℝ )
17 13 16 resubcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝐶 − ( 𝐵 · 𝑌 ) ) ∈ ℝ )
18 simp11l ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → 𝐴 ∈ ℝ )
19 simp11r ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → 𝐴 ≠ 0 )
20 17 18 19 redivcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ∈ ℝ )
21 20 adantr ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) ∧ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) → ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ∈ ℝ )
22 oveq1 ( 𝑥 = ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) → ( 𝑥 ↑ 2 ) = ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) )
23 22 oveq1d ( 𝑥 = ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) → ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) + ( 𝑌 ↑ 2 ) ) )
24 23 eqeq1d ( 𝑥 = ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) → ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ↔ ( ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
25 oveq2 ( 𝑥 = ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) → ( 𝐴 · 𝑥 ) = ( 𝐴 · ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) )
26 25 oveq1d ( 𝑥 = ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) → ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = ( ( 𝐴 · ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) + ( 𝐵 · 𝑌 ) ) )
27 26 eqeq1d ( 𝑥 = ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) → ( ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ↔ ( ( 𝐴 · ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) )
28 24 27 anbi12d ( 𝑥 = ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) → ( ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ↔ ( ( ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) )
29 28 adantl ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) ∧ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) ∧ 𝑥 = ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) → ( ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ↔ ( ( ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) )
30 17 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝐶 − ( 𝐵 · 𝑌 ) ) ∈ ℂ )
31 18 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → 𝐴 ∈ ℂ )
32 30 31 19 sqdivd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) = ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) ↑ 2 ) / ( 𝐴 ↑ 2 ) ) )
33 13 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → 𝐶 ∈ ℂ )
34 16 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝐵 · 𝑌 ) ∈ ℂ )
35 binom2sub ( ( 𝐶 ∈ ℂ ∧ ( 𝐵 · 𝑌 ) ∈ ℂ ) → ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) ↑ 2 ) = ( ( ( 𝐶 ↑ 2 ) − ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) )
36 33 34 35 syl2anc ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) ↑ 2 ) = ( ( ( 𝐶 ↑ 2 ) − ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) )
37 13 resqcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝐶 ↑ 2 ) ∈ ℝ )
38 37 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝐶 ↑ 2 ) ∈ ℂ )
39 2re 2 ∈ ℝ
40 39 a1i ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → 2 ∈ ℝ )
41 13 16 remulcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝐶 · ( 𝐵 · 𝑌 ) ) ∈ ℝ )
42 40 41 remulcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) ∈ ℝ )
43 42 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) ∈ ℂ )
44 38 43 negsubd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) + - ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) ) = ( ( 𝐶 ↑ 2 ) − ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) ) )
45 15 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → 𝐵 ∈ ℂ )
46 7 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → 𝑌 ∈ ℂ )
47 33 45 46 mulassd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐶 · 𝐵 ) · 𝑌 ) = ( 𝐶 · ( 𝐵 · 𝑌 ) ) )
48 47 eqcomd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝐶 · ( 𝐵 · 𝑌 ) ) = ( ( 𝐶 · 𝐵 ) · 𝑌 ) )
49 48 oveq2d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) = ( 2 · ( ( 𝐶 · 𝐵 ) · 𝑌 ) ) )
50 2cnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → 2 ∈ ℂ )
51 13 15 remulcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝐶 · 𝐵 ) ∈ ℝ )
52 51 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
53 50 52 46 mulassd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 2 · ( 𝐶 · 𝐵 ) ) · 𝑌 ) = ( 2 · ( ( 𝐶 · 𝐵 ) · 𝑌 ) ) )
54 53 eqcomd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 2 · ( ( 𝐶 · 𝐵 ) · 𝑌 ) ) = ( ( 2 · ( 𝐶 · 𝐵 ) ) · 𝑌 ) )
55 33 45 mulcomd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝐶 · 𝐵 ) = ( 𝐵 · 𝐶 ) )
56 55 oveq2d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 2 · ( 𝐶 · 𝐵 ) ) = ( 2 · ( 𝐵 · 𝐶 ) ) )
57 56 oveq1d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 2 · ( 𝐶 · 𝐵 ) ) · 𝑌 ) = ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) )
58 49 54 57 3eqtrd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) = ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) )
59 58 negeqd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → - ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) = - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) )
60 59 oveq2d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) + - ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) ) = ( ( 𝐶 ↑ 2 ) + - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) ) )
61 44 60 eqtr3d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) − ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) ) = ( ( 𝐶 ↑ 2 ) + - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) ) )
62 45 46 sqmuld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐵 · 𝑌 ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) )
63 61 62 oveq12d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝐶 ↑ 2 ) − ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) = ( ( ( 𝐶 ↑ 2 ) + - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) )
64 15 13 remulcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝐵 · 𝐶 ) ∈ ℝ )
65 40 64 remulcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 2 · ( 𝐵 · 𝐶 ) ) ∈ ℝ )
66 65 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 2 · ( 𝐵 · 𝐶 ) ) ∈ ℂ )
67 66 46 mulneg1d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) = - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) )
68 2 eqcomi - ( 2 · ( 𝐵 · 𝐶 ) ) = 𝑇
69 68 oveq1i ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) = ( 𝑇 · 𝑌 )
70 69 a1i ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) = ( 𝑇 · 𝑌 ) )
71 67 70 eqtr3d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) = ( 𝑇 · 𝑌 ) )
72 71 oveq2d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) + - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) ) = ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) )
73 72 oveq1d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝐶 ↑ 2 ) + - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) = ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) )
74 36 63 73 3eqtrd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) ↑ 2 ) = ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) )
75 74 oveq1d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) ↑ 2 ) / ( 𝐴 ↑ 2 ) ) = ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) )
76 32 75 eqtrd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) = ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) )
77 resqcl ( 𝑌 ∈ ℝ → ( 𝑌 ↑ 2 ) ∈ ℝ )
78 77 recnd ( 𝑌 ∈ ℝ → ( 𝑌 ↑ 2 ) ∈ ℂ )
79 78 3ad2ant3 ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝑌 ↑ 2 ) ∈ ℂ )
80 18 resqcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
81 80 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
82 recn ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
83 sqne0 ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 2 ) ≠ 0 ↔ 𝐴 ≠ 0 ) )
84 82 83 syl ( 𝐴 ∈ ℝ → ( ( 𝐴 ↑ 2 ) ≠ 0 ↔ 𝐴 ≠ 0 ) )
85 84 biimpar ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐴 ↑ 2 ) ≠ 0 )
86 85 3ad2ant1 ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ↑ 2 ) ≠ 0 )
87 86 3ad2ant1 ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝐴 ↑ 2 ) ≠ 0 )
88 79 81 87 divcan2d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐴 ↑ 2 ) · ( ( 𝑌 ↑ 2 ) / ( 𝐴 ↑ 2 ) ) ) = ( 𝑌 ↑ 2 ) )
89 88 eqcomd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝑌 ↑ 2 ) = ( ( 𝐴 ↑ 2 ) · ( ( 𝑌 ↑ 2 ) / ( 𝐴 ↑ 2 ) ) ) )
90 76 89 oveq12d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝑌 ↑ 2 ) / ( 𝐴 ↑ 2 ) ) ) ) )
91 81 79 81 87 divassd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) / ( 𝐴 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) · ( ( 𝑌 ↑ 2 ) / ( 𝐴 ↑ 2 ) ) ) )
92 91 eqcomd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐴 ↑ 2 ) · ( ( 𝑌 ↑ 2 ) / ( 𝐴 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) / ( 𝐴 ↑ 2 ) ) )
93 92 oveq2d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝑌 ↑ 2 ) / ( 𝐴 ↑ 2 ) ) ) ) = ( ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) / ( 𝐴 ↑ 2 ) ) ) )
94 65 renegcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → - ( 2 · ( 𝐵 · 𝐶 ) ) ∈ ℝ )
95 2 94 eqeltrid ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → 𝑇 ∈ ℝ )
96 95 7 remulcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝑇 · 𝑌 ) ∈ ℝ )
97 37 96 readdcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) ∈ ℝ )
98 15 resqcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝐵 ↑ 2 ) ∈ ℝ )
99 7 resqcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝑌 ↑ 2 ) ∈ ℝ )
100 98 99 remulcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ∈ ℝ )
101 97 100 readdcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) ∈ ℝ )
102 101 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) ∈ ℂ )
103 80 99 remulcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ∈ ℝ )
104 103 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ∈ ℂ )
105 102 104 81 87 divdird ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) = ( ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) / ( 𝐴 ↑ 2 ) ) ) )
106 105 eqcomd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) / ( 𝐴 ↑ 2 ) ) ) = ( ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) )
107 90 93 106 3eqtrd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) )
108 107 adantr ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) ∧ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) → ( ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) )
109 97 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) ∈ ℂ )
110 100 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ∈ ℂ )
111 109 110 104 addassd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) = ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) ) )
112 98 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
113 99 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝑌 ↑ 2 ) ∈ ℂ )
114 112 81 113 adddird ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) = ( ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) )
115 112 81 addcomd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
116 115 oveq1d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) )
117 114 116 eqtr3d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) )
118 117 oveq2d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) ) = ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) ) )
119 96 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝑇 · 𝑌 ) ∈ ℂ )
120 80 98 readdcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∈ ℝ )
121 120 99 remulcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) ∈ ℝ )
122 121 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) ∈ ℂ )
123 38 119 122 addassd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) ) = ( ( 𝐶 ↑ 2 ) + ( ( 𝑇 · 𝑌 ) + ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) ) ) )
124 119 122 addcomd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝑇 · 𝑌 ) + ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) )
125 124 oveq2d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) + ( ( 𝑇 · 𝑌 ) + ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) ) ) = ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) )
126 123 125 eqtrd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) ) = ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) )
127 111 118 126 3eqtrd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) = ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) )
128 127 adantr ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) ∧ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) → ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) = ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) )
129 128 oveq1d ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) ∧ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) → ( ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) = ( ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) / ( 𝐴 ↑ 2 ) ) )
130 1 oveq1i ( 𝑄 · ( 𝑌 ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) )
131 3 oveq2i ( ( 𝑇 · 𝑌 ) + 𝑈 ) = ( ( 𝑇 · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) )
132 130 131 oveq12i ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) )
133 rpre ( 𝑅 ∈ ℝ+𝑅 ∈ ℝ )
134 133 resqcld ( 𝑅 ∈ ℝ+ → ( 𝑅 ↑ 2 ) ∈ ℝ )
135 134 3ad2ant2 ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝑅 ↑ 2 ) ∈ ℝ )
136 80 135 remulcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ∈ ℝ )
137 37 136 resubcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ∈ ℝ )
138 137 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ∈ ℂ )
139 122 119 138 addassd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) )
140 132 139 eqtr4id ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = ( ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) )
141 140 eqeq1d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ↔ ( ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = 0 ) )
142 121 96 readdcld ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ∈ ℝ )
143 142 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ∈ ℂ )
144 addeq0 ( ( ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ∈ ℂ ∧ ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ∈ ℂ ) → ( ( ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = 0 ↔ ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) = - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) )
145 143 138 144 syl2anc ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = 0 ↔ ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) = - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) )
146 141 145 bitrd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ↔ ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) = - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) )
147 oveq2 ( ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) = - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) → ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) = ( ( 𝐶 ↑ 2 ) + - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) )
148 147 oveq1d ( ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) = - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) → ( ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) / ( 𝐴 ↑ 2 ) ) = ( ( ( 𝐶 ↑ 2 ) + - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) / ( 𝐴 ↑ 2 ) ) )
149 38 138 negsubd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) + - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = ( ( 𝐶 ↑ 2 ) − ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) )
150 136 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ∈ ℂ )
151 38 150 nncand ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) − ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) )
152 149 151 eqtrd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) + - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) )
153 152 oveq1d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝐶 ↑ 2 ) + - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) / ( 𝐴 ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) / ( 𝐴 ↑ 2 ) ) )
154 135 recnd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝑅 ↑ 2 ) ∈ ℂ )
155 154 81 87 divcan3d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) / ( 𝐴 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) )
156 153 155 eqtrd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝐶 ↑ 2 ) + - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) / ( 𝐴 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) )
157 148 156 sylan9eqr ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) ∧ ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) = - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) → ( ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) / ( 𝐴 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) )
158 157 ex ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) = - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) → ( ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) / ( 𝐴 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
159 146 158 sylbid ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 → ( ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) / ( 𝐴 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
160 159 imp ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) ∧ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) → ( ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) / ( 𝐴 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) )
161 108 129 160 3eqtrd ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) ∧ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) → ( ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) )
162 30 31 19 divcan2d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( 𝐴 · ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) = ( 𝐶 − ( 𝐵 · 𝑌 ) ) )
163 162 oveq1d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐴 · ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) + ( 𝐵 · 𝑌 ) ) = ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) + ( 𝐵 · 𝑌 ) ) )
164 33 34 npcand ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) + ( 𝐵 · 𝑌 ) ) = 𝐶 )
165 163 164 eqtrd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( 𝐴 · ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) + ( 𝐵 · 𝑌 ) ) = 𝐶 )
166 165 adantr ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) ∧ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) → ( ( 𝐴 · ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) + ( 𝐵 · 𝑌 ) ) = 𝐶 )
167 161 166 jca ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) ∧ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) → ( ( ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) )
168 21 29 167 rspcedvd ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) ∧ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) → ∃ 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) )
169 168 ex ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 → ∃ 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) )
170 11 169 impbid ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+𝑌 ∈ ℝ ) → ( ∃ 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ↔ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) )