Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Basic Properties of Rational Numbers

by
Andrzej Kondracki

MML identifier: RAT_1
[ Mizar article, MML identifier index ]

```environ

vocabulary ARYTM, INT_1, ABSVALUE, ARYTM_3, ARYTM_1, RELAT_1, RAT_1, ORDINAL2,
BOOLE, COMPLEX1, OPPCAT_1, ARYTM_2, QUOFIELD, ORDINAL1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ORDINAL2, ARYTM_3,
ARYTM_2, NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, ABSVALUE,
INT_1, ARYTM_1;
constructors NAT_1, XCMPLX_0, XREAL_0, ORDINAL2, INT_1, ABSVALUE, XBOOLE_0,
ARYTM_3, ARYTM_0, FUNCT_4, ARYTM_2, ARYTM_1, REAL_1;
clusters INT_1, XREAL_0, REAL_1, ZFMISC_1, XBOOLE_0, NUMBERS, ARYTM_3,
ORDINAL2, ARYTM_2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin

reserve X,x for set,
a,b,c,d for real number,
k,k1,l,l1 for Nat,
m,m1,n,n1 for Integer;

:: Auxiliary theorems & redefinitions.

definition let i be integer number;
cluster abs i -> natural;
end;

definition let k;
redefine func abs k -> Nat;
end;

:: We define RAT as a set of real numbers, each of which can be expressed
:: as a quotient of integer dividend and divisor (divisor is not equal
:: to zero).

reserve i,j,i1,j1 for Nat;

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 number;
attr r is rational means
:: RAT_1:def 2
r in RAT;
end;

definition
cluster rational Real;
end;

definition
cluster rational 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;

canceled;

theorem :: RAT_1:3
x is Rational implies ex m,n st n<>0 & x = m/n;

theorem :: RAT_1:4
RAT c= REAL;

definition
cluster rational -> real number;
end;

canceled;

theorem :: RAT_1:6
(ex m,n st x = m/n) implies x is rational;

theorem :: RAT_1:7
for x being Integer holds x is Rational;

definition
cluster integer -> rational number;
end;

canceled 3;

theorem :: RAT_1:11
INT c= RAT;

theorem :: RAT_1:12
NAT c= RAT;

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.

definition let p,q;
cluster p*q -> rational;
cluster p+q -> rational;
cluster p-q -> rational;
end;

definition let p,m;
cluster p+m -> rational;
cluster p-m -> rational;
cluster p*m -> rational;
end;

definition let m,p;
cluster m+p -> rational;
cluster m-p -> rational;
cluster m*p -> rational;
end;

definition let p,k;
cluster p+k -> rational;
cluster p-k -> rational;
cluster p*k -> rational;
end;

definition let k,p;
cluster k+p -> rational;
cluster k-p -> rational;
cluster k*p -> rational;
end;

definition
let p;
cluster -p -> rational;

cluster abs(p) -> rational;
end;

:: Now we prove that the quotient of two rational numbers is rational

canceled 3;

theorem :: RAT_1:16
for p,q holds p/q is Rational;

definition let p, q be rational number;
cluster p/q -> rational;
end;

canceled 4;

theorem :: RAT_1:21
p" is Rational;

definition let p be rational number;
cluster p" -> rational;
end;

:: RAT is dense, that is there exists at least one rational number between
:: any two distinct real numbers.

theorem :: RAT_1:22
a<b implies ex p st a<p & p<b;

canceled;

theorem :: RAT_1:24
ex m,k st k<>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:25
ex m,k st k<>0 & p=m/k & for n,l st l<>0 & p=n/l holds k<=l;

definition let p;
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;
func numerator(p) -> Integer equals
:: RAT_1:def 4
denominator(p)*p;
end;

:: Some basic theorems concerning p, numerator(p) and denominator(p).

canceled;

theorem :: RAT_1:27
0<denominator(p);

canceled;

theorem :: RAT_1:29
1<=denominator(p);

theorem :: RAT_1:30
0<denominator(p)";

canceled 3;

theorem :: RAT_1:34
1>=denominator(p)";

canceled;

theorem :: RAT_1:36
numerator(p)=0 iff p=0;

theorem :: RAT_1:37
p=numerator(p)/denominator(p) & p=numerator(p)*denominator(p)"
& p=denominator(p)"*numerator(p);

theorem :: RAT_1:38
p<>0 implies denominator(p)=numerator(p)/p;

canceled;

theorem :: RAT_1:40
p is Integer implies denominator(p)=1 & numerator(p)=p;

theorem :: RAT_1:41
(numerator(p)=p or denominator(p)=1) implies p is Integer;

theorem :: RAT_1:42
numerator(p)=p iff denominator(p)=1;

canceled;

theorem :: RAT_1:44
(numerator(p)=p or denominator(p)=1) & 0<=p implies p is Nat;

theorem :: RAT_1:45
1<denominator(p) iff p is not integer;

theorem :: RAT_1:46
1>denominator(p)" iff p is not integer;

theorem :: RAT_1:47
numerator(p)=denominator(p) iff p=1;

theorem :: RAT_1:48
numerator(p)=-denominator(p) iff p=-1;

theorem :: RAT_1:49
-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:50
m<>0 implies p=(numerator(p)*m)/(denominator(p)*m);

canceled 9;

theorem :: RAT_1:60
k<>0 & p=m/k implies (ex l st m=numerator(p)*l & k=denominator(p)*l);

theorem :: RAT_1:61
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:62
not ex l st 1<l & ex m,k st numerator(p)=m*l & denominator(p)=k*l;

theorem :: RAT_1:63
(p=m/k & k<>0 & not ex l st 1<l & ex m1,k1 st m=m1*l & k=k1*l)
implies k=denominator(p) & m=numerator(p);

theorem :: RAT_1:64
p<-1 iff numerator(p)<-denominator(p);

theorem :: RAT_1:65
p<=-1 iff numerator(p)<=-denominator(p);

theorem :: RAT_1:66
p<-1 iff denominator(p)<-numerator(p);

theorem :: RAT_1:67
p<=-1 iff denominator(p)<=-numerator(p);

canceled 4;

theorem :: RAT_1:72
p<1 iff numerator(p)<denominator(p);

theorem :: RAT_1:73
p<=1 iff numerator(p)<=denominator(p);

canceled 2;

theorem :: RAT_1:76
p<0 iff numerator(p)<0;

theorem :: RAT_1:77
p<=0 iff numerator(p)<=0;

canceled 2;

theorem :: RAT_1:80
a<p iff a*denominator(p)<numerator(p);

theorem :: RAT_1:81
a<=p iff a*denominator(p)<=numerator(p);

canceled 2;

theorem :: RAT_1:84
p=q iff (denominator(p)=denominator(q) & numerator(p)=numerator(q));

canceled;

theorem :: RAT_1:86
p<q iff numerator(p)*denominator(q)<numerator(q)*denominator(p);

theorem :: RAT_1:87
denominator(-p)=denominator(p) & numerator(-p)=-numerator(p);

theorem :: RAT_1:88
0<p & q=1/p iff numerator(q)=denominator(p) & denominator(q)=numerator(p);

theorem :: RAT_1:89
p<0 & q=1/p iff numerator(q)=-denominator(p) & denominator(q)=-numerator(p);
```