:: Basic Properties of Rational Numbers
::  by Andrzej Kondracki
::
:: Received July 10, 1990
:: Copyright (c) 1990-2012 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;
 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, XBOOLE_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions XREAL_0, TARSKI, XBOOLE_0, XCMPLX_0, ARYTM_3;
 theorems INT_1, NAT_1, TARSKI, XREAL_0, XCMPLX_0, XCMPLX_1, XBOOLE_0, NUMBERS,
      ARYTM_3, ARYTM_0, ARYTM_2, ZFMISC_1, ARYTM_1, XREAL_1, XXREAL_0,
      XBOOLE_1, ORDINAL1, XTUPLE_0;
 schemes NAT_1;

begin

reserve x for set,
  a,b for real number,
  k,k1,l,l1 for Element of NAT,
  m,m1,n, n1 for Integer;

:: 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 i1,j1 for Element of NAT;

Lm1: omega c= ({[c,d] where c,d is Element of omega: c,d are_relative_prime &
d <> {}} \ {[k,1] where k is Element of omega: not contradiction}) \/ omega by
XBOOLE_1:7;

Lm2: quotient(i1,j1) = i1/j1
proof
  set x = quotient(i1,j1);
  per cases;
  suppose
A1: j1 = {};
    hence x = {} by ARYTM_3:def 10
      .= i1/j1 by A1;
  end;
  suppose
A2: j1 <> 0;
    +(0,opp 0) = 0 by ARYTM_0:def 3;
    then
A3: opp 0 = 0 by ARYTM_0:11;
    j1 * j1" = 1 by A2,XCMPLX_0:def 7;
    then consider x1,x2,y1,y2 being Real such that
A4: j1 = [*x1,x2*] and
A5: j1" = [*y1,y2*] and
A6: 1 = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *] by XCMPLX_0:def 5;
    +(*(x1,y2),*(x2,y1)) = 0 by A6,ARYTM_0:24;
    then
A7: 1 = +(*(x1,y1),opp*(x2,y2)) by A6,ARYTM_0:def 5
      .= +(*(x1,y1),opp 0) by A4,ARYTM_0:12,24
      .= *(x1,y1) by A3,ARYTM_0:11;
    x2 = 0 by A4,ARYTM_0:24;
    then
A8: j1 = x1 by A4,ARYTM_0:def 5;
    then x1 in omega;
    then reconsider xx = x1 as Element of RAT+ by Lm1;
    consider yy being Element of RAT+ such that
A9: xx *' yy = one by A2,A8,ARYTM_3:54;
A10: xx in RAT+;
    yy in RAT+;
    then reconsider xx1 = xx, yy1 = yy as Element of REAL+ by A10,ARYTM_2:1;
A11: ex x9,y9 being Element of RAT+ st xx1 = x9 & yy1 = y9 & xx1 *' yy1 =
    x9 *' y9 by ARYTM_2:21;
    yy1 in REAL+;
    then reconsider xx1, yy1 as Element of REAL by ARYTM_0:1;
    ex x9,y9 being Element of REAL+ st xx1 = x9 & yy1 = y9 & *(xx1,yy1) =
    x9 *' y9 by ARYTM_0:def 2;
    then
A12: yy = y1 by A2,A8,A7,A9,A11,ARYTM_0:18;
    then
A13: y1 in RAT+;
    y2 = 0 by A5,ARYTM_0:24;
    then
A14: j1" = y1 by A5,ARYTM_0:def 5;
A15: j1 in omega;
    then reconsider a = x, b = j1 as Element of RAT+ by Lm1;
    consider x91,x92,y91,y92 being Real such that
A16: i1 = [*x91,x92*] and
A17: j1" = [*y91,y92*] and
A18: i1*j1" = [* +(*(x91,y91),opp*(x92,y92)), +(*(x91,y92),*(x92,y91))
    *] by XCMPLX_0:def 5;
A19: +(*(x91,y92),*(x92,y91)) = 0 by A18,ARYTM_0:24;
    x1 in omega by A8;
    then consider x19,y19 being Element of REAL+ such that
A20: x1 = x19 and
A21: y1 = y19 and
A22: *(x1,y1) = x19 *' y19 by A13,ARYTM_0:def 2,ARYTM_2:1,2;
A23: ex x199,y199 being Element of RAT+ st x19 = x199 & y19 = y199 & x19
    *' y19 = x199 *' y199 by A8,A12,A15,A20,A21,Lm1,ARYTM_2:21;
A24: y92 = 0 by A17,ARYTM_0:24;
    then j1" = y91 by A17,ARYTM_0:def 5;
    then
A25: i1*j1" = +(*(x91,y1),opp*(x92,0)) by A14,A18,A24,A19,ARYTM_0:def 5
      .= +(*(x91,y1),0) by A3,ARYTM_0:12
      .= *(x91,y1) by ARYTM_0:11;
    x92 = 0 by A16,ARYTM_0:24;
    then
A26: i1 = x91 by A16,ARYTM_0:def 5;
    then
A27: x91 in omega;
    then x91 in RAT+ by Lm1;
    then consider x9,y9 being Element of REAL+ such that
