:: Arithmetic of Non Negative Rational Numbers
:: by Grzegorz Bancerek
::
:: Received March 7, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ORDINAL1, XBOOLE_0, ORDINAL2, TARSKI, SUBSET_1, ORDINAL3,
ARYTM_3, CARD_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, ORDINAL3;
constructors SUBSET_1, ORDINAL3;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, ORDINAL3;
requirements BOOLE, SUBSET, NUMERALS;
begin :: Natural ordinals
reserve A,B,C for Ordinal;
definition
func one -> set equals
:: ARYTM_3:def 1
1;
end;
begin :: Relative prime numbers and divisibility
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;
theorem :: ARYTM_3:1
not {},{} are_coprime;
theorem :: ARYTM_3:2
1,A are_coprime;
theorem :: ARYTM_3:3
{},A are_coprime implies A = 1;
reserve a,b,c,d for natural Ordinal;
theorem :: ARYTM_3:4
a <> {} or b <> {} implies ex c,d1,d2 being natural Ordinal st d1,d2
are_coprime & a = c *^ d1 & b = c *^ d2;
reserve l,m,n for natural Ordinal;
registration
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 3
ex a being Ordinal st n = k*^a;
reflexivity;
end;
theorem :: ARYTM_3:5
a divides b iff ex c st b = a*^c;
theorem :: ARYTM_3:6
for m,n st {} in m holds n mod^ m in m;
theorem :: ARYTM_3:7
for n,m holds m divides n iff n = m *^ (n div^ m);
theorem :: ARYTM_3:8
for n,m st n divides m & m divides n holds n = m;
theorem :: ARYTM_3:9
n divides {} & 1 divides n;
theorem :: ARYTM_3:10
for n,m st {} in m & n divides m holds n c= m;
theorem :: ARYTM_3:11
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 4
k divides it & n divides it &
for m st k divides m & n divides m holds it divides m;
commutativity;
end;
theorem :: ARYTM_3:12
m lcm n divides m*^n;
theorem :: ARYTM_3:13
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 5
it divides k & it divides n &
for m st m divides k & m divides n holds m divides it;
commutativity;
end;
theorem :: ARYTM_3:14
a hcf {} = a & a lcm {} = {};
theorem :: ARYTM_3:15
a hcf b = {} implies a = {};
theorem :: ARYTM_3:16
a hcf a = a & a lcm a = a;
theorem :: ARYTM_3:17
(a*^c) hcf (b*^c) = (a hcf b)*^c;
theorem :: ARYTM_3:18
b <> {} implies a hcf b <> {} & b div^ (a hcf b) <> {};
theorem :: ARYTM_3:19
a <> {} or b <> {} implies a div^ (a hcf b), b div^ (a hcf b)
are_coprime;
theorem :: ARYTM_3:20
a,b are_coprime iff a hcf b = 1;
definition
let a,b be natural Ordinal;
func RED(a,b) -> Element of omega equals
:: ARYTM_3:def 6
a div^ (a hcf b);
end;
theorem :: ARYTM_3:21
RED(a,b)*^(a hcf b) = a;
theorem :: ARYTM_3:22
a <> {} or b <> {} implies RED(a,b), RED(b,a) are_coprime;
theorem :: ARYTM_3:23
a,b are_coprime implies RED(a,b) = a;
theorem :: ARYTM_3:24
RED(a,1) = a & RED(1,a) = 1;
theorem :: ARYTM_3:25
b <> {} implies RED(b,a) <> {};
theorem :: ARYTM_3:26
RED({},a) = {} & (a <> {} implies RED(a,{}) = 1);
theorem :: ARYTM_3:27
a <> {} implies RED(a,a) = 1;
theorem :: ARYTM_3:28
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+ -> set equals
:: ARYTM_3:def 7
({[i,j]: i,j are_coprime & j <> {}} \ the set of all [k,1]) \/ omega;
end;
reserve x,y,z for Element of RAT+;
registration
cluster RAT+ -> non empty;
end;
registration
cluster non empty ordinal for Element of RAT+;
end;
theorem :: ARYTM_3:29
x in omega or ex i,j st x = [i,j] & i,j are_coprime & j <> {} & j <> 1;
theorem :: ARYTM_3:30
not ex i,j being set st [i,j] is Ordinal;
theorem :: ARYTM_3:31
A in RAT+ implies A in omega;
registration
cluster -> natural for ordinal Element of RAT+;
end;
theorem :: ARYTM_3:32
not ex i,j being object st [i,j] in omega;
theorem :: ARYTM_3:33
[i,j] in RAT+ iff i,j are_coprime & j <> {} & j <> 1;
definition
let x be Element of RAT+;
func numerator x -> Element of omega means
:: ARYTM_3:def 8
it = x if x in omega otherwise ex a st x = [it,a];
func denominator x -> Element of omega means
:: ARYTM_3:def 9
it = 1 if x in omega otherwise ex a st x = [a,it];
end;
theorem :: ARYTM_3:34
numerator x, denominator x are_coprime;
theorem :: ARYTM_3:35
denominator x <> {};
theorem :: ARYTM_3:36
not x in omega implies x = [numerator x, denominator x] & denominator x <> 1;
theorem :: ARYTM_3:37
x <> {} iff numerator x <> {};
theorem :: ARYTM_3:38
x in omega iff denominator x = 1;
definition
let i,j be natural Ordinal;
func i/j -> Element of RAT+ equals
:: ARYTM_3:def 10
{} if j = {}, RED(i,j) if RED(j,i
) = 1 otherwise [RED(i,j), RED(j,i)];
end;
notation
let i,j be natural Ordinal;
synonym quotient(i,j) for i/j;
end;
theorem :: ARYTM_3:39
(numerator x)/(denominator x) = x;
theorem :: ARYTM_3:40
{}/b = {} & a/1 = a;
theorem :: ARYTM_3:41
a <> {} implies a/a = 1;
theorem :: ARYTM_3:42
b <> {} implies numerator (a/b) = RED(a,b) & denominator (a/b) = RED(b,a);
theorem :: ARYTM_3:43
i,j are_coprime & j <> {} implies numerator (i/j) = i &
denominator (i/j) = j;
theorem :: ARYTM_3:44
c <> {} implies (a*^c)/(b*^c) = a/b;
reserve i,j,k for natural Ordinal;
theorem :: ARYTM_3:45
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 11
((numerator x)*^(denominator y)+^(
numerator y)*^(denominator x)) / ((denominator x)*^(denominator y));
commutativity;
func x*'y -> Element of RAT+ equals
:: ARYTM_3:def 12
((numerator x)*^(numerator y)) / ((
denominator x)*^(denominator y));
commutativity;
end;
theorem :: ARYTM_3:46
j <> {} & l <> {} implies (i/j)+(k/l) = (i*^l+^j*^k)/(j*^l);
theorem :: ARYTM_3:47
k <> {} implies (i/k)+(j/k) = (i+^j)/k;
registration
cluster empty for Element of RAT+;
end;
definition
redefine func {} -> Element of RAT+;
redefine func one -> non empty ordinal Element of RAT+;
end;
theorem :: ARYTM_3:48
x*'{} = {};
theorem :: ARYTM_3:49
(i/j)*'(k/l) = (i*^k)/(j*^l);
theorem :: ARYTM_3:50
x+{} = x;
theorem :: ARYTM_3:51
(x+y)+z = x+(y+z);
theorem :: ARYTM_3:52
(x*'y)*'z = x*'(y*'z);
theorem :: ARYTM_3:53
x*'one = x;
theorem :: ARYTM_3:54
x <> {} implies ex y st x*'y = 1;
theorem :: ARYTM_3:55
x <> {} implies ex z st y = x*'z;
theorem :: ARYTM_3:56
x <> {} & x*'y = x*'z implies y = z;
theorem :: ARYTM_3:57
x*'(y+z) = x*'y+x*'z;
theorem :: ARYTM_3:58
for i,j being ordinal Element of RAT+ holds i+j = i+^j;
theorem :: ARYTM_3:59
for i,j being ordinal Element of RAT+ holds i*'j = i*^j;
theorem :: ARYTM_3:60
ex y st x = y+y;
definition
let x,y be Element of RAT+;
pred x <=' y means
:: ARYTM_3:def 13
ex z being Element of RAT+ st y = x+z;
connectedness;
end;
notation
let x,y be Element of RAT+;
antonym y < x for x <=' y;
end;
reserve r,s,t for Element of RAT+;
theorem :: ARYTM_3:61
not ex y being object st [{},y] in RAT+;
theorem :: ARYTM_3:62
s + t = r + t implies s = r;
theorem :: ARYTM_3:63
r+s = {} implies r = {};
theorem :: ARYTM_3:64
{} <=' s;
theorem :: ARYTM_3:65
s <=' {} implies s = {};
theorem :: ARYTM_3:66
r <=' s & s <=' r implies r = s;
theorem :: ARYTM_3:67
r <=' s & s <=' t implies r <=' t;
theorem :: ARYTM_3:68
r < s iff r <=' s & r <> s;
theorem :: ARYTM_3:69
r < s & s <=' t or r <=' s & s < t implies r < t;
theorem :: ARYTM_3:70
r < s & s < t implies r < t;
theorem :: ARYTM_3:71
x in omega & x+y in omega implies y in omega;
theorem :: ARYTM_3:72
for i being ordinal Element of RAT+ st i < x & x < i+one holds not x in omega
;
theorem :: ARYTM_3:73
t <> {} implies ex r st r < t & not r in omega;
theorem :: ARYTM_3:74
{s: s < t} in RAT+ iff t = {};
theorem :: ARYTM_3:75
for A being Subset of RAT+ st (ex t st t in A & t <> {}) & 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:76
s + t <=' r + t iff s <=' r;
theorem :: ARYTM_3:77
s <=' s + t;
theorem :: ARYTM_3:78
r*'s = {} implies r = {} or s = {};
theorem :: ARYTM_3:79
r <=' s *' t implies ex t0 being Element of RAT+ st r = s *' t0 & t0 <=' t;
theorem :: ARYTM_3:80
t <> {} & s *' t <=' r *' t implies s <=' r;
theorem :: ARYTM_3:81
for r1,r2,s1,s2 being Element of RAT+ st r1+r2 = s1+s2 holds r1 <=' s1
or r2 <=' s2;
theorem :: ARYTM_3:82
s <=' r implies s *' t <=' r *' t;
theorem :: ARYTM_3:83
for r1,r2,s1,s2 being Element of RAT+ st r1*'r2 = s1*'s2 holds r1 <='
s1 or r2 <=' s2;
theorem :: ARYTM_3:84
r = {} iff r + s = s;
theorem :: ARYTM_3:85
for s1,t1,s2,t2 being Element of RAT+ st s1 + t1 = s2 + t2 & s1 <=' s2
holds t2 <=' t1;
theorem :: ARYTM_3:86
r <=' s & s <=' r + t implies ex t0 being Element of RAT+ st s =
r + t0 & t0 <=' t;
theorem :: ARYTM_3:87
r <=' s + t implies ex s0,t0 being Element of RAT+ st r = s0 + t0 & s0
<=' s & t0 <=' t;
theorem :: ARYTM_3:88
r < s & r < t implies ex t0 being Element of RAT+ st t0 <=' s & t0 <='
t & r < t0;
theorem :: ARYTM_3:89
r <=' s & s <=' t & s <> t implies r <> t;
theorem :: ARYTM_3:90
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:91
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:92
ex t st r + t = s or s + t = r;
theorem :: ARYTM_3:93
r < s implies ex t st r < t & t < s;
theorem :: ARYTM_3:94
ex s st r < s;
theorem :: ARYTM_3:95
t <> {} implies ex s st s in omega & r <=' s *' t;
scheme :: ARYTM_3:sch 1
DisNat { n0,n1,n2() -> Element of RAT+, P[set] }: ex s st s in omega & P[s]
& not P[s + n1()]
provided
n1() = 1 and
n0() = {} and
n2() in omega and
P[n0()] and
not P[n2()];