let a, b, c, x be complex number ; ( a <> 0 implies ((a * (x ^2 )) + (b * x)) + c = (a * ((x + (b / (2 * a))) ^2 )) - ((delta a,b,c) / (4 * a)) )
assume A1:
a <> 0
; ((a * (x ^2 )) + (b * x)) + c = (a * ((x + (b / (2 * a))) ^2 )) - ((delta a,b,c) / (4 * a))
then A2:
4 * a <> 0
;
((a * (x ^2 )) + (b * x)) + c =
((a * (x ^2 )) + ((b * x) * 1)) + c
.=
((a * (x ^2 )) + ((b * x) * (a * (1 / a)))) + c
by A1, XCMPLX_1:107
.=
(a * ((x ^2 ) + ((b * x) * (1 / a)))) + c
.=
(a * ((x ^2 ) + ((b * x) / a))) + c
by XCMPLX_1:100
.=
(a * ((x ^2 ) + (x * (b / a)))) + c
by XCMPLX_1:75
.=
(a * ((x ^2 ) + (x * ((2 * b) / (2 * a))))) + c
by XCMPLX_1:92
.=
(a * ((x ^2 ) + (x * (2 * (b / (2 * a)))))) + c
by XCMPLX_1:75
.=
((a * ((x ^2 ) + ((2 * x) * (b / (2 * a))))) + ((b ^2 ) / (4 * a))) + (c - ((b ^2 ) / (4 * a)))
.=
((a * ((x ^2 ) + ((2 * x) * (b / (2 * a))))) + (a * (((b ^2 ) / (4 * a)) * (1 / a)))) + (c - ((b ^2 ) / (4 * a)))
by A1, XCMPLX_1:110
.=
((a * ((x ^2 ) + ((2 * x) * (b / (2 * a))))) + (a * (((b ^2 ) * 1) / ((4 * a) * a)))) + (c - ((b ^2 ) / (4 * a)))
by XCMPLX_1:77
.=
((a * ((x ^2 ) + ((2 * x) * (b / (2 * a))))) + (a * ((b ^2 ) / ((2 * a) ^2 )))) + (c - ((b ^2 ) / (4 * a)))
.=
((a * ((x ^2 ) + ((2 * x) * (b / (2 * a))))) + (a * ((b / (2 * a)) ^2 ))) + (c - ((b ^2 ) / (4 * a)))
by XCMPLX_1:77
.=
(a * ((x + (b / (2 * a))) ^2 )) - (((b ^2 ) / (4 * a)) - c)
.=
(a * ((x + (b / (2 * a))) ^2 )) - (((b ^2 ) / (4 * a)) - (((4 * a) * c) / (4 * a)))
by A2, XCMPLX_1:90
.=
(a * ((x + (b / (2 * a))) ^2 )) - (((b ^2 ) - ((4 * a) * c)) / (4 * a))
by XCMPLX_1:121
;
hence
((a * (x ^2 )) + (b * x)) + c = (a * ((x + (b / (2 * a))) ^2 )) - ((delta a,b,c) / (4 * a))
; verum