Addenda , 1998

University of Bialystok

Copyright (c) 1998 Association of Mizar Users

### The abstract of the Mizar article:

### Arithmetic of Non-Negative Rational Numbers

**by****Grzegorz Bancerek**- Received March 7, 1998
- 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()];

Back to top