:: by Grzegorz Bancerek

::

:: Received March 7, 1998

:: Copyright (c) 1998-2015 Association of Mizar Users

Lm1: {} in omega

by ORDINAL1:def 11;

Lm2: 1 in omega

;

definition

let a, b be Ordinal;

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_coprime means :: ARYTM_3:def 2

for c, d1, d2 being Ordinal st a = c *^ d1 & b = c *^ d2 holds

c = 1;

symmetry for c, d1, d2 being Ordinal st a = c *^ d1 & b = c *^ d2 holds

c = 1;

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 defines are_coprime ARYTM_3:def 2 :

for a, b being Ordinal holds

( a,b are_coprime iff for c, d1, d2 being Ordinal st a = c *^ d1 & b = c *^ d2 holds

c = 1 );

for a, b being Ordinal holds

( a,b are_coprime iff for c, d1, d2 being Ordinal st a = c *^ d1 & b = c *^ d2 holds

c = 1 );

defpred S

( B c= $1 & $1 in omega & $1 <> {} & ( for c, d1, d2 being natural Ordinal holds

( not d1,d2 are_coprime 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_coprime & a = c *^ d1 & b = c *^ d2 )

ex c, d1, d2 being natural Ordinal st

( d1,d2 are_coprime & a = c *^ d1 & b = c *^ d2 )

proof end;

registration

let m, n be natural Ordinal;

coherence

m div^ n is natural

m mod^ n is natural

end;
coherence

m div^ n is natural

proof end;

coherence m mod^ n is natural

proof end;

definition
end;

:: deftheorem defines divides ARYTM_3:def 3 :

for k, n being Ordinal holds

( k divides n iff ex a being Ordinal st n = k *^ a );

for k, n being Ordinal holds

( k divides n iff ex a being Ordinal st n = k *^ a );

Lm3: 1 = succ 0

;

definition

let k, n be natural Ordinal;

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 ( k divides it & n divides it & ( for m being natural Ordinal st k divides m & n divides m holds

it divides m ) );

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_{3} being Element of omega holds

( b_{3} = k lcm n iff ( k divides b_{3} & n divides b_{3} & ( for m being natural Ordinal st k divides m & n divides m holds

b_{3} divides m ) ) );

for k, n being natural Ordinal

for b

( b

b

definition

let k, n be natural Ordinal;

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 ( it divides k & it divides n & ( for m being natural Ordinal st m divides k & m divides n holds

m divides it ) );

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_{3} being Element of omega holds

( b_{3} = k hcf n iff ( b_{3} divides k & b_{3} divides n & ( for m being natural Ordinal st m divides k & m divides n holds

m divides b_{3} ) ) );

for k, n being natural Ordinal

for b

( b

m divides b

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_coprime

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

proof end;

Lm4: 0 = {}

;

definition
end;

:: deftheorem defines RED ARYTM_3:def 6 :

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

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

theorem :: ARYTM_3:22

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

1,1 are_coprime

by Th2;

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

by Lm4;

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

Lm5: for a, b being natural Ordinal st [a,b] in RATplus holds

( a,b are_coprime & b <> {} )

proof end;

definition

coherence

( { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega is set ;

;

end;

func RAT+ -> set equals :: ARYTM_3:def 7

( { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega;

correctness ( { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega;

coherence

( { [i,j] where i, j is Element of omega : ( i,j are_coprime & 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_coprime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega;

RAT+ = ( { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega;

Lm6: omega c= RAT+

by XBOOLE_1:7;

registration

existence

ex b_{1} being Element of RAT+ st

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

end;
ex b

( not b

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_coprime & j <> {} & j <> 1 ) )

( x in omega or ex i, j being Element of omega st

( x = [i,j] & i,j are_coprime & j <> {} & j <> 1 ) )

proof end;

registration
end;

definition

let x be Element of RAT+ ;

( ( 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 XTUPLE_0:1;

( ( 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 XTUPLE_0:1;

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 it = x if x in omega

otherwise ex a being natural Ordinal st x = [it,a];

( ( x in omega implies ex b

proof end;

correctness consistency

for b

uniqueness

for b

( ( x in omega & b

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 it = 1 if x in omega

otherwise ex a being natural Ordinal st x = [a,it];

( ( x in omega implies ex b

proof end;

correctness consistency

for b

uniqueness

for b

( ( x in omega & b

by XTUPLE_0:1;

:: deftheorem Def8 defines numerator ARYTM_3:def 8 :

for x being Element of RAT+

for b_{2} being Element of omega holds

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

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_{2} being Element of omega holds

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

for x being Element of RAT+

for b

( ( x in omega implies ( b

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 )

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

proof end;

theorem :: ARYTM_3:38

definition

let i, j be natural Ordinal;

( ( 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 Th26, Lm4;

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 {} if j = {}

RED (i,j) if RED (j,i) = 1

otherwise [(RED (i,j)),(RED (j,i))];

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

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 Th42: :: ARYTM_3:42

for a, b 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 Th43: :: ARYTM_3:43

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

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

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

proof end;

theorem Th45: :: ARYTM_3:45

for l, i, j, 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+ ;

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

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

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

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

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

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, i, j, 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;

definition

:: original: {}

redefine func {} -> Element of RAT+ ;

coherence

{} is Element of RAT+ by Lm1, Lm6;

:: original: one

redefine func one -> non empty ordinal Element of RAT+ ;

coherence

one is non empty ordinal Element of RAT+ by Lm6, Lm4;

end;
redefine func {} -> Element of RAT+ ;

coherence

{} is Element of RAT+ by Lm1, Lm6;

:: original: one

redefine func one -> non empty ordinal Element of RAT+ ;

coherence

one is non empty ordinal Element of RAT+ by Lm6, Lm4;

definition

let x, y be Element of RAT+ ;

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

for x, y being Element of RAT+ holds

( x <=' y iff ex z being Element of RAT+ st y = x + z );

theorem :: ARYTM_3:68

theorem :: ARYTM_3:69

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

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 )

ex r being Element of RAT+ st

( r < t & not r in omega )

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 )

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

ex t0 being Element of RAT+ st

( r = s *' t0 & t0 <=' 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 )

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

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 )

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 )

ex t0 being Element of RAT+ st

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

proof end;

theorem :: ARYTM_3:89

theorem :: ARYTM_3:90

for r, s, 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: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 ) )

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

for r, t 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;