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 46115

Description: Lemma for itsclc0 46117. 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 10961	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2	1	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
3	2	3ad2ant1 1132	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐴 ∈ ℂ)
4		recn 10961	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ ℂ)
5	4	3ad2ant3 1134	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
6	5	3ad2ant1 1132	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐶 ∈ ℂ)
7	3, 6	mulcld 10995	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · 𝐶) ∈ ℂ)
8		recn 10961	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
9	8	3ad2ant2 1133	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
10	9	3ad2ant1 1132	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐵 ∈ ℂ)
11		rpre 12738	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ)
12	11	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷) → 𝑅 ∈ ℝ)
13	12	anim2i 617	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ))
14	13	3adant2 1130	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ))
15		itsclc0xyqsolr.q	. . . . . . . . . . . . . 14 ⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))
16		itsclc0xyqsolr.d	. . . . . . . . . . . . . 14 ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2))
17	15, 16	itsclc0lem3 46104	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ) → 𝐷 ∈ ℝ)
18	14, 17	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐷 ∈ ℝ)
19	18	recnd 11003	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐷 ∈ ℂ)
20	19	sqrtcld 15149	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (√‘𝐷) ∈ ℂ)
21	10, 20	mulcld 10995	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · (√‘𝐷)) ∈ ℂ)
22	7, 21	addcld 10994	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) ∈ ℂ)
23	15	resum2sqcl 46052	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈ ℝ)
24	23	3adant3 1131	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝑄 ∈ ℝ)
25	24	recnd 11003	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝑄 ∈ ℂ)
26	25	3ad2ant1 1132	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝑄 ∈ ℂ)
27		simp11 1202	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐴 ∈ ℝ)
28		simp12 1203	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐵 ∈ ℝ)
29		simp2 1136	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0))
30	15	resum2sqorgt0 46055	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) → 0 < 𝑄)
31	27, 28, 29, 30	syl3anc 1370	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 0 < 𝑄)
32	31	gt0ne0d 11539	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝑄 ≠ 0)
33	22, 26, 32	sqdivd 13877	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) = ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))↑2) / (𝑄↑2)))
34	2, 5	mulcld 10995	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐶) ∈ ℂ)
35	34	3ad2ant1 1132	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · 𝐶) ∈ ℂ)
36		binom2 13933	. . . . . . . . . 10 ⊢ (((𝐴 · 𝐶) ∈ ℂ ∧ (𝐵 · (√‘𝐷)) ∈ ℂ) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))↑2) = ((((𝐴 · 𝐶)↑2) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)))
37	35, 21, 36	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))↑2) = ((((𝐴 · 𝐶)↑2) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)))
38	2, 5	sqmuld 13876	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶)↑2) = ((𝐴↑2) · (𝐶↑2)))
39	38	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶)↑2) = ((𝐴↑2) · (𝐶↑2)))
40	39	oveq1d 7290	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶)↑2) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) = (((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))))
41	10, 20	sqmuld 13876	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · (√‘𝐷))↑2) = ((𝐵↑2) · ((√‘𝐷)↑2)))
42		simp3r 1201	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 0 ≤ 𝐷)
43		resqrtth 14967	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ ℝ ∧ 0 ≤ 𝐷) → ((√‘𝐷)↑2) = 𝐷)
44	18, 42, 43	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((√‘𝐷)↑2) = 𝐷)
45	44	oveq2d 7291	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) · ((√‘𝐷)↑2)) = ((𝐵↑2) · 𝐷))
46	41, 45	eqtrd 2778	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · (√‘𝐷))↑2) = ((𝐵↑2) · 𝐷))
47	40, 46	oveq12d 7293	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶)↑2) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)) = ((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)))
48	37, 47	eqtrd 2778	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))↑2) = ((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)))
49	48	oveq1d 7290	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))↑2) / (𝑄↑2)) = (((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)))
50	33, 49	eqtrd 2778	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) = (((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)))
51	10, 6	mulcld 10995	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · 𝐶) ∈ ℂ)
52	3, 20	mulcld 10995	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (√‘𝐷)) ∈ ℂ)
53	51, 52	subcld 11332	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) ∈ ℂ)
54	53, 26, 32	sqdivd 13877	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2) = ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))↑2) / (𝑄↑2)))
55	27	recnd 11003	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐴 ∈ ℂ)
56	55, 20	mulcld 10995	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (√‘𝐷)) ∈ ℂ)
57		binom2sub 13935	. . . . . . . . . 10 ⊢ (((𝐵 · 𝐶) ∈ ℂ ∧ (𝐴 · (√‘𝐷)) ∈ ℂ) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))↑2) = ((((𝐵 · 𝐶)↑2) − (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)))
58	51, 56, 57	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))↑2) = ((((𝐵 · 𝐶)↑2) − (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)))
59	9, 5	sqmuld 13876	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 · 𝐶)↑2) = ((𝐵↑2) · (𝐶↑2)))
60	59	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶)↑2) = ((𝐵↑2) · (𝐶↑2)))
61	10, 6, 55, 20	mul4d 11187	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))) = ((𝐵 · 𝐴) · (𝐶 · (√‘𝐷))))
62	10, 55	mulcomd 10996	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · 𝐴) = (𝐴 · 𝐵))
63	62	oveq1d 7290	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐴) · (𝐶 · (√‘𝐷))) = ((𝐴 · 𝐵) · (𝐶 · (√‘𝐷))))
64	55, 10, 6, 20	mul4d 11187	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐵) · (𝐶 · (√‘𝐷))) = ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))
65	63, 64	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐴) · (𝐶 · (√‘𝐷))) = ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))
66	61, 65	eqtrd 2778	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))) = ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))
67	66	oveq2d 7291	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷)))) = (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))
68	60, 67	oveq12d 7293	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶)↑2) − (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) = (((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))))
69	55, 20	sqmuld 13876	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (√‘𝐷))↑2) = ((𝐴↑2) · ((√‘𝐷)↑2)))
70	44	oveq2d 7291	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · ((√‘𝐷)↑2)) = ((𝐴↑2) · 𝐷))
71	69, 70	eqtrd 2778	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (√‘𝐷))↑2) = ((𝐴↑2) · 𝐷))
72	68, 71	oveq12d 7293	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶)↑2) − (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)) = ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)))
73	58, 72	eqtrd 2778	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))↑2) = ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)))
74	73	oveq1d 7290	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))↑2) / (𝑄↑2)) = (((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2)))
75	54, 74	eqtrd 2778	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2) = (((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2)))
76	50, 75	oveq12d 7293	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = ((((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)) + (((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2))))
77	3	sqcld 13862	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴↑2) ∈ ℂ)
78	6	sqcld 13862	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐶↑2) ∈ ℂ)
79	77, 78	mulcld 10995	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · (𝐶↑2)) ∈ ℂ)
80		2cnd 12051	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 2 ∈ ℂ)
81	7, 21	mulcld 10995	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))) ∈ ℂ)
82	80, 81	mulcld 10995	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))) ∈ ℂ)
83	79, 82	addcld 10994	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) ∈ ℂ)
84	10	sqcld 13862	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵↑2) ∈ ℂ)
85	84, 19	mulcld 10995	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) · 𝐷) ∈ ℂ)
86	83, 85	addcld 10994	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) ∈ ℂ)
87	84, 78	mulcld 10995	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) · (𝐶↑2)) ∈ ℂ)
88	87, 82	subcld 11332	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) ∈ ℂ)
89	77, 19	mulcld 10995	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · 𝐷) ∈ ℂ)
90	88, 89	addcld 10994	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) ∈ ℂ)
91	26	sqcld 13862	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝑄↑2) ∈ ℂ)
92		2z 12352	. . . . . . . 8 ⊢ 2 ∈ ℤ
93	92	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 2 ∈ ℤ)
94	26, 32, 93	expne0d 13870	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝑄↑2) ≠ 0)
95	86, 90, 91, 94	divdird 11789	. . . . 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 11203	. . . . . . . 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 11372	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) = (((𝐴↑2) · (𝐶↑2)) + ((𝐵↑2) · (𝐶↑2))))
98	55	sqcld 13862	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴↑2) ∈ ℂ)
99	98, 84, 78	adddird 11000	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) + (𝐵↑2)) · (𝐶↑2)) = (((𝐴↑2) · (𝐶↑2)) + ((𝐵↑2) · (𝐶↑2))))
100	15	eqcomi 2747	. . . . . . . . . . . 12 ⊢ ((𝐴↑2) + (𝐵↑2)) = 𝑄
101	100	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) + (𝐵↑2)) = 𝑄)
102	101	oveq1d 7290	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) + (𝐵↑2)) · (𝐶↑2)) = (𝑄 · (𝐶↑2)))
103	97, 99, 102	3eqtr2d 2784	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) = (𝑄 · (𝐶↑2)))
104	84, 98, 19	adddird 11000	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) + (𝐴↑2)) · 𝐷) = (((𝐵↑2) · 𝐷) + ((𝐴↑2) · 𝐷)))
105	84, 98	addcomd 11177	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) + (𝐴↑2)) = ((𝐴↑2) + (𝐵↑2)))
106	105, 101	eqtrd 2778	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) + (𝐴↑2)) = 𝑄)
107	106	oveq1d 7290	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) + (𝐴↑2)) · 𝐷) = (𝑄 · 𝐷))
108	104, 107	eqtr3d 2780	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) · 𝐷) + ((𝐴↑2) · 𝐷)) = (𝑄 · 𝐷))
109	103, 108	oveq12d 7293	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) + (((𝐵↑2) · 𝐷) + ((𝐴↑2) · 𝐷))) = ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)))
110	96, 109	eqtrd 2778	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) + ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷))) = ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)))
111	110	oveq1d 7290	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) + ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷))) / (𝑄↑2)) = (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)))
112	26, 78, 19	adddid 10999	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝑄 · ((𝐶↑2) + 𝐷)) = ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)))
113	112	eqcomd 2744	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) = (𝑄 · ((𝐶↑2) + 𝐷)))
114	26	sqvald 13861	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝑄↑2) = (𝑄 · 𝑄))
115	113, 114	oveq12d 7293	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)) = ((𝑄 · ((𝐶↑2) + 𝐷)) / (𝑄 · 𝑄)))
116	78, 19	addcld 10994	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐶↑2) + 𝐷) ∈ ℂ)
117	116, 26, 26, 32, 32	divcan5d 11777	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝑄 · ((𝐶↑2) + 𝐷)) / (𝑄 · 𝑄)) = (((𝐶↑2) + 𝐷) / 𝑄))
118	115, 117	eqtrd 2778	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)) = (((𝐶↑2) + 𝐷) / 𝑄))
119	16	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)))
120	119	oveq2d 7291	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐶↑2) + 𝐷) = ((𝐶↑2) + (((𝑅↑2) · 𝑄) − (𝐶↑2))))
121		rpcn 12740	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℂ)
122	121	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷) → 𝑅 ∈ ℂ)
123	122	3ad2ant3 1134	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝑅 ∈ ℂ)
124	123	sqcld 13862	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝑅↑2) ∈ ℂ)
125	124, 26	mulcld 10995	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝑅↑2) · 𝑄) ∈ ℂ)
126	78, 125	pncan3d 11335	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐶↑2) + (((𝑅↑2) · 𝑄) − (𝐶↑2))) = ((𝑅↑2) · 𝑄))
127	120, 126	eqtrd 2778	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐶↑2) + 𝐷) = ((𝑅↑2) · 𝑄))
128	116, 124, 26, 32	divmul3d 11785	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐶↑2) + 𝐷) / 𝑄) = (𝑅↑2) ↔ ((𝐶↑2) + 𝐷) = ((𝑅↑2) · 𝑄)))
129	127, 128	mpbird 256	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐶↑2) + 𝐷) / 𝑄) = (𝑅↑2))
130	118, 129	eqtrd 2778	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)) = (𝑅↑2))
131	111, 130	eqtrd 2778	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) + ((((𝐵↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷))) / (𝑄↑2)) = (𝑅↑2))
132	76, 95, 131	3eqtr2d 2784	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2))
133	3, 22, 26, 32	divassd 11786	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) / 𝑄) = (𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
134	3, 7, 21	adddid 10999	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) = ((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))))
135	1	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
136	4	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
137	135, 135, 136	mulassd 10998	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐴) · 𝐶) = (𝐴 · (𝐴 · 𝐶)))
138	135	sqvald 13861	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) = (𝐴 · 𝐴))
139	138	eqcomd 2744	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐴) = (𝐴↑2))
140	139	oveq1d 7290	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐴) · 𝐶) = ((𝐴↑2) · 𝐶))
141	137, 140	eqtr3d 2780	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐴 · 𝐶)) = ((𝐴↑2) · 𝐶))
142	141	3adant2 1130	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐴 · 𝐶)) = ((𝐴↑2) · 𝐶))
143	142	3ad2ant1 1132	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (𝐴 · 𝐶)) = ((𝐴↑2) · 𝐶))
144	3, 10, 20	mulassd 10998	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐵) · (√‘𝐷)) = (𝐴 · (𝐵 · (√‘𝐷))))
145	144	eqcomd 2744	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (𝐵 · (√‘𝐷))) = ((𝐴 · 𝐵) · (√‘𝐷)))
146	143, 145	oveq12d 7293	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (𝐴 · 𝐶)) + (𝐴 · (𝐵 · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))))
147	134, 146	eqtrd 2778	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))))
148	147	oveq1d 7290	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) + (𝐵 · (√‘𝐷)))) / 𝑄) = ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
149	133, 148	eqtr3d 2780	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) = ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
150	10, 53, 26, 32	divassd 11786	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄) = (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)))
151	10, 51, 52	subdid 11431	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) = ((𝐵 · (𝐵 · 𝐶)) − (𝐵 · (𝐴 · (√‘𝐷)))))
152		simpl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℝ)
153	152	recnd 11003	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
154		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
155	154	recnd 11003	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
156	153, 153, 155	mulassd 10998	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 · 𝐵) · 𝐶) = (𝐵 · (𝐵 · 𝐶)))
157	8	sqvald 13861	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ ℝ → (𝐵↑2) = (𝐵 · 𝐵))
158	157	eqcomd 2744	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ ℝ → (𝐵 · 𝐵) = (𝐵↑2))
159	158	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · 𝐵) = (𝐵↑2))
160	159	oveq1d 7290	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 · 𝐵) · 𝐶) = ((𝐵↑2) · 𝐶))
161	156, 160	eqtr3d 2780	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · (𝐵 · 𝐶)) = ((𝐵↑2) · 𝐶))
162	161	3adant1 1129	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · (𝐵 · 𝐶)) = ((𝐵↑2) · 𝐶))
163	162	3ad2ant1 1132	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · (𝐵 · 𝐶)) = ((𝐵↑2) · 𝐶))
164	10, 3, 20	mulassd 10998	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐴) · (√‘𝐷)) = (𝐵 · (𝐴 · (√‘𝐷))))
165	9, 2	mulcomd 10996	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · 𝐴) = (𝐴 · 𝐵))
166	165	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · 𝐴) = (𝐴 · 𝐵))
167	166	oveq1d 7290	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐴) · (√‘𝐷)) = ((𝐴 · 𝐵) · (√‘𝐷)))
168	164, 167	eqtr3d 2780	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · (𝐴 · (√‘𝐷))) = ((𝐴 · 𝐵) · (√‘𝐷)))
169	163, 168	oveq12d 7293	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · (𝐵 · 𝐶)) − (𝐵 · (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))))
170	151, 169	eqtrd 2778	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))))
171	170	oveq1d 7290	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · ((𝐵 · 𝐶) − (𝐴 · (√‘𝐷)))) / 𝑄) = ((((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
172	150, 171	eqtr3d 2780	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) = ((((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
173	149, 172	oveq12d 7293	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = (((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄) + ((((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄)))
174	77, 6	mulcld 10995	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · 𝐶) ∈ ℂ)
175	3, 10	mulcld 10995	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · 𝐵) ∈ ℂ)
176	175, 20	mulcld 10995	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐵) · (√‘𝐷)) ∈ ℂ)
177	174, 176	addcld 10994	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) ∈ ℂ)
178	84, 6	mulcld 10995	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵↑2) · 𝐶) ∈ ℂ)
179	178, 176	subcld 11332	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) ∈ ℂ)
180	177, 179, 26, 32	divdird 11789	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = (((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄) + ((((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄)))
181	174, 176, 178	ppncand 11372	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
182	77, 84, 6	adddird 11000	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) + (𝐵↑2)) · 𝐶) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
183	15	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → 𝑄 = ((𝐴↑2) + (𝐵↑2)))
184	183	eqcomd 2744	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) + (𝐵↑2)) = 𝑄)
185	184	oveq1d 7290	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) + (𝐵↑2)) · 𝐶) = (𝑄 · 𝐶))
186	181, 182, 185	3eqtr2d 2784	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) = (𝑄 · 𝐶))
187	177, 179	addcld 10994	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) ∈ ℂ)
188	187, 6, 26, 32	divmul2d 11784	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = 𝐶 ↔ ((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) = (𝑄 · 𝐶)))
189	186, 188	mpbird 256	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = 𝐶)
190	173, 180, 189	3eqtr2d 2784	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶)
191	132, 190	jca 512	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2) ∧ ((𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶))
192		oveq1 7282	. . . . . 6 ⊢ (𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) → (𝑋↑2) = ((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2))
193		oveq1 7282	. . . . . 6 ⊢ (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → (𝑌↑2) = ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2))
194	192, 193	oveqan12d 7294	. . . . 5 ⊢ ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → ((𝑋↑2) + (𝑌↑2)) = (((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)))
195	194	eqeq1d 2740	. . . 4 ⊢ ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ↔ (((((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2)))
196		oveq2 7283	. . . . . 6 ⊢ (𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) → (𝐴 · 𝑋) = (𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)))
197		oveq2 7283	. . . . . 6 ⊢ (𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) → (𝐵 · 𝑌) = (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)))
198	196, 197	oveqan12d 7294	. . . . 5 ⊢ ((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) → ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = ((𝐴 · (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄))))
199	198	eqeq1d 2740	. . . 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 11332	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ∈ ℂ)
203	202, 26, 32	sqdivd 13877	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) = ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))↑2) / (𝑄↑2)))
204		binom2sub 13935	. . . . . . . . . . 11 ⊢ (((𝐴 · 𝐶) ∈ ℂ ∧ (𝐵 · (√‘𝐷)) ∈ ℂ) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))↑2) = ((((𝐴 · 𝐶)↑2) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)))
205	35, 21, 204	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))↑2) = ((((𝐴 · 𝐶)↑2) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)))
206	39	oveq1d 7290	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶)↑2) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) = (((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))))
207	206, 46	oveq12d 7293	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶)↑2) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵 · (√‘𝐷))↑2)) = ((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)))
208	205, 207	eqtrd 2778	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))↑2) = ((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)))
209	208	oveq1d 7290	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))↑2) / (𝑄↑2)) = (((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)))
210	203, 209	eqtrd 2778	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) = (((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)))
211	51, 56	addcld 10994	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℂ)
212	211, 26, 32	sqdivd 13877	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2) = ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))↑2) / (𝑄↑2)))
213		binom2 13933	. . . . . . . . . . 11 ⊢ (((𝐵 · 𝐶) ∈ ℂ ∧ (𝐴 · (√‘𝐷)) ∈ ℂ) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))↑2) = ((((𝐵 · 𝐶)↑2) + (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)))
214	51, 56, 213	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))↑2) = ((((𝐵 · 𝐶)↑2) + (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)))
215	60, 67	oveq12d 7293	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶)↑2) + (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) = (((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))))
216	215, 71	oveq12d 7293	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶)↑2) + (2 · ((𝐵 · 𝐶) · (𝐴 · (√‘𝐷))))) + ((𝐴 · (√‘𝐷))↑2)) = ((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)))
217	214, 216	eqtrd 2778	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))↑2) = ((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)))
218	217	oveq1d 7290	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))↑2) / (𝑄↑2)) = (((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2)))
219	212, 218	eqtrd 2778	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2) = (((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2)))
220	210, 219	oveq12d 7293	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = ((((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) / (𝑄↑2)) + (((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) / (𝑄↑2))))
221	98, 78	mulcld 10995	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · (𝐶↑2)) ∈ ℂ)
222	35, 21	mulcld 10995	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))) ∈ ℂ)
223	80, 222	mulcld 10995	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))) ∈ ℂ)
224	221, 223	subcld 11332	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) ∈ ℂ)
225	224, 85	addcld 10994	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) ∈ ℂ)
226	87, 223	addcld 10994	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) ∈ ℂ)
227	98, 19	mulcld 10995	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴↑2) · 𝐷) ∈ ℂ)
228	226, 227	addcld 10994	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷)) ∈ ℂ)
229	225, 228, 91, 94	divdird 11789	. . . . . 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 11203	. . . . . . . 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 11359	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) = (((𝐴↑2) · (𝐶↑2)) + ((𝐵↑2) · (𝐶↑2))))
232	231, 99, 102	3eqtr2d 2784	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) = (𝑄 · (𝐶↑2)))
233	232, 108	oveq12d 7293	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + (((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷)))))) + (((𝐵↑2) · 𝐷) + ((𝐴↑2) · 𝐷))) = ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)))
234	230, 233	eqtrd 2778	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) + ((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷))) = ((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)))
235	234	oveq1d 7290	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴↑2) · (𝐶↑2)) − (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐵↑2) · 𝐷)) + ((((𝐵↑2) · (𝐶↑2)) + (2 · ((𝐴 · 𝐶) · (𝐵 · (√‘𝐷))))) + ((𝐴↑2) · 𝐷))) / (𝑄↑2)) = (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)))
236	220, 229, 235	3eqtr2d 2784	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (((𝑄 · (𝐶↑2)) + (𝑄 · 𝐷)) / (𝑄↑2)))
237	236, 130	eqtrd 2778	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2))
238		simp1 1135	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ)
239		simp3 1137	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
240	238, 239	remulcld 11005	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐶) ∈ ℝ)
241	240	recnd 11003	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐶) ∈ ℂ)
242	241	3ad2ant1 1132	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · 𝐶) ∈ ℂ)
243	242, 21	subcld 11332	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) ∈ ℂ)
244	3, 243, 26, 32	divassd 11786	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) / 𝑄) = (𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
245	3, 242, 21	subdid 11431	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) = ((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))))
246	143, 145	oveq12d 7293	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (𝐴 · 𝐶)) − (𝐴 · (𝐵 · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))))
247	245, 246	eqtrd 2778	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))))
248	247	oveq1d 7290	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · ((𝐴 · 𝐶) − (𝐵 · (√‘𝐷)))) / 𝑄) = ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
249	244, 248	eqtr3d 2780	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) = ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
250	51, 52	addcld 10994	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) ∈ ℂ)
251	10, 250, 26, 32	divassd 11786	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄) = (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
252	10, 51, 52	adddid 10999	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) = ((𝐵 · (𝐵 · 𝐶)) + (𝐵 · (𝐴 · (√‘𝐷)))))
253	163, 168	oveq12d 7293	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · (𝐵 · 𝐶)) + (𝐵 · (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))))
254	252, 253	eqtrd 2778	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) = (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))))
255	254	oveq1d 7290	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐵 · ((𝐵 · 𝐶) + (𝐴 · (√‘𝐷)))) / 𝑄) = ((((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
256	251, 255	eqtr3d 2780	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) = ((((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄))
257	249, 256	oveq12d 7293	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = (((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄) + ((((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄)))
258	174, 176	subcld 11332	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) ∈ ℂ)
259	178, 176	addcld 10994	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) ∈ ℂ)
260	258, 259, 26, 32	divdird 11789	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = (((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄) + ((((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷))) / 𝑄)))
261	174, 176, 178	nppcan3d 11359	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) = (((𝐴↑2) · 𝐶) + ((𝐵↑2) · 𝐶)))
262	261, 182, 185	3eqtr2d 2784	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) = (𝑄 · 𝐶))
263	258, 259	addcld 10994	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) ∈ ℂ)
264	263, 6, 26, 32	divmul2d 11784	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = 𝐶 ↔ ((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) = (𝑄 · 𝐶)))
265	262, 264	mpbird 256	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((((𝐴↑2) · 𝐶) − ((𝐴 · 𝐵) · (√‘𝐷))) + (((𝐵↑2) · 𝐶) + ((𝐴 · 𝐵) · (√‘𝐷)))) / 𝑄) = 𝐶)
266	257, 260, 265	3eqtr2d 2784	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶)
267	237, 266	jca 512	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → ((((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2) ∧ ((𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) = 𝐶))
268		oveq1 7282	. . . . . 6 ⊢ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) → (𝑋↑2) = ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2))
269		oveq1 7282	. . . . . 6 ⊢ (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → (𝑌↑2) = ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2))
270	268, 269	oveqan12d 7294	. . . . 5 ⊢ ((𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → ((𝑋↑2) + (𝑌↑2)) = (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)))
271	270	eqeq1d 2740	. . . 4 ⊢ ((𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ↔ (((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)↑2) + ((((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)↑2)) = (𝑅↑2)))
272		oveq2 7283	. . . . . 6 ⊢ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) → (𝐴 · 𝑋) = (𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)))
273		oveq2 7283	. . . . . 6 ⊢ (𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) → (𝐵 · 𝑌) = (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))
274	272, 273	oveqan12d 7294	. . . . 5 ⊢ ((𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)) → ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = ((𝐴 · (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)) + (𝐵 · (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))
275	274	eqeq1d 2740	. . . 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 856	1 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷)) → (((𝑋 = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ (𝑋 = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ 𝑌 = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))) → (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∨ wo 844 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 class class class wbr 5074 ‘cfv 6433 (class class class)co 7275 ℂcc 10869 ℝcr 10870 0cc0 10871 + caddc 10874 · cmul 10876 < clt 11009 ≤ cle 11010 − cmin 11205 / cdiv 11632 2c2 12028 ℤcz 12319 ℝ⁺crp 12730 ↑cexp 13782 √csqrt 14944

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 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 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-er 8498 df-en 8734 df-dom 8735 df-sdom 8736 df-sup 9201 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-n0 12234 df-z 12320 df-uz 12583 df-rp 12731 df-seq 13722 df-exp 13783 df-cj 14810 df-re 14811 df-im 14812 df-sqrt 14946 df-abs 14947

This theorem is referenced by: itsclc0xyqsolb 46116

W3C validator