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