Metamath Proof Explorer

Theorem itscnhlc0xyqsol

Description: Lemma for itsclc0 . Solutions of the quadratic equations for the coordinates of the intersection points of a nonhorizontal line and a circle. (Contributed by AV, 8-Feb-2023)

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

Proof

Step Hyp Ref Expression
1 itscnhlc0yqe.q ⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
2 itsclc0yqsol.d ⊢ 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
3 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℝ )
4 3 3anim1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) )
5 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 𝐴 ≠ 0 )
6 5 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ≠ 0 )
7 6 orcd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) )
8 4 7 jca ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) )
9 8 3anim1i ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) )
10 1 2 itsclc0yqsol ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
11 9 10 syl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
12 11 imp ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
13 oveq2 ⊢ ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → ( 𝐵 · 𝑌 ) = ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
14 13 oveq2d ⊢ ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = ( ( 𝐴 · 𝑋 ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
15 14 eqeq1d ⊢ ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ↔ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) = 𝐶 ) )
16 simp12 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐵 ∈ ℝ )
17 16 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐵 ∈ ℂ )
18 simp13 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐶 ∈ ℝ )
19 18 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐶 ∈ ℂ )
20 17 19 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
21 simp11l ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐴 ∈ ℝ )
22 21 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐴 ∈ ℂ )
23 rpre ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ )
24 23 adantr ⊢ ( ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) → 𝑅 ∈ ℝ )
25 24 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝑅 ∈ ℝ )
26 25 resqcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑅 ↑ 2 ) ∈ ℝ )
27 simp1l ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
28 simp2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
29 1 resum2sqcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝑄 ∈ ℝ )
30 27 28 29 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝑄 ∈ ℝ )
31 30 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝑄 ∈ ℝ )
32 26 31 remulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑅 ↑ 2 ) · 𝑄 ) ∈ ℝ )
33 simpl3 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐶 ∈ ℝ )
34 33 resqcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐶 ↑ 2 ) ∈ ℝ )
35 32 34 resubcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) ) ∈ ℝ )
36 2 35 eqeltrid ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐷 ∈ ℝ )
37 36 3adant3 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐷 ∈ ℝ )
38 37 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐷 ∈ ℂ )
39 38 sqrtcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( √ ‘ 𝐷 ) ∈ ℂ )
40 22 39 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐴 · ( √ ‘ 𝐷 ) ) ∈ ℂ )
41 20 40 subcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ∈ ℂ )
42 30 3ad2ant1 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑄 ∈ ℝ )
43 42 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑄 ∈ ℂ )
44 1 resum2sqgt0 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → 0 < 𝑄 )
45 44 3adant3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 0 < 𝑄 )
46 45 gt0ne0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝑄 ≠ 0 )
47 46 3ad2ant1 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑄 ≠ 0 )
48 17 41 43 47 divassd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) = ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
49 48 eqcomd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) = ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) )
50 49 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐴 · 𝑋 ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) = ( ( 𝐴 · 𝑋 ) + ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) ) )
51 19 43 47 divcan3d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝑄 · 𝐶 ) / 𝑄 ) = 𝐶 )
52 51 eqcomd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐶 = ( ( 𝑄 · 𝐶 ) / 𝑄 ) )
53 50 52 eqeq12d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) = 𝐶 ↔ ( ( 𝐴 · 𝑋 ) + ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) ) = ( ( 𝑄 · 𝐶 ) / 𝑄 ) ) )
54 43 19 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑄 · 𝐶 ) ∈ ℂ )
55 17 41 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ∈ ℂ )
56 54 55 43 47 divsubdird ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) = ( ( ( 𝑄 · 𝐶 ) / 𝑄 ) − ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) ) )
57 56 eqcomd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝑄 · 𝐶 ) / 𝑄 ) − ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) ) = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) )
58 57 eqeq1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑄 · 𝐶 ) / 𝑄 ) − ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) ) = ( 𝐴 · 𝑋 ) ↔ ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) = ( 𝐴 · 𝑋 ) ) )
59 54 43 47 divcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝑄 · 𝐶 ) / 𝑄 ) ∈ ℂ )
60 55 43 47 divcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) ∈ ℂ )
61 simp3l ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑋 ∈ ℝ )
62 61 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑋 ∈ ℂ )
63 22 62 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐴 · 𝑋 ) ∈ ℂ )
64 59 60 63 subadd2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑄 · 𝐶 ) / 𝑄 ) − ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) ) = ( 𝐴 · 𝑋 ) ↔ ( ( 𝐴 · 𝑋 ) + ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) ) = ( ( 𝑄 · 𝐶 ) / 𝑄 ) ) )
65 eqcom ⊢ ( ( ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) / 𝐴 ) = 𝑋 ↔ 𝑋 = ( ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) / 𝐴 ) )
66 65 a1i ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) / 𝐴 ) = 𝑋 ↔ 𝑋 = ( ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) / 𝐴 ) ) )
67 54 55 subcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) ∈ ℂ )
68 67 43 47 divcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) ∈ ℂ )
69 simp11r ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐴 ≠ 0 )
70 68 62 22 69 divmul2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) / 𝐴 ) = 𝑋 ↔ ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) = ( 𝐴 · 𝑋 ) ) )
71 67 43 22 47 69 divdiv1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) / 𝐴 ) = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) )
72 71 eqeq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑋 = ( ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) / 𝐴 ) ↔ 𝑋 = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) ) )
73 66 70 72 3bitr3d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) = ( 𝐴 · 𝑋 ) ↔ 𝑋 = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) ) )
74 58 64 73 3bitr3d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝐴 · 𝑋 ) + ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) ) = ( ( 𝑄 · 𝐶 ) / 𝑄 ) ↔ 𝑋 = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) ) )
75 53 74 bitrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) = 𝐶 ↔ 𝑋 = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) ) )
76 15 75 sylan9bbr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ↔ 𝑋 = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) ) )
77 1 oveq1i ⊢ ( 𝑄 · 𝐶 ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · 𝐶 )
78 27 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℂ )
79 78 sqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
80 28 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
81 80 sqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
82 simp3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
83 82 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℂ )
84 79 81 83 adddird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · 𝐶 ) = ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) )
85 77 84 syl5eq ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝑄 · 𝐶 ) = ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) )
86 85 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑄 · 𝐶 ) = ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) )
87 80 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐵 ∈ ℂ )
88 33 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐶 ∈ ℂ )
89 87 88 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
90 78 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐴 ∈ ℂ )
91 36 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐷 ∈ ℂ )
92 91 sqrtcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( √ ‘ 𝐷 ) ∈ ℂ )
93 90 92 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · ( √ ‘ 𝐷 ) ) ∈ ℂ )
94 87 89 93 subdid ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) = ( ( 𝐵 · ( 𝐵 · 𝐶 ) ) − ( 𝐵 · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) )
95 80 80 83 mulassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐵 · 𝐵 ) · 𝐶 ) = ( 𝐵 · ( 𝐵 · 𝐶 ) ) )
96 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
97 96 sqvald ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 ↑ 2 ) = ( 𝐵 · 𝐵 ) )
98 97 3ad2ant2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 ↑ 2 ) = ( 𝐵 · 𝐵 ) )
99 98 eqcomd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 · 𝐵 ) = ( 𝐵 ↑ 2 ) )
100 99 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐵 · 𝐵 ) · 𝐶 ) = ( ( 𝐵 ↑ 2 ) · 𝐶 ) )
101 95 100 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 · ( 𝐵 · 𝐶 ) ) = ( ( 𝐵 ↑ 2 ) · 𝐶 ) )
102 101 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · ( 𝐵 · 𝐶 ) ) = ( ( 𝐵 ↑ 2 ) · 𝐶 ) )
103 87 90 92 mul12d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) = ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) )
104 102 103 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · ( 𝐵 · 𝐶 ) ) − ( 𝐵 · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) = ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) − ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) )
105 94 104 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) = ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) − ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) )
106 86 105 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) − ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) − ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) )
107 90 sqcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
108 107 88 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 ↑ 2 ) · 𝐶 ) ∈ ℂ )
109 87 sqcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
110 109 88 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 ↑ 2 ) · 𝐶 ) ∈ ℂ )
111 108 110 addcomd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) = ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) )
112 111 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) − ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) − ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) = ( ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) − ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) − ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) )
113 87 92 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · ( √ ‘ 𝐷 ) ) ∈ ℂ )
114 90 113 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ∈ ℂ )
115 110 108 114 pnncand ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) − ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) − ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) )
116 106 112 115 3eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) )
117 116 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) = ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) / ( 𝑄 · 𝐴 ) ) )
118 78 sqvald ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
119 118 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 ↑ 2 ) · 𝐶 ) = ( ( 𝐴 · 𝐴 ) · 𝐶 ) )
120 78 78 83 mulassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 · 𝐴 ) · 𝐶 ) = ( 𝐴 · ( 𝐴 · 𝐶 ) ) )
121 119 120 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 ↑ 2 ) · 𝐶 ) = ( 𝐴 · ( 𝐴 · 𝐶 ) ) )
122 121 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 ↑ 2 ) · 𝐶 ) = ( 𝐴 · ( 𝐴 · 𝐶 ) ) )
123 122 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) = ( ( 𝐴 · ( 𝐴 · 𝐶 ) ) + ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) )
124 31 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝑄 ∈ ℂ )
125 124 90 mulcomd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑄 · 𝐴 ) = ( 𝐴 · 𝑄 ) )
126 123 125 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) / ( 𝑄 · 𝐴 ) ) = ( ( ( 𝐴 · ( 𝐴 · 𝐶 ) ) + ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) / ( 𝐴 · 𝑄 ) ) )
127 90 88 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
128 90 127 113 adddid ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) = ( ( 𝐴 · ( 𝐴 · 𝐶 ) ) + ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) )
129 128 eqcomd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · ( 𝐴 · 𝐶 ) ) + ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) = ( 𝐴 · ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) )
130 129 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 · ( 𝐴 · 𝐶 ) ) + ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) / ( 𝐴 · 𝑄 ) ) = ( ( 𝐴 · ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) / ( 𝐴 · 𝑄 ) ) )
131 127 113 addcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ∈ ℂ )
132 46 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝑄 ≠ 0 )
133 simpl1r ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐴 ≠ 0 )
134 131 124 90 132 133 divcan5d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) / ( 𝐴 · 𝑄 ) ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
135 130 134 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 · ( 𝐴 · 𝐶 ) ) + ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) / ( 𝐴 · 𝑄 ) ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
136 117 126 135 3eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
137 136 eqeq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑋 = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) ↔ 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
138 137 biimpd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑋 = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) → 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
139 138 3adant3 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑋 = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) → 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
140 139 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( 𝑋 = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) → 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
141 76 140 sylbid ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 → 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
142 141 ex ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 → 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
143 142 com23 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
144 143 adantld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
145 144 imp ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
146 145 ancrd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
147 oveq2 ⊢ ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → ( 𝐵 · 𝑌 ) = ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
148 147 oveq2d ⊢ ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = ( ( 𝐴 · 𝑋 ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
149 148 eqeq1d ⊢ ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ↔ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) = 𝐶 ) )
150 20 40 addcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ∈ ℂ )
151 17 150 43 47 divassd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) = ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
152 151 eqcomd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) = ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) )
153 152 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐴 · 𝑋 ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) = ( ( 𝐴 · 𝑋 ) + ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) ) )
154 153 52 eqeq12d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) = 𝐶 ↔ ( ( 𝐴 · 𝑋 ) + ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) ) = ( ( 𝑄 · 𝐶 ) / 𝑄 ) ) )
155 17 150 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ∈ ℂ )
156 54 155 43 47 divsubdird ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) = ( ( ( 𝑄 · 𝐶 ) / 𝑄 ) − ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) ) )
157 156 eqcomd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝑄 · 𝐶 ) / 𝑄 ) − ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) ) = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) )
158 157 eqeq1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑄 · 𝐶 ) / 𝑄 ) − ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) ) = ( 𝐴 · 𝑋 ) ↔ ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) = ( 𝐴 · 𝑋 ) ) )
159 155 43 47 divcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) ∈ ℂ )
160 59 159 63 subadd2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑄 · 𝐶 ) / 𝑄 ) − ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) ) = ( 𝐴 · 𝑋 ) ↔ ( ( 𝐴 · 𝑋 ) + ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) ) = ( ( 𝑄 · 𝐶 ) / 𝑄 ) ) )
161 eqcom ⊢ ( ( ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) / 𝐴 ) = 𝑋 ↔ 𝑋 = ( ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) / 𝐴 ) )
162 161 a1i ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) / 𝐴 ) = 𝑋 ↔ 𝑋 = ( ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) / 𝐴 ) ) )
163 54 155 subcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) ∈ ℂ )
164 163 43 47 divcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) ∈ ℂ )
165 164 62 22 69 divmul2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) / 𝐴 ) = 𝑋 ↔ ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) = ( 𝐴 · 𝑋 ) ) )
166 163 43 22 47 69 divdiv1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) / 𝐴 ) = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) )
167 166 eqeq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑋 = ( ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) / 𝐴 ) ↔ 𝑋 = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) ) )
168 162 165 167 3bitr3d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / 𝑄 ) = ( 𝐴 · 𝑋 ) ↔ 𝑋 = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) ) )
169 158 160 168 3bitr3d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝐴 · 𝑋 ) + ( ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) / 𝑄 ) ) = ( ( 𝑄 · 𝐶 ) / 𝑄 ) ↔ 𝑋 = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) ) )
170 154 169 bitrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) = 𝐶 ↔ 𝑋 = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) ) )
171 149 170 sylan9bbr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ↔ 𝑋 = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) ) )
172 87 89 93 adddid ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) = ( ( 𝐵 · ( 𝐵 · 𝐶 ) ) + ( 𝐵 · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) )
173 102 103 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐵 · ( 𝐵 · 𝐶 ) ) + ( 𝐵 · ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) = ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) )
174 172 173 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) = ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) )
175 86 174 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) − ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) )
176 111 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) − ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) = ( ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) − ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) )
177 110 108 114 pnpcand ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) − ( ( ( 𝐵 ↑ 2 ) · 𝐶 ) + ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) − ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) )
178 175 176 177 3eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) − ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) )
179 178 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) = ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) − ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) / ( 𝑄 · 𝐴 ) ) )
180 122 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) − ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) = ( ( 𝐴 · ( 𝐴 · 𝐶 ) ) − ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) )
181 180 125 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) − ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) / ( 𝑄 · 𝐴 ) ) = ( ( ( 𝐴 · ( 𝐴 · 𝐶 ) ) − ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) / ( 𝐴 · 𝑄 ) ) )
182 90 127 113 subdid ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 · ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) = ( ( 𝐴 · ( 𝐴 · 𝐶 ) ) − ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) )
183 182 eqcomd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · ( 𝐴 · 𝐶 ) ) − ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) = ( 𝐴 · ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) )
184 183 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 · ( 𝐴 · 𝐶 ) ) − ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) / ( 𝐴 · 𝑄 ) ) = ( ( 𝐴 · ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) / ( 𝐴 · 𝑄 ) ) )
185 127 113 subcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ∈ ℂ )
186 185 124 90 132 133 divcan5d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝐴 · ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) / ( 𝐴 · 𝑄 ) ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
187 184 186 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 · ( 𝐴 · 𝐶 ) ) − ( 𝐴 · ( 𝐵 · ( √ ‘ 𝐷 ) ) ) ) / ( 𝐴 · 𝑄 ) ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
188 179 181 187 3eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) )
189 188 eqeq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑋 = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) ↔ 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
190 189 biimpd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑋 = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) → 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
191 190 3adant3 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑋 = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) → 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
192 191 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( 𝑋 = ( ( ( 𝑄 · 𝐶 ) − ( 𝐵 · ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) ) ) / ( 𝑄 · 𝐴 ) ) → 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
193 171 192 sylbid ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 → 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
194 193 ex ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 → 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
195 194 com23 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
196 195 adantld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
197 196 imp ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) )
198 197 ancrd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) → ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) → ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
199 146 198 orim12d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) → ( ( 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∨ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) → ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) )
200 12 199 mpd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) → ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) )
201 200 ex ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( 𝑋 = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ 𝑌 = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) )