Theorem constrrtcc

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

	Ref	Expression
Hypotheses	constrrtcc.s	|- ( ph -> S C_ CC )
	constrrtcc.a	|- ( ph -> A e. S )
	constrrtcc.b	|- ( ph -> B e. S )
	constrrtcc.c	|- ( ph -> C e. S )
	constrrtcc.d	|- ( ph -> D e. S )
	constrrtcc.e	|- ( ph -> E e. S )
	constrrtcc.f	|- ( ph -> F e. S )
	constrrtcc.x	|- ( ph -> X e. CC )
	constrrtcc.1	|- ( ph -> A =/= D )
	constrrtcc.2	|- ( ph -> ( abs ` ( X - A ) ) = ( abs ` ( B - C ) ) )
	constrrtcc.3	|- ( ph -> ( abs ` ( X - D ) ) = ( abs ` ( E - F ) ) )
	constrrtcc.4	|- P = ( ( B - C ) x. ( * ` ( B - C ) ) )
	constrrtcc.5	|- Q = ( ( E - F ) x. ( * ` ( E - F ) ) )
	constrrtcc.m	|- M = ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) / ( ( * ` D ) - ( * ` A ) ) )
	constrrtcc.n	|- N = -u ( ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) / ( ( * ` D ) - ( * ` A ) ) )
