The abstract of the Mizar article:

Basic Properties of Rational Numbers

by

Andrzej Kondracki

Received July 10, 1990

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);