Theorem constrrtcc 33726

Description: In the construction of constructible numbers, circle-circle intersections are roots of a quadratic equation. (Contributed by Thierry Arnoux, 6-Jul-2025.)

Hypotheses

Ref	Expression
constrrtcc.s	⊢ (𝜑 → 𝑆 ⊆ ℂ)
constrrtcc.a	⊢ (𝜑 → 𝐴 ∈ 𝑆)
constrrtcc.b	⊢ (𝜑 → 𝐵 ∈ 𝑆)
constrrtcc.c	⊢ (𝜑 → 𝐶 ∈ 𝑆)
constrrtcc.d	⊢ (𝜑 → 𝐷 ∈ 𝑆)
constrrtcc.e	⊢ (𝜑 → 𝐸 ∈ 𝑆)
constrrtcc.f	⊢ (𝜑 → 𝐹 ∈ 𝑆)
constrrtcc.x	⊢ (𝜑 → 𝑋 ∈ ℂ)
constrrtcc.1	⊢ (𝜑 → 𝐴 ≠ 𝐷)
constrrtcc.2	⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶)))
constrrtcc.3	⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹)))
constrrtcc.4	⊢ 𝑃 = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶)))
constrrtcc.5	⊢ 𝑄 = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹)))
constrrtcc.m	⊢ 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴)))
constrrtcc.n	⊢ 𝑁 = -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴)))

Assertion

Ref	Expression
constrrtcc	⊢ (𝜑 → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)

Proof of Theorem constrrtcc

