Journal of Formalized Mathematics
University of Bialystok
Copyright (c) 1998 Association of Mizar Users

### Arithmetic of Non-Negative Rational Numbers

by
Grzegorz Bancerek

MML identifier: ARYTM_3
[ Mizar article, MML identifier index ]

```environ

vocabulary ORDINAL1, ORDINAL2, BOOLE, ORDINAL3, ARYTM_3, QUOFIELD;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, ORDINAL3;
constructors ORDINAL3, SUBSET_1, XBOOLE_0;
clusters ORDINAL1, ORDINAL2, SUBSET_1, ZFMISC_1, XBOOLE_0;
requirements BOOLE, SUBSET;

begin :: Natural ordinals

reserve A,B,C for Ordinal;

definition
let A be Ordinal;
cluster -> ordinal Element of A;
end;

definition
cluster empty -> natural Ordinal;
cluster one -> natural non empty;
cluster -> natural Element of omega;
end;

definition
cluster non empty natural Ordinal;
end;

definition let a be natural Ordinal;
cluster succ a -> natural;
end;

scheme Omega_Ind {P[set]}:
for a being natural Ordinal holds P[a]
provided
P[{}]
and
for a being natural Ordinal st P[a] holds P[succ a];

definition
let a, b be natural Ordinal;
cluster a +^ b -> natural;
end;

theorem :: ARYTM_3:1
for a,b being Ordinal st a+^b is natural holds a in omega & b in omega;

definition
let a, b be natural Ordinal;
cluster a -^ b -> natural;
cluster a *^ b -> natural;
end;

theorem :: ARYTM_3:2
for a,b being Ordinal st a*^b is natural non empty
holds a in omega & b in omega;

theorem :: ARYTM_3:3
for a,b being natural Ordinal holds a+^b = b+^a;

theorem :: ARYTM_3:4
for a,b being natural Ordinal holds a*^b = b*^a;

definition redefine
let a,b be natural Ordinal;
func a+^b; commutativity;
func a*^b; commutativity;
end;

begin :: Relative prime numbers and divisibility

definition
let a,b be Ordinal;
pred a,b are_relative_prime means
:: ARYTM_3:def 1

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

theorem :: ARYTM_3:5
not {},{} are_relative_prime;

theorem :: ARYTM_3:6
one,A are_relative_prime;

theorem :: ARYTM_3:7
{},A are_relative_prime implies A = one;

reserve a,b,c,d for natural Ordinal;

theorem :: ARYTM_3:8
a <> {} or b <> {} implies
ex c,d1,d2 being natural Ordinal st
d1,d2 are_relative_prime & a = c *^ d1 & b = c *^ d2;

reserve l,m,n for natural Ordinal;

definition let m,n;
cluster m div^ n -> natural;
cluster m mod^ n -> natural;
end;

definition
let k,n be Ordinal;
pred k divides n means
:: ARYTM_3:def 2
ex a being Ordinal st n = k*^a;
reflexivity;
end;

theorem :: ARYTM_3:9
a divides b iff ex c st b = a*^c;

theorem :: ARYTM_3:10
for m,n st {} in m holds n mod^ m in m;

theorem :: ARYTM_3:11
for n,m holds m divides n iff n = m *^ (n div^ m);

canceled;

theorem :: ARYTM_3:13
for n,m st n divides m & m divides n holds n = m;

theorem :: ARYTM_3:14
n divides {} & one divides n;

theorem :: ARYTM_3:15
for n,m st {} in m & n divides m holds n c= m;

theorem :: ARYTM_3:16
for n,m,l st n divides m & n divides m +^ l holds n divides l;

definition let k,n be natural Ordinal;
func k lcm n -> Element of omega means
:: ARYTM_3:def 3
k divides it & n divides it & for m st k divides m & n divides
m holds it divides m;
commutativity;
end;

theorem :: ARYTM_3:17
m lcm n divides m*^n;

theorem :: ARYTM_3:18
n <> {} implies (m*^n) div^ (m lcm n) divides m;

definition let k,n be natural Ordinal;
func k hcf n -> Element of omega means
:: ARYTM_3:def 4
it divides k & it divides n & for m st m divides k & m divides
n holds m divides it;
commutativity;
end;

theorem :: ARYTM_3:19
a hcf {} = a & a lcm {} = {};

theorem :: ARYTM_3:20
a hcf b = {} implies a = {};

theorem :: ARYTM_3:21
a hcf a = a & a lcm a = a;

theorem :: ARYTM_3:22
(a*^c) hcf (b*^c) = (a hcf b)*^c;

theorem :: ARYTM_3:23
b <> {} implies a hcf b <> {} & b div^ (a hcf b) <> {};

theorem :: ARYTM_3:24
a <> {} or b <> {} implies
a div^ (a hcf b), b div^ (a hcf b) are_relative_prime;

theorem :: ARYTM_3:25
a,b are_relative_prime iff a hcf b = one;

definition let a,b be natural Ordinal;
func RED(a,b) -> Element of omega equals
:: ARYTM_3:def 5

a div^ (a hcf b);
end;

theorem :: ARYTM_3:26
RED(a,b)*^(a hcf b) = a;

theorem :: ARYTM_3:27
a <> {} or b <> {} implies RED(a,b), RED(b,a) are_relative_prime;

theorem :: ARYTM_3:28
a,b are_relative_prime implies RED(a,b) = a;

theorem :: ARYTM_3:29
RED(a,one) = a & RED(one,a) = one;

theorem :: ARYTM_3:30
b <> {} implies RED(b,a) <> {};

theorem :: ARYTM_3:31
RED({},a) = {} & (a <> {} implies RED(a,{}) = one);

theorem :: ARYTM_3:32
a <> {} implies RED(a,a) = one;

theorem :: ARYTM_3:33
c <> {} implies RED(a*^c, b*^c) = RED(a, b);

begin :: Non negative rationals

reserve i,j,k for Element of omega;

definition
func RAT+ equals
:: ARYTM_3:def 6

({[i,j]: i,j are_relative_prime & j <> {}} \ {[k,one]: not contradiction})
\/ omega;
end;

theorem :: ARYTM_3:34
omega c= RAT+;

reserve x,y,z for Element of RAT+;

definition
cluster RAT+ -> non empty;
end;

definition
cluster non empty ordinal Element of RAT+;
end;

theorem :: ARYTM_3:35
x in
omega or ex i,j st x = [i,j] & i,j are_relative_prime & j <> {} & j <> one;

theorem :: ARYTM_3:36
not ex i,j being set st [i,j] is Ordinal;

theorem :: ARYTM_3:37
A in RAT+ implies A in omega;

definition
cluster -> natural (ordinal Element of RAT+);
end;

theorem :: ARYTM_3:38
not ex i,j being set st [i,j] in omega;

theorem :: ARYTM_3:39
[i,j] in RAT+ iff i,j are_relative_prime & j <> {} & j <> one;

definition
let x be Element of RAT+;
func numerator x -> Element of omega means
:: ARYTM_3:def 7

it = x if x in omega otherwise ex a st x = [it,a];
func denominator x -> Element of omega means
:: ARYTM_3:def 8

it = one if x in omega otherwise ex a st x = [a,it];
end;

theorem :: ARYTM_3:40
numerator x, denominator x are_relative_prime;

theorem :: ARYTM_3:41
denominator x <> {};

theorem :: ARYTM_3:42
not x in omega implies x = [numerator x, denominator x] & denominator x <> one
;

theorem :: ARYTM_3:43
x <> {} iff numerator x <> {};

theorem :: ARYTM_3:44
x in omega iff denominator x = one;

definition
let i,j be natural Ordinal;
func i/j -> Element of RAT+ equals
:: ARYTM_3:def 9

{} if j = {},
RED(i,j) if RED(j,i) = one otherwise
[RED(i,j), RED(j,i)];
synonym quotient(i,j);
end;

theorem :: ARYTM_3:45
(numerator x)/(denominator x) = x;

theorem :: ARYTM_3:46
{}/b = {} & a/one = a;

theorem :: ARYTM_3:47
a <> {} implies a/a = one;

theorem :: ARYTM_3:48
b <> {} implies numerator (a/b) = RED(a,b) & denominator (a/b) = RED(b,a);

theorem :: ARYTM_3:49
i,j are_relative_prime & j <> {} implies
numerator (i/j) = i & denominator (i/j) = j;

theorem :: ARYTM_3:50
c <> {} implies (a*^c)/(b*^c) = a/b;

reserve i,j,k for natural Ordinal;

theorem :: ARYTM_3:51
j <> {} & l <> {} implies (i/j = k/l iff i*^l = j*^k);

definition
let x,y be Element of RAT+;
func x+y -> Element of RAT+ equals
:: ARYTM_3:def 10

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

((numerator x)*^(numerator y)) / ((denominator x)*^(denominator y));
commutativity;
end;

theorem :: ARYTM_3:52
j <> {} & l <> {} implies (i/j)+(k/l) = (i*^l+^j*^k)/(j*^l);

theorem :: ARYTM_3:53
k <> {} implies (i/k)+(j/k) = (i+^j)/k;

definition
cluster empty Element of RAT+;
end;

definition
redefine
func {} -> empty Element of RAT+;
func one -> non empty ordinal Element of RAT+;
end;

theorem :: ARYTM_3:54
x*'{} = {};

theorem :: ARYTM_3:55
(i/j)*'(k/l) = (i*^k)/(j*^l);

theorem :: ARYTM_3:56
x+{} = x;

theorem :: ARYTM_3:57
(x+y)+z = x+(y+z);

theorem :: ARYTM_3:58
(x*'y)*'z = x*'(y*'z);

theorem :: ARYTM_3:59
x*'one = x;

theorem :: ARYTM_3:60
x <> {} implies ex y st x*'y = one;

theorem :: ARYTM_3:61
x <> {} implies ex z st y = x*'z;

theorem :: ARYTM_3:62
x <> {} & x*'y = x*'z implies y = z;

theorem :: ARYTM_3:63
x*'(y+z) = x*'y+x*'z;

theorem :: ARYTM_3:64
for i,j being ordinal Element of RAT+ holds i+j = i+^j;

theorem :: ARYTM_3:65
for i,j being ordinal Element of RAT+ holds i*'j = i*^j;

theorem :: ARYTM_3:66
ex y st x = y+y;

definition
let x,y be Element of RAT+;
pred x <=' y means
:: ARYTM_3:def 12

ex z being Element of RAT+ st y = x+z;
connectedness;
antonym y < x;
end;

reserve r,s,t for Element of RAT+;

canceled;

theorem :: ARYTM_3:68
not ex y being set st [{},y] in RAT+;

theorem :: ARYTM_3:69
s + t = r + t implies s = r;

theorem :: ARYTM_3:70
r+s = {} implies r = {};

theorem :: ARYTM_3:71
{} <=' s;

theorem :: ARYTM_3:72
s <=' {} implies s = {};

theorem :: ARYTM_3:73
r <=' s & s <=' r implies r = s;

theorem :: ARYTM_3:74
r <=' s & s <=' t implies r <=' t;

theorem :: ARYTM_3:75
r < s iff r <=' s & r <> s;

theorem :: ARYTM_3:76
r < s & s <=' t or r <=' s & s < t implies r < t;

theorem :: ARYTM_3:77
r < s & s < t implies r < t;

theorem :: ARYTM_3:78
x in omega & x+y in omega implies y in omega;

theorem :: ARYTM_3:79
for i being ordinal Element of RAT+
st i < x & x < i+one
holds not x in omega;

theorem :: ARYTM_3:80
t <> {} implies ex r st r < t & not r in omega;

theorem :: ARYTM_3:81
{s: s < t} in RAT+ iff t = {};

theorem :: ARYTM_3:82
for A being Subset of RAT+ st
(ex t st t in A & t <> {}) &   ::  dodany warunek ?!
for r,s st r in A & s <=' r holds s in A
ex r1,r2,r3 being Element of RAT+ st
r1 in A & r2 in A & r3 in A &
r1 <> r2 & r2 <> r3 & r3 <> r1;

theorem :: ARYTM_3:83
s + t <=' r + t iff s <=' r;

canceled;

theorem :: ARYTM_3:85
s <=' s + t;

theorem :: ARYTM_3:86
r*'s = {} implies r = {} or s = {};

theorem :: ARYTM_3:87
r <=' s *' t implies
ex t0 being Element of RAT+ st r = s *' t0 & t0 <=' t;

theorem :: ARYTM_3:88
t <> {} & s *' t <=' r *' t implies s <=' r;

theorem :: ARYTM_3:89
for r1,r2,s1,s2 being Element of RAT+ st r1+r2 = s1+s2
holds r1 <=' s1 or r2 <=' s2;

theorem :: ARYTM_3:90
s <=' r implies s *' t <=' r *' t;

theorem :: ARYTM_3:91
for r1,r2,s1,s2 being Element of RAT+ st r1*'r2 = s1*'s2
holds r1 <=' s1 or r2 <=' s2;

theorem :: ARYTM_3:92
r = {} iff r + s = s;

theorem :: ARYTM_3:93
for s1,t1,s2,t2 being Element of RAT+ st s1 + t1 = s2 + t2 & s1 <=' s2
holds t2 <=' t1;

theorem :: ARYTM_3:94
r <=' s & s <=' r + t implies
ex t0 being Element of RAT+ st s = r + t0 & t0 <=' t;

theorem :: ARYTM_3:95
r <=' s + t implies
ex s0,t0 being Element of RAT+ st r = s0 + t0 & s0 <=' s & t0 <=' t;

theorem :: ARYTM_3:96
r < s & r < t implies
ex t0 being Element of RAT+ st t0 <=' s & t0 <=' t & r < t0;

theorem :: ARYTM_3:97
r <=' s & s <=' t & s <> t implies r <> t;

theorem :: ARYTM_3:98
s < r + t & t <> {} implies
ex r0,t0 being Element of RAT+ st s = r0 + t0 &
r0 <=' r & t0 <=' t & t0 <> t;

theorem :: ARYTM_3:99
for A being non empty Subset of RAT+ st A in RAT+
ex s st s in A & for r st r in A holds r <=' s;

theorem :: ARYTM_3:100
ex t st r + t = s or s + t = r;

theorem :: ARYTM_3:101
r < s implies ex t st r < t & t < s;

theorem :: ARYTM_3:102
ex s st r < s;

theorem :: ARYTM_3:103
t <> {} implies ex s st s in omega & r <=' s *' t;

scheme DisNat { n0,n1,n2() -> Element of RAT+, P[set] }:
ex s st s in omega & P[s] & not P[s + n1()]
provided
n1() = one and
n0() = {} and
n2() in omega and
P[n0()] and
not P[n2()];

```