:: RAT_1 semantic presentation

begin

             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 : verum  }  ) \/ omega
by XBOOLE_1:7;

Lm2:  for i1, j1 being Element of NAT holds quotient (i1,j1) = i1 / j1
proof
let i1, j1 be Element of NAT ; ::_thesis: quotient (i1,j1) = i1 / j1
set x = quotient (i1,j1);
percases ( j1 = {} or j1 <> 0 ) ;
supposeA1: j1 = {} ; ::_thesis: quotient (i1,j1) = i1 / j1
hence  quotient (i1,j1) = {} by ARYTM_3:def_10
.= i1 / j1 by A1 ;
::_thesis: verum
end;
supposeA2: j1 <> 0 ; ::_thesis: quotient (i1,j1) = i1 / j1
 + (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, ARYTM_0: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 = xx1, yy1 = 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 = quotient (i1,j1), 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, ARYTM_2: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  quotient (i1,j1) = i1 / j1 by A2, A33, ARYTM_3:56; ::_thesis: verum
end;
end;
end;

 0 in omega
;

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

Lm3:  for a being real number
for x9 being Element of REAL+ st x9 = a holds
09 - x9 = - a
proof
let a be real number ; ::_thesis: for x9 being Element of REAL+ st x9 = a holds
09 - x9 = - a
let xx be Element of REAL+ ; ::_thesis: ( xx = a implies 09 - xx = - a )
assume A1: xx = a ; ::_thesis: 09 - xx = - a
percases ( xx = 0 or xx <> 0 ) ;
suppose xx = 0 ; ::_thesis: 09 - xx = - a
hence  09 - xx = - a by A1, ARYTM_1:18; ::_thesis: verum
end;
supposeA2: xx <> 0 ; ::_thesis: 09 - xx = - a
set b = 09 - xx;
A3: 09 <=' xx by ARYTM_1:6;
then  not xx <=' 09 by A2, ARYTM_1:4;
then A4: 09 - xx = [{},(xx -' 09)] by ARYTM_1:def_2;
now__::_thesis:_not_09_-_xx_=_[0,0]
assume  09 - xx = [0,0] ; ::_thesis: contradiction
then  xx -' 09 = 0 by A4, XTUPLE_0:1;
hence  contradiction by A2, A3, ARYTM_1:10; ::_thesis: verum
end;
then A5: not 09 - xx 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: 09 - xx in [:{0},REAL+:] by A4, ZFMISC_1:87;
then  09 - xx in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def_3;
then reconsider b = 09 - xx 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  09 - xx = - a ; ::_thesis: verum
end;
end;
end;

Lm4:  for x being set st x in RAT holds
ex m, n being Integer st x = m / n
proof
let x be set ; ::_thesis: ( x in RAT implies ex m, n being Integer st x = m / n )
assume A1: x in RAT ; ::_thesis: ex m, n being Integer st x = m / n
percases ( x in RAT+ or x in [:{0},RAT+:] ) by A1, NUMBERS:def_3, XBOOLE_0:def_3;
suppose x in RAT+ ; ::_thesis: ex m, n being Integer st x = m / n
then reconsider x = x as Element of RAT+ ;
take  numerator x ; ::_thesis: ex n being Integer st x = (numerator x) / n
take  denominator x ; ::_thesis: x = (numerator x) / (denominator x)
 quotient ((numerator x),(denominator x)) = x by ARYTM_3:39;
hence  x = (numerator x) / (denominator x) by Lm2; ::_thesis: verum
end;
supposeA2: x in [:{0},RAT+:] ; ::_thesis: ex m, n being Integer st x = m / n
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 = 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); ::_thesis: ex n being Integer st x = m / n
take n = denominator x2; ::_thesis: x = m / n
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 ;
::_thesis: verum
end;
end;
end;

Lm5:  for x being set
for l being Element of NAT
for m being Integer st x = m / l holds
x in RAT
proof
let x be set ; ::_thesis: for l being Element of NAT
for m being Integer st x = m / l holds
x in RAT
let l be Element of NAT ; ::_thesis: for m being Integer st x = m / l holds
x in RAT
let m be Integer; ::_thesis: ( x = m / l implies x in RAT )
A1: m is Element of INT by INT_1:def_2;
assume A2: x = m / l ; ::_thesis: x in RAT
then A3: not x in {[0,0]} by NUMBERS:def_1, XBOOLE_0:def_5;
percases ( l = 0 or ex k being Element of NAT st m = k or ( l <> 0 & ( for k being Element of NAT holds m <> k ) ) ) ;
suppose l = 0 ; ::_thesis: x in RAT
then x = m * (0 ") by A2
.= 0 ;
then  x in RAT+ \/ [:{0},RAT+:] by Lm1, XBOOLE_0:def_3;
hence  x in RAT by A3, NUMBERS:def_3, XBOOLE_0:def_5; ::_thesis: verum
end;
suppose ex k being Element of NAT st m = k ; ::_thesis: x in RAT
then consider k being Element of NAT  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  x in RAT by A3, NUMBERS:def_3, XBOOLE_0:def_5; ::_thesis: verum
end;
supposethat A5: l <> 0 and
A6: for k being Element of NAT holds m <> k ; ::_thesis: x in RAT
consider k being Element of NAT  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  x in RAT by A3, NUMBERS:def_3, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;

Lm6:  for x being set
for m, n being Integer st x = m / n holds
x in RAT
proof
let x be set ; ::_thesis: for m, n being Integer st x = m / n holds
x in RAT
let m, n be Integer; ::_thesis: ( x = m / n implies x in RAT )
assume A1: x = m / n ; ::_thesis: x in RAT
 n is Element of INT by INT_1:def_2;
then consider k being Element of NAT  such that
A2: ( n = k or n = - k ) by INT_1:def_1;
percases ( n = k or n = - k ) by A2;
suppose n = k ; ::_thesis: x in RAT
hence  x in RAT by A1, Lm5; ::_thesis: verum
end;
suppose n = - k ; ::_thesis: x in RAT
then  x = (- m) / k by A1, XCMPLX_1:192;
hence  x in RAT by Lm5; ::_thesis: verum
end;
end;
end;

definition
redefine func RAT  means :Def1: :: RAT_1:def 1
 for x being set holds
( x in it iff ex m, n being Integer st x = m / n );
compatibility
 for b1 being set holds
( b1 = RAT iff for x being set holds
( x in b1 iff ex m, n being Integer st x = m / n ) )
proof
let R be set ; ::_thesis: ( R = RAT iff for x being set holds
( x in R iff ex m, n being Integer st x = m / n ) )
thus  ( R = RAT implies for x being set holds
( x in R iff ex m, n being Integer st x = m / n ) ) by Lm4, Lm6; ::_thesis: ( ( for x being set holds
( x in R iff ex m, n being Integer st x = m / n ) ) implies R = RAT )
assume A1: for x being set holds
( x in R iff ex m, n being Integer st x = m / n ) ; ::_thesis: R = RAT
thus  R c= RAT :: according to XBOOLE_0:def_10 ::_thesis: RAT c= R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R or x in RAT )
assume  x in R ; ::_thesis: x in RAT
then  ex m, n being Integer st x = m / n by A1;
hence  x in RAT by Lm6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in RAT or x in R )
assume  x in RAT ; ::_thesis: x in R
then  ex m, n being Integer st x = m / n by Lm4;
hence  x in R by A1; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines RAT RAT_1:def_1_:_
 for b1 being set holds
( b1 = RAT iff for x being set holds
( x in b1 iff ex m, n being Integer st x = m / n ) );

definition
let r be number ;
attrr is rational  means :Def2: :: RAT_1:def 2
r in RAT ;
end;

:: deftheorem Def2 defines rational RAT_1:def_2_:_
 for r being number holds
( r is rational iff r in RAT );

registration
cluster ext-real V31() real rational for Element of REAL ;
existence
 ex b1 being Real st b1 is rational
proof
reconsider a = 0 , b = 1 as Integer ;
take x = a / b; ::_thesis: ( x is Real & x is rational )
thus  x is Real ; ::_thesis: x is rational
thus  x in RAT by Def1; :: according to RAT_1:def_2 ::_thesis: verum
end;
end;

registration
cluster rational for set ;
existence
 ex b1 being number st b1 is rational
proof
reconsider a = 0 , b = 1 as Integer ;
take x = a / b; ::_thesis: x is rational
thus  x in RAT by Def1; :: according to RAT_1:def_2 ::_thesis: verum
end;
end;

definition
mode Rational is rational number ;
end;

theorem Th1: :: RAT_1:1
for x being set st x in RAT holds
ex m, n being Integer st
( n <> 0 & x = m / n )
proof
let x be set ; ::_thesis: ( x in RAT implies ex m, n being Integer st
( n <> 0 & x = m / n ) )
assume A1: x in RAT ; ::_thesis: ex m, n being Integer st
( n <> 0 & x = m / n )
percases ( x = 0 or x <> 0 ) ;
suppose x = 0 ; ::_thesis: ex m, n being Integer st
( n <> 0 & x = m / n )
then  x = 0 / 1 ;
hence  ex m, n being Integer st
( n <> 0 & x = m / n ) ; ::_thesis: verum
end;
supposeA2: x <> 0 ; ::_thesis: ex m, n being Integer st
( n <> 0 & x = m / n )
consider m, n being Integer such that
A3: x = m / n by A1, Def1;
take  m ; ::_thesis: ex n being Integer st
( n <> 0 & x = m / n )
take  n ; ::_thesis: ( n <> 0 & x = m / n )
hereby  ::_thesis: x = m / n
assume  n = 0 ; ::_thesis: contradiction
then  n " = 0 ;
hence  contradiction by A2, A3; ::_thesis: verum
end;
thus  x = m / n by A3; ::_thesis: verum
end;
end;
end;

theorem Th2: :: RAT_1:2
for x being set st x is Rational holds
ex m, n being Integer st
( n <> 0 & x = m / n )
proof
let x be set ; ::_thesis: ( x is Rational implies ex m, n being Integer st
( n <> 0 & x = m / n ) )
assume  x is Rational ; ::_thesis: ex m, n being Integer st
( n <> 0 & x = m / n )
then  x in RAT by Def2;
hence  ex m, n being Integer st
( n <> 0 & x = m / n ) by Th1; ::_thesis: verum
end;

registration
cluster rational  ->  real for set ;
coherence
 for b1 being number st b1 is rational holds
b1 is real
proof
let n be number ; ::_thesis: ( n is rational implies n is real )
assume  n in RAT ; :: according to RAT_1:def_2 ::_thesis: n is real
hence  n in REAL by NUMBERS:12; :: according to XREAL_0:def_1 ::_thesis: verum
end;
end;

theorem Th3: :: RAT_1:3
for m, n being Integer holds m / n is rational
proof
let m, n be Integer; ::_thesis: m / n is rational
set x = m / n;
 ( m / n is Rational iff m / n in RAT ) by Def2;
hence  m / n is rational by Def1; ::_thesis: verum
end;

registration
cluster integer  ->  rational for set ;
coherence
 for b1 being number st b1 is integer holds
b1 is rational
proof
let x be number ; ::_thesis: ( x is integer implies x is rational )
assume  x is integer ; ::_thesis: x is rational
then reconsider x = x as Integer ;
 x = x / 1 ;
hence  x is rational by Th3; ::_thesis: verum
end;
end;


registration
let p, q be Rational;
clusterp * q ->  rational ;
coherence
 p * q is rational
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  p * q is rational by Th3; ::_thesis: verum
end;
clusterp + q ->  rational ;
coherence
 p + q is rational
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  p + q is rational by Th3; ::_thesis: verum
end;
clusterp - q ->  rational ;
coherence
 p - q is rational
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  p - q is rational by Th3; ::_thesis: verum
end;
clusterp / q ->  rational ;
coherence
 p / q is rational
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  p / q is rational by Th3; ::_thesis: verum
end;
end;

registration
let p be Rational;
cluster - p ->  rational ;
coherence
 - p is rational
proof
consider m, n being Integer such that
 n <> 0 and
A1: p = m / n by Th2;
 - p = (- m) / n by A1;
hence  - p is rational ; ::_thesis: verum
end;
clusterp "  ->  rational ;
coherence
 p " is rational
proof
 p " = 1 / p ;
hence  p " is rational ; ::_thesis: verum
end;
end;

theorem :: RAT_1:4
canceled;

theorem :: RAT_1:5
canceled;

theorem :: RAT_1:6
canceled;

theorem :: RAT_1:7
for a, b being real number st a < b holds
ex p being Rational st
( a < p & p < b )
proof
let a, b be real number ; ::_thesis: ( a < b implies ex p being Rational st
( a < p & p < b ) )
set d = b - a;
set m = [\((b - a) ")/] + 1;
set l = [\(([\((b - a) ")/] + 1) * a)/] + 1;
set p = ([\(([\((b - a) ")/] + 1) * a)/] + 1) / ([\((b - a) ")/] + 1);
assume  a < b ; ::_thesis: ex p being Rational st
( a < p & p < b )
then A1: a - a < b - a by XREAL_1:9;
then A2: 0 < [\((b - a) ")/] + 1 by INT_1:29;
 ((b - a) ") - 1 < [\((b - a) ")/] by INT_1:def_6;
then  (b - a) " < [\((b - a) ")/] + 1 by XREAL_1:19;
then  ((b - a) ") * (b - a) < ([\((b - a) ")/] + 1) * (b - a) by A1, XREAL_1:68;
then A3: 1 < ([\((b - a) ")/] + 1) * (b - a) by A1, XCMPLX_0:def_7;
take  ([\(([\((b - a) ")/] + 1) * a)/] + 1) / ([\((b - a) ")/] + 1) ; ::_thesis: ( a < ([\(([\((b - a) ")/] + 1) * a)/] + 1) / ([\((b - a) ")/] + 1) & ([\(([\((b - a) ")/] + 1) * a)/] + 1) / ([\((b - a) ")/] + 1) < b )
A4: 0 <> [\((b - a) ")/] + 1 by A1, INT_1:29;
 (([\((b - a) ")/] + 1) * a) - 1 < [\(([\((b - a) ")/] + 1) * a)/] by INT_1:def_6;
then  ([\((b - a) ")/] + 1) * a < [\(([\((b - a) ")/] + 1) * a)/] + 1 by XREAL_1:19;
then  (([\((b - a) ")/] + 1) ") * (([\((b - a) ")/] + 1) * a) < (([\((b - a) ")/] + 1) ") * ([\(([\((b - a) ")/] + 1) * a)/] + 1) by A2, XREAL_1:68;
then  ((([\((b - a) ")/] + 1) ") * ([\((b - a) ")/] + 1)) * a < (([\((b - a) ")/] + 1) ") * ([\(([\((b - a) ")/] + 1) * a)/] + 1) ;
then  1 * a < (([\((b - a) ")/] + 1) ") * ([\(([\((b - a) ")/] + 1) * a)/] + 1) by A4, XCMPLX_0:def_7;
hence  a < ([\(([\((b - a) ")/] + 1) * a)/] + 1) / ([\((b - a) ")/] + 1) ; ::_thesis: ([\(([\((b - a) ")/] + 1) * a)/] + 1) / ([\((b - a) ")/] + 1) < b
 [\(([\((b - a) ")/] + 1) * a)/] <= ([\((b - a) ")/] + 1) * a by INT_1:def_6;
then  [\(([\((b - a) ")/] + 1) * a)/] + 1 < (([\((b - a) ")/] + 1) * a) + (([\((b - a) ")/] + 1) * (b - a)) by A3, XREAL_1:8;
then  (([\((b - a) ")/] + 1) ") * ([\(([\((b - a) ")/] + 1) * a)/] + 1) < (([\((b - a) ")/] + 1) ") * (([\((b - a) ")/] + 1) * b) by A2, XREAL_1:68;
then  (([\((b - a) ")/] + 1) ") * ([\(([\((b - a) ")/] + 1) * a)/] + 1) < ((([\((b - a) ")/] + 1) ") * ([\((b - a) ")/] + 1)) * b ;
then  (([\((b - a) ")/] + 1) ") * ([\(([\((b - a) ")/] + 1) * a)/] + 1) < 1 * b by A4, XCMPLX_0:def_7;
hence  ([\(([\((b - a) ")/] + 1) * a)/] + 1) / ([\((b - a) ")/] + 1) < b ; ::_thesis: verum
end;

theorem Th8: :: RAT_1:8
for p being Rational ex m being Integer ex k being Element of NAT st
( k <> 0 & p = m / k )
proof
let p be Rational; ::_thesis: ex m being Integer ex k being Element of NAT st
( k <> 0 & p = m / k )
consider m, n being Integer such that
A1: n <> 0 and
A2: p = m / n by Th2;
percases ( 0 < n or n < 0 ) by A1;
suppose 0 < n ; ::_thesis: ex m being Integer ex k being Element of NAT st
( k <> 0 & p = m / k )
then  n is Element of NAT by INT_1:3;
hence  ex m being Integer ex k being Element of NAT st
( k <> 0 & p = m / k ) by A1, A2; ::_thesis: verum
end;
supposeA3: n < 0 ; ::_thesis: ex m being Integer ex k being Element of NAT st
( k <> 0 & p = m / k )
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  ex m being Integer ex k being Element of NAT st
( k <> 0 & p = m / k ) by A4, A5; ::_thesis: verum
end;
end;
end;

theorem Th9: :: RAT_1:9
for p being Rational ex m being Integer ex k being Element of NAT st
( k <> 0 & p = m / k & ( for n being Integer
for l being Element of NAT st l <> 0 & p = n / l holds
k <= l ) )
proof
let p be Rational; ::_thesis: ex m being Integer ex k being Element of NAT st
( k <> 0 & p = m / k & ( for n being Integer
for l being Element of NAT st l <> 0 & p = n / l holds
k <= l ) )
defpred S1[ Nat] means ( $1 <> 0 & ex m1 being Integer st p = m1 / $1 );
 ex m being Integer ex k being Element of NAT st
( k <> 0 & p = m / k ) by Th8;
then A1: ex l being Nat st S1[l] ;
 ex k1 being Nat st
( S1[k1] & ( for l1 being Nat st S1[l1] holds
k1 <= l1 ) ) from NAT_1:sch_5(A1);
then consider k1 being Nat such that
A2: k1 <> 0 and
A3: ex m1 being Integer st p = m1 / k1 and
A4: for l1 being Nat st l1 <> 0 & ex n1 being Integer st p = n1 / l1 holds
k1 <= l1 ;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def_12;
consider m1 being Integer such that
A5: p = m1 / k1 and
A6: for l1 being Nat st l1 <> 0 & ex n1 being Integer st p = n1 / l1 holds
k1 <= l1 by A3, A4;
take  m1 ; ::_thesis: ex k being Element of NAT st
( k <> 0 & p = m1 / k & ( for n being Integer
for l being Element of NAT st l <> 0 & p = n / l holds
k <= l ) )
take  k1 ; ::_thesis: ( k1 <> 0 & p = m1 / k1 & ( for n being Integer
for l being Element of NAT st l <> 0 & p = n / l holds
k1 <= l ) )
thus  k1 <> 0 by A2; ::_thesis: ( p = m1 / k1 & ( for n being Integer
for l being Element of NAT st l <> 0 & p = n / l holds
k1 <= l ) )
thus  m1 / k1 = p by A5; ::_thesis: for n being Integer
for l being Element of NAT st l <> 0 & p = n / l holds
k1 <= l
thus  for n being Integer
for l being Element of NAT st l <> 0 & p = n / l holds
k1 <= l by A6; ::_thesis: verum
end;

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

:: deftheorem Def3 defines denominator RAT_1:def_3_:_
 for p being Rational
for b2 being Element of NAT holds
( b2 = denominator p iff ( b2 <> 0 & ex m being Integer st p = m / b2 & ( for n being Integer
for k being Element of NAT st k <> 0 & p = n / k holds
b2 <= k ) ) );

definition
let p be Rational;
func numerator p ->  Integer equals :: RAT_1:def 4
(denominator p) * p;
coherence
 (denominator p) * p is Integer
proof
A1: denominator p <> 0 by Def3;
 ex m being Integer st p = m / (denominator p) by Def3;
hence  (denominator p) * p is Integer by A1, XCMPLX_1:87; ::_thesis: verum
end;
end;

:: deftheorem  defines numerator RAT_1:def_4_:_
 for p being Rational holds numerator p = (denominator p) * p;

theorem Th10: :: RAT_1:10
for p being Rational holds 0 < denominator p
proof
let p be Rational; ::_thesis: 0 < denominator p
 0 <> denominator p by Def3;
hence  0 < denominator p ; ::_thesis: verum
end;

theorem Th11: :: RAT_1:11
for p being Rational holds 1 <= denominator p
proof
let p be Rational; ::_thesis: 1 <= denominator p
 0 < denominator p by Th10;
then  0 + 1 <= denominator p by NAT_1:13;
hence  1 <= denominator p ; ::_thesis: verum
end;

theorem Th12: :: RAT_1:12
for p being Rational holds 0 < (denominator p) "
proof
let p be Rational; ::_thesis: 0 < (denominator p) "
 0 < denominator p by Th10;
hence  0 < (denominator p) " ; ::_thesis: verum
end;

theorem Th13: :: RAT_1:13
for p being Rational holds 1 >= (denominator p) "
proof
let p be Rational; ::_thesis: 1 >= (denominator p) "
A1: 1 * ((denominator p) ") <= (denominator p) * ((denominator p) ") by Th11, XREAL_1:64;
 0 <> denominator p by Def3;
hence  1 >= (denominator p) " by A1, XCMPLX_0:def_7; ::_thesis: verum
end;

theorem Th14: :: RAT_1:14
for p being Rational holds
( numerator p = 0 iff p = 0 )
proof
let p be Rational; ::_thesis: ( numerator p = 0 iff p = 0 )
 denominator p <> 0 by Def3;
hence  ( numerator p = 0 iff p = 0 ) by XCMPLX_1:6; ::_thesis: verum
end;

theorem Th15: :: RAT_1:15
for p being Rational holds
( p = (numerator p) / (denominator p) & p = (numerator p) * ((denominator p) ") & p = ((denominator p) ") * (numerator p) )
proof
let p be Rational; ::_thesis: ( p = (numerator p) / (denominator p) & p = (numerator p) * ((denominator p) ") & p = ((denominator p) ") * (numerator p) )
set x = denominator p;
A1: denominator p <> 0 by Def3;
thus A2: (numerator p) / (denominator p) = p * ((denominator p) * ((denominator p) "))
.= p * 1 by A1, XCMPLX_0:def_7
.= p ; ::_thesis: ( p = (numerator p) * ((denominator p) ") & p = ((denominator p) ") * (numerator p) )
hence  p = (numerator p) * ((denominator p) ") ; ::_thesis: p = ((denominator p) ") * (numerator p)
thus  p = ((denominator p) ") * (numerator p) by A2; ::_thesis: verum
end;

theorem :: RAT_1:16
for p being Rational st p <> 0 holds
denominator p = (numerator p) / p
proof
let p be Rational; ::_thesis: ( p <> 0 implies denominator p = (numerator p) / p )
A1: ((p ") * p) * (denominator p) = (p ") * (numerator p) ;
assume  p <> 0 ; ::_thesis: denominator p = (numerator p) / p
then  1 * (denominator p) = (p ") * (numerator p) by A1, XCMPLX_0:def_7;
hence  denominator p = (numerator p) / p ; ::_thesis: verum
end;

theorem Th17: :: RAT_1:17
for p being Rational st p is Integer holds
( denominator p = 1 & numerator p = p )
proof
let p be Rational; ::_thesis: ( p is Integer implies ( denominator p = 1 & numerator p = p ) )
assume  p is Integer ; ::_thesis: ( denominator p = 1 & numerator p = p )
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; ::_thesis: numerator p = p
hence  numerator p = p ; ::_thesis: verum
end;

theorem Th18: :: RAT_1:18
for p being Rational st ( numerator p = p or denominator p = 1 ) holds
p is Integer
proof
let p be Rational; ::_thesis: ( ( numerator p = p or denominator p = 1 ) implies p is Integer )
assume A1: ( numerator p = p or denominator p = 1 ) ; ::_thesis: p is Integer
percases ( numerator p = p or denominator p = 1 ) by A1;
suppose numerator p = p ; ::_thesis: p is Integer
hence  p is Integer ; ::_thesis: verum
end;
suppose denominator p = 1 ; ::_thesis: p is Integer
then  numerator p = p ;
hence  p is Integer ; ::_thesis: verum
end;
end;
end;

theorem :: RAT_1:19
for p being Rational holds
( numerator p = p iff denominator p = 1 ) by Th17;

theorem :: RAT_1:20
for p being Rational st ( numerator p = p or denominator p = 1 ) & 0 <= p holds
p is Element of NAT
proof
let p be Rational; ::_thesis: ( ( numerator p = p or denominator p = 1 ) & 0 <= p implies p is Element of NAT )
assume that
A1: ( numerator p = p or denominator p = 1 ) and
A2: 0 <= p ; ::_thesis: p is Element of NAT
 p is Integer by A1, Th18;
hence  p is Element of NAT by A2, INT_1:3; ::_thesis: verum
end;

theorem :: RAT_1:21
for p being Rational holds
( 1 < denominator p iff not p is integer )
proof
let p be Rational; ::_thesis: ( 1 < denominator p iff not p is integer )
now__::_thesis:_(_p_is_not_Integer_implies_denominator_p_>_1_)
assume A1: p is not Integer ; ::_thesis: denominator p > 1
 denominator p >= 1 by Th11;
hence  denominator p > 1 by A1, Th18, XXREAL_0:1; ::_thesis: verum
end;
hence  ( 1 < denominator p iff not p is integer ) by Th17; ::_thesis: verum
end;

Lm7:  1 " = 1
;

theorem :: RAT_1:22
for p being Rational holds
( 1 > (denominator p) " iff not p is integer )
proof
let p be Rational; ::_thesis: ( 1 > (denominator p) " iff not p is integer )
A1: (denominator p) " <= 1 by Th13;
now__::_thesis:_(_p_is_not_Integer_implies_(denominator_p)_"_<_1_)
assume  p is not Integer ; ::_thesis: (denominator p) " < 1
then  (denominator p) " <> 1 by Lm7, Th18;
hence  (denominator p) " < 1 by A1, XXREAL_0:1; ::_thesis: verum
end;
hence  ( 1 > (denominator p) " iff not p is integer ) by Lm7, Th17; ::_thesis: verum
end;

theorem Th23: :: RAT_1:23
for p being Rational holds
( numerator p = denominator p iff p = 1 )
proof
let p be Rational; ::_thesis: ( numerator p = denominator p iff p = 1 )
A1: denominator p <> 0 by Def3;
now__::_thesis:_(_numerator_p_=_denominator_p_implies_p_=_1_)
assume  numerator p = denominator p ; ::_thesis: p = 1
then  (numerator p) / (denominator p) = 1 by A1, XCMPLX_1:60;
hence  p = 1 by Th15; ::_thesis: verum
end;
hence  ( numerator p = denominator p iff p = 1 ) ; ::_thesis: verum
end;

theorem Th24: :: RAT_1:24
for p being Rational holds
( numerator p = - (denominator p) iff p = - 1 )
proof
let p be Rational; ::_thesis: ( numerator p = - (denominator p) iff p = - 1 )
A1: 0 <> denominator p by Def3;
now__::_thesis:_(_numerator_p_=_-_(denominator_p)_implies_p_=_-_1_)
assume  numerator p = - (denominator p) ; ::_thesis: p = - 1
hence p = (- (denominator p)) / (denominator p) by Th15
.= - ((denominator p) / (denominator p))
.= - 1 by A1, XCMPLX_1:60 ;
::_thesis: verum
end;
hence  ( numerator p = - (denominator p) iff p = - 1 ) ; ::_thesis: verum
end;

theorem :: RAT_1:25
for p being Rational holds
( - (numerator p) = denominator p iff p = - 1 )
proof
let p be Rational; ::_thesis: ( - (numerator p) = denominator p iff p = - 1 )
 ( - (numerator p) = denominator p iff numerator p = - (denominator p) ) ;
hence  ( - (numerator p) = denominator p iff p = - 1 ) by Th24; ::_thesis: verum
end;

theorem Th26: :: RAT_1:26
for m being Integer
for p being Rational st m <> 0 holds
p = ((numerator p) * m) / ((denominator p) * m)
proof
let m be Integer; ::_thesis: for p being Rational st m <> 0 holds
p = ((numerator p) * m) / ((denominator p) * m)
let p be Rational; ::_thesis: ( m <> 0 implies p = ((numerator p) * m) / ((denominator p) * m) )
assume  m <> 0 ; ::_thesis: p = ((numerator p) * m) / ((denominator p) * m)
then  (numerator p) / (denominator p) = ((numerator p) * m) / ((denominator p) * m) by XCMPLX_1:91;
hence  p = ((numerator p) * m) / ((denominator p) * m) by Th15; ::_thesis: verum
end;

theorem Th27: :: RAT_1:27
for k being Element of NAT
for m being Integer
for p being Rational st k <> 0 & p = m / k holds
ex l being Element of NAT st
( m = (numerator p) * l & k = (denominator p) * l )
proof
let k be Element of NAT ; ::_thesis: for m being Integer
for p being Rational st k <> 0 & p = m / k holds
ex l being Element of NAT st
( m = (numerator p) * l & k = (denominator p) * l )
let m be Integer; ::_thesis: for p being Rational st k <> 0 & p = m / k holds
ex l being Element of NAT st
( m = (numerator p) * l & k = (denominator p) * l )
let p be Rational; ::_thesis: ( k <> 0 & p = m / k implies ex l being Element of NAT st
( m = (numerator p) * l & k = (denominator p) * l ) )
assume that
A1: k <> 0 and
A2: p = m / k ; ::_thesis: ex l being Element of NAT st
( m = (numerator p) * l & k = (denominator p) * l )
A3: p * k = m by A1, A2, XCMPLX_1:87;
defpred S1[ Nat] means $1 * (denominator p) <= k;
A4: denominator p <> 0 by Def3;
A5: for l being Nat st S1[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; ::_thesis: ( S1[l] implies l <= k )
assume A7: l * (denominator p) <= k ; ::_thesis: l <= k
assume  not l <= k ; ::_thesis: contradiction
then  k * (denominator p) < l * (denominator p) by A4, XREAL_1:68;
hence  contradiction by A7, A6, XXREAL_0:2; ::_thesis: verum
end;
A8: 1 * (denominator p) <= k by A1, A2, Def3;
then A9: ex l1 being Nat st S1[l1] ;
consider l being Nat such that
A10: S1[l] and
A11: for l1 being Nat st S1[l1] holds
l1 <= l from NAT_1:sch_6(A5, A9);
reconsider l = l as Element of NAT by ORDINAL1:def_12;
take  l ; ::_thesis: ( m = (numerator p) * l & k = (denominator p) * l )
A12: 0 <> l by A8, A11;
then A13: l * (denominator p) <> 0 by A4, XCMPLX_1:6;
A14: now__::_thesis:_not_l_*_(denominator_p)_<_k
assume A15: l * (denominator p) < k ; ::_thesis: contradiction
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; ::_thesis: verum
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 ;
::_thesis: k = (denominator p) * l
thus  k = (denominator p) * l by A10, A14, XXREAL_0:1; ::_thesis: verum
end;

theorem :: RAT_1:28
for m, n being Integer
for p being Rational st p = m / n & n <> 0 holds
ex m1 being Integer st
( m = (numerator p) * m1 & n = (denominator p) * m1 )
proof
let m, n be Integer; ::_thesis: for p being Rational st p = m / n & n <> 0 holds
ex m1 being Integer st
( m = (numerator p) * m1 & n = (denominator p) * m1 )
let p be Rational; ::_thesis: ( p = m / n & n <> 0 implies ex m1 being Integer st
( m = (numerator p) * m1 & n = (denominator p) * m1 ) )
assume that
A1: p = m / n and
A2: n <> 0 ; ::_thesis: ex m1 being Integer st
( m = (numerator p) * m1 & n = (denominator p) * m1 )
percases ( n < 0 or 0 < n ) by A2;
suppose n < 0 ; ::_thesis: ex m1 being Integer st
( m = (numerator p) * m1 & n = (denominator p) * m1 )
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 being Element of NAT  such that
A4: - m = (numerator p) * k and
A5: x = (denominator p) * k by A3, Th27;
take y = - k; ::_thesis: ( m = (numerator p) * y & n = (denominator p) * y )
thus m = - ((numerator p) * k) by A4
.= (numerator p) * y ; ::_thesis: n = (denominator p) * y
thus n = - ((denominator p) * k) by A5
.= (denominator p) * y ; ::_thesis: verum
end;
suppose 0 < n ; ::_thesis: ex m1 being Integer st
( m = (numerator p) * m1 & n = (denominator p) * m1 )
then reconsider x = n as Element of NAT by INT_1:3;
consider k being Element of NAT  such that
A6: m = (numerator p) * k and
A7: x = (denominator p) * k by A1, A2, Th27;
reconsider y = k as Integer ;
take  y ; ::_thesis: ( m = (numerator p) * y & n = (denominator p) * y )
thus  ( m = (numerator p) * y & n = (denominator p) * y ) by A6, A7; ::_thesis: verum
end;
end;
end;

theorem Th29: :: RAT_1:29
for p being Rational
for l being Element of NAT holds
( not 1 < l or for m being Integer
for k being Element of NAT holds
( not numerator p = m * l or not denominator p = k * l ) )
proof
let p be Rational; ::_thesis: for l being Element of NAT holds
( not 1 < l or for m being Integer
for k being Element of NAT holds
( not numerator p = m * l or not denominator p = k * l ) )
assume  ex l being Element of NAT st
( 1 < l & ex m being Integer ex k being Element of NAT st
( numerator p = m * l & denominator p = k * l ) ) ; ::_thesis: contradiction
then consider l being Element of NAT  such that
A1: 1 < l and
A2: ex m being Integer ex k being Element of NAT st
( numerator p = m * l & denominator p = k * l ) ;
consider m being Integer, k being Element of NAT  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; ::_thesis: verum
end;

theorem Th30: :: RAT_1:30
for k being Element of NAT
for m being Integer
for p being Rational st p = m / k & k <> 0 & ( for l being Element of NAT holds
( not 1 < l or for m1 being Integer
for k1 being Element of NAT holds
( not m = m1 * l or not k = k1 * l ) ) ) holds
( k = denominator p & m = numerator p )
proof
let k be Element of NAT ; ::_thesis: for m being Integer
for p being Rational st p = m / k & k <> 0 & ( for l being Element of NAT holds
( not 1 < l or for m1 being Integer
for k1 being Element of NAT holds
( not m = m1 * l or not k = k1 * l ) ) ) holds
( k = denominator p & m = numerator p )
let m be Integer; ::_thesis: for p being Rational st p = m / k & k <> 0 & ( for l being Element of NAT holds
( not 1 < l or for m1 being Integer
for k1 being Element of NAT holds
( not m = m1 * l or not k = k1 * l ) ) ) holds
( k = denominator p & m = numerator p )
let p be Rational; ::_thesis: ( p = m / k & k <> 0 & ( for l being Element of NAT holds
( not 1 < l or for m1 being Integer
for k1 being Element of NAT holds
( not m = m1 * l or not k = k1 * l ) ) ) implies ( k = denominator p & m = numerator p ) )
assume that
A1: p = m / k and
A2: k <> 0 and
A3: for l being Element of NAT holds
( not 1 < l or for m1 being Integer
for k1 being Element of NAT holds
( not m = m1 * l or not k = k1 * l ) ) ; ::_thesis: ( k = denominator p & m = numerator p )
consider l being Element of NAT  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; ::_thesis: m = numerator p
thus  m = numerator p by A4, A7; ::_thesis: verum
end;

theorem Th31: :: RAT_1:31
for p being Rational holds
( p < - 1 iff numerator p < - (denominator p) )
proof
let p be Rational; ::_thesis: ( p < - 1 iff numerator p < - (denominator p) )
A1: 0 <> denominator p by Def3;
A2: 0 < (denominator p) " by Th12;
A3: now__::_thesis:_(_numerator_p_<_-_(denominator_p)_implies_p_<_-_1_)
assume  numerator p < - (denominator p) ; ::_thesis: p < - 1
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; ::_thesis: verum
end;
A4: 0 < denominator p by Th10;
now__::_thesis:_(_p_<_-_1_implies_numerator_p_<_-_(denominator_p)_)
assume  p < - 1 ; ::_thesis: numerator p < - (denominator p)
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; ::_thesis: verum
end;
hence  ( p < - 1 iff numerator p < - (denominator p) ) by A3; ::_thesis: verum
end;

theorem Th32: :: RAT_1:32
for p being Rational holds
( p <= - 1 iff numerator p <= - (denominator p) )
proof
let p be Rational; ::_thesis: ( p <= - 1 iff numerator p <= - (denominator p) )
A1: now__::_thesis:_(_p_<=_-_1_implies_numerator_p_<=_-_(denominator_p)_)
assume A2: p <= - 1 ; ::_thesis: numerator p <= - (denominator p)
percases ( p = - 1 or p < - 1 ) by A2, XXREAL_0:1;
suppose p = - 1 ; ::_thesis: numerator p <= - (denominator p)
hence  numerator p <= - (denominator p) ; ::_thesis: verum
end;
suppose p < - 1 ; ::_thesis: numerator p <= - (denominator p)
hence  numerator p <= - (denominator p) by Th31; ::_thesis: verum
end;
end;
end;
now__::_thesis:_(_numerator_p_<=_-_(denominator_p)_implies_p_<=_-_1_)
assume A3: numerator p <= - (denominator p) ; ::_thesis: p <= - 1
percases ( numerator p = - (denominator p) or numerator p < - (denominator p) ) by A3, XXREAL_0:1;
suppose numerator p = - (denominator p) ; ::_thesis: p <= - 1
hence  p <= - 1 by Th24; ::_thesis: verum
end;
suppose numerator p < - (denominator p) ; ::_thesis: p <= - 1
hence  p <= - 1 by Th31; ::_thesis: verum
end;
end;
end;
hence  ( p <= - 1 iff numerator p <= - (denominator p) ) by A1; ::_thesis: verum
end;

theorem :: RAT_1:33
for p being Rational holds
( p < - 1 iff denominator p < - (numerator p) )
proof
let p be Rational; ::_thesis: ( p < - 1 iff denominator p < - (numerator p) )
 ( denominator p < - (numerator p) iff - (- (numerator p)) < - (denominator p) ) by XREAL_1:24;
hence  ( p < - 1 iff denominator p < - (numerator p) ) by Th31; ::_thesis: verum
end;

theorem :: RAT_1:34
for p being Rational holds
( p <= - 1 iff denominator p <= - (numerator p) )
proof
let p be Rational; ::_thesis: ( p <= - 1 iff denominator p <= - (numerator p) )
 ( denominator p <= - (numerator p) iff - (- (numerator p)) <= - (denominator p) ) by XREAL_1:24;
hence  ( p <= - 1 iff denominator p <= - (numerator p) ) by Th32; ::_thesis: verum
end;

theorem Th35: :: RAT_1:35
for p being Rational holds
( p < 1 iff numerator p < denominator p )
proof
let p be Rational; ::_thesis: ( p < 1 iff numerator p < denominator p )
A1: 0 <> denominator p by Def3;
A2: 0 < (denominator p) " by Th12;
A3: now__::_thesis:_(_numerator_p_<_denominator_p_implies_p_<_1_)
assume  numerator p < denominator p ; ::_thesis: p < 1
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; ::_thesis: verum
end;
A4: 0 < denominator p by Th10;
now__::_thesis:_(_p_<_1_implies_numerator_p_<_denominator_p_)
assume  p < 1 ; ::_thesis: numerator p < denominator p
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; ::_thesis: verum
end;
hence  ( p < 1 iff numerator p < denominator p ) by A3; ::_thesis: verum
end;

theorem :: RAT_1:36
for p being Rational holds
( p <= 1 iff numerator p <= denominator p )
proof
let p be Rational; ::_thesis: ( p <= 1 iff numerator p <= denominator p )
A1: now__::_thesis:_(_p_<=_1_implies_numerator_p_<=_denominator_p_)
assume A2: p <= 1 ; ::_thesis: numerator p <= denominator p
percases ( p = 1 or p < 1 ) by A2, XXREAL_0:1;
suppose p = 1 ; ::_thesis: numerator p <= denominator p
hence  numerator p <= denominator p ; ::_thesis: verum
end;
suppose p < 1 ; ::_thesis: numerator p <= denominator p
hence  numerator p <= denominator p by Th35; ::_thesis: verum
end;
end;
end;
now__::_thesis:_(_numerator_p_<=_denominator_p_implies_p_<=_1_)
assume A3: numerator p <= denominator p ; ::_thesis: p <= 1
percases ( numerator p = denominator p or numerator p < denominator p ) by A3, XXREAL_0:1;
suppose numerator p = denominator p ; ::_thesis: p <= 1
hence  p <= 1 by Th23; ::_thesis: verum
end;
suppose numerator p < denominator p ; ::_thesis: p <= 1
hence  p <= 1 by Th35; ::_thesis: verum
end;
end;
end;
hence  ( p <= 1 iff numerator p <= denominator p ) by A1; ::_thesis: verum
end;

theorem :: RAT_1:37
for p being Rational holds
( p < 0 iff numerator p < 0 )
proof
let p be Rational; ::_thesis: ( p < 0 iff numerator p < 0 )
now__::_thesis:_(_p_<_0_implies_numerator_p_<_0_)
assume  p < 0 ; ::_thesis: numerator p < 0
then  (numerator p) / (denominator p) < 0 by Th15;
hence  numerator p < 0 ; ::_thesis: verum
end;
hence  ( p < 0 iff numerator p < 0 ) ; ::_thesis: verum
end;

theorem Th38: :: RAT_1:38
for p being Rational holds
( p <= 0 iff numerator p <= 0 )
proof
let p be Rational; ::_thesis: ( p <= 0 iff numerator p <= 0 )
now__::_thesis:_(_numerator_p_<=_0_implies_p_<=_0_)
assume A1: numerator p <= 0 ; ::_thesis: p <= 0
percases ( numerator p = 0 or numerator p < 0 ) by A1;
suppose numerator p = 0 ; ::_thesis: p <= 0
hence  p <= 0 by Th14; ::_thesis: verum
end;
suppose numerator p < 0 ; ::_thesis: p <= 0
hence  p <= 0 ; ::_thesis: verum
end;
end;
end;
hence  ( p <= 0 iff numerator p <= 0 ) ; ::_thesis: verum
end;

theorem Th39: :: RAT_1:39
for a being real number
for p being Rational holds
( a < p iff a * (denominator p) < numerator p )
proof
let a be real number ; ::_thesis: for p being Rational holds
( a < p iff a * (denominator p) < numerator p )
let p be Rational; ::_thesis: ( a < p iff a * (denominator p) < numerator p )
A1: 0 < (denominator p) " by Th12;
A2: 0 <> denominator p by Def3;
A3: now__::_thesis:_(_a_*_(denominator_p)_<_numerator_p_implies_a_<_p_)
assume  a * (denominator p) < numerator p ; ::_thesis: a < 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; ::_thesis: verum
end;
 0 < denominator p by Th10;
hence  ( a < p iff a * (denominator p) < numerator p ) by A3, XREAL_1:68; ::_thesis: verum
end;

theorem :: RAT_1:40
for a being real number
for p being Rational holds
( a <= p iff a * (denominator p) <= numerator p )
proof
let a be real number ; ::_thesis: for p being Rational holds
( a <= p iff a * (denominator p) <= numerator p )
let p be Rational; ::_thesis: ( a <= p iff a * (denominator p) <= numerator p )
A1: denominator p <> 0 by Def3;
A2: now__::_thesis:_(_a_*_(denominator_p)_<=_numerator_p_implies_a_<=_p_)
assume A3: a * (denominator p) <= numerator p ; ::_thesis: a <= p
percases ( a * (denominator p) = numerator p or a * (denominator p) < numerator p ) by A3, XXREAL_0:1;
suppose a * (denominator p) = numerator p ; ::_thesis: a <= 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 ; ::_thesis: verum
end;
suppose a * (denominator p) < numerator p ; ::_thesis: a <= p
hence  a <= p by Th39; ::_thesis: verum
end;
end;
end;
now__::_thesis:_(_a_<=_p_implies_numerator_p_>=_a_*_(denominator_p)_)
assume A4: a <= p ; ::_thesis: numerator p >= a * (denominator p)
percases ( a = p or a < p ) by A4, XXREAL_0:1;
suppose a = p ; ::_thesis: numerator p >= a * (denominator p)
hence  numerator p >= a * (denominator p) ; ::_thesis: verum
end;
suppose a < p ; ::_thesis: a * (denominator p) <= numerator p
hence  a * (denominator p) <= numerator p by Th39; ::_thesis: verum
end;
end;
end;
hence  ( a <= p iff a * (denominator p) <= numerator p ) by A2; ::_thesis: verum
end;

theorem :: RAT_1:41
for p, q being Rational st denominator p = denominator q & numerator p = numerator q holds
p = q
proof
let p, q be Rational; ::_thesis: ( denominator p = denominator q & numerator p = numerator q implies p = q )
assume that
A1: denominator p = denominator q and
A2: numerator p = numerator q ; ::_thesis: p = q
thus p = (numerator q) / (denominator q) by A1, A2, Th15
.= q by Th15 ; ::_thesis: verum
end;

theorem :: RAT_1:42
for p, q being Rational holds
( p < q iff (numerator p) * (denominator q) < (numerator q) * (denominator p) )
proof
let p, q be Rational; ::_thesis: ( p < q iff (numerator p) * (denominator q) < (numerator q) * (denominator p) )
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  ( p < q iff (numerator p) * (denominator q) < (numerator q) * (denominator p) ) by A1, A2, XREAL_1:102, XREAL_1:106; ::_thesis: verum
end;

theorem Th43: :: RAT_1:43
for p being Rational holds
( denominator (- p) = denominator p & numerator (- p) = - (numerator p) )
proof
let p be Rational; ::_thesis: ( denominator (- p) = denominator p & numerator (- p) = - (numerator p) )
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 being Element of NAT  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 being Element of NAT  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; ::_thesis: numerator (- p) = - (numerator p)
thus  numerator (- p) = - (numerator p) by A4, A6; ::_thesis: verum
end;

theorem Th44: :: RAT_1:44
for p, q being Rational holds
( 0 < p & q = 1 / p iff ( numerator q = denominator p & denominator q = numerator p ) )
proof
let p, q be Rational; ::_thesis: ( 0 < p & q = 1 / p iff ( numerator q = denominator p & denominator q = numerator p ) )
A1: now__::_thesis:_(_0_<_p_&_q_=_1_/_p_implies_(_numerator_p_=_denominator_q_&_denominator_p_=_numerator_q_)_)
set x = denominator p;
assume that
A2: 0 < p and
A3: q = 1 / p ; ::_thesis: ( numerator p = denominator q & denominator p = numerator q )
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: for k being Element of NAT holds
( not 1 < k or for m being Integer
for l being Element of NAT holds
( not denominator p = m * k or not y = l * k ) )
proof
assume  ex k being Element of NAT st
( 1 < k & ex m being Integer ex l being Element of NAT st
( denominator p = m * k & y = l * k ) ) ; ::_thesis: contradiction
then consider k being Element of NAT  such that
A6: 1 < k and
A7: ex m being Integer ex l being Element of NAT st
( denominator p = m * k & y = l * k ) ;
consider m being Integer, l being Element of NAT  such that
A8: denominator p = m * k and
A9: y = l * k by A7;
now__::_thesis:_0_<=_m
assume  not 0 <= m ; ::_thesis: contradiction
then  m * k < 0 * m by A6, XREAL_1:69;
hence  contradiction by A8; ::_thesis: verum
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; ::_thesis: verum
end;
 0 <> numerator p by A2, Th38;
hence  ( numerator p = denominator q & denominator p = numerator q ) by A4, A5, Th30; ::_thesis: verum
end;
now__::_thesis:_(_numerator_q_=_denominator_p_&_denominator_q_=_numerator_p_implies_(_0_<_p_&_q_=_1_/_p_)_)
assume that
A10: numerator q = denominator p and
A11: denominator q = numerator p ; ::_thesis: ( 0 < p & q = 1 / p )
thus  0 < p by A11, Th10; ::_thesis: q = 1 / p
thus q = (1 * (denominator p)) / (numerator p) by A10, A11, Th15
.= 1 / ((numerator p) / (denominator p)) by XCMPLX_1:77
.= 1 / p by Th15 ; ::_thesis: verum
end;
hence  ( 0 < p & q = 1 / p iff ( numerator q = denominator p & denominator q = numerator p ) ) by A1; ::_thesis: verum
end;

theorem :: RAT_1:45
for p, q being Rational holds
( p < 0 & q = 1 / p iff ( numerator q = - (denominator p) & denominator q = - (numerator p) ) )
proof
let p, q be Rational; ::_thesis: ( p < 0 & q = 1 / p iff ( numerator q = - (denominator p) & denominator q = - (numerator p) ) )
A1: now__::_thesis:_(_p_<_0_&_q_=_1_/_p_implies_(_numerator_q_=_-_(denominator_p)_&_denominator_q_=_-_(numerator_p)_)_)
set s = - q;
set r = - p;
assume that
A2: p < 0 and
A3: q = 1 / p ; ::_thesis: ( numerator q = - (denominator p) & denominator q = - (numerator p) )
A4: - q = 1 / (- p) by A3, XCMPLX_1:188;
A5: 0 < - p by A2, XREAL_1:58;
then  numerator (- q) = denominator (- p) by A4, Th44;
then  - (numerator q) = denominator (- p) by Th43;
then A6: - (- (numerator q)) = - (denominator p) by Th43;
 denominator (- q) = numerator (- p) by A5, A4, Th44;
then  denominator q = numerator (- p) by Th43;
hence  ( numerator q = - (denominator p) & denominator q = - (numerator p) ) by A6, Th43; ::_thesis: verum
end;
now__::_thesis:_(_numerator_q_=_-_(denominator_p)_&_denominator_q_=_-_(numerator_p)_implies_(_p_<_0_&_q_=_1_/_p_)_)
assume that
A7: numerator q = - (denominator p) and
A8: denominator q = - (numerator p) ; ::_thesis: ( p < 0 & q = 1 / p )
thus  p < 0 by A8, Th10; ::_thesis: q = 1 / p
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 ; ::_thesis: verum
end;
hence  ( p < 0 & q = 1 / p iff ( numerator q = - (denominator p) & denominator q = - (numerator p) ) ) by A1; ::_thesis: verum
end;