:: Integers :: by Micha{\l} J. Trybulec :: :: Received February 7, 1990 :: Copyright (c) 1990-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 NUMBERS, SUBSET_1, XREAL_0, ORDINAL1, ZFMISC_1, CARD_1, XBOOLE_0, ARYTM_1, TARSKI, ARYTM_2, ARYTM_3, ARYTM_0, REAL_1, XXREAL_0, NAT_1, RELAT_1, INT_1, FUNCT_7, XCMPLX_0; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ARYTM_2, ARYTM_1, NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, XXREAL_0; constructors FUNCT_4, ARYTM_1, ARYTM_0, XXREAL_0, REAL_1, NAT_1, FINSET_1, CARD_1, XREAL_0, NUMBERS; registrations ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, CARD_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve X for set, x,y,z for object, k,l,n for Nat, r for Real; 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 in INT; end; registration cluster integer for Real; cluster integer for number; cluster -> integer for Element of INT; end; definition mode Integer is integer Number; end; theorem :: INT_1:1 for k being natural Number st r = k or r = -k holds r is Integer; theorem :: INT_1:2 r is Integer implies ex k st r = k or r = - k; :: Relations between sets INT, NAT and REAL ( and their elements ) registration cluster natural -> integer for object; end; registration cluster integer -> real for object; end; reserve i,i0,i1,i2,i3,i4,i5,i8,i9,j for Integer; registration let i1,i2 be Integer; cluster i1 + i2 -> integer; cluster i1 * i2 -> integer; end; registration let i0 be Integer; cluster - i0 -> integer; end; registration let i1,i2 be Integer; cluster i1 - i2 -> integer; end; :: Some basic theorems about integers theorem :: INT_1:3 0 <= i0 implies i0 in NAT; theorem :: INT_1:4 r is Integer implies r + 1 is Integer & r - 1 is Integer; theorem :: INT_1:5 i2 <= i1 implies i1 - i2 in NAT; theorem :: INT_1:6 i1 + k = i2 implies i1 <= i2; theorem :: INT_1:7 i0 < i1 implies i0 + 1 <= i1; theorem :: INT_1:8 i1 < 0 implies i1 <= - 1; theorem :: INT_1:9 i1 * i2 = 1 iff i1 = 1 & i2 = 1 or i1 = - 1 & i2 = - 1; theorem :: INT_1:10 i1 * i2 = - 1 iff i1 = - 1 & i2 = 1 or i1 = 1 & i2 = - 1; scheme :: INT_1:sch 1 SepInt { P[Integer] } : ex X being Subset of INT st for x being Integer holds x in X iff P[x]; scheme :: INT_1:sch 2 IntIndUp { 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_1:sch 3 IntIndDown { 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_1:sch 4 IntIndFull { 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_1:sch 5 IntMin { 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_1:sch 6 IntMax { 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]; :: The divisibility relation definition let i1,i2 be Integer; pred i1 divides i2 means :: INT_1:def 3 ex i3 st i2 = i1 * i3; reflexivity; end; definition let i1,i2,i3 be Integer; pred i1,i2 are_congruent_mod i3 means :: INT_1:def 4 i3 divides i1 - i2; end; definition let i1,i2,i3 be Integer; redefine pred i1,i2 are_congruent_mod i3 means :: INT_1:def 5 ex i4 st i3 * i4 = i1 - i2; end; theorem :: INT_1:11 i1,i1 are_congruent_mod i2; theorem :: INT_1:12 i1,0 are_congruent_mod i1 & 0,i1 are_congruent_mod i1; theorem :: INT_1:13 i1,i2 are_congruent_mod 1; theorem :: INT_1:14 i1,i2 are_congruent_mod i3 implies i2,i1 are_congruent_mod i3; theorem :: INT_1:15 i1,i2 are_congruent_mod i5 & i2,i3 are_congruent_mod i5 implies i1,i3 are_congruent_mod i5; theorem :: INT_1:16 i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 implies (i1 + i3),(i2 + i4) are_congruent_mod i5; theorem :: INT_1:17 i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 implies (i1 - i3),(i2 - i4) are_congruent_mod i5; theorem :: INT_1:18 i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 implies (i1 * i3),(i2 * i4) are_congruent_mod i5; theorem :: INT_1:19 (i1 + i2),i3 are_congruent_mod i5 iff i1, (i3 - i2) are_congruent_mod i5; theorem :: INT_1:20 i4 * i5 = i3 implies (i1,i2 are_congruent_mod i3 implies i1,i2 are_congruent_mod i4); theorem :: INT_1:21 i1,i2 are_congruent_mod i5 iff (i1 + i5),i2 are_congruent_mod i5; theorem :: INT_1:22 i1,i2 are_congruent_mod i5 iff (i1 - i5),i2 are_congruent_mod i5; theorem :: INT_1:23 i1 <= r & r - 1 < i1 & i2 <= r & r - 1 < i2 implies i1 = i2; theorem :: INT_1:24 r <= i1 & i1 < r + 1 & r <= i2 & i2 < r + 1 implies i1 = i2; reserve r1,p,p1,g,g1,g2 for Real, Y for Subset of REAL; definition let r be Real; func [\ r /] -> Integer means :: INT_1:def 6 it <= r & r - 1 < it; projectivity; end; theorem :: INT_1:25 [\ r /] = r iff r is integer; theorem :: INT_1:26 [\ r /] < r iff r is not integer; theorem :: INT_1:27 [\ r /] - 1 < r & [\ r /] < r + 1; theorem :: INT_1:28 [\ r /] + i0 = [\ r + i0 /]; theorem :: INT_1:29 r < [\ r /] + 1; definition let r be Real; func [/ r \] -> Integer means :: INT_1:def 7 r <= it & it < r + 1; projectivity; end; theorem :: INT_1:30 [/ r \] = r iff r is integer; theorem :: INT_1:31 r < [/ r \] iff r is not integer; theorem :: INT_1:32 r - 1 < [/ r \] & r < [/ r \] + 1; theorem :: INT_1:33 [/ r \] + i0 = [/ r + i0 \]; theorem :: INT_1:34 [\ r /] = [/ r \] iff r is integer; theorem :: INT_1:35 [\ r /] < [/ r \] iff r is not integer; theorem :: INT_1:36 [\ r /] <= [/ r \]; theorem :: INT_1:37 [\ ([/ r \]) /] = [/ r \]; ::$CT 2 theorem :: INT_1:40 [/ ([\ r /]) \] = [\ r /]; theorem :: INT_1:41 [\ r /] = [/ r \] iff not [\ r /] + 1 = [/ r \]; definition let r be Real; func frac r -> number equals :: INT_1:def 8 r - [\ r /]; end; registration let r be Real; cluster frac r -> real; end; theorem :: INT_1:42 r = [\ r /] + frac r; theorem :: INT_1:43 frac r < 1 & 0 <= frac r; theorem :: INT_1:44 [\ frac r /] = 0; theorem :: INT_1:45 frac r = 0 iff r is integer; theorem :: INT_1:46 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 9 [\ i1 / i2 /]; end; definition let i1,i2 be Integer; func i1 mod i2 -> Integer equals :: INT_1:def 10 i1 - (i1 div i2) * i2 if i2 <> 0 otherwise 0; end; theorem :: INT_1:47 for r being Real st r <> 0 holds [\ r / r /] = 1; theorem :: INT_1:48 for i being Integer holds i div 0 = 0; theorem :: INT_1:49 for i being Integer st i <> 0 holds i div i = 1; theorem :: INT_1:50 for i being Integer holds i mod i = 0; begin :: Addenda :: from FSM_1 theorem :: INT_1:51 for k, i being Integer holds k < i implies ex j being Element of NAT st j = i-k & 1 <= j; :: from SCMFSA_7, 2005.02.05, A.T. theorem :: INT_1:52 for a,b being Integer st a < b holds a <= b - 1; :: from UNIFORM1, 2005.08.22, A.T. theorem :: INT_1:53 for r being Real st r>=0 holds [/ r \]>=0 & [\ r /]>=0 & [/ r \] is Element of NAT & [\ r /] is Element of NAT; :: from SCMFSA9A, 2005.11.16, A.T. theorem :: INT_1:54 for i being Integer, r being Real st i <= r holds i <= [\ r /]; theorem :: INT_1:55 for m,n being Nat holds 0 <= m qua Integer div n; :: from SCMFSA9A, 2006.03.14, A.T. theorem :: INT_1:56 0 < i & 1 < j implies i div j < i; :: from NEWTON, 2007.01.02, AK theorem :: INT_1:57 i2 >= 0 implies i1 mod i2 >= 0; theorem :: INT_1:58 i2 > 0 implies i1 mod i2 < i2; theorem :: INT_1:59 i2 <> 0 implies i1 = (i1 div i2) * i2 + (i1 mod i2); :: from AMI_3, 2007.06.14, A.T. theorem :: INT_1:60 for m,j being Integer holds m*j, 0 are_congruent_mod m; :: from AMI_4, 2007.06.14, A.T. theorem :: INT_1:61 i >= 0 & j >= 0 implies i div j >= 0; :: from INT_3, 2007.07.27, A.T. theorem :: INT_1:62 for n being Integer holds n > 0 implies for a being Integer holds a mod n = 0 iff n divides a; :: from JORDAN1D, 2007.07.27, A.T. reserve r, s for Real; theorem :: INT_1:63 r/s is not Integer implies - [\ r/s /] = [\ (-r) / s /] + 1; theorem :: INT_1:64 r/s is Integer implies - [\ r/s /] = [\ (-r) / s /]; :: missing, 2008.05.16, A.T. theorem :: INT_1:65 r <= i implies [/ r \] <= i; :: from POLYNOM2, 2010.02.13, A.T. scheme :: INT_1:sch 7 FinInd{M, N() -> Element of NAT, P[Nat]} : for i being Element of NAT st M() <= i & i <= N() holds P[i] provided P[M()] and for j being Element of NAT st M() <= j & j < N() holds P[j] implies P[j+1]; scheme :: INT_1:sch 8 FinInd2{M,N() -> Element of NAT, P[Nat]} : for i being Element of NAT st M() <= i & i <= N() holds P[i] provided P[M()] and for j being Element of NAT st M() <= j & j < N() holds (for j9 being Element of NAT st M() <= j9 & j9 <= j holds P[j9]) implies P[j+1]; :: from TOPREALA, 2011.04.27, A.T. reserve i for Integer, a, b, r, s for Real; theorem :: INT_1:66 frac(r+i) = frac r; theorem :: INT_1:67 r <= a & a < [\r/]+1 implies [\a/] = [\r/]; theorem :: INT_1:68 r <= a & a < [\r/]+1 implies frac r <= frac a; theorem :: INT_1:69 r < a & a < [\r/]+1 implies frac r < frac a; theorem :: INT_1:70 a >= [\r/]+1 & a <= r+1 implies [\a/] = [\r/]+1; theorem :: INT_1:71 a >= [\r/]+1 & a < r+1 implies frac a < frac r; theorem :: INT_1:72 r <= a & a < r+1 & r <= b & b < r+1 & frac a = frac b implies a = b; :: 28.05.2012, A.T. registration let i be Integer; reduce In(i,INT) to i; end; definition let x be Number; attr x is dim-like means :: INT_1:def 11 x = -1 or x is natural; end; registration cluster natural -> dim-like for object; cluster dim-like -> integer for object; cluster -1 -> dim-like for object; end; registration cluster dim-like for set; end; registration let d be dim-like object; cluster d + 1 -> natural; end; registration let k be dim-like object, n be non zero natural Number; cluster k+n -> natural; end; theorem :: INT_1:73 ::: INT_4:12 for i being Integer holds 0 = 0 mod i; theorem :: INT_1:74 :: moved from CHORD:1 for n being non zero Nat holds n-1 is Nat & 1 <= n;