ARYTM_3

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

:: ARYTM_3 semantic presentation

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

Lm2: 1 in omega
;

definition

func one -> set equals :: ARYTM_3:def 1
1;
correctness ;

end;

:: deftheorem defines one ARYTM_3:def 1 :

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 ;

end;

:: deftheorem Def2 defines are_relative_prime ARYTM_3:def 2 :

theorem :: ARYTM_3:1

canceled;

theorem :: ARYTM_3:2

canceled;

theorem :: ARYTM_3:3

canceled;

theorem :: ARYTM_3:4

canceled;

theorem Th5: :: ARYTM_3:5

not {} , {} are_relative_prime

proof end;

theorem Th6: :: ARYTM_3:6

for A being Ordinal holds 1,A are_relative_prime

proof end;

theorem Th7: :: ARYTM_3:7

for A being Ordinal st {} ,A are_relative_prime holds
A = 1

proof end;

defpred S₁[ 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: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 )

proof end;

registration

let m, n be natural Ordinal;
cluster m div^ n -> natural ;
coherence

proof end;

cluster m mod^ n -> natural ;
coherence

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

proof end;

end;

:: deftheorem Def3 defines divides ARYTM_3:def 3 :

theorem Th9: :: ARYTM_3:9

for a, b being natural Ordinal holds
( a divides b iff ex c being natural Ordinal st b = a *^ c )

proof end;

theorem Th10: :: ARYTM_3:10

for m, n being natural Ordinal st {} in m holds
n mod^ m in m

proof end;

theorem Th11: :: ARYTM_3:11

for n, m being natural Ordinal holds
( m divides n iff n = m *^ (n div^ m) )

proof end;

theorem :: ARYTM_3:12

canceled;

theorem Th13: :: ARYTM_3:13

for n, m being natural Ordinal st n divides m & m divides n holds
n = m

proof end;

theorem Th14: :: ARYTM_3:14

for n being natural Ordinal holds
( n divides {} & 1 divides n )

proof end;

theorem Th15: :: ARYTM_3:15

for n, m being natural Ordinal st {} in m & n divides m holds
n c= m

proof end;

theorem Th16: :: ARYTM_3:16

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

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def4 defines lcm ARYTM_3:def 4 :

theorem Th17: :: ARYTM_3:17

for m, n being natural Ordinal holds m lcm n divides m *^ n

proof end;

theorem Th18: :: ARYTM_3:18

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

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def5 defines hcf ARYTM_3:def 5 :

theorem Th19: :: ARYTM_3:19

for a being natural Ordinal holds
( a hcf {} = a & a lcm {} = {} )

proof end;

theorem Th20: :: ARYTM_3:20

for a, b being natural Ordinal st a hcf b = {} holds
a = {}

proof end;

theorem Th21: :: ARYTM_3:21

for a being natural Ordinal holds
( a hcf a = a & a lcm a = a )

proof end;

theorem Th22: :: ARYTM_3:22

for a, c, b being natural Ordinal holds (a *^ c) hcf (b *^ c) = (a hcf b) *^ c

proof end;

theorem Th23: :: ARYTM_3:23

for b, a being natural Ordinal st b <> {} holds
( a hcf b <> {} & b div^ (a hcf b) <> {} )

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

proof end;

theorem Th25: :: ARYTM_3:25

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 by ORDINAL1:def 13;

end;

:: deftheorem defines RED ARYTM_3:def 6 :

theorem Th26: :: ARYTM_3:26

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

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;

theorem Th28: :: ARYTM_3:28

for a, b being natural Ordinal st a,b are_relative_prime holds
RED a,b = a

proof end;

theorem Th29: :: ARYTM_3:29

for a being natural Ordinal holds
( RED a,1 = a & RED 1,a = 1 )

proof end;

theorem :: ARYTM_3:30

for b, a being natural Ordinal st b <> {} holds
RED b,a <> {} by Th23;

theorem Th31: :: ARYTM_3:31

for a being natural Ordinal holds
( RED {} ,a = {} & ( a <> {} implies RED a,{} = 1 ) )

proof end;

theorem Th32: :: ARYTM_3:32

for a being natural Ordinal st a <> {} holds
RED a,a = 1

proof end;

theorem Th33: :: ARYTM_3:33

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

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 ;

end;

:: deftheorem defines RAT+ ARYTM_3:def 7 :

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

registration

cluster RAT+ -> non empty ;
coherence ;

end;

registration

cluster non empty ordinal Element of RAT+ ;
existence by Lm2, Lm5;

end;

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

proof end;

theorem Th36: :: ARYTM_3:36

for i, j being set holds [i,j] is not Ordinal

proof end;

theorem Th37: :: ARYTM_3:37

for A being Ordinal st A in RAT+ holds
A in omega

proof end;

registration

cluster ordinal -> ordinal natural Element of RAT+ ;
coherence

proof end;

end;

theorem Th38: :: ARYTM_3:38

for i, j being set holds not [i,j] in omega

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

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

proof end;

correctness 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

proof end;

correctness by ZFMISC_1:33;

end;

:: deftheorem Def8 defines numerator ARYTM_3:def 8 :

:: deftheorem Def9 defines denominator ARYTM_3:def 9 :

theorem Th40: :: ARYTM_3:40

for x being Element of RAT+ holds numerator x, denominator x are_relative_prime

proof end;

theorem Th41: :: ARYTM_3:41

for x being Element of RAT+ holds denominator x <> {}

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 )

proof end;

theorem Th43: :: ARYTM_3:43

for x being Element of RAT+ holds
( x <> {} iff numerator x <> {} )

proof end;

theorem :: ARYTM_3:44

for x being Element of RAT+ holds
( x in omega iff denominator x = 1 ) by Def9, Th42;

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

proof end;

consistency by Th31;

end;

:: deftheorem Def10 defines / ARYTM_3:def 10 :

notation

let i, j be natural Ordinal;
synonym quotient i,j for i / j;

end;

theorem Th45: :: ARYTM_3:45

for x being Element of RAT+ holds (numerator x) / (denominator x) = x

proof end;

theorem Th46: :: ARYTM_3:46

for b, a being natural Ordinal holds
( {} / b = {} & a / 1 = a )

proof end;

theorem Th47: :: ARYTM_3:47

for a being natural Ordinal st a <> {} holds
a / a = 1

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 )

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 )

proof end;

theorem Th50: :: ARYTM_3:50

for c, a, b being natural Ordinal st c <> {} holds
(a *^ c) / (b *^ c) = a / b

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 )

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