:: Basic Properties of Real Numbers - Requirements
:: by Library Committee
::
:: Received February 27, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XXREAL_0, NUMBERS, ARYTM_2, SUBSET_1, ARYTM_3, ZFMISC_1, CARD_1,
XCMPLX_0, REAL_1;
notations TARSKI, ZFMISC_1, SUBSET_1, ARYTM_2, ORDINAL1, NUMBERS, XXREAL_0,
XREAL_0;
constructors ARYTM_2, NUMBERS, XXREAL_0, XREAL_0;
registrations ARYTM_2, XREAL_0, ORDINAL1;
requirements SUBSET, BOOLE;
begin
:: This file contains statements which are obvious for Mizar checker if
:: "requirements REAL" is included in the environment description of an article.
:: They are published for testing purposes only.
:: Users should use appropriate requirements instead of referencing
:: to these theorems.
:: Note that the checker needs also "requirements BOOLE" to accept
:: the statements with attribute 'zero'.
reserve x, y, z for Real;
theorem :: REAL:1
x <= y & x is positive implies y is positive;
theorem :: REAL:2
x <= y & y is negative implies x is negative;
theorem :: REAL:3
x <= y & x is non negative implies y is non negative;
theorem :: REAL:4
x <= y & y is non positive implies x is non positive;
theorem :: REAL:5
x <= y & y is non zero & x is non negative implies y is positive;
theorem :: REAL:6
x <= y & x is non zero & y is non positive implies x is negative;
theorem :: REAL:7
not x <= y & x is non positive implies y is negative;
theorem :: REAL:8
not x <= y & y is non negative implies x is positive;
::theorem
:: numeral(X) & X <> 0 implies X is positive;