:: Quadratic Inequalities
:: by Jan Popio\l ek
::
:: Received July 19, 1991
:: Copyright (c) 1991 Association of Mizar Users
:: deftheorem defines delta QUIN_1:def 1 :
theorem Th1: :: QUIN_1:1
theorem :: QUIN_1:2
theorem :: QUIN_1:3
theorem :: QUIN_1:4
theorem :: QUIN_1:5
theorem Th6: :: QUIN_1:6
theorem Th7: :: QUIN_1:7
theorem Th8: :: QUIN_1:8
theorem Th9: :: QUIN_1:9
theorem :: QUIN_1:10
theorem :: QUIN_1:11
theorem :: QUIN_1:12
theorem :: QUIN_1:13
theorem Th14: :: QUIN_1:14
Lm1:
for a, b being complex number holds
( not a ^2 = b ^2 or a = b or a = - b )
theorem :: QUIN_1:15
theorem Th16: :: QUIN_1:16
theorem Th17: :: QUIN_1:17
theorem :: QUIN_1:18
theorem :: QUIN_1:19
theorem :: QUIN_1:20
canceled;
theorem :: QUIN_1:21
canceled;
theorem :: QUIN_1:22
theorem Th23: :: QUIN_1:23
theorem :: QUIN_1:24
theorem Th25: :: QUIN_1:25
theorem :: QUIN_1:26
theorem Th27: :: QUIN_1:27
theorem :: QUIN_1:28
theorem :: QUIN_1:29