:: Arithmetic of Non Negative Rational Numbers
:: by Grzegorz Bancerek
::
:: Received March 7, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

Lm1: {} in omega
by ORDINAL1:def 11;

Lm2: 1 in omega
;

definition
func one -> set equals :: ARYTM_3:def 1
1;
correctness
coherence
1 is set
;
;
end;

:: deftheorem defines one ARYTM_3:def 1 :
one = 1;

begin

definition
let a, b be Ordinal;
pred a,b are_relative_prime means :Def2: :: ARYTM_3:def 2
for c, d1, d2 being Ordinal st a = c *^ d1 & b = c *^ d2 holds
c = 1;
symmetry
for a, b being Ordinal st ( for c, d1, d2 being Ordinal st a = c *^ d1 & b = c *^ d2 holds
c = 1 ) holds
for c, d1, d2 being Ordinal st b = c *^ d1 & a = c *^ d2 holds
c = 1
;
end;

:: deftheorem Def2 defines are_relative_prime ARYTM_3:def 2 :
for a, b being Ordinal holds
( a,b are_relative_prime iff for c, d1, d2 being Ordinal st a = c *^ d1 & b = c *^ d2 holds
c = 1 );

theorem :: ARYTM_3:1
not {} , {} are_relative_prime
proof end;

theorem Th2: :: ARYTM_3:2
for A being Ordinal holds 1,A are_relative_prime
proof end;

theorem Th3: :: ARYTM_3:3
for A being Ordinal st {} ,A are_relative_prime holds
A = 1
proof end;

defpred S1[ set ] means ex B being Ordinal st
( B c= $1 & $1 in omega & $1 <> {} & ( for c, d1, d2 being natural Ordinal holds
( not d1,d2 are_relative_prime or not $1 = c *^ d1 or not B = c *^ d2 ) ) );

theorem :: ARYTM_3:4
for a, b being natural Ordinal st ( a <> {} or b <> {} ) holds
ex c, d1, d2 being natural Ordinal st
( d1,d2 are_relative_prime & a = c *^ d1 & b = c *^ d2 )
proof end;

registration
let m, n be natural Ordinal;
cluster m div^ n -> natural ;
coherence
m div^ n is natural
proof end;
cluster m mod^ n -> natural ;
coherence
m mod^ n is natural
proof end;
end;

definition
let k, n be Ordinal;
pred k divides n means :Def3: :: ARYTM_3:def 3
ex a being Ordinal st n = k *^ a;
reflexivity
for k being Ordinal ex a being Ordinal st k = k *^ a
proof end;
end;

:: deftheorem Def3 defines divides ARYTM_3:def 3 :
for k, n being Ordinal holds
( k divides n iff ex a being Ordinal st n = k *^ a );

theorem Th5: :: ARYTM_3:5
for a, b being natural Ordinal holds
( a divides b iff ex c being natural Ordinal st b = a *^ c )
proof end;

theorem Th6: :: ARYTM_3:6
for m, n being natural Ordinal st {} in m holds
n mod^ m in m
proof end;

theorem Th7: :: ARYTM_3:7
for n, m being natural Ordinal holds
( m divides n iff n = m *^ (n div^ m) )
proof end;

theorem Th8: :: ARYTM_3:8
for n, m being natural Ordinal st n divides m & m divides n holds
n = m
proof end;

theorem Th9: :: ARYTM_3:9
for n being natural Ordinal holds
( n divides {} & 1 divides n )
proof end;

theorem Th10: :: ARYTM_3:10
for n, m being natural Ordinal st {} in m & n divides m holds
n c= m
proof end;

theorem Th11: :: ARYTM_3:11
for n, m, l being natural Ordinal st n divides m & n divides m +^ l holds
n divides l
proof end;

Lm3: 1 = succ {}
;