Step	Hyp	Ref	Expression
1		constrrtcc.m	. . . . . . . . . 10 ⊢ 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴)))
2	1	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))))
3		constrrtcc.5	. . . . . . . . . . . . . . . 16 ⊢ 𝑄 = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹)))
4		constrrtcc.s	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
5		constrrtcc.e	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐸 ∈ 𝑆)
6	4, 5	sseldd 4009	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐸 ∈ ℂ)
7		constrrtcc.f	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
8	4, 7	sseldd 4009	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹 ∈ ℂ)
9	6, 8	subcld 11647	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 − 𝐹) ∈ ℂ)
10	9	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐸 − 𝐹) ∈ ℂ)
11	10	absvalsqd 15491	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((abs‘(𝐸 − 𝐹))↑2) = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))))
12	3, 11	eqtr4id 2799	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑄 = ((abs‘(𝐸 − 𝐹))↑2))
13		constrrtcc.x	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑋 ∈ ℂ)
14	13	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑋 ∈ ℂ)
15		constrrtcc.a	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
16	4, 15	sseldd 4009	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ ℂ)
17	16	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐴 ∈ ℂ)
18	13, 16	subcld 11647	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑋 − 𝐴) ∈ ℂ)
19	18	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑋 − 𝐴) ∈ ℂ)
20		constrrtcc.2	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶)))
21	20	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶)))
22		constrrtcc.b	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐵 ∈ 𝑆)
23	4, 22	sseldd 4009	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐵 ∈ ℂ)
24	23	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 ∈ ℂ)
25		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 = 𝐶)
26	24, 25	subeq0bd 11716	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐵 − 𝐶) = 0)
27	26	abs00bd 15340	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝐵 − 𝐶)) = 0)
28	21, 27	eqtrd 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝑋 − 𝐴)) = 0)
29	19, 28	abs00d 15495	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑋 − 𝐴) = 0)
30	14, 17, 29	subeq0d 11655	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑋 = 𝐴)
31	30	fvoveq1d 7470	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐴 − 𝐷)))
32		constrrtcc.3	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹)))
33	32	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹)))
34		constrrtcc.d	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐷 ∈ 𝑆)
35	4, 34	sseldd 4009	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ∈ ℂ)
36	35	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐷 ∈ ℂ)
37	17, 36	abssubd 15502	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝐴 − 𝐷)) = (abs‘(𝐷 − 𝐴)))
38	31, 33, 37	3eqtr3d 2788	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝐸 − 𝐹)) = (abs‘(𝐷 − 𝐴)))
39	38	oveq1d 7463	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((abs‘(𝐸 − 𝐹))↑2) = ((abs‘(𝐷 − 𝐴))↑2))
40	35, 16	subcld 11647	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐷 − 𝐴) ∈ ℂ)
41	40	absvalsqd 15491	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((abs‘(𝐷 − 𝐴))↑2) = ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))))
42	41	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((abs‘(𝐷 − 𝐴))↑2) = ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))))
43	12, 39, 42	3eqtrd 2784	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑄 = ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))))
44	43	oveq1d 7463	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((∗‘𝐷) · (𝐷 + 𝐴))))
45		constrrtcc.4	. . . . . . . . . . . . . . 15 ⊢ 𝑃 = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶)))
46	26	oveq1d 7463	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))) = (0 · (∗‘(𝐵 − 𝐶))))
47		constrrtcc.c	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐶 ∈ 𝑆)
48	4, 47	sseldd 4009	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐶 ∈ ℂ)
49	23, 48	subcld 11647	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℂ)
50	49	cjcld 15245	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (∗‘(𝐵 − 𝐶)) ∈ ℂ)
51	50	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (∗‘(𝐵 − 𝐶)) ∈ ℂ)
52	51	mul02d 11488	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (0 · (∗‘(𝐵 − 𝐶))) = 0)
53	46, 52	eqtrd 2780	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))) = 0)
54	45, 53	eqtrid 2792	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 = 0)
55	54	oveq1d 7463	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) = (0 − ((∗‘𝐴) · (𝐷 + 𝐴))))
56	44, 55	oveq12d 7466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) = ((((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((∗‘𝐷) · (𝐷 + 𝐴))) − (0 − ((∗‘𝐴) · (𝐷 + 𝐴)))))
57	40	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐷 − 𝐴) ∈ ℂ)
58	57	cjcld 15245	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (∗‘(𝐷 − 𝐴)) ∈ ℂ)
59	57, 58	mulcld 11310	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) ∈ ℂ)
60	36	cjcld 15245	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (∗‘𝐷) ∈ ℂ)
61	36, 17	addcld 11309	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐷 + 𝐴) ∈ ℂ)
62	60, 61	mulcld 11310	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((∗‘𝐷) · (𝐷 + 𝐴)) ∈ ℂ)
63		0cnd 11283	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 0 ∈ ℂ)
64	17	cjcld 15245	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (∗‘𝐴) ∈ ℂ)
65	64, 61	mulcld 11310	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((∗‘𝐴) · (𝐷 + 𝐴)) ∈ ℂ)
66	59, 62, 63, 65	sub4d 11696	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((∗‘𝐷) · (𝐷 + 𝐴))) − (0 − ((∗‘𝐴) · (𝐷 + 𝐴)))) = ((((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − 0) − (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴)))))
67	59	subid1d 11636	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − 0) = ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))))
68	35, 16	cjsubd 32755	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘(𝐷 − 𝐴)) = ((∗‘𝐷) − (∗‘𝐴)))
69	68	oveq1d 7463	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘(𝐷 − 𝐴)) · (𝐷 + 𝐴)) = (((∗‘𝐷) − (∗‘𝐴)) · (𝐷 + 𝐴)))
70	40	cjcld 15245	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘(𝐷 − 𝐴)) ∈ ℂ)
71	35, 16	addcld 11309	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 + 𝐴) ∈ ℂ)
72	70, 71	mulcomd 11311	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘(𝐷 − 𝐴)) · (𝐷 + 𝐴)) = ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴))))
73	35	cjcld 15245	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘𝐷) ∈ ℂ)
74	16	cjcld 15245	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘𝐴) ∈ ℂ)
75	73, 74, 71	subdird 11747	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝐷 + 𝐴)) = (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴))))
76	69, 72, 75	3eqtr3rd 2789	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴))) = ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴))))
77	76	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴))) = ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴))))
78	67, 77	oveq12d 7466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − 0) − (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴)))) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴)))))
79	56, 66, 78	3eqtrd 2784	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴)))))
80	57, 61, 58	subdird 11747	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) − (𝐷 + 𝐴)) · (∗‘(𝐷 − 𝐴))) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴)))))
81	61, 57	negsubdi2d 11663	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -((𝐷 + 𝐴) − (𝐷 − 𝐴)) = ((𝐷 − 𝐴) − (𝐷 + 𝐴)))
82	36, 17, 17	pnncand 11686	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 + 𝐴) − (𝐷 − 𝐴)) = (𝐴 + 𝐴))
83	17	2timesd 12536	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (2 · 𝐴) = (𝐴 + 𝐴))
84	82, 83	eqtr4d 2783	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 + 𝐴) − (𝐷 − 𝐴)) = (2 · 𝐴))
85	84	negeqd 11530	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -((𝐷 + 𝐴) − (𝐷 − 𝐴)) = -(2 · 𝐴))
86	81, 85	eqtr3d 2782	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 − 𝐴) − (𝐷 + 𝐴)) = -(2 · 𝐴))
87	86	oveq1d 7463	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) − (𝐷 + 𝐴)) · (∗‘(𝐷 − 𝐴))) = (-(2 · 𝐴) · (∗‘(𝐷 − 𝐴))))
88	79, 80, 87	3eqtr2rd 2787	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (-(2 · 𝐴) · (∗‘(𝐷 − 𝐴))) = ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))))
89	68	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (∗‘(𝐷 − 𝐴)) = ((∗‘𝐷) − (∗‘𝐴)))
90	88, 89	oveq12d 7466	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((-(2 · 𝐴) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))) = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))))
91		2cnd 12371	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 2 ∈ ℂ)
92	91, 17	mulcld 11310	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (2 · 𝐴) ∈ ℂ)
93	92	negcld 11634	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(2 · 𝐴) ∈ ℂ)
94		constrrtcc.1	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ≠ 𝐷)
95	94	necomd 3002	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ≠ 𝐴)
96	35, 16, 95	subne0d 11656	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷 − 𝐴) ≠ 0)
97	40, 96	cjne0d 15252	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘(𝐷 − 𝐴)) ≠ 0)
98	97	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (∗‘(𝐷 − 𝐴)) ≠ 0)
99	93, 58, 98	divcan4d 12076	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((-(2 · 𝐴) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))) = -(2 · 𝐴))
100	2, 90, 99	3eqtr2d 2786	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑀 = -(2 · 𝐴))
101	100	oveq1d 7463	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑀 · 𝑋) = (-(2 · 𝐴) · 𝑋))
102	92, 14	mulneg1d 11743	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (-(2 · 𝐴) · 𝑋) = -((2 · 𝐴) · 𝑋))
103	91, 17, 14	mulassd 11313	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((2 · 𝐴) · 𝑋) = (2 · (𝐴 · 𝑋)))
104	17, 14	mulcomd 11311	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐴 · 𝑋) = (𝑋 · 𝐴))
105	104	oveq2d 7464	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (2 · (𝐴 · 𝑋)) = (2 · (𝑋 · 𝐴)))
106	103, 105	eqtrd 2780	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((2 · 𝐴) · 𝑋) = (2 · (𝑋 · 𝐴)))
107	106	negeqd 11530	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -((2 · 𝐴) · 𝑋) = -(2 · (𝑋 · 𝐴)))
108	101, 102, 107	3eqtrd 2784	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑀 · 𝑋) = -(2 · (𝑋 · 𝐴)))
109		constrrtcc.n	. . . . . . 7 ⊢ 𝑁 = -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴)))
110	17	sqcld 14194	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐴↑2) ∈ ℂ)
111	54	oveq1d 7463	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑃 · 𝐷) = (0 · 𝐷))
112	36	mul02d 11488	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (0 · 𝐷) = 0)
113	111, 112	eqtrd 2780	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑃 · 𝐷) = 0)
114	113	oveq2d 7464	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) = (((∗‘𝐴) · (𝐷 · 𝐴)) − 0))
115	36, 17	mulcld 11310	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐷 · 𝐴) ∈ ℂ)
116	64, 115	mulcld 11310	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((∗‘𝐴) · (𝐷 · 𝐴)) ∈ ℂ)
117	116	subid1d 11636	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐴) · (𝐷 · 𝐴)) − 0) = ((∗‘𝐴) · (𝐷 · 𝐴)))
118	114, 117	eqtrd 2780	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) = ((∗‘𝐴) · (𝐷 · 𝐴)))
119	43	oveq1d 7463	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑄 · 𝐴) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴))
120	119	oveq2d 7464	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)) = (((∗‘𝐷) · (𝐷 · 𝐴)) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴)))
121	118, 120	oveq12d 7466	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = (((∗‘𝐴) · (𝐷 · 𝐴)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴))))
122	60, 115	mulcld 11310	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((∗‘𝐷) · (𝐷 · 𝐴)) ∈ ℂ)
123	59, 17	mulcld 11310	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴) ∈ ℂ)
124	116, 122, 123	subsubd 11675	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐴) · (𝐷 · 𝐴)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) + (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴)))
125	68	negeqd 11530	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → -(∗‘(𝐷 − 𝐴)) = -((∗‘𝐷) − (∗‘𝐴)))
126	73, 74	negsubdi2d 11663	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → -((∗‘𝐷) − (∗‘𝐴)) = ((∗‘𝐴) − (∗‘𝐷)))
127	125, 126	eqtr2d 2781	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐴) − (∗‘𝐷)) = -(∗‘(𝐷 − 𝐴)))
128	127	oveq1d 7463	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐴) − (∗‘𝐷)) · (𝐷 · 𝐴)) = (-(∗‘(𝐷 − 𝐴)) · (𝐷 · 𝐴)))
129	35, 16	mulcld 11310	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 · 𝐴) ∈ ℂ)
130	74, 73, 129	subdird 11747	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐴) − (∗‘𝐷)) · (𝐷 · 𝐴)) = (((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))))
131	70, 129	mulcomd 11311	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((∗‘(𝐷 − 𝐴)) · (𝐷 · 𝐴)) = ((𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))))
132	131	negeqd 11530	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → -((∗‘(𝐷 − 𝐴)) · (𝐷 · 𝐴)) = -((𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))))
133	70, 129	mulneg1d 11743	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (-(∗‘(𝐷 − 𝐴)) · (𝐷 · 𝐴)) = -((∗‘(𝐷 − 𝐴)) · (𝐷 · 𝐴)))
134	129, 70	mulneg1d 11743	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (-(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))) = -((𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))))
135	132, 133, 134	3eqtr4d 2790	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (-(∗‘(𝐷 − 𝐴)) · (𝐷 · 𝐴)) = (-(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))))
136	128, 130, 135	3eqtr3d 2788	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) = (-(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))))
137	136	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) = (-(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))))
138	57, 58, 17	mul32d 11500	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴) = (((𝐷 − 𝐴) · 𝐴) · (∗‘(𝐷 − 𝐴))))
139	36, 17, 17	subdird 11747	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 − 𝐴) · 𝐴) = ((𝐷 · 𝐴) − (𝐴 · 𝐴)))
140	17	sqvald 14193	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐴↑2) = (𝐴 · 𝐴))
141	140	oveq2d 7464	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 · 𝐴) − (𝐴↑2)) = ((𝐷 · 𝐴) − (𝐴 · 𝐴)))
142	139, 141	eqtr4d 2783	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 − 𝐴) · 𝐴) = ((𝐷 · 𝐴) − (𝐴↑2)))
143	142	oveq1d 7463	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) · 𝐴) · (∗‘(𝐷 − 𝐴))) = (((𝐷 · 𝐴) − (𝐴↑2)) · (∗‘(𝐷 − 𝐴))))
144	138, 143	eqtrd 2780	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴) = (((𝐷 · 𝐴) − (𝐴↑2)) · (∗‘(𝐷 − 𝐴))))
145	137, 144	oveq12d 7466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) + (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴)) = ((-(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))) + (((𝐷 · 𝐴) − (𝐴↑2)) · (∗‘(𝐷 − 𝐴)))))
146	115	negcld 11634	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(𝐷 · 𝐴) ∈ ℂ)
147	115, 110	subcld 11647	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 · 𝐴) − (𝐴↑2)) ∈ ℂ)
148	146, 147, 58	adddird 11315	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((-(𝐷 · 𝐴) + ((𝐷 · 𝐴) − (𝐴↑2))) · (∗‘(𝐷 − 𝐴))) = ((-(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))) + (((𝐷 · 𝐴) − (𝐴↑2)) · (∗‘(𝐷 − 𝐴)))))
149	115	subidd 11635	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 · 𝐴) − (𝐷 · 𝐴)) = 0)
150	149	oveq1d 7463	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 · 𝐴) − (𝐷 · 𝐴)) − (𝐴↑2)) = (0 − (𝐴↑2)))
151	146, 147	addcomd 11492	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (-(𝐷 · 𝐴) + ((𝐷 · 𝐴) − (𝐴↑2))) = (((𝐷 · 𝐴) − (𝐴↑2)) + -(𝐷 · 𝐴)))
152	147, 115	negsubd 11653	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 · 𝐴) − (𝐴↑2)) + -(𝐷 · 𝐴)) = (((𝐷 · 𝐴) − (𝐴↑2)) − (𝐷 · 𝐴)))
153	115, 110, 115	sub32d 11679	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 · 𝐴) − (𝐴↑2)) − (𝐷 · 𝐴)) = (((𝐷 · 𝐴) − (𝐷 · 𝐴)) − (𝐴↑2)))
154	151, 152, 153	3eqtrd 2784	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (-(𝐷 · 𝐴) + ((𝐷 · 𝐴) − (𝐴↑2))) = (((𝐷 · 𝐴) − (𝐷 · 𝐴)) − (𝐴↑2)))
155		df-neg 11523	. . . . . . . . . . . . . . 15 ⊢ -(𝐴↑2) = (0 − (𝐴↑2))
156	155	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(𝐴↑2) = (0 − (𝐴↑2)))
157	150, 154, 156	3eqtr4d 2790	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (-(𝐷 · 𝐴) + ((𝐷 · 𝐴) − (𝐴↑2))) = -(𝐴↑2))
158	157	oveq1d 7463	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((-(𝐷 · 𝐴) + ((𝐷 · 𝐴) − (𝐴↑2))) · (∗‘(𝐷 − 𝐴))) = (-(𝐴↑2) · (∗‘(𝐷 − 𝐴))))
159	145, 148, 158	3eqtr2d 2786	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) + (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴)) = (-(𝐴↑2) · (∗‘(𝐷 − 𝐴))))
160	121, 124, 159	3eqtrd 2784	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = (-(𝐴↑2) · (∗‘(𝐷 − 𝐴))))
161	89	eqcomd 2746	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((∗‘𝐷) − (∗‘𝐴)) = (∗‘(𝐷 − 𝐴)))
162	160, 161	oveq12d 7466	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = ((-(𝐴↑2) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))))
163	110	negcld 11634	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(𝐴↑2) ∈ ℂ)
164	163, 58, 98	divcan4d 12076	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((-(𝐴↑2) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))) = -(𝐴↑2))
165	162, 164	eqtr2d 2781	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(𝐴↑2) = (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))))
166	110, 165	negcon1ad 11642	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = (𝐴↑2))
167	109, 166	eqtrid 2792	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑁 = (𝐴↑2))
168	108, 167	oveq12d 7466	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑀 · 𝑋) + 𝑁) = (-(2 · (𝑋 · 𝐴)) + (𝐴↑2)))
169	168	oveq2d 7464	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = ((𝑋↑2) + (-(2 · (𝑋 · 𝐴)) + (𝐴↑2))))
170	14	sqcld 14194	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑋↑2) ∈ ℂ)
171	14, 17	mulcld 11310	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑋 · 𝐴) ∈ ℂ)
172	91, 171	mulcld 11310	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (2 · (𝑋 · 𝐴)) ∈ ℂ)
173	172	negcld 11634	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(2 · (𝑋 · 𝐴)) ∈ ℂ)
174	170, 173, 110	addassd 11312	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝑋↑2) + -(2 · (𝑋 · 𝐴))) + (𝐴↑2)) = ((𝑋↑2) + (-(2 · (𝑋 · 𝐴)) + (𝐴↑2))))
175	170, 172	negsubd 11653	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑋↑2) + -(2 · (𝑋 · 𝐴))) = ((𝑋↑2) − (2 · (𝑋 · 𝐴))))
176	175	oveq1d 7463	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝑋↑2) + -(2 · (𝑋 · 𝐴))) + (𝐴↑2)) = (((𝑋↑2) − (2 · (𝑋 · 𝐴))) + (𝐴↑2)))
177	169, 174, 176	3eqtr2d 2786	. . 3 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = (((𝑋↑2) − (2 · (𝑋 · 𝐴))) + (𝐴↑2)))
178		binom2sub 14269	. . . 4 ⊢ ((𝑋 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑋 − 𝐴)↑2) = (((𝑋↑2) − (2 · (𝑋 · 𝐴))) + (𝐴↑2)))
179	14, 17, 178	syl2anc 583	. . 3 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑋 − 𝐴)↑2) = (((𝑋↑2) − (2 · (𝑋 · 𝐴))) + (𝐴↑2)))
180	29	sq0id 14243	. . 3 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑋 − 𝐴)↑2) = 0)
181	177, 179, 180	3eqtr2d 2786	. 2 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)
182	1	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))))
183	6	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝐸 ∈ ℂ)
184		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝐸 = 𝐹)
185	183, 184	subeq0bd 11716	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐸 − 𝐹) = 0)
186	185	oveq1d 7463	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))) = (0 · (∗‘(𝐸 − 𝐹))))
187	9	cjcld 15245	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (∗‘(𝐸 − 𝐹)) ∈ ℂ)
188	187	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (∗‘(𝐸 − 𝐹)) ∈ ℂ)
189	188	mul02d 11488	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (0 · (∗‘(𝐸 − 𝐹))) = 0)
190	186, 189	eqtrd 2780	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))) = 0)
191	3, 190	eqtrid 2792	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑄 = 0)
192	191	oveq1d 7463	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) = (0 − ((∗‘𝐷) · (𝐷 + 𝐴))))
193	49	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐵 − 𝐶) ∈ ℂ)
194	193	absvalsqd 15491	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((abs‘(𝐵 − 𝐶))↑2) = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))))
195	45, 194	eqtr4id 2799	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑃 = ((abs‘(𝐵 − 𝐶))↑2))
196	20	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶)))
197	13	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑋 ∈ ℂ)
198	35	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝐷 ∈ ℂ)
199	13, 35	subcld 11647	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑋 − 𝐷) ∈ ℂ)
200	199	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑋 − 𝐷) ∈ ℂ)
201	32	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹)))
202	185	abs00bd 15340	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (abs‘(𝐸 − 𝐹)) = 0)
203	201, 202	eqtrd 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (abs‘(𝑋 − 𝐷)) = 0)
204	200, 203	abs00d 15495	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑋 − 𝐷) = 0)
205	197, 198, 204	subeq0d 11655	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑋 = 𝐷)
206	205	fvoveq1d 7470	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐷 − 𝐴)))
207	196, 206	eqtr3d 2782	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (abs‘(𝐵 − 𝐶)) = (abs‘(𝐷 − 𝐴)))
208	207	oveq1d 7463	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((abs‘(𝐵 − 𝐶))↑2) = ((abs‘(𝐷 − 𝐴))↑2))
209	41	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((abs‘(𝐷 − 𝐴))↑2) = ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))))
210	195, 208, 209	3eqtrd 2784	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑃 = ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))))
211	210	oveq1d 7463	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((∗‘𝐴) · (𝐷 + 𝐴))))
212	192, 211	oveq12d 7466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) = ((0 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((∗‘𝐴) · (𝐷 + 𝐴)))))
213		0cnd 11283	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 0 ∈ ℂ)
214	198	cjcld 15245	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (∗‘𝐷) ∈ ℂ)
215	16	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝐴 ∈ ℂ)
216	198, 215	addcld 11309	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷 + 𝐴) ∈ ℂ)
217	214, 216	mulcld 11310	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((∗‘𝐷) · (𝐷 + 𝐴)) ∈ ℂ)
218	40	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷 − 𝐴) ∈ ℂ)
219	218	cjcld 15245	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (∗‘(𝐷 − 𝐴)) ∈ ℂ)
220	218, 219	mulcld 11310	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) ∈ ℂ)
221	215	cjcld 15245	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (∗‘𝐴) ∈ ℂ)
222	221, 216	mulcld 11310	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((∗‘𝐴) · (𝐷 + 𝐴)) ∈ ℂ)
223	213, 217, 220, 222	sub4d 11696	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((0 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((∗‘𝐴) · (𝐷 + 𝐴)))) = ((0 − ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴)))) − (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴)))))
224	218, 219	mulneg1d 11743	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (-(𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) = -((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))))
225	198, 215	negsubdi2d 11663	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(𝐷 − 𝐴) = (𝐴 − 𝐷))
226	225	oveq1d 7463	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (-(𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) = ((𝐴 − 𝐷) · (∗‘(𝐷 − 𝐴))))
227		df-neg 11523	. . . . . . . . . . . . . . 15 ⊢ -((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) = (0 − ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))))
228	227	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) = (0 − ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴)))))
229	224, 226, 228	3eqtr3rd 2789	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (0 − ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴)))) = ((𝐴 − 𝐷) · (∗‘(𝐷 − 𝐴))))
230	76	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴))) = ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴))))
231	229, 230	oveq12d 7466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((0 − ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴)))) − (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴)))) = (((𝐴 − 𝐷) · (∗‘(𝐷 − 𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴)))))
232	212, 223, 231	3eqtrd 2784	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) = (((𝐴 − 𝐷) · (∗‘(𝐷 − 𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴)))))
233	215, 198	subcld 11647	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐴 − 𝐷) ∈ ℂ)
234	233, 216, 219	subdird 11747	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝐴 − 𝐷) − (𝐷 + 𝐴)) · (∗‘(𝐷 − 𝐴))) = (((𝐴 − 𝐷) · (∗‘(𝐷 − 𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴)))))
235	216, 233	negsubdi2d 11663	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -((𝐷 + 𝐴) − (𝐴 − 𝐷)) = ((𝐴 − 𝐷) − (𝐷 + 𝐴)))
236	198	2timesd 12536	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (2 · 𝐷) = (𝐷 + 𝐷))
237	215, 198, 198	pnncand 11686	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐴 + 𝐷) − (𝐴 − 𝐷)) = (𝐷 + 𝐷))
238	215, 198	addcomd 11492	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐴 + 𝐷) = (𝐷 + 𝐴))
239	238	oveq1d 7463	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐴 + 𝐷) − (𝐴 − 𝐷)) = ((𝐷 + 𝐴) − (𝐴 − 𝐷)))
240	236, 237, 239	3eqtr2rd 2787	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷 + 𝐴) − (𝐴 − 𝐷)) = (2 · 𝐷))
241	240	negeqd 11530	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -((𝐷 + 𝐴) − (𝐴 − 𝐷)) = -(2 · 𝐷))
242	235, 241	eqtr3d 2782	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐴 − 𝐷) − (𝐷 + 𝐴)) = -(2 · 𝐷))
243	242	oveq1d 7463	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝐴 − 𝐷) − (𝐷 + 𝐴)) · (∗‘(𝐷 − 𝐴))) = (-(2 · 𝐷) · (∗‘(𝐷 − 𝐴))))
244	232, 234, 243	3eqtr2rd 2787	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (-(2 · 𝐷) · (∗‘(𝐷 − 𝐴))) = ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))))
245	68	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (∗‘(𝐷 − 𝐴)) = ((∗‘𝐷) − (∗‘𝐴)))
246	244, 245	oveq12d 7466	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((-(2 · 𝐷) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))) = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))))
247		2cnd 12371	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 2 ∈ ℂ)
248	247, 198	mulcld 11310	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (2 · 𝐷) ∈ ℂ)
249	248	negcld 11634	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(2 · 𝐷) ∈ ℂ)
250	97	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (∗‘(𝐷 − 𝐴)) ≠ 0)
251	249, 219, 250	divcan4d 12076	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((-(2 · 𝐷) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))) = -(2 · 𝐷))
252	182, 246, 251	3eqtr2d 2786	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑀 = -(2 · 𝐷))
253	252	oveq1d 7463	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑀 · 𝑋) = (-(2 · 𝐷) · 𝑋))
254	248, 197	mulneg1d 11743	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (-(2 · 𝐷) · 𝑋) = -((2 · 𝐷) · 𝑋))
255	247, 198, 197	mulassd 11313	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((2 · 𝐷) · 𝑋) = (2 · (𝐷 · 𝑋)))
256	198, 197	mulcomd 11311	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷 · 𝑋) = (𝑋 · 𝐷))
257	256	oveq2d 7464	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (2 · (𝐷 · 𝑋)) = (2 · (𝑋 · 𝐷)))
258	255, 257	eqtrd 2780	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((2 · 𝐷) · 𝑋) = (2 · (𝑋 · 𝐷)))
259	258	negeqd 11530	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -((2 · 𝐷) · 𝑋) = -(2 · (𝑋 · 𝐷)))
260	253, 254, 259	3eqtrd 2784	. . . . . 6 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑀 · 𝑋) = -(2 · (𝑋 · 𝐷)))
261	198	sqcld 14194	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷↑2) ∈ ℂ)
262	210	oveq1d 7463	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑃 · 𝐷) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷))
263	262	oveq2d 7464	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) = (((∗‘𝐴) · (𝐷 · 𝐴)) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷)))
264	191	oveq1d 7463	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑄 · 𝐴) = (0 · 𝐴))
265	215	mul02d 11488	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (0 · 𝐴) = 0)
266	264, 265	eqtrd 2780	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑄 · 𝐴) = 0)
267	266	oveq2d 7464	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)) = (((∗‘𝐷) · (𝐷 · 𝐴)) − 0))
268	198, 215	mulcld 11310	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷 · 𝐴) ∈ ℂ)
269	214, 268	mulcld 11310	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((∗‘𝐷) · (𝐷 · 𝐴)) ∈ ℂ)
270	269	subid1d 11636	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((∗‘𝐷) · (𝐷 · 𝐴)) − 0) = ((∗‘𝐷) · (𝐷 · 𝐴)))
271	267, 270	eqtrd 2780	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)) = ((∗‘𝐷) · (𝐷 · 𝐴)))
272	263, 271	oveq12d 7466	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷)) − ((∗‘𝐷) · (𝐷 · 𝐴))))
273	221, 268	mulcld 11310	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((∗‘𝐴) · (𝐷 · 𝐴)) ∈ ℂ)
274	220, 198	mulcld 11310	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷) ∈ ℂ)
275	273, 274, 269	sub32d 11679	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷)) − ((∗‘𝐷) · (𝐷 · 𝐴))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷)))
276	136	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) = (-(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))))
277	218, 219, 198	mul32d 11500	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷) = (((𝐷 − 𝐴) · 𝐷) · (∗‘(𝐷 − 𝐴))))
278	198, 215, 198	subdird 11747	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷 − 𝐴) · 𝐷) = ((𝐷 · 𝐷) − (𝐴 · 𝐷)))
279	198	sqvald 14193	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷↑2) = (𝐷 · 𝐷))
280	198, 215	mulcomd 11311	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷 · 𝐴) = (𝐴 · 𝐷))
281	279, 280	oveq12d 7466	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷↑2) − (𝐷 · 𝐴)) = ((𝐷 · 𝐷) − (𝐴 · 𝐷)))
282	278, 281	eqtr4d 2783	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷 − 𝐴) · 𝐷) = ((𝐷↑2) − (𝐷 · 𝐴)))
283	282	oveq1d 7463	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝐷 − 𝐴) · 𝐷) · (∗‘(𝐷 − 𝐴))) = (((𝐷↑2) − (𝐷 · 𝐴)) · (∗‘(𝐷 − 𝐴))))
284	277, 283	eqtrd 2780	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷) = (((𝐷↑2) − (𝐷 · 𝐴)) · (∗‘(𝐷 − 𝐴))))
285	276, 284	oveq12d 7466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷)) = ((-(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))) − (((𝐷↑2) − (𝐷 · 𝐴)) · (∗‘(𝐷 − 𝐴)))))
286	268	negcld 11634	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(𝐷 · 𝐴) ∈ ℂ)
287	261, 268	subcld 11647	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷↑2) − (𝐷 · 𝐴)) ∈ ℂ)
288	286, 287, 219	subdird 11747	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((-(𝐷 · 𝐴) − ((𝐷↑2) − (𝐷 · 𝐴))) · (∗‘(𝐷 − 𝐴))) = ((-(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))) − (((𝐷↑2) − (𝐷 · 𝐴)) · (∗‘(𝐷 − 𝐴)))))
289	286, 268	addcomd 11492	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (-(𝐷 · 𝐴) + (𝐷 · 𝐴)) = ((𝐷 · 𝐴) + -(𝐷 · 𝐴)))
290	268, 268	negsubd 11653	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷 · 𝐴) + -(𝐷 · 𝐴)) = ((𝐷 · 𝐴) − (𝐷 · 𝐴)))
291	268	subidd 11635	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷 · 𝐴) − (𝐷 · 𝐴)) = 0)
292	289, 290, 291	3eqtrd 2784	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (-(𝐷 · 𝐴) + (𝐷 · 𝐴)) = 0)
293	292	oveq1d 7463	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((-(𝐷 · 𝐴) + (𝐷 · 𝐴)) − (𝐷↑2)) = (0 − (𝐷↑2)))
294	286, 261, 268	subsub3d 11677	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (-(𝐷 · 𝐴) − ((𝐷↑2) − (𝐷 · 𝐴))) = ((-(𝐷 · 𝐴) + (𝐷 · 𝐴)) − (𝐷↑2)))
295		df-neg 11523	. . . . . . . . . . . . . . 15 ⊢ -(𝐷↑2) = (0 − (𝐷↑2))
296	295	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(𝐷↑2) = (0 − (𝐷↑2)))
297	293, 294, 296	3eqtr4d 2790	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (-(𝐷 · 𝐴) − ((𝐷↑2) − (𝐷 · 𝐴))) = -(𝐷↑2))
298	297	oveq1d 7463	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((-(𝐷 · 𝐴) − ((𝐷↑2) − (𝐷 · 𝐴))) · (∗‘(𝐷 − 𝐴))) = (-(𝐷↑2) · (∗‘(𝐷 − 𝐴))))
299	285, 288, 298	3eqtr2d 2786	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷)) = (-(𝐷↑2) · (∗‘(𝐷 − 𝐴))))
300	272, 275, 299	3eqtrd 2784	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = (-(𝐷↑2) · (∗‘(𝐷 − 𝐴))))
301	245	eqcomd 2746	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((∗‘𝐷) − (∗‘𝐴)) = (∗‘(𝐷 − 𝐴)))
302	300, 301	oveq12d 7466	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = ((-(𝐷↑2) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))))
303	261	negcld 11634	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(𝐷↑2) ∈ ℂ)
304	303, 219, 250	divcan4d 12076	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((-(𝐷↑2) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))) = -(𝐷↑2))
305	302, 304	eqtr2d 2781	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(𝐷↑2) = (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))))
306	261, 305	negcon1ad 11642	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = (𝐷↑2))
307	109, 306	eqtrid 2792	. . . . . 6 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑁 = (𝐷↑2))
308	260, 307	oveq12d 7466	. . . . 5 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑀 · 𝑋) + 𝑁) = (-(2 · (𝑋 · 𝐷)) + (𝐷↑2)))
309	308	oveq2d 7464	. . . 4 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = ((𝑋↑2) + (-(2 · (𝑋 · 𝐷)) + (𝐷↑2))))
310	197	sqcld 14194	. . . . 5 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑋↑2) ∈ ℂ)
311	197, 198	mulcld 11310	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑋 · 𝐷) ∈ ℂ)
312	247, 311	mulcld 11310	. . . . . 6 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (2 · (𝑋 · 𝐷)) ∈ ℂ)
313	312	negcld 11634	. . . . 5 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(2 · (𝑋 · 𝐷)) ∈ ℂ)
314	310, 313, 261	addassd 11312	. . . 4 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝑋↑2) + -(2 · (𝑋 · 𝐷))) + (𝐷↑2)) = ((𝑋↑2) + (-(2 · (𝑋 · 𝐷)) + (𝐷↑2))))
315	310, 312	negsubd 11653	. . . . 5 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑋↑2) + -(2 · (𝑋 · 𝐷))) = ((𝑋↑2) − (2 · (𝑋 · 𝐷))))
316	315	oveq1d 7463	. . . 4 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝑋↑2) + -(2 · (𝑋 · 𝐷))) + (𝐷↑2)) = (((𝑋↑2) − (2 · (𝑋 · 𝐷))) + (𝐷↑2)))
317	309, 314, 316	3eqtr2d 2786	. . 3 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = (((𝑋↑2) − (2 · (𝑋 · 𝐷))) + (𝐷↑2)))
318		binom2sub 14269	. . . 4 ⊢ ((𝑋 ∈ ℂ ∧ 𝐷 ∈ ℂ) → ((𝑋 − 𝐷)↑2) = (((𝑋↑2) − (2 · (𝑋 · 𝐷))) + (𝐷↑2)))
319	197, 198, 318	syl2anc 583	. . 3 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑋 − 𝐷)↑2) = (((𝑋↑2) − (2 · (𝑋 · 𝐷))) + (𝐷↑2)))
320	204	sq0id 14243	. . 3 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑋 − 𝐷)↑2) = 0)
321	317, 319, 320	3eqtr2d 2786	. 2 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)
322	4	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝑆 ⊆ ℂ)
323	15	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐴 ∈ 𝑆)
324	22	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐵 ∈ 𝑆)
325	47	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐶 ∈ 𝑆)
326	34	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐷 ∈ 𝑆)
327	5	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐸 ∈ 𝑆)
328	7	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐹 ∈ 𝑆)
329	13	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝑋 ∈ ℂ)
330	94	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐴 ≠ 𝐷)
331	20	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶)))
332	32	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹)))
333		simprl 770	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐵 ≠ 𝐶)
334		simprr 772	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐸 ≠ 𝐹)
335	322, 323, 324, 325, 326, 327, 328, 329, 330, 331, 332, 45, 3, 1, 109, 333, 334	constrrtcclem 33725	. 2 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)
336	181, 321, 335	pm2.61da2ne 3036	1 ⊢ (𝜑 → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108   ≠ wne 2946   ⊆ wss 3976  ‘cfv 6573  (class class class)co 7448  ℂcc 11182  0cc0 11184   + caddc 11187   · cmul 11189   − cmin 11520  -cneg 11521   / cdiv 11947  2c2 12348  ↑cexp 14112  ∗ccj 15145  abscabs 15283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-sup 9511  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-3 12357  df-n0 12554  df-z 12640  df-uz 12904  df-rp 13058  df-seq 14053  df-exp 14113  df-cj 15148  df-re 15149  df-im 15150  df-sqrt 15284  df-abs 15285

This theorem is referenced by:  constrfin  33736  constrelextdg2  33737