   Jaskinie Podróże Nurki Grafika Mizar Teksty Kulinaria Lemkov Namiary Mapa RSS English   Spelunka Trybików Mizar Artykuły Liczby całkowite YAC Software    Wróć Mizar Eddie Artykuły Równoważność automatów deter ministycznych i epsilon niedeter ministycznych Etykietowane systemy tranzycji stanów Kwantyfikatory w wyrażeniach regularnych - co najmniej m wystąpień Systemy przepisywania słów Kwantyfikatory w wyrażeniach regularnych - od m do n wystąpień Języki formalne - konkatenacja i domknięcie Boole'owskie właściwości zbiorów Homomorfizmy i izomorfizmy grup; grupa ilorazowa Liczby całkowite Syntaktyka Mizara-MSE   Liczby całkowite W artykule wprowadzone zostały następujące pojęcia: zbiór liczb całkowitych i jego elementy, kongruencje, zaokrąglanie liczb rzeczywistych w dół i w górę, część ułamkowa liczby rzeczywistej, dzielenie całkowite i reszta dzielenia całkowitego. Dodane także następujące schematy: schemat rozdzielania, schemat indukcji całkowitej, schematy minimum i maksimum (istnienie najmniejszej i największej liczby całkowitej spełniającej zadaną własność). Identyfikator Mizar Mathematical Library: INT_1. Abstrakt w wersji PDF: tutaj. Białystok, 1990. Pliki: Abstrakt ```:: Integers :: by Micha{\l} J. Trybulec :: :: Received February 7, 1990 :: Copyright (c) 1990 Association of Mizar Users environ vocabularies ARYTM, ARYTM_1, ORDINAL2, NAT_1, ARYTM_3, RELAT_1, INT_1, BOOLE, COMPLEX1, ARYTM_2; 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, XREAL_0, REAL_1, NAT_1; registrations XREAL_0, ARYTM_3, REAL_1, ORDINAL2, NUMBERS, ZFMISC_1, XBOOLE_0, XCMPLX_0, NAT_1, XXREAL_0, ORDINAL1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve X,x,y,z for set, k,l,n,n1,n2 for Element of NAT, r for real number; 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 Real; cluster integer number; cluster -> integer Element of INT; end; definition mode Integer is integer number; end; canceled 6; theorem :: INT_1:7 for k being natural number st r = k or r = -k holds r is Integer; theorem :: INT_1:8 r is Integer implies ex k st r = k or r = - k; :: Relations between sets INT, NAT and REAL ( and their elements ) registration cluster -> integer Element of NAT; cluster natural -> integer number; end; registration cluster integer -> real number; end; reserve i,i0,i1,i2,i3,i4,i5,i7,i8,i9,j for Integer; :: Now we are ready to redefine some functions :: Redefinition of functions "+", "*" and "-" 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; :: More redefinitions registration let n be Element of NAT; cluster - n -> integer; let i1 be Integer; cluster i1 + n -> integer; cluster i1 * n -> integer; cluster i1 - n -> integer; end; registration let n1,n2; cluster n1 - n2 -> integer; end; :: Some basic theorems about integers canceled 7; theorem :: INT_1:16 0 <= i0 implies i0 in 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 in 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); 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]; :: abs and sgn functions with integers :: registration let r; :: cluster sgn r -> integer; :: coherence :: proof :: r < 0 or 0 < r or r = 0; :: hence thesis by ABSVALUE:def 2; :: end; :: end; 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 8; 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, 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; registration 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; begin :: Addenda :: from FSM_1 theorem :: INT_1:78 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:79 for a,b being Integer st a < b holds a <= b - 1; :: from UNIFORM1, 2005.08.22, A.T. theorem :: INT_1:80 for r being real number 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:81 for i being Integer, r being real number st i <= r holds i <= [\ r /]; theorem :: INT_1:82 for m,n being natural number holds 0 <= m qua Integer div n; :: from SCMFSA9A, 2006.03.14, A.T. theorem :: INT_1:83 0 < i & 1 < j implies i div j < i; :: from NEWTON, 2007.01.02, AK theorem :: INT_1:84 i2 >= 0 implies i1 mod i2 >= 0; theorem :: INT_1:85 i2 > 0 implies i1 mod i2 < i2; theorem :: INT_1:86 i2 <> 0 implies i1 = (i1 div i2) * i2 + (i1 mod i2);``` Góra Pełny artykuł ```:: Integers :: by Micha{\l} J. Trybulec :: :: Received February 7, 1990 :: Copyright (c) 1990 Association of Mizar Users environ vocabularies ARYTM, ARYTM_1, ORDINAL2, NAT_1, ARYTM_3, RELAT_1, INT_1, BOOLE, COMPLEX1, ARYTM_2; 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, XREAL_0, REAL_1, NAT_1; registrations XREAL_0, ARYTM_3, REAL_1, ORDINAL2, NUMBERS, ZFMISC_1, XBOOLE_0, XCMPLX_0, NAT_1, XXREAL_0, ORDINAL1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI, XBOOLE_0; theorems REAL_1, NAT_1, AXIOMS, TARSKI, XREAL_0, XCMPLX_0, XCMPLX_1, ZFMISC_1, XBOOLE_0, NUMBERS, ARYTM_0, ARYTM_2, ARYTM_1, XREAL_1, XXREAL_0, ORDINAL1; schemes NAT_1, XBOOLE_0, REAL_1; begin reserve X,x,y,z for set, k,l,n,n1,n2 for Element of NAT, r for real number; Lm1: z in [:{0},NAT:] \ {[0,0]} implies ex k st z = -k proof assume A1: z in [:{0},NAT:] \ {[0,0]}; then A2: z in [:{0},NAT:]; then consider x,y such that x in {0} and A3: y in NAT and A4: z = [x,y] by ZFMISC_1:103; reconsider y as Element of NAT by A3; take y; A5: z in NAT \/ [:{0},NAT:] by A2,XBOOLE_0:def 2; not z in {[0,0]} by A1,XBOOLE_0:def 4; then z in INT by A5,NUMBERS:def 4,XBOOLE_0:def 4; then reconsider z' = z as Element of REAL by NUMBERS:15; consider x1,x2,y1,y2 being Element of REAL such that A6: z' = [*x1,x2*] and A7: y = [*y1,y2*] and A8: z' + y = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4; A9: x2 = 0 by A6,ARYTM_0:26; then A10: z' = x1 by A6,ARYTM_0:def 7; A11: y2 = 0 by A7,ARYTM_0:26; then A12: y = y1 by A7,ARYTM_0:def 7; [:{0},NAT:] c= [:{0},REAL+:] by ARYTM_2:2,ZFMISC_1:118; then consider x',y' being Element of REAL+ such that A13: z' = [0,x'] and A14: y = y' and A15: +(z',y) = y' - x' by A2,A3,ARYTM_0:def 2,ARYTM_2:2; x' = y' by A4,A13,A14,ZFMISC_1:33; then A16: y' - x' = 0 by ARYTM_1:18; +(x2,y2) = 0 by A9,A11,ARYTM_0:13; then z' + y = 0 by A8,A10,A12,A15,A16,ARYTM_0:def 7; hence z = -y; end; Lm2: for k st x = -k & k <> x holds x in [:{0},NAT:] \ {[0,0]} proof let k such that A1: x = -k and A2: k <> x; reconsider r = x as Element of REAL by A1; r + k = 0 by A1; then consider x1,x2,y1,y2 being Element of REAL such that A3: r = [*x1,x2*] and A4: k = [*y1,y2*] and A5: 0 = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4; A6: k in omega; x2 = 0 by A3,ARYTM_0:26; then A7: x1 = r by A3,ARYTM_0:def 7; A8: y2 = 0 by A4,ARYTM_0:26; then A9: y1 = k by A4,ARYTM_0:def 7; +(x2,y2) = 0 by A5,ARYTM_0:26; then A10: +(x1,y1) = 0 by A5,ARYTM_0:def 7; reconsider y2 = k as Element of REAL; A11: now assume x1 in REAL+; then consider x',y' being Element of REAL+ such that A12: x1 = x' and A13: y1 = y' and A14: 0 = x' + y' by A6,A9,A10,ARYTM_0:def 2,ARYTM_2:2; x' = 0 & y' = 0 by A14,ARYTM_2:6; hence contradiction by A2,A3,A4,A8,A12,A13,ARYTM_0:26; end; r in REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1,XBOOLE_0:def 4; then x in [:{0},REAL+:] by A7,A11,XBOOLE_0:def 2; then consider x',y' being Element of REAL+ such that A15: x1 = [0,x'] and A16: y1 = y' and A17: 0 = y' - x' by A6,A7,A9,A10,ARYTM_0:def 2,ARYTM_2:2; A18: x' = y' by A17,ARYTM_0:6; 0 in {0} by TARSKI:def 1; then A19: x in [:{0},NAT:] by A7,A9,A15,A16,A18,ZFMISC_1:106; not r in {[0,0]} by NUMBERS:def 1,XBOOLE_0:def 4; hence x in [:{0},NAT:] \ {[0,0]} by A19,XBOOLE_0:def 4; end; definition redefine func INT means :Def1: x in it iff ex k st x = k or x = - k; compatibility proof let I be set; thus I = INT implies for x holds x in I iff ex k st x = k or x = - k proof assume A1: I = INT; let x; thus x in I implies ex k st x = k or x = - k proof assume A2: x in I; then A3: x in NAT \/ [:{0},NAT:] by A1,NUMBERS:def 4; A4: not x in {[0,0]} by A1,A2,NUMBERS:def 4,XBOOLE_0:def 4; per cases by A3,XBOOLE_0:def 2; suppose x in NAT; hence ex k st x = k or x = - k; end; suppose x in [:{0},NAT:]; then x in [:{0},NAT:] \ {[0,0]} by A4,XBOOLE_0:def 4; hence ex k st x = k or x = - k by Lm1; end; end; given k such that A5: x = k or x = - k; per cases by A5; suppose A6: x = k; then A7: x in NAT \/ [:{0},NAT:] by XBOOLE_0:def 2; not x in {[0,0]} by A6,NUMBERS:def 1,XBOOLE_0:def 4; hence x in I by A1,A7,NUMBERS:def 4,XBOOLE_0:def 4; end; suppose x = -k & k <> x; then A8: x in [:{0},NAT:] \ {[0,0]} by Lm2; then x in [:{0},NAT:]; then A9: x in NAT \/ [:{0},NAT:] by XBOOLE_0:def 2; not x in {[0,0]} by A8,XBOOLE_0:def 4; hence x in I by A1,A9,NUMBERS:def 4,XBOOLE_0:def 4; end; end; assume A10: for x holds x in I iff ex k st x = k or x = - k; thus I c= INT proof let x; assume x in I; then consider k such that A11: x = k or x = - k by A10; per cases by A11; suppose A12: x = k; then A13: x in NAT \/ [:{0},NAT:] by XBOOLE_0:def 2; not x in {[0,0]} by A12,NUMBERS:def 1,XBOOLE_0:def 4; hence x in INT by A13,NUMBERS:def 4,XBOOLE_0:def 4; end; suppose x = -k & k <> x; then A14: x in [:{0},NAT:] \ {[0,0]} by Lm2; then x in [:{0},NAT:]; then A15: x in NAT \/ [:{0},NAT:] by XBOOLE_0:def 2; not x in {[0,0]} by A14,XBOOLE_0:def 4; hence x in INT by A15,NUMBERS:def 4,XBOOLE_0:def 4; end; end; let x; assume A16: x in INT; then A17: x in NAT \/ [:{0},NAT:] by NUMBERS:def 4; A18: not x in {[0,0]} by A16,NUMBERS:def 4,XBOOLE_0:def 4; per cases by A17,XBOOLE_0:def 2; suppose x in NAT; hence x in I by A10; end; suppose x in [:{0},NAT:]; then x in [:{0},NAT:] \ {[0,0]} by A18,XBOOLE_0:def 4; then ex k st x = k or x = - k by Lm1; hence x in I by A10; end; end; end; definition let i be number; attr i is integer means :Def2: i in INT; end; registration cluster integer Real; existence proof take 0; thus 0 in INT by Def1; end; cluster integer number; existence proof take 0; thus 0 in INT by Def1; end; cluster -> integer Element of INT; coherence by Def2; end; definition mode Integer is integer number; end; canceled 6; theorem Th7: for k being natural number st r = k or r = -k holds r is Integer proof let k be natural number; A1: k in NAT by ORDINAL1:def 13; assume r = k or r = -k; then r in INT by A1,Def1; hence thesis by Def2; end; theorem Th8: r is Integer implies ex k st r = k or r = - k proof assume r is Integer; then r is Element of INT by Def2; hence thesis by Def1; end; :: Relations between sets INT, NAT and REAL ( and their elements ) registration cluster -> integer Element of NAT; coherence by Th7; cluster natural -> integer number; coherence proof let n be number; assume n is natural; then n is Element of NAT by ORDINAL1:def 13; hence thesis by Th7; end; end; Lm3: x in INT implies x in REAL by NUMBERS:15; registration cluster integer -> real number; coherence proof let n be number; assume n is integer; then n is Element of INT by Def2; then reconsider n as Element of REAL by Lm3; n is real; hence thesis; end; end; reserve i,i0,i1,i2,i3,i4,i5,i7,i8,i9,j for Integer; :: Now we are ready to redefine some functions :: Redefinition of functions "+", "*" and "-" registration let i1,i2 be Integer; cluster i1 + i2 -> integer; coherence proof consider k such that A1: (i1 = k or i1 = - k) by Th8; consider l such that A2: (i2 = l or i2 = - l) by Th8; A3: now assume i1 = k & i2 = l; then i1 + i2 = k + l; hence i1 + i2 is Integer; end; A4: now assume A5: i1 = k & i2 = - l; A6: now assume k - l <= 0; then k <= 0 + l by XREAL_1:22; then consider z being Nat such that A7: l = k + z by NAT_1:10; - z = - l + k by A7; hence k - l is Integer by Th7; end; now assume 0 <= k - l; then 0 + l <= k by XREAL_1:21; then consider z being Nat such that A8: k = l + z by NAT_1:10; thus k - l is Integer by A8; end; hence i1 + i2 is Integer by A5,A6; end; A9: now assume A10: i1 = - k & i2 = l; A11: now assume l - k <= 0; then l <= 0 + k by XREAL_1:22; then consider z being Nat such that A12: k = l + z by NAT_1:10; - z = - k + l by A12; hence l - k is Integer by Th7; end; now assume 0 <= l - k; then 0 + k <= l by XREAL_1:21; then consider z being Nat such that A13: l = k + z by NAT_1:10; thus l - k is Integer by A13; end; hence i1 + i2 is Integer by A10,A11; end; now assume i1 = - k & i2 = - l; then i1 + i2 = - (k + l); hence i1 + i2 is Integer by Th7; end; hence thesis by A1,A2,A3,A4,A9; end; cluster i1 * i2 -> integer; coherence proof consider k such that A14: (i1 = k or i1 = - k) by Th8; consider l such that A15: (i2 = l or i2 = - l) by Th8; A16: now assume i1 = k & i2 = l; then i1 * i2 = k * l; hence i1 * i2 is Integer; end; A17: now assume i1 = - k & i2 = - l; then i1 * i2 = k * l; hence i1 * i2 is Integer; end; now assume (i1 = - k & i2 = l) or (i1 = k & i2 = - l); then i1 * i2 = - (k * l); hence i1 * i2 is Integer by Th7; end; hence i1 * i2 is integer by A14,A15,A16,A17; end; end; registration let i0 be Integer; cluster - i0 -> integer; coherence proof consider k such that A1: i0 = k or i0 = - k by Th8; thus thesis by A1,Th7; end; end; registration let i1,i2 be Integer; cluster i1 - i2 -> integer; coherence proof i1 - i2 = i1 + (- i2); hence i1 - i2 is integer; end; end; :: More redefinitions registration let n be Element of NAT; cluster - n -> integer; coherence; let i1 be Integer; cluster i1 + n -> integer; coherence; cluster i1 * n -> integer; coherence; cluster i1 - n -> integer; coherence; end; registration let n1,n2; cluster n1 - n2 -> integer; coherence; end; :: Some basic theorems about integers canceled 7; theorem Th16: 0 <= i0 implies i0 in NAT proof assume A1: 0 <= i0; consider k such that A2: i0 = k or i0 = - k by Th8; i0 = - k implies i0 is Element of NAT by A1,XXREAL_0:1; hence thesis by A2; end; theorem r is Integer implies r + 1 is Integer & r - 1 is Integer proof assume r is Integer; then reconsider i1 = r as Integer; i1 + 1 is Integer & i1 - 1 is Integer; hence thesis; end; theorem Th18: i2 <= i1 implies i1 - i2 in NAT proof assume i2 <= i1; then i2 - i2 <= i1 - i2 by XREAL_1:11; hence thesis by Th16; end; theorem Th19: i1 + k = i2 implies i1 <= i2 proof now assume A1: i1 + k = i2; reconsider i0 = k as Integer; 0 + (i1 + k) <= k + i2 by A1,XREAL_1:8; then i1 + i0 - i0 <= i2 + i0 - i0 by XREAL_1:11; hence thesis; end; hence thesis; end; Lm4: for j being Element of NAT holds j < 1 implies j = 0 proof let j be Element of NAT; assume j < 1; then j < 0 + 1; then A1: j <= 0 by NAT_1:13; assume j <> 0; hence thesis by A1; end; Lm5: 0 < i1 implies 1 <= i1 proof assume A1: 0 < i1; then reconsider i2 = i1 as Element of NAT by Th16; 0 <> i2 by A1; hence thesis by Lm4; end; theorem Th20: i0 < i1 implies i0 + 1 <= i1 proof assume i0 < i1; then i0 + (- i0) < i1 + (- i0) by XREAL_1:8; then 1 <= i1 + (- i0) by Lm5; then 1 + i0 <= i1 + (- i0) + i0 by XREAL_1:8; hence thesis; end; theorem Th21: i1 < 0 implies i1 <= - 1 proof assume i1 < 0; then 0 < - i1 by XREAL_1:60; then 1 <= - i1 by Lm5; then - - i1 <= - 1 by XREAL_1:26; hence i1 <= - 1; end; theorem Th22: i1 * i2 = 1 iff (i1 = 1 & i2 = 1) or (i1 = - 1 & i2 = - 1) proof thus i1 * i2 = 1 implies (i1 = 1 & i2 = 1) or (i1 = - 1 & i2 = - 1) proof assume A1: i1 * i2 = 1; then A2: not(i1 = 0 or i2 = 0); A3: now assume 0 < i1 & 0 < i2; then i1 is Element of NAT & i2 is Element of NAT by Th16; hence i1 = 1 & i2 = 1 by A1,NAT_1:15; end; now assume i1 < 0 & i2 < 0; then 0 <= - i1 & 0 <= - i2 by XREAL_1:60; then A4: (- i1) is Element of NAT & (- i2) is Element of NAT by Th16; (- i1) * (- i2) = i1 * i2; then - (- i1) = - 1 & - (- i2) = - 1 by A1,A4,NAT_1:15; hence i1 = - 1 & i2 = - 1; end; hence thesis by A1,A2,A3,XREAL_1:134; end; thus thesis; end; theorem i1 * i2 = - 1 iff (i1 = - 1 & i2 = 1) or (i1 = 1 & i2 = - 1) proof thus i1 * i2 = - 1 implies (i1 = - 1 & i2 = 1) or (i1 = 1 & i2 = - 1) proof assume A1: i1 * i2 = - 1; (- i1) * i2 = 1 by A1; then A2: (- (- i1) = - 1 & i2 = 1) or (- i1 = - 1 & i2 = - 1) by Th22; thus thesis by A2; end; assume (i1 = - 1 & i2 = 1) or (i1 = 1 & i2 = - 1); hence thesis; end; Lm6: i0 <= i1 implies ex k st i0 + k = i1 proof assume i0 <= i1; then reconsider k = i1 - i0 as Element of NAT by Th18; i0 + k = i1; hence thesis; end; Lm7: i0 <= i1 implies ex k st i1 - k = i0 proof assume i0 <= i1; then reconsider k = i1 - i0 as Element of NAT by Th18; i1 - k = i0; hence thesis; end; Lm8: r - 1 < r by XREAL_1:148; scheme SepInt { P[Integer] } : ex X being Subset of INT st for x being Integer holds x in X iff P[x] proof defpred P1[set] means ex i0 st i0 = \$1 & P[i0]; consider X such that A1: for y holds y in X iff y in INT & P1[y] from XBOOLE_0:sch 1; X is Subset of INT proof y in X implies y in INT by A1; hence thesis by TARSKI:def 3; end; then reconsider X as Subset of INT; take X; let i0; A2: i0 in X implies P[i0] proof assume i0 in X; then ex i1 st i0 = i1 & P[i1] by A1; hence thesis; end; P[i0] implies i0 in X proof assume A3: P[i0]; i0 in INT by Def2; hence thesis by A1,A3; end; hence thesis by A2; end; scheme IntIndUp { F() -> Integer, P[Integer] } : for i0 st F() <= i0 holds P[i0] provided A1: P[F()] and A2: for i2 st F() <= i2 holds P[i2] implies P[i2 + 1] proof let i0; assume A3: F() <= i0; defpred Q[natural number] means for i2 st \$1 = i2 - F() holds P[i2]; A4: Q by A1; A5: for k st Q[k] holds Q[k + 1] proof let k; reconsider i8 = k as Integer; assume A6: Q[k]; let i2; assume A7: k + 1 = i2 - F(); then k = i2 - 1 - F(); then A8: P[i2 - 1] by A6; F() <= i2 - 1 proof i2 - 1 = i8 + F() by A7; hence thesis by Th19; end; then P[i2 - 1 + 1] by A2,A8; hence thesis; end; A9: for k holds Q[k] from NAT_1:sch 1(A4,A5); reconsider l = i0 - F() as Element of NAT by A3,Th18; l = i0 - F(); hence P[i0] by A9; end; scheme IntIndDown { F() -> Integer, P[Integer] } : for i0 st i0 <= F() holds P[i0] provided A1: P[F()] and A2: for i2 st i2 <= F() holds P[i2] implies P[i2 - 1] proof let i0; assume A3: i0 <= F(); defpred Q[Integer] means for i2 st \$1 = - i2 holds P[i2]; A4: Q[- F()] by A1; A5: for i2 st - F() <= i2 holds Q[i2] implies Q[i2 + 1] proof let i2; assume that A6: - F() <= i2 and A7: Q[i2]; let i3; assume A8: i2 + 1 = - i3; then - i3 - 1 = i2; then i2 = - (i3 + 1); then A9: P[i3 + 1] by A7; i3 + 1 <= F() proof i2 = - i3 - 1 by A8; then - (- i3 - 1) <= - (- F()) by A6,XREAL_1:26; hence thesis; end; then P[i3 + 1 - 1] by A2,A9; hence thesis; end; A10: for i2 st - F() <= i2 holds Q[i2] from IntIndUp(A4,A5); - F() <= - i0 by A3,XREAL_1:26; hence thesis by A10; end; scheme IntIndFull { F() -> Integer, P[Integer] } : for i0 holds P[i0] provided A1: P[F()] and A2: for i2 holds P[i2] implies P[i2 - 1] & P[i2 + 1] proof A3:P[F()] by A1; let i0; A4: now assume A5: F() <= i0; A6: for i2 st F() <= i2 holds P[i2] implies P[i2 + 1] by A2; for i2 st F() <= i2 holds P[i2] from IntIndUp(A3,A6); hence P[i0] by A5; end; now assume A7: i0 <= F(); A8: for i2 st i2 <= F() holds P[i2] implies P[i2 - 1] by A2; for i2 st i2 <= F() holds P[i2] from IntIndDown(A3,A8); hence P[i0] by A7; end; hence thesis by A4; end; scheme IntMin { F() -> Integer, P[Integer] } : ex i0 st P[i0] & for i1 st P[i1] holds i0 <= i1 provided A1: for i1 st P[i1] holds F() <= i1 and A2: ex i1 st P[i1] proof consider i1 such that A3: P[i1] by A2; F() <= i1 by A1,A3; then A4: ex k st F() + k = i1 by Lm6; defpred Q[natural number] means P[F() + \$1]; A5: ex k st Q[k] by A3,A4; consider l such that A6: Q[l] & for n st Q[n] holds l <= n from NAT_1:sch 5 (A5); take i0 = F() + l; for i1 st P[i1] holds i0 <= i1 proof let i1; assume A7: P[i1]; then F() <= i1 by A1; then consider n such that A8: F() + n = i1 by Lm6; i0 - F() <= i1 - F() by A6,A7,A8; hence i0 <= i1 by XREAL_1:11; end; hence thesis by A6; end; scheme IntMax { F() -> Integer, P[Integer] } : ex i0 st P[i0] & for i1 st P[i1] holds i1 <= i0 provided A1: for i1 st P[i1] holds i1 <= F() and A2: ex i1 st P[i1] proof consider i1 such that A3: P[i1] by A2; i1 <= F() by A1,A3; then A4: ex k st i1 = F() - k by Lm7; defpred Q[natural number] means P[F() - \$1]; A5: ex k st Q[k] by A3,A4; consider l such that A6: Q[l] & for n st Q[n] holds l <= n from NAT_1:sch 5 (A5); take i0 = F() - l; for i1 st P[i1] holds i1 <= i0 proof let i1; assume A7: P[i1]; then i1 <= F() by A1; then consider n such that A8: F() - n = i1 by Lm7; l <= n by A6,A7,A8; then F() + (- i0) - F() <= F() - i1 - F() by A8,XREAL_1:11; then - i0 <= F() + (- i1) - F(); hence i1 <= i0 by XREAL_1:26; end; hence thesis by A6; end; :: abs and sgn functions with integers :: registration let r; :: cluster sgn r -> integer; :: coherence :: proof :: r < 0 or 0 < r or r = 0; :: hence thesis by ABSVALUE:def 2; :: end; :: end; definition let i1,i2,i3 be Integer; pred i1,i2 are_congruent_mod i3 means :Def3: ex i4 st i3 * i4 = i1 - i2; end; canceled 8; theorem i1,i1 are_congruent_mod i2 proof i2 * 0 = i1 - i1; hence thesis by Def3; end; theorem i1,0 are_congruent_mod i1 & 0,i1 are_congruent_mod i1 proof i1 * 1 = i1 - 0 & i1 * (- 1) = 0 - i1; hence thesis by Def3; end; theorem i1,i2 are_congruent_mod 1 proof i1 - i2 = 1 * (i1 - i2); hence thesis by Def3; end; theorem i1,i2 are_congruent_mod i3 implies i2,i1 are_congruent_mod i3 proof assume i1,i2 are_congruent_mod i3; then consider i0 such that A1: (i1 - i2) = i3 * i0 by Def3; i2 - i1 = i3 * (- i0) by A1; hence thesis by Def3; end; theorem i1,i2 are_congruent_mod i5 & i2,i3 are_congruent_mod i5 implies i1,i3 are_congruent_mod i5 proof assume A1: i1,i2 are_congruent_mod i5 & i2,i3 are_congruent_mod i5; then consider i8 such that A2: i5 * i8 = i1 - i2 by Def3; consider i9 such that A3: i5 * i9 = i2 - i3 by A1,Def3; (i5 * i8) + (i5 * i9) = i1 - i3 by A2,A3; then i5 * (i8 + i9) = i1 - i3; hence thesis by Def3; end; theorem i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 implies (i1 + i3),(i2 + i4) are_congruent_mod i5 proof assume A1: i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5; then consider i8 such that A2: i5 * i8 = i1 - i2 by Def3; consider i9 such that A3: i5 * i9 = i3 - i4 by A1,Def3; (i5 * i8) + (i5 * i9) = (i1 + i3) - (i2 + i4) by A2,A3; then i5 * (i8 + i9) = (i1 + i3) - (i2 + i4); hence thesis by Def3; end; theorem i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 implies (i1 - i3),(i2 - i4) are_congruent_mod i5 proof assume A1: i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5; then consider i8 such that A2: i5 * i8 = i1 - i2 by Def3; consider i9 such that A3: i5 * i9 = i3 - i4 by A1,Def3; ex i7 st i5 * i7 = (i1 - i3) - (i2 - i4) proof (i1 - i3) - (i2 - i4) = i5 * (i8 - i9) by A2,A3; hence thesis; end; hence thesis by Def3; end; theorem i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 implies (i1 * i3),(i2 * i4) are_congruent_mod i5 proof assume A1: i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5; then consider i8 such that A2: i5 * i8 = i1 - i2 by Def3; consider i9 such that A3: i5 * i9 = i3 - i4 by A1,Def3; ex i7 st i5 * i7 = (i1 * i3) - (i2 * i4) proof (i1 * i3) - (i2 * i4) = (i1 - i2) * i3 + (i3 - i4) * i2 .= (i5 * i8) * i3 + (i5 * i9) * i2 by A2,A3 .= i5 * ((i8 * i3) + (i9 * i2)); hence thesis; end; hence thesis by Def3; end; theorem (i1 + i2),i3 are_congruent_mod i5 iff i1, (i3 - i2) are_congruent_mod i5 proof thus (i1 + i2),i3 are_congruent_mod i5 implies i1,(i3 - i2) are_congruent_mod i5 proof assume (i1 + i2),i3 are_congruent_mod i5; then A1: ex i0 st i5 * i0 = (i1 + i2) - i3 by Def3; (i1 + i2) - i3 = i1 - (i3 - i2); hence thesis by A1,Def3; end; assume i1, (i3 - i2) are_congruent_mod i5; then A2: ex i0 st i5 * i0 = i1 - (i3 - i2) by Def3; i1 - (i3 - i2) = (i1 + i2) - i3; hence thesis by A2,Def3; end; theorem i4 * i5 = i3 implies (i1,i2 are_congruent_mod i3 implies i1,i2 are_congruent_mod i4) proof assume A1: i4 * i5 = i3; assume i1,i2 are_congruent_mod i3; then consider i0 such that A2: i3 * i0 = i1 - i2 by Def3; i1 - i2 = i4 * (i5 * i0) by A1,A2; hence thesis by Def3; end; theorem i1,i2 are_congruent_mod i5 iff (i1 + i5),i2 are_congruent_mod i5 proof thus i1,i2 are_congruent_mod i5 implies (i1 + i5),i2 are_congruent_mod i5 proof assume i1,i2 are_congruent_mod i5; then consider i0 such that A1: i5 * i0 = i1 - i2 by Def3; (i5 * i0) + (i5 * 1) = (i1 + i5) - i2 by A1; then i5 * (i0 + 1) = (i1 + i5) - i2 & (i0 + 1) is Integer; hence thesis by Def3; end; assume (i1 + i5),i2 are_congruent_mod i5; then consider i0 such that A2: i5 * i0 = (i1 + i5) - i2 by Def3; (i5 * i0) - (i5 * 1) = i1 - i2 by A2; then i5 * (i0 - 1) = i1 - i2 & (i0 - 1) is Integer; hence thesis by Def3; end; theorem i1,i2 are_congruent_mod i5 iff (i1 - i5),i2 are_congruent_mod i5 proof thus i1,i2 are_congruent_mod i5 implies (i1 - i5),i2 are_congruent_mod i5 proof assume i1,i2 are_congruent_mod i5; then consider i0 such that A1: i5 * i0 = i1 - i2 by Def3; (i5 * i0) - (i5 * 1) = (i1 - i5) - i2 by A1; then i5 * (i0 - 1) = (i1 - i5) - i2 & (i0 - 1) is Integer; hence thesis by Def3; end; assume (i1 - i5),i2 are_congruent_mod i5; then consider i0 such that A2: i5 * i0 = (i1 - i5) - i2 by Def3; (i5 * i0) + (i5 * 1) = i1 - i2 by A2; then i5 * (i0 + 1) = i1 - i2 & (i0 + 1) is Integer; hence thesis by Def3; end; theorem Th44: (i1 <= r & r - 1 < i1) & (i2 <= r & r - 1 < i2) implies i1 = i2 proof assume A1: (i1 <= r & r - 1 < i1) & (i2 <= r & r - 1 < i2); i2 = i1 + (i2 - i1); then consider i0 such that A2: i2 = i1 + i0; A3: i0 = 0 implies i2 = i1 by A2; A4: now assume i0 < 0 & i1 <> i2; then i0 <= - 1 by Th21; then i1 + i0 <= r + (- 1) by A1,XREAL_1:9; hence contradiction by A1,A2; end; now assume 0 < i0 & i1 <> i2; then 1 <= i0 by Lm5; then r - 1 + 1 < i1 + i0 by A1,XREAL_1:10; hence contradiction by A1,A2; end; hence thesis by A3,A4; end; theorem Th45: (r <= i1 & i1 < r + 1) & (r <= i2 & i2 < r + 1) implies i1 = i2 proof assume A1: (r <= i1 & i1 < r + 1) & (r <= i2 & i2 < r + 1); i2 = i1 + (i2 - i1); then consider i0 such that A2: i2 = i1 + i0; A3: i0 = 0 implies i2 = i1 by A2; A4: now assume i0 < 0 & i1 <> i2; then i0 <= - 1 by Th21; then i1 + i0 < r + 1 + (- 1) by A1,XREAL_1:10; hence contradiction by A1,A2; end; now assume 0 < i0 & i1 <> i2; then 1 <= i0 by Lm5; hence contradiction by A1,A2,XREAL_1:9; end; hence thesis by A3,A4; end; reserve r1,p,p1,g,g1,g2 for real number, Y for Subset of REAL; Lm9:for r ex n st r Integer means :Def4: it <= r & r - 1 < it; existence proof consider n such that A1: - r < n by Lm9; A2: - n < -- r by A1,XREAL_1:26; defpred P[Integer] means r < \$1; A3: for i1 st P[i1] holds -n <= i1 proof let i1; assume r < i1; then r + -n < i1 + r by A2,XREAL_1:10; hence -n <= i1 by XREAL_1:8; end; consider n such that A4: r < n by Lm9; reconsider i0 = n as Integer; r < i0 by A4; then A5: ex i0 st P[i0]; consider i1 such that A6: P[i1] & for i2 st P[i2] holds i1 <= i2 from IntMin(A3,A5); A7: r < i1 - 1 implies i1 <= i1-1 by A6; r - 1 < i1 - 1 by A6,XREAL_1:11; hence thesis by A7,Lm8; end; uniqueness by Th44; end; canceled; theorem Th47: [\ r /] = r iff r is integer proof r is Integer implies [\ r /] = r proof r + 0 < r + 1 by XREAL_1:8; then A1: r - 1 < r + 1 - 1 by XREAL_1:11; assume r is Integer; hence thesis by A1,Def4; end; hence thesis; end; theorem Th48: [\ r /] < r iff r is not integer proof now assume A1: not r is Integer; [\ r /] <= r by Def4; hence [\ r /] < r by A1,REAL_1:def 5; end; hence thesis by Th47; end; canceled; theorem [\ r /] - 1 < r & [\ r /] < r + 1 proof [\ r /] <= r by Def4; then A1: [\ r /] + 0 < r + 1 by XREAL_1:10; then [\ r /] + (- 1) < r + 1 + (- 1) by XREAL_1:8; hence thesis by A1; end; theorem Th51: [\ r /] + i0 = [\ r + i0 /] proof A1: r - 1 < [\ r /] & [\ r /] <= r by Def4; then r - 1 + i0 < [\ r /] + i0 by XREAL_1:8; then A2: r + i0 - 1 < [\ r /] + i0; [\ r /] + i0 <= r + i0 by A1,XREAL_1:8; hence thesis by A2,Def4; end; theorem Th52: r < [\ r /] + 1 proof r - 1 < [\ r /] by Def4; then r - 1 + 1 < [\ r /] + 1 by XREAL_1:8; hence r < [\ r /] + 1; end; definition let r be real number; func [/ r \] -> Integer means :Def5: r <= it & it < r + 1; existence proof A1: now assume A2: r is Integer; r + 0 < r + 1 by XREAL_1:8; hence r <= [\ r /] & [\ r /] < r + 1 by A2,Th47; end; now assume not r is Integer; then [\ r /] < r by Th48; hence r <= [\ r /] + 1 & [\ r /] + 1 < r + 1 by Th52,XREAL_1:8; end; hence thesis by A1; end; uniqueness by Th45; end; canceled; theorem Th54: [/ r \] = r iff r is integer proof r is Integer implies [/ r \] = r proof r + 0 < r + 1 by XREAL_1:8; hence thesis by Def5; end; hence thesis; end; theorem Th55: r < [/ r \] iff r is not integer proof now assume A1: not r is Integer; r <= [/ r \] by Def5; hence r < [/ r \] by A1,REAL_1:def 5; end; hence thesis by Th54; end; canceled; theorem r - 1 < [/ r \] & r < [/ r \] + 1 proof r <= [/ r \] by Def5; then A1: r + 0 < [/ r \] + 1 by XREAL_1:10; then r + (- 1) < [/ r \] + 1 + (- 1) by XREAL_1:8; hence thesis by A1; end; theorem [/ r \] + i0 = [/ r + i0 \] proof A1: r <= [/ r \] & [/ r \] < r + 1 by Def5; then [/ r \] + i0 < r + 1 + i0 by XREAL_1:8; then A2: [/ r \] + i0 < r + i0 + 1; r + i0 <= [/ r \] + i0 by A1,XREAL_1:8; hence thesis by A2,Def5; end; theorem Th59: [\ r /] = [/ r \] iff r is integer proof A1: now assume r is Integer; hence [\ r /] = r & r = [/ r \] by Th47,Th54; hence [\ r /] = [/ r \]; end; now assume not r is Integer; then [\ r /] < r & r < [/ r \] by Th48,Th55; hence [\ r /] <> [/ r \]; end; hence thesis by A1; end; theorem Th60: [\ r /] < [/ r \] iff r is not integer proof now assume not r is Integer; then [\ r /] < r & r < [/ r \] by Th48,Th55; hence [\ r /] < [/ r \] by XXREAL_0:2; end; hence thesis by Th59; end; theorem [\ r /] <= [/ r \] proof [\ r /] <= r & r <= [/ r \] by Def4,Def5; hence thesis by XXREAL_0:2; end; theorem [\ ([/ r \]) /] = [/ r \] by Th47; theorem [\ ([\ r /]) /] = [\ r /] by Th47; theorem [/ ([/ r \]) \] = [/ r \] by Th54; theorem [/ ([\ r /]) \] = [\ r /] by Th54; theorem [\ r /] = [/ r \] iff not [\ r /] + 1 = [/ r \] proof set Diff = [/ r \] + (- [\ r /]); reconsider i0 = 1 as Integer; A1: now assume r is Integer; then [\ r /] = [/ r \] by Th59; hence [\ r /] = [/ r \] & [\ r /] + 1 <> [/ r \]; end; now assume not r is Integer; then [\ r /] < [/ r \] by Th60; then [\ r /] + (- [\ r /]) < Diff by XREAL_1:8; then A2: 1 <= Diff by Lm5; A3: [/ r \] < r + 1 by Def5; r - 1 < [\ r /] by Def4; then - [\ r /] < - (r - 1) by XREAL_1:26; then Diff < r + 1 + (- (r - 1)) by A3,XREAL_1:10; then Diff + 1 + (- 1) <= 1 + 1 + (- 1) by Th20; then [\ r /] + 1 = [\ r /] + Diff by A2,XXREAL_0:1; hence [\ r /] + 1 = [/ r \] & [\ r /] <> [/ r \]; end; hence thesis by A1; end; definition let r be real number; func frac r equals r - [\ r /]; coherence; end; registration let r be real number; cluster frac r -> real; coherence; end; definition let r be real number; redefine func frac r -> Real; coherence by XREAL_0:def 1; end; canceled; theorem r = [\ r /] + frac r; theorem Th69: frac r < 1 & 0 <= frac r proof A1: r - 1 < [\ r /] & [\ r /] <= r by Def4; then frac r + (r - 1) < r - [\ r /] + [\ r /] by XREAL_1:8; then frac r + (- 1) + r - r < r - r by XREAL_1:11; then A2: frac r - 1 + 1 < 0 + 1 by XREAL_1:8; [\ r /] + (r - [\ r /]) <= r + frac r by A1,XREAL_1:8; then r - r <= r + frac r - r by XREAL_1:11; hence thesis by A2; end; theorem [\ frac r /] = 0 proof [\ frac r /] = [\ (r + (- [\ r /])) /] .= [\ r /] + (- [\ r /]) by Th51 .= 0; hence thesis; end; theorem Th71: frac r = 0 iff r is integer proof A1: now assume r is Integer; then A2: r = [\ r /] by Th47; thus frac r = 0 by A2; end; thus thesis by A1; end; theorem 0 < frac r iff r is not integer proof now assume not r is Integer; then 0 <> frac r; hence 0 < frac r by Th69; end; hence thesis by Th71; end; :: Functions div and mod definition let i1,i2 be Integer; func i1 div i2 -> Integer equals [\ i1 / i2 /]; correctness; end; definition let i1,i2 be Integer; func i1 mod i2 -> Integer equals :Def8: i1 - (i1 div i2) * i2 if i2 <> 0 otherwise 0; correctness; end; :: The divisibility relation definition let i1,i2 be Integer; pred i1 divides i2 means ex i3 st i2 = i1 * i3; reflexivity proof let a be Integer; reconsider x = 1 as Integer; take x; thus thesis; end; end; canceled; theorem Th74: for r being real number st r <> 0 holds [\ r / r /] = 1 proof let r be real number; assume r <> 0; hence [\ r / r /] = [\ 1 /] by XCMPLX_1:60 .= 1 by Th47; end; theorem for i being Integer holds i div 0 = 0 proof let i be Integer; A1: 0 - 1 < 0; i / 0 = i * 0" by XCMPLX_0:def 9 .= i * 0; then [\ i / 0 /] = 0 by A1,Def4; hence thesis; end; theorem Th76: for i being Integer st i <> 0 holds i div i = 1 by Th74; theorem for i being Integer holds i mod i = 0 proof let i be Integer; per cases; suppose i = 0; hence i mod i = 0 by Def8; end; suppose A1:i <> 0; hence i mod i = i - (i div i) * i by Def8 .= i - 1 * i by A1,Th76 .= 0; end; end; begin :: Addenda :: from FSM_1 theorem k < i implies ex j being Element of NAT st j = i-k & 1 <= j proof assume k < i; then A1: k - k < i - k by XREAL_1:11; then A2: 0 < i - k; reconsider j = i - k as Element of NAT by A1,Th16; take j; thus j = i - k; reconsider j' = j, 0' = 0 as Integer; 0' + 1 <= j' by A2,Th20; hence 1 <= j; end; :: from SCMFSA_7, 2005.02.05, A.T. theorem for a,b being Integer st a < b holds a <= b - 1 proof let a,b be Integer; assume a < b; then a - 1 < b - 1 by XREAL_1:11; then a - 1 + 1 <= b - 1 by Th20; hence thesis; end; :: from UNIFORM1, 2005.08.22, A.T. theorem for r being real number st r>=0 holds [/ r \]>=0 & [\ r /]>=0 & [/ r \] is Element of NAT & [\ r /] is Element of NAT proof let r be real number;assume A1:r>=0; r-1<[\ r /] by Def4; then r-1+1<[\ r /]+1 by XREAL_1:8; then 0-1<[\ r /]+1-1 by A1,XREAL_1:11; then A2:[\ r /]>=0 by Th21; r<=[/ r \] by Def5; hence thesis by A1,A2,Th16; end; :: from SCMFSA9A, 2005.11.16, A.T. theorem Th81: for i being Integer, r being real number st i <= r holds i <= [\ r /] proof let i be Integer; let r be real number; assume A1: i <= r; A2: r-1 < [\ r /] by Def4; i-1 <= r-1 by A1,XREAL_1:11; then i-1 < [\ r /] by A2,XXREAL_0:2; then i-1+1 <= [\ r /] by Th20; hence i <= [\ r /]; end; theorem for m,n being natural number holds 0 <= m qua Integer div n by Th81; :: from SCMFSA9A, 2006.03.14, A.T. theorem 0 < i & 1 < j implies i div j < i proof assume that A1: 0 < i and A2: 1 < j; A3: 0 <= j by A2; A4: j <> 0 by A2; assume A5: i <= i div j; then 0 < i div j by A1; then A6: 0 < (i div j)" by XREAL_1:124; i div j <= i/j by Def4; then j * (i div j) <= j * (i/j) by A3,XREAL_1:66; then j * (i div j) <= i by A4,XCMPLX_1:88; then j * (i div j) <= i div j by A5,XXREAL_0:2; then j * (i div j) * (i div j)" <= (i div j) * (i div j)" by A6,XREAL_1:66; then j * ((i div j) * (i div j)") <= (i div j) * (i div j)"; then j * 1 <= (i div j) * (i div j)" by A1,A5,XCMPLX_0:def 7; hence contradiction by A1,A2,A5,XCMPLX_0:def 7; end; :: from NEWTON, 2007.01.02, AK theorem i2 >= 0 implies i1 mod i2 >= 0 proof assume A1:i2 >= 0; per cases by A1; suppose A2:i2 > 0; [\ i1/i2 /] <= i1/i2 by Def4; then (i1 div i2)*i2 <= (i1/i2)*i2 by A2,XREAL_1:66; then (i1 div i2)*i2 <= i1 by A2,XCMPLX_1:88; then i1 - (i1 div i2)*i2 >= 0 by XREAL_1:50; hence thesis by A2,Def8; end; suppose i2 = 0; hence thesis by Def8; end; end; theorem i2 > 0 implies i1 mod i2 < i2 proof assume A1: i2 > 0; i1/i2 -1 < [\ i1/i2 /] by Def4; then (i1/i2 -1)*i2 < (i1 div i2)*i2 by A1,XREAL_1:70; then i1/i2*i2 -1*i2 < (i1 div i2)*i2; then i1 -i2 < (i1 div i2)*i2-0 by A1,XCMPLX_1:88; then i1 -(i1 div i2)*i2 < i2-0 by XREAL_1:19; hence thesis by A1,Def8; end; theorem i2 <> 0 implies i1 = (i1 div i2) * i2 + (i1 mod i2) proof assume i2 <> 0; then (i1 div i2) * i2 +(i1 mod i2) = (i1 div i2 )*i2 + (i1 - ( i1 div i2 )*i2 ) by Def8 .= i1; hence thesis; end;``` Góra