Theorem constrrtlc1

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

	Ref	Expression
Hypotheses	constrrtlc.s	|- ( ph -> S C_ CC )
	constrrtlc.a	|- ( ph -> A e. S )
	constrrtlc.b	|- ( ph -> B e. S )
	constrrtlc.c	|- ( ph -> C e. S )
	constrrtlc.e	|- ( ph -> E e. S )
	constrrtlc.f	|- ( ph -> F e. S )
	constrrtlc.t	|- ( ph -> T e. RR )
	constrrtlc.1	|- ( ph -> X = ( A + ( T x. ( B - A ) ) ) )
	constrrtlc.2	|- ( ph -> ( abs ` ( X - C ) ) = ( abs ` ( E - F ) ) )
	constrrtlc.q	|- Q = ( ( ( * ` B ) - ( * ` A ) ) / ( B - A ) )
	constrrtlc.m	|- M = ( ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) / Q )
	constrrtlc.n	|- N = ( -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) / Q )
	constrrtlc1.1	|- ( ph -> A =/= B )
Assertion	constrrtlc1	|- ( ph -> ( ( ( X ^ 2 ) + ( ( M x. X ) + N ) ) = 0 /\ Q =/= 0 ) )

Proof

Step	Hyp	Ref	Expression
1		constrrtlc.s	|- ( ph -> S C_ CC )
2		constrrtlc.a	|- ( ph -> A e. S )
3		constrrtlc.b	|- ( ph -> B e. S )
4		constrrtlc.c	|- ( ph -> C e. S )
5		constrrtlc.e	|- ( ph -> E e. S )
6		constrrtlc.f	|- ( ph -> F e. S )
7		constrrtlc.t	|- ( ph -> T e. RR )
8		constrrtlc.1	|- ( ph -> X = ( A + ( T x. ( B - A ) ) ) )
9		constrrtlc.2	|- ( ph -> ( abs ` ( X - C ) ) = ( abs ` ( E - F ) ) )
10		constrrtlc.q	|- Q = ( ( ( * ` B ) - ( * ` A ) ) / ( B - A ) )
11		constrrtlc.m	|- M = ( ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) / Q )
12		constrrtlc.n	|- N = ( -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) / Q )
13		constrrtlc1.1	|- ( ph -> A =/= B )
14	1 2	sseldd	|- ( ph -> A e. CC )
15	14	cjcld	|- ( ph -> ( * ` A ) e. CC )
16	1 3	sseldd	|- ( ph -> B e. CC )
17	16	cjcld	|- ( ph -> ( * ` B ) e. CC )
18	17 15	subcld	|- ( ph -> ( ( * ` B ) - ( * ` A ) ) e. CC )
19	16 14	subcld	|- ( ph -> ( B - A ) e. CC )
20	13	necomd	|- ( ph -> B =/= A )
21	16 14 20	subne0d	|- ( ph -> ( B - A ) =/= 0 )
22	18 19 21	divcld	|- ( ph -> ( ( ( * ` B ) - ( * ` A ) ) / ( B - A ) ) e. CC )
23	10 22	eqeltrid	|- ( ph -> Q e. CC )
24	14 23	mulcld	|- ( ph -> ( A x. Q ) e. CC )
25	15 24	subcld	|- ( ph -> ( ( * ` A ) - ( A x. Q ) ) e. CC )
26	1 4	sseldd	|- ( ph -> C e. CC )
27	26	cjcld	|- ( ph -> ( * ` C ) e. CC )
28	25 27	subcld	|- ( ph -> ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) e. CC )
29	26 23	mulcld	|- ( ph -> ( C x. Q ) e. CC )
30	28 29	subcld	|- ( ph -> ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) e. CC )
31	16 14	cjsubd	|- ( ph -> ( * ` ( B - A ) ) = ( ( * ` B ) - ( * ` A ) ) )
32	19 21	cjne0d	|- ( ph -> ( * ` ( B - A ) ) =/= 0 )
33	31 32	eqnetrrd	|- ( ph -> ( ( * ` B ) - ( * ` A ) ) =/= 0 )
34	18 19 33 21	divne0d	|- ( ph -> ( ( ( * ` B ) - ( * ` A ) ) / ( B - A ) ) =/= 0 )
35	10	neeq1i	|- ( Q =/= 0 <-> ( ( ( * ` B ) - ( * ` A ) ) / ( B - A ) ) =/= 0 )
36	34 35	sylibr	|- ( ph -> Q =/= 0 )
37	30 23 36	divcld	|- ( ph -> ( ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) / Q ) e. CC )
38	7	recnd	|- ( ph -> T e. CC )
39	38 19	mulcld	|- ( ph -> ( T x. ( B - A ) ) e. CC )
40	14 39	addcld	|- ( ph -> ( A + ( T x. ( B - A ) ) ) e. CC )
41	8 40	eqeltrd	|- ( ph -> X e. CC )
42	37 41	mulcomd	|- ( ph -> ( ( ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) / Q ) x. X ) = ( X x. ( ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) / Q ) ) )
43	11	a1i	|- ( ph -> M = ( ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) / Q ) )
44	43	oveq1d	|- ( ph -> ( M x. X ) = ( ( ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) / Q ) x. X ) )
45	41 30 23 36	divassd	|- ( ph -> ( ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) / Q ) = ( X x. ( ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) / Q ) ) )
46	42 44 45	3eqtr4d	|- ( ph -> ( M x. X ) = ( ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) / Q ) )
47	12	a1i	|- ( ph -> N = ( -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) / Q ) )
48	46 47	oveq12d	|- ( ph -> ( ( M x. X ) + N ) = ( ( ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) / Q ) + ( -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) / Q ) ) )
49	41 30	mulcld	|- ( ph -> ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) e. CC )
50	26 28	mulcld	|- ( ph -> ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) e. CC )
51	41	sqvald	|- ( ph -> ( X ^ 2 ) = ( X x. X ) )
52	51	oveq1d	|- ( ph -> ( ( X ^ 2 ) x. Q ) = ( ( X x. X ) x. Q ) )
53	41 41 23	mulassd	|- ( ph -> ( ( X x. X ) x. Q ) = ( X x. ( X x. Q ) ) )
54	52 53	eqtrd	|- ( ph -> ( ( X ^ 2 ) x. Q ) = ( X x. ( X x. Q ) ) )
55	41 23	mulcld	|- ( ph -> ( X x. Q ) e. CC )
56	41 55	mulcld	|- ( ph -> ( X x. ( X x. Q ) ) e. CC )
57	54 56	eqeltrd	|- ( ph -> ( ( X ^ 2 ) x. Q ) e. CC )
58	57 49 50	addsubd	|- ( ph -> ( ( ( ( X ^ 2 ) x. Q ) + ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) ) - ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) = ( ( ( ( X ^ 2 ) x. Q ) - ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) + ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) ) )
59	54	oveq1d	|- ( ph -> ( ( ( X ^ 2 ) x. Q ) - ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) = ( ( X x. ( X x. Q ) ) - ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) )
60	41 28 29	subdid	|- ( ph -> ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) = ( ( X x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) - ( X x. ( C x. Q ) ) ) )
61	59 60	oveq12d	|- ( ph -> ( ( ( ( X ^ 2 ) x. Q ) - ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) + ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) ) = ( ( ( X x. ( X x. Q ) ) - ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) + ( ( X x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) - ( X x. ( C x. Q ) ) ) ) )
62	41 28	mulcld	|- ( ph -> ( X x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) e. CC )
63	41 29	mulcld	|- ( ph -> ( X x. ( C x. Q ) ) e. CC )
64	56 62 50 63	addsub4d	|- ( ph -> ( ( ( X x. ( X x. Q ) ) + ( X x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) - ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( X x. ( C x. Q ) ) ) ) = ( ( ( X x. ( X x. Q ) ) - ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) + ( ( X x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) - ( X x. ( C x. Q ) ) ) ) )
65	41 26 55 28	submuladdd	|- ( ph -> ( ( X - C ) x. ( ( X x. Q ) + ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) = ( ( ( X x. ( X x. Q ) ) + ( X x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) - ( ( C x. ( X x. Q ) ) + ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) ) )
66	9	oveq1d	|- ( ph -> ( ( abs ` ( X - C ) ) ^ 2 ) = ( ( abs ` ( E - F ) ) ^ 2 ) )
67	41 26	subcld	|- ( ph -> ( X - C ) e. CC )
68	67	absvalsqd	|- ( ph -> ( ( abs ` ( X - C ) ) ^ 2 ) = ( ( X - C ) x. ( * ` ( X - C ) ) ) )
69	1 5	sseldd	|- ( ph -> E e. CC )
70	1 6	sseldd	|- ( ph -> F e. CC )
71	69 70	subcld	|- ( ph -> ( E - F ) e. CC )
72	71	absvalsqd	|- ( ph -> ( ( abs ` ( E - F ) ) ^ 2 ) = ( ( E - F ) x. ( * ` ( E - F ) ) ) )
73	66 68 72	3eqtr3d	|- ( ph -> ( ( X - C ) x. ( * ` ( X - C ) ) ) = ( ( E - F ) x. ( * ` ( E - F ) ) ) )
74	8	fvoveq1d	|- ( ph -> ( * ` ( X - C ) ) = ( * ` ( ( A + ( T x. ( B - A ) ) ) - C ) ) )
75	40 26	cjsubd	|- ( ph -> ( * ` ( ( A + ( T x. ( B - A ) ) ) - C ) ) = ( ( * ` ( A + ( T x. ( B - A ) ) ) ) - ( * ` C ) ) )
76	14 39	cjaddd	|- ( ph -> ( * ` ( A + ( T x. ( B - A ) ) ) ) = ( ( * ` A ) + ( * ` ( T x. ( B - A ) ) ) ) )
77	38 19	cjmuld	|- ( ph -> ( * ` ( T x. ( B - A ) ) ) = ( ( * ` T ) x. ( * ` ( B - A ) ) ) )
78	7	cjred	|- ( ph -> ( * ` T ) = T )
79	14 39 8	mvrladdd	|- ( ph -> ( X - A ) = ( T x. ( B - A ) ) )
80	79 39	eqeltrd	|- ( ph -> ( X - A ) e. CC )
81	80 38 19 21	divmul3d	|- ( ph -> ( ( ( X - A ) / ( B - A ) ) = T <-> ( X - A ) = ( T x. ( B - A ) ) ) )
82	79 81	mpbird	|- ( ph -> ( ( X - A ) / ( B - A ) ) = T )
83	78 82	eqtr4d	|- ( ph -> ( * ` T ) = ( ( X - A ) / ( B - A ) ) )
84	83 31	oveq12d	|- ( ph -> ( ( * ` T ) x. ( * ` ( B - A ) ) ) = ( ( ( X - A ) / ( B - A ) ) x. ( ( * ` B ) - ( * ` A ) ) ) )
85	80 19 18 21	div32d	|- ( ph -> ( ( ( X - A ) / ( B - A ) ) x. ( ( * ` B ) - ( * ` A ) ) ) = ( ( X - A ) x. ( ( ( * ` B ) - ( * ` A ) ) / ( B - A ) ) ) )
86	10	oveq2i	|- ( ( X - A ) x. Q ) = ( ( X - A ) x. ( ( ( * ` B ) - ( * ` A ) ) / ( B - A ) ) )
87	85 86	eqtr4di	|- ( ph -> ( ( ( X - A ) / ( B - A ) ) x. ( ( * ` B ) - ( * ` A ) ) ) = ( ( X - A ) x. Q ) )
88	41 14 23	subdird	|- ( ph -> ( ( X - A ) x. Q ) = ( ( X x. Q ) - ( A x. Q ) ) )
89	84 87 88	3eqtrd	|- ( ph -> ( ( * ` T ) x. ( * ` ( B - A ) ) ) = ( ( X x. Q ) - ( A x. Q ) ) )
90	77 89	eqtrd	|- ( ph -> ( * ` ( T x. ( B - A ) ) ) = ( ( X x. Q ) - ( A x. Q ) ) )
91	90	oveq2d	|- ( ph -> ( ( * ` A ) + ( * ` ( T x. ( B - A ) ) ) ) = ( ( * ` A ) + ( ( X x. Q ) - ( A x. Q ) ) ) )
92	15 55 24	addsub12d	|- ( ph -> ( ( * ` A ) + ( ( X x. Q ) - ( A x. Q ) ) ) = ( ( X x. Q ) + ( ( * ` A ) - ( A x. Q ) ) ) )
93	76 91 92	3eqtrd	|- ( ph -> ( * ` ( A + ( T x. ( B - A ) ) ) ) = ( ( X x. Q ) + ( ( * ` A ) - ( A x. Q ) ) ) )
94	93	oveq1d	|- ( ph -> ( ( * ` ( A + ( T x. ( B - A ) ) ) ) - ( * ` C ) ) = ( ( ( X x. Q ) + ( ( * ` A ) - ( A x. Q ) ) ) - ( * ` C ) ) )
95	55 25 27	addsubassd	|- ( ph -> ( ( ( X x. Q ) + ( ( * ` A ) - ( A x. Q ) ) ) - ( * ` C ) ) = ( ( X x. Q ) + ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) )
96	75 94 95	3eqtrd	|- ( ph -> ( * ` ( ( A + ( T x. ( B - A ) ) ) - C ) ) = ( ( X x. Q ) + ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) )
97	74 96	eqtrd	|- ( ph -> ( * ` ( X - C ) ) = ( ( X x. Q ) + ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) )
98	97	oveq2d	|- ( ph -> ( ( X - C ) x. ( * ` ( X - C ) ) ) = ( ( X - C ) x. ( ( X x. Q ) + ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) )
99	69 70	cjsubd	|- ( ph -> ( * ` ( E - F ) ) = ( ( * ` E ) - ( * ` F ) ) )
100	99	oveq2d	|- ( ph -> ( ( E - F ) x. ( * ` ( E - F ) ) ) = ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) )
101	73 98 100	3eqtr3d	|- ( ph -> ( ( X - C ) x. ( ( X x. Q ) + ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) = ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) )
102	26 41 23	mul12d	|- ( ph -> ( C x. ( X x. Q ) ) = ( X x. ( C x. Q ) ) )
103	102	oveq1d	|- ( ph -> ( ( C x. ( X x. Q ) ) + ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) = ( ( X x. ( C x. Q ) ) + ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) )
104	63 50 103	comraddd	|- ( ph -> ( ( C x. ( X x. Q ) ) + ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) = ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( X x. ( C x. Q ) ) ) )
105	104	oveq2d	|- ( ph -> ( ( ( X x. ( X x. Q ) ) + ( X x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) - ( ( C x. ( X x. Q ) ) + ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) ) = ( ( ( X x. ( X x. Q ) ) + ( X x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) - ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( X x. ( C x. Q ) ) ) ) )
106	65 101 105	3eqtr3rd	|- ( ph -> ( ( ( X x. ( X x. Q ) ) + ( X x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) - ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( X x. ( C x. Q ) ) ) ) = ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) )
107	61 64 106	3eqtr2d	|- ( ph -> ( ( ( ( X ^ 2 ) x. Q ) - ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) + ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) ) = ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) )
108	58 107	eqtrd	|- ( ph -> ( ( ( ( X ^ 2 ) x. Q ) + ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) ) - ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) = ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) )
109	57 49	addcld	|- ( ph -> ( ( ( X ^ 2 ) x. Q ) + ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) ) e. CC )
110	109 50	subcld	|- ( ph -> ( ( ( ( X ^ 2 ) x. Q ) + ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) ) - ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) e. CC )
111	108 110	eqeltrrd	|- ( ph -> ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) e. CC )
112	50 111	addcld	|- ( ph -> ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) e. CC )
113	112	negcld	|- ( ph -> -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) e. CC )
114	49 113 23 36	divdird	|- ( ph -> ( ( ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) + -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) ) / Q ) = ( ( ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) / Q ) + ( -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) / Q ) ) )
115	48 114	eqtr4d	|- ( ph -> ( ( M x. X ) + N ) = ( ( ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) + -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) ) / Q ) )
116	115	oveq2d	|- ( ph -> ( ( X ^ 2 ) + ( ( M x. X ) + N ) ) = ( ( X ^ 2 ) + ( ( ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) + -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) ) / Q ) ) )
117	41	sqcld	|- ( ph -> ( X ^ 2 ) e. CC )
118	49 113	addcld	|- ( ph -> ( ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) + -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) ) e. CC )
119	117 23 118 36	muldivdid	|- ( ph -> ( ( ( ( X ^ 2 ) x. Q ) + ( ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) + -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) ) ) / Q ) = ( ( X ^ 2 ) + ( ( ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) + -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) ) / Q ) ) )
120	57 49 113	addassd	|- ( ph -> ( ( ( ( X ^ 2 ) x. Q ) + ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) ) + -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) ) = ( ( ( X ^ 2 ) x. Q ) + ( ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) + -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) ) ) )
121	109 112	negsubd	|- ( ph -> ( ( ( ( X ^ 2 ) x. Q ) + ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) ) + -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) ) = ( ( ( ( X ^ 2 ) x. Q ) + ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) ) - ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) ) )
122	109 50 111	subsub4d	|- ( ph -> ( ( ( ( ( X ^ 2 ) x. Q ) + ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) ) - ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) - ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) = ( ( ( ( X ^ 2 ) x. Q ) + ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) ) - ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) ) )
123	110 108	subeq0bd	|- ( ph -> ( ( ( ( ( X ^ 2 ) x. Q ) + ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) ) - ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) ) - ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) = 0 )
124	121 122 123	3eqtr2d	|- ( ph -> ( ( ( ( X ^ 2 ) x. Q ) + ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) ) + -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) ) = 0 )
125	120 124	eqtr3d	|- ( ph -> ( ( ( X ^ 2 ) x. Q ) + ( ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) + -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) ) ) = 0 )
126	57 118	addcld	|- ( ph -> ( ( ( X ^ 2 ) x. Q ) + ( ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) + -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) ) ) e. CC )
127	126 23 36	diveq0ad	|- ( ph -> ( ( ( ( ( X ^ 2 ) x. Q ) + ( ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) + -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) ) ) / Q ) = 0 <-> ( ( ( X ^ 2 ) x. Q ) + ( ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) + -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) ) ) = 0 ) )
128	125 127	mpbird	|- ( ph -> ( ( ( ( X ^ 2 ) x. Q ) + ( ( X x. ( ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) - ( C x. Q ) ) ) + -u ( ( C x. ( ( ( * ` A ) - ( A x. Q ) ) - ( * ` C ) ) ) + ( ( E - F ) x. ( ( * ` E ) - ( * ` F ) ) ) ) ) ) / Q ) = 0 )
129	116 119 128	3eqtr2d	|- ( ph -> ( ( X ^ 2 ) + ( ( M x. X ) + N ) ) = 0 )
130	129 36	jca	|- ( ph -> ( ( ( X ^ 2 ) + ( ( M x. X ) + N ) ) = 0 /\ Q =/= 0 ) )