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 44750

Description: Lemma for itsclc0 44752. 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 10621	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2	1	3ad2ant1 1129	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
3	2	3ad2ant1 1129	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐴 ∈ ℂ)
4		recn 10621	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ ℂ)
5	4	3ad2ant3 1131	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
6	5	3ad2ant1 1129	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐶 ∈ ℂ)
7	3, 6	mulcld 10655	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · 𝐶) ∈ ℂ)
8		recn 10621	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
9	8	3ad2ant2 1130	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
10	9	3ad2ant1 1129	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐵 ∈ ℂ)
11		rpre 12391	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ)
12	11	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷) → 𝑅 ∈ ℝ)
13	12	anim2i 618	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ))
14	13	3adant2 1127	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ))
15		itsclc0xyqsolr.q	. . . . . . . . . . . . . 14 ⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))
16		itsclc0xyqsolr.d	. . . . . . . . . . . . . 14 ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2))
17	15, 16	itsclc0lem3 44739	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ) → 𝐷 ∈ ℝ)
18	14, 17	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐷 ∈ ℝ)
19	18	recnd 10663	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐷 ∈ ℂ)
20	19	sqrtcld 14791	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (√‘𝐷) ∈ ℂ)
21	10, 20	mulcld 10655	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · (√‘𝐷)) ∈ ℂ)
22	7, 21	addcld 10654	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) ∈ ℂ)
23	15	resum2sqcl 44687	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈ ℝ)
24	23	3adant3 1128	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝑄 ∈ ℝ)
25	24	recnd 10663	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝑄 ∈ ℂ)
26	25	3ad2ant1 1129	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝑄 ∈ ℂ)
27		simp11 1199	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐴 ∈ ℝ)
28		simp12 1200	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐵 ∈ ℝ)
29		simp2 1133	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0))
30	15	resum2sqorgt0 44690	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) → 0 < 𝑄)
31	27, 28, 29, 30	syl3anc 1367	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 0 < 𝑄)
32	31	gt0ne0d 11198	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝑄 ≠ 0)
33	22, 26, 32	sqdivd 13517	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) = ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))↑2) / (𝑄↑2)))
34	2, 5	mulcld 10655	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐶) ∈ ℂ)
35	34	3ad2ant1 1129	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · 𝐶) ∈ ℂ)
36		binom2 13573	. . . . . . . . . 10 ⊢ (((𝐴 · 𝐶) ∈ ℂ ∧ (𝐵 · (√‘𝐷)) ∈ ℂ) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))↑2) = ((((𝐴 · 𝐶)↑2) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)))
37	35, 21, 36	syl2anc 586	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))↑2) = ((((𝐴 · 𝐶)↑2) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)))
38	2, 5	sqmuld 13516	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶)↑2) = ((𝐴↑2) · (𝐶↑2)))
39	38	3ad2ant1 1129	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶)↑2) = ((𝐴↑2) · (𝐶↑2)))
40	39	oveq1d 7165	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶)↑2) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) = (((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))))
41	10, 20	sqmuld 13516	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · (√‘𝐷))↑2) = ((𝐵↑2) · ((√‘𝐷)↑2)))
42		simp3r 1198	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 0 ≤ 𝐷)
43		resqrtth 14609	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ ℝ ∧ 0 ≤ 𝐷) → ((√‘𝐷)↑2) = 𝐷)
44	18, 42, 43	syl2anc 586	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((√‘𝐷)↑2) = 𝐷)
45	44	oveq2d 7166	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) · ((√‘𝐷)↑2)) = ((𝐵↑2) · 𝐷))
46	41, 45	eqtrd 2856	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · (√‘𝐷))↑2) = ((𝐵↑2) · 𝐷))
47	40, 46	oveq12d 7168	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶)↑2) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)) = ((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)))
48	37, 47	eqtrd 2856	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))↑2) = ((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)))
49	48	oveq1d 7165	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))↑2) / (𝑄↑2)) = (((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)))
50	33, 49	eqtrd 2856	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) = (((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)))
51	10, 6	mulcld 10655	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · 𝐶) ∈ ℂ)
52	3, 20	mulcld 10655	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (√‘𝐷)) ∈ ℂ)
53	51, 52	subcld 10991	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ∈ ℂ)
54	53, 26, 32	sqdivd 13517	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2) = ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))↑2) / (𝑄↑2)))
55	27	recnd 10663	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐴 ∈ ℂ)
56	55, 20	mulcld 10655	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (√‘𝐷)) ∈ ℂ)
57		binom2sub 13575	. . . . . . . . . 10 ⊢ (((𝐵 · 𝐶) ∈ ℂ ∧ (𝐴 · (√‘𝐷)) ∈ ℂ) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))↑2) = ((((𝐵 · 𝐶)↑2) − (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)))
58	51, 56, 57	syl2anc 586	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))↑2) = ((((𝐵 · 𝐶)↑2) − (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)))
59	9, 5	sqmuld 13516	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 · 𝐶)↑2) = ((𝐵↑2) · (𝐶↑2)))
60	59	3ad2ant1 1129	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶)↑2) = ((𝐵↑2) · (𝐶↑2)))
61	10, 6, 55, 20	mul4d 10846	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐴) · (𝐶 · (√‘𝐷))))
62	10, 55	mulcomd 10656	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · 𝐴) = (𝐴 · 𝐵))
63	62	oveq1d 7165	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐴) · (𝐶 · (√‘𝐷))) = ((𝐴 · 𝐵) · (𝐶 · (√‘𝐷))))
64	55, 10, 6, 20	mul4d 10846	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐵) · (𝐶 · (√‘𝐷))) = ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))
65	63, 64	eqtrd 2856	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐴) · (𝐶 · (√‘𝐷))) = ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))
66	61, 65	eqtrd 2856	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))) = ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))
67	66	oveq2d 7166	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷)))) = (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))
68	60, 67	oveq12d 7168	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶)↑2) − (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) = (((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))))
69	55, 20	sqmuld 13516	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (√‘𝐷))↑2) = ((𝐴↑2) · ((√‘𝐷)↑2)))
70	44	oveq2d 7166	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · ((√‘𝐷)↑2)) = ((𝐴↑2) · 𝐷))
71	69, 70	eqtrd 2856	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (√‘𝐷))↑2) = ((𝐴↑2) · 𝐷))
72	68, 71	oveq12d 7168	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶)↑2) − (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)) = ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)))
73	58, 72	eqtrd 2856	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))↑2) = ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)))
74	73	oveq1d 7165	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))↑2) / (𝑄↑2)) = (((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2)))
75	54, 74	eqtrd 2856	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2) = (((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2)))
76	50, 75	oveq12d 7168	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = ((((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)) + (((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2))))
77	3	sqcld 13502	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴↑2) ∈ ℂ)
78	6	sqcld 13502	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐶↑2) ∈ ℂ)
79	77, 78	mulcld 10655	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · (𝐶↑2)) ∈ ℂ)
80		2cnd 11709	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 2 ∈ ℂ)
81	7, 21	mulcld 10655	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))) ∈ ℂ)
82	80, 81	mulcld 10655	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))) ∈ ℂ)
83	79, 82	addcld 10654	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) ∈ ℂ)
84	10	sqcld 13502	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵↑2) ∈ ℂ)
85	84, 19	mulcld 10655	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) · 𝐷) ∈ ℂ)
86	83, 85	addcld 10654	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) ∈ ℂ)
87	84, 78	mulcld 10655	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) · (𝐶↑2)) ∈ ℂ)
88	87, 82	subcld 10991	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) ∈ ℂ)
89	77, 19	mulcld 10655	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · 𝐷) ∈ ℂ)
90	88, 89	addcld 10654	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) ∈ ℂ)
91	26	sqcld 13502	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝑄↑2) ∈ ℂ)
92		2z 12008	. . . . . . . 8 ⊢ 2 ∈ ℤ
93	92	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 2 ∈ ℤ)
94	26, 32, 93	expne0d 13510	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝑄↑2) ≠ 0)
95	86, 90, 91, 94	divdird 11448	. . . . 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 10862	. . . . . . . 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 11031	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) = (((𝐴↑2) · (𝐶↑2)) + ((𝐵↑2) · (𝐶↑2))))
98	55	sqcld 13502	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴↑2) ∈ ℂ)
99	98, 84, 78	adddird 10660	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) + (𝐵↑2)) · (𝐶↑2)) = (((𝐴↑2) · (𝐶↑2)) + ((𝐵↑2) · (𝐶↑2))))
100	15	eqcomi 2830	. . . . . . . . . . . 12 ⊢ ((𝐴↑2) + (𝐵↑2)) = 𝑄
101	100	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) + (𝐵↑2)) = 𝑄)
102	101	oveq1d 7165	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) + (𝐵↑2)) · (𝐶↑2)) = (𝑄 · (𝐶↑2)))
103	97, 99, 102	3eqtr2d 2862	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) = (𝑄 · (𝐶↑2)))
104	84, 98, 19	adddird 10660	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) + (𝐴↑2)) · 𝐷) = (((𝐵↑2) · 𝐷) + ((𝐴↑2) · 𝐷)))
105	84, 98	addcomd 10836	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) + (𝐴↑2)) = ((𝐴↑2) + (𝐵↑2)))
106	105, 101	eqtrd 2856	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) + (𝐴↑2)) = 𝑄)
107	106	oveq1d 7165	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) + (𝐴↑2)) · 𝐷) = (𝑄 · 𝐷))
108	104, 107	eqtr3d 2858	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) · 𝐷) + ((𝐴↑2) · 𝐷)) = (𝑄 · 𝐷))
109	103, 108	oveq12d 7168	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) + (((𝐵↑2) · 𝐷) + ((𝐴↑2) · 𝐷))) = ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)))
110	96, 109	eqtrd 2856	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) + ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷))) = ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)))
111	110	oveq1d 7165	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) + ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷))) / (𝑄↑2)) = (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)))
112	26, 78, 19	adddid 10659	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝑄 · ((𝐶↑2) + 𝐷)) = ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)))
113	112	eqcomd 2827	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) = (𝑄 · ((𝐶↑2) + 𝐷)))
114	26	sqvald 13501	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝑄↑2) = (𝑄 · 𝑄))
115	113, 114	oveq12d 7168	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)) = ((𝑄 · ((𝐶↑2) + 𝐷)) / (𝑄 · 𝑄)))
116	78, 19	addcld 10654	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐶↑2) + 𝐷) ∈ ℂ)
117	116, 26, 26, 32, 32	divcan5d 11436	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝑄 · ((𝐶↑2) + 𝐷)) / (𝑄 · 𝑄)) = (((𝐶↑2) + 𝐷) / 𝑄))
118	115, 117	eqtrd 2856	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)) = (((𝐶↑2) + 𝐷) / 𝑄))
119	16	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)))
120	119	oveq2d 7166	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐶↑2) + 𝐷) = ((𝐶↑2) + (((𝑅↑2) · 𝑄) − (𝐶↑2))))
121		rpcn 12393	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℂ)
122	121	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷) → 𝑅 ∈ ℂ)
123	122	3ad2ant3 1131	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝑅 ∈ ℂ)
124	123	sqcld 13502	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝑅↑2) ∈ ℂ)
125	124, 26	mulcld 10655	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝑅↑2) · 𝑄) ∈ ℂ)
126	78, 125	pncan3d 10994	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐶↑2) + (((𝑅↑2) · 𝑄) − (𝐶↑2))) = ((𝑅↑2) · 𝑄))
127	120, 126	eqtrd 2856	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐶↑2) + 𝐷) = ((𝑅↑2) · 𝑄))
128	116, 124, 26, 32	divmul3d 11444	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐶↑2) + 𝐷) / 𝑄) = (𝑅↑2) ↔ ((𝐶↑2) + 𝐷) = ((𝑅↑2) · 𝑄)))
129	127, 128	mpbird 259	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐶↑2) + 𝐷) / 𝑄) = (𝑅↑2))
130	118, 129	eqtrd 2856	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)) = (𝑅↑2))
131	111, 130	eqtrd 2856	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) + ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷))) / (𝑄↑2)) = (𝑅↑2))
132	76, 95, 131	3eqtr2d 2862	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2))
133	3, 22, 26, 32	divassd 11445	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) / 𝑄) = (𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
134	3, 7, 21	adddid 10659	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) = ((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))))
135	1	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
136	4	adantl 484	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
137	135, 135, 136	mulassd 10658	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐴) · 𝐶) = (𝐴 · (𝐴 · 𝐶)))
138	135	sqvald 13501	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) = (𝐴 · 𝐴))
139	138	eqcomd 2827	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐴) = (𝐴↑2))
140	139	oveq1d 7165	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐴) · 𝐶) = ((𝐴↑2) · 𝐶))
141	137, 140	eqtr3d 2858	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐴 · 𝐶)) = ((𝐴↑2) · 𝐶))
142	141	3adant2 1127	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐴 · 𝐶)) = ((𝐴↑2) · 𝐶))
143	142	3ad2ant1 1129	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (𝐴 · 𝐶)) = ((𝐴↑2) · 𝐶))
144	3, 10, 20	mulassd 10658	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐵) · (√‘𝐷)) = (𝐴 · (𝐵 · (√‘𝐷))))
145	144	eqcomd 2827	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (𝐵 · (√‘𝐷))) = ((𝐴 · 𝐵) · (√‘𝐷)))
146	143, 145	oveq12d 7168	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))))
147	134, 146	eqtrd 2856	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))))
148	147	oveq1d 7165	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) / 𝑄) = ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
149	133, 148	eqtr3d 2858	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) = ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
150	10, 53, 26, 32	divassd 11445	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄) = (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)))
151	10, 51, 52	subdid 11090	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) = ((𝐵 · (𝐵 · 𝐶)) − (𝐵 · (𝐴 · (√‘𝐷)))))
152		simpl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℝ)
153	152	recnd 10663	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
154		simpr 487	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
155	154	recnd 10663	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
156	153, 153, 155	mulassd 10658	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 · 𝐵) · 𝐶) = (𝐵 · (𝐵 · 𝐶)))
157	8	sqvald 13501	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ ℝ → (𝐵↑2) = (𝐵 · 𝐵))
158	157	eqcomd 2827	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ ℝ → (𝐵 · 𝐵) = (𝐵↑2))
159	158	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · 𝐵) = (𝐵↑2))
160	159	oveq1d 7165	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 · 𝐵) · 𝐶) = ((𝐵↑2) · 𝐶))
161	156, 160	eqtr3d 2858	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · (𝐵 · 𝐶)) = ((𝐵↑2) · 𝐶))
162	161	3adant1 1126	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · (𝐵 · 𝐶)) = ((𝐵↑2) · 𝐶))
163	162	3ad2ant1 1129	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · (𝐵 · 𝐶)) = ((𝐵↑2) · 𝐶))
164	10, 3, 20	mulassd 10658	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐴) · (√‘𝐷)) = (𝐵 · (𝐴 · (√‘𝐷))))
165	9, 2	mulcomd 10656	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · 𝐴) = (𝐴 · 𝐵))
166	165	3ad2ant1 1129	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · 𝐴) = (𝐴 · 𝐵))
167	166	oveq1d 7165	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐴) · (√‘𝐷)) = ((𝐴 · 𝐵) · (√‘𝐷)))
168	164, 167	eqtr3d 2858	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · (𝐴 · (√‘𝐷))) = ((𝐴 · 𝐵) · (√‘𝐷)))
169	163, 168	oveq12d 7168	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · (𝐵 · 𝐶)) − (𝐵 · (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))))
170	151, 169	eqtrd 2856	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))))
171	170	oveq1d 7165	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄) = ((((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
172	150, 171	eqtr3d 2858	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) = ((((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
173	149, 172	oveq12d 7168	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = (((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄) + ((((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄)))
174	77, 6	mulcld 10655	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · 𝐶) ∈ ℂ)
175	3, 10	mulcld 10655	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · 𝐵) ∈ ℂ)
176	175, 20	mulcld 10655	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐵) · (√‘𝐷)) ∈ ℂ)
177	174, 176	addcld 10654	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) ∈ ℂ)
178	84, 6	mulcld 10655	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) · 𝐶) ∈ ℂ)
179	178, 176	subcld 10991	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) ∈ ℂ)
180	177, 179, 26, 32	divdird 11448	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = (((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄) + ((((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄)))
181	174, 176, 178	ppncand 11031	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
182	77, 84, 6	adddird 10660	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) + (𝐵↑2)) · 𝐶) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
183	15	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝑄 = ((𝐴↑2) + (𝐵↑2)))
184	183	eqcomd 2827	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) + (𝐵↑2)) = 𝑄)
185	184	oveq1d 7165	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) + (𝐵↑2)) · 𝐶) = (𝑄 · 𝐶))
186	181, 182, 185	3eqtr2d 2862	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) = (𝑄 · 𝐶))
187	177, 179	addcld 10654	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) ∈ ℂ)
188	187, 6, 26, 32	divmul2d 11443	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = 𝐶 ↔ ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) = (𝑄 · 𝐶)))
189	186, 188	mpbird 259	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = 𝐶)
190	173, 180, 189	3eqtr2d 2862	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶)
191	132, 190	jca 514	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2) ∧ ((𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶))
192		oveq1 7157	. . . . . 6 ⊢ (𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) → (𝑋↑2) = ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2))
193		oveq1 7157	. . . . . 6 ⊢ (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → (𝑌↑2) = ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2))
194	192, 193	oveqan12d 7169	. . . . 5 ⊢ ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → ((𝑋↑2) + (𝑌↑2)) = (((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)))
195	194	eqeq1d 2823	. . . 4 ⊢ ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ↔ (((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2)))
196		oveq2 7158	. . . . . 6 ⊢ (𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) → (𝐴 · 𝑋) = (𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
197		oveq2 7158	. . . . . 6 ⊢ (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → (𝐵 · 𝑌) = (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)))
198	196, 197	oveqan12d 7169	. . . . 5 ⊢ ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = ((𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))))
199	198	eqeq1d 2823	. . . 4 ⊢ ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 ↔ ((𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶))
200	195, 199	anbi12d 632	. . 3 ⊢ ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) ↔ ((((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2) ∧ ((𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶)))
201	191, 200	syl5ibrcom 249	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)))
202	35, 21	subcld 10991	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ∈ ℂ)
203	202, 26, 32	sqdivd 13517	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) = ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))↑2) / (𝑄↑2)))
204		binom2sub 13575	. . . . . . . . . . 11 ⊢ (((𝐴 · 𝐶) ∈ ℂ ∧ (𝐵 · (√‘𝐷)) ∈ ℂ) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))↑2) = ((((𝐴 · 𝐶)↑2) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)))
205	35, 21, 204	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))↑2) = ((((𝐴 · 𝐶)↑2) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)))
206	39	oveq1d 7165	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶)↑2) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) = (((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))))
207	206, 46	oveq12d 7168	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶)↑2) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)) = ((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)))
208	205, 207	eqtrd 2856	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))↑2) = ((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)))
209	208	oveq1d 7165	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))↑2) / (𝑄↑2)) = (((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)))
210	203, 209	eqtrd 2856	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) = (((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)))
211	51, 56	addcld 10654	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℂ)
212	211, 26, 32	sqdivd 13517	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2) = ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))↑2) / (𝑄↑2)))
213		binom2 13573	. . . . . . . . . . 11 ⊢ (((𝐵 · 𝐶) ∈ ℂ ∧ (𝐴 · (√‘𝐷)) ∈ ℂ) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))↑2) = ((((𝐵 · 𝐶)↑2) + (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)))
214	51, 56, 213	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))↑2) = ((((𝐵 · 𝐶)↑2) + (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)))
215	60, 67	oveq12d 7168	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶)↑2) + (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) = (((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))))
216	215, 71	oveq12d 7168	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶)↑2) + (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)) = ((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)))
217	214, 216	eqtrd 2856	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))↑2) = ((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)))
218	217	oveq1d 7165	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))↑2) / (𝑄↑2)) = (((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2)))
219	212, 218	eqtrd 2856	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2) = (((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2)))
220	210, 219	oveq12d 7168	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = ((((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)) + (((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2))))
221	98, 78	mulcld 10655	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · (𝐶↑2)) ∈ ℂ)
222	35, 21	mulcld 10655	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))) ∈ ℂ)
223	80, 222	mulcld 10655	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))) ∈ ℂ)
224	221, 223	subcld 10991	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) ∈ ℂ)
225	224, 85	addcld 10654	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) ∈ ℂ)
226	87, 223	addcld 10654	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) ∈ ℂ)
227	98, 19	mulcld 10655	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · 𝐷) ∈ ℂ)
228	226, 227	addcld 10654	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) ∈ ℂ)
229	225, 228, 91, 94	divdird 11448	. . . . . 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 10862	. . . . . . . 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 11018	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) = (((𝐴↑2) · (𝐶↑2)) + ((𝐵↑2) · (𝐶↑2))))
232	231, 99, 102	3eqtr2d 2862	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) = (𝑄 · (𝐶↑2)))
233	232, 108	oveq12d 7168	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) + (((𝐵↑2) · 𝐷) + ((𝐴↑2) · 𝐷))) = ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)))
234	230, 233	eqtrd 2856	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) + ((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷))) = ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)))
235	234	oveq1d 7165	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) + ((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷))) / (𝑄↑2)) = (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)))
236	220, 229, 235	3eqtr2d 2862	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)))
237	236, 130	eqtrd 2856	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2))
238		simp1 1132	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ)
239		simp3 1134	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
240	238, 239	remulcld 10665	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐶) ∈ ℝ)
241	240	recnd 10663	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐶) ∈ ℂ)
242	241	3ad2ant1 1129	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · 𝐶) ∈ ℂ)
243	242, 21	subcld 10991	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ∈ ℂ)
244	3, 243, 26, 32	divassd 11445	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) / 𝑄) = (𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
245	3, 242, 21	subdid 11090	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) = ((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))))
246	143, 145	oveq12d 7168	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))))
247	245, 246	eqtrd 2856	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))))
248	247	oveq1d 7165	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) / 𝑄) = ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
249	244, 248	eqtr3d 2858	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) = ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
250	51, 52	addcld 10654	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℂ)
251	10, 250, 26, 32	divassd 11445	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄) = (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
252	10, 51, 52	adddid 10659	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) = ((𝐵 · (𝐵 · 𝐶)) + (𝐵 · (𝐴 · (√‘𝐷)))))
253	163, 168	oveq12d 7168	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · (𝐵 · 𝐶)) + (𝐵 · (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))))
254	252, 253	eqtrd 2856	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))))
255	254	oveq1d 7165	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄) = ((((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
256	251, 255	eqtr3d 2858	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) = ((((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
257	249, 256	oveq12d 7168	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = (((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄) + ((((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄)))
258	174, 176	subcld 10991	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) ∈ ℂ)
259	178, 176	addcld 10654	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) ∈ ℂ)
260	258, 259, 26, 32	divdird 11448	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = (((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄) + ((((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄)))
261	174, 176, 178	nppcan3d 11018	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
262	261, 182, 185	3eqtr2d 2862	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) = (𝑄 · 𝐶))
263	258, 259	addcld 10654	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) ∈ ℂ)
264	263, 6, 26, 32	divmul2d 11443	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = 𝐶 ↔ ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) = (𝑄 · 𝐶)))
265	262, 264	mpbird 259	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = 𝐶)
266	257, 260, 265	3eqtr2d 2862	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶)
267	237, 266	jca 514	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2) ∧ ((𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶))
268		oveq1 7157	. . . . . 6 ⊢ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) → (𝑋↑2) = ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2))
269		oveq1 7157	. . . . . 6 ⊢ (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → (𝑌↑2) = ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2))
270	268, 269	oveqan12d 7169	. . . . 5 ⊢ ((𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → ((𝑋↑2) + (𝑌↑2)) = (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)))
271	270	eqeq1d 2823	. . . 4 ⊢ ((𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ↔ (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2)))
272		oveq2 7158	. . . . . 6 ⊢ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) → (𝐴 · 𝑋) = (𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
273		oveq2 7158	. . . . . 6 ⊢ (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → (𝐵 · 𝑌) = (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
274	272, 273	oveqan12d 7169	. . . . 5 ⊢ ((𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = ((𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))
275	274	eqeq1d 2823	. . . 4 ⊢ ((𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 ↔ ((𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶))
276	271, 275	anbi12d 632	. . 3 ⊢ ((𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) ↔ ((((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2) ∧ ((𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶)))
277	267, 276	syl5ibrcom 249	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)))
278	201, 277	jaod 855	1 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) → (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 398 ∨ wo 843 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ≠ wne 3016 class class class wbr 5058 ‘cfv 6349 (class class class)co 7150 ℂcc 10529 ℝcr 10530 0cc0 10531 + caddc 10534 · cmul 10536 < clt 10669 ≤ cle 10670 − cmin 10864 / cdiv 11291 2c2 11686 ℤcz 11975 ℝ⁺crp 12383 ↑cexp 13423 √csqrt 14586

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608 ax-pre-sup 10609

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-tp 4565 df-op 4567 df-uni 4832 df-iun 4913 df-br 5059 df-opab 5121 df-mpt 5139 df-tr 5165 df-id 5454 df-eprel 5459 df-po 5468 df-so 5469 df-fr 5508 df-we 5510 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-pred 6142 df-ord 6188 df-on 6189 df-lim 6190 df-suc 6191 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7575 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-er 8283 df-en 8504 df-dom 8505 df-sdom 8506 df-sup 8900 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-div 11292 df-nn 11633 df-2 11694 df-3 11695 df-n0 11892 df-z 11976 df-uz 12238 df-rp 12384 df-seq 13364 df-exp 13424 df-cj 14452 df-re 14453 df-im 14454 df-sqrt 14588 df-abs 14589

This theorem is referenced by: itsclc0xyqsolb 44751

W3C validator