definition
let k, n be natural Ordinal;
func k lcm n -> Element of omega means :Def4: :: ARYTM_3:def 4
( k divides it & n divides it & ( for m being natural Ordinal st k divides m & n divides m holds
it divides m ) );
existence
ex b1 being Element of omega st
( k divides b1 & n divides b1 & ( for m being natural Ordinal st k divides m & n divides m holds
b1 divides m ) )
proof end;
uniqueness
for b1, b2 being Element of omega st k divides b1 & n divides b1 & ( for m being natural Ordinal st k divides m & n divides m holds
b1 divides m ) & k divides b2 & n divides b2 & ( for m being natural Ordinal st k divides m & n divides m holds
b2 divides m ) holds
b1 = b2
proof end;
commutativity
for b1 being Element of omega
for k, n being natural Ordinal st k divides b1 & n divides b1 & ( for m being natural Ordinal st k divides m & n divides m holds
b1 divides m ) holds
( n divides b1 & k divides b1 & ( for m being natural Ordinal st n divides m & k divides m holds
b1 divides m ) )
;
end;

:: deftheorem Def4 defines lcm ARYTM_3:def 4 :
for k, n being natural Ordinal
for b3 being Element of omega holds
( b3 = k lcm n iff ( k divides b3 & n divides b3 & ( for m being natural Ordinal st k divides m & n divides m holds
b3 divides m ) ) );

theorem Th12: :: ARYTM_3:12
for m, n being natural Ordinal holds m lcm n divides m *^ n
proof end;

theorem Th13: :: ARYTM_3:13
for n, m being natural Ordinal st n <> {} holds
(m *^ n) div^ (m lcm n) divides m
proof end;

definition
let k, n be natural Ordinal;
func k hcf n -> Element of omega means :Def5: :: ARYTM_3:def 5
( it divides k & it divides n & ( for m being natural Ordinal st m divides k & m divides n holds
m divides it ) );
existence
ex b1 being Element of omega st
( b1 divides k & b1 divides n & ( for m being natural Ordinal st m divides k & m divides n holds
m divides b1 ) )
proof end;
uniqueness
for b1, b2 being Element of omega st b1 divides k & b1 divides n & ( for m being natural Ordinal st m divides k & m divides n holds
m divides b1 ) & b2 divides k & b2 divides n & ( for m being natural Ordinal st m divides k & m divides n holds
m divides b2 ) holds
b1 = b2
proof end;
commutativity
for b1 being Element of omega
for k, n being natural Ordinal st b1 divides k & b1 divides n & ( for m being natural Ordinal st m divides k & m divides n holds
m divides b1 ) holds
( b1 divides n & b1 divides k & ( for m being natural Ordinal st m divides n & m divides k holds
m divides b1 ) )
;
end;

:: deftheorem Def5 defines hcf ARYTM_3:def 5 :
for k, n being natural Ordinal
for b3 being Element of omega holds
( b3 = k hcf n iff ( b3 divides k & b3 divides n & ( for m being natural Ordinal st m divides k & m divides n holds
m divides b3 ) ) );

theorem Th14: :: ARYTM_3:14
for a being natural Ordinal holds
( a hcf {} = a & a lcm {} = {} )
proof end;

theorem Th15: :: ARYTM_3:15
for a, b being natural Ordinal st a hcf b = {} holds
a = {}
proof end;

theorem Th16: :: ARYTM_3:16
for a being natural Ordinal holds
( a hcf a = a & a lcm a = a )
proof end;

theorem Th17: :: ARYTM_3:17
for a, c, b being natural Ordinal holds (a *^ c) hcf (b *^ c) = (a hcf b) *^ c
proof end;

theorem Th18: :: ARYTM_3:18
for b, a being natural Ordinal st b <> {} holds
( a hcf b <> {} & b div^ (a hcf b) <> {} )
proof end;

theorem Th19: :: ARYTM_3:19
for a, b being natural Ordinal st ( a <> {} or b <> {} ) holds
a div^ (a hcf b),b div^ (a hcf b) are_relative_prime
proof end;

theorem Th20: :: ARYTM_3:20
for a, b being natural Ordinal holds
( a,b are_relative_prime iff a hcf b = 1 )
proof end;

definition
let a, b be natural Ordinal;
func RED (a,b) -> Element of omega equals :: ARYTM_3:def 6
a div^ (a hcf b);
coherence
a div^ (a hcf b) is Element of omega
by ORDINAL1:def 12;
end;

