:: QUIN_1 semantic presentation

definition
let c1, c2, c3 be complex number ;
func delta c1,c2,c3 -> set equals :: QUIN_1:def 1
(a2 ^2 ) - ((4 * a1) * a3);
coherence
(c2 ^2 ) - ((4 * c1) * c3) is set ;
end;

:: deftheorem Def1 defines delta QUIN_1:def 1 :
for b1, b2, b3 being complex number holds delta b1,b2,b3 = (b2 ^2 ) - ((4 * b1) * b3);

registration
let c1, c2, c3 be complex number ;
cluster delta a1,a2,a3 -> complex ;
coherence
delta c1,c2,c3 is complex ;
end;

registration
let c1, c2, c3 be real number ;
cluster delta a1,a2,a3 -> complex real ;
coherence
delta c1,c2,c3 is real ;
end;

definition
let c1, c2, c3 be Real;
redefine func delta as delta c1,c2,c3 -> Real;
coherence
delta c1,c2,c3 is Real by XREAL_0:def 1;
end;

theorem Th1: :: QUIN_1:1
for b1, b2, b3, b4 being complex number st b1 <> 0 holds
((b1 * (b4 ^2 )) + (b2 * b4)) + b3 = (b1 * ((b4 + (b2 / (2 * b1))) ^2 )) - ((delta b1,b2,b3) / (4 * b1))
proof end;

theorem Th2: :: QUIN_1:2
for b1, b2, b3, b4 being real number st b1 > 0 & delta b1,b2,b3 <= 0 holds
((b1 * (b4 ^2 )) + (b2 * b4)) + b3 >= 0
proof end;

theorem Th3: :: QUIN_1:3
for b1, b2, b3, b4 being real number st b1 > 0 & delta b1,b2,b3 < 0 holds
((b1 * (b4 ^2 )) + (b2 * b4)) + b3 > 0
proof end;

theorem Th4: :: QUIN_1:4
for b1, b2, b3, b4 being real number st b1 < 0 & delta b1,b2,b3 <= 0 holds
((b1 * (b4 ^2 )) + (b2 * b4)) + b3 <= 0
proof end;

theorem Th5: :: QUIN_1:5
for b1, b2, b3, b4 being real number st b1 < 0 & delta b1,b2,b3 < 0 holds
((b1 * (b4 ^2 )) + (b2 * b4)) + b3 < 0
proof end;

theorem Th6: :: QUIN_1:6
for b1, b2, b3, b4 being real number st b1 > 0 & ((b1 * (b2 ^2 )) + (b3 * b2)) + b4 >= 0 holds
((((2 * b1) * b2) + b3) ^2 ) - (delta b1,b3,b4) >= 0
proof end;

theorem Th7: :: QUIN_1:7
for b1, b2, b3, b4 being real number st b1 > 0 & ((b1 * (b2 ^2 )) + (b3 * b2)) + b4 > 0 holds
((((2 * b1) * b2) + b3) ^2 ) - (delta b1,b3,b4) > 0
proof end;

theorem Th8: :: QUIN_1:8
for b1, b2, b3, b4 being real number st b1 < 0 & ((b1 * (b2 ^2 )) + (b3 * b2)) + b4 <= 0 holds
((((2 * b1) * b2) + b3) ^2 ) - (delta b1,b3,b4) >= 0
proof end;

theorem Th9: :: QUIN_1:9
for b1, b2, b3, b4 being real number st b1 < 0 & ((b1 * (b2 ^2 )) + (b3 * b2)) + b4 < 0 holds
((((2 * b1) * b2) + b3) ^2 ) - (delta b1,b3,b4) > 0
proof end;

theorem Th10: :: QUIN_1:10
for b1, b2, b3 being real number st ( for b4 being real number holds ((b1 * (b4 ^2 )) + (b2 * b4)) + b3 >= 0 ) & b1 > 0 holds
delta b1,b2,b3 <= 0
proof end;

theorem Th11: :: QUIN_1:11
for b1, b2, b3 being real number st ( for b4 being real number holds ((b1 * (b4 ^2 )) + (b2 * b4)) + b3 <= 0 ) & b1 < 0 holds
delta b1,b2,b3 <= 0
proof end;

theorem Th12: :: QUIN_1:12
for b1, b2, b3 being real number st ( for b4 being real number holds ((b1 * (b4 ^2 )) + (b2 * b4)) + b3 > 0 ) & b1 > 0 holds
delta b1,b2,b3 < 0
proof end;

theorem Th13: :: QUIN_1:13
for b1, b2, b3 being real number st ( for b4 being real number holds ((b1 * (b4 ^2 )) + (b2 * b4)) + b3 < 0 ) & b1 < 0 holds
delta b1,b2,b3 < 0
proof end;

theorem Th14: :: QUIN_1:14
for b1, b2, b3, b4 being complex number st b1 <> 0 & ((b1 * (b4 ^2 )) + (b2 * b4)) + b3 = 0 holds
((((2 * b1) * b4) + b2) ^2 ) - (delta b1,b2,b3) = 0
proof end;

Lemma7: for b1, b2 being complex number holds
( not b1 ^2 = b2 ^2 or b1 = b2 or b1 = - b2 )
proof end;

