let a, b, c be Real; :: thesis: ( 0 <= a & c <= 0 implies 0 <= delta (a,b,c) )
assume that
A1: 0 <= a and
A2: c <= 0 ; :: thesis: 0 <= delta (a,b,c)
A3: delta (a,b,c) = (b ^2) - ((4 * a) * c) by QUIN_1:def 1;
0 <= b * b
proof
per cases ( b = 0 or b <> 0 ) ;
suppose b = 0 ; :: thesis: 0 <= b * b
hence 0 <= b * b ; :: thesis: verum
end;
end;
end;
hence 0 <= delta (a,b,c) by A1, A2, A3; :: thesis: verum