:: deftheorem defines RED ARYTM_3:def 6 :
for a, b being natural Ordinal holds RED (a,b) = a div^ (a hcf b);

theorem Th21: :: ARYTM_3:21
for a, b being natural Ordinal holds (RED (a,b)) *^ (a hcf b) = a
proof end;

theorem :: ARYTM_3:22
for a, b being natural Ordinal st ( a <> {} or b <> {} ) holds
RED (a,b), RED (b,a) are_relative_prime by Th19;

theorem Th23: :: ARYTM_3:23
for a, b being natural Ordinal st a,b are_relative_prime holds
RED (a,b) = a
proof end;

theorem Th24: :: ARYTM_3:24
for a being natural Ordinal holds
( RED (a,1) = a & RED (1,a) = 1 )
proof end;

theorem :: ARYTM_3:25
for b, a being natural Ordinal st b <> {} holds
RED (b,a) <> {} by Th18;

theorem Th26: :: ARYTM_3:26
for a being natural Ordinal holds
( RED ({},a) = {} & ( a <> {} implies RED (a,{}) = 1 ) )
proof end;

theorem Th27: :: ARYTM_3:27
for a being natural Ordinal st a <> {} holds
RED (a,a) = 1
proof end;

theorem Th28: :: ARYTM_3:28
for c, a, b being natural Ordinal st c <> {} holds
RED ((a *^ c),(b *^ c)) = RED (a,b)
proof end;

set RATplus = { [a,b] where a, b is Element of omega : ( a,b are_relative_prime & b <> {} ) } ;

1,1 are_relative_prime
by Th2;

then [1,1] in { [a,b] where a, b is Element of omega : ( a,b are_relative_prime & b <> {} ) }
;

then reconsider RATplus = { [a,b] where a, b is Element of omega : ( a,b are_relative_prime & b <> {} ) } as non empty set ;

Lm4: for a, b being natural Ordinal st [a,b] in RATplus holds
( a,b are_relative_prime & b <> {} )

proof end;

begin

