let a, b, c, x be Complex; ( 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:106
.=
(a * ((x ^2) + ((b * x) * (1 / a)))) + c
.=
(a * ((x ^2) + ((b * x) / a))) + c
by XCMPLX_1:99
.=
(a * ((x ^2) + (x * (b / a)))) + c
by XCMPLX_1:74
.=
(a * ((x ^2) + (x * ((2 * b) / (2 * a))))) + c
by XCMPLX_1:91
.=
(a * ((x ^2) + (x * (2 * (b / (2 * a)))))) + c
by XCMPLX_1:74
.=
((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:109
.=
((a * ((x ^2) + ((2 * x) * (b / (2 * a))))) + (a * (((b ^2) * 1) / ((4 * a) * a)))) + (c - ((b ^2) / (4 * a)))
by XCMPLX_1:76
.=
((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:76
.=
(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:89
.=
(a * ((x + (b / (2 * a))) ^2)) - (((b ^2) - ((4 * a) * c)) / (4 * a))
by XCMPLX_1:120
;
hence
((a * (x ^2)) + (b * x)) + c = (a * ((x + (b / (2 * a))) ^2)) - ((delta (a,b,c)) / (4 * a))
; verum