Theorem quad3

Description: Variant of quadratic equation with discriminant expanded. (Contributed by Filip Cernatescu, 19-Oct-2019)

	Ref	Expression
Hypotheses	quad3.1	|- X e. CC
	quad3.2	|- A e. CC
	quad3.3	|- A =/= 0
	quad3.4	|- B e. CC
	quad3.5	|- C e. CC
	quad3.6	|- ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) = 0
Assertion	quad3	|- ( X = ( ( -u B + ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) / ( 2 x. A ) ) \/ X = ( ( -u B - ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) / ( 2 x. A ) ) )

Proof

Step	Hyp	Ref	Expression
1		quad3.1	|- X e. CC
2		quad3.2	|- A e. CC
3		quad3.3	|- A =/= 0
4		quad3.4	|- B e. CC
5		quad3.5	|- C e. CC
6		quad3.6	|- ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) = 0
7		2cn	|- 2 e. CC
8	7 2	mulcli	|- ( 2 x. A ) e. CC
9		2ne0	|- 2 =/= 0
10	7 2 9 3	mulne0i	|- ( 2 x. A ) =/= 0
11	4 8 10	divcli	|- ( B / ( 2 x. A ) ) e. CC
12	1 11	addcli	|- ( X + ( B / ( 2 x. A ) ) ) e. CC
13	8 12	sqmuli	|- ( ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) ^ 2 ) = ( ( ( 2 x. A ) ^ 2 ) x. ( ( X + ( B / ( 2 x. A ) ) ) ^ 2 ) )
14	1 11	binom2i	|- ( ( X + ( B / ( 2 x. A ) ) ) ^ 2 ) = ( ( ( X ^ 2 ) + ( 2 x. ( X x. ( B / ( 2 x. A ) ) ) ) ) + ( ( B / ( 2 x. A ) ) ^ 2 ) )
15	1	sqcli	|- ( X ^ 2 ) e. CC
16	2 15	mulcli	|- ( A x. ( X ^ 2 ) ) e. CC
17	4 1	mulcli	|- ( B x. X ) e. CC
18	16 17 2 3	divdiri	|- ( ( ( A x. ( X ^ 2 ) ) + ( B x. X ) ) / A ) = ( ( ( A x. ( X ^ 2 ) ) / A ) + ( ( B x. X ) / A ) )
19	15 2 3	divcan3i	|- ( ( A x. ( X ^ 2 ) ) / A ) = ( X ^ 2 )
20	4 1 2 3	div23i	|- ( ( B x. X ) / A ) = ( ( B / A ) x. X )
21	19 20	oveq12i	|- ( ( ( A x. ( X ^ 2 ) ) / A ) + ( ( B x. X ) / A ) ) = ( ( X ^ 2 ) + ( ( B / A ) x. X ) )
22	18 21	eqtr2i	|- ( ( X ^ 2 ) + ( ( B / A ) x. X ) ) = ( ( ( A x. ( X ^ 2 ) ) + ( B x. X ) ) / A )
23	4 2 3	divcli	|- ( B / A ) e. CC
24	23 1	mulcomi	|- ( ( B / A ) x. X ) = ( X x. ( B / A ) )
25	1 23	mulcli	|- ( X x. ( B / A ) ) e. CC
26	25 7 9	divcan2i	|- ( 2 x. ( ( X x. ( B / A ) ) / 2 ) ) = ( X x. ( B / A ) )
27	1 23 7 9	divassi	|- ( ( X x. ( B / A ) ) / 2 ) = ( X x. ( ( B / A ) / 2 ) )
28	2 3	pm3.2i	|- ( A e. CC /\ A =/= 0 )
29	7 9	pm3.2i	|- ( 2 e. CC /\ 2 =/= 0 )
30		divdiv1	|- ( ( B e. CC /\ ( A e. CC /\ A =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( B / A ) / 2 ) = ( B / ( A x. 2 ) ) )
31	4 28 29 30	mp3an	|- ( ( B / A ) / 2 ) = ( B / ( A x. 2 ) )
32	2 7	mulcomi	|- ( A x. 2 ) = ( 2 x. A )
33	32	oveq2i	|- ( B / ( A x. 2 ) ) = ( B / ( 2 x. A ) )
34	31 33	eqtri	|- ( ( B / A ) / 2 ) = ( B / ( 2 x. A ) )
35	34	oveq2i	|- ( X x. ( ( B / A ) / 2 ) ) = ( X x. ( B / ( 2 x. A ) ) )
36	27 35	eqtri	|- ( ( X x. ( B / A ) ) / 2 ) = ( X x. ( B / ( 2 x. A ) ) )
37	36	oveq2i	|- ( 2 x. ( ( X x. ( B / A ) ) / 2 ) ) = ( 2 x. ( X x. ( B / ( 2 x. A ) ) ) )
38	24 26 37	3eqtr2i	|- ( ( B / A ) x. X ) = ( 2 x. ( X x. ( B / ( 2 x. A ) ) ) )
39	38	oveq2i	|- ( ( X ^ 2 ) + ( ( B / A ) x. X ) ) = ( ( X ^ 2 ) + ( 2 x. ( X x. ( B / ( 2 x. A ) ) ) ) )
40	16 17 5	addassi	|- ( ( ( A x. ( X ^ 2 ) ) + ( B x. X ) ) + C ) = ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) )
41	40	eqcomi	|- ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) = ( ( ( A x. ( X ^ 2 ) ) + ( B x. X ) ) + C )
42	41	oveq1i	|- ( ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) - C ) = ( ( ( ( A x. ( X ^ 2 ) ) + ( B x. X ) ) + C ) - C )
43	16 17	addcli	|- ( ( A x. ( X ^ 2 ) ) + ( B x. X ) ) e. CC
44	43 5	pncan3oi	|- ( ( ( ( A x. ( X ^ 2 ) ) + ( B x. X ) ) + C ) - C ) = ( ( A x. ( X ^ 2 ) ) + ( B x. X ) )
45	42 44	eqtr2i	|- ( ( A x. ( X ^ 2 ) ) + ( B x. X ) ) = ( ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) - C )
46	6	oveq1i	|- ( ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) - C ) = ( 0 - C )
47		df-neg	|- -u C = ( 0 - C )
48	46 47	eqtr4i	|- ( ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) - C ) = -u C
49	45 48	eqtri	|- ( ( A x. ( X ^ 2 ) ) + ( B x. X ) ) = -u C
50	49	oveq1i	|- ( ( ( A x. ( X ^ 2 ) ) + ( B x. X ) ) / A ) = ( -u C / A )
51	22 39 50	3eqtr3i	|- ( ( X ^ 2 ) + ( 2 x. ( X x. ( B / ( 2 x. A ) ) ) ) ) = ( -u C / A )
52	51	oveq1i	|- ( ( ( X ^ 2 ) + ( 2 x. ( X x. ( B / ( 2 x. A ) ) ) ) ) + ( ( B / ( 2 x. A ) ) ^ 2 ) ) = ( ( -u C / A ) + ( ( B / ( 2 x. A ) ) ^ 2 ) )
53	14 52	eqtri	|- ( ( X + ( B / ( 2 x. A ) ) ) ^ 2 ) = ( ( -u C / A ) + ( ( B / ( 2 x. A ) ) ^ 2 ) )
54	5	negcli	|- -u C e. CC
55	54 2 3	divcli	|- ( -u C / A ) e. CC
56	11	sqcli	|- ( ( B / ( 2 x. A ) ) ^ 2 ) e. CC
57	55 56	addcomi	|- ( ( -u C / A ) + ( ( B / ( 2 x. A ) ) ^ 2 ) ) = ( ( ( B / ( 2 x. A ) ) ^ 2 ) + ( -u C / A ) )
58	4 8 10	sqdivi	|- ( ( B / ( 2 x. A ) ) ^ 2 ) = ( ( B ^ 2 ) / ( ( 2 x. A ) ^ 2 ) )
59		4cn	|- 4 e. CC
60	59 2	mulcli	|- ( 4 x. A ) e. CC
61		4ne0	|- 4 =/= 0
62	59 2 61 3	mulne0i	|- ( 4 x. A ) =/= 0
63	60 60 54 2 62 3	divmuldivi	|- ( ( ( 4 x. A ) / ( 4 x. A ) ) x. ( -u C / A ) ) = ( ( ( 4 x. A ) x. -u C ) / ( ( 4 x. A ) x. A ) )
64	60 62	dividi	|- ( ( 4 x. A ) / ( 4 x. A ) ) = 1
65	64	eqcomi	|- 1 = ( ( 4 x. A ) / ( 4 x. A ) )
66	65	oveq1i	|- ( 1 x. ( -u C / A ) ) = ( ( ( 4 x. A ) / ( 4 x. A ) ) x. ( -u C / A ) )
67	55	mullidi	|- ( 1 x. ( -u C / A ) ) = ( -u C / A )
68	66 67	eqtr3i	|- ( ( ( 4 x. A ) / ( 4 x. A ) ) x. ( -u C / A ) ) = ( -u C / A )
69	5	mulm1i	|- ( -u 1 x. C ) = -u C
70	69	eqcomi	|- -u C = ( -u 1 x. C )
71	70	oveq2i	|- ( ( 4 x. A ) x. -u C ) = ( ( 4 x. A ) x. ( -u 1 x. C ) )
72		neg1cn	|- -u 1 e. CC
73	60 72 5	mulassi	|- ( ( ( 4 x. A ) x. -u 1 ) x. C ) = ( ( 4 x. A ) x. ( -u 1 x. C ) )
74	71 73	eqtr4i	|- ( ( 4 x. A ) x. -u C ) = ( ( ( 4 x. A ) x. -u 1 ) x. C )
75	60 72	mulcomi	|- ( ( 4 x. A ) x. -u 1 ) = ( -u 1 x. ( 4 x. A ) )
76	75	oveq1i	|- ( ( ( 4 x. A ) x. -u 1 ) x. C ) = ( ( -u 1 x. ( 4 x. A ) ) x. C )
77	72 60 5	mulassi	|- ( ( -u 1 x. ( 4 x. A ) ) x. C ) = ( -u 1 x. ( ( 4 x. A ) x. C ) )
78	74 76 77	3eqtri	|- ( ( 4 x. A ) x. -u C ) = ( -u 1 x. ( ( 4 x. A ) x. C ) )
79	59 2 5	mulassi	|- ( ( 4 x. A ) x. C ) = ( 4 x. ( A x. C ) )
80	79	oveq2i	|- ( -u 1 x. ( ( 4 x. A ) x. C ) ) = ( -u 1 x. ( 4 x. ( A x. C ) ) )
81	2 5	mulcli	|- ( A x. C ) e. CC
82	59 81	mulcli	|- ( 4 x. ( A x. C ) ) e. CC
83	82	mulm1i	|- ( -u 1 x. ( 4 x. ( A x. C ) ) ) = -u ( 4 x. ( A x. C ) )
84	78 80 83	3eqtri	|- ( ( 4 x. A ) x. -u C ) = -u ( 4 x. ( A x. C ) )
85		2t2e4	|- ( 2 x. 2 ) = 4
86	85	eqcomi	|- 4 = ( 2 x. 2 )
87	86	oveq1i	|- ( 4 x. A ) = ( ( 2 x. 2 ) x. A )
88	87	oveq1i	|- ( ( 4 x. A ) x. A ) = ( ( ( 2 x. 2 ) x. A ) x. A )
89	7 7 2	mulassi	|- ( ( 2 x. 2 ) x. A ) = ( 2 x. ( 2 x. A ) )
90	89	oveq1i	|- ( ( ( 2 x. 2 ) x. A ) x. A ) = ( ( 2 x. ( 2 x. A ) ) x. A )
91	88 90	eqtri	|- ( ( 4 x. A ) x. A ) = ( ( 2 x. ( 2 x. A ) ) x. A )
92	7 8	mulcomi	|- ( 2 x. ( 2 x. A ) ) = ( ( 2 x. A ) x. 2 )
93	92	oveq1i	|- ( ( 2 x. ( 2 x. A ) ) x. A ) = ( ( ( 2 x. A ) x. 2 ) x. A )
94	8 7 2	mulassi	|- ( ( ( 2 x. A ) x. 2 ) x. A ) = ( ( 2 x. A ) x. ( 2 x. A ) )
95	91 93 94	3eqtri	|- ( ( 4 x. A ) x. A ) = ( ( 2 x. A ) x. ( 2 x. A ) )
96	8	sqvali	|- ( ( 2 x. A ) ^ 2 ) = ( ( 2 x. A ) x. ( 2 x. A ) )
97	95 96	eqtr4i	|- ( ( 4 x. A ) x. A ) = ( ( 2 x. A ) ^ 2 )
98	84 97	oveq12i	|- ( ( ( 4 x. A ) x. -u C ) / ( ( 4 x. A ) x. A ) ) = ( -u ( 4 x. ( A x. C ) ) / ( ( 2 x. A ) ^ 2 ) )
99	63 68 98	3eqtr3i	|- ( -u C / A ) = ( -u ( 4 x. ( A x. C ) ) / ( ( 2 x. A ) ^ 2 ) )
100	58 99	oveq12i	|- ( ( ( B / ( 2 x. A ) ) ^ 2 ) + ( -u C / A ) ) = ( ( ( B ^ 2 ) / ( ( 2 x. A ) ^ 2 ) ) + ( -u ( 4 x. ( A x. C ) ) / ( ( 2 x. A ) ^ 2 ) ) )
101	4	sqcli	|- ( B ^ 2 ) e. CC
102	82	negcli	|- -u ( 4 x. ( A x. C ) ) e. CC
103	8	sqcli	|- ( ( 2 x. A ) ^ 2 ) e. CC
104	8 8 10 10	mulne0i	|- ( ( 2 x. A ) x. ( 2 x. A ) ) =/= 0
105	96 104	eqnetri	|- ( ( 2 x. A ) ^ 2 ) =/= 0
106	101 102 103 105	divdiri	|- ( ( ( B ^ 2 ) + -u ( 4 x. ( A x. C ) ) ) / ( ( 2 x. A ) ^ 2 ) ) = ( ( ( B ^ 2 ) / ( ( 2 x. A ) ^ 2 ) ) + ( -u ( 4 x. ( A x. C ) ) / ( ( 2 x. A ) ^ 2 ) ) )
107	101 82	negsubi	|- ( ( B ^ 2 ) + -u ( 4 x. ( A x. C ) ) ) = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) )
108	107	oveq1i	|- ( ( ( B ^ 2 ) + -u ( 4 x. ( A x. C ) ) ) / ( ( 2 x. A ) ^ 2 ) ) = ( ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) / ( ( 2 x. A ) ^ 2 ) )
109	100 106 108	3eqtr2i	|- ( ( ( B / ( 2 x. A ) ) ^ 2 ) + ( -u C / A ) ) = ( ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) / ( ( 2 x. A ) ^ 2 ) )
110	53 57 109	3eqtri	|- ( ( X + ( B / ( 2 x. A ) ) ) ^ 2 ) = ( ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) / ( ( 2 x. A ) ^ 2 ) )
111	110	oveq2i	|- ( ( ( 2 x. A ) ^ 2 ) x. ( ( X + ( B / ( 2 x. A ) ) ) ^ 2 ) ) = ( ( ( 2 x. A ) ^ 2 ) x. ( ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) / ( ( 2 x. A ) ^ 2 ) ) )
112	101 82	subcli	|- ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) e. CC
113	112 103 105	divcan2i	|- ( ( ( 2 x. A ) ^ 2 ) x. ( ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) / ( ( 2 x. A ) ^ 2 ) ) ) = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) )
114	13 111 113	3eqtri	|- ( ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) ^ 2 ) = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) )
115	8 12	mulcli	|- ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) e. CC
116	115 112	pm3.2i	|- ( ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) e. CC /\ ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) e. CC )
117		eqsqrtor	|- ( ( ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) e. CC /\ ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) e. CC ) -> ( ( ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) ^ 2 ) = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) <-> ( ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) = ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) \/ ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) = -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) ) )
118	116 117	ax-mp	|- ( ( ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) ^ 2 ) = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) <-> ( ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) = ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) \/ ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) = -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) )
119	114 118	mpbi	|- ( ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) = ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) \/ ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) = -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) )
120		sqrtcl	|- ( ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) e. CC -> ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) e. CC )
121	112 120	ax-mp	|- ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) e. CC
122	121 8 12 10	divmuli	|- ( ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) = ( X + ( B / ( 2 x. A ) ) ) <-> ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) = ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) )
123		eqcom	|- ( ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) = ( X + ( B / ( 2 x. A ) ) ) <-> ( X + ( B / ( 2 x. A ) ) ) = ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) )
124	122 123	bitr3i	|- ( ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) = ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) <-> ( X + ( B / ( 2 x. A ) ) ) = ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) )
125	121 8 10	divcli	|- ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) e. CC
126	125 11 1	subadd2i	|- ( ( ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) - ( B / ( 2 x. A ) ) ) = X <-> ( X + ( B / ( 2 x. A ) ) ) = ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) )
127		eqcom	|- ( ( ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) - ( B / ( 2 x. A ) ) ) = X <-> X = ( ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) - ( B / ( 2 x. A ) ) ) )
128	126 127	bitr3i	|- ( ( X + ( B / ( 2 x. A ) ) ) = ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) <-> X = ( ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) - ( B / ( 2 x. A ) ) ) )
129		divneg	|- ( ( B e. CC /\ ( 2 x. A ) e. CC /\ ( 2 x. A ) =/= 0 ) -> -u ( B / ( 2 x. A ) ) = ( -u B / ( 2 x. A ) ) )
130	4 8 10 129	mp3an	|- -u ( B / ( 2 x. A ) ) = ( -u B / ( 2 x. A ) )
131	130	oveq2i	|- ( ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) + -u ( B / ( 2 x. A ) ) ) = ( ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) + ( -u B / ( 2 x. A ) ) )
132	125 11	negsubi	|- ( ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) + -u ( B / ( 2 x. A ) ) ) = ( ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) - ( B / ( 2 x. A ) ) )
133	4	negcli	|- -u B e. CC
134	133 8 10	divcli	|- ( -u B / ( 2 x. A ) ) e. CC
135	125 134	addcomi	|- ( ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) + ( -u B / ( 2 x. A ) ) ) = ( ( -u B / ( 2 x. A ) ) + ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) )
136	131 132 135	3eqtr3i	|- ( ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) - ( B / ( 2 x. A ) ) ) = ( ( -u B / ( 2 x. A ) ) + ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) )
137	133 121 8 10	divdiri	|- ( ( -u B + ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) / ( 2 x. A ) ) = ( ( -u B / ( 2 x. A ) ) + ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) )
138	136 137	eqtr4i	|- ( ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) - ( B / ( 2 x. A ) ) ) = ( ( -u B + ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) / ( 2 x. A ) )
139	138	eqeq2i	|- ( X = ( ( ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) - ( B / ( 2 x. A ) ) ) <-> X = ( ( -u B + ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) / ( 2 x. A ) ) )
140	124 128 139	3bitri	|- ( ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) = ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) <-> X = ( ( -u B + ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) / ( 2 x. A ) ) )
141	121	negcli	|- -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) e. CC
142	141 8 12 10	divmuli	|- ( ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) = ( X + ( B / ( 2 x. A ) ) ) <-> ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) = -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) )
143		eqcom	|- ( ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) = ( X + ( B / ( 2 x. A ) ) ) <-> ( X + ( B / ( 2 x. A ) ) ) = ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) )
144	142 143	bitr3i	|- ( ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) = -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) <-> ( X + ( B / ( 2 x. A ) ) ) = ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) )
145	141 8 10	divcli	|- ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) e. CC
146	145 11 1	subadd2i	|- ( ( ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) - ( B / ( 2 x. A ) ) ) = X <-> ( X + ( B / ( 2 x. A ) ) ) = ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) )
147		eqcom	|- ( ( ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) - ( B / ( 2 x. A ) ) ) = X <-> X = ( ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) - ( B / ( 2 x. A ) ) ) )
148	146 147	bitr3i	|- ( ( X + ( B / ( 2 x. A ) ) ) = ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) <-> X = ( ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) - ( B / ( 2 x. A ) ) ) )
149	130	oveq2i	|- ( ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) + -u ( B / ( 2 x. A ) ) ) = ( ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) + ( -u B / ( 2 x. A ) ) )
150	145 11	negsubi	|- ( ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) + -u ( B / ( 2 x. A ) ) ) = ( ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) - ( B / ( 2 x. A ) ) )
151	145 134	addcomi	|- ( ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) + ( -u B / ( 2 x. A ) ) ) = ( ( -u B / ( 2 x. A ) ) + ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) )
152	149 150 151	3eqtr3i	|- ( ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) - ( B / ( 2 x. A ) ) ) = ( ( -u B / ( 2 x. A ) ) + ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) )
153	133 141 8 10	divdiri	|- ( ( -u B + -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) / ( 2 x. A ) ) = ( ( -u B / ( 2 x. A ) ) + ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) )
154	133 121	negsubi	|- ( -u B + -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) = ( -u B - ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) )
155	154	oveq1i	|- ( ( -u B + -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) / ( 2 x. A ) ) = ( ( -u B - ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) / ( 2 x. A ) )
156	152 153 155	3eqtr2i	|- ( ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) - ( B / ( 2 x. A ) ) ) = ( ( -u B - ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) / ( 2 x. A ) )
157	156	eqeq2i	|- ( X = ( ( -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) / ( 2 x. A ) ) - ( B / ( 2 x. A ) ) ) <-> X = ( ( -u B - ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) / ( 2 x. A ) ) )
158	144 148 157	3bitri	|- ( ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) = -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) <-> X = ( ( -u B - ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) / ( 2 x. A ) ) )
159	140 158	orbi12i	|- ( ( ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) = ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) \/ ( ( 2 x. A ) x. ( X + ( B / ( 2 x. A ) ) ) ) = -u ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) <-> ( X = ( ( -u B + ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) / ( 2 x. A ) ) \/ X = ( ( -u B - ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) / ( 2 x. A ) ) ) )
160	119 159	mpbi	|- ( X = ( ( -u B + ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) / ( 2 x. A ) ) \/ X = ( ( -u B - ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) / ( 2 x. A ) ) )