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 47101

Description: Lemma for itsclc0 47103. 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 11182	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2	1	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
3	2	3ad2ant1 1133	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐴 ∈ ℂ)
4		recn 11182	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ ℂ)
5	4	3ad2ant3 1135	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
6	5	3ad2ant1 1133	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐶 ∈ ℂ)
7	3, 6	mulcld 11216	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · 𝐶) ∈ ℂ)
8		recn 11182	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
9	8	3ad2ant2 1134	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
10	9	3ad2ant1 1133	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐵 ∈ ℂ)
11		rpre 12964	. . . . . . . . . . . . . . . 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 47090	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ) → 𝐷 ∈ ℝ)
18	14, 17	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐷 ∈ ℝ)
19	18	recnd 11224	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐷 ∈ ℂ)
20	19	sqrtcld 15366	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (√‘𝐷) ∈ ℂ)
21	10, 20	mulcld 11216	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · (√‘𝐷)) ∈ ℂ)
22	7, 21	addcld 11215	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) ∈ ℂ)
23	15	resum2sqcl 47038	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈ ℝ)
24	23	3adant3 1132	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝑄 ∈ ℝ)
25	24	recnd 11224	. . . . . . . . 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 47041	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) → 0 < 𝑄)
31	27, 28, 29, 30	syl3anc 1371	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 0 < 𝑄)
32	31	gt0ne0d 11760	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝑄 ≠ 0)
33	22, 26, 32	sqdivd 14106	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) = ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))↑2) / (𝑄↑2)))
34	2, 5	mulcld 11216	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐶) ∈ ℂ)
35	34	3ad2ant1 1133	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · 𝐶) ∈ ℂ)
36		binom2 14163	. . . . . . . . . 10 ⊢ (((𝐴 · 𝐶) ∈ ℂ ∧ (𝐵 · (√‘𝐷)) ∈ ℂ) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))↑2) = ((((𝐴 · 𝐶)↑2) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)))
37	35, 21, 36	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))↑2) = ((((𝐴 · 𝐶)↑2) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)))
38	2, 5	sqmuld 14105	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶)↑2) = ((𝐴↑2) · (𝐶↑2)))
39	38	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶)↑2) = ((𝐴↑2) · (𝐶↑2)))
40	39	oveq1d 7408	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶)↑2) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) = (((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))))
41	10, 20	sqmuld 14105	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · (√‘𝐷))↑2) = ((𝐵↑2) · ((√‘𝐷)↑2)))
42		simp3r 1202	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 0 ≤ 𝐷)
43		resqrtth 15184	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ ℝ ∧ 0 ≤ 𝐷) → ((√‘𝐷)↑2) = 𝐷)
44	18, 42, 43	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((√‘𝐷)↑2) = 𝐷)
45	44	oveq2d 7409	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) · ((√‘𝐷)↑2)) = ((𝐵↑2) · 𝐷))
46	41, 45	eqtrd 2771	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · (√‘𝐷))↑2) = ((𝐵↑2) · 𝐷))
47	40, 46	oveq12d 7411	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶)↑2) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)) = ((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)))
48	37, 47	eqtrd 2771	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))↑2) = ((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)))
49	48	oveq1d 7408	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))↑2) / (𝑄↑2)) = (((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)))
50	33, 49	eqtrd 2771	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) = (((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)))
51	10, 6	mulcld 11216	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · 𝐶) ∈ ℂ)
52	3, 20	mulcld 11216	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (√‘𝐷)) ∈ ℂ)
53	51, 52	subcld 11553	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ∈ ℂ)
54	53, 26, 32	sqdivd 14106	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2) = ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))↑2) / (𝑄↑2)))
55	27	recnd 11224	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐴 ∈ ℂ)
56	55, 20	mulcld 11216	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (√‘𝐷)) ∈ ℂ)
57		binom2sub 14165	. . . . . . . . . 10 ⊢ (((𝐵 · 𝐶) ∈ ℂ ∧ (𝐴 · (√‘𝐷)) ∈ ℂ) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))↑2) = ((((𝐵 · 𝐶)↑2) − (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)))
58	51, 56, 57	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))↑2) = ((((𝐵 · 𝐶)↑2) − (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)))
59	9, 5	sqmuld 14105	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 · 𝐶)↑2) = ((𝐵↑2) · (𝐶↑2)))
60	59	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶)↑2) = ((𝐵↑2) · (𝐶↑2)))
61	10, 6, 55, 20	mul4d 11408	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐴) · (𝐶 · (√‘𝐷))))
62	10, 55	mulcomd 11217	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · 𝐴) = (𝐴 · 𝐵))
63	62	oveq1d 7408	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐴) · (𝐶 · (√‘𝐷))) = ((𝐴 · 𝐵) · (𝐶 · (√‘𝐷))))
64	55, 10, 6, 20	mul4d 11408	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐵) · (𝐶 · (√‘𝐷))) = ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))
65	63, 64	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐴) · (𝐶 · (√‘𝐷))) = ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))
66	61, 65	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))) = ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))
67	66	oveq2d 7409	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷)))) = (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))
68	60, 67	oveq12d 7411	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶)↑2) − (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) = (((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))))
69	55, 20	sqmuld 14105	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (√‘𝐷))↑2) = ((𝐴↑2) · ((√‘𝐷)↑2)))
70	44	oveq2d 7409	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · ((√‘𝐷)↑2)) = ((𝐴↑2) · 𝐷))
71	69, 70	eqtrd 2771	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (√‘𝐷))↑2) = ((𝐴↑2) · 𝐷))
72	68, 71	oveq12d 7411	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶)↑2) − (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)) = ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)))
73	58, 72	eqtrd 2771	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))↑2) = ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)))
74	73	oveq1d 7408	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))↑2) / (𝑄↑2)) = (((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2)))
75	54, 74	eqtrd 2771	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2) = (((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2)))
76	50, 75	oveq12d 7411	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = ((((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)) + (((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2))))
77	3	sqcld 14091	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴↑2) ∈ ℂ)
78	6	sqcld 14091	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐶↑2) ∈ ℂ)
79	77, 78	mulcld 11216	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · (𝐶↑2)) ∈ ℂ)
80		2cnd 12272	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 2 ∈ ℂ)
81	7, 21	mulcld 11216	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))) ∈ ℂ)
82	80, 81	mulcld 11216	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))) ∈ ℂ)
83	79, 82	addcld 11215	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) ∈ ℂ)
84	10	sqcld 14091	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵↑2) ∈ ℂ)
85	84, 19	mulcld 11216	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) · 𝐷) ∈ ℂ)
86	83, 85	addcld 11215	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) ∈ ℂ)
87	84, 78	mulcld 11216	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) · (𝐶↑2)) ∈ ℂ)
88	87, 82	subcld 11553	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) ∈ ℂ)
89	77, 19	mulcld 11216	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · 𝐷) ∈ ℂ)
90	88, 89	addcld 11215	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) ∈ ℂ)
91	26	sqcld 14091	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝑄↑2) ∈ ℂ)
92		2z 12576	. . . . . . . 8 ⊢ 2 ∈ ℤ
93	92	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 2 ∈ ℤ)
94	26, 32, 93	expne0d 14099	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝑄↑2) ≠ 0)
95	86, 90, 91, 94	divdird 12010	. . . . 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 11424	. . . . . . . 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 11593	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) = (((𝐴↑2) · (𝐶↑2)) + ((𝐵↑2) · (𝐶↑2))))
98	55	sqcld 14091	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴↑2) ∈ ℂ)
99	98, 84, 78	adddird 11221	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) + (𝐵↑2)) · (𝐶↑2)) = (((𝐴↑2) · (𝐶↑2)) + ((𝐵↑2) · (𝐶↑2))))
100	15	eqcomi 2740	. . . . . . . . . . . 12 ⊢ ((𝐴↑2) + (𝐵↑2)) = 𝑄
101	100	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) + (𝐵↑2)) = 𝑄)
102	101	oveq1d 7408	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) + (𝐵↑2)) · (𝐶↑2)) = (𝑄 · (𝐶↑2)))
103	97, 99, 102	3eqtr2d 2777	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) = (𝑄 · (𝐶↑2)))
104	84, 98, 19	adddird 11221	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) + (𝐴↑2)) · 𝐷) = (((𝐵↑2) · 𝐷) + ((𝐴↑2) · 𝐷)))
105	84, 98	addcomd 11398	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) + (𝐴↑2)) = ((𝐴↑2) + (𝐵↑2)))
106	105, 101	eqtrd 2771	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) + (𝐴↑2)) = 𝑄)
107	106	oveq1d 7408	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) + (𝐴↑2)) · 𝐷) = (𝑄 · 𝐷))
108	104, 107	eqtr3d 2773	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) · 𝐷) + ((𝐴↑2) · 𝐷)) = (𝑄 · 𝐷))
109	103, 108	oveq12d 7411	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) + (((𝐵↑2) · 𝐷) + ((𝐴↑2) · 𝐷))) = ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)))
110	96, 109	eqtrd 2771	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) + ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷))) = ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)))
111	110	oveq1d 7408	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) + ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷))) / (𝑄↑2)) = (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)))
112	26, 78, 19	adddid 11220	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝑄 · ((𝐶↑2) + 𝐷)) = ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)))
113	112	eqcomd 2737	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) = (𝑄 · ((𝐶↑2) + 𝐷)))
114	26	sqvald 14090	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝑄↑2) = (𝑄 · 𝑄))
115	113, 114	oveq12d 7411	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)) = ((𝑄 · ((𝐶↑2) + 𝐷)) / (𝑄 · 𝑄)))
116	78, 19	addcld 11215	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐶↑2) + 𝐷) ∈ ℂ)
117	116, 26, 26, 32, 32	divcan5d 11998	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝑄 · ((𝐶↑2) + 𝐷)) / (𝑄 · 𝑄)) = (((𝐶↑2) + 𝐷) / 𝑄))
118	115, 117	eqtrd 2771	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)) = (((𝐶↑2) + 𝐷) / 𝑄))
119	16	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)))
120	119	oveq2d 7409	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐶↑2) + 𝐷) = ((𝐶↑2) + (((𝑅↑2) · 𝑄) − (𝐶↑2))))
121		rpcn 12966	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℂ)
122	121	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷) → 𝑅 ∈ ℂ)
123	122	3ad2ant3 1135	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝑅 ∈ ℂ)
124	123	sqcld 14091	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝑅↑2) ∈ ℂ)
125	124, 26	mulcld 11216	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝑅↑2) · 𝑄) ∈ ℂ)
126	78, 125	pncan3d 11556	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐶↑2) + (((𝑅↑2) · 𝑄) − (𝐶↑2))) = ((𝑅↑2) · 𝑄))
127	120, 126	eqtrd 2771	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐶↑2) + 𝐷) = ((𝑅↑2) · 𝑄))
128	116, 124, 26, 32	divmul3d 12006	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐶↑2) + 𝐷) / 𝑄) = (𝑅↑2) ↔ ((𝐶↑2) + 𝐷) = ((𝑅↑2) · 𝑄)))
129	127, 128	mpbird 256	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐶↑2) + 𝐷) / 𝑄) = (𝑅↑2))
130	118, 129	eqtrd 2771	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)) = (𝑅↑2))
131	111, 130	eqtrd 2771	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) + ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷))) / (𝑄↑2)) = (𝑅↑2))
132	76, 95, 131	3eqtr2d 2777	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2))
133	3, 22, 26, 32	divassd 12007	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) / 𝑄) = (𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
134	3, 7, 21	adddid 11220	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) = ((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))))
135	1	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
136	4	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
137	135, 135, 136	mulassd 11219	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐴) · 𝐶) = (𝐴 · (𝐴 · 𝐶)))
138	135	sqvald 14090	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) = (𝐴 · 𝐴))
139	138	eqcomd 2737	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐴) = (𝐴↑2))
140	139	oveq1d 7408	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐴) · 𝐶) = ((𝐴↑2) · 𝐶))
141	137, 140	eqtr3d 2773	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐴 · 𝐶)) = ((𝐴↑2) · 𝐶))
142	141	3adant2 1131	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐴 · 𝐶)) = ((𝐴↑2) · 𝐶))
143	142	3ad2ant1 1133	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (𝐴 · 𝐶)) = ((𝐴↑2) · 𝐶))
144	3, 10, 20	mulassd 11219	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐵) · (√‘𝐷)) = (𝐴 · (𝐵 · (√‘𝐷))))
145	144	eqcomd 2737	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (𝐵 · (√‘𝐷))) = ((𝐴 · 𝐵) · (√‘𝐷)))
146	143, 145	oveq12d 7411	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))))
147	134, 146	eqtrd 2771	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))))
148	147	oveq1d 7408	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) / 𝑄) = ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
149	133, 148	eqtr3d 2773	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) = ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
150	10, 53, 26, 32	divassd 12007	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄) = (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)))
151	10, 51, 52	subdid 11652	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) = ((𝐵 · (𝐵 · 𝐶)) − (𝐵 · (𝐴 · (√‘𝐷)))))
152		simpl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℝ)
153	152	recnd 11224	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
154		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
155	154	recnd 11224	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
156	153, 153, 155	mulassd 11219	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 · 𝐵) · 𝐶) = (𝐵 · (𝐵 · 𝐶)))
157	8	sqvald 14090	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ ℝ → (𝐵↑2) = (𝐵 · 𝐵))
158	157	eqcomd 2737	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ ℝ → (𝐵 · 𝐵) = (𝐵↑2))
159	158	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · 𝐵) = (𝐵↑2))
160	159	oveq1d 7408	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 · 𝐵) · 𝐶) = ((𝐵↑2) · 𝐶))
161	156, 160	eqtr3d 2773	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · (𝐵 · 𝐶)) = ((𝐵↑2) · 𝐶))
162	161	3adant1 1130	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · (𝐵 · 𝐶)) = ((𝐵↑2) · 𝐶))
163	162	3ad2ant1 1133	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · (𝐵 · 𝐶)) = ((𝐵↑2) · 𝐶))
164	10, 3, 20	mulassd 11219	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐴) · (√‘𝐷)) = (𝐵 · (𝐴 · (√‘𝐷))))
165	9, 2	mulcomd 11217	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · 𝐴) = (𝐴 · 𝐵))
166	165	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · 𝐴) = (𝐴 · 𝐵))
167	166	oveq1d 7408	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐴) · (√‘𝐷)) = ((𝐴 · 𝐵) · (√‘𝐷)))
168	164, 167	eqtr3d 2773	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · (𝐴 · (√‘𝐷))) = ((𝐴 · 𝐵) · (√‘𝐷)))
169	163, 168	oveq12d 7411	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · (𝐵 · 𝐶)) − (𝐵 · (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))))
170	151, 169	eqtrd 2771	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))))
171	170	oveq1d 7408	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄) = ((((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
172	150, 171	eqtr3d 2773	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) = ((((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
173	149, 172	oveq12d 7411	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = (((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄) + ((((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄)))
174	77, 6	mulcld 11216	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · 𝐶) ∈ ℂ)
175	3, 10	mulcld 11216	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · 𝐵) ∈ ℂ)
176	175, 20	mulcld 11216	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐵) · (√‘𝐷)) ∈ ℂ)
177	174, 176	addcld 11215	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) ∈ ℂ)
178	84, 6	mulcld 11216	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) · 𝐶) ∈ ℂ)
179	178, 176	subcld 11553	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) ∈ ℂ)
180	177, 179, 26, 32	divdird 12010	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = (((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄) + ((((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄)))
181	174, 176, 178	ppncand 11593	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
182	77, 84, 6	adddird 11221	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) + (𝐵↑2)) · 𝐶) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
183	15	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝑄 = ((𝐴↑2) + (𝐵↑2)))
184	183	eqcomd 2737	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) + (𝐵↑2)) = 𝑄)
185	184	oveq1d 7408	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) + (𝐵↑2)) · 𝐶) = (𝑄 · 𝐶))
186	181, 182, 185	3eqtr2d 2777	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) = (𝑄 · 𝐶))
187	177, 179	addcld 11215	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) ∈ ℂ)
188	187, 6, 26, 32	divmul2d 12005	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = 𝐶 ↔ ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) = (𝑄 · 𝐶)))
189	186, 188	mpbird 256	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = 𝐶)
190	173, 180, 189	3eqtr2d 2777	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶)
191	132, 190	jca 512	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2) ∧ ((𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶))
192		oveq1 7400	. . . . . 6 ⊢ (𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) → (𝑋↑2) = ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2))
193		oveq1 7400	. . . . . 6 ⊢ (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → (𝑌↑2) = ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2))
194	192, 193	oveqan12d 7412	. . . . 5 ⊢ ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → ((𝑋↑2) + (𝑌↑2)) = (((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)))
195	194	eqeq1d 2733	. . . 4 ⊢ ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ↔ (((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2)))
196		oveq2 7401	. . . . . 6 ⊢ (𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) → (𝐴 · 𝑋) = (𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
197		oveq2 7401	. . . . . 6 ⊢ (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → (𝐵 · 𝑌) = (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)))
198	196, 197	oveqan12d 7412	. . . . 5 ⊢ ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = ((𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))))
199	198	eqeq1d 2733	. . . 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 11553	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ∈ ℂ)
203	202, 26, 32	sqdivd 14106	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) = ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))↑2) / (𝑄↑2)))
204		binom2sub 14165	. . . . . . . . . . 11 ⊢ (((𝐴 · 𝐶) ∈ ℂ ∧ (𝐵 · (√‘𝐷)) ∈ ℂ) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))↑2) = ((((𝐴 · 𝐶)↑2) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)))
205	35, 21, 204	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))↑2) = ((((𝐴 · 𝐶)↑2) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)))
206	39	oveq1d 7408	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶)↑2) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) = (((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))))
207	206, 46	oveq12d 7411	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶)↑2) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)) = ((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)))
208	205, 207	eqtrd 2771	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))↑2) = ((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)))
209	208	oveq1d 7408	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))↑2) / (𝑄↑2)) = (((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)))
210	203, 209	eqtrd 2771	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) = (((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)))
211	51, 56	addcld 11215	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℂ)
212	211, 26, 32	sqdivd 14106	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2) = ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))↑2) / (𝑄↑2)))
213		binom2 14163	. . . . . . . . . . 11 ⊢ (((𝐵 · 𝐶) ∈ ℂ ∧ (𝐴 · (√‘𝐷)) ∈ ℂ) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))↑2) = ((((𝐵 · 𝐶)↑2) + (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)))
214	51, 56, 213	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))↑2) = ((((𝐵 · 𝐶)↑2) + (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)))
215	60, 67	oveq12d 7411	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶)↑2) + (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) = (((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))))
216	215, 71	oveq12d 7411	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶)↑2) + (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)) = ((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)))
217	214, 216	eqtrd 2771	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))↑2) = ((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)))
218	217	oveq1d 7408	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))↑2) / (𝑄↑2)) = (((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2)))
219	212, 218	eqtrd 2771	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2) = (((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2)))
220	210, 219	oveq12d 7411	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = ((((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)) + (((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2))))
221	98, 78	mulcld 11216	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · (𝐶↑2)) ∈ ℂ)
222	35, 21	mulcld 11216	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))) ∈ ℂ)
223	80, 222	mulcld 11216	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))) ∈ ℂ)
224	221, 223	subcld 11553	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) ∈ ℂ)
225	224, 85	addcld 11215	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) ∈ ℂ)
226	87, 223	addcld 11215	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) ∈ ℂ)
227	98, 19	mulcld 11216	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · 𝐷) ∈ ℂ)
228	226, 227	addcld 11215	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) ∈ ℂ)
229	225, 228, 91, 94	divdird 12010	. . . . . 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 11424	. . . . . . . 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 11580	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) = (((𝐴↑2) · (𝐶↑2)) + ((𝐵↑2) · (𝐶↑2))))
232	231, 99, 102	3eqtr2d 2777	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) = (𝑄 · (𝐶↑2)))
233	232, 108	oveq12d 7411	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) + (((𝐵↑2) · 𝐷) + ((𝐴↑2) · 𝐷))) = ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)))
234	230, 233	eqtrd 2771	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) + ((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷))) = ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)))
235	234	oveq1d 7408	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) + ((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷))) / (𝑄↑2)) = (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)))
236	220, 229, 235	3eqtr2d 2777	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)))
237	236, 130	eqtrd 2771	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2))
238		simp1 1136	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ)
239		simp3 1138	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
240	238, 239	remulcld 11226	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐶) ∈ ℝ)
241	240	recnd 11224	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐶) ∈ ℂ)
242	241	3ad2ant1 1133	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · 𝐶) ∈ ℂ)
243	242, 21	subcld 11553	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ∈ ℂ)
244	3, 243, 26, 32	divassd 12007	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) / 𝑄) = (𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
245	3, 242, 21	subdid 11652	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) = ((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))))
246	143, 145	oveq12d 7411	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))))
247	245, 246	eqtrd 2771	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))))
248	247	oveq1d 7408	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) / 𝑄) = ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
249	244, 248	eqtr3d 2773	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) = ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
250	51, 52	addcld 11215	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℂ)
251	10, 250, 26, 32	divassd 12007	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄) = (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
252	10, 51, 52	adddid 11220	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) = ((𝐵 · (𝐵 · 𝐶)) + (𝐵 · (𝐴 · (√‘𝐷)))))
253	163, 168	oveq12d 7411	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · (𝐵 · 𝐶)) + (𝐵 · (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))))
254	252, 253	eqtrd 2771	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))))
255	254	oveq1d 7408	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄) = ((((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
256	251, 255	eqtr3d 2773	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) = ((((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
257	249, 256	oveq12d 7411	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = (((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄) + ((((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄)))
258	174, 176	subcld 11553	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) ∈ ℂ)
259	178, 176	addcld 11215	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) ∈ ℂ)
260	258, 259, 26, 32	divdird 12010	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = (((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄) + ((((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄)))
261	174, 176, 178	nppcan3d 11580	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
262	261, 182, 185	3eqtr2d 2777	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) = (𝑄 · 𝐶))
263	258, 259	addcld 11215	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) ∈ ℂ)
264	263, 6, 26, 32	divmul2d 12005	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = 𝐶 ↔ ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) = (𝑄 · 𝐶)))
265	262, 264	mpbird 256	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = 𝐶)
266	257, 260, 265	3eqtr2d 2777	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶)
267	237, 266	jca 512	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2) ∧ ((𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶))
268		oveq1 7400	. . . . . 6 ⊢ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) → (𝑋↑2) = ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2))
269		oveq1 7400	. . . . . 6 ⊢ (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → (𝑌↑2) = ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2))
270	268, 269	oveqan12d 7412	. . . . 5 ⊢ ((𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → ((𝑋↑2) + (𝑌↑2)) = (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)))
271	270	eqeq1d 2733	. . . 4 ⊢ ((𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ↔ (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2)))
272		oveq2 7401	. . . . . 6 ⊢ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) → (𝐴 · 𝑋) = (𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
273		oveq2 7401	. . . . . 6 ⊢ (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → (𝐵 · 𝑌) = (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
274	272, 273	oveqan12d 7412	. . . . 5 ⊢ ((𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = ((𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))
275	274	eqeq1d 2733	. . . 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 2939 class class class wbr 5141 ‘cfv 6532 (class class class)co 7393 ℂcc 11090 ℝcr 11091 0cc0 11092 + caddc 11095 · cmul 11097 < clt 11230 ≤ cle 11231 − cmin 11426 / cdiv 11853 2c2 12249 ℤcz 12540 ℝ⁺crp 12956 ↑cexp 14009 √csqrt 15162

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 2702 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7708 ax-cnex 11148 ax-resscn 11149 ax-1cn 11150 ax-icn 11151 ax-addcl 11152 ax-addrcl 11153 ax-mulcl 11154 ax-mulrcl 11155 ax-mulcom 11156 ax-addass 11157 ax-mulass 11158 ax-distr 11159 ax-i2m1 11160 ax-1ne0 11161 ax-1rid 11162 ax-rnegex 11163 ax-rrecex 11164 ax-cnre 11165 ax-pre-lttri 11166 ax-pre-lttrn 11167 ax-pre-ltadd 11168 ax-pre-mulgt0 11169 ax-pre-sup 11170

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 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4523 df-pw 4598 df-sn 4623 df-pr 4625 df-op 4629 df-uni 4902 df-iun 4992 df-br 5142 df-opab 5204 df-mpt 5225 df-tr 5259 df-id 5567 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-we 5626 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-pred 6289 df-ord 6356 df-on 6357 df-lim 6358 df-suc 6359 df-iota 6484 df-fun 6534 df-fn 6535 df-f 6536 df-f1 6537 df-fo 6538 df-f1o 6539 df-fv 6540 df-riota 7349 df-ov 7396 df-oprab 7397 df-mpo 7398 df-om 7839 df-2nd 7958 df-frecs 8248 df-wrecs 8279 df-recs 8353 df-rdg 8392 df-er 8686 df-en 8923 df-dom 8924 df-sdom 8925 df-sup 9419 df-pnf 11232 df-mnf 11233 df-xr 11234 df-ltxr 11235 df-le 11236 df-sub 11428 df-neg 11429 df-div 11854 df-nn 12195 df-2 12257 df-3 12258 df-n0 12455 df-z 12541 df-uz 12805 df-rp 12957 df-seq 13949 df-exp 14010 df-cj 15028 df-re 15029 df-im 15030 df-sqrt 15164 df-abs 15165

This theorem is referenced by: itsclc0xyqsolb 47102

W3C validator