A28: x91 = x9 and
A29: y1 = y9 and
A30: i1 * j1" = x9 *' y9 by A25,A13,ARYTM_0:def 2,ARYTM_2:1;
    consider x99,y99 being Element of RAT+ such that
A31: x9 = x99 and
A32: y9 = y99 and
A33: i1 * j1" = x99 *' y99 by A27,A12,A28,A29,A30,Lm1,ARYTM_2:21;
    a *' b = quotient(i1,j1) *' quotient(j1,one) by ARYTM_3:40
      .= quotient(i1*^j1,j1*^one) by ARYTM_3:49
      .= quotient(i1,one) *' quotient(j1,j1) by ARYTM_3:49
      .= quotient(i1,one) *' one by A2,ARYTM_3:41
      .= quotient(i1,one) by ARYTM_3:53
      .= i1 by ARYTM_3:40
      .= x99 *' one by A26,A28,A31,ARYTM_3:53
      .= x99 *' y99 *' b by A8,A7,A29,A32,A20,A21,A22,A23,ARYTM_3:52;
    hence thesis by A2,A33,ARYTM_3:56;
  end;
end;

0 in omega;

then reconsider 09 = 0 as Element of REAL+ by ARYTM_2:2;

Lm3: for x9 being Element of REAL+ st x9 = a holds 09 - x9 = -a
proof
  let xx being Element of REAL+ such that
A1: xx = a;
  per cases;
  suppose
    xx = 0;
    hence thesis by A1,ARYTM_1:18;
  end;
  suppose
A2: xx <> 0;
    set b = 09 - xx;
A3: 09 <=' xx by ARYTM_1:6;
    then not xx <=' 09 by A2,ARYTM_1:4;
    then
