ARYTM_3: Arithmetic of Non Negative Rational Numbers

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

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

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_coprime means :: ARYTM_3:def 2
for c, d1, d2 being Ordinal st a = c *^ d1 & b = c *^ d2 holds
c = 1;

symmetry ;

end;

:: deftheorem defines are_coprime ARYTM_3:def 2 :

theorem :: ARYTM_3:1

not {} , {} are_coprime

proof end;

theorem Th2: :: ARYTM_3:2

for A being Ordinal holds 1,A are_coprime by ORDINAL3:37;

theorem Th3: :: ARYTM_3:3

for A being Ordinal st {} ,A are_coprime 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_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 )

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 :: ARYTM_3:def 3
ex a being Ordinal st n = k *^ a;

reflexivity

proof end;

end;

:: deftheorem defines divides ARYTM_3:def 3 :

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

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 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 m, n 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 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, b, c being natural Ordinal holds (a *^ c) hcf (b *^ c) = (a hcf b) *^ c

proof end;

theorem Th18: :: ARYTM_3:18

for a, b 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_coprime

proof end;

Lm4: 0 = {}
;

theorem Th20: :: ARYTM_3:20

for a, b being natural Ordinal holds
( a,b are_coprime 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 12;

end;

:: deftheorem defines RED ARYTM_3:def 6 :

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_coprime by Th19;

theorem Th23: :: ARYTM_3:23

for a, b being natural Ordinal st a,b are_coprime 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 a, b 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 a, b, c 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_coprime & b <> {} ) } ;

Lm5: for a, b being natural Ordinal st [a,b] in { [a,b] where a, b is Element of omega : ( a,b are_coprime & b <> {} ) } holds
( a,b are_coprime & b <> {} )

proof end;

definition

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 ;

end;

:: deftheorem defines RAT+ ARYTM_3:def 7 :

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

registration

cluster RAT+ -> non empty ;

coherence ;

end;

registration

cluster non empty ordinal for Element of RAT+ ;

existence by Lm2, Lm6, Lm4;

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_coprime & 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

proof end;

end;

theorem Th32: :: ARYTM_3:32

for i, j being object 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_coprime & 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 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

proof end;

correctness by XTUPLE_0:1;

end;

:: deftheorem Def8 defines numerator ARYTM_3:def 8 :

:: deftheorem Def9 defines denominator ARYTM_3:def 9 :

theorem Th34: :: ARYTM_3:34

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

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

proof end;

consistency by Th26, Lm4;

end;

:: deftheorem Def10 defines / ARYTM_3:def 10 :

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 a, b 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 a, b 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_coprime & j <> {} holds
( numerator (i / j) = i & denominator (i / j) = j )

proof end;

theorem Th44: :: ARYTM_3:44

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

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 )

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 ;

func x *' y -> Element of RAT+ equals :: ARYTM_3:def 12
((numerator x) *^ (numerator y)) / ((denominator x) *^ (denominator y));

coherence ;
commutativity ;

end;

:: deftheorem defines + ARYTM_3:def 11 :

:: deftheorem defines *' ARYTM_3:def 12 :

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)

proof end;

theorem Th47: :: ARYTM_3:47

for i, j, k being natural Ordinal st k <> {} holds
(i / k) + (j / k) = (i +^ j) / k

proof end;

registration

cluster empty for Element of RAT+ ;

existence by Lm1, Lm6;

end;

definition

:: original: {}
redefine func {} -> Element of RAT+ ;
coherence by Lm1, Lm6;
:: original: one
redefine func one -> non empty ordinal Element of RAT+ ;
coherence by Lm6, Lm4;

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

proof end;

end;

:: deftheorem Def13 defines <=' ARYTM_3:def 13 :

notation

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

end;

theorem :: ARYTM_3:61

for y being object holds not [{},y] in RAT+

proof end;

theorem Th62: :: ARYTM_3:62

for r, s, t 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 = {} by Th63;

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

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 r, s, t 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 r, s, 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 ) by Th76;

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

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 r, t 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{ F₁() -> Element of RAT+ , F₂() -> Element of RAT+ , F₃() -> Element of RAT+ , P₁[ set ] } :

ex s being Element of RAT+ st
( s in omega & P₁[s] & P₁[s + F₂()] )

provided

A1: F₂() = 1 and
A2: F₁() = {} and
A3: F₃() in omega and
A4: P₁[F₁()] and
A5: P₁[F₃()]

proof end;