Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  itscnhlc0xyqsol Structured version   Visualization version   GIF version

Theorem itscnhlc0xyqsol 46470
Description: Lemma for itsclc0 46476. 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.)
Hypotheses
Ref Expression
itscnhlc0yqe.q 𝑄 = ((𝐴↑2) + (𝐵↑2))
itsclc0yqsol.d 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2))
Assertion
Ref Expression
itscnhlc0xyqsol ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))))

Proof of Theorem itscnhlc0xyqsol
StepHypRef Expression
1 simpl 483 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℝ)
213anim1i 1151 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ))
3 simpr 485 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 𝐴 ≠ 0)
433ad2ant1 1132 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ≠ 0)
54orcd 870 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0))
62, 5jca 512 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)))
763anim1i 1151 . . . . 5 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)))
8 itscnhlc0yqe.q . . . . . 6 𝑄 = ((𝐴↑2) + (𝐵↑2))
9 itsclc0yqsol.d . . . . . 6 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2))
108, 9itsclc0yqsol 46469 . . . . 5 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∨ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))
117, 10syl 17 . . . 4 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∨ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))
1211imp 407 . . 3 (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∨ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
13 oveq2 7345 . . . . . . . . . . . . 13 (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → (𝐵 · 𝑌) = (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)))
1413oveq2d 7353 . . . . . . . . . . . 12 (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = ((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))))
1514eqeq1d 2738 . . . . . . . . . . 11 (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 ↔ ((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶))
16 simp12 1203 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐵 ∈ ℝ)
1716recnd 11104 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐵 ∈ ℂ)
18 simp13 1204 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 ∈ ℝ)
1918recnd 11104 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 ∈ ℂ)
2017, 19mulcld 11096 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · 𝐶) ∈ ℂ)
21 simp11l 1283 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ∈ ℝ)
2221recnd 11104 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ∈ ℂ)
23 rpre 12839 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑅 ∈ ℝ+𝑅 ∈ ℝ)
2423adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) → 𝑅 ∈ ℝ)
2524adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝑅 ∈ ℝ)
2625resqcld 14066 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑅↑2) ∈ ℝ)
27 simp1l 1196 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ)
28 simp2 1136 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℝ)
298resum2sqcl 46411 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈ ℝ)
3027, 28, 29syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝑄 ∈ ℝ)
3130adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝑄 ∈ ℝ)
3226, 31remulcld 11106 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝑅↑2) · 𝑄) ∈ ℝ)
33 simpl3 1192 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐶 ∈ ℝ)
3433resqcld 14066 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐶↑2) ∈ ℝ)
3532, 34resubcld 11504 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝑅↑2) · 𝑄) − (𝐶↑2)) ∈ ℝ)
369, 35eqeltrid 2841 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐷 ∈ ℝ)
37363adant3 1131 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐷 ∈ ℝ)
3837recnd 11104 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐷 ∈ ℂ)
3938sqrtcld 15248 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (√‘𝐷) ∈ ℂ)
4022, 39mulcld 11096 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴 · (√‘𝐷)) ∈ ℂ)
4120, 40subcld 11433 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ∈ ℂ)
42303ad2ant1 1132 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑄 ∈ ℝ)
4342recnd 11104 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑄 ∈ ℂ)
448resum2sqgt0 46412 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → 0 < 𝑄)
45443adant3 1131 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 0 < 𝑄)
4645gt0ne0d 11640 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝑄 ≠ 0)
47463ad2ant1 1132 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑄 ≠ 0)
4817, 41, 43, 47divassd 11887 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄) = (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)))
4948eqcomd 2742 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) = ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄))
5049oveq2d 7353 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = ((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)))
5119, 43, 47divcan3d 11857 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑄 · 𝐶) / 𝑄) = 𝐶)
5251eqcomd 2742 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 = ((𝑄 · 𝐶) / 𝑄))
5350, 52eqeq12d 2752 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶 ↔ ((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)) = ((𝑄 · 𝐶) / 𝑄)))
5443, 19mulcld 11096 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑄 · 𝐶) ∈ ℂ)
5517, 41mulcld 11096 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) ∈ ℂ)
5654, 55, 43, 47divsubdird 11891 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) = (((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)))
5756eqcomd 2742 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)) = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄))
5857eqeq1d 2738 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)) = (𝐴 · 𝑋) ↔ (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) = (𝐴 · 𝑋)))
5954, 43, 47divcld 11852 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑄 · 𝐶) / 𝑄) ∈ ℂ)
6055, 43, 47divcld 11852 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄) ∈ ℂ)
61 simp3l 1200 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑋 ∈ ℝ)
6261recnd 11104 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑋 ∈ ℂ)
6322, 62mulcld 11096 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴 · 𝑋) ∈ ℂ)
6459, 60, 63subadd2d 11452 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)) = (𝐴 · 𝑋) ↔ ((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)) = ((𝑄 · 𝐶) / 𝑄)))
65 eqcom 2743 . . . . . . . . . . . . . . 15 (((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = 𝑋𝑋 = ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴))
6665a1i 11 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = 𝑋𝑋 = ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴)))
6754, 55subcld 11433 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) ∈ ℂ)
6867, 43, 47divcld 11852 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) ∈ ℂ)
69 simp11r 1284 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ≠ 0)
7068, 62, 22, 69divmul2d 11885 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = 𝑋 ↔ (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) = (𝐴 · 𝑋)))
7167, 43, 22, 47, 69divdiv1d 11883 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)))
7271eqeq2d 2747 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑋 = ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
7366, 70, 723bitr3d 308 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) = (𝐴 · 𝑋) ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
7458, 64, 733bitr3d 308 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)) = ((𝑄 · 𝐶) / 𝑄) ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
7553, 74bitrd 278 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
7615, 75sylan9bbr 511 . . . . . . . . . 10 (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
778oveq1i 7347 . . . . . . . . . . . . . . . . . . . 20 (𝑄 · 𝐶) = (((𝐴↑2) + (𝐵↑2)) · 𝐶)
7827recnd 11104 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
7978sqcld 13963 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) ∈ ℂ)
8028recnd 11104 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
8180sqcld 13963 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵↑2) ∈ ℂ)
82 simp3 1137 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
8382recnd 11104 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
8479, 81, 83adddird 11101 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (((𝐴↑2) + (𝐵↑2)) · 𝐶) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
8577, 84eqtrid 2788 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑄 · 𝐶) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
8685adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑄 · 𝐶) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
8780adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐵 ∈ ℂ)
8833recnd 11104 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐶 ∈ ℂ)
8987, 88mulcld 11096 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · 𝐶) ∈ ℂ)
9078adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐴 ∈ ℂ)
9136recnd 11104 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐷 ∈ ℂ)
9291sqrtcld 15248 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (√‘𝐷) ∈ ℂ)
9390, 92mulcld 11096 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐴 · (√‘𝐷)) ∈ ℂ)
9487, 89, 93subdid 11532 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) = ((𝐵 · (𝐵 · 𝐶)) − (𝐵 · (𝐴 · (√‘𝐷)))))
9580, 80, 83mulassd 11099 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 · 𝐵) · 𝐶) = (𝐵 · (𝐵 · 𝐶)))
96 recn 11062 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
9796sqvald 13962 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐵 ∈ ℝ → (𝐵↑2) = (𝐵 · 𝐵))
98973ad2ant2 1133 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵↑2) = (𝐵 · 𝐵))
9998eqcomd 2742 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · 𝐵) = (𝐵↑2))
10099oveq1d 7352 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 · 𝐵) · 𝐶) = ((𝐵↑2) · 𝐶))
10195, 100eqtr3d 2778 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · (𝐵 · 𝐶)) = ((𝐵↑2) · 𝐶))
102101adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · (𝐵 · 𝐶)) = ((𝐵↑2) · 𝐶))
10387, 90, 92mul12d 11285 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · (𝐴 · (√‘𝐷))) = (𝐴 · (𝐵 · (√‘𝐷))))
104102, 103oveq12d 7355 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐵 · (𝐵 · 𝐶)) − (𝐵 · (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))))
10594, 104eqtrd 2776 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))))
10686, 105oveq12d 7355 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) = ((((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷))))))
10790sqcld 13963 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐴↑2) ∈ ℂ)
108107, 88mulcld 11096 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · 𝐶) ∈ ℂ)
10987sqcld 13963 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵↑2) ∈ ℂ)
110109, 88mulcld 11096 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) · 𝐶) ∈ ℂ)
111108, 110addcomd 11278 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)) = (((𝐵↑2) · 𝐶) + ((𝐴↑2) · 𝐶)))
112111oveq1d 7352 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷))))) = ((((𝐵↑2) · 𝐶) + ((𝐴↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷))))))
11387, 92mulcld 11096 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · (√‘𝐷)) ∈ ℂ)
11490, 113mulcld 11096 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐴 · (𝐵 · (√‘𝐷))) ∈ ℂ)
115110, 108, 114pnncand 11472 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((((𝐵↑2) · 𝐶) + ((𝐴↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷))))) = (((𝐴↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))))
116106, 112, 1153eqtrd 2780 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) = (((𝐴↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))))
117116oveq1d 7352 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) = ((((𝐴↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))) / (𝑄 · 𝐴)))
11878sqvald 13962 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) = (𝐴 · 𝐴))
119118oveq1d 7352 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴↑2) · 𝐶) = ((𝐴 · 𝐴) · 𝐶))
12078, 78, 83mulassd 11099 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐴) · 𝐶) = (𝐴 · (𝐴 · 𝐶)))
121119, 120eqtrd 2776 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴↑2) · 𝐶) = (𝐴 · (𝐴 · 𝐶)))
122121adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · 𝐶) = (𝐴 · (𝐴 · 𝐶)))
123122oveq1d 7352 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))) = ((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))))
12431recnd 11104 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝑄 ∈ ℂ)
125124, 90mulcomd 11097 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑄 · 𝐴) = (𝐴 · 𝑄))
126123, 125oveq12d 7355 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))) / (𝑄 · 𝐴)) = (((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)))
12790, 88mulcld 11096 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐴 · 𝐶) ∈ ℂ)
12890, 127, 113adddid 11100 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) = ((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))))
129128eqcomd 2742 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))) = (𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))))
130129oveq1d 7352 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)) = ((𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)))
131127, 113addcld 11095 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) ∈ ℂ)
13246adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝑄 ≠ 0)
133 simpl1r 1224 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐴 ≠ 0)
134131, 124, 90, 132, 133divcan5d 11878 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄))
135130, 134eqtrd 2776 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄))
136117, 126, 1353eqtrd 2780 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄))
137136eqeq2d 2747 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) ↔ 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
138137biimpd 228 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
1391383adant3 1131 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
140139adantr 481 . . . . . . . . . 10 (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
14176, 140sylbid 239 . . . . . . . . 9 (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
142141ex 413 . . . . . . . 8 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄))))
143142com23 86 . . . . . . 7 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄))))
144143adantld 491 . . . . . 6 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄))))
145144imp 407 . . . . 5 (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
146145ancrd 552 . . . 4 (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → (𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))))
147 oveq2 7345 . . . . . . . . . . . . 13 (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → (𝐵 · 𝑌) = (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
148147oveq2d 7353 . . . . . . . . . . . 12 (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = ((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))
149148eqeq1d 2738 . . . . . . . . . . 11 (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 ↔ ((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶))
15020, 40addcld 11095 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℂ)
15117, 150, 43, 47divassd 11887 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄) = (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
152151eqcomd 2742 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) = ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄))
153152oveq2d 7353 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = ((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)))
154153, 52eqeq12d 2752 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶 ↔ ((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)) = ((𝑄 · 𝐶) / 𝑄)))
15517, 150mulcld 11096 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) ∈ ℂ)
15654, 155, 43, 47divsubdird 11891 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) = (((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)))
157156eqcomd 2742 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)) = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄))
158157eqeq1d 2738 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)) = (𝐴 · 𝑋) ↔ (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) = (𝐴 · 𝑋)))
159155, 43, 47divcld 11852 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄) ∈ ℂ)
16059, 159, 63subadd2d 11452 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)) = (𝐴 · 𝑋) ↔ ((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)) = ((𝑄 · 𝐶) / 𝑄)))
161 eqcom 2743 . . . . . . . . . . . . . . 15 (((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = 𝑋𝑋 = ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴))
162161a1i 11 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = 𝑋𝑋 = ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴)))
16354, 155subcld 11433 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) ∈ ℂ)
164163, 43, 47divcld 11852 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) ∈ ℂ)
165164, 62, 22, 69divmul2d 11885 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = 𝑋 ↔ (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) = (𝐴 · 𝑋)))
166163, 43, 22, 47, 69divdiv1d 11883 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)))
167166eqeq2d 2747 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑋 = ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
168162, 165, 1673bitr3d 308 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) = (𝐴 · 𝑋) ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
169158, 160, 1683bitr3d 308 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)) = ((𝑄 · 𝐶) / 𝑄) ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
170154, 169bitrd 278 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
171149, 170sylan9bbr 511 . . . . . . . . . 10 (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
17287, 89, 93adddid 11100 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) = ((𝐵 · (𝐵 · 𝐶)) + (𝐵 · (𝐴 · (√‘𝐷)))))
173102, 103oveq12d 7355 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐵 · (𝐵 · 𝐶)) + (𝐵 · (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))))
174172, 173eqtrd 2776 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))))
17586, 174oveq12d 7355 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) = ((((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷))))))
176111oveq1d 7352 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷))))) = ((((𝐵↑2) · 𝐶) + ((𝐴↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷))))))
177110, 108, 114pnpcand 11470 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((((𝐵↑2) · 𝐶) + ((𝐴↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷))))) = (((𝐴↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))))
178175, 176, 1773eqtrd 2780 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) = (((𝐴↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))))
179178oveq1d 7352 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) = ((((𝐴↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))) / (𝑄 · 𝐴)))
180122oveq1d 7352 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))) = ((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))))
181180, 125oveq12d 7355 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))) / (𝑄 · 𝐴)) = (((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)))
18290, 127, 113subdid 11532 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) = ((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))))
183182eqcomd 2742 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))) = (𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))))
184183oveq1d 7352 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)) = ((𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)))
185127, 113subcld 11433 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ∈ ℂ)
186185, 124, 90, 132, 133divcan5d 11878 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))
187184, 186eqtrd 2776 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))
188179, 181, 1873eqtrd 2780 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))
189188eqeq2d 2747 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) ↔ 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
190189biimpd 228 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
1911903adant3 1131 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
192191adantr 481 . . . . . . . . . 10 (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
193171, 192sylbid 239 . . . . . . . . 9 (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
194193ex 413 . . . . . . . 8 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))))
195194com23 86 . . . . . . 7 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 → (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))))
196195adantld 491 . . . . . 6 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))))
197196imp 407 . . . . 5 (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
198197ancrd 552 . . . 4 (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))
199146, 198orim12d 962 . . 3 (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → ((𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∨ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))))
20012, 199mpd 15 . 2 (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))
201200ex 413 1 ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 844  w3a 1086   = wceq 1540  wcel 2105  wne 2940   class class class wbr 5092  cfv 6479  (class class class)co 7337  cc 10970  cr 10971  0cc0 10972   + caddc 10975   · cmul 10977   < clt 11110  cle 11111  cmin 11306   / cdiv 11733  2c2 12129  +crp 12831  cexp 13883  csqrt 15043
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-cnex 11028  ax-resscn 11029  ax-1cn 11030  ax-icn 11031  ax-addcl 11032  ax-addrcl 11033  ax-mulcl 11034  ax-mulrcl 11035  ax-mulcom 11036  ax-addass 11037  ax-mulass 11038  ax-distr 11039  ax-i2m1 11040  ax-1ne0 11041  ax-1rid 11042  ax-rnegex 11043  ax-rrecex 11044  ax-cnre 11045  ax-pre-lttri 11046  ax-pre-lttrn 11047  ax-pre-ltadd 11048  ax-pre-mulgt0 11049  ax-pre-sup 11050
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5176  df-tr 5210  df-id 5518  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5575  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6238  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-riota 7293  df-ov 7340  df-oprab 7341  df-mpo 7342  df-om 7781  df-2nd 7900  df-frecs 8167  df-wrecs 8198  df-recs 8272  df-rdg 8311  df-er 8569  df-en 8805  df-dom 8806  df-sdom 8807  df-sup 9299  df-pnf 11112  df-mnf 11113  df-xr 11114  df-ltxr 11115  df-le 11116  df-sub 11308  df-neg 11309  df-div 11734  df-nn 12075  df-2 12137  df-3 12138  df-4 12139  df-n0 12335  df-z 12421  df-uz 12684  df-rp 12832  df-seq 13823  df-exp 13884  df-cj 14909  df-re 14910  df-im 14911  df-sqrt 15045  df-abs 15046
This theorem is referenced by:  itsclc0xyqsol  46473
  Copyright terms: Public domain W3C validator