:: by Grzegorz Bancerek

::

:: Received March 7, 1998

:: Copyright (c) 1998 Association of Mizar Users

begin

Lm1: {} in omega

by ORDINAL1:def 12;

Lm2: 1 in omega

;

:: 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;
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 ;

:: 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

canceled;

theorem :: ARYTM_3:2

canceled;

theorem :: ARYTM_3:3

canceled;

theorem :: ARYTM_3:4

canceled;

theorem :: ARYTM_3:5

proof end;

theorem Th6: :: ARYTM_3:6

for A being Ordinal holds 1,A are_relative_prime

proof end;

theorem Th7: :: ARYTM_3:7

proof end;

defpred S

( 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:8

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 )

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

coherence

m mod^ n is natural

end;
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;

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

end;
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;

:: 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 Th9: :: ARYTM_3:9

proof end;

theorem Th10: :: ARYTM_3:10

proof end;

theorem Th11: :: ARYTM_3:11

proof end;

theorem :: ARYTM_3:12

canceled;

theorem Th13: :: ARYTM_3:13

proof end;

theorem Th14: :: ARYTM_3:14

proof end;

theorem Th15: :: ARYTM_3:15

proof end;

theorem Th16: :: ARYTM_3:16

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 b_{1} being Element of omega st

( k divides b_{1} & n divides b_{1} & ( for m being natural Ordinal st k divides m & n divides m holds

b_{1} divides m ) )

for b_{1}, b_{2} being Element of omega st k divides b_{1} & n divides b_{1} & ( for m being natural Ordinal st k divides m & n divides m holds

b_{1} divides m ) & k divides b_{2} & n divides b_{2} & ( for m being natural Ordinal st k divides m & n divides m holds

b_{2} divides m ) holds

b_{1} = b_{2}

for b_{1} being Element of omega

for k, n being natural Ordinal st k divides b_{1} & n divides b_{1} & ( for m being natural Ordinal st k divides m & n divides m holds

b_{1} divides m ) holds

( n divides b_{1} & k divides b_{1} & ( for m being natural Ordinal st n divides m & k divides m holds

b_{1} divides m ) )
;

end;
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 b

