:: Arithmetic of Non Negative Rational Numbers
:: by Grzegorz Bancerek
::
:: Received March 7, 1998
:: Copyright (c) 1998-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 ORDINAL1, XBOOLE_0, ORDINAL2, TARSKI, SUBSET_1, ORDINAL3,
ARYTM_3, CARD_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, ORDINAL3;
constructors SUBSET_1, ORDINAL3;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, ORDINAL3;
requirements BOOLE, SUBSET, NUMERALS;
definitions TARSKI, ORDINAL1;
equalities TARSKI, ORDINAL1;
expansions TARSKI;
theorems TARSKI, XBOOLE_0, ORDINAL1, ORDINAL2, ORDINAL3, XBOOLE_1, XTUPLE_0;
schemes ORDINAL1;
begin :: Natural ordinals
reserve A,B,C for Ordinal;
Lm1: {} in omega by ORDINAL1:def 11;
Lm2: 1 in omega;
definition
func one -> set equals
1;
correctness;
end;
begin :: Relative prime numbers and divisibility
definition
let a,b be Ordinal;
pred a,b are_coprime means
for c,d1,d2 being Ordinal st a = c *^ d1 & b = c *^ d2 holds c = 1;
symmetry;
end;
theorem
not {},{} are_coprime
proof
take {}, {}, {};
thus thesis by ORDINAL2:35;
end;
theorem Th2:
1,A are_coprime
by ORDINAL3:37;
theorem Th3:
{},A are_coprime implies A = 1
proof
A1: {} = A*^{} & A = A*^1 by ORDINAL2:38,39;
assume {},A are_coprime & A <> 1;
hence contradiction by A1;
end;
reserve a,b,c,d for natural Ordinal;
defpred PP[set] means ex B st B c= $1 & $1 in omega & $1 <> {} & not ex c,d1,
d2 being natural Ordinal st d1,d2 are_coprime & $1 = c *^ d1 & B = c *^
d2;
theorem
a <> {} or b <> {} implies ex c,d1,d2 being natural Ordinal st d1,d2
are_coprime & a = c *^ d1 & b = c *^ d2
proof
assume that
A1: a <> {} or b <> {} and
A2: not ex c,d1,d2 being natural Ordinal st d1,d2 are_coprime & a
= c *^ d1 & b = c *^ d2;
A3: ex A st PP[A]
proof
per cases;
suppose
A4: a c= b;
take A = b, B = a;
thus B c= A & A in omega & A <> {} by A1,A4,ORDINAL1:def 12;
thus thesis by A2;
end;
suppose
A5: b c= a;
take A = a, B = b;
thus B c= A & A in omega & A <> {} by A1,A5,ORDINAL1:def 12;
thus thesis by A2;
end;
end;
consider A such that
A6: PP[A] and
A7: for C st PP[C] holds A c= C from ORDINAL1:sch 1(A3);
consider B such that
A8: B c= A and
A9: A in omega and
A10: A <> {} and
A11: not ex c,d1,d2 being natural Ordinal st d1,d2 are_coprime &
A = c *^ d1 & B = c *^ d2 by A6;
reconsider A,B as Element of omega by A8,A9,ORDINAL1:12;
A = 1 *^ A & B = 1 *^ B by ORDINAL2:39;
then not A,B are_coprime by A11;
then consider c,d1,d2 being Ordinal such that
A12: A = c *^ d1 and
A13: B = c *^ d2 and
A14: c <> 1;
A15: c <> {} by A10,A12,ORDINAL2:35;
then
A16: d1 c= A & d2 c= B by A12,A13,ORDINAL3:36;
A17: d1 <> {} by A10,A12,ORDINAL2:38;
then c c= A by A12,ORDINAL3:36;
then reconsider c,d1,d2 as Element of omega by A16,ORDINAL1:12;
1 in c or c in 1 by A14,ORDINAL1:14;
then 1*^d1 in A by A12,A17,A15,ORDINAL3:14,19;
then
A18: d1 in A by ORDINAL2:39;
A19: now
let c9,d19,d29 be natural Ordinal;
assume that
A20: d19,d29 are_coprime and
A21: d1 = c9 *^ d19 & d2 = c9 *^ d29;
A = c*^c9*^d19 & B = c*^c9*^d29 by A12,A13,A21,ORDINAL3:50;
hence contradiction by A11,A20;
end;
A = d1*^c & B = d2*^c by A12,A13;
then d2 c= d1 by A8,A15,ORDINAL3:35;
hence contradiction by A7,A17,A19,A18,ORDINAL1:5;
end;
reserve l,m,n for natural Ordinal;
registration
let m,n;
cluster m div^ n -> natural;
coherence
proof
A1: n = {} implies m div^ n = {} & {}*^1 = {} by ORDINAL2:35,ORDINAL3:def 6;
n in 1 or 1 c= n by ORDINAL1:16;
then (m div^ n)*^1 c= (m div^ n)*^n by A1,ORDINAL3:14,20;
then
A2: m div^ n c= (m div^ n)*^n by ORDINAL2:39;
(m div^ n)*^n c= m & m in omega by ORDINAL1:def 12,ORDINAL3:64;
hence m div^ n in omega by A2,ORDINAL1:12,XBOOLE_1:1;
end;
cluster m mod^ n -> natural;
coherence
proof
(m div^ n)*^n+^(m mod^ n) = m by ORDINAL3:65;
then
A3: m mod^ n c= m by ORDINAL3:24;
m in omega by ORDINAL1:def 12;
hence m mod^ n in omega by A3,ORDINAL1:12;
end;
end;
definition
let k,n be Ordinal;
pred k divides n means
ex a being Ordinal st n = k*^a;
reflexivity
proof
let n be Ordinal;
take 1;
thus thesis by ORDINAL2:39;
end;
end;
theorem Th5:
a divides b iff ex c st b = a*^c
proof
thus a divides b implies ex c st b = a*^c
proof
given c being Ordinal such that
A1: b = a*^c;
per cases;
suppose
b = {};
then b = a*^{} by ORDINAL2:38;
hence thesis;
end;
suppose
b <> {};
then c is Element of omega by A1,ORDINAL3:75;
hence thesis by A1;
end;
end;
thus thesis;
end;
theorem Th6:
for m,n st {} in m holds n mod^ m in m
proof
let m,n;
assume {} in m;
then
A1: ex C st n = (n div^ m)*^m+^C & C in m by ORDINAL3:def 6;
n mod^ m = n-^(n div^ m)*^m by ORDINAL3:def 7;
hence thesis by A1,ORDINAL3:52;
end;
theorem Th7:
for n,m holds m divides n iff n = m *^ (n div^ m)
proof
let n,m;
assume
A1: not thesis;
then consider a such that
A2: n = m*^a by Th5;
{}*^a = {} by ORDINAL2:35;
then {} <> m by A1,A2,ORDINAL2:35;
then
A3: {} in m by ORDINAL3:8;
n = a*^m+^{} by A2,ORDINAL2:27;
hence thesis by A1,A2,A3,ORDINAL3:def 6;
end;
theorem Th8:
for n,m st n divides m & m divides n holds n = m
proof
let n,m;
assume that
A1: n divides m and
A2: m divides n;
A3: m = n *^ (m div^ n) by A1,Th7;
A4: (m div^ n) *^ (n div^ m) = 1 implies n = m
proof
assume (m div^ n) *^ (n div^ m) = 1;
then m div^ n = 1 by ORDINAL3:37;
hence thesis by A3,ORDINAL2:39;
end;
n = m *^ (n div^ m) by A2,Th7;
then
A5: n *^ 1 = n & n = n *^ ((m div^ n) *^ (n div^ m)) by A3,ORDINAL2:39
,ORDINAL3:50;
n = {} implies n = m by A3,ORDINAL2:35;
hence thesis by A5,A4,ORDINAL3:33;
end;
theorem Th9:
n divides {} & 1 divides n
proof
{} = n *^ {} by ORDINAL2:35;
hence n divides {};
n = 1 *^ n by ORDINAL2:39;
hence thesis;
end;
theorem Th10:
for n,m st {} in m & n divides m holds n c= m
proof
let n,m such that
A1: {} in m;
given a being Ordinal such that
A2: m = n*^a;
a <> {} by A1,A2,ORDINAL2:38;
hence thesis by A2,ORDINAL3:36;
end;
theorem Th11:
for n,m,l st n divides m & n divides m +^ l holds n divides l
proof
let n,m,l;
assume n divides m;
then consider a such that
A1: m = n*^a by Th5;
assume n divides m +^ l;
then consider b such that
A2: m +^ l = n*^b by Th5;
assume
A3: not n divides l;
l = n*^b -^ n*^a by A1,A2,ORDINAL3:52
.= (b-^a)*^n by ORDINAL3:63;
hence thesis by A3;
end;
Lm3: 1 = succ 0;
definition
let k,n be natural Ordinal;
func k lcm n -> Element of omega means
: Def4:
k divides it & n divides it &
for m st k divides m & n divides m holds it divides m;
existence
proof
per cases;
suppose
A1: k = {} or n = {};
reconsider w = {} as Element of omega by ORDINAL1:def 12;
take w;
thus k divides w & n divides w by Th9;
let m;
assume k divides m & n divides m;
hence thesis by A1;
end;
suppose
A2: k <> {} & n <> {};
{} c= k;
then {} c< k by A2,XBOOLE_0:def 8;
then
A3: {} in k by ORDINAL1:11;
{} c= n;
then {} c< n by A2,XBOOLE_0:def 8;
then {} in n by ORDINAL1:11;
then
A4: 1 c= n by Lm3,ORDINAL1:21;
defpred P[Ordinal] means ex m st $1 = m & k divides m & n divides m & k
c= m;
A5: k*^1 = k by ORDINAL2:39;
k divides k *^ n & n divides k *^ n;
then
A6: ex A st P[A] by A4,A5,ORDINAL2:41;
consider A such that
A7: P[A] and
A8: for B st P[B] holds A c= B from ORDINAL1:sch 1(A6);
consider l such that
A9: A = l and
A10: k divides l and
A11: n divides l and
A12: k c= l by A7;
reconsider l as Element of omega by ORDINAL1:def 12;
take l;
thus k divides l & n divides l by A10,A11;
let m such that
A13: k divides m and
A14: n divides m;
A15: m = l*^(m div^ l)+^(m mod^ l) by ORDINAL3:65;
l = k*^(l div^ k) by A10,Th7;
then l*^(m div^ l) = k*^((l div^ k)*^(m div^ l)) by ORDINAL3:50;
then k divides l*^(m div^ l);
then
A16: k divides m mod^ l by A13,A15,Th11;
l = n*^(l div^ n) by A11,Th7;
then l*^(m div^ l) = n*^((l div^ n)*^(m div^ l)) by ORDINAL3:50;
then n divides l*^(m div^ l);
then
A17: n divides m mod^ l by A14,A15,Th11;
now
A18: {} c= m mod^ l;
assume m mod^ l <> {};
then {} c< m mod^ l by A18,XBOOLE_0:def 8;
then k c= m mod^ l by A16,Th10,ORDINAL1:11;
then l c= m mod^ l by A8,A9,A16,A17;
hence contradiction by A12,A3,Th6,ORDINAL1:5;
end;
then m = l*^(m div^ l) by A15,ORDINAL2:27;
hence thesis;
end;
end;
uniqueness
proof
let m1,m2 be Element of omega;
assume k divides m1 & n divides m1 & ( for m st k divides m & n divides
m holds m1 divides m)& k divides m2 &( n divides m2 & for m st k divides m & n
divides m holds m2 divides m );
then m1 divides m2 & m2 divides m1;
hence thesis by Th8;
end;
commutativity;
end;
theorem Th12:
m lcm n divides m*^n
proof
m divides m*^n & n divides m*^n;
hence thesis by Def4;
end;
theorem Th13:
n <> {} implies (m*^n) div^ (m lcm n) divides m
proof
assume
A1: n <> {};
take ((m lcm n) div^ n);
n divides m lcm n by Def4;
then
A2: m lcm n = n*^((m lcm n) div^ n) by Th7;
m lcm n divides m*^n by Th12;
then m*^n = (m lcm n)*^ ((m*^n) div^ (m lcm n)) by Th7;
then n*^m = n*^(((m lcm n) div^ n)*^ ((m*^n) div^ (m lcm n))) by A2,
ORDINAL3:50;
hence m = ((m*^n) div^ (m lcm n))*^((m lcm n) div^ n) by A1,ORDINAL3:33;
end;
definition
let k,n be natural Ordinal;
func k hcf n -> Element of omega means
: Def5:
it divides k & it divides n &
for m st m divides k & m divides n holds m divides it;
existence
proof
per cases;
suppose
A1: k = {} or n = {};
then reconsider m1 = k \/ n as Element of omega by ORDINAL1:def 12;
take m1;
thus m1 divides k & m1 divides n by A1,Th9;
thus thesis by A1;
end;
suppose
A2: k <> {} & n <> {};
reconsider l = (k*^n) div^ (k lcm n) as Element of omega by
ORDINAL1:def 12;
take l;
thus l divides k & l divides n by A2,Th13;
let m;
assume that
A3: m divides k and
A4: m divides n;
A5: n = m*^(n div^ m) by A4,Th7;
then
A6: n div^ m <> {} by A2,ORDINAL2:35;
m*^(k div^ m)*^(n div^ m) = n*^(k div^ m) by A5,ORDINAL3:50;
then
A7: n divides m*^(k div^ m)*^(n div^ m);
set mm = m*^((k div^ m)*^(n div^ m));
A8: mm = m*^(k div^ m)*^(n div^ m) by ORDINAL3:50;
A9: k = m*^(k div^ m) by A3,Th7;
then k div^ m <> {} by A2,ORDINAL2:35;
then
A10: (k div^ m)*^(n div^ m) <> {} by A6,ORDINAL3:31;
k divides m*^(k div^ m)*^(n div^ m) by A9;
then k lcm n divides m*^(k div^ m)*^(n div^ m) by A7,Def4;
then
A11: mm = (k lcm n)*^(mm div^ (k lcm n)) by A8,Th7;
m <> {} by A2,A9,ORDINAL2:35;
then k lcm n <> {} by A11,A10,ORDINAL2:35,ORDINAL3:31;
then
A12: k*^n = k*^n+^{} & {} in k lcm n by ORDINAL2:27,ORDINAL3:8;
mm*^m = (k lcm n)*^(m*^(mm div^ (k lcm n))) by A11,ORDINAL3:50;
then k*^n = (k lcm n)*^(m*^(mm div^ (k lcm n))) by A9,A5,A8,ORDINAL3:50;
then l = m*^(mm div^ (k lcm n)) by A12,ORDINAL3:66;
hence thesis;
end;
end;
uniqueness
proof
let m1,m2 be Element of omega;
assume m1 divides k & m1 divides n & ( for m st m divides k & m divides
n holds m divides m1)& m2 divides k &( m2 divides n & for m st m divides k & m
divides n holds m divides m2 );
then m1 divides m2 & m2 divides m1;
hence thesis by Th8;
end;
commutativity;
end;
theorem Th14:
a hcf {} = a & a lcm {} = {}
proof
reconsider e = a, c = {} as Element of omega by ORDINAL1:def 12;
A1: for b st a divides b & {} divides b holds c divides b;
( for n st n divides a & n divides {} holds n divides e)& a divides c by Th9;
hence thesis by A1,Def4,Def5;
end;
theorem Th15:
a hcf b = {} implies a = {}
proof
a hcf b divides a by Def5;
then a = (a hcf b)*^(a div^ (a hcf b)) by Th7;
hence thesis by ORDINAL2:35;
end;
theorem Th16:
a hcf a = a & a lcm a = a
proof
reconsider c = a as Element of omega by ORDINAL1:def 12;
for b st b divides a & b divides a holds b divides c;
hence a hcf a = a by Def5;
for b st a divides b & a divides b holds c divides b;
hence thesis by Def4;
end;
theorem Th17:
(a*^c) hcf (b*^c) = (a hcf b)*^c
proof
per cases;
suppose
A1: c = {};
then
A2: (a hcf b)*^c = {} by ORDINAL2:35;
a*^c = {} & b*^c = {} by A1,ORDINAL2:35;
hence thesis by A2,Th16;
end;
suppose
A3: c <> {} & a <> {};
reconsider d = (a hcf b)*^c as Element of omega by ORDINAL1:def 12;
set e = ((a*^c) hcf (b*^c)) div^ d;
a hcf b divides b by Def5;
then b = (a hcf b)*^(b div^ (a hcf b)) by Th7;
then b*^c = d*^(b div^ (a hcf b)) by ORDINAL3:50;
then
A4: d divides b*^c;
a hcf b divides a by Def5;
then a = (a hcf b)*^(a div^ (a hcf b)) by Th7;
then a*^c = d*^(a div^ (a hcf b)) by ORDINAL3:50;
then d divides a*^c;
then d divides (a*^c) hcf (b*^c) by A4,Def5;
then
A5: (a*^c) hcf (b*^c) = d*^e by Th7
.= (a hcf b)*^e*^c by ORDINAL3:50;
then (a hcf b)*^e*^c divides b*^c by Def5;
then (a hcf b)*^e*^c*^((b*^c)div^((a hcf b)*^e*^c)) = b*^c by Th7;
then (a hcf b)*^e*^((b*^c)div^((a hcf b)*^e*^c))*^c = b*^c by ORDINAL3:50;
then (a hcf b)*^e*^((b*^c)div^((a hcf b)*^e*^c)) = b by A3,ORDINAL3:33;
then
A6: (a hcf b)*^e divides b;
(a hcf b)*^e*^c divides a*^c by A5,Def5;
then (a hcf b)*^e*^c*^((a*^c)div^((a hcf b)*^e*^c)) = a*^c by Th7;
then (a hcf b)*^e*^((a*^c)div^((a hcf b)*^e*^c))*^c = a*^c by ORDINAL3:50;
then (a hcf b)*^e*^((a*^c)div^((a hcf b)*^e*^c)) = a by A3,ORDINAL3:33;
then (a hcf b)*^e divides a;
then (a hcf b)*^e divides a hcf b by A6,Def5;
then (a hcf b)*^e*^((a hcf b) div^ ((a hcf b)*^e)) = a hcf b by Th7;
then (a hcf b)*^(e*^((a hcf b) div^ ((a hcf b)*^e))) = a hcf b by
ORDINAL3:50
.= (a hcf b)*^1 by ORDINAL2:39;
then a hcf b = {} or e*^((a hcf b) div^ ((a hcf b)*^e)) = 1 by ORDINAL3:33;
then e = 1 by A3,Th15,ORDINAL3:37;
hence thesis by A5,ORDINAL2:39;
end;
suppose
a = {};
then a hcf b = b & a*^c = {} by Th14,ORDINAL2:35;
hence thesis by Th14;
end;
end;
theorem Th18:
b <> {} implies a hcf b <> {} & b div^ (a hcf b) <> {}
proof
a hcf b divides b by Def5;
then b = (a hcf b)*^(b div^ (a hcf b)) by Th7;
hence thesis by ORDINAL2:35;
end;
theorem Th19:
a <> {} or b <> {} implies a div^ (a hcf b), b div^ (a hcf b)
are_coprime
proof
assume
A1: a <> {} or b <> {};
set ab = a hcf b;
A2: 1*^a = a & 1*^b = b by ORDINAL2:39;
per cases;
suppose
a = {} or b = {};
then ab = b & b div^ b = 1 or ab = a & a div^ a = 1 by A1,A2,Th14,
ORDINAL3:68;
hence thesis by Th2;
end;
suppose
A3: a <> {} & b <> {};
ab divides b by Def5;
then
A4: b = ab*^(b div^ ab) by Th7;
then
A5: b div^ ab <> {} by A3,ORDINAL2:35;
let c,d1,d2 be Ordinal such that
A6: a div^ (a hcf b) = c *^ d1 and
A7: b div^ (a hcf b) = c *^ d2;
ab divides a by Def5;
then
A8: a = ab*^(a div^ ab) by Th7;
then a div^ ab <> {} by A3,ORDINAL2:35;
then reconsider c,d1,d2 as Element of omega by A6,A7,A5,ORDINAL3:75;
b = ab*^c*^d2 by A4,A7,ORDINAL3:50;
then
A9: ab*^c divides b;
a = ab*^c*^d1 by A8,A6,ORDINAL3:50;
then ab*^c divides a;
then ab*^c divides ab by A9,Def5;
then ab = (ab*^c)*^(ab div^ (ab*^c)) by Th7;
then ab = ab*^(c*^(ab div^ (ab*^c))) by ORDINAL3:50;
then
A10: ab*^1 = ab*^(c*^(ab div^ (ab*^c))) by ORDINAL2:39;
ab <> {} by A3,A8,ORDINAL2:35;
then 1 = c*^(ab div^ (ab*^c)) by A10,ORDINAL3:33;
hence thesis by ORDINAL3:37;
end;
end;
Lm4: 0 = {};
theorem Th20:
a,b are_coprime iff a hcf b = 1
proof
a hcf b divides b by Def5;
then
A1: b = (a hcf b)*^(b div^ (a hcf b)) by Th7;
a hcf b divides a by Def5;
then a = (a hcf b)*^(a div^ (a hcf b)) by Th7;
hence a,b are_coprime implies a hcf b = 1 by A1;
assume
A2: a hcf b = 1;
let c,d1,d2 be Ordinal such that
A3: a = c*^d1 & b = c*^d2;
a <> {} or b <> {} by A2,Th14,Lm4;
then reconsider c as Element of omega by A3,ORDINAL3:75;
c divides a & c divides b by A3;
then c divides 1 by A2,Def5;
then ex d st 1 = c*^d by Th5;
hence thesis by ORDINAL3:37;
end;
definition
let a,b be natural Ordinal;
func RED(a,b) -> Element of omega equals
a div^ (a hcf b);
coherence by ORDINAL1:def 12;
end;
theorem Th21:
RED(a,b)*^(a hcf b) = a
proof
a hcf b divides a by Def5;
hence thesis by Th7;
end;
theorem
a <> {} or b <> {} implies RED(a,b), RED(b,a) are_coprime by Th19;
theorem Th23:
a,b are_coprime implies RED(a,b) = a
proof
assume a,b are_coprime;
then a hcf b = 1 by Th20;
hence thesis by ORDINAL3:71;
end;
theorem Th24:
RED(a,1) = a & RED(1,a) = 1
proof
a,1 are_coprime by Th2;
then a hcf 1 = 1 by Th20;
hence thesis by ORDINAL3:71;
end;
theorem
b <> {} implies RED(b,a) <> {} by Th18;
theorem Th26:
RED({},a) = {} & (a <> {} implies RED(a,{}) = 1)
proof
thus RED({},a) = {} by ORDINAL3:70;
assume
A1: a <> {};
thus RED(a,{}) = a div^ a by Th14
.= a*^1 div^ a by ORDINAL2:39
.= 1 by A1,ORDINAL3:68;
end;
theorem Th27:
a <> {} implies RED(a,a) = 1
proof
assume
A1: a <> {};
thus RED(a,a) = a div^ a by Th16
.= a*^1 div^ a by ORDINAL2:39
.= 1 by A1,ORDINAL3:68;
end;
theorem Th28:
c <> {} implies RED(a*^c, b*^c) = RED(a, b)
proof
assume
A1: c <> {};
a <> {} implies a hcf b <> {} by Th18;
then
A2: a <> {} implies (a hcf b)*^c <> {} by A1,ORDINAL3:31;
A3: RED({},b) = {} & {}*^((a hcf b)*^c) = {} by ORDINAL2:35,ORDINAL3:70;
A4: a hcf b divides a by Def5;
thus RED(a*^c, b*^c) = (a*^c)div^((a hcf b)*^c) by Th17
.= (((a div^(a hcf b))*^(a hcf b))*^c)div^((a hcf b)*^c) by A4,Th7
.= (RED(a,b)*^((a hcf b)*^c))div^((a hcf b)*^c) by ORDINAL3:50
.= RED(a, b) by A2,A3,ORDINAL3:68,70;
end;
set RATplus = {[a,b] where a,b is Element of omega: a,b are_coprime & b
<> {}};
Lm5: [a,b] in RATplus implies a,b are_coprime & b <> {}
proof
assume [a,b] in RATplus;
then consider c,d being Element of omega such that
A1: [a,b] = [c,d] and
A2: c,d are_coprime & d <> {};
a = c by A1,XTUPLE_0:1;
hence thesis by A1,A2,XTUPLE_0:1;
end;
begin :: Non negative rationals
reserve i,j,k for Element of omega;
definition
func RAT+ -> set equals
({[i,j]: i,j are_coprime & j <> {}} \ the set of all [k,1]) \/ omega;
correctness;
end;
Lm6: omega c= RAT+ by XBOOLE_1:7;
reserve x,y,z for Element of RAT+;
registration
cluster RAT+ -> non empty;
coherence;
end;
registration
cluster non empty ordinal for Element of RAT+;
existence by Lm2,Lm6,Lm4;
end;
theorem Th29:
x in omega or ex i,j st x = [i,j] & i,j are_coprime & j <> {} & j <> 1
proof
assume not x in omega;
then
A1: x in RATplus \ the set of all [k,1] by XBOOLE_0:def 3;
then
A2: not x in the set of all [k,1] by XBOOLE_0:def 5;
x in RATplus by A1;
then consider a,b being Element of omega such that
A3: x = [a,b] & a,b are_coprime & b <> {};
[a,1] in the set of all [k,1];
hence thesis by A2,A3;
end;
theorem Th30:
not ex i,j being set st [i,j] is Ordinal
proof
given i,j being set such that
A1: [i,j] is Ordinal;
{} in {{i},{i,j}} by A1,ORDINAL3:8;
hence thesis by TARSKI:def 2;
end;
theorem Th31:
A in RAT+ implies A in omega
proof
assume A in RAT+ & not A in omega;
then ex i,j st A = [i,j] & i,j are_coprime & j <> {} & j <> 1 by Th29;
hence thesis by Th30;
end;
registration
cluster -> natural for ordinal Element of RAT+;
coherence
proof
let x be ordinal Element of RAT+;
assume not x in omega;
then
A1: ex i,j st x = [i,j] & i,j are_coprime & j <> {} & j <> 1 by Th29;
then {} in x by ORDINAL3:8;
hence thesis by A1,TARSKI:def 2;
end;
end;
theorem Th32:
not ex i,j being object st [i,j] in omega
proof
given i,j being object such that
A1: [i,j] in omega;
reconsider a = [i,j] as Element of omega by A1;
{} in a by ORDINAL3:8;
hence thesis by TARSKI:def 2;
end;
theorem Th33:
[i,j] in RAT+ iff i,j are_coprime & j <> {} & j <> 1
proof
A1: not [i,j] in omega by Th32;
hereby
assume [i,j] in RAT+;
then
A2: [i,j] in RATplus \ the set of all [k,1] by A1,XBOOLE_0:def 3;
hence i,j are_coprime & j <> {} by Lm5;
not [i,j] in the set of all [k,1] by A2,XBOOLE_0:def 5;
hence j <> 1;
end;
assume i,j are_coprime & j <> {};
then
A3: [i,j] in RATplus;
assume j <> 1;
then not ex k st [i,j] = [k,1] by XTUPLE_0:1;
then not [i,j] in the set of all [k,1];
then [i,j] in RATplus \ the set of all [k,1] by A3,XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
definition
let x be Element of RAT+;
func numerator x -> Element of omega means
:Def8:
it = x if x in omega otherwise ex a st x = [it,a];
existence
proof
thus x in omega implies ex a being Element of omega st a = x;
assume not x in omega;
then x in RATplus \ the set of all [k,1] by XBOOLE_0:def 3;
then x in RATplus;
then consider a,b being Element of omega such that
A1: x = [a,b] and
a,b are_coprime and
b <> {};
take a,b;
thus thesis by A1;
end;
correctness by XTUPLE_0:1;
func denominator x -> Element of omega means
: Def9:
it = 1 if x in omega otherwise ex a st x = [a,it];
existence
proof
thus x in omega implies ex a being Element of omega st a = 1;
assume not x in omega;
then x in RATplus \ the set of all [k,1] by XBOOLE_0:def 3;
then x in RATplus;
then consider a,b being Element of omega such that
A2: x = [a,b] and
a,b are_coprime and
b <> {};
take b,a;
thus thesis by A2;
end;
correctness by XTUPLE_0:1;
end;
theorem Th34:
numerator x, denominator x are_coprime
proof
per cases;
suppose
x in omega;
then denominator x = 1 by Def9;
hence thesis by Th2;
end;
suppose
A1: not x in omega;
then consider i,j such that
A2: x = [i,j] and
A3: i,j are_coprime and
j <> {} and
j <> 1 by Th29;
i = numerator x by A1,A2,Def8;
hence thesis by A1,A2,A3,Def9;
end;
end;
theorem Th35:
denominator x <> {}
proof
per cases;
suppose
x in omega;
hence thesis by Def9,Lm4;
end;
suppose
A1: not x in omega;
then ex i,j st x = [i,j] & i,j are_coprime & j <> {} & j <> 1 by
Th29;
hence thesis by A1,Def9;
end;
end;
theorem Th36:
not x in omega implies x = [numerator x, denominator x] & denominator x <> 1
proof
assume
A1: not x in omega;
then consider i,j such that
A2: x = [i,j] and
i,j are_coprime and
j <> {} and
A3: j <> 1 by Th29;
i = numerator x by A1,A2,Def8;
hence thesis by A1,A2,A3,Def9;
end;
theorem Th37:
x <> {} iff numerator x <> {}
proof
hereby
assume that
A1: x <> {} and
A2: numerator x = {};
A3: not x in omega by A1,A2,Def8;
then consider i,j such that
A4: x = [i,j] and
A5: i,j are_coprime and
j <> {} and
A6: j <> 1 by Th29;
i = {} by A2,A3,A4,Def8;
hence contradiction by A5,A6,Th3;
end;
{} in omega by ORDINAL1:def 11;
hence thesis by Def8;
end;
theorem
x in omega iff denominator x = 1 by Def9,Th36;
definition
let i,j be natural Ordinal;
func i/j -> Element of RAT+ equals
:Def10:
{} if j = {}, RED(i,j) if RED(j,i
) = 1 otherwise [RED(i,j), RED(j,i)];
coherence
proof
A1: now
assume j <> {};
then RED(i,j), RED(j,i) are_coprime & RED(j,i) <> {} by Th18,Th19;
hence RED(j,i) <> 1 implies [RED(i,j), RED(j,i)] in RAT+ by Th33;
end;
thus thesis by A1,Lm1,Lm6;
end;
consistency by Th26,Lm4;
end;
notation
let i,j be natural Ordinal;
synonym quotient(i,j) for i/j;
end;
theorem Th39:
(numerator x)/(denominator x) = x
proof
A1: denominator x <> {} by Th35;
A2: RED(numerator x, denominator x) = numerator x by Th23,Th34;
numerator x, denominator x are_coprime by Th34;
then
A3: RED(denominator x, numerator x) = denominator x by Th23;
per cases;
suppose
A4: denominator x = 1;
then x in omega by Th36;
then numerator x = x by Def8;
hence thesis by A2,A3,A4,Def10;
end;
suppose
A5: denominator x <> 1;
then not x in omega by Def9;
then x = [numerator x, denominator x] by Th36;
hence thesis by A1,A2,A3,A5,Def10;
end;
end;
theorem Th40:
{}/b = {} & a/1 = a
proof
A1: b <> {} implies RED(b,{}) = 1 by Th26;
RED({},b) = {} by Th26;
hence {}/b = {} by A1,Def10;
RED(1,a) = 1 & RED(a,1) = a by Th24;
hence thesis by Def10;
end;
theorem Th41:
a <> {} implies a/a = 1
proof
assume a <> {};
then RED(a,a) = 1 by Th27;
hence thesis by Def10;
end;
theorem Th42:
b <> {} implies numerator (a/b) = RED(a,b) & denominator (a/b) = RED(b,a)
proof
assume
A1: b <> {};
per cases;
suppose
A2: RED(b,a) = 1;
then a/b = RED(a,b) by Def10;
hence thesis by A2,Def8,Def9;
end;
suppose
A3: RED(b,a) <> 1;
A4: not [RED(a,b), RED(b,a)] in omega by Th32;
a/b = [RED(a,b), RED(b,a)] by A1,A3,Def10;
hence thesis by A4,Def8,Def9;
end;
end;
theorem Th43:
i,j are_coprime & j <> {} implies numerator (i/j) = i &
denominator (i/j) = j
proof
assume i,j are_coprime;
then RED(i,j) = i & RED(j,i) = j by Th23;
hence thesis by Th42;
end;
theorem Th44:
c <> {} implies (a*^c)/(b*^c) = a/b
proof
assume
A1: c <> {};
per cases;
suppose
b = {};
then a/b = {} & b*^c = {} by Def10,ORDINAL2:35;
hence thesis by Def10;
end;
suppose
A2: b <> {};
then
A3: b*^c <> {} by A1,ORDINAL3:31;
then
A4: denominator ((a*^c)/(b*^c)) = RED(b*^c,a*^c) by Th42
.= RED(b,a) by A1,Th28
.= denominator (a/b) by A2,Th42;
numerator ((a*^c)/(b*^c)) = RED(a*^c,b*^c) by A3,Th42
.= RED(a,b) by A1,Th28
.= numerator (a/b) by A2,Th42;
hence (a*^c)/(b*^c) = (numerator (a/b))/denominator (a/b) by A4,Th39
.= a/b by Th39;
end;
end;
reserve i,j,k for natural Ordinal;
theorem Th45:
j <> {} & l <> {} implies (i/j = k/l iff i*^l = j*^k)
proof
assume that
A1: j <> {} and
A2: l <> {};
set x = i/j, y = k/l;
set ny = numerator y, dy = denominator y;
A3: ny = RED(k,l) by A2,Th42;
set nx = numerator x, dx = denominator x;
A4: dx = RED(j,i) by A1,Th42;
A5: dy = RED(l,k) by A2,Th42;
A6: nx = RED(i,j) by A1,Th42;
hereby
assume i/j = k/l;
then i = ny*^(i hcf j) & l = dx*^(l hcf k) by A6,A5,Th21;
hence i*^l = ny*^(i hcf j)*^dx*^(l hcf k) by ORDINAL3:50
.= ny*^((i hcf j)*^dx)*^(l hcf k) by ORDINAL3:50
.= ny*^j*^(l hcf k) by A4,Th21
.= j*^(ny*^(l hcf k)) by ORDINAL3:50
.= j*^k by A3,Th21;
end;
assume
A7: i*^l = j*^k;
then dx = RED(j*^l,j*^k) by A2,A4,Th28;
then
A8: dx = dy by A1,A5,Th28;
nx = RED(j*^k,j*^l) by A2,A6,A7,Th28;
then nx = ny by A1,A3,Th28;
then x = ny/dy by A8,Th39;
hence thesis by Th39;
end;
definition
let x,y be Element of RAT+;
func x+y -> Element of RAT+ equals
((numerator x)*^(denominator y)+^(
numerator y)*^(denominator x)) / ((denominator x)*^(denominator y));
coherence;
commutativity;
func x*'y -> Element of RAT+ equals
((numerator x)*^(numerator y)) / ((
denominator x)*^(denominator y));
coherence;
commutativity;
end;
theorem Th46:
j <> {} & l <> {} implies (i/j)+(k/l) = (i*^l+^j*^k)/(j*^l)
proof
assume that
A1: j <> {} and
A2: l <> {};
A3: denominator (k/l) = RED(l,k) & denominator (i/j) = RED(j,i) by A1,A2,Th42;
numerator (k/l) = RED(k,l) & numerator (i/j) = RED(i,j) by A1,A2,Th42;
hence
(i/j)+(k/l) = (RED(i,j)*^RED(l,k)+^RED(j,i)*^RED(k,l))*^(i hcf j) /(RED
(j,i)*^RED(l,k)*^(i hcf j)) by A1,A3,Th15,Th44
.= (RED(i,j)*^RED(l,k)+^RED(j,i)*^RED(k,l))*^(i hcf j) /(RED(l,k)*^(RED(
j,i)*^(i hcf j))) by ORDINAL3:50
.= (RED(i,j)*^RED(l,k)+^RED(j,i)*^RED(k,l))*^(i hcf j)/(RED(l,k)*^j) by
Th21
.= (RED(i,j)*^RED(l,k)*^(i hcf j)+^RED(j,i)*^RED(k,l)*^(i hcf j)) /(RED(
l,k)*^j) by ORDINAL3:46
.= (RED(l,k)*^(RED(i,j)*^(i hcf j))+^RED(j,i)*^RED(k,l)*^(i hcf j)) /(
RED(l,k)*^j) by ORDINAL3:50
.= (RED(l,k)*^i+^RED(j,i)*^RED(k,l)*^(i hcf j))/(RED(l,k)*^j) by Th21
.= (RED(l,k)*^i+^RED(k,l)*^(RED(j,i)*^(i hcf j)))/(RED(l,k)*^j) by
ORDINAL3:50
.= (RED(l,k)*^i+^RED(k,l)*^j)/(RED(l,k)*^j) by Th21
.= ((RED(l,k)*^i+^RED(k,l)*^j)*^(k hcf l))/(RED(l,k)*^j*^(k hcf l)) by A2
,Th15,Th44
.= ((RED(l,k)*^i+^RED(k,l)*^j)*^(k hcf l))/(j*^(RED(l,k)*^(k hcf l))) by
ORDINAL3:50
.= ((RED(l,k)*^i+^RED(k,l)*^j)*^(k hcf l))/(j*^l) by Th21
.= (RED(l,k)*^i*^(k hcf l)+^RED(k,l)*^j*^(k hcf l))/(j*^l) by ORDINAL3:46
.= (i*^(RED(l,k)*^(k hcf l))+^RED(k,l)*^j*^(k hcf l))/(j*^l) by ORDINAL3:50
.= (i*^l+^RED(k,l)*^j*^(k hcf l))/(j*^l) by Th21
.= (i*^l+^j*^(RED(k,l)*^(k hcf l)))/(j*^l) by ORDINAL3:50
.= (i*^l+^j*^k)/(j*^l) by Th21;
end;
theorem Th47:
k <> {} implies (i/k)+(j/k) = (i+^j)/k
proof
assume
A1: k <> {};
hence (i/k)+(j/k) = (i*^k+^j*^k)/(k*^k) by Th46
.= ((i+^j)*^k)/(k*^k) by ORDINAL3:46
.= (i+^j)/k by A1,Th44;
end;
registration
cluster empty for Element of RAT+;
existence by Lm1,Lm6;
end;
definition
redefine func {} -> Element of RAT+; :: redefines {} (XBOOLE_0, definition)
coherence by Lm1,Lm6;
redefine func one -> non empty ordinal Element of RAT+; :: redefines one (ARYTM_3, definition)
coherence by Lm6,Lm4;
end;
theorem Th48:
x*'{} = {}
proof
numerator {} = {} & (numerator x)*^{} = {} by Def8,Lm1,ORDINAL2:35;
hence thesis by Th40;
end;
theorem Th49:
(i/j)*'(k/l) = (i*^k)/(j*^l)
proof
per cases;
suppose
A1: j <> {} & l <> {};
then
A2: denominator (k/l) = RED(l,k) & denominator (i/j) = RED(j,i) by Th42;
numerator (k/l) = RED(k,l) & numerator (i/j) = RED(i,j) by A1,Th42;
hence
(i/j)*'(k/l) = (RED(i,j)*^RED(k,l)*^(i hcf j))/(RED(j,i)*^RED(l,k)*^(
i hcf j)) by A1,A2,Th15,Th44
.= (RED(k,l)*^(RED(i,j)*^(i hcf j)))/(RED(j,i)*^RED(l,k)*^(i hcf j))
by ORDINAL3:50
.= (RED(k,l)*^i)/(RED(j,i)*^RED(l,k)*^(i hcf j)) by Th21
.= (RED(k,l)*^i)/(RED(l,k)*^(RED(j,i)*^(i hcf j))) by ORDINAL3:50
.= (RED(k,l)*^i)/(RED(l,k)*^j) by Th21
.= (RED(k,l)*^i*^(l hcf k))/(RED(l,k)*^j*^(l hcf k)) by A1,Th15,Th44
.= (i*^(RED(k,l)*^(l hcf k)))/(RED(l,k)*^j*^(l hcf k)) by ORDINAL3:50
.= (i*^k)/(RED(l,k)*^j*^(l hcf k)) by Th21
.= (i*^k)/(j*^(RED(l,k)*^(l hcf k))) by ORDINAL3:50
.= (i*^k)/(j*^l) by Th21;
end;
suppose
A3: j = {} or l = {};
then i/j = {} or k/l = {} by Def10;
then
A4: (i/j)*'(k/l) = {} by Th48;
j*^l = {} by A3,ORDINAL2:35;
hence thesis by A4,Def10;
end;
end;
theorem Th50:
x+{} = x
proof
A1: (numerator x)*^1 = numerator x & {}*^(denominator x) = {} by ORDINAL2:35,39
;
A2: (denominator x)*^1 = denominator x & (numerator x)+^{} = numerator x by
ORDINAL2:27,39;
denominator {} = 1 & numerator {} = {} by Def8,Def9,Lm1;
hence thesis by A1,A2,Th39;
end;
theorem Th51:
(x+y)+z = x+(y+z)
proof
set nx = numerator x, ny = numerator y, nz = numerator z;
set dx = denominator x, dy = denominator y, dz = denominator z;
A1: dy <> {} by Th35;
A2: dz <> {} by Th35;
then
A3: dy*^dz <> {} by A1,ORDINAL3:31;
A4: dx <> {} by Th35;
then
A5: dx*^dy <> {} by A1,ORDINAL3:31;
thus x+y+z = (nx*^dy+^dx*^ny)/(dx*^dy)+nz/dz by Th39
.= ((nx*^dy+^dx*^ny)*^dz+^(dx*^dy)*^nz)/(dx*^dy*^dz) by A2,A5,Th46
.= (nx*^dy*^dz+^dx*^ny*^dz+^dx*^dy*^nz)/(dx*^dy*^dz) by ORDINAL3:46
.= (nx*^(dy*^dz)+^dx*^ny*^dz+^dx*^dy*^nz)/(dx*^dy*^dz) by ORDINAL3:50
.= (nx*^(dy*^dz)+^dx*^(ny*^dz)+^dx*^dy*^nz)/(dx*^dy*^dz) by ORDINAL3:50
.= (nx*^(dy*^dz)+^dx*^(ny*^dz)+^dx*^(dy*^nz))/(dx*^dy*^dz) by ORDINAL3:50
.= (nx*^(dy*^dz)+^(dx*^(ny*^dz)+^dx*^(dy*^nz)))/(dx*^dy*^dz) by ORDINAL3:30
.= (nx*^(dy*^dz)+^dx*^(ny*^dz+^dy*^nz))/(dx*^dy*^dz) by ORDINAL3:46
.= (nx*^(dy*^dz)+^dx*^(ny*^dz+^dy*^nz))/(dx*^(dy*^dz)) by ORDINAL3:50
.= (ny*^dz+^dy*^nz)/(dy*^dz)+nx/dx by A4,A3,Th46
.= x+(y+z) by Th39;
end;
theorem Th52:
(x*'y)*'z = x*'(y*'z)
proof
set nx = numerator x, ny = numerator y, nz = numerator z;
set dx = denominator x, dy = denominator y, dz = denominator z;
A1: x = nx/dx by Th39;
z = nz/dz by Th39;
hence (x*'y)*'z = (nx*^ny*^nz)/(dx*^dy*^dz) by Th49
.= (nx*^(ny*^nz))/(dx*^dy*^dz) by ORDINAL3:50
.= (nx*^(ny*^nz))/(dx*^(dy*^dz)) by ORDINAL3:50
.= x*'(y*'z) by A1,Th49;
end;
theorem Th53:
x*'one = x
proof
set y = one;
A1: (numerator x)*^1 = numerator x & (denominator x)*^1 = denominator x by
ORDINAL2:39;
numerator y = 1 & denominator y = 1 by Def8,Def9;
hence thesis by A1,Th39;
end;
theorem Th54:
x <> {} implies ex y st x*'y = 1
proof
set nx = numerator x, dx = denominator x;
A1: dx <> {} by Th35;
assume x <> {};
then
A2: nx <> {} by Th37;
take y = dx/nx;
nx, dx are_coprime by Th34;
then denominator y = nx & numerator y = dx by A2,Th43;
hence thesis by A2,A1,Th41,ORDINAL3:31;
end;
theorem Th55:
x <> {} implies ex z st y = x*'z
proof
reconsider o = one as Element of RAT+;
assume x <> {};
then consider z such that
A1: x*'z = 1 by Th54;
take z*'y;
thus y = y*'o by Th53
.= x*'(z*'y) by A1,Th52;
end;
theorem Th56:
x <> {} & x*'y = x*'z implies y = z
proof
assume x <> {};
then consider r being Element of RAT+ such that
A1: x*'r = 1 by Th54;
r*'(x*'y) = one*'y by A1,Th52;
then
A2: r*'(x*'y) = y by Th53;
r*'(x*'z) = one*'z by A1,Th52;
hence thesis by A2,Th53;
end;
theorem Th57:
x*'(y+z) = x*'y+x*'z
proof
set nx = numerator x, ny = numerator y, nz = numerator z;
set dx = denominator x, dy = denominator y, dz = denominator z;
A1: dx <> {} by Th35;
dz <> {} by Th35;
then
A2: dx*^dz <> {} by A1,ORDINAL3:31;
dy <> {} by Th35;
then
A3: dx*^dy <> {} by A1,ORDINAL3:31;
x = nx/dx by Th39;
hence x*'(y+z) = (nx*^(ny*^dz+^dy*^nz))/(dx*^(dy*^dz)) by Th49
.= (nx*^(ny*^dz)+^nx*^(dy*^nz))/(dx*^(dy*^dz)) by ORDINAL3:46
.= (nx*^ny*^dz+^nx*^(dy*^nz))/(dx*^(dy*^dz)) by ORDINAL3:50
.= (nx*^ny*^dz+^dy*^(nx*^nz))/(dx*^(dy*^dz)) by ORDINAL3:50
.= (nx*^ny*^dz+^dy*^(nx*^nz))/(dy*^(dx*^dz)) by ORDINAL3:50
.= (dx*^((nx*^ny)*^dz+^(dy*^(nx*^nz))))/(dx*^(dy*^(dx*^dz))) by Th35,Th44
.= (dx*^((nx*^ny)*^dz)+^dx*^(dy*^(nx*^nz)))/(dx*^(dy*^(dx*^dz))) by
ORDINAL3:46
.= (dx*^((nx*^ny)*^dz)+^(dx*^dy)*^(nx*^nz))/(dx*^(dy*^(dx*^dz))) by
ORDINAL3:50
.= ((nx*^ny)*^(dx*^dz)+^(dx*^dy)*^(nx*^nz))/(dx*^(dy*^(dx*^dz))) by
ORDINAL3:50
.= ((nx*^ny)*^(dx*^dz)+^(dx*^dy)*^(nx*^nz))/((dx*^dy)*^(dx*^dz)) by
ORDINAL3:50
.= x*'y+x*'z by A2,A3,Th46;
end;
theorem Th58:
for i,j being ordinal Element of RAT+ holds i+j = i+^j
proof
let i,j be ordinal Element of RAT+;
set ni = numerator i, nj = numerator j;
A1: j in omega by ORDINAL1:def 12;
then
A2: denominator j = 1 by Def9;
A3: i in omega by ORDINAL1:def 12;
then denominator i = 1 by Def9;
hence i+j = (ni*^1+^1*^nj)/1 by A2,ORDINAL2:39
.= (ni+^1*^nj)/1 by ORDINAL2:39
.= (ni+^nj)/1 by ORDINAL2:39
.= ni+^nj by Th40
.= i+^nj by A3,Def8
.= i+^j by A1,Def8;
end;
theorem
for i,j being ordinal Element of RAT+ holds i*'j = i*^j
proof
let i,j be ordinal Element of RAT+;
set ni = numerator i, nj = numerator j;
A1: j in omega by ORDINAL1:def 12;
then
A2: denominator j = 1 by Def9;
A3: i in omega by ORDINAL1:def 12;
then denominator i = 1 by Def9;
hence i*'j = (ni*^nj)/1 by A2,ORDINAL2:39
.= ni*^nj by Th40
.= i*^nj by A3,Def8
.= i*^j by A1,Def8;
end;
theorem Th60:
ex y st x = y+y
proof
set O2 = one+one;
O2 = 1+^1 by Th58;
then O2 <> {} by ORDINAL3:26;
then consider z such that
A1: O2*'z = 1 by Th54;
take y = z*'x;
thus x = one*'x by Th53
.= O2*'y by A1,Th52
.= one*'y+one*'y by Th57
.= y+one*'y by Th53
.= y+y by Th53;
end;
definition
let x,y be Element of RAT+;
pred x <=' y means
: Def13:
ex z being Element of RAT+ st y = x+z;
connectedness
proof
let x,y be Element of RAT+;
set nx = numerator x, ny = numerator y;
set dx = denominator x, dy = denominator y;
A1: dx <> {} & dy <> {} by Th35;
A2: nx/dx = x & ny/dy = y by Th39;
nx*^dy c= ny*^dx or ny*^dx c= nx*^dy;
then
A3: ny*^dx = nx*^dy+^(ny*^dx -^ nx*^dy) or nx*^dy = ny*^dx+^(nx*^dy -^ ny
*^dx) by ORDINAL3:def 5;
nx*^dy/(dx*^dy) = nx/dx & ny*^dx/(dx*^dy) = ny/dy by Th35,Th44;
then x = y+((nx*^dy -^ ny*^dx)/(dx*^dy)) or y = x+((ny*^dx -^ nx*^dy)/(dx
*^dy)) by A1,A2,A3,Th47,ORDINAL3:31;
hence thesis;
end;
end;
notation
let x,y be Element of RAT+;
antonym y < x for x <=' y;
end;
reserve r,s,t for Element of RAT+;
theorem
not ex y being object st [{},y] in RAT+
proof
given y being object such that
A1: [{},y] in RAT+;
consider i,j being Element of omega such that
A2: [{},y] = [i,j] and
A3: i,j are_coprime and
j <> {} and
A4: j <> 1 by A1,Th29,Th32;
i = {} by A2,XTUPLE_0:1;
hence thesis by A3,A4,Th3;
end;
theorem Th62:
s + t = r + t implies s = r
proof
assume
A1: s + t = r + t;
set r1 = numerator r, r2 = denominator r;
set t1 = numerator t, t2 = denominator t;
set s1 = numerator s, s2 = denominator s;
A2: t2 <> {} by Th35;
A3: s2 <> {} by Th35;
then
A4: s2*^t2 <> {} by A2,ORDINAL3:31;
A5: r2 <> {} by Th35;
then r2*^t2 <> {} by A2,ORDINAL3:31;
then (s1*^t2+^s2*^t1)*^(r2*^t2) = (r1*^t2+^r2*^t1)*^(s2*^t2) by A1,A4,Th45
.= (r1*^t2+^r2*^t1)*^s2*^t2 by ORDINAL3:50;
then (s1*^t2+^s2*^t1)*^r2*^t2 = (r1*^t2+^r2*^t1)*^s2*^t2 by ORDINAL3:50;
then (s1*^t2+^s2*^t1)*^r2 = (r1*^t2+^r2*^t1)*^s2 by A2,ORDINAL3:33
.= r1*^t2*^s2+^r2*^t1*^s2 by ORDINAL3:46;
then s1*^t2*^r2+^s2*^t1*^r2 = r1*^t2*^s2+^r2*^t1*^s2 by ORDINAL3:46
.= r1*^t2*^s2+^s2*^t1*^r2 by ORDINAL3:50;
then s1*^t2*^r2 = r1*^t2*^s2 by ORDINAL3:21
.= r1*^s2*^t2 by ORDINAL3:50;
then s1*^r2*^t2 = r1*^s2*^t2 by ORDINAL3:50;
then s1*^r2 = r1*^s2 by A2,ORDINAL3:33;
then s1/s2 = r1/r2 by A3,A5,Th45
.= r by Th39;
hence thesis by Th39;
end;
theorem Th63:
r+s = {} implies r = {}
proof
set nr = numerator r, dr = denominator r;
set ns = numerator s, ds = denominator s;
assume
A1: r+s = {};
denominator {} = 1 & numerator {} = {} by Def8,Def9,Lm1;
then
A2: (nr*^ds+^ns*^dr)/(dr*^ds) = {}/1 by A1,Th39;
A3: ds <> {} by Th35;
dr <> {} by Th35;
then dr*^ds <> {} by A3,ORDINAL3:31;
then (nr*^ds+^ns*^dr)*^1 = (dr*^ds)*^{} by A2,Th45,Lm4
.= {} by ORDINAL2:35;
then nr*^ds+^ns*^dr = {} by ORDINAL3:31,Lm4;
then nr*^ds = {} by ORDINAL3:26;
then nr = {} by A3,ORDINAL3:31;
hence thesis by Th37;
end;
theorem Th64:
{} <=' s
proof
take s;
thus thesis by Th50;
end;
theorem
s <=' {} implies s = {}
by Th63;
theorem Th66:
r <=' s & s <=' r implies r = s
proof
given x such that
A1: s = r+x;
given y such that
A2: r = s+y;
r+{} = r by Th50
.= r+(x+y) by A1,A2,Th51;
then x = {} by Th62,Th63;
hence thesis by A1,Th50;
end;
theorem Th67:
r <=' s & s <=' t implies r <=' t
proof
given x such that
A1: s = r+x;
given y such that
A2: t = s+y;
take x+y;
thus thesis by A1,A2,Th51;
end;
theorem
r < s iff r <=' s & r <> s by Th66;
theorem
r < s & s <=' t or r <=' s & s < t implies r < t by Th67;
theorem
r < s & s < t implies r < t by Th67;
theorem Th71:
x in omega & x+y in omega implies y in omega
proof
assume that
A1: x in omega and
A2: x+y in omega;
A3: denominator (x+y) = 1 by A2,Def9;
set nx = numerator x, dx = denominator x;
A4: dx = 1 by A1,Def9;
set ny = numerator y, dy = denominator y;
A5: x+y = numerator (x+y)/denominator (x+y) & (nx*^dy+^ny*^dx)*^1 = nx*^dy+^
ny*^ dx by Th39,ORDINAL2:39;
dy <> {} by Th35;
then dx*^dy <> {} by A4,ORDINAL3:31,Lm4;
then nx*^dy+^ny*^dx = dx*^dy*^numerator (x+y) by A3,A5,Th45,Lm4
.= dy*^numerator (x+y) by A4,ORDINAL2:39;
then nx*^dy+^ny = dy*^numerator (x+y) by A4,ORDINAL2:39;
then ny = (dy*^numerator (x+y))-^nx*^dy by ORDINAL3:52;
then ny = dy*^((numerator (x+y))-^nx) by ORDINAL3:63;
then
A6: dy divides ny;
A7: ny,dy are_coprime by Th34;
for m being natural Ordinal st m divides dy & m divides ny holds m
divides dy;
then dy hcf ny = dy by A6,Def5;
then
A8: dy = 1 by A7,Th20;
y = ny/dy by Th39;
then y = ny by A8,Th40;
hence thesis;
end;
theorem Th72:
for i being ordinal Element of RAT+ st i < x & x < i+one holds not x in omega
proof
let i be ordinal Element of RAT+;
assume that
A1: i < x and
A2: x < i+one and
A3: x in omega;
consider z such that
A4: i+one = x+z by A2,Def13;
i+one = i+^1 by Th58;
then i+one in omega by Th31;
then reconsider z9 = z as Element of omega by A3,A4,Th71;
consider y such that
A5: x = i+y by A1,Def13;
i in omega by Th31;
then reconsider y9 = y as Element of omega by A3,A5,Th71;
i+one = i+(y+z) by A5,A4,Th51;
then 1 = y+z by Th62
.= y9+^z9 by Th58;
then y9 c= 1 by ORDINAL3:24;
then y = {} or y = 1 by ORDINAL3:16;
then i = x or i+one = x by A5,Th50;
hence contradiction by A1,A2;
end;
theorem Th73:
t <> {} implies ex r st r < t & not r in omega
proof
assume
A1: t <> {};
A2: 1+^1 = succ 1 by ORDINAL2:31;
per cases;
suppose
A3: one <=' t;
consider r such that
A4: one = r+r by Th60;
take r;
r <=' one & r <> 1 by A2,A4,Th58;
then r < one by Th66;
hence r < t by A3,Th67;
A5: 1*^1 = 1 by ORDINAL2:39;
assume r in omega;
then
A6: denominator r = 1 by Def9;
then (numerator r)*^denominator r = numerator r by ORDINAL2:39;
then
A7: 1 = (numerator r)+^numerator r by A4,A6,A5,Th40;
then numerator r c= 1 by ORDINAL3:24;
then numerator r = {} or numerator r = 1 by ORDINAL3:16;
hence contradiction by A2,A7,ORDINAL2:27;
end;
suppose
A8: t < one;
consider r such that
A9: t = r+r by Th60;
A10: {} <=' r by Th64;
r <> {} by A1,A9,Th50;
then
A11: {} < r by A10,Th66;
take r;
A12: 1 = {}+one by Th50;
A13: r <=' t by A9;
now
assume r = t;
then t+{} = t+t by A9,Th50;
hence contradiction by A1,Th62;
end;
hence r < t by A13,Th66;
r < one by A8,A13,Th67;
hence thesis by A11,A12,Th72;
end;
end;
theorem
{s: s < t} in RAT+ iff t = {}
proof
hereby
assume
A1: {s: s < t} in RAT+ & t <> {};
then consider r such that
A2: r < t and
A3: not r in omega by Th73;
{} <=' t by Th64;
then {} < t by A1,Th66;
then
A4: {} in {s: s < t};
r in {s: s < t} by A2;
then {s: s < t} in omega implies r is Ordinal;
then ex i,j being Element of omega st {s: s < t} = [i,j] & i,j
are_coprime & j <> {} & j <> 1 by A1,A3,Th29,Th31;
hence contradiction by A4,TARSKI:def 2;
end;
assume
A5: t = {};
{s: s < t} c= {}
proof
let a be object;
assume a in {s: s < t};
then ex s st a = s & s < t;
hence thesis by A5,Th64;
end;
then {s: s < t} = {};
hence thesis;
end;
theorem
for A being Subset of RAT+ st (ex t st t in A & t <> {}) & for r,s st
r in A & s <=' r holds s in A ex r1,r2,r3 being Element of RAT+ st r1 in A & r2
in A & r3 in A & r1 <> r2 & r2 <> r3 & r3 <> r1
proof
let A be Subset of RAT+;
given t such that
A1: t in A and
A2: t <> {};
assume
A3: for r,s st r in A & s <=' r holds s in A;
consider x such that
A4: t = x+x by Th60;
take {}, x, t;
x <=' t by A4;
hence {} in A & x in A & t in A by A1,A3,Th64;
thus {} <> x by A2,A4,Th50;
hereby
assume x = t;
then t+{} = t+t by A4,Th50;
hence contradiction by A2,Th62;
end;
thus thesis by A2;
end;
theorem Th76:
s + t <=' r + t iff s <=' r
proof
thus s + t <=' r + t implies s <=' r
proof
given z such that
A1: r+t = s+t+z;
take z;
r+t = s+z+t by A1,Th51;
hence thesis by Th62;
end;
given z such that
A2: r = s+z;
take z;
thus thesis by A2,Th51;
end;
theorem
s <=' s + t;
theorem
r*'s = {} implies r = {} or s = {}
proof
set nr = numerator r, dr = denominator r;
set ns = numerator s, ds = denominator s;
assume
A1: r*'s = {};
dr <> {} & ds <> {} by Th35;
then
A2: dr*^ds <> {} by ORDINAL3:31;
denominator {} = 1 & numerator {} = {} by Def8,Def9,Lm1;
then (nr*^ns)/(dr*^ds) = {}/1 by A1,Th39;
then (nr*^ns)*^1 = (dr*^ds)*^{} by A2,Th45,Lm4
.= {} by ORDINAL2:35;
then nr*^ns = {} by ORDINAL3:31,Lm4;
then nr = {} or ns = {} by ORDINAL3:31;
hence thesis by Th37;
end;
theorem Th79:
r <=' s *' t implies ex t0 being Element of RAT+ st r = s *' t0 & t0 <=' t
proof
given x such that
A1: s*'t = r+x;
per cases;
suppose
A2: s = {};
take t;
s*'t = {} by A2,Th48;
hence thesis by A1,Th63;
end;
suppose
A3: s <> {};
then consider t1 being Element of RAT+ such that
A4: x = s*'t1 by Th55;
consider t0 being Element of RAT+ such that
A5: r = s*'t0 by A3,Th55;
take t0;
thus r = s*'t0 by A5;
take t1;
s*'t = s*'(t0+t1) by A1,A5,A4,Th57;
hence thesis by A3,Th56;
end;
end;
theorem
t <> {} & s *' t <=' r *' t implies s <=' r
proof
assume that
A1: t <> {} and
A2: s *' t <=' r *' t;
ex x st s*'t = t*'x & x <=' r by A2,Th79;
hence thesis by A1,Th56;
end;
theorem
for r1,r2,s1,s2 being Element of RAT+ st r1+r2 = s1+s2 holds r1 <=' s1
or r2 <=' s2
proof
let r1,r2,s1,s2 be Element of RAT+ such that
A1: r1+r2 = s1+s2;
assume that
A2: s1 < r1 and
A3: s2 < r2;
s1+s2 < r1+s2 by A2,Th76;
hence thesis by A1,A3,Th76;
end;
theorem Th82:
s <=' r implies s *' t <=' r *' t
proof
given x such that
A1: r = s+x;
take x*'t;
thus thesis by A1,Th57;
end;
theorem
for r1,r2,s1,s2 being Element of RAT+ st r1*'r2 = s1*'s2 holds r1 <='
s1 or r2 <=' s2
proof
let r1,r2,s1,s2 be Element of RAT+ such that
A1: r1*'r2 = s1*'s2;
A2: {} <=' s1 by Th64;
assume that
A3: s1 < r1 and
A4: s2 < r2;
s2 <> r2 & s1*'s2 <=' r1*'s2 by A3,A4,Th82;
then s1*'s2 < r1*'s2 by A1,A3,A2,Th56,Th66;
hence thesis by A1,A4,Th82;
end;
theorem
r = {} iff r + s = s
proof
s+{} = s by Th50;
hence thesis by Th62;
end;
theorem
for s1,t1,s2,t2 being Element of RAT+ st s1 + t1 = s2 + t2 & s1 <=' s2
holds t2 <=' t1
proof
let s1,t1,s2,t2 be Element of RAT+ such that
A1: s1 + t1 = s2 + t2;
given x such that
A2: s2 = s1+x;
take x;
s1+t1 = s1+(x+t2) by A1,A2,Th51;
hence thesis by Th62;
end;
theorem Th86:
r <=' s & s <=' r + t implies ex t0 being Element of RAT+ st s =
r + t0 & t0 <=' t
by Th76;
theorem
r <=' s + t implies ex s0,t0 being Element of RAT+ st r = s0 + t0 & s0
<=' s & t0 <=' t
proof
assume
A1: r <=' s + t;
per cases;
suppose
s <=' r;
then
s <=' s & ex t0 being Element of RAT+ st r = s + t0 & t0 <=' t by A1,Th86;
hence thesis;
end;
suppose
A2: r <=' s;
r = r+{} & {} <=' t by Th50,Th64;
hence thesis by A2;
end;
end;
theorem
r < s & r < t implies ex t0 being Element of RAT+ st t0 <=' s & t0 <='
t & r < t0
proof
s <=' t & s <=' s or t <=' s & t <=' t;
hence thesis;
end;
theorem
r <=' s & s <=' t & s <> t implies r <> t by Th66;
theorem
s < r + t & t <> {} implies ex r0,t0 being Element of RAT+ st s = r0 +
t0 & r0 <=' r & t0 <=' t & t0 <> t
proof
assume that
A1: s < r + t and
A2: t <> {};
per cases;
suppose
r <=' s;
then consider t0 being Element of RAT+ such that
A3: s = r + t0 & t0 <=' t by A1,Th86;
take r,t0;
thus thesis by A1,A3;
end;
suppose
A4: s <=' r;
s = s+{} & {} <=' t by Th50,Th64;
hence thesis by A2,A4;
end;
end;
theorem
for A being non empty Subset of RAT+ st A in RAT+ ex s st s in A & for
r st r in A holds r <=' s
proof
let A be non empty Subset of RAT+;
A1: now
given i,j being Element of omega such that
A2: A = [i,j] and
A3: i,j are_coprime and
j <> {} and
A4: j <> 1;
A5: now
assume {i} in omega;
then {} in {i} by ORDINAL3:8;
then {} = i by TARSKI:def 1;
hence contradiction by A3,A4,Th3;
end;
{i} in A by A2,TARSKI:def 2;
then consider i1,j1 being Element of omega such that
A6: {i} = [i1,j1] and
A7: i1,j1 are_coprime and
j1 <> {} and
A8: j1 <> 1 by A5,Th29;
{i1,j1} in {i} by A6,TARSKI:def 2;
then
A9: i = {i1,j1} by TARSKI:def 1;
{i1} in {i} by A6,TARSKI:def 2;
then i = {i1} by TARSKI:def 1;
then j1 in {i1} by A9,TARSKI:def 2;
then
A10: j1 = i1 by TARSKI:def 1;
j1 = j1*^1 by ORDINAL2:39;
hence contradiction by A7,A8,A10;
end;
assume A in RAT+;
then reconsider B = A as Element of omega by A1,Th29;
A11: {} in B by ORDINAL3:8;
now
assume B is limit_ordinal;
then omega c= B by A11,ORDINAL1:def 11;
hence contradiction by ORDINAL1:5;
end;
then consider C such that
A12: B = succ C by ORDINAL1:29;
C in B by A12,ORDINAL1:6;
then reconsider C as ordinal Element of RAT+;
take C;
thus C in A by A12,ORDINAL1:6;
let r;
assume
A13: r in A;
then r in B;
then reconsider r as ordinal Element of RAT+;
C-^r in omega by ORDINAL1:def 12;
then reconsider x = C-^r as ordinal Element of RAT+ by Lm6;
r c= C by A12,A13,ORDINAL1:22;
then C = r+^x by ORDINAL3:def 5
.= r+x by Th58;
hence thesis;
end;
theorem
ex t st r + t = s or s + t = r
proof
r <=' s or s <=' r;
hence thesis;
end;
theorem
r < s implies ex t st r < t & t < s
proof
assume
A1: r < s;
then consider x such that
A2: s = r+x by Def13;
consider y such that
A3: x = y+y by Th60;
take t = r+y;
A4: s = t+y by A2,A3,Th51;
then
A5: t <=' s;
r <=' t;
hence r < t by A1,A4,Th66;
r <> s by A1;
then s <> t by A4,Th62;
hence thesis by A5,Th66;
end;
theorem
ex s st r < s
proof
take s = r+one;
s+{} = s by Th50;
then
A1: r <> s by Th62;
r <=' s;
hence thesis by A1,Th66;
end;
theorem
t <> {} implies ex s st s in omega & r <=' s *' t
proof
set y=((numerator r)*^(((numerator t)*^denominator r)-^1))/denominator r;
A1: denominator r <> {} by Th35;
(denominator t)*^(numerator r) in omega by ORDINAL1:def 12;
then reconsider
s = (denominator t)*^(numerator r) as ordinal Element of RAT+ by Lm6;
assume t <> {};
then numerator t <> {} by Th37;
then {} in (numerator t)*^denominator r by A1,ORDINAL3:8,31;
then one c= (numerator t)*^denominator r by Lm3,ORDINAL1:21;
then (numerator t)*^denominator r = 1+^(((numerator t)*^denominator r)-^ 1)
by ORDINAL3:def 5;
then
s*^((numerator t)*^denominator r) = (denominator t)*^ ((numerator r)*^(1
+^(((numerator t)*^denominator r)-^1))) by ORDINAL3:50
.= (denominator t)*^((numerator r)*^1+^ (numerator r)*^(((numerator t)*^
denominator r)-^1)) by ORDINAL3:46;
then
A2: s*^(numerator t)*^denominator r = (denominator t)*^((numerator r)*^1+^
(numerator r)*^(((numerator t)*^denominator r)-^1)) by ORDINAL3:50;
take s;
thus s in omega by ORDINAL1:def 12;
take y;
denominator t <> {} by Th35;
then
(s*^(numerator t))/denominator t = ((numerator r)*^1+^ (numerator r)*^(
((numerator t)*^denominator r)-^1))/denominator r by A1,A2,Th45
.= (((numerator r)*^1)/denominator r)+y by Th35,Th47
.= ((numerator r)/denominator r)+y by ORDINAL2:39
.= r+y by Th39;
then r+y = (s*^(numerator t))/(1*^denominator t) by ORDINAL2:39
.= (s/1)*'((numerator t)/denominator t) by Th49
.= s*'((numerator t)/denominator t) by Th40;
hence thesis by Th39;
end;
scheme
DisNat { n0,n1,n2() -> Element of RAT+, P[set] }: ex s st s in omega & P[s]
& not P[s + n1()]
provided
A1: n1() = 1 and
A2: n0() = {} and
A3: n2() in omega and
A4: P[n0()] and
A5: not P[n2()]
proof
defpred P1[Ordinal] means not P[$1] & $1 in omega;
A6: ex A st P1[A] by A3,A5;
consider A such that
A7: P1[A] and
A8: for B st P1[B] holds A c= B from ORDINAL1:sch 1(A6);
A9: {} in A by A2,A4,A7,ORDINAL3:8;
now
assume A is limit_ordinal;
then omega c= A by A9,ORDINAL1:def 11;
then A in A by A7;
hence contradiction;
end;
then consider B being Ordinal such that
A10: A = succ B by ORDINAL1:29;
A11: B in A by A10,ORDINAL1:8;
then
A12: B in omega by A7,ORDINAL1:10;
then reconsider s = B as ordinal Element of RAT+ by Lm6;
take s;
thus s in omega & P[s] by A8,A11,A12,ORDINAL1:5;
A = B+^1 by A10,ORDINAL2:31;
hence thesis by A1,A7,Th58;
end;