itsclc0xyqsolr - Mathbox for Alexander van der Vekens

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

Theorem itsclc0xyqsolr 46845

Description: Lemma for itsclc0 46847. 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 11141	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2	1	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
3	2	3ad2ant1 1133	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐴 ∈ ℂ)
4		recn 11141	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ ℂ)
5	4	3ad2ant3 1135	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
6	5	3ad2ant1 1133	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐶 ∈ ℂ)
7	3, 6	mulcld 11175	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · 𝐶) ∈ ℂ)
8		recn 11141	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
9	8	3ad2ant2 1134	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
10	9	3ad2ant1 1133	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐵 ∈ ℂ)
11		rpre 12923	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ)
12	11	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷) → 𝑅 ∈ ℝ)
13	12	anim2i 617	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ))
14	13	3adant2 1131	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ))
15		itsclc0xyqsolr.q	. . . . . . . . . . . . . 14 ⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))
16		itsclc0xyqsolr.d	. . . . . . . . . . . . . 14 ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2))
17	15, 16	itsclc0lem3 46834	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ) → 𝐷 ∈ ℝ)
18	14, 17	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐷 ∈ ℝ)
19	18	recnd 11183	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐷 ∈ ℂ)
20	19	sqrtcld 15322	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (√‘𝐷) ∈ ℂ)
21	10, 20	mulcld 11175	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · (√‘𝐷)) ∈ ℂ)
22	7, 21	addcld 11174	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) ∈ ℂ)
23	15	resum2sqcl 46782	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈ ℝ)
24	23	3adant3 1132	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝑄 ∈ ℝ)
25	24	recnd 11183	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝑄 ∈ ℂ)
26	25	3ad2ant1 1133	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝑄 ∈ ℂ)
27		simp11 1203	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐴 ∈ ℝ)
28		simp12 1204	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐵 ∈ ℝ)
29		simp2 1137	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0))
30	15	resum2sqorgt0 46785	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) → 0 < 𝑄)
31	27, 28, 29, 30	syl3anc 1371	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 0 < 𝑄)
32	31	gt0ne0d 11719	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝑄 ≠ 0)
33	22, 26, 32	sqdivd 14064	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) = ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))↑2) / (𝑄↑2)))
34	2, 5	mulcld 11175	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐶) ∈ ℂ)
35	34	3ad2ant1 1133	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · 𝐶) ∈ ℂ)
36		binom2 14121	. . . . . . . . . 10 ⊢ (((𝐴 · 𝐶) ∈ ℂ ∧ (𝐵 · (√‘𝐷)) ∈ ℂ) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))↑2) = ((((𝐴 · 𝐶)↑2) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)))
37	35, 21, 36	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))↑2) = ((((𝐴 · 𝐶)↑2) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)))
38	2, 5	sqmuld 14063	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶)↑2) = ((𝐴↑2) · (𝐶↑2)))
39	38	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶)↑2) = ((𝐴↑2) · (𝐶↑2)))
40	39	oveq1d 7372	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶)↑2) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) = (((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))))
41	10, 20	sqmuld 14063	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · (√‘𝐷))↑2) = ((𝐵↑2) · ((√‘𝐷)↑2)))
42		simp3r 1202	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 0 ≤ 𝐷)
43		resqrtth 15140	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ ℝ ∧ 0 ≤ 𝐷) → ((√‘𝐷)↑2) = 𝐷)
44	18, 42, 43	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((√‘𝐷)↑2) = 𝐷)
45	44	oveq2d 7373	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) · ((√‘𝐷)↑2)) = ((𝐵↑2) · 𝐷))
46	41, 45	eqtrd 2776	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · (√‘𝐷))↑2) = ((𝐵↑2) · 𝐷))
47	40, 46	oveq12d 7375	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶)↑2) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)) = ((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)))
48	37, 47	eqtrd 2776	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))↑2) = ((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)))
49	48	oveq1d 7372	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))↑2) / (𝑄↑2)) = (((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)))
50	33, 49	eqtrd 2776	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) = (((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)))
51	10, 6	mulcld 11175	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · 𝐶) ∈ ℂ)
52	3, 20	mulcld 11175	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (√‘𝐷)) ∈ ℂ)
53	51, 52	subcld 11512	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ∈ ℂ)
54	53, 26, 32	sqdivd 14064	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2) = ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))↑2) / (𝑄↑2)))
55	27	recnd 11183	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐴 ∈ ℂ)
56	55, 20	mulcld 11175	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (√‘𝐷)) ∈ ℂ)
57		binom2sub 14123	. . . . . . . . . 10 ⊢ (((𝐵 · 𝐶) ∈ ℂ ∧ (𝐴 · (√‘𝐷)) ∈ ℂ) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))↑2) = ((((𝐵 · 𝐶)↑2) − (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)))
58	51, 56, 57	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))↑2) = ((((𝐵 · 𝐶)↑2) − (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)))
59	9, 5	sqmuld 14063	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 · 𝐶)↑2) = ((𝐵↑2) · (𝐶↑2)))
60	59	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶)↑2) = ((𝐵↑2) · (𝐶↑2)))
61	10, 6, 55, 20	mul4d 11367	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐴) · (𝐶 · (√‘𝐷))))
62	10, 55	mulcomd 11176	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · 𝐴) = (𝐴 · 𝐵))
63	62	oveq1d 7372	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐴) · (𝐶 · (√‘𝐷))) = ((𝐴 · 𝐵) · (𝐶 · (√‘𝐷))))
64	55, 10, 6, 20	mul4d 11367	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐵) · (𝐶 · (√‘𝐷))) = ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))
65	63, 64	eqtrd 2776	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐴) · (𝐶 · (√‘𝐷))) = ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))
66	61, 65	eqtrd 2776	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))) = ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))
67	66	oveq2d 7373	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷)))) = (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))
68	60, 67	oveq12d 7375	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶)↑2) − (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) = (((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))))
69	55, 20	sqmuld 14063	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (√‘𝐷))↑2) = ((𝐴↑2) · ((√‘𝐷)↑2)))
70	44	oveq2d 7373	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · ((√‘𝐷)↑2)) = ((𝐴↑2) · 𝐷))
71	69, 70	eqtrd 2776	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (√‘𝐷))↑2) = ((𝐴↑2) · 𝐷))
72	68, 71	oveq12d 7375	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶)↑2) − (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)) = ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)))
73	58, 72	eqtrd 2776	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))↑2) = ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)))
74	73	oveq1d 7372	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))↑2) / (𝑄↑2)) = (((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2)))
75	54, 74	eqtrd 2776	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2) = (((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2)))
76	50, 75	oveq12d 7375	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = ((((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)) + (((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2))))
77	3	sqcld 14049	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴↑2) ∈ ℂ)
78	6	sqcld 14049	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐶↑2) ∈ ℂ)
79	77, 78	mulcld 11175	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · (𝐶↑2)) ∈ ℂ)
80		2cnd 12231	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 2 ∈ ℂ)
81	7, 21	mulcld 11175	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))) ∈ ℂ)
82	80, 81	mulcld 11175	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))) ∈ ℂ)
83	79, 82	addcld 11174	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) ∈ ℂ)
84	10	sqcld 14049	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵↑2) ∈ ℂ)
85	84, 19	mulcld 11175	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) · 𝐷) ∈ ℂ)
86	83, 85	addcld 11174	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) ∈ ℂ)
87	84, 78	mulcld 11175	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) · (𝐶↑2)) ∈ ℂ)
88	87, 82	subcld 11512	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) ∈ ℂ)
89	77, 19	mulcld 11175	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · 𝐷) ∈ ℂ)
90	88, 89	addcld 11174	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) ∈ ℂ)
91	26	sqcld 14049	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝑄↑2) ∈ ℂ)
92		2z 12535	. . . . . . . 8 ⊢ 2 ∈ ℤ
93	92	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 2 ∈ ℤ)
94	26, 32, 93	expne0d 14057	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝑄↑2) ≠ 0)
95	86, 90, 91, 94	divdird 11969	. . . . 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 11383	. . . . . . . 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 11552	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) = (((𝐴↑2) · (𝐶↑2)) + ((𝐵↑2) · (𝐶↑2))))
98	55	sqcld 14049	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴↑2) ∈ ℂ)
99	98, 84, 78	adddird 11180	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) + (𝐵↑2)) · (𝐶↑2)) = (((𝐴↑2) · (𝐶↑2)) + ((𝐵↑2) · (𝐶↑2))))
100	15	eqcomi 2745	. . . . . . . . . . . 12 ⊢ ((𝐴↑2) + (𝐵↑2)) = 𝑄
101	100	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) + (𝐵↑2)) = 𝑄)
102	101	oveq1d 7372	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) + (𝐵↑2)) · (𝐶↑2)) = (𝑄 · (𝐶↑2)))
103	97, 99, 102	3eqtr2d 2782	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) = (𝑄 · (𝐶↑2)))
104	84, 98, 19	adddird 11180	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) + (𝐴↑2)) · 𝐷) = (((𝐵↑2) · 𝐷) + ((𝐴↑2) · 𝐷)))
105	84, 98	addcomd 11357	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) + (𝐴↑2)) = ((𝐴↑2) + (𝐵↑2)))
106	105, 101	eqtrd 2776	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) + (𝐴↑2)) = 𝑄)
107	106	oveq1d 7372	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) + (𝐴↑2)) · 𝐷) = (𝑄 · 𝐷))
108	104, 107	eqtr3d 2778	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) · 𝐷) + ((𝐴↑2) · 𝐷)) = (𝑄 · 𝐷))
109	103, 108	oveq12d 7375	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) + (((𝐵↑2) · 𝐷) + ((𝐴↑2) · 𝐷))) = ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)))
110	96, 109	eqtrd 2776	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) + ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷))) = ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)))
111	110	oveq1d 7372	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) + ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷))) / (𝑄↑2)) = (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)))
112	26, 78, 19	adddid 11179	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝑄 · ((𝐶↑2) + 𝐷)) = ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)))
113	112	eqcomd 2742	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) = (𝑄 · ((𝐶↑2) + 𝐷)))
114	26	sqvald 14048	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝑄↑2) = (𝑄 · 𝑄))
115	113, 114	oveq12d 7375	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)) = ((𝑄 · ((𝐶↑2) + 𝐷)) / (𝑄 · 𝑄)))
116	78, 19	addcld 11174	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐶↑2) + 𝐷) ∈ ℂ)
117	116, 26, 26, 32, 32	divcan5d 11957	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝑄 · ((𝐶↑2) + 𝐷)) / (𝑄 · 𝑄)) = (((𝐶↑2) + 𝐷) / 𝑄))
118	115, 117	eqtrd 2776	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)) = (((𝐶↑2) + 𝐷) / 𝑄))
119	16	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)))
120	119	oveq2d 7373	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐶↑2) + 𝐷) = ((𝐶↑2) + (((𝑅↑2) · 𝑄) − (𝐶↑2))))
121		rpcn 12925	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℂ)
122	121	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷) → 𝑅 ∈ ℂ)
123	122	3ad2ant3 1135	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝑅 ∈ ℂ)
124	123	sqcld 14049	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝑅↑2) ∈ ℂ)
125	124, 26	mulcld 11175	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝑅↑2) · 𝑄) ∈ ℂ)
126	78, 125	pncan3d 11515	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐶↑2) + (((𝑅↑2) · 𝑄) − (𝐶↑2))) = ((𝑅↑2) · 𝑄))
127	120, 126	eqtrd 2776	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐶↑2) + 𝐷) = ((𝑅↑2) · 𝑄))
128	116, 124, 26, 32	divmul3d 11965	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐶↑2) + 𝐷) / 𝑄) = (𝑅↑2) ↔ ((𝐶↑2) + 𝐷) = ((𝑅↑2) · 𝑄)))
129	127, 128	mpbird 256	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐶↑2) + 𝐷) / 𝑄) = (𝑅↑2))
130	118, 129	eqtrd 2776	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)) = (𝑅↑2))
131	111, 130	eqtrd 2776	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) + ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷))) / (𝑄↑2)) = (𝑅↑2))
132	76, 95, 131	3eqtr2d 2782	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2))
133	3, 22, 26, 32	divassd 11966	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) / 𝑄) = (𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
134	3, 7, 21	adddid 11179	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) = ((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))))
135	1	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
136	4	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
137	135, 135, 136	mulassd 11178	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐴) · 𝐶) = (𝐴 · (𝐴 · 𝐶)))
138	135	sqvald 14048	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) = (𝐴 · 𝐴))
139	138	eqcomd 2742	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐴) = (𝐴↑2))
140	139	oveq1d 7372	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐴) · 𝐶) = ((𝐴↑2) · 𝐶))
141	137, 140	eqtr3d 2778	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐴 · 𝐶)) = ((𝐴↑2) · 𝐶))
142	141	3adant2 1131	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐴 · 𝐶)) = ((𝐴↑2) · 𝐶))
143	142	3ad2ant1 1133	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (𝐴 · 𝐶)) = ((𝐴↑2) · 𝐶))
144	3, 10, 20	mulassd 11178	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐵) · (√‘𝐷)) = (𝐴 · (𝐵 · (√‘𝐷))))
145	144	eqcomd 2742	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (𝐵 · (√‘𝐷))) = ((𝐴 · 𝐵) · (√‘𝐷)))
146	143, 145	oveq12d 7375	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))))
147	134, 146	eqtrd 2776	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))))
148	147	oveq1d 7372	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) / 𝑄) = ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
149	133, 148	eqtr3d 2778	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) = ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
150	10, 53, 26, 32	divassd 11966	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄) = (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)))
151	10, 51, 52	subdid 11611	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) = ((𝐵 · (𝐵 · 𝐶)) − (𝐵 · (𝐴 · (√‘𝐷)))))
152		simpl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℝ)
153	152	recnd 11183	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
154		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
155	154	recnd 11183	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
156	153, 153, 155	mulassd 11178	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 · 𝐵) · 𝐶) = (𝐵 · (𝐵 · 𝐶)))
157	8	sqvald 14048	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ ℝ → (𝐵↑2) = (𝐵 · 𝐵))
158	157	eqcomd 2742	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ ℝ → (𝐵 · 𝐵) = (𝐵↑2))
159	158	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · 𝐵) = (𝐵↑2))
160	159	oveq1d 7372	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 · 𝐵) · 𝐶) = ((𝐵↑2) · 𝐶))
161	156, 160	eqtr3d 2778	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · (𝐵 · 𝐶)) = ((𝐵↑2) · 𝐶))
162	161	3adant1 1130	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · (𝐵 · 𝐶)) = ((𝐵↑2) · 𝐶))
163	162	3ad2ant1 1133	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · (𝐵 · 𝐶)) = ((𝐵↑2) · 𝐶))
164	10, 3, 20	mulassd 11178	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐴) · (√‘𝐷)) = (𝐵 · (𝐴 · (√‘𝐷))))
165	9, 2	mulcomd 11176	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · 𝐴) = (𝐴 · 𝐵))
166	165	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · 𝐴) = (𝐴 · 𝐵))
167	166	oveq1d 7372	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐴) · (√‘𝐷)) = ((𝐴 · 𝐵) · (√‘𝐷)))
168	164, 167	eqtr3d 2778	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · (𝐴 · (√‘𝐷))) = ((𝐴 · 𝐵) · (√‘𝐷)))
169	163, 168	oveq12d 7375	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · (𝐵 · 𝐶)) − (𝐵 · (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))))
170	151, 169	eqtrd 2776	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))))
171	170	oveq1d 7372	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄) = ((((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
172	150, 171	eqtr3d 2778	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) = ((((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
173	149, 172	oveq12d 7375	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = (((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄) + ((((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄)))
174	77, 6	mulcld 11175	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · 𝐶) ∈ ℂ)
175	3, 10	mulcld 11175	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · 𝐵) ∈ ℂ)
176	175, 20	mulcld 11175	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐵) · (√‘𝐷)) ∈ ℂ)
177	174, 176	addcld 11174	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) ∈ ℂ)
178	84, 6	mulcld 11175	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) · 𝐶) ∈ ℂ)
179	178, 176	subcld 11512	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) ∈ ℂ)
180	177, 179, 26, 32	divdird 11969	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = (((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄) + ((((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄)))
181	174, 176, 178	ppncand 11552	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
182	77, 84, 6	adddird 11180	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) + (𝐵↑2)) · 𝐶) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
183	15	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝑄 = ((𝐴↑2) + (𝐵↑2)))
184	183	eqcomd 2742	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) + (𝐵↑2)) = 𝑄)
185	184	oveq1d 7372	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) + (𝐵↑2)) · 𝐶) = (𝑄 · 𝐶))
186	181, 182, 185	3eqtr2d 2782	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) = (𝑄 · 𝐶))
187	177, 179	addcld 11174	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) ∈ ℂ)
188	187, 6, 26, 32	divmul2d 11964	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = 𝐶 ↔ ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) = (𝑄 · 𝐶)))
189	186, 188	mpbird 256	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = 𝐶)
190	173, 180, 189	3eqtr2d 2782	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶)
191	132, 190	jca 512	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2) ∧ ((𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶))
192		oveq1 7364	. . . . . 6 ⊢ (𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) → (𝑋↑2) = ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2))
193		oveq1 7364	. . . . . 6 ⊢ (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → (𝑌↑2) = ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2))
194	192, 193	oveqan12d 7376	. . . . 5 ⊢ ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → ((𝑋↑2) + (𝑌↑2)) = (((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)))
195	194	eqeq1d 2738	. . . 4 ⊢ ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ↔ (((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2)))
196		oveq2 7365	. . . . . 6 ⊢ (𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) → (𝐴 · 𝑋) = (𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
197		oveq2 7365	. . . . . 6 ⊢ (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → (𝐵 · 𝑌) = (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)))
198	196, 197	oveqan12d 7376	. . . . 5 ⊢ ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = ((𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))))
199	198	eqeq1d 2738	. . . 4 ⊢ ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 ↔ ((𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶))
200	195, 199	anbi12d 631	. . 3 ⊢ ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) ↔ ((((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2) ∧ ((𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶)))
201	191, 200	syl5ibrcom 246	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)))
202	35, 21	subcld 11512	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ∈ ℂ)
203	202, 26, 32	sqdivd 14064	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) = ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))↑2) / (𝑄↑2)))
204		binom2sub 14123	. . . . . . . . . . 11 ⊢ (((𝐴 · 𝐶) ∈ ℂ ∧ (𝐵 · (√‘𝐷)) ∈ ℂ) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))↑2) = ((((𝐴 · 𝐶)↑2) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)))
205	35, 21, 204	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))↑2) = ((((𝐴 · 𝐶)↑2) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)))
206	39	oveq1d 7372	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶)↑2) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) = (((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))))
207	206, 46	oveq12d 7375	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶)↑2) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)) = ((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)))
208	205, 207	eqtrd 2776	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))↑2) = ((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)))
209	208	oveq1d 7372	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))↑2) / (𝑄↑2)) = (((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)))
210	203, 209	eqtrd 2776	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) = (((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)))
211	51, 56	addcld 11174	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℂ)
212	211, 26, 32	sqdivd 14064	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2) = ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))↑2) / (𝑄↑2)))
213		binom2 14121	. . . . . . . . . . 11 ⊢ (((𝐵 · 𝐶) ∈ ℂ ∧ (𝐴 · (√‘𝐷)) ∈ ℂ) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))↑2) = ((((𝐵 · 𝐶)↑2) + (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)))
214	51, 56, 213	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))↑2) = ((((𝐵 · 𝐶)↑2) + (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)))
215	60, 67	oveq12d 7375	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶)↑2) + (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) = (((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))))
216	215, 71	oveq12d 7375	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶)↑2) + (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)) = ((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)))
217	214, 216	eqtrd 2776	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))↑2) = ((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)))
218	217	oveq1d 7372	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))↑2) / (𝑄↑2)) = (((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2)))
219	212, 218	eqtrd 2776	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2) = (((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2)))
220	210, 219	oveq12d 7375	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = ((((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)) + (((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2))))
221	98, 78	mulcld 11175	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · (𝐶↑2)) ∈ ℂ)
222	35, 21	mulcld 11175	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))) ∈ ℂ)
223	80, 222	mulcld 11175	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))) ∈ ℂ)
224	221, 223	subcld 11512	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) ∈ ℂ)
225	224, 85	addcld 11174	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) ∈ ℂ)
226	87, 223	addcld 11174	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) ∈ ℂ)
227	98, 19	mulcld 11175	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · 𝐷) ∈ ℂ)
228	226, 227	addcld 11174	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) ∈ ℂ)
229	225, 228, 91, 94	divdird 11969	. . . . . 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 11383	. . . . . . . 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 11539	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) = (((𝐴↑2) · (𝐶↑2)) + ((𝐵↑2) · (𝐶↑2))))
232	231, 99, 102	3eqtr2d 2782	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) = (𝑄 · (𝐶↑2)))
233	232, 108	oveq12d 7375	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) + (((𝐵↑2) · 𝐷) + ((𝐴↑2) · 𝐷))) = ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)))
234	230, 233	eqtrd 2776	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) + ((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷))) = ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)))
235	234	oveq1d 7372	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) + ((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷))) / (𝑄↑2)) = (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)))
236	220, 229, 235	3eqtr2d 2782	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)))
237	236, 130	eqtrd 2776	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2))
238		simp1 1136	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ)
239		simp3 1138	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
240	238, 239	remulcld 11185	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐶) ∈ ℝ)
241	240	recnd 11183	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐶) ∈ ℂ)
242	241	3ad2ant1 1133	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · 𝐶) ∈ ℂ)
243	242, 21	subcld 11512	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ∈ ℂ)
244	3, 243, 26, 32	divassd 11966	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) / 𝑄) = (𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
245	3, 242, 21	subdid 11611	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) = ((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))))
246	143, 145	oveq12d 7375	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))))
247	245, 246	eqtrd 2776	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))))
248	247	oveq1d 7372	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) / 𝑄) = ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
249	244, 248	eqtr3d 2778	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) = ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
250	51, 52	addcld 11174	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℂ)
251	10, 250, 26, 32	divassd 11966	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄) = (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
252	10, 51, 52	adddid 11179	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) = ((𝐵 · (𝐵 · 𝐶)) + (𝐵 · (𝐴 · (√‘𝐷)))))
253	163, 168	oveq12d 7375	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · (𝐵 · 𝐶)) + (𝐵 · (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))))
254	252, 253	eqtrd 2776	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))))
255	254	oveq1d 7372	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄) = ((((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
256	251, 255	eqtr3d 2778	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) = ((((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
257	249, 256	oveq12d 7375	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = (((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄) + ((((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄)))
258	174, 176	subcld 11512	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) ∈ ℂ)
259	178, 176	addcld 11174	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) ∈ ℂ)
260	258, 259, 26, 32	divdird 11969	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = (((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄) + ((((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄)))
261	174, 176, 178	nppcan3d 11539	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
262	261, 182, 185	3eqtr2d 2782	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) = (𝑄 · 𝐶))
263	258, 259	addcld 11174	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) ∈ ℂ)
264	263, 6, 26, 32	divmul2d 11964	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = 𝐶 ↔ ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) = (𝑄 · 𝐶)))
265	262, 264	mpbird 256	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = 𝐶)
266	257, 260, 265	3eqtr2d 2782	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶)
267	237, 266	jca 512	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2) ∧ ((𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶))
268		oveq1 7364	. . . . . 6 ⊢ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) → (𝑋↑2) = ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2))
269		oveq1 7364	. . . . . 6 ⊢ (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → (𝑌↑2) = ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2))
270	268, 269	oveqan12d 7376	. . . . 5 ⊢ ((𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → ((𝑋↑2) + (𝑌↑2)) = (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)))
271	270	eqeq1d 2738	. . . 4 ⊢ ((𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ↔ (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2)))
272		oveq2 7365	. . . . . 6 ⊢ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) → (𝐴 · 𝑋) = (𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
273		oveq2 7365	. . . . . 6 ⊢ (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → (𝐵 · 𝑌) = (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
274	272, 273	oveqan12d 7376	. . . . 5 ⊢ ((𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = ((𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))
275	274	eqeq1d 2738	. . . 4 ⊢ ((𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 ↔ ((𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶))
276	271, 275	anbi12d 631	. . 3 ⊢ ((𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) ↔ ((((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2) ∧ ((𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶)))
277	267, 276	syl5ibrcom 246	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)))
278	201, 277	jaod 857	1 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) → (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∨ wo 845 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ≠ wne 2943 class class class wbr 5105 ‘cfv 6496 (class class class)co 7357 ℂcc 11049 ℝcr 11050 0cc0 11051 + caddc 11054 · cmul 11056 < clt 11189 ≤ cle 11190 − cmin 11385 / cdiv 11812 2c2 12208 ℤcz 12499 ℝ⁺crp 12915 ↑cexp 13967 √csqrt 15118

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128 ax-pre-sup 11129

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7803 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-er 8648 df-en 8884 df-dom 8885 df-sdom 8886 df-sup 9378 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-div 11813 df-nn 12154 df-2 12216 df-3 12217 df-n0 12414 df-z 12500 df-uz 12764 df-rp 12916 df-seq 13907 df-exp 13968 df-cj 14984 df-re 14985 df-im 14986 df-sqrt 15120 df-abs 15121

This theorem is referenced by: itsclc0xyqsolb 46846

W3C validator