Copyright (c) 1990 Association of Mizar Users
environ
vocabulary ARYTM, INT_1, ABSVALUE, ARYTM_3, ARYTM_1, RELAT_1, RAT_1, ORDINAL2,
BOOLE, COMPLEX1, OPPCAT_1, ARYTM_2, QUOFIELD, ORDINAL1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ORDINAL2, ARYTM_3,
ARYTM_2, NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, ABSVALUE,
INT_1, ARYTM_1;
constructors NAT_1, XCMPLX_0, XREAL_0, ORDINAL2, INT_1, ABSVALUE, XBOOLE_0,
ARYTM_3, ARYTM_0, FUNCT_4, ARYTM_2, ARYTM_1, REAL_1;
clusters INT_1, XREAL_0, REAL_1, ZFMISC_1, XBOOLE_0, NUMBERS, ARYTM_3,
ORDINAL2, ARYTM_2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions XREAL_0, TARSKI, XBOOLE_0;
theorems AXIOMS, REAL_1, INT_1, NAT_1, ABSVALUE, TARSKI, XREAL_0, XCMPLX_0,
XCMPLX_1, ORDINAL2, XBOOLE_0, NUMBERS, ARYTM_3, ARYTM_0, ARYTM_2,
ZFMISC_1, ARYTM_1;
schemes NAT_1;
begin
Lm0: one = succ 0 by ORDINAL2:def 4 .= 1;
reserve X,x for set,
a,b,c,d for real number,
k,k1,l,l1 for Nat,
m,m1,n,n1 for Integer;
:: Auxiliary theorems & redefinitions.
definition let i be integer number;
cluster abs i -> natural;
coherence
proof 0 <= abs i by ABSVALUE:5;
hence thesis by INT_1:16;
end;
end;
definition let k;
redefine func abs k -> Nat;
coherence by ORDINAL2:def 21;
end;
Lm1:0<b & 0<d implies (a*d<c*b iff a/b<c/d)
proof
assume A1:0<b & 0<d; then A2:0<b" & 0<d" by REAL_1:72;
A3:now assume a*d<c*b;
then (a*d)*d"<(c*b)*d" by A2,REAL_1:70;
then a*(d*d")<(c*b)*d" by XCMPLX_1:4;
then a*1<(c*b)*d" by A1,XCMPLX_0:def 7;
then a<b*(c*d") by XCMPLX_1:4;
then a<b*(c/d) by XCMPLX_0:def 9;
then b"*a<b"*(b*(c/d)) by A2,REAL_1:70;
then b"*a<(b"*b)*(c/d) by XCMPLX_1:4;
then b"*a<1*(c/d) by A1,XCMPLX_0:def 7;
hence a/b<c/d by XCMPLX_0:def 9;
end;
now assume a/b<c/d;
then a/b*b<c/d*b by A1,REAL_1:70;
then a<b*(c/d) by A1,XCMPLX_1:88;
then a*d<(b*(c/d))*d by A1,REAL_1:70;
then a*d<b*(c/d*d) by XCMPLX_1:4;
hence a*d<c*b by A1,XCMPLX_1:88;
end;
hence thesis by A3;
end;
:: We define RAT as a set of real numbers, each of which can be expressed
:: as a quotient of integer dividend and divisor (divisor is not equal
:: to zero).
reserve i,j,i1,j1 for Nat;
Lm_2:
quotient(i1,j1) = i1/j1
proof
set x = quotient(i1,j1);
per cases;
suppose
S: j1 = 0;
hence x = 0 by ARYTM_3:def 9 .= i1/j1 by S,XCMPLX_1:49;
suppose
S2: j1 <> 0;
j1 * j1" = 1 by XCMPLX_0:def 7,S2;
then consider x1,x2,y1,y2 being Real such that
W1: j1 = [*x1,x2*] and
W2: j1" = [*y1,y2*] and
W3: 1 = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *]
by XCMPLX_0:def 5;
X2: x2 = 0 by W1,ARYTM_0:26;
then
X1: j1 = x1 by W1,ARYTM_0:def 7;
y2 = 0 by W2,ARYTM_0:26;
then
Y1: j1" = y1 by W2,ARYTM_0:def 7;
+(0,opp 0) = 0 by ARYTM_0:def 4;
then
OP: opp 0 = 0 by ARYTM_0:13;
+(*(x1,y2),*(x2,y1)) = 0 by W3,ARYTM_0:26;
then
XY1: 1 = +(*(x1,y1),opp*(x2,y2)) by W3,ARYTM_0:def 7
.= +(*(x1,y1),opp 0) by ARYTM_0:14,X2
.= *(x1,y1) by ARYTM_0:13,OP;
consider x'1,x'2,y'1,y'2 being Real such that
W4: i1 = [*x'1,x'2*] and
W5: j1" = [*y'1,y'2*] and
W6: i1*j1" = [* +(*(x'1,y'1),opp*(x'2,y'2)), +(*(x'1,y'2),*(x'2,y'1)) *]
by XCMPLX_0:def 5;
x'2 = 0 by W4,ARYTM_0:26;
then
X'1: i1 = x'1 by W4,ARYTM_0:def 7;
Y'2: y'2 = 0 by W5,ARYTM_0:26;
then
Y'1: j1" = y'1 by W5,ARYTM_0:def 7;
+(*(x'1,y'2),*(x'2,y'1)) = 0 by W6,ARYTM_0:26;
then
XY'1: i1*j1" = +(*(x'1,y1),opp*(x'2,0)) by W6,ARYTM_0:def 7,Y'1,Y1,Y'2
.= +(*(x'1,y1),0) by ARYTM_0:14,OP
.= *(x'1,y1) by ARYTM_0:13;
x'1 in omega by X'1;
then
B: x'1 in RAT+ by ARYTM_3:34;
x1 in omega by X1;
then reconsider xx = x1 as Element of RAT+ by ARYTM_3:34;
consider yy being Element of RAT+ such that
WW: xx *' yy = one by ARYTM_3:60,S2,X1;
xx in RAT+ & yy in RAT+;
then reconsider xx1 = xx, yy1 = yy as Element of REAL+ by ARYTM_2:1;
I: ex x',y' being Element of RAT+
st xx1 = x' & yy1 = y' & xx1 *' yy1 = x' *' y' by ARYTM_2:22;
xx1 in REAL+ & yy1 in REAL+;
then reconsider xx1, yy1 as Element of REAL by ARYTM_0:1;
ex x',y' being Element of REAL+
st xx1 = x' & yy1 = y' & *(xx1,yy1) = x' *' y' by ARYTM_0:def 3;
then yy = y1 by S2,XY1,Lm0,ARYTM_0:20,X1,I,WW;
then
G: y1 in RAT+;
then consider x',y' being Element of REAL+ such that
W7: x'1 = x' and
W8: y1 = y' and
W9: i1 * j1" = x' *' y' by B,ARYTM_0:def 3,XY'1,ARYTM_2:1;
consider x'',y'' being Element of RAT+ such that
W10: x' = x'' and
W11: y' = y'' and
W12: i1 * j1" = x'' *' y'' by B,ARYTM_2:22,W9,W7,W8,G;
HH: j1 in omega;
then reconsider a = x, b = j1 as Element of RAT+ by ARYTM_3:34;
x1 in omega by X1;
then consider x1',y1' being Element of REAL+ such that
W13: x1 = x1' and
W14: y1 = y1' and
W15: *(x1,y1) = x1' *' y1' by ARYTM_0:def 3,G,ARYTM_2:1,2;
ex x1'',y1'' being Element of RAT+
st x1' = x1'' & y1' = y1'' & x1' *' y1' = x1'' *' y1''
by ARYTM_2:22,W13,W14,G,X1,ARYTM_3:34,HH;
then
XX: b *' y'' = 1 by XY1,W15,X1,W14,W13,W11,W8;
a *' b = quotient(i1,j1) *' quotient(j1,one) by ARYTM_3:46
.= quotient(i1*^j1,j1*^one) by ARYTM_3:55
.= quotient(i1,one) *' quotient(j1,j1) by ARYTM_3:55
.= quotient(i1,one) *' one by S2, ARYTM_3:47
.= quotient(i1,one) by ARYTM_3:59
.= i1 by ARYTM_3:46
.= x'' *' one by ARYTM_3:59,W10,W7,X'1
.= x'' *' y'' *' b by ARYTM_3:58,XX,Lm0;
hence x = i1 * j1" by ARYTM_3:62,S2,W12
.= i1/j1 by XCMPLX_0:def 9;
end;
0 in omega;
then reconsider 0' = 0 as Element of REAL+ by ARYTM_2:2;
Lm_3:
for x' being Element of REAL+ st x' = a
holds 0' - x' = -a
proof let xx being Element of REAL+ such that
Z: xx = a;
per cases;
suppose xx = 0;
hence 0' - xx = -a by Z,ARYTM_1:18;
suppose
S: xx <> 0;
set b = 0' - xx;
U: 0' <=' xx by ARYTM_1:6;
not xx <=' 0' by U,S,ARYTM_1:4;
then
X: b = [{},xx -' 0'] by ARYTM_1:def 2;
now assume b = [0,0];
then xx -' 0' = 0 by X,ZFMISC_1:33;
hence contradiction by S,U,ARYTM_1:10;
end;
then
Y: not b in {[0,0]} by TARSKI:def 1;
0 in {0} by TARSKI:def 1;
then
V: b in [:{0},REAL+:] by X,ZFMISC_1:106;
then b in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 2;
then reconsider b as Element of REAL by Y,XBOOLE_0:def 4,NUMBERS:def 1;
consider x1,x2,y1,y2 being Element of REAL such that
W1: a = [*x1,x2*] and
W2: b = [*y1,y2*] and
W3: a+b = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4;
a in REAL by XREAL_0:def 1;
then x2 = 0 by W1,ARYTM_0:26;
then
X1: a = x1 by W1,ARYTM_0:def 7;
y2 = 0 by W2,ARYTM_0:26;
then
Y1: b = y1 by W2,ARYTM_0:def 7;
a+b in REAL by XREAL_0:def 1;
then
+(x2,y2) = 0 by W3,ARYTM_0:26;
then
XY1: a+b = +(x1,y1) by W3,ARYTM_0:def 7;
y1 in [:{0},REAL+:] by Y1,V;
then consider x',y' being Element of REAL+ such that
W4: x1 = x' and
W5: y1 = [0,y'] and
W6: +(x1,y1) = x' - y' by ARYTM_0:def 2,Z,X1;
P: y' = xx -' 0' by W5,Y1,X,ZFMISC_1:33;
Q: xx -' 0' = xx -' 0' + 0' by ARYTM_2:def 8
.= xx by ARYTM_1:def 1,U;
a + b = +(x1,y1) by XY1
.= 0 by ARYTM_1:18,W6,P,W4,X1,Z,Q;
hence 0' - xx = -a by XCMPLX_0:def 6;
end;
Lm_0: x in RAT implies ex m,n st x = m/n
proof assume
Z: x in RAT;
pc: x in RAT+ \/ [:{0},RAT+:] by Z,XBOOLE_0:def 4,NUMBERS:def 3;
per cases by pc,XBOOLE_0:def 2;
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:45;
hence thesis by Lm_2;
suppose x in [:{0},RAT+:];
then consider x1,x2 being set such that
W1: x1 in {0} and
W2: x2 in RAT+ and
W3: x = [x1,x2] by ZFMISC_1:103;
reconsider x2 as Element of RAT+ by W2;
reconsider x' = x2 as Element of REAL+ by W2,ARYTM_2:1;
take m = -numerator x2, n = denominator x2;
A: x2 = quotient(numerator x2,denominator x2) by ARYTM_3:45
.= numerator x2/n by Lm_2;
x1 = 0 by W1,TARSKI:def 1;
then
C: x = [0,x'] by W3;
not x in {[0,0]} by Z,XBOOLE_0:def 4,NUMBERS:def 3;
then x <> [0,0] by TARSKI:def 1;
then
B: x2 <> 0 by C;
thus x = 0' - x' by C,ARYTM_1:19,B
.= -numerator x2/n by Lm_3,A
.= m/n by XCMPLX_1:188;
end;
Lm_1': x = m/l implies x in RAT
proof assume
Z: x = m/l;
then x in REAL by XREAL_0:def 1;
then
A: not x in {[0,0]} by NUMBERS:def 1,XBOOLE_0:def 4;
m is Element of INT by INT_1:def 2;
then
K: ex k st m = k or m = -k by INT_1:def 1;
per cases;
suppose l = 0;
then x = m * 0" by Z,XCMPLX_0:def 9
.= 0;
then x in omega;
then x in RAT+ by ARYTM_3:34;
then x in RAT+ \/ [:{0},RAT+:] by XBOOLE_0:def 2;
hence thesis by A,XBOOLE_0:def 4,NUMBERS:def 3;
suppose ex k st m = k;
then consider k such that
W: m = k;
x = quotient(k,l) by Z,Lm_2,W;
then x in RAT+ \/ [:{0},RAT+:] by XBOOLE_0:def 2;
hence x in RAT by XBOOLE_0:def 4,NUMBERS:def 3,A;
suppose that
S1: l <> 0 and
S2: for k holds m <> k;
consider k such that
W: m = -k by K,S2;
B: x = -k/l by W,Z, XCMPLX_1:188;
k/l = quotient(k,l) by Lm_2;
then
E: k/l in RAT+;
then k/l in REAL+ by ARYTM_2:1;
then reconsider x' = k/l as Element of REAL+;
m <> 0 by S2;
then
C: x' <> 0 by B,Z,XCMPLX_1:50,S1;
D: x = 0' - x' by Lm_3,B
.= [0,x'] by ARYTM_1:19,C;
0 in {0} by TARSKI:def 1;
then x in [:{0},RAT+:] by D,ZFMISC_1:106,E;
then x in RAT+ \/ [:{0},RAT+:] by XBOOLE_0:def 2;
hence x in RAT by A,XBOOLE_0:def 4,NUMBERS:def 3;
end;
Lm_1: x = m/n implies x in RAT
proof assume
Z: x = m/n;
n is Element of INT by INT_1:def 2;
then consider k such that
W: n = k or n = -k by INT_1:def 1;
per cases by W;
suppose n = k;
hence x in RAT by Z,Lm_1';
suppose n = -k;
then x = (-m)/k by Z, XCMPLX_1:193;
hence x in RAT by Lm_1';
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 Lm_0,Lm_1;
assume
Z: 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 Z;
hence thesis by Lm_1;
end;
let x;
assume x in RAT;
then ex m,n st x = m/n by Lm_0;
hence thesis by Z;
end;
end;
definition let r be number;
attr r is rational means
:Def2: r in RAT;
end;
definition
cluster rational 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;
definition
cluster rational number;
existence
proof
reconsider a = 0 as Integer;
reconsider 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;
suppose
A2: x <> 0;
consider m,n such that
A3: x = m/n by A1,Def1;
take m,n;
A4: x = m*n" by A3,XCMPLX_0:def 9;
hereby assume n = 0;
then n" = 0 by XCMPLX_0:def 7;
hence contradiction by A2,A4;
end;
thus thesis by A3;
end;
canceled;
theorem Th3:
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;
theorem Th4:
RAT c= REAL by NUMBERS:12;
definition
cluster rational -> real number;
coherence
proof let n be number;
assume n in RAT;
hence n in REAL by Th4;
end;
end;
canceled;
theorem Th6:
(ex m,n st x = m/n) implies x is rational
proof
x is Rational iff x in RAT by Def2;
hence thesis by Def1;
end;
theorem Th7:
for x being Integer holds x is Rational
proof
let x be Integer;
x = x/1;
hence thesis by Th6;
end;
definition
cluster integer -> rational number;
coherence by Th7;
end;
canceled 3;
theorem
INT c= RAT by NUMBERS:14;
theorem
NAT c= RAT by NUMBERS:18;
reserve p,q for Rational;
:: Now we prove that fractions of integer denominator and natural numerator
:: or of natural denominator and numerator, etc., are all rational numbers.
definition let p,q;
cluster p*q -> rational;
coherence
proof
consider m1,n1 being Integer such that n1<>0
and A2: p = m1/n1 by Th3;
consider m2,n2 being Integer such that n2<>0
and A4: q = m2/n2 by Th3;
p*q=(m1*m2)/(n1*n2) by A2,A4,XCMPLX_1:77;
hence thesis by Th6;
end;
cluster p+q -> rational;
coherence
proof
consider m1,n1 being Integer such that A6: n1<>0
and A7: p = m1/n1 by Th3;
consider m2,n2 being Integer such that A8: n2<>0
and A9: q = m2/n2 by Th3;
p+q=(m1*n2+m2*n1)/(n1*n2) by A6,A7,A8,A9,XCMPLX_1:117;
hence thesis by Th6;
end;
cluster p-q -> rational;
coherence
proof
consider m1,n1 being Integer such that A11: n1<>0
and A12: p = m1/n1 by Th3;
consider m2,n2 being Integer such that A13: n2<>0
and A14: q = m2/n2 by Th3;
p-q=(m1*n2-m2*n1)/(n1*n2) by A11,A12,A13,A14,XCMPLX_1:131;
hence thesis by Th6;
end;
end;
definition let p,m;
cluster p+m -> rational;
coherence
proof
reconsider x=m as Rational by Th7;
p+x is Rational;hence thesis;
end;
cluster p-m -> rational;
coherence
proof
reconsider x=m as Rational by Th7;
p-x is Rational;hence thesis;
end;
cluster p*m -> rational;
coherence
proof
reconsider x=m as Rational by Th7;
p*x is Rational;hence thesis;
end;
end;
definition let m,p;
cluster m+p -> rational;
coherence
proof
reconsider x=m as Rational by Th7;
x+p is Rational;hence thesis;
end;
cluster m-p -> rational;
coherence
proof
reconsider x=m as Rational by Th7;
x-p is Rational;hence thesis;
end;
cluster m*p -> rational;
coherence
proof
reconsider x=m as Rational by Th7;
x*p is Rational;hence thesis;
end;
end;
definition let p,k;
cluster p+k -> rational;
coherence;
cluster p-k -> rational;
coherence;
cluster p*k -> rational;
coherence;
end;
definition let k,p;
cluster k+p -> rational;
coherence;
cluster k-p -> rational;
coherence;
cluster k*p -> rational;
coherence;
end;
definition
let p;
cluster -p -> rational;
coherence
proof
consider m,n such that n<>0 and A2: p=m/n by Th3;
-p = (-m)/n by A2,XCMPLX_1:188;
hence thesis by Th6;
end;
cluster abs(p) -> rational;
coherence
proof
consider m,n such that A3:n<>0 & p=m/n by Th3;
abs(p)=abs(m)/abs(n) by A3,ABSVALUE:16;
hence thesis by Th6;
end;
end;
:: Now we prove that the quotient of two rational numbers is rational
canceled 3;
theorem Th16:
for p,q holds p/q is Rational
proof
let p,q;
consider m1,n1 being Integer such that n1<>0
and A3: p = m1/n1 by Th3;
consider m2,n2 being Integer such that n2<>0
and A4: q = m2/n2 by Th3;
p/q = p*(m2/n2)" by A4,XCMPLX_0:def 9
.= p*(1/(m2/n2)) by XCMPLX_1:217
.= p*((1*n2)/m2) by XCMPLX_1:78
.= (m1*n2)/(n1*m2) by A3,XCMPLX_1:77;
hence thesis by Th6;
end;
definition let p, q be rational number;
cluster p/q -> rational;
coherence by Th16;
end;
canceled 4;
theorem Th21:
p" is Rational
proof
p" = 1/p by XCMPLX_1:217;
hence thesis;
end;
definition let p be rational number;
cluster p" -> rational;
coherence by Th21;
end;
:: 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
assume A1:a<b;
set d=b-a;set m=[\d"/]+1;set l=[\m*a/]+1;
a-a<b-a by A1,REAL_1:54;
then a+ -a<d by XCMPLX_0:def 8;
then A2:0<d by XCMPLX_0:def 6;
then A3:0<d" by REAL_1:72;
A4: d"<=m by INT_1:52;then
A5:0<m by A3;
A6:0<>m by A2,A4,REAL_1:72;
reconsider p=l/m as Rational;
take p;
A7:0<m" by A5,REAL_1:72;
thus a<p
proof
m*a-1<[\m*a/] by INT_1:def 4;
then m*a<[\m*a/]+1 by REAL_1:84;
then m"*(m*a)<m"*l by A7,REAL_1:70;
then (m"*m)*a<m"*l by XCMPLX_1:4;
then 1*a<m"*l by A6,XCMPLX_0:def 7;
hence thesis by XCMPLX_0:def 9;
end;
A8:[\m*a/]<=m*a by INT_1:def 4;
thus p<b
proof
d"-1<[\d"/] by INT_1:def 4;
then d"<[\d"/]+1 by REAL_1:84;
then d"*d<m*d by A2,REAL_1:70;
then 1<m*d by A2,XCMPLX_0:def 7;
then [\m*a/]+1<m*a+m*d by A8,REAL_1:67;
then l<m*(a+d) by XCMPLX_1:8;
then l<m*(a+(-a+b)) by XCMPLX_0:def 8;
then l<m*((a+ -a)+b) by XCMPLX_1:1;
then l<m*(0+b) by XCMPLX_0:def 6;
then m"*l<m"*(m*b) by A7,REAL_1:70;
then m"*l<(m"*m)*b by XCMPLX_1:4;
then m"*l<1*b by A6,XCMPLX_0:def 7;
hence thesis by XCMPLX_0:def 9;
end;
end;
canceled;
theorem Th24:
ex m,k st k<>0 & p=m/k
proof
consider m,n such that A1:n<>0 & p=m/n by Th3;
now per cases by A1;
suppose 0<n;
then n is Nat by INT_1:16;
hence thesis by A1;
suppose n<0;
then 0<=-n by REAL_1:66;
then A2:-n is Nat by INT_1:16;
A3:p = -(-m/n) by A1
.= -(-m)/n by XCMPLX_1:188
.= (-m)/(-n) by XCMPLX_1:189;
-n<>0 by A1,XCMPLX_1:135;
hence thesis by A2,A3;
end;
hence thesis;
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 Th25:
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);
consider m,k such that A1:k<>0 & p=m/k by Th24;
A2:ex l st P[l] by A1;
ex k1 st P[k1]
& for l1 st P[l1] holds k1<=l1 from Min(A2);
then consider k1 such that A3: (k1<>0 & ex m1 st p=m1/k1)
& for l1 st (l1<>0 & ex n1 st p=n1/l1) holds k1<=l1;
consider m1 such that A4:p=m1/k1
& for l1 st (l1<>0 & ex n1 st p=n1/l1) holds k1<=l1 by A3;
take m1; take k1;
thus k1<>0 by A3;
thus m1/k1=p by A4;
thus for n,l st l<> 0 & p=n/l holds k1 <= l by A4;
thus thesis;
end;
definition let p;
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 & p=m/k
& for n,l st l<>0 & p=n/l holds k<=l by Th25;
take k;
thus thesis by A1;
end;
uniqueness
proof
let k,l such that
A2:k<>0 & (ex m st p=m/k) & for m1,k1 st k1<>0 & p=m1/k1 holds k<=k1 and
A3:l<>0 & (ex n st p=n/l) & for n1,l1 st l1<>0 & p=n1/l1 holds l<=l1;
k<=l & l<=k by A2,A3;
hence thesis by AXIOMS:21;
end;
end;
definition let p;
func numerator(p) -> Integer equals
:Def4: denominator(p)*p;
coherence
proof
consider m such that A1:p=m/denominator(p) by Def3;
denominator(p)<>0 by Def3;
hence thesis by A1,XCMPLX_1:88;
end;
end;
:: Some basic theorems concerning p, numerator(p) and denominator(p).
canceled;
theorem Th27:
0<denominator(p)
proof
0<>denominator(p) by Def3;
hence thesis by NAT_1:19;
end;
canceled;
theorem Th29:
1<=denominator(p)
proof 0<denominator(p) by Th27;
then 0+1<=denominator(p) by NAT_1:38;
hence thesis;
end;
theorem Th30:
0<denominator(p)"
proof
0<denominator(p) by Th27;
hence thesis by REAL_1:72;
end;
canceled 3;
theorem Th34:
1>=denominator(p)"
proof
A1:0<>denominator(p) by Def3;
A2:1<=denominator(p) by Th29;
0<=denominator(p)" by Th30;
then 1*denominator(p)"<=denominator(p)*denominator(p)" by A2,AXIOMS:25;
hence thesis by A1,XCMPLX_0:def 7;
end;
canceled;
theorem Th36:
numerator(p)=0 iff p=0
proof
A1:numerator(p)=denominator(p)*p by Def4;
denominator(p)<>0 by Def3;
hence thesis by A1,XCMPLX_1:6;
end;
theorem Th37:
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)=numerator(p)*x" by XCMPLX_0:def 9
.=(p*x)*x" by Def4
.=p*(x*x") by XCMPLX_1:4
.=p*1 by A1,XCMPLX_0:def 7
.=p;
hence p=numerator(p)*denominator(p)" by XCMPLX_0:def 9;
thus p=denominator(p)"*numerator(p) by A2,XCMPLX_0:def 9;
end;
theorem
p<>0 implies denominator(p)=numerator(p)/p
proof
assume A1:p<>0;
A2:denominator(p)<>0 by Def3;
p*denominator(p)=numerator(p)/denominator(p)*denominator(p) by Th37;
then p"*(p*denominator(p))=p"*numerator(p) by A2,XCMPLX_1:88;
then (p"*p)*denominator(p)=p"*numerator(p) by XCMPLX_1:4;
then 1*denominator(p)=p"*numerator(p) by A1,XCMPLX_0:def 7;
hence denominator(p) =numerator(p)/p by XCMPLX_0:def 9;
end;
canceled;
theorem Th40:
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 Th29;
hence A2:denominator(p)=1 by A1,AXIOMS:21;
numerator(p)=denominator(p)*p by Def4;
hence numerator(p)=p by A2;
end;
theorem Th41:
(numerator(p)=p or denominator(p)=1) implies p is Integer
proof
assume A1:numerator(p)=p or denominator(p)=1;
now per cases by A1;
suppose numerator(p)=p;hence thesis;
suppose denominator(p)=1;
then numerator(p)=p*1 by Def4
.=p;
hence thesis;
end;
hence thesis;
end;
theorem
numerator(p)=p iff denominator(p)=1
proof
now assume denominator(p)=1;
then p is Integer by Th41;
hence numerator(p)=p by Th40;
end;
hence thesis by Th40;
end;
canceled;
theorem
(numerator(p)=p or denominator(p)=1) & 0<=p implies p is Nat
proof
assume A1:(numerator(p)=p or denominator(p)=1) & 0<=p;
then p is Integer by Th41;
hence thesis by A1,INT_1:16;
end;
theorem
1<denominator(p) iff p is not integer
proof
now assume not p is Integer;
then A1:denominator(p)<>1 by Th41;
denominator(p)>=1 by Th29;
hence denominator(p)>1 by A1,REAL_1:def 5;
end;
hence thesis by Th40;
end;
Lm2:1"=1;
theorem
1>denominator(p)" iff p is not integer
proof
A1:denominator(p)"<=1 by Th34;
now assume not p is Integer;
then denominator(p)" <> 1 by Lm2,Th41;
hence denominator(p)"<1 by A1,REAL_1:def 5;
end;
hence thesis by Lm2,Th40;
end;
theorem Th47:
numerator(p)=denominator(p) iff p=1
proof
A1:denominator(p)<>0 by Def3;
A2:now assume numerator(p)=denominator(p);
then numerator(p)/denominator(p)=1 by A1,XCMPLX_1:60;
hence p=1 by Th37;
end;
now assume A3:p=1; then numerator(p)=1 by Th40;
hence numerator(p)=denominator(p) by A3,Th40;
end;
hence thesis by A2;
end;
theorem Th48:
numerator(p)=-denominator(p) iff p=-1
proof
A1:0<>denominator(p) by Def3;
A2:now assume numerator(p)=-denominator(p);
hence p=(-denominator(p))/denominator(p) by Th37
.=-denominator(p)/denominator(p) by XCMPLX_1:188
.=-1 by A1,XCMPLX_1:60;
end;
now assume A3:p=-1; then numerator(p)=-1 by Th40;
hence numerator(p)=-denominator(p) by A3,Th40;
end;
hence thesis by A2;
end;
theorem
-numerator(p)=denominator(p) iff p=-1
proof
-numerator(p)=denominator(p) iff numerator(p)=-denominator(p);
hence thesis by Th48;
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 Th50:
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:92;
hence p=(numerator(p)*m)/(denominator(p)*m) by Th37;
end;
canceled 9;
theorem Th60:
k<>0 & p=m/k implies (ex l st m=numerator(p)*l & k=denominator(p)*l)
proof
assume A1:k<>0 & p=m/k;
A2:denominator(p)<>0 by Def3;
defpred P[Nat] means $1*denominator(p)<=k;
A3:for l st P[l] holds l<=k
proof
let l such that A4:l*denominator(p)<=k;
assume A5: not thesis;
0<denominator(p) by A2,NAT_1:19;
then 0+1<=denominator(p) by NAT_1:38;
then A6:k*1<=k*denominator(p) by NAT_1:20;
0<denominator(p) by A2,NAT_1:19;
then k*denominator(p)<l*denominator(p) by A5,REAL_1:70;
hence contradiction by A4,A6,AXIOMS:22;
end;
A7:1*denominator(p)<=k by A1,Def3;
then A8:ex l1 st P[l1];
consider l such that A9:P[l] and
A10:for l1 st P[l1] holds l1<=l from Max(A3,A8);
take l;
A11:0<>l by A7,A10;
then A12:l*denominator(p)<>0 by A2,XCMPLX_1:6;
A13: now
assume A14:l*denominator(p)<k;
then A15: 0+l*denominator(p)<k;
then 0<=k-l*denominator(p) by REAL_1:86;
then reconsider x=k-l*denominator(p) as Nat by INT_1:16;
A16:0<>x by A15,REAL_1:86;
m/k=(numerator(p)*l)/(l*denominator(p)) by A1,A11,Th50;
then p=(m-numerator(p)*l)/x by A1,A12,A14,XCMPLX_1:124;
then denominator(p)<=k-l*denominator(p) by A16,Def3;
then l*denominator(p)+1*denominator(p)<=k by REAL_1:84;
then (l+1)*denominator(p)<=k by XCMPLX_1:8;
then l+1<=l by A10;
hence contradiction by NAT_1:38;
end;
then A17:k=denominator(p)*l by A9,AXIOMS:21;
p*k=m by A1,XCMPLX_1:88;
hence m=numerator(p)/denominator(p)*(denominator(p)*l) by A17,Th37
.=(numerator(p)/denominator(p)*denominator(p))*l by XCMPLX_1:4
.=numerator(p)*l by A2,XCMPLX_1:88;
thus k=denominator(p)*l by A9,A13,AXIOMS:21;
end;
theorem
p=m/n & n<>0 implies ex m1 st m=numerator(p)*m1 & n=denominator(p)*m1
proof
assume A1:p=m/n & n<>0;
per cases by A1;
suppose n<0; then 0<=-n by REAL_1:66;
then reconsider x=-n as Nat by INT_1:16;A2:x<>0 by A1,XCMPLX_1:135;
p=-(-m/n) by A1
.=-(-m)/n by XCMPLX_1:188
.=(-m)/x by XCMPLX_1:189;
then consider k such that A3:-m=numerator(p)*k & x=denominator(p)*k
by A2,Th60;
take y=-k;
thus m=-numerator(p)*k by A3
.=numerator(p)*y by XCMPLX_1:175;
thus n=-denominator(p)*k by A3
.=denominator(p)*y by XCMPLX_1:175;
suppose 0<n;
then reconsider x=n as Nat by INT_1:16;
consider k such that A4:m=numerator(p)*k & x=denominator(p)*k
by A1,Th60;
reconsider y=k as Integer;take y;
thus m=numerator(p)*y by A4;
thus n=denominator(p)*y by A4;
end;
:: Fraction numerator(p)/denominator(p) is irreducible.
theorem Th62:
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
& ex m,k st numerator(p)=m*l & denominator(p)=k*l;
consider m,k such that A2:numerator(p)=m*l & denominator(p)=k*l by A1;
A3:0<>l by A1;
A4:k<>0 by A2,Def3;
then A5:0<k by NAT_1:19;
A6:now k*1<k*l by A1,A5,REAL_1:70;
hence k<denominator(p) by A2;
end;
p=(m*l)/(k*l) by A2,Th37
.=(m/k)*(l/l) by XCMPLX_1:77
.=m/k*1 by A3,XCMPLX_1:60
.=m/k;
hence contradiction by A4,A6,Def3;
end;
theorem Th63:
(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 A1:(p=m/k & k<>0 & not ex l st 1<l & ex m1,k1 st m=m1*l & k=k1*l);
then consider l such that A2:m=numerator(p)*l & k=denominator(p)*l by Th60;
A3:l<=1 by A1,A2;
l<>0 by A1,A2;
then 0<l by NAT_1:19; then 0+1<=l by NAT_1:38;
then A4:l=1 by A3,AXIOMS:21;
hence k=denominator(p) by A2;
thus m=numerator(p) by A2,A4;
end;
theorem Th64:
p<-1 iff numerator(p)<-denominator(p)
proof
A1:0<>denominator(p) by Def3;
A2:0<denominator(p)" by Th30;
A3:0<denominator(p) by Th27;
A4:now
assume p<-1;
then numerator(p)/denominator(p)<-1 by Th37;
then (numerator(p)/denominator(p))*denominator(p)<(-1)*denominator(p)
by A3,REAL_1:70;
then numerator(p)<(-1)*denominator(p) by A1,XCMPLX_1:88;
then numerator(p)<-(1*denominator(p)) by XCMPLX_1:175;
hence numerator(p)<-denominator(p);
end;
now
assume numerator(p)<-denominator(p);
then numerator(p)<-(1*denominator(p));
then numerator(p)<(-1)*denominator(p) by XCMPLX_1:175;
then numerator(p)*denominator(p)"<((-1)*denominator(p))*denominator(p)"
by A2,REAL_1:70;
then numerator(p)*denominator(p)"<(-1)*(denominator(p)*denominator(p)")
by XCMPLX_1:4;
then numerator(p)*denominator(p)"<(-1)*1 by A1,XCMPLX_0:def 7;
hence p<-1 by Th37;
end;
hence thesis by A4;
end;
theorem Th65:
p<=-1 iff numerator(p)<=-denominator(p)
proof
A1:now assume A2:p<=-1;
now per cases by A2,REAL_1:def 5;
suppose p=-1;
hence numerator(p)<=-denominator(p) by Th48;
suppose p<-1;
hence numerator(p)<=-denominator(p) by Th64;
end;
hence numerator(p)<=-denominator(p);
end;
now assume A3:numerator(p)<=-denominator(p);
now per cases by A3,REAL_1:def 5;
suppose numerator(p)=-denominator(p);
hence p<=-1 by Th48;
suppose numerator(p)<-denominator(p);
hence p<=-1 by Th64;
end;
hence p<=-1;
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 REAL_1:50;
hence thesis by Th64;
end;
theorem
p<=-1 iff denominator(p)<=-numerator(p)
proof
denominator(p)<=-numerator(p) iff -(-numerator(p))<=-denominator(p)
by REAL_1:50;
hence thesis by Th65;
end;
canceled 4;
theorem Th72:
p<1 iff numerator(p)<denominator(p)
proof
A1:0<denominator(p) by Th27;
A2:0<>denominator(p) by Def3;
A3:0<denominator(p)" by Th30;
A4:now assume p<1;
then numerator(p)/denominator(p)<1 by Th37;
then numerator(p)/denominator(p)*denominator(p)<1*denominator(p)
by A1,REAL_1:70;
hence numerator(p)<denominator(p) by A2,XCMPLX_1:88;
end;
now assume numerator(p)<denominator(p);
then numerator(p)*denominator(p)"<denominator(p)*denominator(p)"
by A3,REAL_1:70;
then numerator(p)*denominator(p)"<1 by A2,XCMPLX_0:def 7;
hence p<1 by Th37;
end;
hence thesis by A4;
end;
theorem
p<=1 iff numerator(p)<=denominator(p)
proof
A1:now assume A2:p<=1;
now per cases by A2,REAL_1:def 5;
suppose p=1;
hence numerator(p)<=denominator(p) by Th47;
suppose p<1;
hence numerator(p)<=denominator(p) by Th72;
end;
hence numerator(p)<=denominator(p);
end;
now assume A3:numerator(p)<=denominator(p);
now per cases by A3,REAL_1:def 5;
suppose numerator(p)=denominator(p);
hence p<=1 by Th47;
suppose numerator(p)<denominator(p);
hence p<=1 by Th72;
end;
hence p<=1;
end;
hence thesis by A1;
end;
canceled 2;
theorem Th76:
p<0 iff numerator(p)<0
proof
A1:0<denominator(p) by Th27;
A2:0<>denominator(p) by Def3;
A3:0<denominator(p)" by Th30;
A4:now assume p<0;
then numerator(p)/denominator(p)<0 by Th37;
then numerator(p)/denominator(p)*denominator(p)<0*denominator(p)
by A1,REAL_1:70;
hence numerator(p)<0 by A2,XCMPLX_1:88;
end;
now assume numerator(p)<0;
then numerator(p)*denominator(p)"<0*denominator(p)" by A3,REAL_1:70;
hence p<0 by Th37;
end;
hence thesis by A4;
end;
theorem Th77:
p<=0 iff numerator(p)<=0
proof
A1:now assume A2:p<=0;
now per cases by A2;
suppose p=0;
hence numerator(p)<=0 by Th40;
suppose p<0;
hence numerator(p)<=0 by Th76;
end;
hence numerator(p)<=0;
end;
now assume A3:numerator(p)<=0;
now per cases by A3;
suppose numerator(p)=0;
hence p<=0 by Th36;
suppose numerator(p)<0;
hence p<=0 by Th76;
end;
hence p<=0;
end;
hence thesis by A1;
end;
canceled 2;
theorem Th80:
a<p iff a*denominator(p)<numerator(p)
proof
A1:0<denominator(p) by Th27;
A2:0<>denominator(p) by Def3;
A3:0<denominator(p)" by Th30;
A4:now assume a<p;
then a*denominator(p)<p*denominator(p) by A1,REAL_1:70;
hence a*denominator(p)<numerator(p) by Def4;
end;
now assume a*denominator(p)<numerator(p);
then (a*denominator(p))*denominator(p)"<numerator(p)*denominator(p)"
by A3,REAL_1:70;
then a*(denominator(p)*denominator(p)")<numerator(p)*denominator(p)"
by XCMPLX_1:4;
then a*1<numerator(p)*denominator(p)" by A2,XCMPLX_0:def 7;
hence a<p by Th37;
end;
hence thesis by A4;
end;
theorem
a<=p iff a*denominator(p)<=numerator(p)
proof
A1:denominator(p)<>0 by Def3;
A2:now assume A3:a<=p;
now per cases by A3,REAL_1:def 5;
suppose a=p;
hence numerator(p)>=a*denominator(p) by Def4;
suppose a<p;
hence a*denominator(p)<=numerator(p) by Th80;
end;
hence a*denominator(p)<=numerator(p);
end;
now assume A4:a*denominator(p)<=numerator(p);
now per cases by A4,REAL_1:def 5;
suppose a*denominator(p)=numerator(p);
then p=(a*denominator(p))/(1*denominator(p)) by Th37
.=(a/1)*(denominator(p)/denominator(p)) by XCMPLX_1:77
.=a/1*1 by A1,XCMPLX_1:60
.=a;
hence a<=p;
suppose a*denominator(p)<numerator(p);
hence a<=p by Th80;
end;
hence a<=p;
end;
hence thesis by A2;
end;
canceled 2;
theorem
p=q iff (denominator(p)=denominator(q) & numerator(p)=numerator(q))
proof
now assume denominator(p)=denominator(q) & numerator(p)=numerator(q);
hence p=numerator(q)/denominator(q) by Th37
.=q by Th37;
end;
hence thesis;
end;
canceled;
theorem
p<q iff numerator(p)*denominator(q)<numerator(q)*denominator(p)
proof A1:0<denominator(p) & 0<denominator(q) by Th27;
p<q iff numerator(p)/denominator(p)<q by Th37;
then p<q iff numerator(p)/denominator(p)<numerator(q)/denominator(q)
by Th37;
hence thesis by A1,Lm1;
end;
theorem Th87:
denominator(-p)=denominator(p) & numerator(-p)=-numerator(p)
proof
A1:denominator(p)<>0 by Def3;
A2:denominator(-p)<>0 by Def3;
A3:0<=denominator(p) by Th27;
A4:0<=denominator(-p) by Th27;
A5:p=numerator(p)/denominator(p) by Th37;
-p=-numerator(p)/denominator(p) by Th37
.=(-numerator(p))/denominator(p) by XCMPLX_1:188;
then consider k such that A6:-numerator(p)=numerator(-p)*k
& denominator(p)=denominator(-p)*k by A1,Th60;
k<>0 by A6,Def3;
then 0<k by NAT_1:19; then 0+1<=k by NAT_1:38;
then A7: denominator(-p)*1<=denominator(-p)*k by A4,AXIOMS:25;
A8:p=-(-p)
.=-numerator(-p)/denominator(-p) by Th37
.=(-numerator(-p))/denominator(-p) by XCMPLX_1:188;
then consider l such that A9:-numerator(-p)=numerator(p)*l
& denominator(-p)=denominator(p)*l by A2,Th60;
l<>0 by A9,Def3;
then 0<l by NAT_1:19; then 0+1<=l by NAT_1:38;
then A10: denominator(p)*1<=denominator(p)*l by A3,AXIOMS:25;
hence denominator(p)=denominator(-p) by A6,A7,A9,AXIOMS:21;
numerator(p)/denominator(p)*denominator(p)
=(-numerator(-p))/denominator(p)*denominator(p)
by A5,A6,A7,A8,A9,A10,AXIOMS:21;
then numerator(p)=(-numerator(-p))/denominator(p)*denominator(p)
by A1,XCMPLX_1:88;
then -numerator(p)=-(-numerator(-p)) by A1,XCMPLX_1:88;
hence -numerator(p)=numerator(-p);
end;
theorem Th88:
0<p & q=1/p iff numerator(q)=denominator(p) & denominator(q)=numerator(p)
proof
A1:now assume A2:0<p & q=1/p;
then A3:0<numerator(p) by Th77;A4:0<>numerator(p) by A2,Th77;
A5:q=1/(numerator(p)/denominator(p)) by A2,Th37
.=(1*denominator(p))/numerator(p) by XCMPLX_1:78
.=denominator(p)/numerator(p);
reconsider x=denominator(p) as Integer;
reconsider y=numerator(p) as Nat by A3,INT_1:16;
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 & ex m,l st x=m*k & y=l*k;
consider m,l such that A7:x=m*k & y=l*k by A6;
A8: 0<k by A6,AXIOMS:22;
now assume not 0<=m;
then m*k<0*m by A8,REAL_1:71;
hence contradiction by A7,Th27;
end;
then reconsider z=m as Nat by INT_1:16;
reconsider v=l as Integer;
1<k & numerator(p)=v*k & denominator(p)=z*k by A6,A7;
hence contradiction by Th62;
end;
hence numerator(p)=denominator(q) & denominator(p)=numerator(q) by A4,A5,
Th63;
end;
now assume A9:numerator(q)=denominator(p) & denominator(q)=numerator(p);
then 0<numerator(p) by Th27;
hence 0<p by Th77;
thus q =(1*denominator(p))/numerator(p) by A9,Th37
.=1/(numerator(p)/denominator(p)) by XCMPLX_1:78
.=1/p by Th37;
end;
hence thesis by A1;
end;
theorem
p<0 & q=1/p iff numerator(q)=-denominator(p) & denominator(q)=-numerator(p)
proof
A1:now assume A2:p<0 & q=1/p;
set r=-p;A3:0<r by A2,REAL_1:66;
set s=-q; s=1/r by A2,XCMPLX_1:189;
then numerator(s)=denominator(r) & denominator(s)=numerator(r) by A3,Th88;
then -numerator(q)=denominator(r) & denominator(q)=numerator(r) by Th87;
then -(-numerator(q))=-denominator(p) & denominator(q)=-numerator(p) by
Th87;
hence numerator(q)=-denominator(p) & denominator(q)=-numerator(p);
end;
now assume A4:numerator(q)=-denominator(p) & denominator(q)=-numerator(p);
then 0<-numerator(p) by Th27;
then numerator(p)<0 by REAL_1:66;
hence p<0 by Th76;
thus q=(-denominator(p))/(-numerator(p)) by A4,Th37
.=-(denominator(p)/(-numerator(p))) by XCMPLX_1:188
.=-(-denominator(p)/numerator(p)) by XCMPLX_1:189
.=(1*denominator(p))/numerator(p)
.=1/(numerator(p)/denominator(p)) by XCMPLX_1:78
.=1/p by Th37;
end;
hence thesis by A1;
end;