Assertion	constrrtcc	|- ( ph -> ( ( X ^ 2 ) + ( ( M x. X ) + N ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		constrrtcc.s	|- ( ph -> S C_ CC )
2		constrrtcc.a	|- ( ph -> A e. S )
3		constrrtcc.b	|- ( ph -> B e. S )
4		constrrtcc.c	|- ( ph -> C e. S )
5		constrrtcc.d	|- ( ph -> D e. S )
6		constrrtcc.e	|- ( ph -> E e. S )
7		constrrtcc.f	|- ( ph -> F e. S )
8		constrrtcc.x	|- ( ph -> X e. CC )
9		constrrtcc.1	|- ( ph -> A =/= D )
10		constrrtcc.2	|- ( ph -> ( abs ` ( X - A ) ) = ( abs ` ( B - C ) ) )
11		constrrtcc.3	|- ( ph -> ( abs ` ( X - D ) ) = ( abs ` ( E - F ) ) )
12		constrrtcc.4	|- P = ( ( B - C ) x. ( * ` ( B - C ) ) )
13		constrrtcc.5	|- Q = ( ( E - F ) x. ( * ` ( E - F ) ) )
14		constrrtcc.m	|- M = ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) / ( ( * ` D ) - ( * ` A ) ) )
15		constrrtcc.n	|- N = -u ( ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) / ( ( * ` D ) - ( * ` A ) ) )
16	14	a1i	|- ( ( ph /\ B = C ) -> M = ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) / ( ( * ` D ) - ( * ` A ) ) ) )
17	1 6	sseldd	|- ( ph -> E e. CC )
18	1 7	sseldd	|- ( ph -> F e. CC )
19	17 18	subcld	|- ( ph -> ( E - F ) e. CC )
20	19	adantr	|- ( ( ph /\ B = C ) -> ( E - F ) e. CC )
21	20	absvalsqd	|- ( ( ph /\ B = C ) -> ( ( abs ` ( E - F ) ) ^ 2 ) = ( ( E - F ) x. ( * ` ( E - F ) ) ) )
22	13 21	eqtr4id	|- ( ( ph /\ B = C ) -> Q = ( ( abs ` ( E - F ) ) ^ 2 ) )
23	8	adantr	|- ( ( ph /\ B = C ) -> X e. CC )
24	1 2	sseldd	|- ( ph -> A e. CC )
25	24	adantr	|- ( ( ph /\ B = C ) -> A e. CC )
26	8 24	subcld	|- ( ph -> ( X - A ) e. CC )
27	26	adantr	|- ( ( ph /\ B = C ) -> ( X - A ) e. CC )
28	10	adantr	|- ( ( ph /\ B = C ) -> ( abs ` ( X - A ) ) = ( abs ` ( B - C ) ) )
29	1 3	sseldd	|- ( ph -> B e. CC )
30	29	adantr	|- ( ( ph /\ B = C ) -> B e. CC )
31		simpr	|- ( ( ph /\ B = C ) -> B = C )
32	30 31	subeq0bd	|- ( ( ph /\ B = C ) -> ( B - C ) = 0 )
33	32	abs00bd	|- ( ( ph /\ B = C ) -> ( abs ` ( B - C ) ) = 0 )
34	28 33	eqtrd	|- ( ( ph /\ B = C ) -> ( abs ` ( X - A ) ) = 0 )
35	27 34	abs00d	|- ( ( ph /\ B = C ) -> ( X - A ) = 0 )
36	23 25 35	subeq0d	|- ( ( ph /\ B = C ) -> X = A )
37	36	fvoveq1d	|- ( ( ph /\ B = C ) -> ( abs ` ( X - D ) ) = ( abs ` ( A - D ) ) )
38	11	adantr	|- ( ( ph /\ B = C ) -> ( abs ` ( X - D ) ) = ( abs ` ( E - F ) ) )
39	1 5	sseldd	|- ( ph -> D e. CC )
40	39	adantr	|- ( ( ph /\ B = C ) -> D e. CC )
41	25 40	abssubd	|- ( ( ph /\ B = C ) -> ( abs ` ( A - D ) ) = ( abs ` ( D - A ) ) )
42	37 38 41	3eqtr3d	|- ( ( ph /\ B = C ) -> ( abs ` ( E - F ) ) = ( abs ` ( D - A ) ) )
43	42	oveq1d	|- ( ( ph /\ B = C ) -> ( ( abs ` ( E - F ) ) ^ 2 ) = ( ( abs ` ( D - A ) ) ^ 2 ) )
44	39 24	subcld	|- ( ph -> ( D - A ) e. CC )
45	44	absvalsqd	|- ( ph -> ( ( abs ` ( D - A ) ) ^ 2 ) = ( ( D - A ) x. ( * ` ( D - A ) ) ) )
46	45	adantr	|- ( ( ph /\ B = C ) -> ( ( abs ` ( D - A ) ) ^ 2 ) = ( ( D - A ) x. ( * ` ( D - A ) ) ) )
47	22 43 46	3eqtrd	|- ( ( ph /\ B = C ) -> Q = ( ( D - A ) x. ( * ` ( D - A ) ) ) )
48	47	oveq1d	|- ( ( ph /\ B = C ) -> ( Q - ( ( * ` D ) x. ( D + A ) ) ) = ( ( ( D - A ) x. ( * ` ( D - A ) ) ) - ( ( * ` D ) x. ( D + A ) ) ) )
49	32	oveq1d	|- ( ( ph /\ B = C ) -> ( ( B - C ) x. ( * ` ( B - C ) ) ) = ( 0 x. ( * ` ( B - C ) ) ) )
50	1 4	sseldd	|- ( ph -> C e. CC )
51	29 50	subcld	|- ( ph -> ( B - C ) e. CC )
52	51	cjcld	|- ( ph -> ( * ` ( B - C ) ) e. CC )
53	52	adantr	|- ( ( ph /\ B = C ) -> ( * ` ( B - C ) ) e. CC )
54	53	mul02d	|- ( ( ph /\ B = C ) -> ( 0 x. ( * ` ( B - C ) ) ) = 0 )
55	49 54	eqtrd	|- ( ( ph /\ B = C ) -> ( ( B - C ) x. ( * ` ( B - C ) ) ) = 0 )
56	12 55	eqtrid	|- ( ( ph /\ B = C ) -> P = 0 )
57	56	oveq1d	|- ( ( ph /\ B = C ) -> ( P - ( ( * ` A ) x. ( D + A ) ) ) = ( 0 - ( ( * ` A ) x. ( D + A ) ) ) )
58	48 57	oveq12d	|- ( ( ph /\ B = C ) -> ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) = ( ( ( ( D - A ) x. ( * ` ( D - A ) ) ) - ( ( * ` D ) x. ( D + A ) ) ) - ( 0 - ( ( * ` A ) x. ( D + A ) ) ) ) )
59	44	adantr	|- ( ( ph /\ B = C ) -> ( D - A ) e. CC )
60	59	cjcld	|- ( ( ph /\ B = C ) -> ( * ` ( D - A ) ) e. CC )
61	59 60	mulcld	|- ( ( ph /\ B = C ) -> ( ( D - A ) x. ( * ` ( D - A ) ) ) e. CC )
62	40	cjcld	|- ( ( ph /\ B = C ) -> ( * ` D ) e. CC )
63	40 25	addcld	|- ( ( ph /\ B = C ) -> ( D + A ) e. CC )
64	62 63	mulcld	|- ( ( ph /\ B = C ) -> ( ( * ` D ) x. ( D + A ) ) e. CC )
65		0cnd	|- ( ( ph /\ B = C ) -> 0 e. CC )
66	25	cjcld	|- ( ( ph /\ B = C ) -> ( * ` A ) e. CC )
67	66 63	mulcld	|- ( ( ph /\ B = C ) -> ( ( * ` A ) x. ( D + A ) ) e. CC )
68	61 64 65 67	sub4d	|- ( ( ph /\ B = C ) -> ( ( ( ( D - A ) x. ( * ` ( D - A ) ) ) - ( ( * ` D ) x. ( D + A ) ) ) - ( 0 - ( ( * ` A ) x. ( D + A ) ) ) ) = ( ( ( ( D - A ) x. ( * ` ( D - A ) ) ) - 0 ) - ( ( ( * ` D ) x. ( D + A ) ) - ( ( * ` A ) x. ( D + A ) ) ) ) )
69	61	subid1d	|- ( ( ph /\ B = C ) -> ( ( ( D - A ) x. ( * ` ( D - A ) ) ) - 0 ) = ( ( D - A ) x. ( * ` ( D - A ) ) ) )
70	39 24	cjsubd	|- ( ph -> ( * ` ( D - A ) ) = ( ( * ` D ) - ( * ` A ) ) )
71	70	oveq1d	|- ( ph -> ( ( * ` ( D - A ) ) x. ( D + A ) ) = ( ( ( * ` D ) - ( * ` A ) ) x. ( D + A ) ) )
72	44	cjcld	|- ( ph -> ( * ` ( D - A ) ) e. CC )
73	39 24	addcld	|- ( ph -> ( D + A ) e. CC )
74	72 73	mulcomd	|- ( ph -> ( ( * ` ( D - A ) ) x. ( D + A ) ) = ( ( D + A ) x. ( * ` ( D - A ) ) ) )
75	39	cjcld	|- ( ph -> ( * ` D ) e. CC )
76	24	cjcld	|- ( ph -> ( * ` A ) e. CC )
77	75 76 73	subdird	|- ( ph -> ( ( ( * ` D ) - ( * ` A ) ) x. ( D + A ) ) = ( ( ( * ` D ) x. ( D + A ) ) - ( ( * ` A ) x. ( D + A ) ) ) )
78	71 74 77	3eqtr3rd	|- ( ph -> ( ( ( * ` D ) x. ( D + A ) ) - ( ( * ` A ) x. ( D + A ) ) ) = ( ( D + A ) x. ( * ` ( D - A ) ) ) )
79	78	adantr	|- ( ( ph /\ B = C ) -> ( ( ( * ` D ) x. ( D + A ) ) - ( ( * ` A ) x. ( D + A ) ) ) = ( ( D + A ) x. ( * ` ( D - A ) ) ) )
80	69 79	oveq12d	|- ( ( ph /\ B = C ) -> ( ( ( ( D - A ) x. ( * ` ( D - A ) ) ) - 0 ) - ( ( ( * ` D ) x. ( D + A ) ) - ( ( * ` A ) x. ( D + A ) ) ) ) = ( ( ( D - A ) x. ( * ` ( D - A ) ) ) - ( ( D + A ) x. ( * ` ( D - A ) ) ) ) )
81	58 68 80	3eqtrd	|- ( ( ph /\ B = C ) -> ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) = ( ( ( D - A ) x. ( * ` ( D - A ) ) ) - ( ( D + A ) x. ( * ` ( D - A ) ) ) ) )
82	59 63 60	subdird	|- ( ( ph /\ B = C ) -> ( ( ( D - A ) - ( D + A ) ) x. ( * ` ( D - A ) ) ) = ( ( ( D - A ) x. ( * ` ( D - A ) ) ) - ( ( D + A ) x. ( * ` ( D - A ) ) ) ) )
83	63 59	negsubdi2d	|- ( ( ph /\ B = C ) -> -u ( ( D + A ) - ( D - A ) ) = ( ( D - A ) - ( D + A ) ) )
84	40 25 25	pnncand	|- ( ( ph /\ B = C ) -> ( ( D + A ) - ( D - A ) ) = ( A + A ) )
85	25	2timesd	|- ( ( ph /\ B = C ) -> ( 2 x. A ) = ( A + A ) )
86	84 85	eqtr4d	|- ( ( ph /\ B = C ) -> ( ( D + A ) - ( D - A ) ) = ( 2 x. A ) )
87	86	negeqd	|- ( ( ph /\ B = C ) -> -u ( ( D + A ) - ( D - A ) ) = -u ( 2 x. A ) )
88	83 87	eqtr3d	|- ( ( ph /\ B = C ) -> ( ( D - A ) - ( D + A ) ) = -u ( 2 x. A ) )
89	88	oveq1d	|- ( ( ph /\ B = C ) -> ( ( ( D - A ) - ( D + A ) ) x. ( * ` ( D - A ) ) ) = ( -u ( 2 x. A ) x. ( * ` ( D - A ) ) ) )
90	81 82 89	3eqtr2rd	|- ( ( ph /\ B = C ) -> ( -u ( 2 x. A ) x. ( * ` ( D - A ) ) ) = ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) )
91	70	adantr	|- ( ( ph /\ B = C ) -> ( * ` ( D - A ) ) = ( ( * ` D ) - ( * ` A ) ) )
92	90 91	oveq12d	|- ( ( ph /\ B = C ) -> ( ( -u ( 2 x. A ) x. ( * ` ( D - A ) ) ) / ( * ` ( D - A ) ) ) = ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) / ( ( * ` D ) - ( * ` A ) ) ) )
93		2cnd	|- ( ( ph /\ B = C ) -> 2 e. CC )
94	93 25	mulcld	|- ( ( ph /\ B = C ) -> ( 2 x. A ) e. CC )
95	94	negcld	|- ( ( ph /\ B = C ) -> -u ( 2 x. A ) e. CC )
96	9	necomd	|- ( ph -> D =/= A )
97	39 24 96	subne0d	|- ( ph -> ( D - A ) =/= 0 )
98	44 97	cjne0d	|- ( ph -> ( * ` ( D - A ) ) =/= 0 )
99	98	adantr	|- ( ( ph /\ B = C ) -> ( * ` ( D - A ) ) =/= 0 )
100	95 60 99	divcan4d	|- ( ( ph /\ B = C ) -> ( ( -u ( 2 x. A ) x. ( * ` ( D - A ) ) ) / ( * ` ( D - A ) ) ) = -u ( 2 x. A ) )
101	16 92 100	3eqtr2d	|- ( ( ph /\ B = C ) -> M = -u ( 2 x. A ) )
102	101	oveq1d	|- ( ( ph /\ B = C ) -> ( M x. X ) = ( -u ( 2 x. A ) x. X ) )
103	94 23	mulneg1d	|- ( ( ph /\ B = C ) -> ( -u ( 2 x. A ) x. X ) = -u ( ( 2 x. A ) x. X ) )
104	93 25 23	mulassd	|- ( ( ph /\ B = C ) -> ( ( 2 x. A ) x. X ) = ( 2 x. ( A x. X ) ) )
105	25 23	mulcomd	|- ( ( ph /\ B = C ) -> ( A x. X ) = ( X x. A ) )
106	105	oveq2d	|- ( ( ph /\ B = C ) -> ( 2 x. ( A x. X ) ) = ( 2 x. ( X x. A ) ) )
107	104 106	eqtrd	|- ( ( ph /\ B = C ) -> ( ( 2 x. A ) x. X ) = ( 2 x. ( X x. A ) ) )
108	107	negeqd	|- ( ( ph /\ B = C ) -> -u ( ( 2 x. A ) x. X ) = -u ( 2 x. ( X x. A ) ) )
109	102 103 108	3eqtrd	|- ( ( ph /\ B = C ) -> ( M x. X ) = -u ( 2 x. ( X x. A ) ) )
110	25	sqcld	|- ( ( ph /\ B = C ) -> ( A ^ 2 ) e. CC )
111	56	oveq1d	|- ( ( ph /\ B = C ) -> ( P x. D ) = ( 0 x. D ) )
112	40	mul02d	|- ( ( ph /\ B = C ) -> ( 0 x. D ) = 0 )
113	111 112	eqtrd	|- ( ( ph /\ B = C ) -> ( P x. D ) = 0 )
114	113	oveq2d	|- ( ( ph /\ B = C ) -> ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) = ( ( ( * ` A ) x. ( D x. A ) ) - 0 ) )
115	40 25	mulcld	|- ( ( ph /\ B = C ) -> ( D x. A ) e. CC )
116	66 115	mulcld	|- ( ( ph /\ B = C ) -> ( ( * ` A ) x. ( D x. A ) ) e. CC )
117	116	subid1d	|- ( ( ph /\ B = C ) -> ( ( ( * ` A ) x. ( D x. A ) ) - 0 ) = ( ( * ` A ) x. ( D x. A ) ) )
118	114 117	eqtrd	|- ( ( ph /\ B = C ) -> ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) = ( ( * ` A ) x. ( D x. A ) ) )
119	47	oveq1d	|- ( ( ph /\ B = C ) -> ( Q x. A ) = ( ( ( D - A ) x. ( * ` ( D - A ) ) ) x. A ) )
120	119	oveq2d	|- ( ( ph /\ B = C ) -> ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) = ( ( ( * ` D ) x. ( D x. A ) ) - ( ( ( D - A ) x. ( * ` ( D - A ) ) ) x. A ) ) )
121	118 120	oveq12d	|- ( ( ph /\ B = C ) -> ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) = ( ( ( * ` A ) x. ( D x. A ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( ( ( D - A ) x. ( * ` ( D - A ) ) ) x. A ) ) ) )
122	62 115	mulcld	|- ( ( ph /\ B = C ) -> ( ( * ` D ) x. ( D x. A ) ) e. CC )
123	61 25	mulcld	|- ( ( ph /\ B = C ) -> ( ( ( D - A ) x. ( * ` ( D - A ) ) ) x. A ) e. CC )
124	116 122 123	subsubd	|- ( ( ph /\ B = C ) -> ( ( ( * ` A ) x. ( D x. A ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( ( ( D - A ) x. ( * ` ( D - A ) ) ) x. A ) ) ) = ( ( ( ( * ` A ) x. ( D x. A ) ) - ( ( * ` D ) x. ( D x. A ) ) ) + ( ( ( D - A ) x. ( * ` ( D - A ) ) ) x. A ) ) )
125	70	negeqd	|- ( ph -> -u ( * ` ( D - A ) ) = -u ( ( * ` D ) - ( * ` A ) ) )
126	75 76	negsubdi2d	|- ( ph -> -u ( ( * ` D ) - ( * ` A ) ) = ( ( * ` A ) - ( * ` D ) ) )
127	125 126	eqtr2d	|- ( ph -> ( ( * ` A ) - ( * ` D ) ) = -u ( * ` ( D - A ) ) )
128	127	oveq1d	|- ( ph -> ( ( ( * ` A ) - ( * ` D ) ) x. ( D x. A ) ) = ( -u ( * ` ( D - A ) ) x. ( D x. A ) ) )
129	39 24	mulcld	|- ( ph -> ( D x. A ) e. CC )
130	76 75 129	subdird	|- ( ph -> ( ( ( * ` A ) - ( * ` D ) ) x. ( D x. A ) ) = ( ( ( * ` A ) x. ( D x. A ) ) - ( ( * ` D ) x. ( D x. A ) ) ) )
131	72 129	mulcomd	|- ( ph -> ( ( * ` ( D - A ) ) x. ( D x. A ) ) = ( ( D x. A ) x. ( * ` ( D - A ) ) ) )
132	131	negeqd	|- ( ph -> -u ( ( * ` ( D - A ) ) x. ( D x. A ) ) = -u ( ( D x. A ) x. ( * ` ( D - A ) ) ) )
133	72 129	mulneg1d	|- ( ph -> ( -u ( * ` ( D - A ) ) x. ( D x. A ) ) = -u ( ( * ` ( D - A ) ) x. ( D x. A ) ) )
134	129 72	mulneg1d	|- ( ph -> ( -u ( D x. A ) x. ( * ` ( D - A ) ) ) = -u ( ( D x. A ) x. ( * ` ( D - A ) ) ) )
135	132 133 134	3eqtr4d	|- ( ph -> ( -u ( * ` ( D - A ) ) x. ( D x. A ) ) = ( -u ( D x. A ) x. ( * ` ( D - A ) ) ) )
136	128 130 135	3eqtr3d	|- ( ph -> ( ( ( * ` A ) x. ( D x. A ) ) - ( ( * ` D ) x. ( D x. A ) ) ) = ( -u ( D x. A ) x. ( * ` ( D - A ) ) ) )
137	136	adantr	|- ( ( ph /\ B = C ) -> ( ( ( * ` A ) x. ( D x. A ) ) - ( ( * ` D ) x. ( D x. A ) ) ) = ( -u ( D x. A ) x. ( * ` ( D - A ) ) ) )
138	59 60 25	mul32d	|- ( ( ph /\ B = C ) -> ( ( ( D - A ) x. ( * ` ( D - A ) ) ) x. A ) = ( ( ( D - A ) x. A ) x. ( * ` ( D - A ) ) ) )
139	40 25 25	subdird	|- ( ( ph /\ B = C ) -> ( ( D - A ) x. A ) = ( ( D x. A ) - ( A x. A ) ) )
140	25	sqvald	|- ( ( ph /\ B = C ) -> ( A ^ 2 ) = ( A x. A ) )
141	140	oveq2d	|- ( ( ph /\ B = C ) -> ( ( D x. A ) - ( A ^ 2 ) ) = ( ( D x. A ) - ( A x. A ) ) )
142	139 141	eqtr4d	|- ( ( ph /\ B = C ) -> ( ( D - A ) x. A ) = ( ( D x. A ) - ( A ^ 2 ) ) )
143	142	oveq1d	|- ( ( ph /\ B = C ) -> ( ( ( D - A ) x. A ) x. ( * ` ( D - A ) ) ) = ( ( ( D x. A ) - ( A ^ 2 ) ) x. ( * ` ( D - A ) ) ) )
144	138 143	eqtrd	|- ( ( ph /\ B = C ) -> ( ( ( D - A ) x. ( * ` ( D - A ) ) ) x. A ) = ( ( ( D x. A ) - ( A ^ 2 ) ) x. ( * ` ( D - A ) ) ) )
145	137 144	oveq12d	|- ( ( ph /\ B = C ) -> ( ( ( ( * ` A ) x. ( D x. A ) ) - ( ( * ` D ) x. ( D x. A ) ) ) + ( ( ( D - A ) x. ( * ` ( D - A ) ) ) x. A ) ) = ( ( -u ( D x. A ) x. ( * ` ( D - A ) ) ) + ( ( ( D x. A ) - ( A ^ 2 ) ) x. ( * ` ( D - A ) ) ) ) )
146	115	negcld	|- ( ( ph /\ B = C ) -> -u ( D x. A ) e. CC )
147	115 110	subcld	|- ( ( ph /\ B = C ) -> ( ( D x. A ) - ( A ^ 2 ) ) e. CC )
148	146 147 60	adddird	|- ( ( ph /\ B = C ) -> ( ( -u ( D x. A ) + ( ( D x. A ) - ( A ^ 2 ) ) ) x. ( * ` ( D - A ) ) ) = ( ( -u ( D x. A ) x. ( * ` ( D - A ) ) ) + ( ( ( D x. A ) - ( A ^ 2 ) ) x. ( * ` ( D - A ) ) ) ) )
149	115	subidd	|- ( ( ph /\ B = C ) -> ( ( D x. A ) - ( D x. A ) ) = 0 )
150	149	oveq1d	|- ( ( ph /\ B = C ) -> ( ( ( D x. A ) - ( D x. A ) ) - ( A ^ 2 ) ) = ( 0 - ( A ^ 2 ) ) )
151	146 147	addcomd	|- ( ( ph /\ B = C ) -> ( -u ( D x. A ) + ( ( D x. A ) - ( A ^ 2 ) ) ) = ( ( ( D x. A ) - ( A ^ 2 ) ) + -u ( D x. A ) ) )
152	147 115	negsubd	|- ( ( ph /\ B = C ) -> ( ( ( D x. A ) - ( A ^ 2 ) ) + -u ( D x. A ) ) = ( ( ( D x. A ) - ( A ^ 2 ) ) - ( D x. A ) ) )
153	115 110 115	sub32d	|- ( ( ph /\ B = C ) -> ( ( ( D x. A ) - ( A ^ 2 ) ) - ( D x. A ) ) = ( ( ( D x. A ) - ( D x. A ) ) - ( A ^ 2 ) ) )
154	151 152 153	3eqtrd	|- ( ( ph /\ B = C ) -> ( -u ( D x. A ) + ( ( D x. A ) - ( A ^ 2 ) ) ) = ( ( ( D x. A ) - ( D x. A ) ) - ( A ^ 2 ) ) )
155		df-neg	|- -u ( A ^ 2 ) = ( 0 - ( A ^ 2 ) )
156	155	a1i	|- ( ( ph /\ B = C ) -> -u ( A ^ 2 ) = ( 0 - ( A ^ 2 ) ) )
157	150 154 156	3eqtr4d	|- ( ( ph /\ B = C ) -> ( -u ( D x. A ) + ( ( D x. A ) - ( A ^ 2 ) ) ) = -u ( A ^ 2 ) )
158	157	oveq1d	|- ( ( ph /\ B = C ) -> ( ( -u ( D x. A ) + ( ( D x. A ) - ( A ^ 2 ) ) ) x. ( * ` ( D - A ) ) ) = ( -u ( A ^ 2 ) x. ( * ` ( D - A ) ) ) )
159	145 148 158	3eqtr2d	|- ( ( ph /\ B = C ) -> ( ( ( ( * ` A ) x. ( D x. A ) ) - ( ( * ` D ) x. ( D x. A ) ) ) + ( ( ( D - A ) x. ( * ` ( D - A ) ) ) x. A ) ) = ( -u ( A ^ 2 ) x. ( * ` ( D - A ) ) ) )
160	121 124 159	3eqtrd	|- ( ( ph /\ B = C ) -> ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) = ( -u ( A ^ 2 ) x. ( * ` ( D - A ) ) ) )
161	91	eqcomd	|- ( ( ph /\ B = C ) -> ( ( * ` D ) - ( * ` A ) ) = ( * ` ( D - A ) ) )
162	160 161	oveq12d	|- ( ( ph /\ B = C ) -> ( ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) / ( ( * ` D ) - ( * ` A ) ) ) = ( ( -u ( A ^ 2 ) x. ( * ` ( D - A ) ) ) / ( * ` ( D - A ) ) ) )
163	110	negcld	|- ( ( ph /\ B = C ) -> -u ( A ^ 2 ) e. CC )
164	163 60 99	divcan4d	|- ( ( ph /\ B = C ) -> ( ( -u ( A ^ 2 ) x. ( * ` ( D - A ) ) ) / ( * ` ( D - A ) ) ) = -u ( A ^ 2 ) )
165	162 164	eqtr2d	|- ( ( ph /\ B = C ) -> -u ( A ^ 2 ) = ( ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) / ( ( * ` D ) - ( * ` A ) ) ) )
166	110 165	negcon1ad	|- ( ( ph /\ B = C ) -> -u ( ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) / ( ( * ` D ) - ( * ` A ) ) ) = ( A ^ 2 ) )
167	15 166	eqtrid	|- ( ( ph /\ B = C ) -> N = ( A ^ 2 ) )
168	109 167	oveq12d	|- ( ( ph /\ B = C ) -> ( ( M x. X ) + N ) = ( -u ( 2 x. ( X x. A ) ) + ( A ^ 2 ) ) )
169	168	oveq2d	|- ( ( ph /\ B = C ) -> ( ( X ^ 2 ) + ( ( M x. X ) + N ) ) = ( ( X ^ 2 ) + ( -u ( 2 x. ( X x. A ) ) + ( A ^ 2 ) ) ) )
170	23	sqcld	|- ( ( ph /\ B = C ) -> ( X ^ 2 ) e. CC )
171	23 25	mulcld	|- ( ( ph /\ B = C ) -> ( X x. A ) e. CC )
172	93 171	mulcld	|- ( ( ph /\ B = C ) -> ( 2 x. ( X x. A ) ) e. CC )
173	172	negcld	|- ( ( ph /\ B = C ) -> -u ( 2 x. ( X x. A ) ) e. CC )
174	170 173 110	addassd	|- ( ( ph /\ B = C ) -> ( ( ( X ^ 2 ) + -u ( 2 x. ( X x. A ) ) ) + ( A ^ 2 ) ) = ( ( X ^ 2 ) + ( -u ( 2 x. ( X x. A ) ) + ( A ^ 2 ) ) ) )
175	170 172	negsubd	|- ( ( ph /\ B = C ) -> ( ( X ^ 2 ) + -u ( 2 x. ( X x. A ) ) ) = ( ( X ^ 2 ) - ( 2 x. ( X x. A ) ) ) )
176	175	oveq1d	|- ( ( ph /\ B = C ) -> ( ( ( X ^ 2 ) + -u ( 2 x. ( X x. A ) ) ) + ( A ^ 2 ) ) = ( ( ( X ^ 2 ) - ( 2 x. ( X x. A ) ) ) + ( A ^ 2 ) ) )
177	169 174 176	3eqtr2d	|- ( ( ph /\ B = C ) -> ( ( X ^ 2 ) + ( ( M x. X ) + N ) ) = ( ( ( X ^ 2 ) - ( 2 x. ( X x. A ) ) ) + ( A ^ 2 ) ) )
178		binom2sub	|- ( ( X e. CC /\ A e. CC ) -> ( ( X - A ) ^ 2 ) = ( ( ( X ^ 2 ) - ( 2 x. ( X x. A ) ) ) + ( A ^ 2 ) ) )
179	23 25 178	syl2anc	|- ( ( ph /\ B = C ) -> ( ( X - A ) ^ 2 ) = ( ( ( X ^ 2 ) - ( 2 x. ( X x. A ) ) ) + ( A ^ 2 ) ) )
180	35	sq0id	|- ( ( ph /\ B = C ) -> ( ( X - A ) ^ 2 ) = 0 )
181	177 179 180	3eqtr2d	|- ( ( ph /\ B = C ) -> ( ( X ^ 2 ) + ( ( M x. X ) + N ) ) = 0 )
182	14	a1i	|- ( ( ph /\ E = F ) -> M = ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) / ( ( * ` D ) - ( * ` A ) ) ) )
183	17	adantr	|- ( ( ph /\ E = F ) -> E e. CC )
184		simpr	|- ( ( ph /\ E = F ) -> E = F )
185	183 184	subeq0bd	|- ( ( ph /\ E = F ) -> ( E - F ) = 0 )
186	185	oveq1d	|- ( ( ph /\ E = F ) -> ( ( E - F ) x. ( * ` ( E - F ) ) ) = ( 0 x. ( * ` ( E - F ) ) ) )
187	19	cjcld	|- ( ph -> ( * ` ( E - F ) ) e. CC )
188	187	adantr	|- ( ( ph /\ E = F ) -> ( * ` ( E - F ) ) e. CC )
189	188	mul02d	|- ( ( ph /\ E = F ) -> ( 0 x. ( * ` ( E - F ) ) ) = 0 )
190	186 189	eqtrd	|- ( ( ph /\ E = F ) -> ( ( E - F ) x. ( * ` ( E - F ) ) ) = 0 )
191	13 190	eqtrid	|- ( ( ph /\ E = F ) -> Q = 0 )
192	191	oveq1d	|- ( ( ph /\ E = F ) -> ( Q - ( ( * ` D ) x. ( D + A ) ) ) = ( 0 - ( ( * ` D ) x. ( D + A ) ) ) )
193	51	adantr	|- ( ( ph /\ E = F ) -> ( B - C ) e. CC )
194	193	absvalsqd	|- ( ( ph /\ E = F ) -> ( ( abs ` ( B - C ) ) ^ 2 ) = ( ( B - C ) x. ( * ` ( B - C ) ) ) )
195	12 194	eqtr4id	|- ( ( ph /\ E = F ) -> P = ( ( abs ` ( B - C ) ) ^ 2 ) )
196	10	adantr	|- ( ( ph /\ E = F ) -> ( abs ` ( X - A ) ) = ( abs ` ( B - C ) ) )
197	8	adantr	|- ( ( ph /\ E = F ) -> X e. CC )
198	39	adantr	|- ( ( ph /\ E = F ) -> D e. CC )
199	8 39	subcld	|- ( ph -> ( X - D ) e. CC )
200	199	adantr	|- ( ( ph /\ E = F ) -> ( X - D ) e. CC )
201	11	adantr	|- ( ( ph /\ E = F ) -> ( abs ` ( X - D ) ) = ( abs ` ( E - F ) ) )
202	185	abs00bd	|- ( ( ph /\ E = F ) -> ( abs ` ( E - F ) ) = 0 )
203	201 202	eqtrd	|- ( ( ph /\ E = F ) -> ( abs ` ( X - D ) ) = 0 )
204	200 203	abs00d	|- ( ( ph /\ E = F ) -> ( X - D ) = 0 )
205	197 198 204	subeq0d	|- ( ( ph /\ E = F ) -> X = D )
206	205	fvoveq1d	|- ( ( ph /\ E = F ) -> ( abs ` ( X - A ) ) = ( abs ` ( D - A ) ) )
207	196 206	eqtr3d	|- ( ( ph /\ E = F ) -> ( abs ` ( B - C ) ) = ( abs ` ( D - A ) ) )
208	207	oveq1d	|- ( ( ph /\ E = F ) -> ( ( abs ` ( B - C ) ) ^ 2 ) = ( ( abs ` ( D - A ) ) ^ 2 ) )
209	45	adantr	|- ( ( ph /\ E = F ) -> ( ( abs ` ( D - A ) ) ^ 2 ) = ( ( D - A ) x. ( * ` ( D - A ) ) ) )
210	195 208 209	3eqtrd	|- ( ( ph /\ E = F ) -> P = ( ( D - A ) x. ( * ` ( D - A ) ) ) )
211	210	oveq1d	|- ( ( ph /\ E = F ) -> ( P - ( ( * ` A ) x. ( D + A ) ) ) = ( ( ( D - A ) x. ( * ` ( D - A ) ) ) - ( ( * ` A ) x. ( D + A ) ) ) )
212	192 211	oveq12d	|- ( ( ph /\ E = F ) -> ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) = ( ( 0 - ( ( * ` D ) x. ( D + A ) ) ) - ( ( ( D - A ) x. ( * ` ( D - A ) ) ) - ( ( * ` A ) x. ( D + A ) ) ) ) )
213		0cnd	|- ( ( ph /\ E = F ) -> 0 e. CC )
214	198	cjcld	|- ( ( ph /\ E = F ) -> ( * ` D ) e. CC )
215	24	adantr	|- ( ( ph /\ E = F ) -> A e. CC )
216	198 215	addcld	|- ( ( ph /\ E = F ) -> ( D + A ) e. CC )
217	214 216	mulcld	|- ( ( ph /\ E = F ) -> ( ( * ` D ) x. ( D + A ) ) e. CC )
218	44	adantr	|- ( ( ph /\ E = F ) -> ( D - A ) e. CC )
219	218	cjcld	|- ( ( ph /\ E = F ) -> ( * ` ( D - A ) ) e. CC )
220	218 219	mulcld	|- ( ( ph /\ E = F ) -> ( ( D - A ) x. ( * ` ( D - A ) ) ) e. CC )
221	215	cjcld	|- ( ( ph /\ E = F ) -> ( * ` A ) e. CC )
222	221 216	mulcld	|- ( ( ph /\ E = F ) -> ( ( * ` A ) x. ( D + A ) ) e. CC )
223	213 217 220 222	sub4d	|- ( ( ph /\ E = F ) -> ( ( 0 - ( ( * ` D ) x. ( D + A ) ) ) - ( ( ( D - A ) x. ( * ` ( D - A ) ) ) - ( ( * ` A ) x. ( D + A ) ) ) ) = ( ( 0 - ( ( D - A ) x. ( * ` ( D - A ) ) ) ) - ( ( ( * ` D ) x. ( D + A ) ) - ( ( * ` A ) x. ( D + A ) ) ) ) )
224	218 219	mulneg1d	|- ( ( ph /\ E = F ) -> ( -u ( D - A ) x. ( * ` ( D - A ) ) ) = -u ( ( D - A ) x. ( * ` ( D - A ) ) ) )
225	198 215	negsubdi2d	|- ( ( ph /\ E = F ) -> -u ( D - A ) = ( A - D ) )
226	225	oveq1d	|- ( ( ph /\ E = F ) -> ( -u ( D - A ) x. ( * ` ( D - A ) ) ) = ( ( A - D ) x. ( * ` ( D - A ) ) ) )
227		df-neg	|- -u ( ( D - A ) x. ( * ` ( D - A ) ) ) = ( 0 - ( ( D - A ) x. ( * ` ( D - A ) ) ) )
228	227	a1i	|- ( ( ph /\ E = F ) -> -u ( ( D - A ) x. ( * ` ( D - A ) ) ) = ( 0 - ( ( D - A ) x. ( * ` ( D - A ) ) ) ) )
229	224 226 228	3eqtr3rd	|- ( ( ph /\ E = F ) -> ( 0 - ( ( D - A ) x. ( * ` ( D - A ) ) ) ) = ( ( A - D ) x. ( * ` ( D - A ) ) ) )
230	78	adantr	|- ( ( ph /\ E = F ) -> ( ( ( * ` D ) x. ( D + A ) ) - ( ( * ` A ) x. ( D + A ) ) ) = ( ( D + A ) x. ( * ` ( D - A ) ) ) )
231	229 230	oveq12d	|- ( ( ph /\ E = F ) -> ( ( 0 - ( ( D - A ) x. ( * ` ( D - A ) ) ) ) - ( ( ( * ` D ) x. ( D + A ) ) - ( ( * ` A ) x. ( D + A ) ) ) ) = ( ( ( A - D ) x. ( * ` ( D - A ) ) ) - ( ( D + A ) x. ( * ` ( D - A ) ) ) ) )
232	212 223 231	3eqtrd	|- ( ( ph /\ E = F ) -> ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) = ( ( ( A - D ) x. ( * ` ( D - A ) ) ) - ( ( D + A ) x. ( * ` ( D - A ) ) ) ) )
233	215 198	subcld	|- ( ( ph /\ E = F ) -> ( A - D ) e. CC )
234	233 216 219	subdird	|- ( ( ph /\ E = F ) -> ( ( ( A - D ) - ( D + A ) ) x. ( * ` ( D - A ) ) ) = ( ( ( A - D ) x. ( * ` ( D - A ) ) ) - ( ( D + A ) x. ( * ` ( D - A ) ) ) ) )
235	216 233	negsubdi2d	|- ( ( ph /\ E = F ) -> -u ( ( D + A ) - ( A - D ) ) = ( ( A - D ) - ( D + A ) ) )
236	198	2timesd	|- ( ( ph /\ E = F ) -> ( 2 x. D ) = ( D + D ) )
237	215 198 198	pnncand	|- ( ( ph /\ E = F ) -> ( ( A + D ) - ( A - D ) ) = ( D + D ) )
238	215 198	addcomd	|- ( ( ph /\ E = F ) -> ( A + D ) = ( D + A ) )
239	238	oveq1d	|- ( ( ph /\ E = F ) -> ( ( A + D ) - ( A - D ) ) = ( ( D + A ) - ( A - D ) ) )
240	236 237 239	3eqtr2rd	|- ( ( ph /\ E = F ) -> ( ( D + A ) - ( A - D ) ) = ( 2 x. D ) )
241	240	negeqd	|- ( ( ph /\ E = F ) -> -u ( ( D + A ) - ( A - D ) ) = -u ( 2 x. D ) )
242	235 241	eqtr3d	|- ( ( ph /\ E = F ) -> ( ( A - D ) - ( D + A ) ) = -u ( 2 x. D ) )
243	242	oveq1d	|- ( ( ph /\ E = F ) -> ( ( ( A - D ) - ( D + A ) ) x. ( * ` ( D - A ) ) ) = ( -u ( 2 x. D ) x. ( * ` ( D - A ) ) ) )
244	232 234 243	3eqtr2rd	|- ( ( ph /\ E = F ) -> ( -u ( 2 x. D ) x. ( * ` ( D - A ) ) ) = ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) )
245	70	adantr	|- ( ( ph /\ E = F ) -> ( * ` ( D - A ) ) = ( ( * ` D ) - ( * ` A ) ) )
246	244 245	oveq12d	|- ( ( ph /\ E = F ) -> ( ( -u ( 2 x. D ) x. ( * ` ( D - A ) ) ) / ( * ` ( D - A ) ) ) = ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) / ( ( * ` D ) - ( * ` A ) ) ) )
247		2cnd	|- ( ( ph /\ E = F ) -> 2 e. CC )
248	247 198	mulcld	|- ( ( ph /\ E = F ) -> ( 2 x. D ) e. CC )
249	248	negcld	|- ( ( ph /\ E = F ) -> -u ( 2 x. D ) e. CC )
250	98	adantr	|- ( ( ph /\ E = F ) -> ( * ` ( D - A ) ) =/= 0 )
251	249 219 250	divcan4d	|- ( ( ph /\ E = F ) -> ( ( -u ( 2 x. D ) x. ( * ` ( D - A ) ) ) / ( * ` ( D - A ) ) ) = -u ( 2 x. D ) )
252	182 246 251	3eqtr2d	|- ( ( ph /\ E = F ) -> M = -u ( 2 x. D ) )
253	252	oveq1d	|- ( ( ph /\ E = F ) -> ( M x. X ) = ( -u ( 2 x. D ) x. X ) )
254	248 197	mulneg1d	|- ( ( ph /\ E = F ) -> ( -u ( 2 x. D ) x. X ) = -u ( ( 2 x. D ) x. X ) )
255	247 198 197	mulassd	|- ( ( ph /\ E = F ) -> ( ( 2 x. D ) x. X ) = ( 2 x. ( D x. X ) ) )
256	198 197	mulcomd	|- ( ( ph /\ E = F ) -> ( D x. X ) = ( X x. D ) )
257	256	oveq2d	|- ( ( ph /\ E = F ) -> ( 2 x. ( D x. X ) ) = ( 2 x. ( X x. D ) ) )
258	255 257	eqtrd	|- ( ( ph /\ E = F ) -> ( ( 2 x. D ) x. X ) = ( 2 x. ( X x. D ) ) )
259	258	negeqd	|- ( ( ph /\ E = F ) -> -u ( ( 2 x. D ) x. X ) = -u ( 2 x. ( X x. D ) ) )
260	253 254 259	3eqtrd	|- ( ( ph /\ E = F ) -> ( M x. X ) = -u ( 2 x. ( X x. D ) ) )
261	198	sqcld	|- ( ( ph /\ E = F ) -> ( D ^ 2 ) e. CC )
262	210	oveq1d	|- ( ( ph /\ E = F ) -> ( P x. D ) = ( ( ( D - A ) x. ( * ` ( D - A ) ) ) x. D ) )
263	262	oveq2d	|- ( ( ph /\ E = F ) -> ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) = ( ( ( * ` A ) x. ( D x. A ) ) - ( ( ( D - A ) x. ( * ` ( D - A ) ) ) x. D ) ) )
264	191	oveq1d	|- ( ( ph /\ E = F ) -> ( Q x. A ) = ( 0 x. A ) )
265	215	mul02d	|- ( ( ph /\ E = F ) -> ( 0 x. A ) = 0 )
266	264 265	eqtrd	|- ( ( ph /\ E = F ) -> ( Q x. A ) = 0 )
267	266	oveq2d	|- ( ( ph /\ E = F ) -> ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) = ( ( ( * ` D ) x. ( D x. A ) ) - 0 ) )
268	198 215	mulcld	|- ( ( ph /\ E = F ) -> ( D x. A ) e. CC )
269	214 268	mulcld	|- ( ( ph /\ E = F ) -> ( ( * ` D ) x. ( D x. A ) ) e. CC )
270	269	subid1d	|- ( ( ph /\ E = F ) -> ( ( ( * ` D ) x. ( D x. A ) ) - 0 ) = ( ( * ` D ) x. ( D x. A ) ) )
271	267 270	eqtrd	|- ( ( ph /\ E = F ) -> ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) = ( ( * ` D ) x. ( D x. A ) ) )
272	263 271	oveq12d	|- ( ( ph /\ E = F ) -> ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) = ( ( ( ( * ` A ) x. ( D x. A ) ) - ( ( ( D - A ) x. ( * ` ( D - A ) ) ) x. D ) ) - ( ( * ` D ) x. ( D x. A ) ) ) )
273	221 268	mulcld	|- ( ( ph /\ E = F ) -> ( ( * ` A ) x. ( D x. A ) ) e. CC )
274	220 198	mulcld	|- ( ( ph /\ E = F ) -> ( ( ( D - A ) x. ( * ` ( D - A ) ) ) x. D ) e. CC )
275	273 274 269	sub32d	|- ( ( ph /\ E = F ) -> ( ( ( ( * ` A ) x. ( D x. A ) ) - ( ( ( D - A ) x. ( * ` ( D - A ) ) ) x. D ) ) - ( ( * ` D ) x. ( D x. A ) ) ) = ( ( ( ( * ` A ) x. ( D x. A ) ) - ( ( * ` D ) x. ( D x. A ) ) ) - ( ( ( D - A ) x. ( * ` ( D - A ) ) ) x. D ) ) )
276	136	adantr	|- ( ( ph /\ E = F ) -> ( ( ( * ` A ) x. ( D x. A ) ) - ( ( * ` D ) x. ( D x. A ) ) ) = ( -u ( D x. A ) x. ( * ` ( D - A ) ) ) )
277	218 219 198	mul32d	|- ( ( ph /\ E = F ) -> ( ( ( D - A ) x. ( * ` ( D - A ) ) ) x. D ) = ( ( ( D - A ) x. D ) x. ( * ` ( D - A ) ) ) )
278	198 215 198	subdird	|- ( ( ph /\ E = F ) -> ( ( D - A ) x. D ) = ( ( D x. D ) - ( A x. D ) ) )
279	198	sqvald	|- ( ( ph /\ E = F ) -> ( D ^ 2 ) = ( D x. D ) )
280	198 215	mulcomd	|- ( ( ph /\ E = F ) -> ( D x. A ) = ( A x. D ) )
281	279 280	oveq12d	|- ( ( ph /\ E = F ) -> ( ( D ^ 2 ) - ( D x. A ) ) = ( ( D x. D ) - ( A x. D ) ) )
282	278 281	eqtr4d	|- ( ( ph /\ E = F ) -> ( ( D - A ) x. D ) = ( ( D ^ 2 ) - ( D x. A ) ) )
283	282	oveq1d	|- ( ( ph /\ E = F ) -> ( ( ( D - A ) x. D ) x. ( * ` ( D - A ) ) ) = ( ( ( D ^ 2 ) - ( D x. A ) ) x. ( * ` ( D - A ) ) ) )
284	277 283	eqtrd	|- ( ( ph /\ E = F ) -> ( ( ( D - A ) x. ( * ` ( D - A ) ) ) x. D ) = ( ( ( D ^ 2 ) - ( D x. A ) ) x. ( * ` ( D - A ) ) ) )
285	276 284	oveq12d	|- ( ( ph /\ E = F ) -> ( ( ( ( * ` A ) x. ( D x. A ) ) - ( ( * ` D ) x. ( D x. A ) ) ) - ( ( ( D - A ) x. ( * ` ( D - A ) ) ) x. D ) ) = ( ( -u ( D x. A ) x. ( * ` ( D - A ) ) ) - ( ( ( D ^ 2 ) - ( D x. A ) ) x. ( * ` ( D - A ) ) ) ) )
286	268	negcld	|- ( ( ph /\ E = F ) -> -u ( D x. A ) e. CC )
287	261 268	subcld	|- ( ( ph /\ E = F ) -> ( ( D ^ 2 ) - ( D x. A ) ) e. CC )
288	286 287 219	subdird	|- ( ( ph /\ E = F ) -> ( ( -u ( D x. A ) - ( ( D ^ 2 ) - ( D x. A ) ) ) x. ( * ` ( D - A ) ) ) = ( ( -u ( D x. A ) x. ( * ` ( D - A ) ) ) - ( ( ( D ^ 2 ) - ( D x. A ) ) x. ( * ` ( D - A ) ) ) ) )
289	286 268	addcomd	|- ( ( ph /\ E = F ) -> ( -u ( D x. A ) + ( D x. A ) ) = ( ( D x. A ) + -u ( D x. A ) ) )
290	268 268	negsubd	|- ( ( ph /\ E = F ) -> ( ( D x. A ) + -u ( D x. A ) ) = ( ( D x. A ) - ( D x. A ) ) )
291	268	subidd	|- ( ( ph /\ E = F ) -> ( ( D x. A ) - ( D x. A ) ) = 0 )
292	289 290 291	3eqtrd	|- ( ( ph /\ E = F ) -> ( -u ( D x. A ) + ( D x. A ) ) = 0 )
293	292	oveq1d	|- ( ( ph /\ E = F ) -> ( ( -u ( D x. A ) + ( D x. A ) ) - ( D ^ 2 ) ) = ( 0 - ( D ^ 2 ) ) )
294	286 261 268	subsub3d	|- ( ( ph /\ E = F ) -> ( -u ( D x. A ) - ( ( D ^ 2 ) - ( D x. A ) ) ) = ( ( -u ( D x. A ) + ( D x. A ) ) - ( D ^ 2 ) ) )
295		df-neg	|- -u ( D ^ 2 ) = ( 0 - ( D ^ 2 ) )
296	295	a1i	|- ( ( ph /\ E = F ) -> -u ( D ^ 2 ) = ( 0 - ( D ^ 2 ) ) )
297	293 294 296	3eqtr4d	|- ( ( ph /\ E = F ) -> ( -u ( D x. A ) - ( ( D ^ 2 ) - ( D x. A ) ) ) = -u ( D ^ 2 ) )
298	297	oveq1d	|- ( ( ph /\ E = F ) -> ( ( -u ( D x. A ) - ( ( D ^ 2 ) - ( D x. A ) ) ) x. ( * ` ( D - A ) ) ) = ( -u ( D ^ 2 ) x. ( * ` ( D - A ) ) ) )
299	285 288 298	3eqtr2d	|- ( ( ph /\ E = F ) -> ( ( ( ( * ` A ) x. ( D x. A ) ) - ( ( * ` D ) x. ( D x. A ) ) ) - ( ( ( D - A ) x. ( * ` ( D - A ) ) ) x. D ) ) = ( -u ( D ^ 2 ) x. ( * ` ( D - A ) ) ) )
300	272 275 299	3eqtrd	|- ( ( ph /\ E = F ) -> ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) = ( -u ( D ^ 2 ) x. ( * ` ( D - A ) ) ) )
301	245	eqcomd	|- ( ( ph /\ E = F ) -> ( ( * ` D ) - ( * ` A ) ) = ( * ` ( D - A ) ) )
302	300 301	oveq12d	|- ( ( ph /\ E = F ) -> ( ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) / ( ( * ` D ) - ( * ` A ) ) ) = ( ( -u ( D ^ 2 ) x. ( * ` ( D - A ) ) ) / ( * ` ( D - A ) ) ) )
303	261	negcld	|- ( ( ph /\ E = F ) -> -u ( D ^ 2 ) e. CC )
304	303 219 250	divcan4d	|- ( ( ph /\ E = F ) -> ( ( -u ( D ^ 2 ) x. ( * ` ( D - A ) ) ) / ( * ` ( D - A ) ) ) = -u ( D ^ 2 ) )
305	302 304	eqtr2d	|- ( ( ph /\ E = F ) -> -u ( D ^ 2 ) = ( ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) / ( ( * ` D ) - ( * ` A ) ) ) )
306	261 305	negcon1ad	|- ( ( ph /\ E = F ) -> -u ( ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) / ( ( * ` D ) - ( * ` A ) ) ) = ( D ^ 2 ) )
307	15 306	eqtrid	|- ( ( ph /\ E = F ) -> N = ( D ^ 2 ) )
308	260 307	oveq12d	|- ( ( ph /\ E = F ) -> ( ( M x. X ) + N ) = ( -u ( 2 x. ( X x. D ) ) + ( D ^ 2 ) ) )
309	308	oveq2d	|- ( ( ph /\ E = F ) -> ( ( X ^ 2 ) + ( ( M x. X ) + N ) ) = ( ( X ^ 2 ) + ( -u ( 2 x. ( X x. D ) ) + ( D ^ 2 ) ) ) )
310	197	sqcld	|- ( ( ph /\ E = F ) -> ( X ^ 2 ) e. CC )
311	197 198	mulcld	|- ( ( ph /\ E = F ) -> ( X x. D ) e. CC )
312	247 311	mulcld	|- ( ( ph /\ E = F ) -> ( 2 x. ( X x. D ) ) e. CC )
313	312	negcld	|- ( ( ph /\ E = F ) -> -u ( 2 x. ( X x. D ) ) e. CC )
314	310 313 261	addassd	|- ( ( ph /\ E = F ) -> ( ( ( X ^ 2 ) + -u ( 2 x. ( X x. D ) ) ) + ( D ^ 2 ) ) = ( ( X ^ 2 ) + ( -u ( 2 x. ( X x. D ) ) + ( D ^ 2 ) ) ) )
315	310 312	negsubd	|- ( ( ph /\ E = F ) -> ( ( X ^ 2 ) + -u ( 2 x. ( X x. D ) ) ) = ( ( X ^ 2 ) - ( 2 x. ( X x. D ) ) ) )
316	315	oveq1d	|- ( ( ph /\ E = F ) -> ( ( ( X ^ 2 ) + -u ( 2 x. ( X x. D ) ) ) + ( D ^ 2 ) ) = ( ( ( X ^ 2 ) - ( 2 x. ( X x. D ) ) ) + ( D ^ 2 ) ) )
317	309 314 316	3eqtr2d	|- ( ( ph /\ E = F ) -> ( ( X ^ 2 ) + ( ( M x. X ) + N ) ) = ( ( ( X ^ 2 ) - ( 2 x. ( X x. D ) ) ) + ( D ^ 2 ) ) )
318		binom2sub	|- ( ( X e. CC /\ D e. CC ) -> ( ( X - D ) ^ 2 ) = ( ( ( X ^ 2 ) - ( 2 x. ( X x. D ) ) ) + ( D ^ 2 ) ) )
319	197 198 318	syl2anc	|- ( ( ph /\ E = F ) -> ( ( X - D ) ^ 2 ) = ( ( ( X ^ 2 ) - ( 2 x. ( X x. D ) ) ) + ( D ^ 2 ) ) )
320	204	sq0id	|- ( ( ph /\ E = F ) -> ( ( X - D ) ^ 2 ) = 0 )
321	317 319 320	3eqtr2d	|- ( ( ph /\ E = F ) -> ( ( X ^ 2 ) + ( ( M x. X ) + N ) ) = 0 )
322	1	adantr	|- ( ( ph /\ ( B =/= C /\ E =/= F ) ) -> S C_ CC )
323	2	adantr	|- ( ( ph /\ ( B =/= C /\ E =/= F ) ) -> A e. S )
324	3	adantr	|- ( ( ph /\ ( B =/= C /\ E =/= F ) ) -> B e. S )
325	4	adantr	|- ( ( ph /\ ( B =/= C /\ E =/= F ) ) -> C e. S )
326	5	adantr	|- ( ( ph /\ ( B =/= C /\ E =/= F ) ) -> D e. S )
327	6	adantr	|- ( ( ph /\ ( B =/= C /\ E =/= F ) ) -> E e. S )
328	7	adantr	|- ( ( ph /\ ( B =/= C /\ E =/= F ) ) -> F e. S )
329	8	adantr	|- ( ( ph /\ ( B =/= C /\ E =/= F ) ) -> X e. CC )
330	9	adantr	|- ( ( ph /\ ( B =/= C /\ E =/= F ) ) -> A =/= D )
331	10	adantr	|- ( ( ph /\ ( B =/= C /\ E =/= F ) ) -> ( abs ` ( X - A ) ) = ( abs ` ( B - C ) ) )
332	11	adantr	|- ( ( ph /\ ( B =/= C /\ E =/= F ) ) -> ( abs ` ( X - D ) ) = ( abs ` ( E - F ) ) )
333		simprl	|- ( ( ph /\ ( B =/= C /\ E =/= F ) ) -> B =/= C )
334		simprr	|- ( ( ph /\ ( B =/= C /\ E =/= F ) ) -> E =/= F )
335	322 323 324 325 326 327 328 329 330 331 332 12 13 14 15 333 334	constrrtcclem	|- ( ( ph /\ ( B =/= C /\ E =/= F ) ) -> ( ( X ^ 2 ) + ( ( M x. X ) + N ) ) = 0 )
336	181 321 335	pm2.61da2ne	|- ( ph -> ( ( X ^ 2 ) + ( ( M x. X ) + N ) ) = 0 )