A4: b = [{},xx -' 09] by ARYTM_1:def 2;
    now
      assume b = [0,0];
      then xx -' 09 = 0 by A4,XTUPLE_0:1;
      hence contradiction by A2,A3,ARYTM_1:10;
    end;
    then
A5: not b in {[0,0]} by TARSKI:def 1;
A6: xx -' 09 = xx -' 09 + 09 by ARYTM_2:def 8
      .= xx by A3,ARYTM_1:def 1;
    0 in {0} by TARSKI:def 1;
    then
A7: b in [:{0},REAL+:] by A4,ZFMISC_1:87;
    then b in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 3;
    then reconsider b as Element of REAL by A5,NUMBERS:def 1,XBOOLE_0:def 5;
    consider x1,x2,y1,y2 being Element of REAL such that
A8: a = [*x1,x2*] and
A9: b = [*y1,y2*] and
A10: a+b = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4;
    +(x2,y2) = 0 by A10,ARYTM_0:24;
    then
A11: a+b = +(x1,y1) by A10,ARYTM_0:def 5;
    a in REAL by XREAL_0:def 1;
    then x2 = 0 by A8,ARYTM_0:24;
    then
A12: a = x1 by A8,ARYTM_0:def 5;
    y2 = 0 by A9,ARYTM_0:24;
    then
A13: b = y1 by A9,ARYTM_0:def 5;
    then consider x9,y9 being Element of REAL+ such that
A14: x1 = x9 and
A15: y1 = [0,y9] and
A16: +(x1,y1) = x9 - y9 by A1,A7,A12,ARYTM_0:def 1;
    y9 = xx -' 09 by A4,A13,A15,XTUPLE_0:1;
    then a + b = 0 by A1,A12,A11,A14,A16,A6,ARYTM_1:18;
    hence thesis;
  end;
end;

Lm4: x in RAT implies ex m,n st x = m/n
proof
  assume
A1: x in RAT;
  per cases by A1,NUMBERS:def 3,XBOOLE_0:def 3;
  suppose
    x in RAT+;
    then reconsider x as Element of RAT+;
    take numerator x,denominator x;
    quotient(numerator x,denominator x) = x by ARYTM_3:39;
    hence thesis by Lm2;
  end;
  suppose
A2: x in [:{0},RAT+:];
A3: not x in {[0,0]} by A1,NUMBERS:def 3,XBOOLE_0:def 5;
    consider x1,x2 being set such that
A4: x1 in {0} and
A5: x2 in RAT+ and
A6: x = [x1,x2] by A2,ZFMISC_1:84;
    reconsider x2 as Element of RAT+ by A5;
    reconsider x9 = x2 as Element of REAL+ by A5,ARYTM_2:1;
    x = [0,x9] by A4,A6,TARSKI:def 1;
    then
A7: x2 <> 0 by A3,TARSKI:def 1;
    take m = -numerator x2, n = denominator x2;
A8: x2 = quotient(numerator x2,denominator x2) by ARYTM_3:39
      .= numerator x2/n by Lm2;
    x1 = 0 by A4,TARSKI:def 1;
    hence x = 09 - x9 by A6,A7,ARYTM_1:19
      .= -numerator x2/n by A8,Lm3
      .= m/n;
  end;
end;

Lm5: x = m/l implies x in RAT
proof
A1: m is Element of INT by INT_1:def 2;
  assume
A2: x = m/l;
  then
A3: not x in {[0,0]} by NUMBERS:def 1,XBOOLE_0:def 5;
  per cases;
  suppose
    l = 0;
    then x = m * 0" by A2
      .= 0;
    then x in RAT+ \/ [:{0},RAT+:] by Lm1,XBOOLE_0:def 3;
    hence thesis by A3,NUMBERS:def 3,XBOOLE_0:def 5;
  end;
  suppose
    ex k st m = k;
    then consider k such that
A4: m = k;
    x = quotient(k,l) by A2,A4,Lm2;
    then x in RAT+ \/ [:{0},RAT+:] by XBOOLE_0:def 3;
    hence thesis by A3,NUMBERS:def 3,XBOOLE_0:def 5;
  end;
  suppose that
A5: l <> 0 and
A6: for k holds m <> k;
    consider k such that
A7: m = -k by A1,A6,INT_1:def 1;
A8: k/l = quotient(k,l) by Lm2;
    then k/l in RAT+;
    then reconsider x9 = k/l as Element of REAL+ by ARYTM_2:1;
A9: 0 in {0} by TARSKI:def 1;
A10: x = -k/l by A2,A7;
    m <> 0 by A6;
    then
A11: x9 <> 0 by A2,A5,A10,XCMPLX_1:50;
    x = 09 - x9 by A10,Lm3
      .= [0,x9] by A11,ARYTM_1:19;
    then x in [:{0},RAT+:] by A8,A9,ZFMISC_1:87;
    then x in RAT+ \/ [:{0},RAT+:] by XBOOLE_0:def 3;
    hence thesis by A3,NUMBERS:def 3,XBOOLE_0:def 5;
  end;
end;

Lm6: x = m/n implies x in RAT
proof
  assume
A1: x = m/n;
  n is Element of INT by INT_1:def 2;
  then consider k such that
A2: n = k or n = -k by INT_1:def 1;
  per cases by A2;
  suppose
    n = k;
    hence thesis by A1,Lm5;
  end;
  suppose
    n = -k;
    then x = (-m)/k by A1,XCMPLX_1:192;
    hence thesis by Lm5;
  end;
end;

definition
  redefine func RAT means
  :Def1:
  x in it iff ex m,n st x = m/n;
  compatibility
  proof
    let R be set;
    thus R = RAT implies for x holds x in R iff ex m,n st x = m/n by Lm4,Lm6;
    assume
A1: for x holds x in R iff ex m,n st x = m/n;
    thus R c= RAT
    proof
      let x;
      assume x in R;
      then ex m,n st x = m/n by A1;
      hence thesis by Lm6;
    end;
    let x;
    assume x in RAT;
    then ex m,n st x = m/n by Lm4;
    hence thesis by A1;
  end;
end;

definition
  let r be number;
  attr r is rational means
  :Def2:
  r in RAT;
end;

registration
  cluster rational for Real;
  existence
  proof
    reconsider a = 0, b = 1 as Integer;
    take x=a/b;
    thus x is Real;
    thus x in RAT by Def1;
  end;
end;

registration
  cluster rational for number;
  existence
  proof
    reconsider a = 0, b = 1 as Integer;
    take x=a/b;
    thus x in RAT by Def1;
  end;
end;

definition
  mode Rational is rational number;
end;

theorem Th1:
  x in RAT implies ex m,n st n<>0 & x = m/n
proof
  assume
A1: x in RAT;
  per cases;
  suppose
    x = 0;
    then x = 0/1;
    hence thesis;
  end;
  suppose
A2: x <> 0;
    consider m,n such that
A3: x = m/n by A1,Def1;
    take m,n;
    hereby
      assume n = 0;
      then n" = 0;
      hence contradiction by A2,A3;
    end;
    thus thesis by A3;
  end;
end;

theorem Th2:
  x is Rational implies ex m,n st n<>0 & x = m/n
proof
  assume x is Rational;
  then x in RAT by Def2;
  hence thesis by Th1;
end;

registration
  cluster rational -> real for number;
  coherence
  proof
    let n be number;
    assume n in RAT;
    hence n in REAL by NUMBERS:12;
  end;
end;

theorem Th3:
  m/n is rational
proof
  set x = m/n;
  x is Rational iff x in RAT by Def2;
  hence thesis by Def1;
end;

registration
  cluster integer -> rational for number;
  coherence
  proof
    let x be number;
    assume x is integer;
    then reconsider x as Integer;
    x = x/1;
    hence thesis by Th3;
  end;
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;
  cluster p*q -> rational;
  coherence
  proof
    consider m2,n2 being Integer such that
    n2<>0 and
A1: q = m2/n2 by Th2;
    consider m1,n1 being Integer such that
    n1<>0 and
A2: p = m1/n1 by Th2;
    p*q=(m1*m2)/(n1*n2) by A2,A1,XCMPLX_1:76;
    hence thesis by Th3;
  end;
  cluster p+q -> rational;
  coherence
  proof
    consider m2,n2 being Integer such that
A3: n2<>0 and
A4: q = m2/n2 by Th2;
    consider m1,n1 being Integer such that
A5: n1<>0 and
A6: p = m1/n1 by Th2;
    p+q=(m1*n2+m2*n1)/(n1*n2) by A5,A6,A3,A4,XCMPLX_1:116;
    hence thesis by Th3;
  end;
  cluster p-q -> rational;
  coherence
  proof
    consider m2,n2 being Integer such that
A7: n2<>0 and
A8: q = m2/n2 by Th2;
    consider m1,n1 being Integer such that
A9: n1<>0 and
A10: p = m1/n1 by Th2;
    p-q=(m1*n2-m2*n1)/(n1*n2) by A9,A10,A7,A8,XCMPLX_1:130;
    hence thesis by Th3;
  end;
  cluster p/q -> rational;
  coherence
  proof
    consider m1,n1 being Integer such that
    n1<>0 and
A11: p = m1/n1 by Th2;
    consider m2,n2 being Integer such that
    n2<>0 and
A12: q = m2/n2 by Th2;
    p/q = p*(1/(m2/n2)) by A12
    .= p*((1*n2)/m2) by XCMPLX_1:77
    .= (m1*n2)/(n1*m2) by A11,XCMPLX_1:76;
    hence thesis by Th3;
  end;
end;

registration
  let p;
  cluster -p -> rational;
  coherence
  proof
    consider m,n such that
    n<>0 and
A1: p=m/n by Th2;
    -p = (-m)/n by A1;
    hence thesis;
  end;
  cluster p" -> rational;
  coherence
  proof
    p" = 1/p;
    hence thesis;
  end;
end;

canceled 3;

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

theorem
  a<b implies ex p st a<p & p<b
proof
  set d=b-a;
  set m=[\d"/]+1;
  set l=[\m*a/]+1;
  set p=l/m;
  assume a<b;
  then
A1: a-a<b-a by XREAL_1:9;
  then
A2: 0<m by INT_1:29;
  d"-1<[\d"/] by INT_1:def 6;
  then d"<[\d"/]+1 by XREAL_1:19;
  then d"*d<m*d by A1,XREAL_1:68;
  then
