:: Basic Properties of Rational Numbers
:: by Andrzej Kondracki
::
:: Received July 10, 1990
:: Copyright (c) 1990-2018 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;
definitions XREAL_0, TARSKI, XBOOLE_0;
equalities XBOOLE_0, XCMPLX_0, ARYTM_3;
expansions TARSKI;
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 object,
a,b for Real,
k,k1,i1,j1,w for 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).
Lm1: omega c= ({[c,d] where c,d is Element of omega: c,d are_coprime &
d <> {}} \ the set of all [k,1] where k is Element of omega) \/ 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;
+(In(0,REAL),opp In(0,REAL)) = 0 by ARYTM_0:def 3;
then
A3: opp In(0,REAL) = 0 by ARYTM_0:11;
reconsider y = 1 as Element of REAL by NUMBERS:19;
j1 * j1" = 1 by A2,XCMPLX_0:def 7;
then consider x1,x2,y1,y2 being Element of REAL such that
A4: j1 = [*x1,x2*] and
A5: j1" = [*y1,y2*] and
A6: y = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *] by XCMPLX_0:def 5;
A7: j1 in REAL by XREAL_0:def 1;
+(*(x1,y2),*(x2,y1)) = 0 by A6,ARYTM_0:24;
then
A8: 1 = +(*(x1,y1),opp*(x2,y2)) by A6,ARYTM_0:def 5
.= +(*(x1,y1),opp In(0,REAL)) by A4,ARYTM_0:12,24,A7
.= *(x1,y1) by A3,ARYTM_0:11;
j1 in REAL by XREAL_0:def 1;
then x2 = 0 by A4,ARYTM_0:24;
then
A9: j1 = x1 by A4,ARYTM_0:def 5;
then x1 in omega by ORDINAL1:def 12;
then reconsider xx = x1 as Element of RAT+ by Lm1;
consider yy being Element of RAT+ such that
A10: xx *' yy = one by A2,A9,ARYTM_3:54;
reconsider xx1 = xx, yy1 = yy as Element of REAL+ by ARYTM_2:1;
A11: ex x9,y9 being Element of RAT+ st xx1 = x9 & yy1 = y9 & xx1 *' yy1 =
x9 *' y9 by ARYTM_2:21;
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,A9,A8,A10,A11,ARYTM_0:18;
then
A13: y1 in RAT+;
j1" in REAL by XREAL_0:def 1;
then y2 = 0 by A5,ARYTM_0:24;
then
A14: j1" = y1 by A5,ARYTM_0:def 5;
A15: j1 in omega by ORDINAL1:def 12;
then reconsider a = x, b = j1 as Element of RAT+ by Lm1;
consider x91,x92,y91,y92 being Element of 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;
i1*j1" in REAL by XREAL_0:def 1;
then
A19: +(*(x91,y92),*(x92,y91)) = 0 by A18,ARYTM_0:24;
x1 in omega by A9,ORDINAL1:def 12;
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 A9,A12,A15,A20,A21,Lm1,ARYTM_2:21;
j1" in REAL by XREAL_0:def 1;
then
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,In(0,REAL)))
by A14,A18,A24,A19,ARYTM_0:def 5
.= +(*(x91,y1),In(0,REAL)) by A3,ARYTM_0:12
.= *(x91,y1) by ARYTM_0:11;
i1 in REAL by XREAL_0:def 1;
then x92 = 0 by A16,ARYTM_0:24;
then
A26: i1 = x91 by A16,ARYTM_0:def 5;
then
A27: x91 in omega by ORDINAL1:def 12;
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 A9,A8,A29,A32,A20,A21,A22,A23,ARYTM_3:52;
hence thesis by A2,A33,ARYTM_3:56;
end;
end;
Lm3: for 09 be Element of REAL+ st 09 = 0
for x9 being Element of REAL+ st x9 = a holds 09 - x9 = -a
proof
let 09 be Element of REAL+ such that A0:09 = 0;
let xx being Element of REAL+ such that
A1: xx = a;
per cases;
suppose
xx = 0;
hence thesis by A0,A1,ARYTM_1:18;
end;
suppose
A2: xx <> 0;
set b = 09 - xx;
A3: 09 <=' xx by A0,ARYTM_1:6;
then not xx <=' 09 by A0,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 A0,A2,A3,ARYTM_1:10;
end;
then
A5: not b in {[0,0]} by TARSKI:def 1;
A6: xx -' 09 = xx -' 09 + 09 by A0,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;
a+b in REAL by XREAL_0:def 1;
then +(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 object 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 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;
reconsider 09 = 0 as Element of REAL+ by ARYTM_2:2;
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/w implies x in RAT
proof
reconsider 09 = 0 as Element of REAL+ by ARYTM_2:2;
A1: m is Element of INT by INT_1:def 2;
assume
A2: x = m/w;
then x in REAL by XREAL_0:def 1;
then
A3: not x in {[0,0]} by NUMBERS:def 1,XBOOLE_0:def 5;
reconsider w as Element of NAT by ORDINAL1:def 12;
per cases;
suppose
w = 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 being Nat st m = k;
then consider k being Nat such that
A4: m = k;
x = quotient(k,w) 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: w <> 0 and
A6: for k being Nat holds m <> k;
consider k being Nat such that
A7: m = -k by A1,A6,INT_1:def 1;
A8: k/w = quotient(k,w) by Lm2;
then k/w in RAT+;
then reconsider x9 = k/w as Element of REAL+ by ARYTM_2:1;
A9: 0 in {0} by TARSKI:def 1;
A10: x = -k/w 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 being Nat 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 be object;
assume x in R;
then ex m,n st x = m/n by A1;
hence thesis by Lm6;
end;
let x be object;
assume x in RAT;
then ex m,n st x = m/n by Lm4;
hence thesis by A1;
end;
end;
definition
let r be object;
attr r is rational means
r in RAT;
end;
registration
cluster rational for Real;
existence
proof
reconsider a = 0, b = 1 as Integer;
take x=a/b;
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 by Th1;
registration
cluster rational -> real for object;
coherence
by NUMBERS:12;
end;
theorem Th3:
m/n is rational by Def1;
registration
cluster integer -> rational for object;
coherence
proof
let x be object;
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 be Rational;
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 be Rational;
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;
::$CT 3
:: RAT is dense, that is there exists at least one rational number between
:: any two distinct real numbers.
theorem
am 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)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
00 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 Th6:
ex m,k st k<>0 & p=m/k & for n,w st w<>0 & p=n/w holds k<=w
proof
defpred P[Nat] means ($1<>0 & ex m1 st p=m1/$1);
ex m,k st k<>0 & p=m/k by Th5;
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 be Rational;
func denominator(p) -> 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,w st w<>0 & p=n/w holds k<=w by Th6;
reconsider k as Element of NAT by ORDINAL1:def 12;
take k;
thus thesis by A1,A2,A3;
end;
uniqueness
proof
let k,l be Nat 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,k1 st k1<>0 & p=n1/k1 holds l<=k1;
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 be Rational;
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 Th7:
0 < denominator(p)
proof
0 <> denominator p by Def3;
hence thesis;
end;
registration
let p;
cluster denominator(p) -> positive;
coherence by Th7;
end;
theorem Th8:
1 <= denominator(p)
proof
0+1<=denominator(p) by NAT_1:13;
hence thesis;
end;
theorem
0 < denominator(p)";
theorem Th10:
1 >= denominator(p)"
proof
1*denominator(p)"<=denominator(p)*denominator(p)" by Th8,XREAL_1:64;
hence thesis by XCMPLX_0:def 7;
end;
theorem Th11:
numerator(p)=0 iff p=0 by XCMPLX_1:6;
theorem Th12:
p=numerator(p)/denominator(p) & p=numerator(p)*denominator(p)"
proof
set x=denominator(p);
thus numerator(p)/denominator(p)=p*(x*x") .=p*1 by XCMPLX_0:def 7
.=p;
hence thesis;
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 Th14:
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 Th8;
hence denominator(p)=1 by A1,XXREAL_0:1;
hence thesis;
end;
theorem Th15:
(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 Th14;
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,Th15;
hence thesis by A2,INT_1:3;
end;
theorem
1=1 by Th8;
hence denominator(p)>1 by A1,Th15,XXREAL_0:1;
end;
hence thesis by Th14;
end;
Lm7: 1"=1;
theorem
1>denominator(p)" iff p is not integer
proof
A1: denominator(p)"<=1 by Th10;
now
assume not p is Integer;
then denominator(p)" <> 1 by Lm7,Th15;
hence denominator(p)"<1 by A1,XXREAL_0:1;
end;
hence thesis by Lm7,Th14;
end;
theorem Th20:
numerator(p)=denominator(p) iff p=1
proof
hereby
assume numerator(p)=denominator(p);
then numerator(p)/denominator(p)=1 by XCMPLX_1:60;
hence p=1 by Th12;
end;
thus thesis;
end;
theorem Th21:
numerator(p)=-denominator(p) iff p=-1
proof
hereby
assume numerator(p)=-denominator(p);
hence p=(-denominator(p))/denominator(p) by Th12
.=-denominator(p)/denominator(p)
.=-1 by XCMPLX_1:60;
end;
thus thesis;
end;
theorem
-numerator(p)=denominator(p) iff p=-1
proof
-numerator(p)=denominator(p) iff numerator(p)=-denominator(p);
hence thesis by Th21;
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 Th23:
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 Th12;
end;
theorem Th24:
k<>0 & p=m/k implies ex w st m=numerator(p)*w & k=denominator(p)*w
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;
A5: for l be Nat st P[l] holds l<=k
proof
0+1<=denominator(p) by 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 by A8,A11;
then
A13: l*denominator(p)<>0 by XCMPLX_1:6;
A14: now
assume
A15: l*denominator(p)x by A15;
m/k=(numerator(p)*l)/(l*denominator(p)) by A2,A12,Th23;
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,Th12
.=(numerator(p)/denominator(p)*denominator(p))*l
.=numerator(p)*l by 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,Th24;
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
00 by A4;
then k*10 & not ex w st 10 and
A3: not ex w st 1=a*denominator(p);
end;
suppose
a

numerator(p) by A2,Th35;
hence numerator(p)=denominator(q) & denominator(p)=numerator(q) by A4,A5
,Th27;
end;
now
assume that
A10: numerator(q)=denominator(p) and
A11: denominator(q)=numerator(p);
thus 0