( k divides b

b

proof end;

uniqueness for b

b

b

b

proof end;

commutativity for b

for k, n being natural Ordinal st k divides b

b

( n divides b

b

:: deftheorem Def4 defines lcm ARYTM_3:def 4 :

for k, n being natural Ordinal

for b

( b

b

theorem Th17: :: ARYTM_3:17

proof end;

theorem Th18: :: ARYTM_3:18

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 b_{1} being Element of omega st

( b_{1} divides k & b_{1} divides n & ( for m being natural Ordinal st m divides k & m divides n holds

m divides b_{1} ) )

for b_{1}, b_{2} being Element of omega st b_{1} divides k & b_{1} divides n & ( for m being natural Ordinal st m divides k & m divides n holds

m divides b_{1} ) & b_{2} divides k & b_{2} divides n & ( for m being natural Ordinal st m divides k & m divides n holds

m divides b_{2} ) holds

b_{1} = b_{2}

for b_{1} being Element of omega

for k, n being natural Ordinal st b_{1} divides k & b_{1} divides n & ( for m being natural Ordinal st m divides k & m divides n holds

m divides b_{1} ) holds

( b_{1} divides n & b_{1} divides k & ( for m being natural Ordinal st m divides n & m divides k holds

m divides b_{1} ) )
;

end;
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 b

( b

m divides b

proof end;

uniqueness for b

m divides b

m divides b

b

proof end;

commutativity for b

for k, n being natural Ordinal st b

m divides b

( b

m divides b

:: deftheorem Def5 defines hcf ARYTM_3:def 5 :

for k, n being natural Ordinal

for b

( b

m divides b

theorem Th19: :: ARYTM_3:19

proof end;

theorem Th20: :: ARYTM_3:20

proof end;

theorem Th21: :: ARYTM_3:21

proof end;

theorem Th22: :: ARYTM_3:22

proof end;

theorem Th23: :: ARYTM_3:23

proof end;

theorem Th24: :: ARYTM_3:24

for a, b being natural Ordinal st ( a <> {} or b <> {} ) holds

a div^ (a hcf b),b div^ (a hcf b) are_relative_prime

a div^ (a hcf b),b div^ (a hcf b) are_relative_prime

proof end;

theorem Th25: :: ARYTM_3:25

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 13;

end;
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 13;

:: deftheorem defines RED ARYTM_3:def 6 :

for a, b being natural Ordinal holds RED (a,b) = a div^ (a hcf b);

theorem Th26: :: ARYTM_3:26

proof end;

theorem :: ARYTM_3:27

for a, b being natural Ordinal st ( a <> {} or b <> {} ) holds

RED (a,b), RED (b,a) are_relative_prime by Th24;

RED (a,b), RED (b,a) are_relative_prime by Th24;

theorem Th28: :: ARYTM_3:28

proof end;

theorem Th29: :: ARYTM_3:29

proof end;

theorem :: ARYTM_3:30

theorem Th31: :: ARYTM_3:31

proof end;

theorem Th32: :: ARYTM_3:32

proof end;

theorem Th33: :: ARYTM_3:33

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 Th6;

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;
( { [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 ;

;

:: 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 non empty ordinal Element of RAT+ ;

existence

ex b_{1} being Element of RAT+ st

( not b_{1} is empty & b_{1} is ordinal )
by Lm2, Lm5;

end;
existence

ex b

( not b

theorem :: ARYTM_3:34

canceled;

theorem Th35: :: ARYTM_3:35

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 ) )

( 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 Th36: :: ARYTM_3:36

proof end;

theorem Th37: :: ARYTM_3:37

proof end;

registration

cluster ordinal -> ordinal natural Element of RAT+ ;

coherence

for b_{1} being ordinal Element of RAT+ holds b_{1} is natural

end;
coherence

for b

proof end;

theorem Th38: :: ARYTM_3:38

proof end;

theorem Th39: :: ARYTM_3:39

for i, j being Element of omega holds

( [i,j] in RAT+ iff ( i,j are_relative_prime & j <> {} & j <> 1 ) )

( [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 b_{1} being Element of omega st b_{1} = x ) & ( not x in omega implies ex b_{1} being Element of omega ex a being natural Ordinal st x = [b_{1},a] ) )

consistency

for b_{1} being Element of omega holds verum;

uniqueness

for b_{1}, b_{2} being Element of omega holds

( ( x in omega & b_{1} = x & b_{2} = x implies b_{1} = b_{2} ) & ( not x in omega & ex a being natural Ordinal st x = [b_{1},a] & ex a being natural Ordinal st x = [b_{2},a] implies b_{1} = b_{2} ) );

by ZFMISC_1:33;

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 b_{1} being Element of omega st b_{1} = 1 ) & ( not x in omega implies ex b_{1} being Element of omega ex a being natural Ordinal st x = [a,b_{1}] ) )

consistency

for b_{1} being Element of omega holds verum;

uniqueness

for b_{1}, b_{2} being Element of omega holds

( ( x in omega & b_{1} = 1 & b_{2} = 1 implies b_{1} = b_{2} ) & ( not x in omega & ex a being natural Ordinal st x = [a,b_{1}] & ex a being natural Ordinal st x = [a,b_{2}] implies b_{1} = b_{2} ) );

by ZFMISC_1:33;

end;
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 b

proof end;

correctness consistency

for b

uniqueness

for b

( ( x in omega & b

by ZFMISC_1:33;

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 b

proof end;

correctness consistency

for b

uniqueness

for b

( ( x in omega & b

by ZFMISC_1:33;

:: deftheorem Def8 defines numerator ARYTM_3:def 8 :

for x being Element of RAT+

for b

( ( x in omega implies ( b

:: deftheorem Def9 defines denominator ARYTM_3:def 9 :

for x being Element of RAT+

for b

( ( x in omega implies ( b

theorem Th40: :: ARYTM_3:40

proof end;

theorem Th41: :: ARYTM_3:41

proof end;

theorem Th42: :: ARYTM_3:42

for x being Element of RAT+ st not x in omega holds

( x = [(numerator x),(denominator x)] & denominator x <> 1 )

( x = [(numerator x),(denominator x)] & denominator x <> 1 )

proof end;

theorem Th43: :: ARYTM_3:43

proof end;

theorem :: ARYTM_3:44

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+ ) )

for b_{1} being Element of RAT+ st j = {} & RED (j,i) = 1 holds

( b_{1} = {} iff b_{1} = RED (i,j) )
by Th31;

end;
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 b

( b

:: 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))] ) );

theorem Th45: :: ARYTM_3:45

proof end;

theorem Th46: :: ARYTM_3:46

proof end;

theorem Th47: :: ARYTM_3:47

proof end;

theorem Th48: :: ARYTM_3:48

for b, a being natural Ordinal st b <> {} holds

( numerator (a / b) = RED (a,b) & denominator (a / b) = RED (b,a) )

( numerator (a / b) = RED (a,b) & denominator (a / b) = RED (b,a) )

proof end;

theorem Th49: :: ARYTM_3:49

for i, j being Element of omega st i,j are_relative_prime & j <> {} holds

( numerator (i / j) = i & denominator (i / j) = j )

( numerator (i / j) = i & denominator (i / j) = j )

proof end;

theorem Th50: :: ARYTM_3:50

proof end;

theorem Th51: :: ARYTM_3:51

for l, j, i, k being natural Ordinal st j <> {} & l <> {} holds

( i / j = k / l iff i *^ l = j *^ k )

( 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 b_{1}, x, y being Element of RAT+ st b_{1} = (((numerator x) *^ (denominator y)) +^ ((numerator y) *^ (denominator x))) / ((denominator x) *^ (denominator y)) holds

b_{1} = (((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 b_{1}, x, y being Element of RAT+ st b_{1} = ((numerator x) *^ (numerator y)) / ((denominator x) *^ (denominator y)) holds

b_{1} = ((numerator y) *^ (numerator x)) / ((denominator y) *^ (denominator x))
;

end;
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 b

b

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 b

b

:: 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 Th52: :: ARYTM_3:52

for l, j, i, k being natural Ordinal st j <> {} & l <> {} holds

(i / j) + (k / l) = ((i *^ l) +^ (j *^ k)) / (j *^ l)

(i / j) + (k / l) = ((i *^ l) +^ (j *^ k)) / (j *^ l)

proof end;

theorem Th53: :: ARYTM_3:53

proof end;

registration

cluster empty Element of RAT+ ;

existence

ex b_{1} being Element of RAT+ st b_{1} is empty
by Lm1, Lm5;

end;
existence

ex b

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;
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;

theorem Th54: :: ARYTM_3:54

proof end;

theorem Th55: :: ARYTM_3:55

proof end;

theorem Th56: :: ARYTM_3:56

proof end;

theorem Th57: :: ARYTM_3:57

proof end;

theorem Th58: :: ARYTM_3:58

proof end;

theorem Th59: :: ARYTM_3:59

proof end;

theorem Th60: :: ARYTM_3:60

proof end;

theorem Th61: :: ARYTM_3:61

proof end;

theorem Th62: :: ARYTM_3:62

proof end;

theorem Th63: :: ARYTM_3:63

proof end;

theorem Th64: :: ARYTM_3:64

proof end;

theorem :: ARYTM_3:65

proof end;

theorem Th66: :: ARYTM_3:66

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

end;
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;

:: 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 );

theorem :: ARYTM_3:67

canceled;

theorem :: ARYTM_3:68

proof end;

theorem Th69: :: ARYTM_3:69

proof end;

theorem Th70: :: ARYTM_3:70

proof end;

theorem Th71: :: ARYTM_3:71

proof end;

theorem :: ARYTM_3:72

proof end;

theorem Th73: :: ARYTM_3:73

proof end;

theorem Th74: :: ARYTM_3:74

proof end;

theorem :: ARYTM_3:75

theorem :: ARYTM_3:76

for r, s, t being Element of RAT+ st ( ( r < s & s <=' t ) or ( r <=' s & s < t ) ) holds

r < t by Th74;

r < t by Th74;

theorem :: ARYTM_3:77

theorem Th78: :: ARYTM_3:78

proof end;

theorem Th79: :: ARYTM_3:79

for x being Element of RAT+

for i being ordinal Element of RAT+ st i < x & x < i + one holds

not x in omega

for i being ordinal Element of RAT+ st i < x & x < i + one holds

not x in omega

proof end;

theorem Th80: :: ARYTM_3:80

for t being Element of RAT+ st t <> {} holds

ex r being Element of RAT+ st

( r < t & not r in omega )

ex r being Element of RAT+ st

( r < t & not r in omega )

proof end;

theorem :: ARYTM_3:81

proof end;

theorem :: ARYTM_3:82

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 )

( 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 Th83: :: ARYTM_3:83

proof end;

theorem :: ARYTM_3:84

canceled;

theorem :: ARYTM_3:85

proof end;

theorem :: ARYTM_3:86

proof end;

theorem Th87: :: ARYTM_3:87

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 )

ex t0 being Element of RAT+ st

( r = s *' t0 & t0 <=' t )

proof end;

theorem :: ARYTM_3:88

proof end;

theorem :: ARYTM_3:89

proof end;

theorem Th90: :: ARYTM_3:90

proof end;

theorem :: ARYTM_3:91

for r1, r2, s1, s2 being Element of RAT+ holds

( not r1 *' r2 = s1 *' s2 or r1 <=' s1 or r2 <=' s2 )

( not r1 *' r2 = s1 *' s2 or r1 <=' s1 or r2 <=' s2 )

proof end;

theorem :: ARYTM_3:92

proof end;

theorem :: ARYTM_3:93

proof end;

theorem Th94: :: ARYTM_3:94

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 )

ex t0 being Element of RAT+ st

( s = r + t0 & t0 <=' t )

proof end;

theorem :: ARYTM_3:95

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 )

ex s0, t0 being Element of RAT+ st

( r = s0 + t0 & s0 <=' s & t0 <=' t )

proof end;

theorem :: ARYTM_3:96

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 )

ex t0 being Element of RAT+ st

( t0 <=' s & t0 <=' t & r < t0 )

proof end;

theorem :: ARYTM_3:97

theorem :: ARYTM_3:98

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 )

ex r0, t0 being Element of RAT+ st

( s = r0 + t0 & r0 <=' r & t0 <=' t & t0 <> t )

proof end;

theorem :: ARYTM_3:99

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 ) )

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:100

proof end;

theorem :: ARYTM_3:101

proof end;

theorem :: ARYTM_3:102

proof end;

theorem :: ARYTM_3:103

for t, r being Element of RAT+ st t <> {} holds

ex s being Element of RAT+ st

( s in omega & r <=' s *' t )

ex s being Element of RAT+ st

( s in omega & r <=' s *' t )

proof end;

scheme :: ARYTM_3:sch 1

DisNat{ F_{1}() -> Element of RAT+ , F_{2}() -> Element of RAT+ , F_{3}() -> Element of RAT+ , P_{1}[ set ] } :

provided

DisNat{ F

provided

A1:
F_{2}() = 1
and

A2: F_{1}() = {}
and

A3: F_{3}() in omega
and

A4: P_{1}[F_{1}()]
and

A5: P_{1}[F_{3}()]

A2: F

A3: F

A4: P

A5: P

proof end;