:: Basic Properties of Rational Numbers
:: by Andrzej Kondracki
::
:: Received July 10, 1990
:: Copyright (c) 1990-2017 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 NUMBERS, XREAL_0, ORDINAL1, SUBSET_1, INT_1, TARSKI, ARYTM_3,
XBOOLE_0, CARD_1, ARYTM_0, RELAT_1, REAL_1, ARYTM_2, ORDINAL2, ARYTM_1,
ZFMISC_1, XXREAL_0, NAT_1, RAT_1, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ORDINAL3, ARYTM_3,
ARYTM_2, NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, INT_1,
ARYTM_1, XXREAL_0;
constructors FUNCT_4, ARYTM_1, ARYTM_0, XXREAL_0, REAL_1, NAT_1, INT_1,
ORDINAL3;
registrations ORDINAL1, ARYTM_3, ARYTM_2, NUMBERS, XXREAL_0, XREAL_0, NAT_1,
INT_1, ORDINAL3;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin
reserve x for object,
a,b for Real,
k,k1,i1,j1,w for Nat,
m,m1,n,n1 for Integer;
definition
redefine func RAT means
:: RAT_1:def 1
x in it iff ex m,n st x = m/n;
end;
definition
let r be object;
attr r is rational means
:: RAT_1:def 2
r in RAT;
end;
registration
cluster rational for Real;
end;
registration
cluster rational for number;
end;
definition
mode Rational is rational Number;
end;
theorem :: RAT_1:1
x in RAT implies ex m,n st n<>0 & x = m/n;
theorem :: RAT_1:2
x is rational implies ex m,n st n<>0 & x = m/n;
registration
cluster rational -> real for object;
end;
theorem :: RAT_1:3
m/n is rational;
registration
cluster integer -> rational for object;
end;
reserve p,q for Rational;
:: Now we prove that fractions of integer denominator and natural numerator
:: or of natural denominator and numerator, etc., are all rational numbers.
registration
let p,q be Rational;
cluster p*q -> rational;
cluster p+q -> rational;
cluster p-q -> rational;
cluster p/q -> rational;
end;
registration
let p be Rational;
cluster -p -> rational;
cluster p" -> rational;
end;
::$CT 3
:: RAT is dense, that is there exists at least one rational number between
:: any two distinct real numbers.
theorem :: RAT_1:7
a**0 & p=m/k;
:: Each rational number can be uniquely expressed as a ratio of two
:: relatively prime numbers, the first is integer and the latter is natural
:: (but not equal to zero). Function denominator(p) is defined as the least
:: natural denominator of all denominators of fractions integer/natural=p.
:: Function numerator(p) is defined as a product of p and denominator(p).
theorem :: RAT_1:9
ex m,k st k<>0 & p=m/k & for n,w st w<>0 & p=n/w holds k<=w;
definition
let p be Rational;
func denominator(p) -> Nat means
:: RAT_1:def 3
it<>0 & (ex m st p=m/it) & for n,k st k<>0 & p=n/k holds it<=k;
end;
definition
let p be Rational;
func numerator(p) -> Integer equals
:: RAT_1:def 4
denominator(p)*p;
end;
:: Some basic theorems concerning p, numerator(p) and denominator(p).
theorem :: RAT_1:10
0 < denominator(p);
registration
let p;
cluster denominator(p) -> positive;
end;
theorem :: RAT_1:11
1 <= denominator(p);
theorem :: RAT_1:12
0 < denominator(p)";
theorem :: RAT_1:13
1 >= denominator(p)";
theorem :: RAT_1:14
numerator(p)=0 iff p=0;
theorem :: RAT_1:15
p=numerator(p)/denominator(p) & p=numerator(p)*denominator(p)";
theorem :: RAT_1:16
p<>0 implies denominator(p)=numerator(p)/p;
theorem :: RAT_1:17
p is Integer implies denominator(p)=1 & numerator(p)=p;
theorem :: RAT_1:18
(numerator(p)=p or denominator(p)=1) implies p is Integer;
theorem :: RAT_1:19
numerator(p)=p iff denominator(p)=1;
theorem :: RAT_1:20
(numerator(p)=p or denominator(p)=1) & 0<=p implies p is Element of NAT;
theorem :: RAT_1:21
1denominator(p)" iff p is not integer;
theorem :: RAT_1:23
numerator(p)=denominator(p) iff p=1;
theorem :: RAT_1:24
numerator(p)=-denominator(p) iff p=-1;
theorem :: RAT_1:25
-numerator(p)=denominator(p) iff p=-1;
:: We can multiple the numerator and the denominator of any rational number
:: by any integer (natural) number which is not equal to zero.
theorem :: RAT_1:26
m<>0 implies p=(numerator(p)*m)/(denominator(p)*m);
theorem :: RAT_1:27
k<>0 & p=m/k implies ex w st m=numerator(p)*w & k=denominator(p)*w;
theorem :: RAT_1:28
p=m/n & n<>0 implies ex m1 st m=numerator(p)*m1 & n=denominator(p)*m1;
:: Fraction numerator(p)/denominator(p) is irreducible.
theorem :: RAT_1:29
not ex w st 10 & not ex w st 1**