Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Integers

**by****Michal J. Trybulec**- Received February 7, 1990
- MML identifier: INT_1

- [ Mizar article, MML identifier index ]

environ vocabulary ARYTM, ARYTM_1, ORDINAL2, ABSVALUE, NAT_1, ARYTM_3, RELAT_1, INT_1, BOOLE, COMPLEX1, ARYTM_2, XCMPLX_0; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ORDINAL2, ARYTM_2, ARYTM_1, NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0, REAL_1, ABSVALUE, NAT_1; constructors REAL_1, ABSVALUE, NAT_1, XCMPLX_0, XREAL_0, XBOOLE_0, ARYTM_0, ARYTM_3, ARYTM_2, FUNCT_4, ARYTM_1; clusters XREAL_0, ARYTM_3, REAL_1, ORDINAL2, NUMBERS, ZFMISC_1, XBOOLE_0, XCMPLX_0; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve X,x,y,z for set, k,l,n,n1,n2 for Nat, r for real number; definition cluster -> complex Element of COMPLEX; end; definition redefine func INT means :: INT_1:def 1 x in it iff ex k st x = k or x = - k; end; definition let i be number; attr i is integer means :: INT_1:def 2 i is Element of INT; end; definition cluster integer Real; cluster integer number; cluster -> integer Element of INT; end; definition mode Integer is integer number; end; canceled 7; theorem :: INT_1:8 r is Integer iff ex k st r = k or r = - k; :: Relations between sets INT, NAT and REAL ( and their elements ) definition cluster -> integer Nat; cluster natural -> integer number; end; canceled 2; theorem :: INT_1:11 x in INT implies x in REAL; definition cluster integer -> real number; end; theorem :: INT_1:12 x is Integer iff x in INT; canceled; theorem :: INT_1:14 NAT c= INT; theorem :: INT_1:15 INT c= REAL; reserve i0,i1,i2,i3,i4,i5,i7,i8,i9 for Integer; :: Now we are ready to redefine some functions :: Redefinition of functions "+", "*" and "-" definition let i1,i2 be Integer; cluster i1 + i2 -> integer; cluster i1 * i2 -> integer; end; definition let i0 be Integer; cluster - i0 -> integer; end; definition let i1,i2 be Integer; cluster i1 - i2 -> integer; end; :: More redefinitions definition let n be Nat; cluster - n -> integer; let i1 be Integer; cluster i1 + n -> integer; cluster i1 * n -> integer; cluster i1 - n -> integer; end; definition let n1,n2; cluster n1 - n2 -> integer; end; :: Some basic theorems about integers theorem :: INT_1:16 0 <= i0 implies i0 is Nat; theorem :: INT_1:17 r is Integer implies r + 1 is Integer & r - 1 is Integer; theorem :: INT_1:18 i2 <= i1 implies i1 - i2 is Nat; theorem :: INT_1:19 i1 + k = i2 implies i1 <= i2; theorem :: INT_1:20 i0 < i1 implies i0 + 1 <= i1; theorem :: INT_1:21 i1 < 0 implies i1 <= - 1; theorem :: INT_1:22 i1 * i2 = 1 iff (i1 = 1 & i2 = 1) or (i1 = - 1 & i2 = - 1); theorem :: INT_1:23 i1 * i2 = - 1 iff (i1 = - 1 & i2 = 1) or (i1 = 1 & i2 = - 1); canceled 2; theorem :: INT_1:26 r - 1 < r; scheme SepInt { P[Integer] } : ex X being Subset of INT st for x being Integer holds x in X iff P[x]; scheme Int_Ind_Up { F() -> Integer, P[Integer] } : for i0 st F() <= i0 holds P[i0] provided P[F()] and for i2 st F() <= i2 holds P[i2] implies P[i2 + 1]; scheme Int_Ind_Down { F() -> Integer, P[Integer] } : for i0 st i0 <= F() holds P[i0] provided P[F()] and for i2 st i2 <= F() holds P[i2] implies P[i2 - 1]; scheme Int_Ind_Full { F() -> Integer, P[Integer] } : for i0 holds P[i0] provided P[F()] and for i2 holds P[i2] implies P[i2 - 1] & P[i2 + 1]; scheme Int_Min { F() -> Integer, P[Integer] } : ex i0 st P[i0] & for i1 st P[i1] holds i0 <= i1 provided for i1 st P[i1] holds F() <= i1 and ex i1 st P[i1]; scheme Int_Max { F() -> Integer, P[Integer] } : ex i0 st P[i0] & for i1 st P[i1] holds i1 <= i0 provided for i1 st P[i1] holds i1 <= F() and ex i1 st P[i1]; :: abs and sgn functions with integers definition let r; cluster sgn r -> integer; end; canceled 2; theorem :: INT_1:29 sgn r = 1 or sgn r = - 1 or sgn r = 0; theorem :: INT_1:30 abs r = r or abs r = - r; definition let i0; cluster abs i0 -> integer; end; :: Congruences definition let i1,i2,i3 be Integer; pred i1,i2 are_congruent_mod i3 means :: INT_1:def 3 ex i4 st i3 * i4 = i1 - i2; end; canceled; theorem :: INT_1:32 i1,i1 are_congruent_mod i2; theorem :: INT_1:33 i1,0 are_congruent_mod i1 & 0,i1 are_congruent_mod i1; theorem :: INT_1:34 i1,i2 are_congruent_mod 1; theorem :: INT_1:35 i1,i2 are_congruent_mod i3 implies i2,i1 are_congruent_mod i3; theorem :: INT_1:36 i1,i2 are_congruent_mod i5 & i2,i3 are_congruent_mod i5 implies i1,i3 are_congruent_mod i5; theorem :: INT_1:37 i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 implies (i1 + i3),(i2 + i4) are_congruent_mod i5; theorem :: INT_1:38 i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 implies (i1 - i3),(i2 - i4) are_congruent_mod i5; theorem :: INT_1:39 i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 implies (i1 * i3),(i2 * i4) are_congruent_mod i5; theorem :: INT_1:40 (i1 + i2),i3 are_congruent_mod i5 iff i1, (i3 - i2) are_congruent_mod i5; theorem :: INT_1:41 i4 * i5 = i3 implies (i1,i2 are_congruent_mod i3 implies i1,i2 are_congruent_mod i4); theorem :: INT_1:42 i1,i2 are_congruent_mod i5 iff (i1 + i5),i2 are_congruent_mod i5; theorem :: INT_1:43 i1,i2 are_congruent_mod i5 iff (i1 - i5),i2 are_congruent_mod i5; theorem :: INT_1:44 (i1 <= r & r - 1 < i1) & (i2 <= r & r - 1 < i2) implies i1 = i2; theorem :: INT_1:45 (r <= i1 & i1 < r + 1) & (r <= i2 & i2 < r + 1) implies i1 = i2; reserve r1,p,p1,g,g1,g2 for real number, X,Y for Subset of REAL; definition let r be real number; func [\ r /] -> Integer means :: INT_1:def 4 it <= r & r - 1 < it; end; canceled; theorem :: INT_1:47 [\ r /] = r iff r is integer; theorem :: INT_1:48 [\ r /] < r iff r is not integer; canceled; theorem :: INT_1:50 [\ r /] - 1 < r & [\ r /] < r + 1; theorem :: INT_1:51 [\ r /] + i0 = [\ r + i0 /]; theorem :: INT_1:52 r < [\ r /] + 1; definition let r be real number; func [/ r \] -> Integer means :: INT_1:def 5 r <= it & it < r + 1; end; canceled; theorem :: INT_1:54 [/ r \] = r iff r is integer; theorem :: INT_1:55 r < [/ r \] iff r is not integer; canceled; theorem :: INT_1:57 r - 1 < [/ r \] & r < [/ r \] + 1; theorem :: INT_1:58 [/ r \] + i0 = [/ r + i0 \]; theorem :: INT_1:59 [\ r /] = [/ r \] iff r is integer; theorem :: INT_1:60 [\ r /] < [/ r \] iff r is not integer; theorem :: INT_1:61 [\ r /] <= [/ r \]; theorem :: INT_1:62 [\ ([/ r \]) /] = [/ r \]; theorem :: INT_1:63 [\ ([\ r /]) /] = [\ r /]; theorem :: INT_1:64 [/ ([/ r \]) \] = [/ r \]; theorem :: INT_1:65 [/ ([\ r /]) \] = [\ r /]; theorem :: INT_1:66 [\ r /] = [/ r \] iff not [\ r /] + 1 = [/ r \]; definition let r be real number; func frac r equals :: INT_1:def 6 r - [\ r /]; end; definition let r be real number; cluster frac r -> real; end; definition let r be real number; redefine func frac r -> Real; end; canceled; theorem :: INT_1:68 r = [\ r /] + frac r; theorem :: INT_1:69 frac r < 1 & 0 <= frac r; theorem :: INT_1:70 [\ frac r /] = 0; theorem :: INT_1:71 frac r = 0 iff r is integer; theorem :: INT_1:72 0 < frac r iff r is not integer; :: Functions div and mod definition let i1,i2 be Integer; func i1 div i2 -> Integer equals :: INT_1:def 7 [\ i1 / i2 /]; end; definition let i1,i2 be Integer; func i1 mod i2 -> Integer equals :: INT_1:def 8 i1 - (i1 div i2) * i2 if i2 <> 0 otherwise 0; end; :: The divisibility relation definition let i1,i2 be Integer; pred i1 divides i2 means :: INT_1:def 9 ex i3 st i2 = i1 * i3; reflexivity; end; canceled; theorem :: INT_1:74 for r being real number st r <> 0 holds [\ r / r /] = 1; theorem :: INT_1:75 for i being Integer holds i div 0 = 0; theorem :: INT_1:76 for i being Integer st i <> 0 holds i div i = 1; theorem :: INT_1:77 for i being Integer holds i mod i = 0;

Back to top