Theorem itscnhlc0xyqsol 48776

Description: Lemma for itsclc0 48782. 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

Step	Hyp	Ref	Expression
1		simpl 482	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℝ)
2	1	3anim1i 1152	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ))
3		simpr 484	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 𝐴 ≠ 0)
4	3	3ad2ant1 1133	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ≠ 0)
5	4	orcd 873	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0))
6	2, 5	jca 511	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)))
7	6	3anim1i 1152	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)))
8		itscnhlc0yqe.q	. . . . . 6 ⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))
9		itsclc0yqsol.d	. . . . . 6 ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2))
10	8, 9	itsclc0yqsol 48775	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∨ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))
11	7, 10	syl 17	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∨ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))
12	11	imp 406	. . 3 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∨ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
13		oveq2 7349	. . . . . . . . . . . . 13 ⊢ (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → (𝐵 · 𝑌) = (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)))
14	13	oveq2d 7357	. . . . . . . . . . . 12 ⊢ (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = ((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))))
15	14	eqeq1d 2732	. . . . . . . . . . 11 ⊢ (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 ↔ ((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶))
16		simp12 1205	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐵 ∈ ℝ)
17	16	recnd 11132	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐵 ∈ ℂ)
18		simp13 1206	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 ∈ ℝ)
19	18	recnd 11132	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 ∈ ℂ)
20	17, 19	mulcld 11124	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · 𝐶) ∈ ℂ)
21		simp11l 1285	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ∈ ℝ)
22	21	recnd 11132	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ∈ ℂ)
23		rpre 12891	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ)
24	23	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) → 𝑅 ∈ ℝ)
25	24	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝑅 ∈ ℝ)
26	25	resqcld 14024	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑅↑2) ∈ ℝ)
27		simp1l 1198	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ)
28		simp2 1137	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℝ)
29	8	resum2sqcl 48717	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈ ℝ)
30	27, 28, 29	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝑄 ∈ ℝ)
31	30	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝑄 ∈ ℝ)
32	26, 31	remulcld 11134	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝑅↑2) · 𝑄) ∈ ℝ)
33		simpl3 1194	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐶 ∈ ℝ)
34	33	resqcld 14024	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐶↑2) ∈ ℝ)
35	32, 34	resubcld 11537	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝑅↑2) · 𝑄) − (𝐶↑2)) ∈ ℝ)
36	9, 35	eqeltrid 2833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐷 ∈ ℝ)
37	36	3adant3 1132	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐷 ∈ ℝ)
38	37	recnd 11132	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐷 ∈ ℂ)
39	38	sqrtcld 15339	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (√‘𝐷) ∈ ℂ)
40	22, 39	mulcld 11124	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴 · (√‘𝐷)) ∈ ℂ)
41	20, 40	subcld 11464	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ∈ ℂ)
42	30	3ad2ant1 1133	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑄 ∈ ℝ)
43	42	recnd 11132	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑄 ∈ ℂ)
44	8	resum2sqgt0 48718	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → 0 < 𝑄)
45	44	3adant3 1132	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 0 < 𝑄)
46	45	gt0ne0d 11673	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝑄 ≠ 0)
47	46	3ad2ant1 1133	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑄 ≠ 0)
48	17, 41, 43, 47	divassd 11924	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄) = (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)))
49	48	eqcomd 2736	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) = ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄))
50	49	oveq2d 7357	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = ((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)))
51	19, 43, 47	divcan3d 11894	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑄 · 𝐶) / 𝑄) = 𝐶)
52	51	eqcomd 2736	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 = ((𝑄 · 𝐶) / 𝑄))
53	50, 52	eqeq12d 2746	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶 ↔ ((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)) = ((𝑄 · 𝐶) / 𝑄)))
54	43, 19	mulcld 11124	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑄 · 𝐶) ∈ ℂ)
55	17, 41	mulcld 11124	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) ∈ ℂ)
56	54, 55, 43, 47	divsubdird 11928	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) = (((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)))
57	56	eqcomd 2736	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)) = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄))
58	57	eqeq1d 2732	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)) = (𝐴 · 𝑋) ↔ (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) = (𝐴 · 𝑋)))
59	54, 43, 47	divcld 11889	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑄 · 𝐶) / 𝑄) ∈ ℂ)
60	55, 43, 47	divcld 11889	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄) ∈ ℂ)
61		simp3l 1202	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑋 ∈ ℝ)
62	61	recnd 11132	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑋 ∈ ℂ)
63	22, 62	mulcld 11124	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴 · 𝑋) ∈ ℂ)
64	59, 60, 63	subadd2d 11483	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)) = (𝐴 · 𝑋) ↔ ((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)) = ((𝑄 · 𝐶) / 𝑄)))
65		eqcom 2737	. . . . . . . . . . . . . . 15 ⊢ (((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = 𝑋 ↔ 𝑋 = ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴))
66	65	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = 𝑋 ↔ 𝑋 = ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴)))
67	54, 55	subcld 11464	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) ∈ ℂ)
68	67, 43, 47	divcld 11889	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) ∈ ℂ)
69		simp11r 1286	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ≠ 0)
70	68, 62, 22, 69	divmul2d 11922	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = 𝑋 ↔ (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) = (𝐴 · 𝑋)))
71	67, 43, 22, 47, 69	divdiv1d 11920	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)))
72	71	eqeq2d 2741	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑋 = ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
73	66, 70, 72	3bitr3d 309	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) = (𝐴 · 𝑋) ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
74	58, 64, 73	3bitr3d 309	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)) = ((𝑄 · 𝐶) / 𝑄) ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
75	53, 74	bitrd 279	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶 ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
76	15, 75	sylan9bbr 510	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
77	8	oveq1i 7351	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 · 𝐶) = (((𝐴↑2) + (𝐵↑2)) · 𝐶)
78	27	recnd 11132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
79	78	sqcld 14043	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) ∈ ℂ)
80	28	recnd 11132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
81	80	sqcld 14043	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵↑2) ∈ ℂ)
82		simp3 1138	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
83	82	recnd 11132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
84	79, 81, 83	adddird 11129	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (((𝐴↑2) + (𝐵↑2)) · 𝐶) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
85	77, 84	eqtrid 2777	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑄 · 𝐶) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
86	85	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑄 · 𝐶) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
87	80	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐵 ∈ ℂ)
88	33	recnd 11132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐶 ∈ ℂ)
89	87, 88	mulcld 11124	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · 𝐶) ∈ ℂ)
90	78	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐴 ∈ ℂ)
91	36	recnd 11132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐷 ∈ ℂ)
92	91	sqrtcld 15339	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (√‘𝐷) ∈ ℂ)
93	90, 92	mulcld 11124	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐴 · (√‘𝐷)) ∈ ℂ)
94	87, 89, 93	subdid 11565	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) = ((𝐵 · (𝐵 · 𝐶)) − (𝐵 · (𝐴 · (√‘𝐷)))))
95	80, 80, 83	mulassd 11127	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 · 𝐵) · 𝐶) = (𝐵 · (𝐵 · 𝐶)))
96		recn 11088	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
97	96	sqvald 14042	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐵 ∈ ℝ → (𝐵↑2) = (𝐵 · 𝐵))
98	97	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵↑2) = (𝐵 · 𝐵))
99	98	eqcomd 2736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · 𝐵) = (𝐵↑2))
100	99	oveq1d 7356	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 · 𝐵) · 𝐶) = ((𝐵↑2) · 𝐶))
101	95, 100	eqtr3d 2767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · (𝐵 · 𝐶)) = ((𝐵↑2) · 𝐶))
102	101	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · (𝐵 · 𝐶)) = ((𝐵↑2) · 𝐶))
103	87, 90, 92	mul12d 11314	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · (𝐴 · (√‘𝐷))) = (𝐴 · (𝐵 · (√‘𝐷))))
104	102, 103	oveq12d 7359	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐵 · (𝐵 · 𝐶)) − (𝐵 · (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))))
105	94, 104	eqtrd 2765	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))))
106	86, 105	oveq12d 7359	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) = ((((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷))))))
107	90	sqcld 14043	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐴↑2) ∈ ℂ)
108	107, 88	mulcld 11124	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · 𝐶) ∈ ℂ)
109	87	sqcld 14043	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵↑2) ∈ ℂ)
110	109, 88	mulcld 11124	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) · 𝐶) ∈ ℂ)
111	108, 110	addcomd 11307	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)) = (((𝐵↑2) · 𝐶) + ((𝐴↑2) · 𝐶)))
112	111	oveq1d 7356	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷))))) = ((((𝐵↑2) · 𝐶) + ((𝐴↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷))))))
113	87, 92	mulcld 11124	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · (√‘𝐷)) ∈ ℂ)
114	90, 113	mulcld 11124	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐴 · (𝐵 · (√‘𝐷))) ∈ ℂ)
115	110, 108, 114	pnncand 11503	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((((𝐵↑2) · 𝐶) + ((𝐴↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷))))) = (((𝐴↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))))
116	106, 112, 115	3eqtrd 2769	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) = (((𝐴↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))))
117	116	oveq1d 7356	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) = ((((𝐴↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))) / (𝑄 · 𝐴)))
118	78	sqvald 14042	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) = (𝐴 · 𝐴))
119	118	oveq1d 7356	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴↑2) · 𝐶) = ((𝐴 · 𝐴) · 𝐶))
120	78, 78, 83	mulassd 11127	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐴) · 𝐶) = (𝐴 · (𝐴 · 𝐶)))
121	119, 120	eqtrd 2765	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴↑2) · 𝐶) = (𝐴 · (𝐴 · 𝐶)))
122	121	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · 𝐶) = (𝐴 · (𝐴 · 𝐶)))
123	122	oveq1d 7356	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))) = ((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))))
124	31	recnd 11132	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝑄 ∈ ℂ)
125	124, 90	mulcomd 11125	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑄 · 𝐴) = (𝐴 · 𝑄))
126	123, 125	oveq12d 7359	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))) / (𝑄 · 𝐴)) = (((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)))
127	90, 88	mulcld 11124	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐴 · 𝐶) ∈ ℂ)
128	90, 127, 113	adddid 11128	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) = ((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))))
129	128	eqcomd 2736	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))) = (𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))))
130	129	oveq1d 7356	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)) = ((𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)))
131	127, 113	addcld 11123	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) ∈ ℂ)
132	46	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝑄 ≠ 0)
133		simpl1r 1226	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐴 ≠ 0)
134	131, 124, 90, 132, 133	divcan5d 11915	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄))
135	130, 134	eqtrd 2765	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄))
136	117, 126, 135	3eqtrd 2769	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄))
137	136	eqeq2d 2741	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) ↔ 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
138	137	biimpd 229	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
139	138	3adant3 1132	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
140	139	adantr 480	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
141	76, 140	sylbid 240	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
142	141	ex 412	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄))))
143	142	com23 86	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄))))
144	143	adantld 490	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄))))
145	144	imp 406	. . . . 5 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
146	145	ancrd 551	. . . 4 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → (𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))))
147		oveq2 7349	. . . . . . . . . . . . 13 ⊢ (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → (𝐵 · 𝑌) = (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
148	147	oveq2d 7357	. . . . . . . . . . . 12 ⊢ (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = ((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))
149	148	eqeq1d 2732	. . . . . . . . . . 11 ⊢ (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 ↔ ((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶))
150	20, 40	addcld 11123	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℂ)
151	17, 150, 43, 47	divassd 11924	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄) = (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
152	151	eqcomd 2736	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) = ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄))
153	152	oveq2d 7357	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = ((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)))
154	153, 52	eqeq12d 2746	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶 ↔ ((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)) = ((𝑄 · 𝐶) / 𝑄)))
155	17, 150	mulcld 11124	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) ∈ ℂ)
156	54, 155, 43, 47	divsubdird 11928	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) = (((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)))
157	156	eqcomd 2736	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)) = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄))
158	157	eqeq1d 2732	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)) = (𝐴 · 𝑋) ↔ (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) = (𝐴 · 𝑋)))
159	155, 43, 47	divcld 11889	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄) ∈ ℂ)
160	59, 159, 63	subadd2d 11483	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)) = (𝐴 · 𝑋) ↔ ((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)) = ((𝑄 · 𝐶) / 𝑄)))
161		eqcom 2737	. . . . . . . . . . . . . . 15 ⊢ (((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = 𝑋 ↔ 𝑋 = ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴))
162	161	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = 𝑋 ↔ 𝑋 = ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴)))
163	54, 155	subcld 11464	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) ∈ ℂ)
164	163, 43, 47	divcld 11889	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) ∈ ℂ)
165	164, 62, 22, 69	divmul2d 11922	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = 𝑋 ↔ (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) = (𝐴 · 𝑋)))
166	163, 43, 22, 47, 69	divdiv1d 11920	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)))
167	166	eqeq2d 2741	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑋 = ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
168	162, 165, 167	3bitr3d 309	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) = (𝐴 · 𝑋) ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
169	158, 160, 168	3bitr3d 309	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)) = ((𝑄 · 𝐶) / 𝑄) ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
170	154, 169	bitrd 279	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶 ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
171	149, 170	sylan9bbr 510	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
172	87, 89, 93	adddid 11128	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) = ((𝐵 · (𝐵 · 𝐶)) + (𝐵 · (𝐴 · (√‘𝐷)))))
173	102, 103	oveq12d 7359	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐵 · (𝐵 · 𝐶)) + (𝐵 · (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))))
174	172, 173	eqtrd 2765	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))))
175	86, 174	oveq12d 7359	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) = ((((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷))))))
176	111	oveq1d 7356	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷))))) = ((((𝐵↑2) · 𝐶) + ((𝐴↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷))))))
177	110, 108, 114	pnpcand 11501	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((((𝐵↑2) · 𝐶) + ((𝐴↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷))))) = (((𝐴↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))))
178	175, 176, 177	3eqtrd 2769	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) = (((𝐴↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))))
179	178	oveq1d 7356	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) = ((((𝐴↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))) / (𝑄 · 𝐴)))
180	122	oveq1d 7356	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))) = ((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))))
181	180, 125	oveq12d 7359	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))) / (𝑄 · 𝐴)) = (((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)))
182	90, 127, 113	subdid 11565	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) = ((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))))
183	182	eqcomd 2736	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))) = (𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))))
184	183	oveq1d 7356	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)) = ((𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)))
185	127, 113	subcld 11464	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ∈ ℂ)
186	185, 124, 90, 132, 133	divcan5d 11915	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))
187	184, 186	eqtrd 2765	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))
188	179, 181, 187	3eqtrd 2769	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))
189	188	eqeq2d 2741	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) ↔ 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
190	189	biimpd 229	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
191	190	3adant3 1132	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
192	191	adantr 480	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
193	171, 192	sylbid 240	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
194	193	ex 412	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))))
195	194	com23 86	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 → (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))))
196	195	adantld 490	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))))
197	196	imp 406	. . . . 5 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
198	197	ancrd 551	. . . 4 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))
199	146, 198	orim12d 966	. . 3 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → ((𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∨ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))))
200	12, 199	mpd 15	. 2 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))
201	200	ex 412	1 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1541   ∈ wcel 2110   ≠ wne 2926   class class class wbr 5089  ‘cfv 6477  (class class class)co 7341  ℂcc 10996  ℝcr 10997  0cc0 10998   + caddc 11001   · cmul 11003   < clt 11138   ≤ cle 11139   − cmin 11336   / cdiv 11766  2c2 12172  ℝ⁺crp 12882  ↑cexp 13960  √csqrt 15132

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 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7663  ax-cnex 11054  ax-resscn 11055  ax-1cn 11056  ax-icn 11057  ax-addcl 11058  ax-addrcl 11059  ax-mulcl 11060  ax-mulrcl 11061  ax-mulcom 11062  ax-addass 11063  ax-mulass 11064  ax-distr 11065  ax-i2m1 11066  ax-1ne0 11067  ax-1rid 11068  ax-rnegex 11069  ax-rrecex 11070  ax-cnre 11071  ax-pre-lttri 11072  ax-pre-lttrn 11073  ax-pre-ltadd 11074  ax-pre-mulgt0 11075  ax-pre-sup 11076

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3344  df-reu 3345  df-rab 3394  df-v 3436  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-pss 3920  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6244  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6433  df-fun 6479  df-fn 6480  df-f 6481  df-f1 6482  df-fo 6483  df-f1o 6484  df-fv 6485  df-riota 7298  df-ov 7344  df-oprab 7345  df-mpo 7346  df-om 7792  df-2nd 7917  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-sup 9321  df-pnf 11140  df-mnf 11141  df-xr 11142  df-ltxr 11143  df-le 11144  df-sub 11338  df-neg 11339  df-div 11767  df-nn 12118  df-2 12180  df-3 12181  df-4 12182  df-n0 12374  df-z 12461  df-uz 12725  df-rp 12883  df-seq 13901  df-exp 13961  df-cj 14998  df-re 14999  df-im 15000  df-sqrt 15134  df-abs 15135

This theorem is referenced by:  itsclc0xyqsol  48779