:: Arithmetic of Non Negative Rational Numbers :: by Grzegorz Bancerek :: :: Received March 7, 1998 :: Copyright (c) 1998-2016 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()];