Theorem itscnhlc0xyqsol 49378

Description: Lemma for itsclc0 49384. 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 486	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℝ)
2	1	3anim1i 1166	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ))
3		simpr 488	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 𝐴 ≠ 0)
4	3	3ad2ant1 1147	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ≠ 0)
5	4	orcd 884	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0))
6	2, 5	jca 519	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)))
7	6	3anim1i 1166	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)))
8		itscnhlc0yqe.q	. . . . . 6 ⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))
9		itsclc0yqsol.d	. . . . . 6 ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2))
10	8, 9	itsclc0yqsol 49377	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∨ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))
11	7, 10	syl 17	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∨ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))
12	11	imp 410	. . 3 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∨ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
13		oveq2 7404	. . . . . . . . . . . . 13 ⊢ (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → (𝐵 · 𝑌) = (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)))
14	13	oveq2d 7412	. . . . . . . . . . . 12 ⊢ (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = ((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))))
15	14	eqeq1d 2765	. . . . . . . . . . 11 ⊢ (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 ↔ ((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶))
16		simp12 1219	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐵 ∈ ℝ)
17	16	recnd 11221	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐵 ∈ ℂ)
18		simp13 1220	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 ∈ ℝ)
19	18	recnd 11221	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 ∈ ℂ)
20	17, 19	mulcld 11213	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · 𝐶) ∈ ℂ)
21		simp11l 1299	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ∈ ℝ)
22	21	recnd 11221	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ∈ ℂ)
23		rpre 13012	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ)
24	23	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) → 𝑅 ∈ ℝ)
25	24	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝑅 ∈ ℝ)
26	25	resqcld 14148	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑅↑2) ∈ ℝ)
27		simp1l 1212	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ)
28		simp2 1151	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℝ)
29	8	resum2sqcl 49319	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈ ℝ)
30	27, 28, 29	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝑄 ∈ ℝ)
31	30	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝑄 ∈ ℝ)
32	26, 31	remulcld 11223	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝑅↑2) · 𝑄) ∈ ℝ)
33		simpl3 1208	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐶 ∈ ℝ)
34	33	resqcld 14148	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐶↑2) ∈ ℝ)
35	32, 34	resubcld 11626	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝑅↑2) · 𝑄) − (𝐶↑2)) ∈ ℝ)
36	9, 35	eqeltrid 2867	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐷 ∈ ℝ)
37	36	3adant3 1146	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐷 ∈ ℝ)
38	37	recnd 11221	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐷 ∈ ℂ)
39	38	sqrtcld 15477	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (√‘𝐷) ∈ ℂ)
40	22, 39	mulcld 11213	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴 · (√‘𝐷)) ∈ ℂ)
41	20, 40	subcld 11553	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ∈ ℂ)
42	30	3ad2ant1 1147	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑄 ∈ ℝ)
43	42	recnd 11221	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑄 ∈ ℂ)
44	8	resum2sqgt0 49320	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → 0 < 𝑄)
45	44	3adant3 1146	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 0 < 𝑄)
46	45	gt0ne0d 11762	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝑄 ≠ 0)
47	46	3ad2ant1 1147	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑄 ≠ 0)
48	17, 41, 43, 47	divassd 12013	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄) = (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)))
49	48	eqcomd 2769	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) = ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄))
50	49	oveq2d 7412	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = ((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)))
51	19, 43, 47	divcan3d 11983	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑄 · 𝐶) / 𝑄) = 𝐶)
52	51	eqcomd 2769	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 = ((𝑄 · 𝐶) / 𝑄))
53	50, 52	eqeq12d 2779	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶 ↔ ((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)) = ((𝑄 · 𝐶) / 𝑄)))
54	43, 19	mulcld 11213	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑄 · 𝐶) ∈ ℂ)
55	17, 41	mulcld 11213	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) ∈ ℂ)
56	54, 55, 43, 47	divsubdird 12017	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) = (((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)))
57	56	eqcomd 2769	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)) = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄))
58	57	eqeq1d 2765	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)) = (𝐴 · 𝑋) ↔ (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) = (𝐴 · 𝑋)))
59	54, 43, 47	divcld 11978	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑄 · 𝐶) / 𝑄) ∈ ℂ)
60	55, 43, 47	divcld 11978	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄) ∈ ℂ)
61		simp3l 1216	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑋 ∈ ℝ)
62	61	recnd 11221	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑋 ∈ ℂ)
63	22, 62	mulcld 11213	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴 · 𝑋) ∈ ℂ)
64	59, 60, 63	subadd2d 11572	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)) = (𝐴 · 𝑋) ↔ ((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)) = ((𝑄 · 𝐶) / 𝑄)))
65		eqcom 2770	. . . . . . . . . . . . . . 15 ⊢ (((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = 𝑋 ↔ 𝑋 = ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴))
66	65	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = 𝑋 ↔ 𝑋 = ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴)))
67	54, 55	subcld 11553	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) ∈ ℂ)
68	67, 43, 47	divcld 11978	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) ∈ ℂ)
69		simp11r 1300	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ≠ 0)
70	68, 62, 22, 69	divmul2d 12011	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = 𝑋 ↔ (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) = (𝐴 · 𝑋)))
71	67, 43, 22, 47, 69	divdiv1d 12009	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)))
72	71	eqeq2d 2774	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑋 = ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
73	66, 70, 72	3bitr3d 311	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / 𝑄) = (𝐴 · 𝑋) ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
74	58, 64, 73	3bitr3d 311	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄)) = ((𝑄 · 𝐶) / 𝑄) ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
75	53, 74	bitrd 281	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶 ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
76	15, 75	sylan9bbr 518	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
77	8	oveq1i 7406	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 · 𝐶) = (((𝐴↑2) + (𝐵↑2)) · 𝐶)
78	27	recnd 11221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
79	78	sqcld 14167	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) ∈ ℂ)
80	28	recnd 11221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
81	80	sqcld 14167	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵↑2) ∈ ℂ)
82		simp3 1152	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
83	82	recnd 11221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
84	79, 81, 83	adddird 11218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (((𝐴↑2) + (𝐵↑2)) · 𝐶) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
85	77, 84	eqtrid 2810	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑄 · 𝐶) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
86	85	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑄 · 𝐶) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
87	80	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐵 ∈ ℂ)
88	33	recnd 11221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐶 ∈ ℂ)
89	87, 88	mulcld 11213	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · 𝐶) ∈ ℂ)
90	78	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐴 ∈ ℂ)
91	36	recnd 11221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐷 ∈ ℂ)
92	91	sqrtcld 15477	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (√‘𝐷) ∈ ℂ)
93	90, 92	mulcld 11213	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐴 · (√‘𝐷)) ∈ ℂ)
94	87, 89, 93	subdid 11654	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) = ((𝐵 · (𝐵 · 𝐶)) − (𝐵 · (𝐴 · (√‘𝐷)))))
95	80, 80, 83	mulassd 11216	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 · 𝐵) · 𝐶) = (𝐵 · (𝐵 · 𝐶)))
96		recn 11174	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
97	96	sqvald 14166	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐵 ∈ ℝ → (𝐵↑2) = (𝐵 · 𝐵))
98	97	3ad2ant2 1148	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵↑2) = (𝐵 · 𝐵))
99	98	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · 𝐵) = (𝐵↑2))
100	99	oveq1d 7411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 · 𝐵) · 𝐶) = ((𝐵↑2) · 𝐶))
101	95, 100	eqtr3d 2800	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · (𝐵 · 𝐶)) = ((𝐵↑2) · 𝐶))
102	101	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · (𝐵 · 𝐶)) = ((𝐵↑2) · 𝐶))
103	87, 90, 92	mul12d 11403	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · (𝐴 · (√‘𝐷))) = (𝐴 · (𝐵 · (√‘𝐷))))
104	102, 103	oveq12d 7414	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐵 · (𝐵 · 𝐶)) − (𝐵 · (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))))
105	94, 104	eqtrd 2798	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))))
106	86, 105	oveq12d 7414	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) = ((((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷))))))
107	90	sqcld 14167	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐴↑2) ∈ ℂ)
108	107, 88	mulcld 11213	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · 𝐶) ∈ ℂ)
109	87	sqcld 14167	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵↑2) ∈ ℂ)
110	109, 88	mulcld 11213	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) · 𝐶) ∈ ℂ)
111	108, 110	addcomd 11396	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)) = (((𝐵↑2) · 𝐶) + ((𝐴↑2) · 𝐶)))
112	111	oveq1d 7411	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷))))) = ((((𝐵↑2) · 𝐶) + ((𝐴↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷))))))
113	87, 92	mulcld 11213	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · (√‘𝐷)) ∈ ℂ)
114	90, 113	mulcld 11213	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐴 · (𝐵 · (√‘𝐷))) ∈ ℂ)
115	110, 108, 114	pnncand 11592	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((((𝐵↑2) · 𝐶) + ((𝐴↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷))))) = (((𝐴↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))))
116	106, 112, 115	3eqtrd 2802	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) = (((𝐴↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))))
117	116	oveq1d 7411	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) = ((((𝐴↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))) / (𝑄 · 𝐴)))
118	78	sqvald 14166	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) = (𝐴 · 𝐴))
119	118	oveq1d 7411	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴↑2) · 𝐶) = ((𝐴 · 𝐴) · 𝐶))
120	78, 78, 83	mulassd 11216	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐴) · 𝐶) = (𝐴 · (𝐴 · 𝐶)))
121	119, 120	eqtrd 2798	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴↑2) · 𝐶) = (𝐴 · (𝐴 · 𝐶)))
122	121	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · 𝐶) = (𝐴 · (𝐴 · 𝐶)))
123	122	oveq1d 7411	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))) = ((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))))
124	31	recnd 11221	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝑄 ∈ ℂ)
125	124, 90	mulcomd 11214	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑄 · 𝐴) = (𝐴 · 𝑄))
126	123, 125	oveq12d 7414	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))) / (𝑄 · 𝐴)) = (((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)))
127	90, 88	mulcld 11213	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐴 · 𝐶) ∈ ℂ)
128	90, 127, 113	adddid 11217	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) = ((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))))
129	128	eqcomd 2769	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))) = (𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))))
130	129	oveq1d 7411	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)) = ((𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)))
131	127, 113	addcld 11212	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) ∈ ℂ)
132	46	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝑄 ≠ 0)
133		simpl1r 1240	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → 𝐴 ≠ 0)
134	131, 124, 90, 132, 133	divcan5d 12004	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄))
135	130, 134	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄))
136	117, 126, 135	3eqtrd 2802	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄))
137	136	eqeq2d 2774	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) ↔ 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
138	137	biimpd 231	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
139	138	3adant3 1146	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
140	139	adantr 484	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
141	76, 140	sylbid 242	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
142	141	ex 416	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄))))
143	142	com23 86	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄))))
144	143	adantld 494	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄))))
145	144	imp 410	. . . . 5 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → 𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
146	145	ancrd 559	. . . 4 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → (𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))))
147		oveq2 7404	. . . . . . . . . . . . 13 ⊢ (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → (𝐵 · 𝑌) = (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
148	147	oveq2d 7412	. . . . . . . . . . . 12 ⊢ (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = ((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))
149	148	eqeq1d 2765	. . . . . . . . . . 11 ⊢ (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 ↔ ((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶))
150	20, 40	addcld 11212	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℂ)
151	17, 150, 43, 47	divassd 12013	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄) = (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
152	151	eqcomd 2769	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) = ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄))
153	152	oveq2d 7412	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = ((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)))
154	153, 52	eqeq12d 2779	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶 ↔ ((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)) = ((𝑄 · 𝐶) / 𝑄)))
155	17, 150	mulcld 11213	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) ∈ ℂ)
156	54, 155, 43, 47	divsubdird 12017	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) = (((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)))
157	156	eqcomd 2769	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)) = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄))
158	157	eqeq1d 2765	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)) = (𝐴 · 𝑋) ↔ (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) = (𝐴 · 𝑋)))
159	155, 43, 47	divcld 11978	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄) ∈ ℂ)
160	59, 159, 63	subadd2d 11572	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) / 𝑄) − ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)) = (𝐴 · 𝑋) ↔ ((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)) = ((𝑄 · 𝐶) / 𝑄)))
161		eqcom 2770	. . . . . . . . . . . . . . 15 ⊢ (((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = 𝑋 ↔ 𝑋 = ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴))
162	161	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = 𝑋 ↔ 𝑋 = ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴)))
163	54, 155	subcld 11553	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) ∈ ℂ)
164	163, 43, 47	divcld 11978	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) ∈ ℂ)
165	164, 62, 22, 69	divmul2d 12011	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = 𝑋 ↔ (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) = (𝐴 · 𝑋)))
166	163, 43, 22, 47, 69	divdiv1d 12009	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)))
167	166	eqeq2d 2774	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑋 = ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) / 𝐴) ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
168	162, 165, 167	3bitr3d 311	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / 𝑄) = (𝐴 · 𝑋) ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
169	158, 160, 168	3bitr3d 311	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄)) = ((𝑄 · 𝐶) / 𝑄) ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
170	154, 169	bitrd 281	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶 ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
171	149, 170	sylan9bbr 518	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 ↔ 𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴))))
172	87, 89, 93	adddid 11217	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) = ((𝐵 · (𝐵 · 𝐶)) + (𝐵 · (𝐴 · (√‘𝐷)))))
173	102, 103	oveq12d 7414	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐵 · (𝐵 · 𝐶)) + (𝐵 · (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))))
174	172, 173	eqtrd 2798	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷)))))
175	86, 174	oveq12d 7414	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) = ((((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷))))))
176	111	oveq1d 7411	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷))))) = ((((𝐵↑2) · 𝐶) + ((𝐴↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷))))))
177	110, 108, 114	pnpcand 11590	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((((𝐵↑2) · 𝐶) + ((𝐴↑2) · 𝐶)) − (((𝐵↑2) · 𝐶) + (𝐴 · (𝐵 · (√‘𝐷))))) = (((𝐴↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))))
178	175, 176, 177	3eqtrd 2802	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) = (((𝐴↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))))
179	178	oveq1d 7411	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) = ((((𝐴↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))) / (𝑄 · 𝐴)))
180	122	oveq1d 7411	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))) = ((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))))
181	180, 125	oveq12d 7414	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) − (𝐴 · (𝐵 · (√‘𝐷)))) / (𝑄 · 𝐴)) = (((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)))
182	90, 127, 113	subdid 11654	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) = ((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))))
183	182	eqcomd 2769	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))) = (𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))))
184	183	oveq1d 7411	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)) = ((𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)))
185	127, 113	subcld 11553	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ∈ ℂ)
186	185, 124, 90, 132, 133	divcan5d 12004	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))
187	184, 186	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))) / (𝐴 · 𝑄)) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))
188	179, 181, 187	3eqtrd 2802	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))
189	188	eqeq2d 2774	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) ↔ 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
190	189	biimpd 231	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
191	190	3adant3 1146	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
192	191	adantr 484	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → (𝑋 = (((𝑄 · 𝐶) − (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))))) / (𝑄 · 𝐴)) → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
193	171, 192	sylbid 242	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
194	193	ex 416	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))))
195	194	com23 86	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 → (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))))
196	195	adantld 494	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄))))
197	196	imp 410	. . . . 5 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → 𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
198	197	ancrd 559	. . . 4 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))
199	146, 198	orim12d 977	. . 3 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → ((𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∨ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))))
200	12, 199	mpd 15	. 2 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) ∧ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)) → ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))
201	200	ex 416	1 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858   ∧ w3a 1099   = wceq 1561   ∈ wcel 2143   ≠ wne 2958   class class class wbr 5101  ‘cfv 6521  (class class class)co 7396  ℂcc 11082  ℝcr 11083  0cc0 11084   + caddc 11087   · cmul 11089   < clt 11227   ≤ cle 11228   − cmin 11425   / cdiv 11855  2c2 12282  ℝ⁺crp 13003  ↑cexp 14084  √csqrt 15270

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7718  ax-cnex 11140  ax-resscn 11141  ax-1cn 11142  ax-icn 11143  ax-addcl 11144  ax-addrcl 11145  ax-mulcl 11146  ax-mulrcl 11147  ax-mulcom 11148  ax-addass 11149  ax-mulass 11150  ax-distr 11151  ax-i2m1 11152  ax-1ne0 11153  ax-1rid 11154  ax-rnegex 11155  ax-rrecex 11156  ax-cnre 11157  ax-pre-lttri 11158  ax-pre-lttrn 11159  ax-pre-ltadd 11160  ax-pre-mulgt0 11161  ax-pre-sup 11162

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5102  df-opab 5164  df-mpt 5183  df-tr 5209  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-sup 9386  df-pnf 11229  df-mnf 11230  df-xr 11231  df-ltxr 11232  df-le 11233  df-sub 11427  df-neg 11428  df-div 11856  df-nn 12221  df-2 12290  df-3 12291  df-4 12292  df-n0 12492  df-z 12579  df-uz 12850  df-rp 13004  df-seq 14025  df-exp 14085  df-cj 15136  df-re 15137  df-im 15138  df-sqrt 15272  df-abs 15273

This theorem is referenced by:  itsclc0xyqsol  49381