A3: 1<m*d by A1,XCMPLX_0:def 7;
  take p;
A4: 0<>m by A1,INT_1:29;
  m*a-1<[\m*a/] by INT_1:def 6;
  then m*a<[\m*a/]+1 by XREAL_1:19;
  then m"*(m*a)<m"*l by A2,XREAL_1:68;
  then (m"*m)*a<m"*l;
  then 1*a<m"*l by A4,XCMPLX_0:def 7;
  hence a<p;
  [\m*a/]<=m*a by INT_1:def 6;
  then [\m*a/]+1<m*a+m*d by A3,XREAL_1:8;
  then m"*l<m"*(m*b) by A2,XREAL_1:68;
  then m"*l<(m"*m)*b;
  then m"*l<1*b by A4,XCMPLX_0:def 7;
  hence p<b;
end;

theorem Th8:
  ex m,k st k<>0 & p=m/k
proof
  consider m,n such that
A1: n<>0 and
A2: p=m/n by Th2;
  per cases by A1;
  suppose
    0<n;
    then n is Element of NAT by INT_1:3;
    hence thesis by A1,A2;
  end;
  suppose
A3: n<0;
A4: p = -(-m)/n by A2
      .= (-m)/(-n) by XCMPLX_1:188;
A5: -n<>0 by A1;
    -n is Element of NAT by A3,INT_1:3;
    hence thesis by A4,A5;
  end;
end;

:: 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 Th9:
  ex m,k st k<>0 & p=m/k & for n,l st l<>0 & p=n/l holds k<=l
proof
  defpred P[Nat] means ($1<>0 & ex m1 st p=m1/$1);
  ex m,k st k<>0 & p=m/k by Th8;
  then
A1: ex l be Nat st P[l];
  ex k1 be Nat st P[k1] & for l1 be Nat st P[l1] holds k1<=l1 from NAT_1:
  sch 5(A1);
  then consider k1 be Nat such that
A2: k1<>0 and
A3: ex m1 st p=m1/k1 and
A4: for l1 be Nat st (l1<>0 & ex n1 st p=n1/l1) holds k1<=l1;
  reconsider k1 as Element of NAT by ORDINAL1:def 12;
  consider m1 such that
A5: p=m1/k1 and
A6: for l1 be Nat st (l1<>0 & ex n1 st p=n1/l1) holds k1<=l1 by A3,A4;
  take m1, k1;
  thus k1<>0 by A2;
  thus m1/k1=p by A5;
  thus thesis by A6;
end;

definition
  let p;
  func denominator(p) -> Element of NAT means
  :Def3:
  it<>0 & (ex m st p=m/it) & for n,k st k<>0 & p=n/k holds it<=k;
  existence
  proof
    consider m,k such that
A1: k<>0 and
A2: p=m/k and
A3: for n,l st l<>0 & p=n/l holds k<=l by Th9;
    take k;
    thus thesis by A1,A2,A3;
  end;
  uniqueness
  proof
    let k,l such that
A4: k<>0 and
A5: ex m st p=m/k and
A6: for m1,k1 st k1<>0 & p=m1/k1 holds k<=k1 and
A7: l<>0 and
A8: ex n st p=n/l and
A9: for n1,l1 st l1<>0 & p=n1/l1 holds l<=l1;
A10: l<=k by A4,A5,A9;
    k<=l by A6,A7,A8;
    hence thesis by A10,XXREAL_0:1;
  end;
