:: Basic Properties of Rational Numbers
:: by Andrzej Kondracki
::
:: Received July 10, 1990
:: Copyright (c) 1990-2026 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, XCMPLX_0;
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, ZFMISC_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions 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, SUBSET_1, CARD_1;
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 Z9 be Element of REAL+ st Z9 = 0
for x9 being Element of REAL+ st x9 = a holds Z9 - x9 = -a
proof
let Z9 be Element of REAL+ such that A0:Z9 = 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 = Z9 - xx;
A3: Z9 <=' xx by A0,ARYTM_1:6;
then not xx <=' Z9 by A0,A2,ARYTM_1:4;
then
A4: b = [{},xx -' Z9] by ARYTM_1:def 2;
now
assume b = [0,0];
then xx -' Z9 = 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 -' Z9 = xx -' Z9 + Z9 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 -' Z9 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 Z9 = 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 = Z9 - 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 Z9 = 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 = Z9 - 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 :: redefines RAT (NUMBERS, definition)
: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 :Def2:
r in RAT;
end;
registration
cluster rational for Real;
existence
proof
take x = 0/1;
thus x in RAT by Def1;
end;
end;
registration
cluster rational for number;
existence
proof
take x = 0/1;
thus x in RAT by Def1;
end;
end;
definition
mode Rational is rational Number;
end;
registration
let r be Rational;
reduce In(r,RAT) to r;
reducibility by Def2,SUBSET_1:def 8;
end;
registration
let r,s be Rational;
reduce In([r,s],[:RAT,RAT:]) to [r,s];
reducibility
proof
[In(r,RAT),In(s,RAT)] in [:RAT,RAT:] by ZFMISC_1:87;
hence thesis by SUBSET_1:def 8;
end;
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;
per cases;
suppose n = 0;
hence thesis by A2,A3,XCMPLX_1:49;
end;
suppose
A4: n > 0;
take m,n;
thus n > 0 by A4;
thus thesis by A3;
end;
suppose
A5: n < 0;
take -m,-n;
thus -n > 0 by A5,XREAL_1:58;
thus thesis by A3,XCMPLX_1:191;
end;
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
a < b implies ex p st a < p & p < b
proof
set d=b-a;
set m=[\d"/]+1;
set l=[\m*a/]+1;
set p=l/m;
assume a<b;
then
A1: a-a<b-a by XREAL_1:9;
then
A2: 0<m;
d"-1<[\d"/] by INT_1:def 6;
then d"<[\d"/]+1 by XREAL_1:19;
then d"*d<m*d by A1,XREAL_1:68;
then
A3: 1<m*d by A1,XCMPLX_0:def 7;
take p;
A4: 0<>m by A1;
m*a-1<[\m*a/] by INT_1:def 6;
then m*a<[\m*a/]+1 by XREAL_1:19;
then m"*(m*a)<m"*l by A2,XREAL_1:68;
then (m"*m)*a<m"*l;
then 1*a<m"*l by A4,XCMPLX_0:def 7;
hence a<p;
[\m*a/]<=m*a by INT_1:def 6;
then [\m*a/]+1<m*a+m*d by A3,XREAL_1:8;
then m"*l<m"*(m*b) by A2,XREAL_1:68;
then m"*l<(m"*m)*b;
then m"*l<1*b by A4,XCMPLX_0:def 7;
hence p<b;
end;
theorem Th5:
ex m,k st k > 0 & p = m/k
proof
consider m,n such that
A1: n > 0 and
A2: p = m/n by Th2;
per cases by A1;
suppose
0<n;
then n is Element of NAT by INT_1:3;
hence thesis by A1,A2;
end;
suppose
A3: n<0;
A4: p = -(-m)/n by A2
.= (-m)/(-n) by XCMPLX_1:188;
A5: -n<>0 by A1;
-n is Element of NAT by A3,INT_1:3;
hence thesis by A4,A5;
end;
end;
:: Each rational number can be uniquely expressed as a ratio of two
:: relatively prime numbers, the first is integer and the latter is natural
:: (but not equal to zero). Function denominator(p) is defined as the least
:: natural denominator of all denominators of fractions integer/natural=p.
:: Function numerator(p) is defined as a product of p and denominator(p).
theorem 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 IT=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 < denominator p iff p is not integer
proof
now
assume
A1: not p is Integer;
denominator(p)>=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*denominator(p) by XREAL_1:68;
hence contradiction by A7,A6,XXREAL_0:2;
end;
A8: 1*denominator(p)<=k by A1,A2,Def3;
then
A9: ex l1 be Nat st P[l1];
consider l be Nat such that
A10: P[l] and
A11: for l1 be Nat st P[l1] holds l1<=l from NAT_1:sch 6(A5,A9);
reconsider l as Element of NAT by ORDINAL1:def 12;
take l;
A12: 0<>l by A8,A11;
then
A13: l*denominator(p)<>0 by XCMPLX_1:6;
A14: now
assume
A15: l*denominator(p)<k;
then 0+l*denominator(p)<k;
then 0<=k-l*denominator(p) by XREAL_1:20;
then reconsider x=k-l*denominator(p) as Element of NAT by INT_1:3;
A16: 0<>x by A15;
m/k=(numerator(p)*l)/(l*denominator(p)) by A2,A12,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
0<n;
then reconsider x=n as Element of NAT by INT_1:3;
consider k such that
A6: m=numerator(p)*k and
A7: x=denominator(p)*k by A1,A2,Th24;
reconsider y=k as Integer;
take y;
thus thesis by A6,A7;
end;
end;
:: Fraction numerator(p)/denominator(p) is irreducible.
theorem Th26:
not ex w st 1 < w & ex m,k st numerator(p) = m*w & denominator(p) = k*w
proof
assume not thesis;
then consider w such that
A1: 1<w and
A2: ex m,k st numerator(p)=m*w & denominator(p)=k*w;
consider m,k such that
A3: numerator(p)=m*w and
A4: denominator(p)=k*w by A2;
A5: p=(m*w)/(k*w) by A3,A4,Th12
.=(m/k)*(w/w) by XCMPLX_1:76
.=m/k*1 by A1,XCMPLX_1:60
.=m/k;
A6: k<>0 by A4;
then k*1<k*w by A1,XREAL_1:68;
hence contradiction by A4,A6,A5,Def3;
end;
theorem Th27:
(p = m/k & k <> 0 & not ex w st 1 < w & ex m1,k1 st m = m1*w & k = k1*w)
implies k = denominator(p) & m = numerator(p)
proof
assume that
A1: p=m/k and
A2: k<>0 and
A3: not ex w st 1<w & ex m1,k1 st m=m1*w & k=k1*w;
consider w such that
A4: m=numerator(p)*w and
A5: k=denominator(p)*w by A1,A2,Th24;
0<w by A2,A5;
then
A6: 0+1<=w by NAT_1:13;
w<=1 by A3,A4,A5;
then
A7: w=1 by A6,XXREAL_0:1;
hence k=denominator(p) by A5;
thus thesis by A4,A7;
end;
theorem Th28:
p < -1 iff numerator(p) < -denominator(p)
proof
hereby
assume p<-1;
then numerator(p)/denominator(p)<-1 by Th12;
then
(numerator(p)/denominator(p))*denominator(p)<(-1)*denominator(p)
by XREAL_1:68;
hence numerator(p)<-denominator(p) by XCMPLX_1:87;
end;
assume numerator(p)<-denominator(p);
then
numerator(p)*denominator(p)"<((-1)*denominator(p))*denominator(p)"
by XREAL_1:68;
then numerator(p)*denominator(p)"<(-1)*(denominator(p)*denominator(p)");
then numerator(p)*denominator(p)"<(-1)*1 by XCMPLX_0:def 7;
hence p<-1 by Th12;
end;
theorem Th29:
p <= -1 iff numerator(p) <= -denominator(p)
proof
hereby
assume
A2: p<=-1;
per cases by A2,XXREAL_0:1;
suppose
p=-1;
hence numerator(p)<=-denominator(p);
end;
suppose
p<-1;
hence numerator(p)<=-denominator(p) by Th28;
end;
end;
assume
A3: numerator(p)<=-denominator(p);
per cases by A3,XXREAL_0:1;
suppose
numerator(p)=-denominator(p);
hence p<=-1 by Th21;
end;
suppose
numerator(p)<-denominator(p);
hence p<=-1 by Th28;
end;
end;
theorem
p < -1 iff denominator(p) < -numerator(p)
proof
denominator(p)<-numerator(p) iff -(-numerator(p))<-denominator(p) by
XREAL_1:24;
hence thesis by Th28;
end;
theorem
p <= -1 iff denominator(p) <= -numerator(p)
proof
denominator(p)<=-numerator(p) iff -(-numerator(p))<=-denominator(p) by
XREAL_1:24;
hence thesis by Th29;
end;
theorem Th32:
p < 1 iff numerator(p) < denominator(p)
proof
hereby
assume p<1;
then numerator(p)/denominator(p)<1 by Th12;
then numerator(p)/denominator(p)*denominator(p)<1*denominator(p)
by XREAL_1:68;
hence numerator(p)<denominator(p) by XCMPLX_1:87;
end;
assume numerator(p)<denominator(p);
then numerator(p)*denominator(p)"<denominator(p)*denominator(p)"
by XREAL_1:68;
then numerator(p)*denominator(p)"<1 by XCMPLX_0:def 7;
hence p<1 by Th12;
end;
theorem
p <= 1 iff numerator(p) <= denominator(p)
proof
hereby
assume
A2: p<=1;
per cases by A2,XXREAL_0:1;
suppose
p=1;
hence numerator(p)<=denominator(p);
end;
suppose
p<1;
hence numerator(p)<=denominator(p) by Th32;
end;
end;
assume
A3: numerator(p)<=denominator(p);
per cases by A3,XXREAL_0:1;
suppose
numerator(p)=denominator(p);
hence p<=1 by Th20;
end;
suppose
numerator(p)<denominator(p);
hence p<=1 by Th32;
end;
end;
theorem
p < 0 iff numerator(p) < 0
proof
hereby
assume p<0;
then numerator(p)/denominator(p)<0 by Th12;
hence numerator(p)<0;
end;
thus thesis;
end;
theorem Th35:
p <= 0 iff numerator(p) <= 0
proof
now
assume
A1: numerator(p)<=0;
per cases by A1;
suppose
numerator(p)=0;
hence p<=0 by Th11;
end;
suppose
numerator(p)<0;
hence p<=0;
end;
end;
hence thesis;
end;
theorem Th36:
a < p iff a*denominator(p) < numerator(p)
proof
A3: now
assume a*denominator(p)<numerator(p);
then
(a*denominator(p))*denominator(p)"<numerator(p)*denominator(p)"
by XREAL_1:68;
then a*(denominator(p)*denominator(p)")<numerator(p)*denominator(p)";
then a*1<numerator(p)*denominator(p)" by XCMPLX_0:def 7;
hence a<p by Th12;
end;
thus thesis by A3,XREAL_1:68;
end;
theorem
a <= p iff a*denominator(p) <= numerator(p)
proof
hereby
assume
A4: a<=p;
per cases by A4,XXREAL_0:1;
suppose
a=p;
hence numerator(p)>=a*denominator(p);
end;
suppose
a<p;
hence a*denominator(p)<=numerator(p) by Th36;
end;
end;
assume
A3: a*denominator(p)<=numerator(p);
per cases by A3,XXREAL_0:1;
suppose
a*denominator(p)=numerator(p);
then p=(a*denominator(p))/(1*denominator(p)) by Th12
.=(a/1)*(denominator(p)/denominator(p))
.=a by XCMPLX_1:60;
hence a<=p;
end;
suppose
a*denominator(p)<numerator(p);
hence a<=p by Th36;
end;
end;
theorem
denominator p = denominator q & numerator p = numerator q implies p = q
proof
assume that
A1: denominator(p)=denominator(q) and
A2: numerator(p)=numerator(q);
thus p=numerator(q)/denominator(q) by A1,A2,Th12
.=q by Th12;
end;
theorem
p < q iff numerator(p)*denominator(q) < numerator(q)*denominator(p)
proof
p<q iff numerator(p)/denominator(p)<q by Th12;
then
p<q iff numerator(p)/denominator(p)<numerator(q)/denominator(q) by Th12;
hence thesis by XREAL_1:102,106;
end;
theorem Th40:
denominator(-p) = denominator(p) & numerator(-p) = -numerator(p)
proof
A2: p=-(-p) .=-numerator(-p)/denominator(-p) by Th12
.=(-numerator(-p))/denominator(-p);
consider w such that
-numerator(-p)=numerator(p)*w and
A3: denominator(-p)=denominator(p)*w by A2,Th24;
-p=-numerator(p)/denominator(p) by Th12
.=(-numerator(p))/denominator(p);
then consider k such that
A4: -numerator(p)=numerator(-p)*k and
A5: denominator(p)=denominator(-p)*k by Th24;
denominator p = denominator(p)*w*k by A5,A3
.= denominator(p)*(w*k);
then
A6: k = 1 by NAT_1:15,XCMPLX_1:7;
hence denominator(p)=denominator(-p) by A5;
thus thesis by A4,A6;
end;
theorem Th41:
0 < p iff numerator(1/p) = denominator p & denominator(1/p) = numerator p
proof
set q = 1/p;
A1: now
set x=denominator(p);
assume
A2: 0<p;
A4: q=1/(numerator(p)/denominator(p)) by Th12
.=(1*denominator(p))/numerator(p) by XCMPLX_1:77
.=denominator(p)/numerator(p);
reconsider y=numerator(p) as Element of NAT by A2,INT_1:3;
A5: not ex k st 1<k & ex m,w st x=m*k & y=w*k
proof
assume not thesis;
then consider k such that
A6: 1<k and
A7: ex m,w st x=m*k & y=w*k;
consider m,w such that
A8: x=m*k and
A9: y=w*k by A7;
0<=m by A8;
then reconsider z=m as Element of NAT by INT_1:3;
denominator(p)=z*k by A8;
hence contradiction by A6,A9,Th26;
end;
0<>numerator(p) by A2,Th35;
hence numerator(p)=denominator(q) & denominator(p)=numerator(q)
by A4,A5,Th27;
end;
thus thesis by A1;
end;
theorem
p < 0 iff numerator(1/p) = -denominator p & denominator(1/p) = -numerator p
proof
set q = 1/p;
A1: now
set s=-q;
set r=-p;
assume
A2: p<0;
A4: s=1/r by XCMPLX_1:188;
A5: 0<r by A2,XREAL_1:58;
then numerator(s)=denominator(r) by A4,Th41;
then -numerator(q)=denominator(r) by Th40;
then
A6: -(-numerator(q))=-denominator(p) by Th40;
denominator(s)=numerator(r) by A5,A4,Th41;
then denominator(q)=numerator(r) by Th40;
hence numerator(q)=-denominator(p) & denominator(q)=-numerator(p)
by A6,Th40;
end;
thus thesis by A1;
end;
ThA: 1/2 is non integer
proof
set p = 1/2;
assume 1/2 is integer; then
A1: denominator p = 1 & numerator p = p by Th14;
A2: numerator(1/p) = denominator p by Th41;
denominator p = 2 by A2,Th14;
hence thesis by A1;
end;
Thx:
ex k be Rational st k is positive non integer by ThA;
Thx1:
ex k be Rational st k is negative non integer
proof
take a = -1/2;
thus thesis by ThA;
end;
registration
cluster positive for Rational;
existence by Thx;
cluster non integer for positive Rational;
existence by Thx;
cluster negative for Rational;
existence by Thx1;
end;
registration
cluster non integer for negative Rational;
existence
proof
A1: -(1/2) is non integer by ThA;
-(1/2) < 0; then
-(1/2) is negative;
hence thesis by A1;
end;
end;
registration
let a be non zero Rational;
cluster numerator a -> non zero;
coherence by Th11;
end;
registration
let a be non negative Rational;
cluster numerator a -> non negative;
coherence;
end;
registration
let a be non positive Rational;
cluster numerator a -> non positive;
coherence;
end;
registration
let a be Integer;
cluster denominator a -> non zero trivial;
coherence by Th14,CARD_1:49;
end;
registration
let a be Integer;
reduce numerator a to a;
reducibility by Th14;
end;
registration
let a be Rational;
reduce (numerator a)/(denominator a) to a;
reducibility by Th12;
reduce numerator ((numerator a)/(denominator a)) to numerator a;
reducibility;
reduce denominator ((numerator a)/(denominator a)) to denominator a;
reducibility;
end;
registration let a be Rational;
reduce numerator numerator a to numerator a;
reducibility;
reduce numerator denominator a to denominator a;
reducibility;
end;