:: Basic Properties of Rational Numbers
::  by Andrzej Kondracki
::
:: Received July 10, 1990
:: Copyright (c) 1990-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 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<b implies ex p st a<p & p<b;

theorem :: RAT_1:8
  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: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
  1<denominator(p) iff p is not integer;

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

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

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

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

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

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

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

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

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

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

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

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

theorem :: RAT_1:41
  denominator p=denominator q & numerator p=numerator q implies p = q;

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

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

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

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