end;

definition
  let p;
  func numerator(p) -> Integer equals
  denominator(p)*p;
  coherence
  proof
A1: denominator(p)<>0 by Def3;
    ex m st p=m/denominator(p) by Def3;
    hence thesis by A1,XCMPLX_1:87;
  end;
end;

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

theorem Th10:
  0<denominator(p)
proof
  0 <> denominator p by Def3;
  hence thesis;
end;

theorem Th11:
  1<=denominator(p)
proof
  0<denominator(p) by Th10;
  then 0+1<=denominator(p) by NAT_1:13;
  hence thesis;
end;

theorem Th12:
  0<denominator(p)"
proof
  0<denominator(p) by Th10;
  hence thesis;
end;

theorem Th13:
  1>=denominator(p)"
proof
A1: 1*denominator(p)"<=denominator(p)*denominator(p)" by Th11,XREAL_1:64;
  0<>denominator(p) by Def3;
  hence thesis by A1,XCMPLX_0:def 7;
end;

theorem Th14:
  numerator(p)=0 iff p=0
proof
  denominator(p)<>0 by Def3;
  hence thesis by XCMPLX_1:6;
end;

theorem Th15:
  p=numerator(p)/denominator(p) & p=numerator(p)*denominator(p)" &
  p=denominator(p)"*numerator(p)
proof
  set x=denominator(p);
A1: x<>0 by Def3;
  thus