definition
func RAT+ -> set equals :: ARYTM_3:def 7
( { [i,j] where i, j is Element of omega : ( i,j are_relative_prime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega;
correctness
coherence
( { [i,j] where i, j is Element of omega : ( i,j are_relative_prime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega is set
;
;
end;

:: deftheorem defines RAT+ ARYTM_3:def 7 :
RAT+ = ( { [i,j] where i, j is Element of omega : ( i,j are_relative_prime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega;

Lm5: omega c= RAT+
by XBOOLE_1:7;

registration
cluster RAT+ -> non empty ;
coherence
not RAT+ is empty
;
end;

registration
cluster non empty ordinal for Element of RAT+ ;
existence
ex b1 being Element of RAT+ st
( not b1 is empty & b1 is ordinal )
by Lm2, Lm5;
end;

theorem Th29: :: ARYTM_3:29
for x being Element of RAT+ holds
( x in omega or ex i, j being Element of omega st
( x = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 ) )
proof end;

theorem Th30: :: ARYTM_3:30
for i, j being set holds [i,j] is not Ordinal
proof end;

theorem Th31: :: ARYTM_3:31
for A being Ordinal st A in RAT+ holds
A in omega
proof end;

registration
cluster ordinal -> ordinal natural for Element of RAT+ ;
coherence
for b1 being ordinal Element of RAT+ holds b1 is natural
proof end;
end;

theorem Th32: :: ARYTM_3:32
for i, j being set holds not [i,j] in omega
proof end;

theorem Th33: :: ARYTM_3:33
for i, j being Element of omega holds
( [i,j] in RAT+ iff ( i,j are_relative_prime & j <> {} & j <> 1 ) )
proof end;

definition
let x be Element of RAT+ ;
func numerator x -> Element of omega means :Def8: :: ARYTM_3:def 8
it = x if x in omega
otherwise ex a being natural Ordinal st x = [it,a];
existence
( ( x in omega implies ex b1 being Element of omega st b1 = x ) & ( not x in omega implies ex b1 being Element of omega ex a being natural Ordinal st x = [b1,a] ) )
proof end;
correctness
consistency
for b1 being Element of omega holds verum
;
uniqueness
for b1, b2 being Element of omega holds
( ( x in omega & b1 = x & b2 = x implies b1 = b2 ) & ( not x in omega & ex a being natural Ordinal st x = [b1,a] & ex a being natural Ordinal st x = [b2,a] implies b1 = b2 ) )
;
by XTUPLE_0:1;
func denominator x -> Element of omega means :Def9: :: ARYTM_3:def 9
it = 1 if x in omega
otherwise ex a being natural Ordinal st x = [a,it];
existence
( ( x in omega implies ex b1 being Element of omega st b1 = 1 ) & ( not x in omega implies ex b1 being Element of omega ex a being natural Ordinal st x = [a,b1] ) )
proof end;
correctness
consistency
for b1 being Element of omega holds verum
;
uniqueness
for b1, b2 being Element of omega holds
( ( x in omega & b1 = 1 & b2 = 1 implies b1 = b2 ) & ( not x in omega & ex a being natural Ordinal st x = [a,b1] & ex a being natural Ordinal st x = [a,b2] implies b1 = b2 ) )
;
by XTUPLE_0:1;
end;

:: deftheorem Def8 defines numerator ARYTM_3:def 8 :
for x being Element of RAT+
for b2 being Element of omega holds
( ( x in omega implies ( b2 = numerator x iff b2 = x ) ) & ( not x in omega implies ( b2 = numerator x iff ex a being natural Ordinal st x = [b2,a] ) ) );

:: deftheorem Def9 defines denominator ARYTM_3:def 9 :
for x being Element of RAT+
for b2 being Element of omega holds
( ( x in omega implies ( b2 = denominator x iff b2 = 1 ) ) & ( not x in omega implies ( b2 = denominator x iff ex a being natural Ordinal st x = [a,b2] ) ) );

theorem Th34: :: ARYTM_3:34
for x being Element of RAT+ holds numerator x, denominator x are_relative_prime
proof end;

theorem Th35: :: ARYTM_3:35
for x being Element of RAT+ holds denominator x <> {}
proof end;

theorem Th36: :: ARYTM_3:36
for x being Element of RAT+ st not x in omega holds
( x = [(numerator x),(denominator x)] & denominator x <> 1 )
proof end;

theorem Th37: :: ARYTM_3:37
for x being Element of RAT+ holds
( x <> {} iff numerator x <> {} )
proof end;

theorem :: ARYTM_3:38
for x being Element of RAT+ holds
( 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: :: ARYTM_3:def 10
{} if j = {}
RED (i,j) if RED (j,i) = 1
otherwise [(RED (i,j)),(RED (j,i))];
coherence
( ( j = {} implies {} is Element of RAT+ ) & ( RED (j,i) = 1 implies RED (i,j) is Element of RAT+ ) & ( not j = {} & not RED (j,i) = 1 implies [(RED (i,j)),(RED (j,i))] is Element of RAT+ ) )
proof end;
consistency
for b1 being Element of RAT+ st j = {} & RED (j,i) = 1 holds
( b1 = {} iff b1 = RED (i,j) )
by Th26;
end;

:: deftheorem Def10 defines / ARYTM_3:def 10 :
for i, j being natural Ordinal holds
( ( j = {} implies i / j = {} ) & ( RED (j,i) = 1 implies i / j = RED (i,j) ) & ( not j = {} & not RED (j,i) = 1 implies i / j = [(RED (i,j)),(RED (j,i))] ) );

notation
let i, j be natural Ordinal;
synonym quotient (i,j) for i / j;
end;

theorem Th39: :: ARYTM_3:39
for x being Element of RAT+ holds (numerator x) / (denominator x) = x
proof end;

theorem Th40: :: ARYTM_3:40
for b, a being natural Ordinal holds
( {} / b = {} & a / 1 = a )
proof end;

theorem Th41: :: ARYTM_3:41
for a being natural Ordinal st a <> {} holds
a / a = 1
proof end;

theorem Th42: :: ARYTM_3:42
for b, a being natural Ordinal st b <> {} holds
( numerator (a / b) = RED (a,b) & denominator (a / b) = RED (b,a) )
proof end;

theorem Th43: :: ARYTM_3:43
for i, j being Element of omega st i,j are_relative_prime & j <> {} holds
( numerator (i / j) = i & denominator (i / j) = j )
proof end;

theorem Th44: :: ARYTM_3:44
for c, a, b being natural Ordinal st c <> {} holds
(a *^ c) / (b *^ c) = a / b
proof end;

theorem Th45: :: ARYTM_3:45
for l, j, i, k being natural Ordinal st j <> {} & l <> {} holds
( i / j = k / l iff i *^ l = j *^ k )
proof end;

definition
let x, y be Element of RAT+ ;
func x + y -> Element of RAT+ equals :: ARYTM_3:def 11
(((numerator x) *^ (denominator y)) +^ ((numerator y) *^ (denominator x))) / ((denominator x) *^ (denominator y));
coherence
(((numerator x) *^ (denominator y)) +^ ((numerator y) *^ (denominator x))) / ((denominator x) *^ (denominator y)) is Element of RAT+
;
commutativity
for b1, x, y being Element of RAT+ st b1 = (((numerator x) *^ (denominator y)) +^ ((numerator y) *^ (denominator x))) / ((denominator x) *^ (denominator y)) holds
b1 = (((numerator y) *^ (denominator x)) +^ ((numerator x) *^ (denominator y))) / ((denominator y) *^ (denominator x))
;
func x *' y -> Element of RAT+ equals :: ARYTM_3:def 12
((numerator x) *^ (numerator y)) / ((denominator x) *^ (denominator y));
coherence
((numerator x) *^ (numerator y)) / ((denominator x) *^ (denominator y)) is Element of RAT+
;
commutativity
for b1, x, y being Element of RAT+ st b1 = ((numerator x) *^ (numerator y)) / ((denominator x) *^ (denominator y)) holds
b1 = ((numerator y) *^ (numerator x)) / ((denominator y) *^ (denominator x))
;
end;

:: deftheorem defines + ARYTM_3:def 11 :
for x, y being Element of RAT+ holds x + y = (((numerator x) *^ (denominator y)) +^ ((numerator y) *^ (denominator x))) / ((denominator x) *^ (denominator y));

:: deftheorem defines *' ARYTM_3:def 12 :
for x, y being Element of RAT+ holds x *' y = ((numerator x) *^ (numerator y)) / ((denominator x) *^ (denominator y));

theorem Th46: :: ARYTM_3:46
for l, j, i, k being natural Ordinal st j <> {} & l <> {} holds
(i / j) + (k / l) = ((i *^ l) +^ (j *^ k)) / (j *^ l)
proof end;

theorem Th47: :: ARYTM_3:47
for k, i, j being natural Ordinal st k <> {} holds
(i / k) + (j / k) = (i +^ j) / k
proof end;

registration
cluster empty for Element of RAT+ ;
existence
ex b1 being Element of RAT+ st b1 is empty
by Lm1, Lm5;
end;

definition
:: original: {}
redefine func {} -> Element of RAT+ ;
coherence
{} is Element of RAT+
by Lm1, Lm5;
:: original: one
redefine func one -> non empty ordinal Element of RAT+ ;
coherence
one is non empty ordinal Element of RAT+
by Lm2, Lm5;
end;

theorem Th48: :: ARYTM_3:48
for x being Element of RAT+ holds x *' {} = {}
proof end;

theorem Th49: :: ARYTM_3:49
for l, i, j, k being natural Ordinal holds (i / j) *' (k / l) = (i *^ k) / (j *^ l)
proof end;

theorem Th50: :: ARYTM_3:50
for x being Element of RAT+ holds x + {} = x
proof end;

theorem Th51: :: ARYTM_3:51
for x, y, z being Element of RAT+ holds (x + y) + z = x + (y + z)
proof end;

theorem Th52: :: ARYTM_3:52
for x, y, z being Element of RAT+ holds (x *' y) *' z = x *' (y *' z)
proof end;

theorem Th53: :: ARYTM_3:53
for x being Element of RAT+ holds x *' one = x
proof end;

theorem Th54: :: ARYTM_3:54
for x being Element of RAT+ st x <> {} holds
ex y being Element of RAT+ st x *' y = 1
proof end;

theorem Th55: :: ARYTM_3:55
for x, y being Element of RAT+ st x <> {} holds
ex z being Element of RAT+ st y = x *' z
proof end;

theorem Th56: :: ARYTM_3:56
for x, y, z being Element of RAT+ st x <> {} & x *' y = x *' z holds
y = z
proof end;

theorem Th57: :: ARYTM_3:57
for x, y, z being Element of RAT+ holds x *' (y + z) = (x *' y) + (x *' z)
proof end;

theorem Th58: :: ARYTM_3:58
for i, j being ordinal Element of RAT+ holds i + j = i +^ j
proof end;

theorem :: ARYTM_3:59
for i, j being ordinal Element of RAT+ holds i *' j = i *^ j
proof end;

theorem Th60: :: ARYTM_3:60
for x being Element of RAT+ ex y being Element of RAT+ st x = y + y
proof end;

definition
let x, y be Element of RAT+ ;
pred x <=' y means :Def13: :: ARYTM_3:def 13
ex z being Element of RAT+ st y = x + z;
connectedness
for x, y being Element of RAT+ st ( for z being Element of RAT+ holds not y = x + z ) holds
ex z being Element of RAT+ st x = y + z
proof end;
end;

:: deftheorem Def13 defines <=' ARYTM_3:def 13 :
for x, y being Element of RAT+ holds
( x <=' y iff ex z being Element of RAT+ st y = x + z );

notation
let x, y be Element of RAT+ ;
antonym y < x for x <=' y;
end;

theorem :: ARYTM_3:61
for y being set holds not [{},y] in RAT+
proof end;

theorem Th62: :: ARYTM_3:62
for s, t, r being Element of RAT+ st s + t = r + t holds
s = r
proof end;

theorem Th63: :: ARYTM_3:63
for r, s being Element of RAT+ st r + s = {} holds
r = {}
proof end;

theorem Th64: :: ARYTM_3:64
for s being Element of RAT+ holds {} <=' s
proof end;

theorem :: ARYTM_3:65
for s being Element of RAT+ st s <=' {} holds
s = {}
proof end;

theorem Th66: :: ARYTM_3:66
for r, s being Element of RAT+ st r <=' s & s <=' r holds
r = s
proof end;

theorem Th67: :: ARYTM_3:67
for r, s, t being Element of RAT+ st r <=' s & s <=' t holds
r <=' t
proof end;

theorem :: ARYTM_3:68
for r, s being Element of RAT+ holds
( r < s iff ( r <=' s & r <> s ) ) by Th66;

theorem :: ARYTM_3:69
for r, s, t being Element of RAT+ st ( ( r < s & s <=' t ) or ( r <=' s & s < t ) ) holds
r < t by Th67;

theorem :: ARYTM_3:70
for r, s, t being Element of RAT+ st r < s & s < t holds
r < t by Th67;

theorem Th71: :: ARYTM_3:71
for x, y being Element of RAT+ st x in omega & x + y in omega holds
y in omega
proof end;

theorem Th72: :: ARYTM_3:72
for x being Element of RAT+
for i being ordinal Element of RAT+ st i < x & x < i + one holds
not x in omega
proof end;

theorem Th73: :: ARYTM_3:73
for t being Element of RAT+ st t <> {} holds
ex r being Element of RAT+ st
( r < t & not r in omega )
proof end;

theorem :: ARYTM_3:74
for t being Element of RAT+ holds
( { s where s is Element of RAT+ : s < t } in RAT+ iff t = {} )
proof end;

theorem :: ARYTM_3:75
for A being Subset of RAT+ st ex t being Element of RAT+ st
( t in A & t <> {} ) & ( for r, s being Element of RAT+ st r in A & s <=' r holds
s in A ) holds
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 end;

theorem Th76: :: ARYTM_3:76
for s, t, r being Element of RAT+ holds
( s + t <=' r + t iff s <=' r )
proof end;

theorem :: ARYTM_3:77
for s, t being Element of RAT+ holds s <=' s + t
proof end;

theorem :: ARYTM_3:78
for r, s being Element of RAT+ holds
( not r *' s = {} or r = {} or s = {} )
proof end;

theorem Th79: :: ARYTM_3:79
for r, s, t being Element of RAT+ st r <=' s *' t holds
ex t0 being Element of RAT+ st
( r = s *' t0 & t0 <=' t )
proof end;

theorem :: ARYTM_3:80
for t, s, r being Element of RAT+ st t <> {} & s *' t <=' r *' t holds
s <=' r
proof end;

theorem :: ARYTM_3:81
for r1, r2, s1, s2 being Element of RAT+ holds
( not r1 + r2 = s1 + s2 or r1 <=' s1 or r2 <=' s2 )
proof end;

theorem Th82: :: ARYTM_3:82
for s, r, t being Element of RAT+ st s <=' r holds
s *' t <=' r *' t
proof end;

theorem :: ARYTM_3:83
for r1, r2, s1, s2 being Element of RAT+ holds
( not r1 *' r2 = s1 *' s2 or r1 <=' s1 or r2 <=' s2 )
proof end;

theorem :: ARYTM_3:84
for r, s being Element of RAT+ holds
( r = {} iff r + s = s )
proof end;

theorem :: ARYTM_3:85
for s1, t1, s2, t2 being Element of RAT+ st s1 + t1 = s2 + t2 & s1 <=' s2 holds
t2 <=' t1
proof end;

theorem Th86: :: ARYTM_3:86
for r, s, t being Element of RAT+ st r <=' s & s <=' r + t holds
ex t0 being Element of RAT+ st
( s = r + t0 & t0 <=' t )
proof end;

theorem :: ARYTM_3:87
for r, s, t being Element of RAT+ st r <=' s + t holds
ex s0, t0 being Element of RAT+ st
( r = s0 + t0 & s0 <=' s & t0 <=' t )
proof end;

theorem :: ARYTM_3:88
for r, s, t being Element of RAT+ st r < s & r < t holds
ex t0 being Element of RAT+ st
( t0 <=' s & t0 <=' t & r < t0 )
proof end;

theorem :: ARYTM_3:89
for r, s, t being Element of RAT+ st r <=' s & s <=' t & s <> t holds
r <> t by Th66;

theorem :: ARYTM_3:90
for s, r, t being Element of RAT+ st s < r + t & t <> {} holds
ex r0, t0 being Element of RAT+ st
( s = r0 + t0 & r0 <=' r & t0 <=' t & t0 <> t )
proof end;

theorem :: ARYTM_3:91
for A being non empty Subset of RAT+ st A in RAT+ holds
ex s being Element of RAT+ st
( s in A & ( for r being Element of RAT+ st r in A holds
r <=' s ) )
proof end;

theorem :: ARYTM_3:92
for r, s being Element of RAT+ ex t being Element of RAT+ st
( r + t = s or s + t = r )
proof end;

theorem :: ARYTM_3:93
for r, s being Element of RAT+ st r < s holds
ex t being Element of RAT+ st
( r < t & t < s )
proof end;

theorem :: ARYTM_3:94
for r being Element of RAT+ ex s being Element of RAT+ st r < s
proof end;

theorem :: ARYTM_3:95
for t, r being Element of RAT+ st t <> {} holds
ex s being Element of RAT+ st
( s in omega & r <=' s *' t )
proof end;

scheme :: ARYTM_3:sch 1
DisNat{ F1() -> Element of RAT+ , F2() -> Element of RAT+ , F3() -> Element of RAT+ , P1[ set ] } :
ex s being Element of RAT+ st
( s in omega & P1[s] & P1[s + F2()] )
provided
A1: F2() = 1 and
A2: F1() = {} and
A3: F3() in omega and
A4: P1[F1()] and
A5: P1[F3()]
proof end;