Theorem constrrtcclem

Description: In the construction of constructible numbers, circle-circle intersections are roots of a quadratic equation. Case of non-degenerate circles. (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 ) ) )
	constrrtcclem.1	|- ( ph -> B =/= C )
	constrrtcclem.2	|- ( ph -> E =/= F )
Assertion	constrrtcclem	|- ( 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		constrrtcclem.1	|- ( ph -> B =/= C )
17		constrrtcclem.2	|- ( ph -> E =/= F )
18	8	sqcld	|- ( ph -> ( X ^ 2 ) e. CC )
19	1 6	sseldd	|- ( ph -> E e. CC )
20	1 7	sseldd	|- ( ph -> F e. CC )
21	19 20	subcld	|- ( ph -> ( E - F ) e. CC )
22	21	cjcld	|- ( ph -> ( * ` ( E - F ) ) e. CC )
23	21 22	mulcld	|- ( ph -> ( ( E - F ) x. ( * ` ( E - F ) ) ) e. CC )
24	13 23	eqeltrid	|- ( ph -> Q e. CC )
25	1 5	sseldd	|- ( ph -> D e. CC )
26	25	cjcld	|- ( ph -> ( * ` D ) e. CC )
27	1 2	sseldd	|- ( ph -> A e. CC )
28	25 27	addcld	|- ( ph -> ( D + A ) e. CC )
29	26 28	mulcld	|- ( ph -> ( ( * ` D ) x. ( D + A ) ) e. CC )
30	24 29	subcld	|- ( ph -> ( Q - ( ( * ` D ) x. ( D + A ) ) ) e. CC )
31	1 3	sseldd	|- ( ph -> B e. CC )
32	1 4	sseldd	|- ( ph -> C e. CC )
33	31 32	subcld	|- ( ph -> ( B - C ) e. CC )
34	33	cjcld	|- ( ph -> ( * ` ( B - C ) ) e. CC )
35	33 34	mulcld	|- ( ph -> ( ( B - C ) x. ( * ` ( B - C ) ) ) e. CC )
36	12 35	eqeltrid	|- ( ph -> P e. CC )
37	27	cjcld	|- ( ph -> ( * ` A ) e. CC )
38	37 28	mulcld	|- ( ph -> ( ( * ` A ) x. ( D + A ) ) e. CC )
39	36 38	subcld	|- ( ph -> ( P - ( ( * ` A ) x. ( D + A ) ) ) e. CC )
40	30 39	subcld	|- ( ph -> ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) e. CC )
41	26 37	subcld	|- ( ph -> ( ( * ` D ) - ( * ` A ) ) e. CC )
42	25 27	cjsubd	|- ( ph -> ( * ` ( D - A ) ) = ( ( * ` D ) - ( * ` A ) ) )
43	25 27	subcld	|- ( ph -> ( D - A ) e. CC )
44	9	necomd	|- ( ph -> D =/= A )
45	25 27 44	subne0d	|- ( ph -> ( D - A ) =/= 0 )
46	43 45	cjne0d	|- ( ph -> ( * ` ( D - A ) ) =/= 0 )
47	42 46	eqnetrrd	|- ( ph -> ( ( * ` D ) - ( * ` A ) ) =/= 0 )
48	40 41 47	divcld	|- ( ph -> ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) / ( ( * ` D ) - ( * ` A ) ) ) e. CC )
49	14 48	eqeltrid	|- ( ph -> M e. CC )
50	49 8	mulcld	|- ( ph -> ( M x. X ) e. CC )
51	25 27	mulcld	|- ( ph -> ( D x. A ) e. CC )
52	37 51	mulcld	|- ( ph -> ( ( * ` A ) x. ( D x. A ) ) e. CC )
53	36 25	mulcld	|- ( ph -> ( P x. D ) e. CC )
54	52 53	subcld	|- ( ph -> ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) e. CC )
55	26 51	mulcld	|- ( ph -> ( ( * ` D ) x. ( D x. A ) ) e. CC )
56	24 27	mulcld	|- ( ph -> ( Q x. A ) e. CC )
57	55 56	subcld	|- ( ph -> ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) e. CC )
58	54 57	subcld	|- ( ph -> ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) e. CC )
59	58 41 47	divcld	|- ( ph -> ( ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) / ( ( * ` D ) - ( * ` A ) ) ) e. CC )
60	59	negcld	|- ( ph -> -u ( ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) / ( ( * ` D ) - ( * ` A ) ) ) e. CC )
61	15 60	eqeltrid	|- ( ph -> N e. CC )
62	18 50 61	addassd	|- ( ph -> ( ( ( X ^ 2 ) + ( M x. X ) ) + N ) = ( ( X ^ 2 ) + ( ( M x. X ) + N ) ) )
63	41 18	mulcld	|- ( ph -> ( ( ( * ` D ) - ( * ` A ) ) x. ( X ^ 2 ) ) e. CC )
64	40 8	mulcld	|- ( ph -> ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) x. X ) e. CC )
65	26 37 18	subdird	|- ( ph -> ( ( ( * ` D ) - ( * ` A ) ) x. ( X ^ 2 ) ) = ( ( ( * ` D ) x. ( X ^ 2 ) ) - ( ( * ` A ) x. ( X ^ 2 ) ) ) )
66	30 39 8	subdird	|- ( ph -> ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) x. X ) = ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) x. X ) - ( ( P - ( ( * ` A ) x. ( D + A ) ) ) x. X ) ) )
67	65 66	oveq12d	|- ( ph -> ( ( ( ( * ` D ) - ( * ` A ) ) x. ( X ^ 2 ) ) + ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) x. X ) ) = ( ( ( ( * ` D ) x. ( X ^ 2 ) ) - ( ( * ` A ) x. ( X ^ 2 ) ) ) + ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) x. X ) - ( ( P - ( ( * ` A ) x. ( D + A ) ) ) x. X ) ) ) )
68	26 18	mulcld	|- ( ph -> ( ( * ` D ) x. ( X ^ 2 ) ) e. CC )
69	30 8	mulcld	|- ( ph -> ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) x. X ) e. CC )
70	37 18	mulcld	|- ( ph -> ( ( * ` A ) x. ( X ^ 2 ) ) e. CC )
71	39 8	mulcld	|- ( ph -> ( ( P - ( ( * ` A ) x. ( D + A ) ) ) x. X ) e. CC )
72	68 69 70 71	addsub4d	|- ( ph -> ( ( ( ( * ` D ) x. ( X ^ 2 ) ) + ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) x. X ) ) - ( ( ( * ` A ) x. ( X ^ 2 ) ) + ( ( P - ( ( * ` A ) x. ( D + A ) ) ) x. X ) ) ) = ( ( ( ( * ` D ) x. ( X ^ 2 ) ) - ( ( * ` A ) x. ( X ^ 2 ) ) ) + ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) x. X ) - ( ( P - ( ( * ` A ) x. ( D + A ) ) ) x. X ) ) ) )
73	8 27	subcld	|- ( ph -> ( X - A ) e. CC )
74	8 25	subcld	|- ( ph -> ( X - D ) e. CC )
75	73 74	mulcomd	|- ( ph -> ( ( X - A ) x. ( X - D ) ) = ( ( X - D ) x. ( X - A ) ) )
76	75	oveq2d	|- ( ph -> ( ( * ` X ) x. ( ( X - A ) x. ( X - D ) ) ) = ( ( * ` X ) x. ( ( X - D ) x. ( X - A ) ) ) )
77	73	cjcld	|- ( ph -> ( * ` ( X - A ) ) e. CC )
78	31 32 16	subne0d	|- ( ph -> ( B - C ) =/= 0 )
79	33 78	absne0d	|- ( ph -> ( abs ` ( B - C ) ) =/= 0 )
80	10 79	eqnetrd	|- ( ph -> ( abs ` ( X - A ) ) =/= 0 )
81	73	abs00ad	|- ( ph -> ( ( abs ` ( X - A ) ) = 0 <-> ( X - A ) = 0 ) )
82	81	necon3bid	|- ( ph -> ( ( abs ` ( X - A ) ) =/= 0 <-> ( X - A ) =/= 0 ) )
83	80 82	mpbid	|- ( ph -> ( X - A ) =/= 0 )
84	10	oveq1d	|- ( ph -> ( ( abs ` ( X - A ) ) ^ 2 ) = ( ( abs ` ( B - C ) ) ^ 2 ) )
85	73	absvalsqd	|- ( ph -> ( ( abs ` ( X - A ) ) ^ 2 ) = ( ( X - A ) x. ( * ` ( X - A ) ) ) )
86	33	absvalsqd	|- ( ph -> ( ( abs ` ( B - C ) ) ^ 2 ) = ( ( B - C ) x. ( * ` ( B - C ) ) ) )
87	84 85 86	3eqtr3d	|- ( ph -> ( ( X - A ) x. ( * ` ( X - A ) ) ) = ( ( B - C ) x. ( * ` ( B - C ) ) ) )
88	87 12	eqtr4di	|- ( ph -> ( ( X - A ) x. ( * ` ( X - A ) ) ) = P )
89	73 77 83 88	mvllmuld	|- ( ph -> ( * ` ( X - A ) ) = ( P / ( X - A ) ) )
90	89 77	eqeltrrd	|- ( ph -> ( P / ( X - A ) ) e. CC )
91	37 90	addcld	|- ( ph -> ( ( * ` A ) + ( P / ( X - A ) ) ) e. CC )
92	91 73 74	mulassd	|- ( ph -> ( ( ( ( * ` A ) + ( P / ( X - A ) ) ) x. ( X - A ) ) x. ( X - D ) ) = ( ( ( * ` A ) + ( P / ( X - A ) ) ) x. ( ( X - A ) x. ( X - D ) ) ) )
93	36 73 83	divcan1d	|- ( ph -> ( ( P / ( X - A ) ) x. ( X - A ) ) = P )
94	93	oveq2d	|- ( ph -> ( ( ( * ` A ) x. ( X - A ) ) + ( ( P / ( X - A ) ) x. ( X - A ) ) ) = ( ( ( * ` A ) x. ( X - A ) ) + P ) )
95	37 73 90 94	joinlmuladdmuld	|- ( ph -> ( ( ( * ` A ) + ( P / ( X - A ) ) ) x. ( X - A ) ) = ( ( ( * ` A ) x. ( X - A ) ) + P ) )
96	95	oveq1d	|- ( ph -> ( ( ( ( * ` A ) + ( P / ( X - A ) ) ) x. ( X - A ) ) x. ( X - D ) ) = ( ( ( ( * ` A ) x. ( X - A ) ) + P ) x. ( X - D ) ) )
97	37 73	mulcld	|- ( ph -> ( ( * ` A ) x. ( X - A ) ) e. CC )
98	97 36 74	adddird	|- ( ph -> ( ( ( ( * ` A ) x. ( X - A ) ) + P ) x. ( X - D ) ) = ( ( ( ( * ` A ) x. ( X - A ) ) x. ( X - D ) ) + ( P x. ( X - D ) ) ) )
99	37 73 74	mulassd	|- ( ph -> ( ( ( * ` A ) x. ( X - A ) ) x. ( X - D ) ) = ( ( * ` A ) x. ( ( X - A ) x. ( X - D ) ) ) )
100	8 27 8 25	mulsubd	|- ( ph -> ( ( X - A ) x. ( X - D ) ) = ( ( ( X x. X ) + ( D x. A ) ) - ( ( X x. D ) + ( X x. A ) ) ) )
101	8	sqvald	|- ( ph -> ( X ^ 2 ) = ( X x. X ) )
102	101	oveq1d	|- ( ph -> ( ( X ^ 2 ) + ( D x. A ) ) = ( ( X x. X ) + ( D x. A ) ) )
103	8 25 27	adddid	|- ( ph -> ( X x. ( D + A ) ) = ( ( X x. D ) + ( X x. A ) ) )
104	102 103	oveq12d	|- ( ph -> ( ( ( X ^ 2 ) + ( D x. A ) ) - ( X x. ( D + A ) ) ) = ( ( ( X x. X ) + ( D x. A ) ) - ( ( X x. D ) + ( X x. A ) ) ) )
105	8 28	mulcld	|- ( ph -> ( X x. ( D + A ) ) e. CC )
106	18 51 105	addsubd	|- ( ph -> ( ( ( X ^ 2 ) + ( D x. A ) ) - ( X x. ( D + A ) ) ) = ( ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) + ( D x. A ) ) )
107	100 104 106	3eqtr2d	|- ( ph -> ( ( X - A ) x. ( X - D ) ) = ( ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) + ( D x. A ) ) )
108	107	oveq2d	|- ( ph -> ( ( * ` A ) x. ( ( X - A ) x. ( X - D ) ) ) = ( ( * ` A ) x. ( ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) + ( D x. A ) ) ) )
109	18 105	subcld	|- ( ph -> ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) e. CC )
110	37 109 51	adddid	|- ( ph -> ( ( * ` A ) x. ( ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) + ( D x. A ) ) ) = ( ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( ( * ` A ) x. ( D x. A ) ) ) )
111	99 108 110	3eqtrd	|- ( ph -> ( ( ( * ` A ) x. ( X - A ) ) x. ( X - D ) ) = ( ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( ( * ` A ) x. ( D x. A ) ) ) )
112	36 8 25	subdid	|- ( ph -> ( P x. ( X - D ) ) = ( ( P x. X ) - ( P x. D ) ) )
113	111 112	oveq12d	|- ( ph -> ( ( ( ( * ` A ) x. ( X - A ) ) x. ( X - D ) ) + ( P x. ( X - D ) ) ) = ( ( ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( ( * ` A ) x. ( D x. A ) ) ) + ( ( P x. X ) - ( P x. D ) ) ) )
114	96 98 113	3eqtrd	|- ( ph -> ( ( ( ( * ` A ) + ( P / ( X - A ) ) ) x. ( X - A ) ) x. ( X - D ) ) = ( ( ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( ( * ` A ) x. ( D x. A ) ) ) + ( ( P x. X ) - ( P x. D ) ) ) )
115	8 27	cjsubd	|- ( ph -> ( * ` ( X - A ) ) = ( ( * ` X ) - ( * ` A ) ) )
116	115 89	eqtr3d	|- ( ph -> ( ( * ` X ) - ( * ` A ) ) = ( P / ( X - A ) ) )
117	8	cjcld	|- ( ph -> ( * ` X ) e. CC )
118	117 37 90	subaddd	|- ( ph -> ( ( ( * ` X ) - ( * ` A ) ) = ( P / ( X - A ) ) <-> ( ( * ` A ) + ( P / ( X - A ) ) ) = ( * ` X ) ) )
119	116 118	mpbid	|- ( ph -> ( ( * ` A ) + ( P / ( X - A ) ) ) = ( * ` X ) )
120	119	oveq1d	|- ( ph -> ( ( ( * ` A ) + ( P / ( X - A ) ) ) x. ( ( X - A ) x. ( X - D ) ) ) = ( ( * ` X ) x. ( ( X - A ) x. ( X - D ) ) ) )
121	92 114 120	3eqtr3rd	|- ( ph -> ( ( * ` X ) x. ( ( X - A ) x. ( X - D ) ) ) = ( ( ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( ( * ` A ) x. ( D x. A ) ) ) + ( ( P x. X ) - ( P x. D ) ) ) )
122	37 109	mulcld	|- ( ph -> ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) e. CC )
123	122 52	addcld	|- ( ph -> ( ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( ( * ` A ) x. ( D x. A ) ) ) e. CC )
124	36 8	mulcld	|- ( ph -> ( P x. X ) e. CC )
125	123 124 53	addsubassd	|- ( ph -> ( ( ( ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( ( * ` A ) x. ( D x. A ) ) ) + ( P x. X ) ) - ( P x. D ) ) = ( ( ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( ( * ` A ) x. ( D x. A ) ) ) + ( ( P x. X ) - ( P x. D ) ) ) )
126	122 52 124	add32d	|- ( ph -> ( ( ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( ( * ` A ) x. ( D x. A ) ) ) + ( P x. X ) ) = ( ( ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( P x. X ) ) + ( ( * ` A ) x. ( D x. A ) ) ) )
127	126	oveq1d	|- ( ph -> ( ( ( ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( ( * ` A ) x. ( D x. A ) ) ) + ( P x. X ) ) - ( P x. D ) ) = ( ( ( ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( P x. X ) ) + ( ( * ` A ) x. ( D x. A ) ) ) - ( P x. D ) ) )
128	121 125 127	3eqtr2d	|- ( ph -> ( ( * ` X ) x. ( ( X - A ) x. ( X - D ) ) ) = ( ( ( ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( P x. X ) ) + ( ( * ` A ) x. ( D x. A ) ) ) - ( P x. D ) ) )
129	122 124	addcld	|- ( ph -> ( ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( P x. X ) ) e. CC )
130	129 52 53	addsubassd	|- ( ph -> ( ( ( ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( P x. X ) ) + ( ( * ` A ) x. ( D x. A ) ) ) - ( P x. D ) ) = ( ( ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( P x. X ) ) + ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) ) )
131	38 8	mulcld	|- ( ph -> ( ( ( * ` A ) x. ( D + A ) ) x. X ) e. CC )
132	70 131 124	subadd23d	|- ( ph -> ( ( ( ( * ` A ) x. ( X ^ 2 ) ) - ( ( ( * ` A ) x. ( D + A ) ) x. X ) ) + ( P x. X ) ) = ( ( ( * ` A ) x. ( X ^ 2 ) ) + ( ( P x. X ) - ( ( ( * ` A ) x. ( D + A ) ) x. X ) ) ) )
133	37 18 105	subdid	|- ( ph -> ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) = ( ( ( * ` A ) x. ( X ^ 2 ) ) - ( ( * ` A ) x. ( X x. ( D + A ) ) ) ) )
134	37 8 28	mul12d	|- ( ph -> ( ( * ` A ) x. ( X x. ( D + A ) ) ) = ( X x. ( ( * ` A ) x. ( D + A ) ) ) )
135	8 38	mulcomd	|- ( ph -> ( X x. ( ( * ` A ) x. ( D + A ) ) ) = ( ( ( * ` A ) x. ( D + A ) ) x. X ) )
136	134 135	eqtrd	|- ( ph -> ( ( * ` A ) x. ( X x. ( D + A ) ) ) = ( ( ( * ` A ) x. ( D + A ) ) x. X ) )
137	136	oveq2d	|- ( ph -> ( ( ( * ` A ) x. ( X ^ 2 ) ) - ( ( * ` A ) x. ( X x. ( D + A ) ) ) ) = ( ( ( * ` A ) x. ( X ^ 2 ) ) - ( ( ( * ` A ) x. ( D + A ) ) x. X ) ) )
138	133 137	eqtrd	|- ( ph -> ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) = ( ( ( * ` A ) x. ( X ^ 2 ) ) - ( ( ( * ` A ) x. ( D + A ) ) x. X ) ) )
139	138	oveq1d	|- ( ph -> ( ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( P x. X ) ) = ( ( ( ( * ` A ) x. ( X ^ 2 ) ) - ( ( ( * ` A ) x. ( D + A ) ) x. X ) ) + ( P x. X ) ) )
140	36 38 8	subdird	|- ( ph -> ( ( P - ( ( * ` A ) x. ( D + A ) ) ) x. X ) = ( ( P x. X ) - ( ( ( * ` A ) x. ( D + A ) ) x. X ) ) )
141	140	oveq2d	|- ( ph -> ( ( ( * ` A ) x. ( X ^ 2 ) ) + ( ( P - ( ( * ` A ) x. ( D + A ) ) ) x. X ) ) = ( ( ( * ` A ) x. ( X ^ 2 ) ) + ( ( P x. X ) - ( ( ( * ` A ) x. ( D + A ) ) x. X ) ) ) )
142	132 139 141	3eqtr4d	|- ( ph -> ( ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( P x. X ) ) = ( ( ( * ` A ) x. ( X ^ 2 ) ) + ( ( P - ( ( * ` A ) x. ( D + A ) ) ) x. X ) ) )
143	142	oveq1d	|- ( ph -> ( ( ( ( * ` A ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( P x. X ) ) + ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) ) = ( ( ( ( * ` A ) x. ( X ^ 2 ) ) + ( ( P - ( ( * ` A ) x. ( D + A ) ) ) x. X ) ) + ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) ) )
144	128 130 143	3eqtrd	|- ( ph -> ( ( * ` X ) x. ( ( X - A ) x. ( X - D ) ) ) = ( ( ( ( * ` A ) x. ( X ^ 2 ) ) + ( ( P - ( ( * ` A ) x. ( D + A ) ) ) x. X ) ) + ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) ) )
145	74	cjcld	|- ( ph -> ( * ` ( X - D ) ) e. CC )
146	19 20 17	subne0d	|- ( ph -> ( E - F ) =/= 0 )
147	21 146	absne0d	|- ( ph -> ( abs ` ( E - F ) ) =/= 0 )
148	11 147	eqnetrd	|- ( ph -> ( abs ` ( X - D ) ) =/= 0 )
149	74	abs00ad	|- ( ph -> ( ( abs ` ( X - D ) ) = 0 <-> ( X - D ) = 0 ) )
150	149	necon3bid	|- ( ph -> ( ( abs ` ( X - D ) ) =/= 0 <-> ( X - D ) =/= 0 ) )
151	148 150	mpbid	|- ( ph -> ( X - D ) =/= 0 )
152	11	oveq1d	|- ( ph -> ( ( abs ` ( X - D ) ) ^ 2 ) = ( ( abs ` ( E - F ) ) ^ 2 ) )
153	74	absvalsqd	|- ( ph -> ( ( abs ` ( X - D ) ) ^ 2 ) = ( ( X - D ) x. ( * ` ( X - D ) ) ) )
154	21	absvalsqd	|- ( ph -> ( ( abs ` ( E - F ) ) ^ 2 ) = ( ( E - F ) x. ( * ` ( E - F ) ) ) )
155	152 153 154	3eqtr3d	|- ( ph -> ( ( X - D ) x. ( * ` ( X - D ) ) ) = ( ( E - F ) x. ( * ` ( E - F ) ) ) )
156	155 13	eqtr4di	|- ( ph -> ( ( X - D ) x. ( * ` ( X - D ) ) ) = Q )
157	74 145 151 156	mvllmuld	|- ( ph -> ( * ` ( X - D ) ) = ( Q / ( X - D ) ) )
158	157 145	eqeltrrd	|- ( ph -> ( Q / ( X - D ) ) e. CC )
159	26 158	addcld	|- ( ph -> ( ( * ` D ) + ( Q / ( X - D ) ) ) e. CC )
160	159 74 73	mulassd	|- ( ph -> ( ( ( ( * ` D ) + ( Q / ( X - D ) ) ) x. ( X - D ) ) x. ( X - A ) ) = ( ( ( * ` D ) + ( Q / ( X - D ) ) ) x. ( ( X - D ) x. ( X - A ) ) ) )
161	24 74 151	divcan1d	|- ( ph -> ( ( Q / ( X - D ) ) x. ( X - D ) ) = Q )
162	161	oveq2d	|- ( ph -> ( ( ( * ` D ) x. ( X - D ) ) + ( ( Q / ( X - D ) ) x. ( X - D ) ) ) = ( ( ( * ` D ) x. ( X - D ) ) + Q ) )
163	26 74 158 162	joinlmuladdmuld	|- ( ph -> ( ( ( * ` D ) + ( Q / ( X - D ) ) ) x. ( X - D ) ) = ( ( ( * ` D ) x. ( X - D ) ) + Q ) )
164	163	oveq1d	|- ( ph -> ( ( ( ( * ` D ) + ( Q / ( X - D ) ) ) x. ( X - D ) ) x. ( X - A ) ) = ( ( ( ( * ` D ) x. ( X - D ) ) + Q ) x. ( X - A ) ) )
165	26 74	mulcld	|- ( ph -> ( ( * ` D ) x. ( X - D ) ) e. CC )
166	165 24 73	adddird	|- ( ph -> ( ( ( ( * ` D ) x. ( X - D ) ) + Q ) x. ( X - A ) ) = ( ( ( ( * ` D ) x. ( X - D ) ) x. ( X - A ) ) + ( Q x. ( X - A ) ) ) )
167	26 74 73	mulassd	|- ( ph -> ( ( ( * ` D ) x. ( X - D ) ) x. ( X - A ) ) = ( ( * ` D ) x. ( ( X - D ) x. ( X - A ) ) ) )
168	75	oveq2d	|- ( ph -> ( ( * ` D ) x. ( ( X - A ) x. ( X - D ) ) ) = ( ( * ` D ) x. ( ( X - D ) x. ( X - A ) ) ) )
169	167 168	eqtr4d	|- ( ph -> ( ( ( * ` D ) x. ( X - D ) ) x. ( X - A ) ) = ( ( * ` D ) x. ( ( X - A ) x. ( X - D ) ) ) )
170	107	oveq2d	|- ( ph -> ( ( * ` D ) x. ( ( X - A ) x. ( X - D ) ) ) = ( ( * ` D ) x. ( ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) + ( D x. A ) ) ) )
171	26 109 51	adddid	|- ( ph -> ( ( * ` D ) x. ( ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) + ( D x. A ) ) ) = ( ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( ( * ` D ) x. ( D x. A ) ) ) )
172	169 170 171	3eqtrd	|- ( ph -> ( ( ( * ` D ) x. ( X - D ) ) x. ( X - A ) ) = ( ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( ( * ` D ) x. ( D x. A ) ) ) )
173	24 8 27	subdid	|- ( ph -> ( Q x. ( X - A ) ) = ( ( Q x. X ) - ( Q x. A ) ) )
174	172 173	oveq12d	|- ( ph -> ( ( ( ( * ` D ) x. ( X - D ) ) x. ( X - A ) ) + ( Q x. ( X - A ) ) ) = ( ( ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( ( * ` D ) x. ( D x. A ) ) ) + ( ( Q x. X ) - ( Q x. A ) ) ) )
175	164 166 174	3eqtrd	|- ( ph -> ( ( ( ( * ` D ) + ( Q / ( X - D ) ) ) x. ( X - D ) ) x. ( X - A ) ) = ( ( ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( ( * ` D ) x. ( D x. A ) ) ) + ( ( Q x. X ) - ( Q x. A ) ) ) )
176	8 25	cjsubd	|- ( ph -> ( * ` ( X - D ) ) = ( ( * ` X ) - ( * ` D ) ) )
177	176 157	eqtr3d	|- ( ph -> ( ( * ` X ) - ( * ` D ) ) = ( Q / ( X - D ) ) )
178	117 26 158	subaddd	|- ( ph -> ( ( ( * ` X ) - ( * ` D ) ) = ( Q / ( X - D ) ) <-> ( ( * ` D ) + ( Q / ( X - D ) ) ) = ( * ` X ) ) )
179	177 178	mpbid	|- ( ph -> ( ( * ` D ) + ( Q / ( X - D ) ) ) = ( * ` X ) )
180	179	oveq1d	|- ( ph -> ( ( ( * ` D ) + ( Q / ( X - D ) ) ) x. ( ( X - D ) x. ( X - A ) ) ) = ( ( * ` X ) x. ( ( X - D ) x. ( X - A ) ) ) )
181	160 175 180	3eqtr3rd	|- ( ph -> ( ( * ` X ) x. ( ( X - D ) x. ( X - A ) ) ) = ( ( ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( ( * ` D ) x. ( D x. A ) ) ) + ( ( Q x. X ) - ( Q x. A ) ) ) )
182	26 109	mulcld	|- ( ph -> ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) e. CC )
183	182 55	addcld	|- ( ph -> ( ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( ( * ` D ) x. ( D x. A ) ) ) e. CC )
184	24 8	mulcld	|- ( ph -> ( Q x. X ) e. CC )
185	183 184 56	addsubassd	|- ( ph -> ( ( ( ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( ( * ` D ) x. ( D x. A ) ) ) + ( Q x. X ) ) - ( Q x. A ) ) = ( ( ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( ( * ` D ) x. ( D x. A ) ) ) + ( ( Q x. X ) - ( Q x. A ) ) ) )
186	182 55 184	add32d	|- ( ph -> ( ( ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( ( * ` D ) x. ( D x. A ) ) ) + ( Q x. X ) ) = ( ( ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( Q x. X ) ) + ( ( * ` D ) x. ( D x. A ) ) ) )
187	186	oveq1d	|- ( ph -> ( ( ( ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( ( * ` D ) x. ( D x. A ) ) ) + ( Q x. X ) ) - ( Q x. A ) ) = ( ( ( ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( Q x. X ) ) + ( ( * ` D ) x. ( D x. A ) ) ) - ( Q x. A ) ) )
188	181 185 187	3eqtr2d	|- ( ph -> ( ( * ` X ) x. ( ( X - D ) x. ( X - A ) ) ) = ( ( ( ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( Q x. X ) ) + ( ( * ` D ) x. ( D x. A ) ) ) - ( Q x. A ) ) )
189	182 184	addcld	|- ( ph -> ( ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( Q x. X ) ) e. CC )
190	189 55 56	addsubassd	|- ( ph -> ( ( ( ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( Q x. X ) ) + ( ( * ` D ) x. ( D x. A ) ) ) - ( Q x. A ) ) = ( ( ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( Q x. X ) ) + ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) )
191	29 8	mulcld	|- ( ph -> ( ( ( * ` D ) x. ( D + A ) ) x. X ) e. CC )
192	68 191 184	subadd23d	|- ( ph -> ( ( ( ( * ` D ) x. ( X ^ 2 ) ) - ( ( ( * ` D ) x. ( D + A ) ) x. X ) ) + ( Q x. X ) ) = ( ( ( * ` D ) x. ( X ^ 2 ) ) + ( ( Q x. X ) - ( ( ( * ` D ) x. ( D + A ) ) x. X ) ) ) )
193	26 18 105	subdid	|- ( ph -> ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) = ( ( ( * ` D ) x. ( X ^ 2 ) ) - ( ( * ` D ) x. ( X x. ( D + A ) ) ) ) )
194	26 8 28	mul12d	|- ( ph -> ( ( * ` D ) x. ( X x. ( D + A ) ) ) = ( X x. ( ( * ` D ) x. ( D + A ) ) ) )
195	8 29	mulcomd	|- ( ph -> ( X x. ( ( * ` D ) x. ( D + A ) ) ) = ( ( ( * ` D ) x. ( D + A ) ) x. X ) )
196	194 195	eqtrd	|- ( ph -> ( ( * ` D ) x. ( X x. ( D + A ) ) ) = ( ( ( * ` D ) x. ( D + A ) ) x. X ) )
197	196	oveq2d	|- ( ph -> ( ( ( * ` D ) x. ( X ^ 2 ) ) - ( ( * ` D ) x. ( X x. ( D + A ) ) ) ) = ( ( ( * ` D ) x. ( X ^ 2 ) ) - ( ( ( * ` D ) x. ( D + A ) ) x. X ) ) )
198	193 197	eqtrd	|- ( ph -> ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) = ( ( ( * ` D ) x. ( X ^ 2 ) ) - ( ( ( * ` D ) x. ( D + A ) ) x. X ) ) )
199	198	oveq1d	|- ( ph -> ( ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( Q x. X ) ) = ( ( ( ( * ` D ) x. ( X ^ 2 ) ) - ( ( ( * ` D ) x. ( D + A ) ) x. X ) ) + ( Q x. X ) ) )
200	24 29 8	subdird	|- ( ph -> ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) x. X ) = ( ( Q x. X ) - ( ( ( * ` D ) x. ( D + A ) ) x. X ) ) )
201	200	oveq2d	|- ( ph -> ( ( ( * ` D ) x. ( X ^ 2 ) ) + ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) x. X ) ) = ( ( ( * ` D ) x. ( X ^ 2 ) ) + ( ( Q x. X ) - ( ( ( * ` D ) x. ( D + A ) ) x. X ) ) ) )
202	192 199 201	3eqtr4d	|- ( ph -> ( ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( Q x. X ) ) = ( ( ( * ` D ) x. ( X ^ 2 ) ) + ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) x. X ) ) )
203	202	oveq1d	|- ( ph -> ( ( ( ( * ` D ) x. ( ( X ^ 2 ) - ( X x. ( D + A ) ) ) ) + ( Q x. X ) ) + ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) = ( ( ( ( * ` D ) x. ( X ^ 2 ) ) + ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) x. X ) ) + ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) )
204	188 190 203	3eqtrd	|- ( ph -> ( ( * ` X ) x. ( ( X - D ) x. ( X - A ) ) ) = ( ( ( ( * ` D ) x. ( X ^ 2 ) ) + ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) x. X ) ) + ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) )
205	76 144 204	3eqtr3d	|- ( ph -> ( ( ( ( * ` A ) x. ( X ^ 2 ) ) + ( ( P - ( ( * ` A ) x. ( D + A ) ) ) x. X ) ) + ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) ) = ( ( ( ( * ` D ) x. ( X ^ 2 ) ) + ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) x. X ) ) + ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) )
206	142 129	eqeltrrd	|- ( ph -> ( ( ( * ` A ) x. ( X ^ 2 ) ) + ( ( P - ( ( * ` A ) x. ( D + A ) ) ) x. X ) ) e. CC )
207	202 189	eqeltrrd	|- ( ph -> ( ( ( * ` D ) x. ( X ^ 2 ) ) + ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) x. X ) ) e. CC )
208	206 54 207 57	addsubeq4d	|- ( ph -> ( ( ( ( ( * ` A ) x. ( X ^ 2 ) ) + ( ( P - ( ( * ` A ) x. ( D + A ) ) ) x. X ) ) + ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) ) = ( ( ( ( * ` D ) x. ( X ^ 2 ) ) + ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) x. X ) ) + ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) <-> ( ( ( ( * ` D ) x. ( X ^ 2 ) ) + ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) x. X ) ) - ( ( ( * ` A ) x. ( X ^ 2 ) ) + ( ( P - ( ( * ` A ) x. ( D + A ) ) ) x. X ) ) ) = ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) ) )
209	205 208	mpbid	|- ( ph -> ( ( ( ( * ` D ) x. ( X ^ 2 ) ) + ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) x. X ) ) - ( ( ( * ` A ) x. ( X ^ 2 ) ) + ( ( P - ( ( * ` A ) x. ( D + A ) ) ) x. X ) ) ) = ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) )
210	67 72 209	3eqtr2d	|- ( ph -> ( ( ( ( * ` D ) - ( * ` A ) ) x. ( X ^ 2 ) ) + ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) x. X ) ) = ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) )
211	63 64 210	mvlraddd	|- ( ph -> ( ( ( * ` D ) - ( * ` A ) ) x. ( X ^ 2 ) ) = ( ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) - ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) x. X ) ) )
212	41 18 47 211	mvllmuld	|- ( ph -> ( X ^ 2 ) = ( ( ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) - ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) x. X ) ) / ( ( * ` D ) - ( * ` A ) ) ) )
213	58 64 41 47	divsubdird	|- ( ph -> ( ( ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) - ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) x. X ) ) / ( ( * ` D ) - ( * ` A ) ) ) = ( ( ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) / ( ( * ` D ) - ( * ` A ) ) ) - ( ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) x. X ) / ( ( * ` D ) - ( * ` A ) ) ) ) )
214	15	eqcomi	|- -u ( ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) / ( ( * ` D ) - ( * ` A ) ) ) = N
215	214	a1i	|- ( ph -> -u ( ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) / ( ( * ` D ) - ( * ` A ) ) ) = N )
216	59 215	negcon1ad	|- ( ph -> -u N = ( ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) / ( ( * ` D ) - ( * ` A ) ) ) )
217	216	oveq1d	|- ( ph -> ( -u N - ( ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) x. X ) / ( ( * ` D ) - ( * ` A ) ) ) ) = ( ( ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) / ( ( * ` D ) - ( * ` A ) ) ) - ( ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) x. X ) / ( ( * ` D ) - ( * ` A ) ) ) ) )
218	213 217	eqtr4d	|- ( ph -> ( ( ( ( ( ( * ` A ) x. ( D x. A ) ) - ( P x. D ) ) - ( ( ( * ` D ) x. ( D x. A ) ) - ( Q x. A ) ) ) - ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) x. X ) ) / ( ( * ` D ) - ( * ` A ) ) ) = ( -u N - ( ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) x. X ) / ( ( * ` D ) - ( * ` A ) ) ) ) )
219	40 8 41 47	div23d	|- ( ph -> ( ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) x. X ) / ( ( * ` D ) - ( * ` A ) ) ) = ( ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) / ( ( * ` D ) - ( * ` A ) ) ) x. X ) )
220	14	oveq1i	|- ( M x. X ) = ( ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) / ( ( * ` D ) - ( * ` A ) ) ) x. X )
221	219 220	eqtr4di	|- ( ph -> ( ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) x. X ) / ( ( * ` D ) - ( * ` A ) ) ) = ( M x. X ) )
222	221	oveq2d	|- ( ph -> ( -u N - ( ( ( ( Q - ( ( * ` D ) x. ( D + A ) ) ) - ( P - ( ( * ` A ) x. ( D + A ) ) ) ) x. X ) / ( ( * ` D ) - ( * ` A ) ) ) ) = ( -u N - ( M x. X ) ) )
223	212 218 222	3eqtrd	|- ( ph -> ( X ^ 2 ) = ( -u N - ( M x. X ) ) )
224	216 59	eqeltrd	|- ( ph -> -u N e. CC )
225	18 50 224	addlsub	|- ( ph -> ( ( ( X ^ 2 ) + ( M x. X ) ) = -u N <-> ( X ^ 2 ) = ( -u N - ( M x. X ) ) ) )
226	223 225	mpbird	|- ( ph -> ( ( X ^ 2 ) + ( M x. X ) ) = -u N )
227	18 50	addcld	|- ( ph -> ( ( X ^ 2 ) + ( M x. X ) ) e. CC )
228		addeq0	|- ( ( ( ( X ^ 2 ) + ( M x. X ) ) e. CC /\ N e. CC ) -> ( ( ( ( X ^ 2 ) + ( M x. X ) ) + N ) = 0 <-> ( ( X ^ 2 ) + ( M x. X ) ) = -u N ) )
229	227 61 228	syl2anc	|- ( ph -> ( ( ( ( X ^ 2 ) + ( M x. X ) ) + N ) = 0 <-> ( ( X ^ 2 ) + ( M x. X ) ) = -u N ) )
230	226 229	mpbird	|- ( ph -> ( ( ( X ^ 2 ) + ( M x. X ) ) + N ) = 0 )
231	62 230	eqtr3d	|- ( ph -> ( ( X ^ 2 ) + ( ( M x. X ) + N ) ) = 0 )