theorem Th15: :: QUIN_1:15
for b1, b2, b3, b4 being real number st b1 <> 0 & delta b1,b2,b3 >= 0 & ((b1 * (b4 ^2 )) + (b2 * b4)) + b3 = 0 & not b4 = ((- b2) - (sqrt (delta b1,b2,b3))) / (2 * b1) holds
b4 = ((- b2) + (sqrt (delta b1,b2,b3))) / (2 * b1)
proof end;

theorem Th16: :: QUIN_1:16
for b1, b2, b3, b4 being real number st b1 <> 0 & delta b1,b2,b3 >= 0 holds
((b1 * (b4 ^2 )) + (b2 * b4)) + b3 = (b1 * (b4 - (((- b2) - (sqrt (delta b1,b2,b3))) / (2 * b1)))) * (b4 - (((- b2) + (sqrt (delta b1,b2,b3))) / (2 * b1)))
proof end;

theorem Th17: :: QUIN_1:17
for b1, b2, b3 being real number st b1 < 0 & delta b1,b2,b3 > 0 holds
((- b2) + (sqrt (delta b1,b2,b3))) / (2 * b1) < ((- b2) - (sqrt (delta b1,b2,b3))) / (2 * b1)
proof end;

theorem Th18: :: QUIN_1:18
for b1, b2, b3, b4 being real number st b1 < 0 & delta b1,b2,b3 > 0 holds
( ((b1 * (b4 ^2 )) + (b2 * b4)) + b3 > 0 iff ( ((- b2) + (sqrt (delta b1,b2,b3))) / (2 * b1) < b4 & b4 < ((- b2) - (sqrt (delta b1,b2,b3))) / (2 * b1) ) )
proof end;

theorem Th19: :: QUIN_1:19
for b1, b2, b3, b4 being real number st b1 < 0 & delta b1,b2,b3 > 0 holds
( ( b4 < ((- b2) + (sqrt (delta b1,b2,b3))) / (2 * b1) or b4 > ((- b2) - (sqrt (delta b1,b2,b3))) / (2 * b1) ) iff ((b1 * (b4 ^2 )) + (b2 * b4)) + b3 < 0 )
proof end;

theorem Th20: :: QUIN_1:20
canceled;

theorem Th21: :: QUIN_1:21
canceled;

theorem Th22: :: QUIN_1:22
for b1, b2, b3, b4 being complex number st b1 <> 0 & delta b1,b2,b3 = 0 & ((b1 * (b4 ^2 )) + (b2 * b4)) + b3 = 0 holds
b4 = - (b2 / (2 * b1))
proof end;

theorem Th23: :: QUIN_1:23
for b1, b2, b3, b4 being real number st b1 > 0 & ((((2 * b1) * b2) + b3) ^2 ) - (delta b1,b3,b4) > 0 holds
((b1 * (b2 ^2 )) + (b3 * b2)) + b4 > 0
proof end;

theorem Th24: :: QUIN_1:24
for b1, b2, b3, b4 being real number st b1 > 0 & delta b1,b2,b3 = 0 holds
( ((b1 * (b4 ^2 )) + (b2 * b4)) + b3 > 0 iff b4 <> - (b2 / (2 * b1)) )
proof end;

theorem Th25: :: QUIN_1:25
for b1, b2, b3, b4 being real number st b1 < 0 & ((((2 * b1) * b2) + b3) ^2 ) - (delta b1,b3,b4) > 0 holds
((b1 * (b2 ^2 )) + (b3 * b2)) + b4 < 0
proof end;

theorem Th26: :: QUIN_1:26
for b1, b2, b3, b4 being real number st b1 < 0 & delta b1,b2,b3 = 0 holds
( ((b1 * (b4 ^2 )) + (b2 * b4)) + b3 < 0 iff b4 <> - (b2 / (2 * b1)) )
proof end;

theorem Th27: :: QUIN_1:27
for b1, b2, b3 being real number st b1 > 0 & delta b1,b2,b3 > 0 holds
((- b2) + (sqrt (delta b1,b2,b3))) / (2 * b1) > ((- b2) - (sqrt (delta b1,b2,b3))) / (2 * b1)
proof end;

theorem Th28: :: QUIN_1:28
for b1, b2, b3, b4 being real number st b1 > 0 & delta b1,b2,b3 > 0 holds
( ((b1 * (b4 ^2 )) + (b2 * b4)) + b3 < 0 iff ( ((- b2) - (sqrt (delta b1,b2,b3))) / (2 * b1) < b4 & b4 < ((- b2) + (sqrt (delta b1,b2,b3))) / (2 * b1) ) )
proof end;

theorem Th29: :: QUIN_1:29
for b1, b2, b3, b4 being real number st b1 > 0 & delta b1,b2,b3 > 0 holds
( ( b4 < ((- b2) - (sqrt (delta b1,b2,b3))) / (2 * b1) or b4 > ((- b2) + (sqrt (delta b1,b2,b3))) / (2 * b1) ) iff ((b1 * (b4 ^2 )) + (b2 * b4)) + b3 > 0 )
proof end;