Metamath Proof Explorer

Theorem itsclc0xyqsolr

Description: Lemma for itsclc0 . Solutions of the quadratic equations for the coordinates of the intersection points of a (nondegenerate) line and a circle. (Contributed by AV, 2-May-2023) (Revised by AV, 14-May-2023)

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

Proof

Step Hyp Ref Expression
1 itsclc0xyqsolr.q ⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
2 itsclc0xyqsolr.d ⊢ 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
3 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
4 3 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℂ )
5 4 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐴 ∈ ℂ )
6 recn ⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
7 6 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℂ )
8 7 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐶 ∈ ℂ )
9 5 8 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
10 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
11 10 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
12 11 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐵 ∈ ℂ )
13 rpre ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ )
14 13 adantr ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) → 𝑅 ∈ ℝ )
15 14 anim2i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ) )
16 15 3adant2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ) )
17 1 2 itsclc0lem3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ) → 𝐷 ∈ ℝ )
18 16 17 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐷 ∈ ℝ )
19 18 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐷 ∈ ℂ )
20 19 sqrtcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( √ ‘ 𝐷 ) ∈ ℂ )
21 12 20 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · ( √ ‘ 𝐷 ) ) ∈ ℂ )
22 9 21 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ∈ ℂ )
23 1 resum2sqcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝑄 ∈ ℝ )
24 23 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝑄 ∈ ℝ )
25 24 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝑄 ∈ ℂ )
26 25 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝑄 ∈ ℂ )
27 simp11 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐴 ∈ ℝ )
28 simp12 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐵 ∈ ℝ )
29 simp2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) )
30 1 resum2sqorgt0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) → 0 < 𝑄 )
31 27 28 29 30 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 0 < 𝑄 )
32 31 gt0ne0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝑄 ≠ 0 )
33 22 26 32 sqdivd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) = ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ↑ 2 ) / ( 𝑄 ↑ 2 ) ) )
34 4 7 mulcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
35 34 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
36 binom2 ⊢ ( ( ( 𝐴 · 𝐶 ) ∈ ℂ ∧ ( 𝐵 · ( √ ‘ 𝐷 ) ) ∈ ℂ ) → ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ↑ 2 ) = ( ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 · ( √ ‘ 𝐷 ) ) ↑ 2 ) ) )
37 35 21 36 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ↑ 2 ) = ( ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 · ( √ ‘ 𝐷 ) ) ↑ 2 ) ) )
38 4 7 sqmuld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 · 𝐶 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) )
39 38 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · 𝐶 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) )
40 39 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) )
41 12 20 sqmuld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · ( √ ‘ 𝐷 ) ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) · ( ( √ ‘ 𝐷 ) ↑ 2 ) ) )
42 simp3r ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 0 ≤ 𝐷 )
43 resqrtth ⊢ ( ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( ( √ ‘ 𝐷 ) ↑ 2 ) = 𝐷 )
44 18 42 43 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( √ ‘ 𝐷 ) ↑ 2 ) = 𝐷 )
45 44 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 ↑ 2 ) · ( ( √ ‘ 𝐷 ) ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) · 𝐷 ) )
46 41 45 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · ( √ ‘ 𝐷 ) ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) · 𝐷 ) )
47 40 46 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 · ( √ ‘ 𝐷 ) ) ↑ 2 ) ) = ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) )
48 37 47 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ↑ 2 ) = ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) )
49 48 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ↑ 2 ) / ( 𝑄 ↑ 2 ) ) = ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) )
50 33 49 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) = ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) )
51 12 8 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
52 5 20 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · ( √ ‘ 𝐷 ) ) ∈ ℂ )
53 51 52 subcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ∈ ℂ )
54 53 26 32 sqdivd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) = ( ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ↑ 2 ) / ( 𝑄 ↑ 2 ) ) )
55 27 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐴 ∈ ℂ )
56 55 20 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · ( √ ‘ 𝐷 ) ) ∈ ℂ )
57 binom2sub ⊢ ( ( ( 𝐵 · 𝐶 ) ∈ ℂ ∧ ( 𝐴 · ( √ ‘ 𝐷 ) ) ∈ ℂ ) → ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ↑ 2 ) = ( ( ( ( 𝐵 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐵 · 𝐶 ) · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 · ( √ ‘ 𝐷 ) ) ↑ 2 ) ) )
58 51 56 57 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ↑ 2 ) = ( ( ( ( 𝐵 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐵 · 𝐶 ) · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 · ( √ ‘ 𝐷 ) ) ↑ 2 ) ) )
59 11 7 sqmuld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐵 · 𝐶 ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) )
60 59 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · 𝐶 ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) )
61 12 8 55 20 mul4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · 𝐶 ) · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) = ( ( 𝐵 · 𝐴 ) · ( 𝐶 · ( √ ‘ 𝐷 ) ) ) )
62 12 55 mulcomd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · 𝐴 ) = ( 𝐴 · 𝐵 ) )
63 62 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · 𝐴 ) · ( 𝐶 · ( √ ‘ 𝐷 ) ) ) = ( ( 𝐴 · 𝐵 ) · ( 𝐶 · ( √ ‘ 𝐷 ) ) ) )
64 55 12 8 20 mul4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · 𝐵 ) · ( 𝐶 · ( √ ‘ 𝐷 ) ) ) = ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) )
65 63 64 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · 𝐴 ) · ( 𝐶 · ( √ ‘ 𝐷 ) ) ) = ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) )
66 61 65 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · 𝐶 ) · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) = ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) )
67 66 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 2 · ( ( 𝐵 · 𝐶 ) · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) = ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) )
68 60 67 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐵 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐵 · 𝐶 ) · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) = ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) )
69 55 20 sqmuld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · ( √ ‘ 𝐷 ) ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) · ( ( √ ‘ 𝐷 ) ↑ 2 ) ) )
70 44 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 ↑ 2 ) · ( ( √ ‘ 𝐷 ) ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) · 𝐷 ) )
71 69 70 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · ( √ ‘ 𝐷 ) ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) · 𝐷 ) )
72 68 71 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐵 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐵 · 𝐶 ) · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 · ( √ ‘ 𝐷 ) ) ↑ 2 ) ) = ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) )
73 58 72 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ↑ 2 ) = ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) )
74 73 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ↑ 2 ) / ( 𝑄 ↑ 2 ) ) = ( ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) )
75 54 74 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) = ( ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) )
76 50 75 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) + ( ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) ) = ( ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) + ( ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) ) )
77 5 sqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
78 8 sqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐶 ↑ 2 ) ∈ ℂ )
79 77 78 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ∈ ℂ )
80 2cnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 2 ∈ ℂ )
81 9 21 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ∈ ℂ )
82 80 81 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ∈ ℂ )
83 79 82 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) ∈ ℂ )
84 12 sqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
85 84 19 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 ↑ 2 ) · 𝐷 ) ∈ ℂ )
86 83 85 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) ∈ ℂ )
87 84 78 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ∈ ℂ )
88 87 82 subcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) ∈ ℂ )
89 77 19 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 ↑ 2 ) · 𝐷 ) ∈ ℂ )
90 88 89 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ∈ ℂ )
91 26 sqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑄 ↑ 2 ) ∈ ℂ )
92 2z ⊢ 2 ∈ ℤ
93 92 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 2 ∈ ℤ )
94 26 32 93 expne0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑄 ↑ 2 ) ≠ 0 )
95 86 90 91 94 divdird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) + ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) / ( 𝑄 ↑ 2 ) ) = ( ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) + ( ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) ) )
96 83 85 88 89 add4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) + ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) = ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) ) + ( ( ( 𝐵 ↑ 2 ) · 𝐷 ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) )
97 79 82 87 ppncand ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
98 55 sqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
99 98 84 78 adddird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝐶 ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
100 1 eqcomi ⊢ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 𝑄
101 100 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 𝑄 )
102 101 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝐶 ↑ 2 ) ) = ( 𝑄 · ( 𝐶 ↑ 2 ) ) )
103 97 99 102 3eqtr2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) ) = ( 𝑄 · ( 𝐶 ↑ 2 ) ) )
104 84 98 19 adddird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) · 𝐷 ) = ( ( ( 𝐵 ↑ 2 ) · 𝐷 ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) )
105 84 98 addcomd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
106 105 101 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = 𝑄 )
107 106 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) · 𝐷 ) = ( 𝑄 · 𝐷 ) )
108 104 107 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐵 ↑ 2 ) · 𝐷 ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) = ( 𝑄 · 𝐷 ) )
109 103 108 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) ) + ( ( ( 𝐵 ↑ 2 ) · 𝐷 ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) = ( ( 𝑄 · ( 𝐶 ↑ 2 ) ) + ( 𝑄 · 𝐷 ) ) )
110 96 109 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) + ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) = ( ( 𝑄 · ( 𝐶 ↑ 2 ) ) + ( 𝑄 · 𝐷 ) ) )
111 110 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) + ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) / ( 𝑄 ↑ 2 ) ) = ( ( ( 𝑄 · ( 𝐶 ↑ 2 ) ) + ( 𝑄 · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) )
112 26 78 19 adddid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑄 · ( ( 𝐶 ↑ 2 ) + 𝐷 ) ) = ( ( 𝑄 · ( 𝐶 ↑ 2 ) ) + ( 𝑄 · 𝐷 ) ) )
113 112 eqcomd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑄 · ( 𝐶 ↑ 2 ) ) + ( 𝑄 · 𝐷 ) ) = ( 𝑄 · ( ( 𝐶 ↑ 2 ) + 𝐷 ) ) )
114 26 sqvald ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑄 ↑ 2 ) = ( 𝑄 · 𝑄 ) )
115 113 114 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝑄 · ( 𝐶 ↑ 2 ) ) + ( 𝑄 · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) = ( ( 𝑄 · ( ( 𝐶 ↑ 2 ) + 𝐷 ) ) / ( 𝑄 · 𝑄 ) ) )
116 78 19 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐶 ↑ 2 ) + 𝐷 ) ∈ ℂ )
117 116 26 26 32 32 divcan5d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑄 · ( ( 𝐶 ↑ 2 ) + 𝐷 ) ) / ( 𝑄 · 𝑄 ) ) = ( ( ( 𝐶 ↑ 2 ) + 𝐷 ) / 𝑄 ) )
118 115 117 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝑄 · ( 𝐶 ↑ 2 ) ) + ( 𝑄 · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) = ( ( ( 𝐶 ↑ 2 ) + 𝐷 ) / 𝑄 ) )
119 2 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) ) )
120 119 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐶 ↑ 2 ) + 𝐷 ) = ( ( 𝐶 ↑ 2 ) + ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) ) ) )
121 rpcn ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℂ )
122 121 adantr ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) → 𝑅 ∈ ℂ )
123 122 3ad2ant3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝑅 ∈ ℂ )
124 123 sqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑅 ↑ 2 ) ∈ ℂ )
125 124 26 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑅 ↑ 2 ) · 𝑄 ) ∈ ℂ )
126 78 125 pncan3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐶 ↑ 2 ) + ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) ) ) = ( ( 𝑅 ↑ 2 ) · 𝑄 ) )
127 120 126 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐶 ↑ 2 ) + 𝐷 ) = ( ( 𝑅 ↑ 2 ) · 𝑄 ) )
128 116 124 26 32 divmul3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐶 ↑ 2 ) + 𝐷 ) / 𝑄 ) = ( 𝑅 ↑ 2 ) ↔ ( ( 𝐶 ↑ 2 ) + 𝐷 ) = ( ( 𝑅 ↑ 2 ) · 𝑄 ) ) )
129 127 128 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐶 ↑ 2 ) + 𝐷 ) / 𝑄 ) = ( 𝑅 ↑ 2 ) )
130 118 129 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝑄 · ( 𝐶 ↑ 2 ) ) + ( 𝑄 · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) )
131 111 130 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) + ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) / ( 𝑄 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) )
132 76 95 131 3eqtr2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) + ( ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) )
133 5 22 26 32 divassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) = ( 𝐴 · ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
134 5 9 21 adddid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) = ( ( 𝐴 · ( 𝐴 · 𝐶 ) ) + ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) )
135 3 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℂ )
136 6 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℂ )
137 135 135 136 mulassd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 · 𝐴 ) · 𝐶 ) = ( 𝐴 · ( 𝐴 · 𝐶 ) ) )
138 135 sqvald ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
139 138 eqcomd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 𝐴 ) = ( 𝐴 ↑ 2 ) )
140 139 oveq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 · 𝐴 ) · 𝐶 ) = ( ( 𝐴 ↑ 2 ) · 𝐶 ) )
141 137 140 eqtr3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · ( 𝐴 · 𝐶 ) ) = ( ( 𝐴 ↑ 2 ) · 𝐶 ) )
142 141 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · ( 𝐴 · 𝐶 ) ) = ( ( 𝐴 ↑ 2 ) · 𝐶 ) )
143 142 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · ( 𝐴 · 𝐶 ) ) = ( ( 𝐴 ↑ 2 ) · 𝐶 ) )
144 5 12 20 mulassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) = ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) )
145 144 eqcomd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) = ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) )
146 143 145 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · ( 𝐴 · 𝐶 ) ) + ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) )
147 134 146 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) )
148 147 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) = ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
149 133 148 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) = ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
150 12 53 26 32 divassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) = ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
151 12 51 52 subdid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) = ( ( 𝐵 · ( 𝐵 · 𝐶 ) ) − ( 𝐵 · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) )
152 simpl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
153 152 recnd ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
154 simpr ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
155 154 recnd ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℂ )
156 153 153 155 mulassd ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐵 · 𝐵 ) · 𝐶 ) = ( 𝐵 · ( 𝐵 · 𝐶 ) ) )
157 10 sqvald ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 ↑ 2 ) = ( 𝐵 · 𝐵 ) )
158 157 eqcomd ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 · 𝐵 ) = ( 𝐵 ↑ 2 ) )
159 158 adantr ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 · 𝐵 ) = ( 𝐵 ↑ 2 ) )
160 159 oveq1d ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐵 · 𝐵 ) · 𝐶 ) = ( ( 𝐵 ↑ 2 ) · 𝐶 ) )
161 156 160 eqtr3d ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 · ( 𝐵 · 𝐶 ) ) = ( ( 𝐵 ↑ 2 ) · 𝐶 ) )
162 161 3adant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 · ( 𝐵 · 𝐶 ) ) = ( ( 𝐵 ↑ 2 ) · 𝐶 ) )
163 162 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · ( 𝐵 · 𝐶 ) ) = ( ( 𝐵 ↑ 2 ) · 𝐶 ) )
164 12 5 20 mulassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · 𝐴 ) · ( √ ‘ 𝐷 ) ) = ( 𝐵 · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) )
165 11 4 mulcomd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 · 𝐴 ) = ( 𝐴 · 𝐵 ) )
166 165 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · 𝐴 ) = ( 𝐴 · 𝐵 ) )
167 166 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · 𝐴 ) · ( √ ‘ 𝐷 ) ) = ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) )
168 164 167 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) = ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) )
169 163 168 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · ( 𝐵 · 𝐶 ) ) − ( 𝐵 · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) = ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) )
170 151 169 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) = ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) )
171 170 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) = ( ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
172 150 171 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) = ( ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
173 149 172 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) = ( ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) + ( ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
174 77 8 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 ↑ 2 ) · 𝐶 ) ∈ ℂ )
175 5 12 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
176 175 20 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ∈ ℂ )
177 174 176 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) ∈ ℂ )
178 84 8 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 ↑ 2 ) · 𝐶 ) ∈ ℂ )
179 178 176 subcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) ∈ ℂ )
180 177 179 26 32 divdird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) = ( ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) + ( ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
181 174 176 178 ppncand ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) )
182 77 84 8 adddird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · 𝐶 ) = ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) )
183 1 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
184 183 eqcomd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 𝑄 )
185 184 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · 𝐶 ) = ( 𝑄 · 𝐶 ) )
186 181 182 185 3eqtr2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) ) = ( 𝑄 · 𝐶 ) )
187 177 179 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) ) ∈ ℂ )
188 187 8 26 32 divmul2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) = 𝐶 ↔ ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) ) = ( 𝑄 · 𝐶 ) ) )
189 186 188 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) = 𝐶 )
190 173 180 189 3eqtr2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) = 𝐶 )
191 132 190 jca ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) + ( ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) = 𝐶 ) )
192 oveq1 ⊢ ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → ( 𝑋 ↑ 2 ) = ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) )
193 oveq1 ⊢ ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → ( 𝑌 ↑ 2 ) = ( ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) )
194 192 193 oveqan12d ⊢ ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) + ( ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) ) )
195 194 eqeq1d ⊢ ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ↔ ( ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) + ( ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
196 oveq2 ⊢ ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → ( 𝐴 · 𝑋 ) = ( 𝐴 · ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
197 oveq2 ⊢ ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → ( 𝐵 · 𝑌 ) = ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
198 196 197 oveqan12d ⊢ ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = ( ( 𝐴 · ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
199 198 eqeq1d ⊢ ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ↔ ( ( 𝐴 · ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) = 𝐶 ) )
200 195 199 anbi12d ⊢ ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ↔ ( ( ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) + ( ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) = 𝐶 ) ) )
201 191 200 syl5ibrcom ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) )
202 35 21 subcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ∈ ℂ )
203 202 26 32 sqdivd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) = ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ↑ 2 ) / ( 𝑄 ↑ 2 ) ) )
204 binom2sub ⊢ ( ( ( 𝐴 · 𝐶 ) ∈ ℂ ∧ ( 𝐵 · ( √ ‘ 𝐷 ) ) ∈ ℂ ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ↑ 2 ) = ( ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 · ( √ ‘ 𝐷 ) ) ↑ 2 ) ) )
205 35 21 204 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ↑ 2 ) = ( ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 · ( √ ‘ 𝐷 ) ) ↑ 2 ) ) )
206 39 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) )
207 206 46 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 · ( √ ‘ 𝐷 ) ) ↑ 2 ) ) = ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) )
208 205 207 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ↑ 2 ) = ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) )
209 208 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ↑ 2 ) / ( 𝑄 ↑ 2 ) ) = ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) )
210 203 209 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) = ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) )
211 51 56 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ∈ ℂ )
212 211 26 32 sqdivd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) = ( ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ↑ 2 ) / ( 𝑄 ↑ 2 ) ) )
213 binom2 ⊢ ( ( ( 𝐵 · 𝐶 ) ∈ ℂ ∧ ( 𝐴 · ( √ ‘ 𝐷 ) ) ∈ ℂ ) → ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ↑ 2 ) = ( ( ( ( 𝐵 · 𝐶 ) ↑ 2 ) + ( 2 · ( ( 𝐵 · 𝐶 ) · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 · ( √ ‘ 𝐷 ) ) ↑ 2 ) ) )
214 51 56 213 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ↑ 2 ) = ( ( ( ( 𝐵 · 𝐶 ) ↑ 2 ) + ( 2 · ( ( 𝐵 · 𝐶 ) · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 · ( √ ‘ 𝐷 ) ) ↑ 2 ) ) )
215 60 67 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐵 · 𝐶 ) ↑ 2 ) + ( 2 · ( ( 𝐵 · 𝐶 ) · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) = ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) )
216 215 71 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐵 · 𝐶 ) ↑ 2 ) + ( 2 · ( ( 𝐵 · 𝐶 ) · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 · ( √ ‘ 𝐷 ) ) ↑ 2 ) ) = ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) )
217 214 216 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ↑ 2 ) = ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) )
218 217 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ↑ 2 ) / ( 𝑄 ↑ 2 ) ) = ( ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) )
219 212 218 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) = ( ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) )
220 210 219 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) + ( ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) ) = ( ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) + ( ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) ) )
221 98 78 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ∈ ℂ )
222 35 21 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ∈ ℂ )
223 80 222 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ∈ ℂ )
224 221 223 subcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) ∈ ℂ )
225 224 85 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) ∈ ℂ )
226 87 223 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) ∈ ℂ )
227 98 19 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 ↑ 2 ) · 𝐷 ) ∈ ℂ )
228 226 227 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ∈ ℂ )
229 225 228 91 94 divdird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) + ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) / ( 𝑄 ↑ 2 ) ) = ( ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) + ( ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) ) )
230 224 85 226 227 add4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) + ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) = ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) ) + ( ( ( 𝐵 ↑ 2 ) · 𝐷 ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) )
231 221 223 87 nppcan3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
232 231 99 102 3eqtr2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) ) = ( 𝑄 · ( 𝐶 ↑ 2 ) ) )
233 232 108 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) ) + ( ( ( 𝐵 ↑ 2 ) · 𝐷 ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) = ( ( 𝑄 · ( 𝐶 ↑ 2 ) ) + ( 𝑄 · 𝐷 ) ) )
234 230 233 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) + ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) = ( ( 𝑄 · ( 𝐶 ↑ 2 ) ) + ( 𝑄 · 𝐷 ) ) )
235 234 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐵 ↑ 2 ) · 𝐷 ) ) + ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) / ( 𝑄 ↑ 2 ) ) = ( ( ( 𝑄 · ( 𝐶 ↑ 2 ) ) + ( 𝑄 · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) )
236 220 229 235 3eqtr2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) + ( ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) ) = ( ( ( 𝑄 · ( 𝐶 ↑ 2 ) ) + ( 𝑄 · 𝐷 ) ) / ( 𝑄 ↑ 2 ) ) )
237 236 130 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) + ( ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) )
238 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
239 simp3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
240 238 239 remulcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 𝐶 ) ∈ ℝ )
241 240 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
242 241 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
243 242 21 subcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ∈ ℂ )
244 5 243 26 32 divassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) = ( 𝐴 · ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
245 5 242 21 subdid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) = ( ( 𝐴 · ( 𝐴 · 𝐶 ) ) − ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) )
246 143 145 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · ( 𝐴 · 𝐶 ) ) − ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) )
247 245 246 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) )
248 247 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) = ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
249 244 248 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) = ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
250 51 52 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ∈ ℂ )
251 12 250 26 32 divassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) = ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
252 12 51 52 adddid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) = ( ( 𝐵 · ( 𝐵 · 𝐶 ) ) + ( 𝐵 · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) )
253 163 168 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · ( 𝐵 · 𝐶 ) ) + ( 𝐵 · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) = ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) )
254 252 253 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) = ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) )
255 254 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) = ( ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
256 251 255 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) = ( ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
257 249 256 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) = ( ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) + ( ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
258 174 176 subcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) ∈ ℂ )
259 178 176 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) ∈ ℂ )
260 258 259 26 32 divdird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) = ( ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) + ( ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
261 174 176 178 nppcan3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) )
262 261 182 185 3eqtr2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) ) = ( 𝑄 · 𝐶 ) )
263 258 259 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) ) ∈ ℂ )
264 263 8 26 32 divmul2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) = 𝐶 ↔ ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) ) = ( 𝑄 · 𝐶 ) ) )
265 262 264 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) − ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 · 𝐵 ) · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) = 𝐶 )
266 257 260 265 3eqtr2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) = 𝐶 )
267 237 266 jca ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) + ( ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) = 𝐶 ) )
268 oveq1 ⊢ ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → ( 𝑋 ↑ 2 ) = ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) )
269 oveq1 ⊢ ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → ( 𝑌 ↑ 2 ) = ( ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) )
270 268 269 oveqan12d ⊢ ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) + ( ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) ) )
271 270 eqeq1d ⊢ ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ↔ ( ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) + ( ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
272 oveq2 ⊢ ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → ( 𝐴 · 𝑋 ) = ( 𝐴 · ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
273 oveq2 ⊢ ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → ( 𝐵 · 𝑌 ) = ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
274 272 273 oveqan12d ⊢ ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = ( ( 𝐴 · ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
275 274 eqeq1d ⊢ ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ↔ ( ( 𝐴 · ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) = 𝐶 ) )
276 271 275 anbi12d ⊢ ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ↔ ( ( ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) + ( ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) = 𝐶 ) ) )
277 267 276 syl5ibrcom ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) )
278 201 277 jaod ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) → ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) )