Theorem itsclc0xyqsolr 47765

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

Hypotheses

Ref	Expression
itsclc0xyqsolr.q	⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))
itsclc0xyqsolr.d	⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2))

Assertion

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

Proof of Theorem itsclc0xyqsolr

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 846   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099   ≠ wne 2935   class class class wbr 5142  ‘cfv 6542  (class class class)co 7414  ℂcc 11128  ℝcr 11129  0cc0 11130   + caddc 11133   · cmul 11135   < clt 11270   ≤ cle 11271   − cmin 11466   / cdiv 11893  2c2 12289  ℤcz 12580  ℝ⁺crp 12998  ↑cexp 14050  √csqrt 15204

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-er 8718  df-en 8956  df-dom 8957  df-sdom 8958  df-sup 9457  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-n0 12495  df-z 12581  df-uz 12845  df-rp 12999  df-seq 13991  df-exp 14051  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207

This theorem is referenced by:  itsclc0xyqsolb  47766