Metamath Proof Explorer

Theorem itscnhlc0yqe

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

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

Proof

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