Theorem constrrtcc 34367

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 3932	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐸 ∈ ℂ)
7		constrrtcc.f	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
8	4, 7	sseldd 3932	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹 ∈ ℂ)
9	6, 8	subcld 11669	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 − 𝐹) ∈ ℂ)
10	9	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐸 − 𝐹) ∈ ℂ)
11	10	absvalsqd 15612	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((abs‘(𝐸 − 𝐹))↑2) = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))))
12	3, 11	eqtr4id 2815	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑄 = ((abs‘(𝐸 − 𝐹))↑2))
13		constrrtcc.x	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑋 ∈ ℂ)
14	13	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑋 ∈ ℂ)
15		constrrtcc.a	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
16	4, 15	sseldd 3932	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ ℂ)
17	16	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐴 ∈ ℂ)
18	13, 16	subcld 11669	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑋 − 𝐴) ∈ ℂ)
19	18	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑋 − 𝐴) ∈ ℂ)
20		constrrtcc.2	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶)))
21	20	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶)))
22		constrrtcc.b	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐵 ∈ 𝑆)
23	4, 22	sseldd 3932	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐵 ∈ ℂ)
24	23	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 ∈ ℂ)
25		simpr 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 = 𝐶)
26	24, 25	subeq0bd 11742	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐵 − 𝐶) = 0)
27	26	abs00bd 15458	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝐵 − 𝐶)) = 0)
28	21, 27	eqtrd 2796	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝑋 − 𝐴)) = 0)
29	19, 28	abs00d 15616	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑋 − 𝐴) = 0)
30	14, 17, 29	subeq0d 11678	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑋 = 𝐴)
31	30	fvoveq1d 7442	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐴 − 𝐷)))
32		constrrtcc.3	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹)))
33	32	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹)))
34		constrrtcc.d	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐷 ∈ 𝑆)
35	4, 34	sseldd 3932	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ∈ ℂ)
36	35	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐷 ∈ ℂ)
37	17, 36	abssubd 15623	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝐴 − 𝐷)) = (abs‘(𝐷 − 𝐴)))
38	31, 33, 37	3eqtr3d 2804	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝐸 − 𝐹)) = (abs‘(𝐷 − 𝐴)))
39	38	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((abs‘(𝐸 − 𝐹))↑2) = ((abs‘(𝐷 − 𝐴))↑2))
40	35, 16	subcld 11669	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐷 − 𝐴) ∈ ℂ)
41	40	absvalsqd 15612	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((abs‘(𝐷 − 𝐴))↑2) = ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))))
42	41	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((abs‘(𝐷 − 𝐴))↑2) = ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))))
43	12, 39, 42	3eqtrd 2800	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑄 = ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))))
44	43	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((∗‘𝐷) · (𝐷 + 𝐴))))
45		constrrtcc.4	. . . . . . . . . . . . . . 15 ⊢ 𝑃 = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶)))
46	26	oveq1d 7435	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))) = (0 · (∗‘(𝐵 − 𝐶))))
47		constrrtcc.c	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐶 ∈ 𝑆)
48	4, 47	sseldd 3932	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐶 ∈ ℂ)
49	23, 48	subcld 11669	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℂ)
50	49	cjcld 15363	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (∗‘(𝐵 − 𝐶)) ∈ ℂ)
51	50	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (∗‘(𝐵 − 𝐶)) ∈ ℂ)
52	51	mul02d 11508	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (0 · (∗‘(𝐵 − 𝐶))) = 0)
53	46, 52	eqtrd 2796	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))) = 0)
54	45, 53	eqtrid 2808	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 = 0)
55	54	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) = (0 − ((∗‘𝐴) · (𝐷 + 𝐴))))
56	44, 55	oveq12d 7438	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) = ((((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((∗‘𝐷) · (𝐷 + 𝐴))) − (0 − ((∗‘𝐴) · (𝐷 + 𝐴)))))
57	40	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐷 − 𝐴) ∈ ℂ)
58	57	cjcld 15363	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (∗‘(𝐷 − 𝐴)) ∈ ℂ)
59	57, 58	mulcld 11329	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) ∈ ℂ)
60	36	cjcld 15363	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (∗‘𝐷) ∈ ℂ)
61	36, 17	addcld 11328	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐷 + 𝐴) ∈ ℂ)
62	60, 61	mulcld 11329	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((∗‘𝐷) · (𝐷 + 𝐴)) ∈ ℂ)
63		0cnd 11299	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 0 ∈ ℂ)
64	17	cjcld 15363	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (∗‘𝐴) ∈ ℂ)
65	64, 61	mulcld 11329	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((∗‘𝐴) · (𝐷 + 𝐴)) ∈ ℂ)
66	59, 62, 63, 65	sub4d 11718	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((∗‘𝐷) · (𝐷 + 𝐴))) − (0 − ((∗‘𝐴) · (𝐷 + 𝐴)))) = ((((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − 0) − (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴)))))
67	59	subid1d 11658	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − 0) = ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))))
68	35, 16	cjsubd 33334	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘(𝐷 − 𝐴)) = ((∗‘𝐷) − (∗‘𝐴)))
69	68	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘(𝐷 − 𝐴)) · (𝐷 + 𝐴)) = (((∗‘𝐷) − (∗‘𝐴)) · (𝐷 + 𝐴)))
70	40	cjcld 15363	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘(𝐷 − 𝐴)) ∈ ℂ)
71	35, 16	addcld 11328	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 + 𝐴) ∈ ℂ)
72	70, 71	mulcomd 11330	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘(𝐷 − 𝐴)) · (𝐷 + 𝐴)) = ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴))))
73	35	cjcld 15363	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘𝐷) ∈ ℂ)
74	16	cjcld 15363	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘𝐴) ∈ ℂ)
75	73, 74, 71	subdird 11773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝐷 + 𝐴)) = (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴))))
76	69, 72, 75	3eqtr3rd 2805	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴))) = ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴))))
77	76	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴))) = ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴))))
78	67, 77	oveq12d 7438	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − 0) − (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴)))) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴)))))
79	56, 66, 78	3eqtrd 2800	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴)))))
80	57, 61, 58	subdird 11773	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) − (𝐷 + 𝐴)) · (∗‘(𝐷 − 𝐴))) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴)))))
81	61, 57	negsubdi2d 11685	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -((𝐷 + 𝐴) − (𝐷 − 𝐴)) = ((𝐷 − 𝐴) − (𝐷 + 𝐴)))
82	36, 17, 17	pnncand 11708	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 + 𝐴) − (𝐷 − 𝐴)) = (𝐴 + 𝐴))
83	17	2timesd 12589	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (2 · 𝐴) = (𝐴 + 𝐴))
84	82, 83	eqtr4d 2799	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 + 𝐴) − (𝐷 − 𝐴)) = (2 · 𝐴))
85	84	negeqd 11551	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -((𝐷 + 𝐴) − (𝐷 − 𝐴)) = -(2 · 𝐴))
86	81, 85	eqtr3d 2798	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 − 𝐴) − (𝐷 + 𝐴)) = -(2 · 𝐴))
87	86	oveq1d 7435	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) − (𝐷 + 𝐴)) · (∗‘(𝐷 − 𝐴))) = ( -(2 · 𝐴) · (∗‘(𝐷 − 𝐴))))
88	79, 80, 87	3eqtr2rd 2803	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ( -(2 · 𝐴) · (∗‘(𝐷 − 𝐴))) = ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))))
89	68	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (∗‘(𝐷 − 𝐴)) = ((∗‘𝐷) − (∗‘𝐴)))
90	88, 89	oveq12d 7438	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (( -(2 · 𝐴) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))) = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))))
91		2cnd 12421	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 2 ∈ ℂ)
92	91, 17	mulcld 11329	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (2 · 𝐴) ∈ ℂ)
93	92	negcld 11656	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(2 · 𝐴) ∈ ℂ)
94		constrrtcc.1	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ≠ 𝐷)
95	94	necomd 3011	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ≠ 𝐴)
96	35, 16, 95	subne0d 11679	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷 − 𝐴) ≠ 0)
97	40, 96	cjne0d 15370	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘(𝐷 − 𝐴)) ≠ 0)
98	97	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (∗‘(𝐷 − 𝐴)) ≠ 0)
99	93, 58, 98	divcan4d 12099	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (( -(2 · 𝐴) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))) = -(2 · 𝐴))
100	2, 90, 99	3eqtr2d 2802	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑀 = -(2 · 𝐴))
101	100	oveq1d 7435	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑀 · 𝑋) = ( -(2 · 𝐴) · 𝑋))
102	92, 14	mulneg1d 11769	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ( -(2 · 𝐴) · 𝑋) = -((2 · 𝐴) · 𝑋))
103	91, 17, 14	mulassd 11332	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((2 · 𝐴) · 𝑋) = (2 · (𝐴 · 𝑋)))
104	17, 14	mulcomd 11330	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐴 · 𝑋) = (𝑋 · 𝐴))
105	104	oveq2d 7436	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (2 · (𝐴 · 𝑋)) = (2 · (𝑋 · 𝐴)))
106	103, 105	eqtrd 2796	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((2 · 𝐴) · 𝑋) = (2 · (𝑋 · 𝐴)))
107	106	negeqd 11551	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -((2 · 𝐴) · 𝑋) = -(2 · (𝑋 · 𝐴)))
108	101, 102, 107	3eqtrd 2800	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑀 · 𝑋) = -(2 · (𝑋 · 𝐴)))
109		constrrtcc.n	. . . . . . 7 ⊢ 𝑁 = -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴)))
110	17	sqcld 14287	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐴↑2) ∈ ℂ)
111	54	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑃 · 𝐷) = (0 · 𝐷))
112	36	mul02d 11508	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (0 · 𝐷) = 0)
113	111, 112	eqtrd 2796	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑃 · 𝐷) = 0)
114	113	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) = (((∗‘𝐴) · (𝐷 · 𝐴)) − 0))
115	36, 17	mulcld 11329	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐷 · 𝐴) ∈ ℂ)
116	64, 115	mulcld 11329	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((∗‘𝐴) · (𝐷 · 𝐴)) ∈ ℂ)
117	116	subid1d 11658	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐴) · (𝐷 · 𝐴)) − 0) = ((∗‘𝐴) · (𝐷 · 𝐴)))
118	114, 117	eqtrd 2796	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) = ((∗‘𝐴) · (𝐷 · 𝐴)))
119	43	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑄 · 𝐴) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴))
120	119	oveq2d 7436	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)) = (((∗‘𝐷) · (𝐷 · 𝐴)) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴)))
121	118, 120	oveq12d 7438	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = (((∗‘𝐴) · (𝐷 · 𝐴)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴))))
122	60, 115	mulcld 11329	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((∗‘𝐷) · (𝐷 · 𝐴)) ∈ ℂ)
123	59, 17	mulcld 11329	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴) ∈ ℂ)
124	116, 122, 123	subsubd 11697	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐴) · (𝐷 · 𝐴)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) + (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴)))
125	68	negeqd 11551	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → -(∗‘(𝐷 − 𝐴)) = -((∗‘𝐷) − (∗‘𝐴)))
126	73, 74	negsubdi2d 11685	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → -((∗‘𝐷) − (∗‘𝐴)) = ((∗‘𝐴) − (∗‘𝐷)))
127	125, 126	eqtr2d 2797	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐴) − (∗‘𝐷)) = -(∗‘(𝐷 − 𝐴)))
128	127	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐴) − (∗‘𝐷)) · (𝐷 · 𝐴)) = ( -(∗‘(𝐷 − 𝐴)) · (𝐷 · 𝐴)))
129	35, 16	mulcld 11329	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 · 𝐴) ∈ ℂ)
130	74, 73, 129	subdird 11773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐴) − (∗‘𝐷)) · (𝐷 · 𝐴)) = (((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))))
131	70, 129	mulcomd 11330	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((∗‘(𝐷 − 𝐴)) · (𝐷 · 𝐴)) = ((𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))))
132	131	negeqd 11551	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → -((∗‘(𝐷 − 𝐴)) · (𝐷 · 𝐴)) = -((𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))))
133	70, 129	mulneg1d 11769	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( -(∗‘(𝐷 − 𝐴)) · (𝐷 · 𝐴)) = -((∗‘(𝐷 − 𝐴)) · (𝐷 · 𝐴)))
134	129, 70	mulneg1d 11769	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( -(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))) = -((𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))))
135	132, 133, 134	3eqtr4d 2806	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ( -(∗‘(𝐷 − 𝐴)) · (𝐷 · 𝐴)) = ( -(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))))
136	128, 130, 135	3eqtr3d 2804	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) = ( -(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))))
137	136	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) = ( -(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))))
138	57, 58, 17	mul32d 11520	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴) = (((𝐷 − 𝐴) · 𝐴) · (∗‘(𝐷 − 𝐴))))
139	36, 17, 17	subdird 11773	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 − 𝐴) · 𝐴) = ((𝐷 · 𝐴) − (𝐴 · 𝐴)))
140	17	sqvald 14286	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐴↑2) = (𝐴 · 𝐴))
141	140	oveq2d 7436	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 · 𝐴) − (𝐴↑2)) = ((𝐷 · 𝐴) − (𝐴 · 𝐴)))
142	139, 141	eqtr4d 2799	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 − 𝐴) · 𝐴) = ((𝐷 · 𝐴) − (𝐴↑2)))
143	142	oveq1d 7435	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) · 𝐴) · (∗‘(𝐷 − 𝐴))) = (((𝐷 · 𝐴) − (𝐴↑2)) · (∗‘(𝐷 − 𝐴))))
144	138, 143	eqtrd 2796	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴) = (((𝐷 · 𝐴) − (𝐴↑2)) · (∗‘(𝐷 − 𝐴))))
145	137, 144	oveq12d 7438	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) + (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴)) = (( -(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))) + (((𝐷 · 𝐴) − (𝐴↑2)) · (∗‘(𝐷 − 𝐴)))))
146	115	negcld 11656	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(𝐷 · 𝐴) ∈ ℂ)
147	115, 110	subcld 11669	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 · 𝐴) − (𝐴↑2)) ∈ ℂ)
148	146, 147, 58	adddird 11334	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (( -(𝐷 · 𝐴) + ((𝐷 · 𝐴) − (𝐴↑2))) · (∗‘(𝐷 − 𝐴))) = (( -(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))) + (((𝐷 · 𝐴) − (𝐴↑2)) · (∗‘(𝐷 − 𝐴)))))
149	115	subidd 11657	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 · 𝐴) − (𝐷 · 𝐴)) = 0)
150	149	oveq1d 7435	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 · 𝐴) − (𝐷 · 𝐴)) − (𝐴↑2)) = (0 − (𝐴↑2)))
151	146, 147	addcomd 11512	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ( -(𝐷 · 𝐴) + ((𝐷 · 𝐴) − (𝐴↑2))) = (((𝐷 · 𝐴) − (𝐴↑2)) + -(𝐷 · 𝐴)))
152	147, 115	negsubd 11675	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 · 𝐴) − (𝐴↑2)) + -(𝐷 · 𝐴)) = (((𝐷 · 𝐴) − (𝐴↑2)) − (𝐷 · 𝐴)))
153	115, 110, 115	sub32d 11701	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 · 𝐴) − (𝐴↑2)) − (𝐷 · 𝐴)) = (((𝐷 · 𝐴) − (𝐷 · 𝐴)) − (𝐴↑2)))
154	151, 152, 153	3eqtrd 2800	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ( -(𝐷 · 𝐴) + ((𝐷 · 𝐴) − (𝐴↑2))) = (((𝐷 · 𝐴) − (𝐷 · 𝐴)) − (𝐴↑2)))
155		df-neg 11544	. . . . . . . . . . . . . . 15 ⊢ -(𝐴↑2) = (0 − (𝐴↑2))
156	155	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(𝐴↑2) = (0 − (𝐴↑2)))
157	150, 154, 156	3eqtr4d 2806	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ( -(𝐷 · 𝐴) + ((𝐷 · 𝐴) − (𝐴↑2))) = -(𝐴↑2))
158	157	oveq1d 7435	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (( -(𝐷 · 𝐴) + ((𝐷 · 𝐴) − (𝐴↑2))) · (∗‘(𝐷 − 𝐴))) = ( -(𝐴↑2) · (∗‘(𝐷 − 𝐴))))
159	145, 148, 158	3eqtr2d 2802	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) + (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴)) = ( -(𝐴↑2) · (∗‘(𝐷 − 𝐴))))
160	121, 124, 159	3eqtrd 2800	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = ( -(𝐴↑2) · (∗‘(𝐷 − 𝐴))))
161	89	eqcomd 2767	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((∗‘𝐷) − (∗‘𝐴)) = (∗‘(𝐷 − 𝐴)))
162	160, 161	oveq12d 7438	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = (( -(𝐴↑2) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))))
163	110	negcld 11656	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(𝐴↑2) ∈ ℂ)
164	163, 58, 98	divcan4d 12099	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (( -(𝐴↑2) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))) = -(𝐴↑2))
165	162, 164	eqtr2d 2797	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(𝐴↑2) = (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))))
166	110, 165	negcon1ad 11664	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = (𝐴↑2))
167	109, 166	eqtrid 2808	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑁 = (𝐴↑2))
168	108, 167	oveq12d 7438	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑀 · 𝑋) + 𝑁) = ( -(2 · (𝑋 · 𝐴)) + (𝐴↑2)))
169	168	oveq2d 7436	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = ((𝑋↑2) + ( -(2 · (𝑋 · 𝐴)) + (𝐴↑2))))
170	14	sqcld 14287	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑋↑2) ∈ ℂ)
171	14, 17	mulcld 11329	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑋 · 𝐴) ∈ ℂ)
172	91, 171	mulcld 11329	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (2 · (𝑋 · 𝐴)) ∈ ℂ)
173	172	negcld 11656	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(2 · (𝑋 · 𝐴)) ∈ ℂ)
174	170, 173, 110	addassd 11331	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝑋↑2) + -(2 · (𝑋 · 𝐴))) + (𝐴↑2)) = ((𝑋↑2) + ( -(2 · (𝑋 · 𝐴)) + (𝐴↑2))))
175	170, 172	negsubd 11675	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑋↑2) + -(2 · (𝑋 · 𝐴))) = ((𝑋↑2) − (2 · (𝑋 · 𝐴))))
176	175	oveq1d 7435	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝑋↑2) + -(2 · (𝑋 · 𝐴))) + (𝐴↑2)) = (((𝑋↑2) − (2 · (𝑋 · 𝐴))) + (𝐴↑2)))
177	169, 174, 176	3eqtr2d 2802	. . 3 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = (((𝑋↑2) − (2 · (𝑋 · 𝐴))) + (𝐴↑2)))
178		binom2sub 14364	. . . 4 ⊢ ((𝑋 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑋 − 𝐴)↑2) = (((𝑋↑2) − (2 · (𝑋 · 𝐴))) + (𝐴↑2)))
179	14, 17, 178	syl2anc 596	. . 3 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑋 − 𝐴)↑2) = (((𝑋↑2) − (2 · (𝑋 · 𝐴))) + (𝐴↑2)))
180	29	sq0id 14337	. . 3 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑋 − 𝐴)↑2) = 0)
181	177, 179, 180	3eqtr2d 2802	. 2 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)
182	1	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))))
183	6	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝐸 ∈ ℂ)
184		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝐸 = 𝐹)
185	183, 184	subeq0bd 11742	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐸 − 𝐹) = 0)
186	185	oveq1d 7435	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))) = (0 · (∗‘(𝐸 − 𝐹))))
187	9	cjcld 15363	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (∗‘(𝐸 − 𝐹)) ∈ ℂ)
188	187	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (∗‘(𝐸 − 𝐹)) ∈ ℂ)
189	188	mul02d 11508	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (0 · (∗‘(𝐸 − 𝐹))) = 0)
190	186, 189	eqtrd 2796	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))) = 0)
191	3, 190	eqtrid 2808	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑄 = 0)
192	191	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) = (0 − ((∗‘𝐷) · (𝐷 + 𝐴))))
193	49	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐵 − 𝐶) ∈ ℂ)
194	193	absvalsqd 15612	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((abs‘(𝐵 − 𝐶))↑2) = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))))
195	45, 194	eqtr4id 2815	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑃 = ((abs‘(𝐵 − 𝐶))↑2))
196	20	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶)))
197	13	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑋 ∈ ℂ)
198	35	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝐷 ∈ ℂ)
199	13, 35	subcld 11669	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑋 − 𝐷) ∈ ℂ)
200	199	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑋 − 𝐷) ∈ ℂ)
201	32	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹)))
202	185	abs00bd 15458	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (abs‘(𝐸 − 𝐹)) = 0)
203	201, 202	eqtrd 2796	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (abs‘(𝑋 − 𝐷)) = 0)
204	200, 203	abs00d 15616	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑋 − 𝐷) = 0)
205	197, 198, 204	subeq0d 11678	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑋 = 𝐷)
206	205	fvoveq1d 7442	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐷 − 𝐴)))
207	196, 206	eqtr3d 2798	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (abs‘(𝐵 − 𝐶)) = (abs‘(𝐷 − 𝐴)))
208	207	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((abs‘(𝐵 − 𝐶))↑2) = ((abs‘(𝐷 − 𝐴))↑2))
209	41	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((abs‘(𝐷 − 𝐴))↑2) = ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))))
210	195, 208, 209	3eqtrd 2800	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑃 = ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))))
211	210	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((∗‘𝐴) · (𝐷 + 𝐴))))
212	192, 211	oveq12d 7438	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) = ((0 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((∗‘𝐴) · (𝐷 + 𝐴)))))
213		0cnd 11299	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 0 ∈ ℂ)
214	198	cjcld 15363	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (∗‘𝐷) ∈ ℂ)
215	16	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝐴 ∈ ℂ)
216	198, 215	addcld 11328	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷 + 𝐴) ∈ ℂ)
217	214, 216	mulcld 11329	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((∗‘𝐷) · (𝐷 + 𝐴)) ∈ ℂ)
218	40	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷 − 𝐴) ∈ ℂ)
219	218	cjcld 15363	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (∗‘(𝐷 − 𝐴)) ∈ ℂ)
220	218, 219	mulcld 11329	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) ∈ ℂ)
221	215	cjcld 15363	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (∗‘𝐴) ∈ ℂ)
222	221, 216	mulcld 11329	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((∗‘𝐴) · (𝐷 + 𝐴)) ∈ ℂ)
223	213, 217, 220, 222	sub4d 11718	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((0 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((∗‘𝐴) · (𝐷 + 𝐴)))) = ((0 − ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴)))) − (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴)))))
224	218, 219	mulneg1d 11769	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ( -(𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) = -((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))))
225	198, 215	negsubdi2d 11685	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(𝐷 − 𝐴) = (𝐴 − 𝐷))
226	225	oveq1d 7435	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ( -(𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) = ((𝐴 − 𝐷) · (∗‘(𝐷 − 𝐴))))
227		df-neg 11544	. . . . . . . . . . . . . . 15 ⊢ -((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) = (0 − ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))))
228	227	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) = (0 − ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴)))))
229	224, 226, 228	3eqtr3rd 2805	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (0 − ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴)))) = ((𝐴 − 𝐷) · (∗‘(𝐷 − 𝐴))))
230	76	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴))) = ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴))))
231	229, 230	oveq12d 7438	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((0 − ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴)))) − (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴)))) = (((𝐴 − 𝐷) · (∗‘(𝐷 − 𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴)))))
232	212, 223, 231	3eqtrd 2800	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) = (((𝐴 − 𝐷) · (∗‘(𝐷 − 𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴)))))
233	215, 198	subcld 11669	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐴 − 𝐷) ∈ ℂ)
234	233, 216, 219	subdird 11773	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝐴 − 𝐷) − (𝐷 + 𝐴)) · (∗‘(𝐷 − 𝐴))) = (((𝐴 − 𝐷) · (∗‘(𝐷 − 𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴)))))
235	216, 233	negsubdi2d 11685	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -((𝐷 + 𝐴) − (𝐴 − 𝐷)) = ((𝐴 − 𝐷) − (𝐷 + 𝐴)))
236	198	2timesd 12589	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (2 · 𝐷) = (𝐷 + 𝐷))
237	215, 198, 198	pnncand 11708	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐴 + 𝐷) − (𝐴 − 𝐷)) = (𝐷 + 𝐷))
238	215, 198	addcomd 11512	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐴 + 𝐷) = (𝐷 + 𝐴))
239	238	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐴 + 𝐷) − (𝐴 − 𝐷)) = ((𝐷 + 𝐴) − (𝐴 − 𝐷)))
240	236, 237, 239	3eqtr2rd 2803	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷 + 𝐴) − (𝐴 − 𝐷)) = (2 · 𝐷))
241	240	negeqd 11551	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -((𝐷 + 𝐴) − (𝐴 − 𝐷)) = -(2 · 𝐷))
242	235, 241	eqtr3d 2798	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐴 − 𝐷) − (𝐷 + 𝐴)) = -(2 · 𝐷))
243	242	oveq1d 7435	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝐴 − 𝐷) − (𝐷 + 𝐴)) · (∗‘(𝐷 − 𝐴))) = ( -(2 · 𝐷) · (∗‘(𝐷 − 𝐴))))
244	232, 234, 243	3eqtr2rd 2803	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ( -(2 · 𝐷) · (∗‘(𝐷 − 𝐴))) = ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))))
245	68	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (∗‘(𝐷 − 𝐴)) = ((∗‘𝐷) − (∗‘𝐴)))
246	244, 245	oveq12d 7438	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (( -(2 · 𝐷) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))) = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))))
247		2cnd 12421	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 2 ∈ ℂ)
248	247, 198	mulcld 11329	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (2 · 𝐷) ∈ ℂ)
249	248	negcld 11656	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(2 · 𝐷) ∈ ℂ)
250	97	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (∗‘(𝐷 − 𝐴)) ≠ 0)
251	249, 219, 250	divcan4d 12099	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (( -(2 · 𝐷) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))) = -(2 · 𝐷))
252	182, 246, 251	3eqtr2d 2802	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑀 = -(2 · 𝐷))
253	252	oveq1d 7435	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑀 · 𝑋) = ( -(2 · 𝐷) · 𝑋))
254	248, 197	mulneg1d 11769	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ( -(2 · 𝐷) · 𝑋) = -((2 · 𝐷) · 𝑋))
255	247, 198, 197	mulassd 11332	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((2 · 𝐷) · 𝑋) = (2 · (𝐷 · 𝑋)))
256	198, 197	mulcomd 11330	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷 · 𝑋) = (𝑋 · 𝐷))
257	256	oveq2d 7436	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (2 · (𝐷 · 𝑋)) = (2 · (𝑋 · 𝐷)))
258	255, 257	eqtrd 2796	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((2 · 𝐷) · 𝑋) = (2 · (𝑋 · 𝐷)))
259	258	negeqd 11551	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -((2 · 𝐷) · 𝑋) = -(2 · (𝑋 · 𝐷)))
260	253, 254, 259	3eqtrd 2800	. . . . . 6 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑀 · 𝑋) = -(2 · (𝑋 · 𝐷)))
261	198	sqcld 14287	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷↑2) ∈ ℂ)
262	210	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑃 · 𝐷) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷))
263	262	oveq2d 7436	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) = (((∗‘𝐴) · (𝐷 · 𝐴)) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷)))
264	191	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑄 · 𝐴) = (0 · 𝐴))
265	215	mul02d 11508	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (0 · 𝐴) = 0)
266	264, 265	eqtrd 2796	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑄 · 𝐴) = 0)
267	266	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)) = (((∗‘𝐷) · (𝐷 · 𝐴)) − 0))
268	198, 215	mulcld 11329	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷 · 𝐴) ∈ ℂ)
269	214, 268	mulcld 11329	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((∗‘𝐷) · (𝐷 · 𝐴)) ∈ ℂ)
270	269	subid1d 11658	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((∗‘𝐷) · (𝐷 · 𝐴)) − 0) = ((∗‘𝐷) · (𝐷 · 𝐴)))
271	267, 270	eqtrd 2796	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)) = ((∗‘𝐷) · (𝐷 · 𝐴)))
272	263, 271	oveq12d 7438	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷)) − ((∗‘𝐷) · (𝐷 · 𝐴))))
273	221, 268	mulcld 11329	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((∗‘𝐴) · (𝐷 · 𝐴)) ∈ ℂ)
274	220, 198	mulcld 11329	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷) ∈ ℂ)
275	273, 274, 269	sub32d 11701	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷)) − ((∗‘𝐷) · (𝐷 · 𝐴))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷)))
276	136	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) = ( -(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))))
277	218, 219, 198	mul32d 11520	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷) = (((𝐷 − 𝐴) · 𝐷) · (∗‘(𝐷 − 𝐴))))
278	198, 215, 198	subdird 11773	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷 − 𝐴) · 𝐷) = ((𝐷 · 𝐷) − (𝐴 · 𝐷)))
279	198	sqvald 14286	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷↑2) = (𝐷 · 𝐷))
280	198, 215	mulcomd 11330	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷 · 𝐴) = (𝐴 · 𝐷))
281	279, 280	oveq12d 7438	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷↑2) − (𝐷 · 𝐴)) = ((𝐷 · 𝐷) − (𝐴 · 𝐷)))
282	278, 281	eqtr4d 2799	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷 − 𝐴) · 𝐷) = ((𝐷↑2) − (𝐷 · 𝐴)))
283	282	oveq1d 7435	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝐷 − 𝐴) · 𝐷) · (∗‘(𝐷 − 𝐴))) = (((𝐷↑2) − (𝐷 · 𝐴)) · (∗‘(𝐷 − 𝐴))))
284	277, 283	eqtrd 2796	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷) = (((𝐷↑2) − (𝐷 · 𝐴)) · (∗‘(𝐷 − 𝐴))))
285	276, 284	oveq12d 7438	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷)) = (( -(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))) − (((𝐷↑2) − (𝐷 · 𝐴)) · (∗‘(𝐷 − 𝐴)))))
286	268	negcld 11656	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(𝐷 · 𝐴) ∈ ℂ)
287	261, 268	subcld 11669	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷↑2) − (𝐷 · 𝐴)) ∈ ℂ)
288	286, 287, 219	subdird 11773	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (( -(𝐷 · 𝐴) − ((𝐷↑2) − (𝐷 · 𝐴))) · (∗‘(𝐷 − 𝐴))) = (( -(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))) − (((𝐷↑2) − (𝐷 · 𝐴)) · (∗‘(𝐷 − 𝐴)))))
289	286, 268	addcomd 11512	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ( -(𝐷 · 𝐴) + (𝐷 · 𝐴)) = ((𝐷 · 𝐴) + -(𝐷 · 𝐴)))
290	268, 268	negsubd 11675	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷 · 𝐴) + -(𝐷 · 𝐴)) = ((𝐷 · 𝐴) − (𝐷 · 𝐴)))
291	268	subidd 11657	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷 · 𝐴) − (𝐷 · 𝐴)) = 0)
292	289, 290, 291	3eqtrd 2800	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ( -(𝐷 · 𝐴) + (𝐷 · 𝐴)) = 0)
293	292	oveq1d 7435	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (( -(𝐷 · 𝐴) + (𝐷 · 𝐴)) − (𝐷↑2)) = (0 − (𝐷↑2)))
294	286, 261, 268	subsub3d 11699	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ( -(𝐷 · 𝐴) − ((𝐷↑2) − (𝐷 · 𝐴))) = (( -(𝐷 · 𝐴) + (𝐷 · 𝐴)) − (𝐷↑2)))
295		df-neg 11544	. . . . . . . . . . . . . . 15 ⊢ -(𝐷↑2) = (0 − (𝐷↑2))
296	295	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(𝐷↑2) = (0 − (𝐷↑2)))
297	293, 294, 296	3eqtr4d 2806	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ( -(𝐷 · 𝐴) − ((𝐷↑2) − (𝐷 · 𝐴))) = -(𝐷↑2))
298	297	oveq1d 7435	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (( -(𝐷 · 𝐴) − ((𝐷↑2) − (𝐷 · 𝐴))) · (∗‘(𝐷 − 𝐴))) = ( -(𝐷↑2) · (∗‘(𝐷 − 𝐴))))
299	285, 288, 298	3eqtr2d 2802	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷)) = ( -(𝐷↑2) · (∗‘(𝐷 − 𝐴))))
300	272, 275, 299	3eqtrd 2800	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = ( -(𝐷↑2) · (∗‘(𝐷 − 𝐴))))
301	245	eqcomd 2767	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((∗‘𝐷) − (∗‘𝐴)) = (∗‘(𝐷 − 𝐴)))
302	300, 301	oveq12d 7438	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = (( -(𝐷↑2) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))))
303	261	negcld 11656	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(𝐷↑2) ∈ ℂ)
304	303, 219, 250	divcan4d 12099	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (( -(𝐷↑2) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))) = -(𝐷↑2))
305	302, 304	eqtr2d 2797	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(𝐷↑2) = (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))))
306	261, 305	negcon1ad 11664	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = (𝐷↑2))
307	109, 306	eqtrid 2808	. . . . . 6 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑁 = (𝐷↑2))
308	260, 307	oveq12d 7438	. . . . 5 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑀 · 𝑋) + 𝑁) = ( -(2 · (𝑋 · 𝐷)) + (𝐷↑2)))
309	308	oveq2d 7436	. . . 4 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = ((𝑋↑2) + ( -(2 · (𝑋 · 𝐷)) + (𝐷↑2))))
310	197	sqcld 14287	. . . . 5 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑋↑2) ∈ ℂ)
311	197, 198	mulcld 11329	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑋 · 𝐷) ∈ ℂ)
312	247, 311	mulcld 11329	. . . . . 6 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (2 · (𝑋 · 𝐷)) ∈ ℂ)
313	312	negcld 11656	. . . . 5 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(2 · (𝑋 · 𝐷)) ∈ ℂ)
314	310, 313, 261	addassd 11331	. . . 4 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝑋↑2) + -(2 · (𝑋 · 𝐷))) + (𝐷↑2)) = ((𝑋↑2) + ( -(2 · (𝑋 · 𝐷)) + (𝐷↑2))))
315	310, 312	negsubd 11675	. . . . 5 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑋↑2) + -(2 · (𝑋 · 𝐷))) = ((𝑋↑2) − (2 · (𝑋 · 𝐷))))
316	315	oveq1d 7435	. . . 4 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝑋↑2) + -(2 · (𝑋 · 𝐷))) + (𝐷↑2)) = (((𝑋↑2) − (2 · (𝑋 · 𝐷))) + (𝐷↑2)))
317	309, 314, 316	3eqtr2d 2802	. . 3 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = (((𝑋↑2) − (2 · (𝑋 · 𝐷))) + (𝐷↑2)))
318		binom2sub 14364	. . . 4 ⊢ ((𝑋 ∈ ℂ ∧ 𝐷 ∈ ℂ) → ((𝑋 − 𝐷)↑2) = (((𝑋↑2) − (2 · (𝑋 · 𝐷))) + (𝐷↑2)))
319	197, 198, 318	syl2anc 596	. . 3 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑋 − 𝐷)↑2) = (((𝑋↑2) − (2 · (𝑋 · 𝐷))) + (𝐷↑2)))
320	204	sq0id 14337	. . 3 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑋 − 𝐷)↑2) = 0)
321	317, 319, 320	3eqtr2d 2802	. 2 ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)
322	4	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝑆 ⊆ ℂ)
323	15	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐴 ∈ 𝑆)
324	22	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐵 ∈ 𝑆)
325	47	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐶 ∈ 𝑆)
326	34	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐷 ∈ 𝑆)
327	5	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐸 ∈ 𝑆)
328	7	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐹 ∈ 𝑆)
329	13	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝑋 ∈ ℂ)
330	94	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐴 ≠ 𝐷)
331	20	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶)))
332	32	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹)))
333		simprl 783	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐵 ≠ 𝐶)
334		simprr 785	. . 3 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐸 ≠ 𝐹)
335	322, 323, 324, 325, 326, 327, 328, 329, 330, 331, 332, 45, 3, 1, 109, 333, 334	constrrtcclem 34366	. 2 ⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)
336	181, 321, 335	pm2.61da2ne 3044	1 ⊢ (𝜑 → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ≠ wne 2956   ⊆ wss 3899  ‘cfv 6538  (class class class)co 7420  ℂcc 11198  0cc0 11200   + caddc 11203   · cmul 11205   − cmin 11541   -cneg 11542   / cdiv 11973  2c2 12397  ↑cexp 14204  ∗ccj 15263  abscabs 15401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-cnex 11256  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277  ax-pre-sup 11278

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-sup 9434  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-div 11974  df-nn 12336  df-2 12405  df-3 12406  df-n0 12607  df-z 12694  df-uz 12966  df-rp 13121  df-seq 14145  df-exp 14205  df-cj 15266  df-re 15267  df-im 15268  df-sqrt 15402  df-abs 15403

This theorem is used by:  constrfin  34378  constrelextdg2  34379