A2: numerator(p)/denominator(p)=p*(x*x") .=p*1 by A1,XCMPLX_0:def 7
    .=p;
  hence p=numerator(p)*denominator(p)";
  thus thesis by A2;
end;

theorem
  p<>0 implies denominator(p)=numerator(p)/p
proof
A1: (p"*p)*denominator(p)=p"*numerator(p);
  assume p<>0;
  then 1*denominator(p)=p"*numerator(p) by A1,XCMPLX_0:def 7;
  hence thesis;
end;

theorem Th17:
  p is Integer implies denominator(p)=1 & numerator(p)=p
proof
  assume p is Integer;
  then reconsider m=p as Integer;
  p =m/1;
  then
A1: denominator(p)<=1 by Def3;
  1<=denominator(p) by Th11;
  hence denominator(p)=1 by A1,XXREAL_0:1;
  hence thesis;
end;

theorem Th18:
  (numerator(p)=p or denominator(p)=1) implies p is Integer
proof
  assume
A1: numerator(p)=p or denominator(p)=1;
  per cases by A1;
  suppose
    numerator(p)=p;
    hence thesis;
  end;
  suppose
    denominator(p)=1;
    then numerator(p)=p;
    hence thesis;
  end;
end;

theorem
  numerator(p)=p iff denominator(p)=1 by Th17;

theorem
  (numerator(p)=p or denominator(p)=1) & 0<=p implies p is Element of NAT
proof
  assume that
A1: numerator(p)=p or denominator(p)=1 and
A2: 0<=p;
  p is Integer by A1,Th18;
  hence thesis by A2,INT_1:3;
end;

theorem
  1<denominator(p) iff p is not integer
proof
  now
    assume
A1: not p is Integer;
    denominator(p)>=1 by Th11;
    hence denominator(p)>1 by A1,Th18,XXREAL_0:1;
  end;
  hence thesis by Th17;
end;

Lm7: 1"=1;

theorem
  1>denominator(p)" iff p is not integer
proof
A1: denominator(p)"<=1 by Th13;
  now
    assume not p is Integer;
    then denominator(p)" <> 1 by Lm7,Th18;
    hence denominator(p)"<1 by A1,XXREAL_0:1;
  end;
  hence thesis by Lm7,Th17;
end;

theorem Th23:
  numerator(p)=denominator(p) iff p=1
proof
A1: denominator(p)<>0 by Def3;
  now
    assume numerator(p)=denominator(p);
    then numerator(p)/denominator(p)=1 by A1,XCMPLX_1:60;
    hence p=1 by Th15;
  end;
  hence thesis;
end;

theorem Th24:
  numerator(p)=-denominator(p) iff p=-1
proof
A1: 0<>denominator(p) by Def3;
  now
    assume numerator(p)=-denominator(p);
    hence p=(-denominator(p))/denominator(p) by Th15
      .=-denominator(p)/denominator(p)
      .=-1 by A1,XCMPLX_1:60;
  end;
  hence thesis;
end;

theorem
  -numerator(p)=denominator(p) iff p=-1
proof
  -numerator(p)=denominator(p) iff numerator(p)=-denominator(p);
  hence thesis by Th24;
end;

:: We can multiple the numerator and the denominator of any rational number
:: by any integer (natural) number which is not equal to zero.

theorem Th26:
  m<>0 implies p=(numerator(p)*m)/(denominator(p)*m)
proof
  assume m<>0;
  then numerator(p)/denominator(p)=(numerator(p)*m)/(denominator(p)*m) by
XCMPLX_1:91;
  hence thesis by Th15;
end;

theorem Th27:
  k<>0 & p=m/k implies ex l st m=numerator(p)*l & k=denominator(p) *l
proof
  assume that
A1: k<>0 and
A2: p=m/k;
A3: p*k=m by A1,A2,XCMPLX_1:87;
  defpred P[Nat] means $1*denominator(p)<=k;
A4: denominator(p)<>0 by Def3;
A5: for l be Nat st P[l] holds l<=k
  proof
    0+1<=denominator(p) by A4,NAT_1:13;
    then
A6: k*1<=k*denominator(p) by NAT_1:4;
    let l be Nat such that
A7: l*denominator(p)<=k;
    assume not thesis;
    then k*denominator(p)<l*denominator(p) by A4,XREAL_1:68;
    hence contradiction by A7,A6,XXREAL_0:2;
  end;
A8: 1*denominator(p)<=k by A1,A2,Def3;
  then
A9: ex l1 be Nat st P[l1];
  consider l be Nat such that
A10: P[l] and
A11: for l1 be Nat st P[l1] holds l1<=l from NAT_1:sch 6(A5,A9);
  reconsider l as Element of NAT by ORDINAL1:def 12;
  take l;
A12: 0<>l by A8,A11;
  then
A13: l*denominator(p)<>0 by A4,XCMPLX_1:6;
A14: now
    assume
A15: l*denominator(p)<k;
    then 0+l*denominator(p)<k;
    then 0<=k-l*denominator(p) by XREAL_1:20;
    then reconsider x=k-l*denominator(p) as Element of NAT by INT_1:3;
A16: 0<>x by A15;
    m/k=(numerator(p)*l)/(l*denominator(p)) by A2,A12,Th26;
    then p=(m-numerator(p)*l)/x by A2,A13,A15,XCMPLX_1:123;
    then denominator(p)<=k-l*denominator(p) by A16,Def3;
    then l*denominator(p)+1*denominator(p)<=k by XREAL_1:19;
    then (l+1)*denominator(p)<=k;
    then l+1<=l by A11;
    hence contradiction by NAT_1:13;
  end;
  then k=denominator(p)*l by A10,XXREAL_0:1;
  hence m=numerator(p)/denominator(p)*(denominator(p)*l) by A3,Th15
    .=(numerator(p)/denominator(p)*denominator(p))*l
    .=numerator(p)*l by A4,XCMPLX_1:87;
  thus thesis by A10,A14,XXREAL_0:1;
end;

theorem
  p=m/n & n<>0 implies ex m1 st m=numerator(p)*m1 & n=denominator(p)*m1
proof
  assume that
A1: p=m/n and
A2: n<>0;
  per cases by A2;
  suppose
    n<0;
    then reconsider x=-n as Element of NAT by INT_1:3;
A3: p=-(-m)/n by A1
      .=(-m)/x by XCMPLX_1:188;
    x<>0 by A2;
    then consider k such that
A4: -m=numerator(p)*k and
A5: x=denominator(p)*k by A3,Th27;
    take y=-k;
    thus m=-numerator(p)*k by A4
      .=numerator(p)*y;
    thus n=-denominator(p)*k by A5
      .=denominator(p)*y;
  end;
  suppose
    0<n;
    then reconsider x=n as Element of NAT by INT_1:3;
    consider k such that
A6: m=numerator(p)*k and
A7: x=denominator(p)*k by A1,A2,Th27;
    reconsider y=k as Integer;
    take y;
    thus thesis by A6,A7;
  end;
end;

:: Fraction numerator(p)/denominator(p) is irreducible.

theorem Th29:
  not ex l st 1<l & ex m,k st numerator(p)=m*l & denominator(p)=k* l
proof
  assume not thesis;
  then consider l such that
A1: 1<l and
A2: ex m,k st numerator(p)=m*l & denominator(p)=k*l;
  consider m,k such that
A3: numerator(p)=m*l and
A4: denominator(p)=k*l by A2;
A5: p=(m*l)/(k*l) by A3,A4,Th15
    .=(m/k)*(l/l) by XCMPLX_1:76
    .=m/k*1 by A1,XCMPLX_1:60
    .=m/k;
A6: k<>0 by A4,Def3;
  then k*1<k*l by A1,XREAL_1:68;
  hence contradiction by A4,A6,A5,Def3;
end;

theorem Th30:
  (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)
proof
  assume that
A1: p=m/k and
A2: k<>0 and
A3: not ex l st 1<l & ex m1,k1 st m=m1*l & k=k1*l;
  consider l such that
A4: m=numerator(p)*l and
A5: k=denominator(p)*l by A1,A2,Th27;
  0<l by A2,A5;
  then
A6: 0+1<=l by NAT_1:13;
  l<=1 by A3,A4,A5;
  then
A7: l=1 by A6,XXREAL_0:1;
  hence k=denominator(p) by A5;
  thus thesis by A4,A7;
end;

theorem Th31:
  p<-1 iff numerator(p)<-denominator(p)
proof
A1: 0<>denominator(p) by Def3;
A2: 0<denominator(p)" by Th12;
A3: now
    assume numerator(p)<-denominator(p);
    then
    numerator(p)*denominator(p)"<((-1)*denominator(p))*denominator(p)" by A2,
XREAL_1:68;
    then numerator(p)*denominator(p)"<(-1)*(denominator(p)*denominator(p)");
    then numerator(p)*denominator(p)"<(-1)*1 by A1,XCMPLX_0:def 7;
    hence p<-1 by Th15;
  end;
A4: 0<denominator(p) by Th10;
  now
    assume p<-1;
    then numerator(p)/denominator(p)<-1 by Th15;
    then
    (numerator(p)/denominator(p))*denominator(p)<(-1)*denominator(p) by A4,
XREAL_1:68;
    hence numerator(p)<-denominator(p) by A1,XCMPLX_1:87;
  end;
  hence thesis by A3;
end;

theorem Th32:
  p<=-1 iff numerator(p)<=-denominator(p)
proof
A1: now
    assume
A2: p<=-1;
    per cases by A2,XXREAL_0:1;
    suppose
      p=-1;
      hence numerator(p)<=-denominator(p);
    end;
    suppose
      p<-1;
      hence numerator(p)<=-denominator(p) by Th31;
    end;
  end;
  now
    assume
A3: numerator(p)<=-denominator(p);
    per cases by A3,XXREAL_0:1;
    suppose
      numerator(p)=-denominator(p);
      hence p<=-1 by Th24;
    end;
    suppose
      numerator(p)<-denominator(p);
      hence p<=-1 by Th31;
    end;
  end;
  hence thesis by A1;
end;

theorem
  p<-1 iff denominator(p)<-numerator(p)
proof
  denominator(p)<-numerator(p) iff -(-numerator(p))<-denominator(p) by
XREAL_1:24;
  hence thesis by Th31;
end;

theorem
  p<=-1 iff denominator(p)<=-numerator(p)
proof
  denominator(p)<=-numerator(p) iff -(-numerator(p))<=-denominator(p) by
XREAL_1:24;
  hence thesis by Th32;
end;

theorem Th35:
  p<1 iff numerator(p)<denominator(p)
proof
A1: 0<>denominator(p) by Def3;
A2: 0<denominator(p)" by Th12;
A3: now
    assume numerator(p)<denominator(p);
    then numerator(p)*denominator(p)"<denominator(p)*denominator(p)" by A2,
XREAL_1:68;
    then numerator(p)*denominator(p)"<1 by A1,XCMPLX_0:def 7;
    hence p<1 by Th15;
  end;
A4: 0<denominator(p) by Th10;
  now
    assume p<1;
    then numerator(p)/denominator(p)<1 by Th15;
    then numerator(p)/denominator(p)*denominator(p)<1*denominator(p) by A4,
XREAL_1:68;
    hence numerator(p)<denominator(p) by A1,XCMPLX_1:87;
  end;
  hence thesis by A3;
end;

theorem
  p<=1 iff numerator(p)<=denominator(p)
proof
A1: now
    assume
A2: p<=1;
    per cases by A2,XXREAL_0:1;
    suppose
      p=1;
      hence numerator(p)<=denominator(p);
    end;
    suppose
      p<1;
      hence numerator(p)<=denominator(p) by Th35;
    end;
  end;
  now
    assume
A3: numerator(p)<=denominator(p);
    per cases by A3,XXREAL_0:1;
    suppose
      numerator(p)=denominator(p);
      hence p<=1 by Th23;
    end;
    suppose
      numerator(p)<denominator(p);
      hence p<=1 by Th35;
    end;
  end;
  hence thesis by A1;
end;

theorem
  p<0 iff numerator(p)<0
proof
  now
    assume p<0;
    then numerator(p)/denominator(p)<0 by Th15;
    hence numerator(p)<0;
  end;
  hence thesis;
end;

theorem Th38:
  p<=0 iff numerator(p)<=0
proof
  now
    assume
A1: numerator(p)<=0;
    per cases by A1;
    suppose
      numerator(p)=0;
      hence p<=0 by Th14;
    end;
    suppose
      numerator(p)<0;
      hence p<=0;
    end;
  end;
  hence thesis;
end;

theorem Th39:
  a<p iff a*denominator(p)<numerator(p)
proof
A1: 0<denominator(p)" by Th12;
A2: 0<>denominator(p) by Def3;
A3: now
    assume a*denominator(p)<numerator(p);
    then
    (a*denominator(p))*denominator(p)"<numerator(p)*denominator(p)" by A1,
XREAL_1:68;
    then a*(denominator(p)*denominator(p)")<numerator(p)*denominator(p)";
    then a*1<numerator(p)*denominator(p)" by A2,XCMPLX_0:def 7;
    hence a<p by Th15;
  end;
  0<denominator(p) by Th10;
  hence thesis by A3,XREAL_1:68;
end;

theorem
  a<=p iff a*denominator(p)<=numerator(p)
proof
A1: denominator(p)<>0 by Def3;
A2: now
    assume
A3: a*denominator(p)<=numerator(p);
    per cases by A3,XXREAL_0:1;
    suppose
      a*denominator(p)=numerator(p);
      then p=(a*denominator(p))/(1*denominator(p)) by Th15
        .=(a/1)*(denominator(p)/denominator(p))
        .=a by A1,XCMPLX_1:60;
      hence a<=p;
    end;
    suppose
      a*denominator(p)<numerator(p);
      hence a<=p by Th39;
    end;
  end;
  now
    assume
A4: a<=p;
    per cases by A4,XXREAL_0:1;
    suppose
      a=p;
      hence numerator(p)>=a*denominator(p);
    end;
    suppose
      a<p;
      hence a*denominator(p)<=numerator(p) by Th39;
    end;
  end;
  hence thesis by A2;
end;

theorem
  denominator p=denominator q & numerator p=numerator q implies p = q
proof
  assume that
A1: denominator(p)=denominator(q) and
A2: numerator(p)=numerator(q);
  thus p=numerator(q)/denominator(q) by A1,A2,Th15
    .=q by Th15;
end;

theorem
  p<q iff numerator(p)*denominator(q)<numerator(q)*denominator(p)
proof
A1: 0<denominator(q) by Th10;
  p<q iff numerator(p)/denominator(p)<q by Th15;
  then
A2: p<q iff numerator(p)/denominator(p)<numerator(q)/denominator(q) by Th15;
  0<denominator(p) by Th10;
  hence thesis by A1,A2,XREAL_1:102,106;
end;

theorem Th43:
  denominator(-p)=denominator(p) & numerator(-p)=-numerator(p)
proof
A1: denominator(p)<>0 by Def3;
A2: p=-(-p) .=-numerator(-p)/denominator(-p) by Th15
    .=(-numerator(-p))/denominator(-p);
  denominator(-p)<>0 by Def3;
  then consider l such that
  -numerator(-p)=numerator(p)*l and
A3: denominator(-p)=denominator(p)*l by A2,Th27;
  -p=-numerator(p)/denominator(p) by Th15
    .=(-numerator(p))/denominator(p);
  then consider k such that
A4: -numerator(p)=numerator(-p)*k and
A5: denominator(p)=denominator(-p)*k by A1,Th27;
  denominator p = denominator(p)*l*k by A5,A3
    .= denominator(p)*(l*k);
  then
A6: k = 1 by A1,NAT_1:15,XCMPLX_1:7;
  hence denominator(p)=denominator(-p) by A5;
  thus thesis by A4,A6;
end;

theorem Th44:
  0<p & q=1/p iff numerator(q)=denominator(p) & denominator(q)= numerator(p)
proof
A1: now
    set x=denominator(p);
    assume that
A2: 0<p and
A3: q=1/p;
A4: q=1/(numerator(p)/denominator(p)) by A3,Th15
      .=(1*denominator(p))/numerator(p) by XCMPLX_1:77
      .=denominator(p)/numerator(p);
    reconsider y=numerator(p) as Element of NAT by A2,INT_1:3;
A5: not ex k st 1<k & ex m,l st x=m*k & y=l*k
    proof
      assume not thesis;
      then consider k such that
A6:   1<k and
A7:   ex m,l st x=m*k & y=l*k;
      consider m,l such that
A8:   x=m*k and
A9:   y=l*k by A7;
      now
        assume not 0<=m;
        then m*k<0*m by A6,XREAL_1:69;
        hence contradiction by A8;
      end;
      then reconsider z=m as Element of NAT by INT_1:3;
      denominator(p)=z*k by A8;
      hence contradiction by A6,A9,Th29;
    end;
    0<>numerator(p) by A2,Th38;
    hence numerator(p)=denominator(q) & denominator(p)=numerator(q) by A4,A5
,Th30;
  end;
  now
    assume that
A10: numerator(q)=denominator(p) and
A11: denominator(q)=numerator(p);
    thus 0<p by A11,Th10;
    thus q =(1*denominator(p))/numerator(p) by A10,A11,Th15
      .=1/(numerator(p)/denominator(p)) by XCMPLX_1:77
      .=1/p by Th15;
  end;
  hence thesis by A1;
end;

theorem
  p<0 & q=1/p iff numerator(q)=-denominator(p) & denominator(q)=- numerator(p)
proof
A1: now
    set s=-q;
    set r=-p;
    assume that
A2: p<0 and
A3: q=1/p;
A4: s=1/r by A3,XCMPLX_1:188;
A5: 0<r by A2,XREAL_1:58;
    then numerator(s)=denominator(r) by A4,Th44;
    then -numerator(q)=denominator(r) by Th43;
    then
A6: -(-numerator(q))=-denominator(p) by Th43;
    denominator(s)=numerator(r) by A5,A4,Th44;
    then denominator(q)=numerator(r) by Th43;
    hence numerator(q)=-denominator(p) & denominator(q)=-numerator(p) by A6
,Th43;
  end;
  now
    assume that
A7: numerator(q)=-denominator(p) and
A8: denominator(q)=-numerator( p);
    thus p<0 by A8,Th10;
    thus q=(-denominator(p))/(-numerator(p)) by A7,A8,Th15
      .=-(denominator(p)/(-numerator(p)))
      .=-(-denominator(p)/numerator(p)) by XCMPLX_1:188
      .=(1*denominator(p))/numerator(p)
      .=1/(numerator(p)/denominator(p)) by XCMPLX_1:77
      .=1/p by Th15;
  end;
  hence thesis by A1;
end;