:: 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; preda,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 proofend; theorem Th2: :: ARYTM_3:2 for A being Ordinal holds 1,A are_relative_prime proofend; theorem Th3: :: ARYTM_3:3 for A being Ordinal st {} ,A are_relative_prime holds A = 1 proofend; 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 ) proofend; registration let m, n be natural Ordinal; clusterm div^ n -> natural ; coherence m div^ n is natural proofend; clusterm mod^ n -> natural ; coherence m mod^ n is natural proofend; end; definition let k, n be Ordinal; predk 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 proofend; 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 ) proofend; theorem Th6: :: ARYTM_3:6 for m, n being natural Ordinal st {} in m holds n mod^ m in m proofend; theorem Th7: :: ARYTM_3:7 for n, m being natural Ordinal holds ( m divides n iff n = m *^ (n div^ m) ) proofend; theorem Th8: :: ARYTM_3:8 for n, m being natural Ordinal st n divides m & m divides n holds n = m proofend; theorem Th9: :: ARYTM_3:9 for n being natural Ordinal holds ( n divides {} & 1 divides n ) proofend; theorem Th10: :: ARYTM_3:10 for n, m being natural Ordinal st {} in m & n divides m holds n c= m proofend; theorem Th11: :: ARYTM_3:11 for n, m, l being natural Ordinal st n divides m & n divides m +^ l holds n divides l proofend; Lm3: 1 = succ {} ; definition let k, n be natural Ordinal; funck 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 ) ) proofend; 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 proofend; 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 proofend; theorem Th13: :: ARYTM_3:13 for n, m being natural Ordinal st n <> {} holds (m *^ n) div^ (m lcm n) divides m proofend; definition let k, n be natural Ordinal; funck 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 ) ) proofend; 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 proofend; 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 {} = {} ) proofend; theorem Th15: :: ARYTM_3:15 for a, b being natural Ordinal st a hcf b = {} holds a = {} proofend; theorem Th16: :: ARYTM_3:16 for a being natural Ordinal holds ( a hcf a = a & a lcm a = a ) proofend; theorem Th17: :: ARYTM_3:17 for a, c, b being natural Ordinal holds (a *^ c) hcf (b *^ c) = (a hcf b) *^ c proofend; theorem Th18: :: ARYTM_3:18 for b, a being natural Ordinal st b <> {} holds ( a hcf b <> {} & b div^ (a hcf b) <> {} ) proofend; 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 proofend; theorem Th20: :: ARYTM_3:20 for a, b being natural Ordinal holds ( a,b are_relative_prime iff a hcf b = 1 ) proofend; 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 proofend; 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 proofend; theorem Th24: :: ARYTM_3:24 for a being natural Ordinal holds ( RED (a,1) = a & RED (1,a) = 1 ) proofend; 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 ) ) proofend; theorem Th27: :: ARYTM_3:27 for a being natural Ordinal st a <> {} holds RED (a,a) = 1 proofend; theorem Th28: :: ARYTM_3:28 for c, a, b being natural Ordinal st c <> {} holds RED ((a *^ c),(b *^ c)) = RED (a,b) proofend; 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 <> {} ) proofend; 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 ) ) proofend; theorem Th30: :: ARYTM_3:30 for i, j being set holds [i,j] is not Ordinal proofend; theorem Th31: :: ARYTM_3:31 for A being Ordinal st A in RAT+ holds A in omega proofend; registration cluster ordinal -> ordinal natural for Element of RAT+ ; coherence for b1 being ordinal Element of RAT+ holds b1 is natural proofend; end; theorem Th32: :: ARYTM_3:32 for i, j being set holds not [i,j] in omega proofend; 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 ) ) proofend; 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] ) ) proofend; 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] ) ) proofend; 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 proofend; theorem Th35: :: ARYTM_3:35 for x being Element of RAT+ holds denominator x <> {} proofend; 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 ) proofend; theorem Th37: :: ARYTM_3:37 for x being Element of RAT+ holds ( x <> {} iff numerator x <> {} ) proofend; 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; funci / 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+ ) ) proofend; 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 proofend; theorem Th40: :: ARYTM_3:40 for b, a being natural Ordinal holds ( {} / b = {} & a / 1 = a ) proofend; theorem Th41: :: ARYTM_3:41 for a being natural Ordinal st a <> {} holds a / a = 1 proofend; 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) ) proofend; 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 ) proofend; theorem Th44: :: ARYTM_3:44 for c, a, b being natural Ordinal st c <> {} holds (a *^ c) / (b *^ c) = a / b proofend; 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 ) proofend; definition let x, y be Element of RAT+ ; funcx + 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)) ; funcx *' 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) proofend; theorem Th47: :: ARYTM_3:47 for k, i, j being natural Ordinal st k <> {} holds (i / k) + (j / k) = (i +^ j) / k proofend; 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 *' {} = {} proofend; theorem Th49: :: ARYTM_3:49 for l, i, j, k being natural Ordinal holds (i / j) *' (k / l) = (i *^ k) / (j *^ l) proofend; theorem Th50: :: ARYTM_3:50 for x being Element of RAT+ holds x + {} = x proofend; theorem Th51: :: ARYTM_3:51 for x, y, z being Element of RAT+ holds (x + y) + z = x + (y + z) proofend; theorem Th52: :: ARYTM_3:52 for x, y, z being Element of RAT+ holds (x *' y) *' z = x *' (y *' z) proofend; theorem Th53: :: ARYTM_3:53 for x being Element of RAT+ holds x *' one = x proofend; theorem Th54: :: ARYTM_3:54 for x being Element of RAT+ st x <> {} holds ex y being Element of RAT+ st x *' y = 1 proofend; 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 proofend; theorem Th56: :: ARYTM_3:56 for x, y, z being Element of RAT+ st x <> {} & x *' y = x *' z holds y = z proofend; theorem Th57: :: ARYTM_3:57 for x, y, z being Element of RAT+ holds x *' (y + z) = (x *' y) + (x *' z) proofend; theorem Th58: :: ARYTM_3:58 for i, j being ordinal Element of RAT+ holds i + j = i +^ j proofend; theorem :: ARYTM_3:59 for i, j being ordinal Element of RAT+ holds i *' j = i *^ j proofend; theorem Th60: :: ARYTM_3:60 for x being Element of RAT+ ex y being Element of RAT+ st x = y + y proofend; definition let x, y be Element of RAT+ ; predx <=' 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 proofend; 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+ proofend; theorem Th62: :: ARYTM_3:62 for s, t, r being Element of RAT+ st s + t = r + t holds s = r proofend; theorem Th63: :: ARYTM_3:63 for r, s being Element of RAT+ st r + s = {} holds r = {} proofend; theorem Th64: :: ARYTM_3:64 for s being Element of RAT+ holds {} <=' s proofend; theorem :: ARYTM_3:65 for s being Element of RAT+ st s <=' {} holds s = {} proofend; theorem Th66: :: ARYTM_3:66 for r, s being Element of RAT+ st r <=' s & s <=' r holds r = s proofend; theorem Th67: :: ARYTM_3:67 for r, s, t being Element of RAT+ st r <=' s & s <=' t holds r <=' t proofend; 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 proofend; 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 proofend; 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 ) proofend; theorem :: ARYTM_3:74 for t being Element of RAT+ holds ( { s where s is Element of RAT+ : s < t } in RAT+ iff t = {} ) proofend; 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 ) proofend; theorem Th76: :: ARYTM_3:76 for s, t, r being Element of RAT+ holds ( s + t <=' r + t iff s <=' r ) proofend; theorem :: ARYTM_3:77 for s, t being Element of RAT+ holds s <=' s + t proofend; theorem :: ARYTM_3:78 for r, s being Element of RAT+ holds ( not r *' s = {} or r = {} or s = {} ) proofend; 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 ) proofend; theorem :: ARYTM_3:80 for t, s, r being Element of RAT+ st t <> {} & s *' t <=' r *' t holds s <=' r proofend; 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 ) proofend; theorem Th82: :: ARYTM_3:82 for s, r, t being Element of RAT+ st s <=' r holds s *' t <=' r *' t proofend; 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 ) proofend; theorem :: ARYTM_3:84 for r, s being Element of RAT+ holds ( r = {} iff r + s = s ) proofend; theorem :: ARYTM_3:85 for s1, t1, s2, t2 being Element of RAT+ st s1 + t1 = s2 + t2 & s1 <=' s2 holds t2 <=' t1 proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) ) proofend; 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 ) proofend; 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 ) proofend; theorem :: ARYTM_3:94 for r being Element of RAT+ ex s being Element of RAT+ st r < s proofend; 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 ) proofend; 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()] proofend;