:: Integers
:: by Micha{\l} J. Trybulec
::
:: Received February 7, 1990
:: Copyright (c) 1990-2026 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, SQUARE_1;
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,
SQUARE_1;
constructors FUNCT_4, ARYTM_1, ARYTM_0, XXREAL_0, REAL_1, NAT_1, FINSET_1,
CARD_1, XREAL_0, NUMBERS, SQUARE_1;
registrations ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, CARD_1, SQUARE_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, SQUARE_1;
expansions XXREAL_0;
theorems 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, XTUPLE_0, SUBSET_1, SQUARE_1;
schemes NAT_1, XBOOLE_0, SUBSET_1;
begin
reserve X for set, x,y,z for object,
k,l,n for Nat,
r for Real;
Lm1: z in [:{0},NAT:] \ {[0,0]} implies ex k st z = -k
proof
A1: [:{0},NAT:] c= [:{0},REAL+:] by ARYTM_2:2,ZFMISC_1:95;
assume
A2: z in [:{0},NAT:] \ {[0,0]};
then
A3: not z in {[0,0]} by XBOOLE_0:def 5;
z in NAT \/ [:{0},NAT:] by A2,XBOOLE_0:def 3;
then z in INT by A3,NUMBERS:def 4,XBOOLE_0:def 5;
then reconsider z9 = z as Element of REAL by NUMBERS:15;
consider x,y being object such that
x in {0} and
A4: y in NAT and
A5: z = [x,y] by A2,ZFMISC_1:84;
reconsider y as Element of REAL by A4, NUMBERS:19;
z in [:{0},NAT:] by A2;
then consider x9,y9 being Element of REAL+ such that
A6: z9 = [0,x9] and
A7: y = y9 and
A8: +(z9,y) = y9 - x9 by A4,A1,ARYTM_0:def 1,ARYTM_2:2;
x9 = y9 by A5,A6,A7,XTUPLE_0:1;
then
A9: y9 - x9 = 0 by ARYTM_1:18;
reconsider y as Element of NAT by A4;
take y;
consider x1,x2,y1,y2 being Element of REAL such that
A10: z9 = [*x1,x2*] and
A11: y = [*y1,y2*] and
A12: z9 + y = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4;
A13: x2 = 0 by A10,ARYTM_0:24;
then
A14: +(x2,y2) = 0 by A11,ARYTM_0:11,24;
y2 = 0 by A11,ARYTM_0:24;
then
A15: y = y1 by A11,ARYTM_0:def 5;
z9 = x1 by A10,A13,ARYTM_0:def 5;
then z9 + y = 0 by A12,A15,A8,A9,A14,ARYTM_0:def 5;
hence thesis;
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,XREAL_0:def 1;
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 NAT by ORDINAL1:def 12;
then k in REAL by NUMBERS:19;
then
A7: y2 = 0 by A4,ARYTM_0:24;
then
A8: y1 = k by A4,ARYTM_0:def 5;
+(x2,y2) = In(0,REAL) by A5,ARYTM_0:24;
then
A9: +(x1,y1) = 0 by A5,ARYTM_0:def 5;
A10: now
assume x1 in REAL+;
then consider x9,y9 being Element of REAL+ such that
A11: x1 = x9 and
A12: y1 = y9 and
A13: 0 = x9 + y9 by A6,A8,A9,ARYTM_0:def 1,ARYTM_2:2;
A14: y9 = 0 by A13,ARYTM_2:5;
x9 = 0 by A13,ARYTM_2:5;
hence contradiction by A2,A3,A4,A7,A11,A12,A14,ARYTM_0:24;
end;
x2 = 0 by A3,ARYTM_0:24;
then
A15: x1 = r by A3,ARYTM_0:def 5;
r in REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1,XBOOLE_0:def 5;
then x in [:{0},REAL+:] by A15,A10,XBOOLE_0:def 3;
then consider x9,y9 being Element of REAL+ such that
A16: x1 = [0,x9] and
A17: y1 = y9 and
A18: 0 = y9 - x9 by A6,A15,A8,A9,ARYTM_0:def 1,ARYTM_2:2;
A19: 0 in {0} by TARSKI:def 1;
A20: not r in {[0,0]} by NUMBERS:def 1,XBOOLE_0:def 5;
x9 = y9 by A18,ARYTM_0:6;
then x in [:{0},NAT:] by A15,A8,A16,A17,A19,ZFMISC_1:87,A6;
hence thesis by A20,XBOOLE_0:def 5;
end;
definition
redefine func INT means :: redefines INT (NUMBERS, definition)
: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: not x in {[0,0]} by A1,NUMBERS:def 4,XBOOLE_0:def 5;
per cases by A1,A2,NUMBERS:def 4,XBOOLE_0:def 3;
suppose
x in NAT;
hence thesis;
end;
suppose
x in [:{0},NAT:];
then x in [:{0},NAT:] \ {[0,0]} by A3,XBOOLE_0:def 5;
hence thesis by Lm1;
end;
end;
given k such that
A4: x = k or x = - k;
per cases by A4;
suppose x = k;
then
A5: x in NAT by ORDINAL1:def 12;
then x in REAL by NUMBERS:19;
then
A6: not x in {[0,0]} by NUMBERS:def 1,XBOOLE_0:def 5;
x in NAT \/ [:{0},NAT:] by XBOOLE_0:def 3,A5;
hence thesis by A1,A6,NUMBERS:def 4,XBOOLE_0:def 5;
end;
suppose
x = -k & k <> x;
then
A7: x in [:{0},NAT:] \ {[0,0]} by Lm2;
then
A8: not x in {[0,0]} by XBOOLE_0:def 5;
x in NAT \/ [:{0},NAT:] by A7,XBOOLE_0:def 3;
hence thesis by A1,A8,NUMBERS:def 4,XBOOLE_0:def 5;
end;
end;
assume
A9: for x holds x in I iff ex k st x = k or x = - k;
thus I c= INT
proof
let x be object;
assume x in I;
then consider k such that
A10: x = k or x = - k by A9;
per cases by A10;
suppose x = k;
then
A11: x in NAT by ORDINAL1:def 12;
then x in REAL by NUMBERS:19;
then
A12: not x in {[0,0]} by NUMBERS:def 1,XBOOLE_0:def 5;
x in NAT \/ [:{0},NAT:] by XBOOLE_0:def 3,A11;
hence thesis by A12,NUMBERS:def 4,XBOOLE_0:def 5;
end;
suppose
x = -k & k <> x;
then
A13: x in [:{0},NAT:] \ {[0,0]} by Lm2;
then
A14: not x in {[0,0]} by XBOOLE_0:def 5;
x in NAT \/ [:{0},NAT:] by A13,XBOOLE_0:def 3;
hence thesis by A14,NUMBERS:def 4,XBOOLE_0:def 5;
end;
end;
let x be object;
assume
A15: x in INT;
then
A16: not x in {[0,0]} by NUMBERS:def 4,XBOOLE_0:def 5;
per cases by A15,NUMBERS:def 4,XBOOLE_0:def 3;
suppose
x in NAT;
hence thesis by A9;
end;
suppose
x in [:{0},NAT:];
then x in [:{0},NAT:] \ {[0,0]} by A16,XBOOLE_0:def 5;
then ex k st x = k or x = - k by Lm1;
hence thesis by A9;
end;
end;
end;
definition
let i be Number;
attr i is integer means
:Def2:
i in INT;
end;
registration
cluster integer for Real;
existence
proof
take 0;
thus 0 in INT by Def1;
end;
cluster integer for number;
existence
proof
take 0;
thus 0 in INT by Def1;
end;
cluster -> integer for Element of INT;
coherence;
end;
definition
mode Integer is integer Number;
end;
theorem Th1:
for k being natural Number st r = k or r = -k holds r is Integer
proof
let k be natural Number;
A1: k is Nat by TARSKI:1;
assume r = k or r = -k;
then r in INT by A1,Def1;
hence thesis;
end;
theorem Th2:
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 natural -> integer for object;
coherence by Th1;
end;
registration
cluster integer -> real for object;
coherence by NUMBERS:15;
end;
reserve i,i0,i1,i2,i3,i4,i5,i8,i9,j for Integer;
registration
let i1,i2 be Integer;
cluster i1 + i2 -> integer;
coherence
proof
consider l such that
A1: i2 = l or i2 = - l by Th2;
consider k such that
A2: i1 = k or i1 = - k by Th2;
A3: now
A4: now
assume l - k <= 0;
then l <= 0 + k by XREAL_1:20;
then consider z being Nat such that
A5: k = l + z by NAT_1:10;
- z = - k + l by A5;
hence l - k is Integer by Th1;
end;
assume that
A6: i1 = - k and
A7: i2 = l;
now
assume 0 <= l - k;
then 0 + k <= l by XREAL_1:19;
then ex z being Nat st l = k + z by NAT_1:10;
hence l - k is Integer;
end;
hence i1 + i2 is Integer by A6,A7,A4;
end;
A8: now
A9: now
assume k - l <= 0;
then k <= 0 + l by XREAL_1:20;
then consider z being Nat such that
A10: l = k + z by NAT_1:10;
- z = - l + k by A10;
hence k - l is Integer by Th1;
end;
assume that
A11: i1 = k and
A12: i2 = - l;
now
assume 0 <= k - l;
then 0 + l <= k by XREAL_1:19;
then ex z being Nat st k = l + z by NAT_1:10;
hence k - l is Integer;
end;
hence i1 + i2 is Integer by A11,A12,A9;
end;
now
assume that
A13: i1 = - k and
A14: i2 = - l;
i1 + i2 = - (k + l) by A13,A14;
hence i1 + i2 is Integer by Th1;
end;
hence thesis by A2,A1,A8,A3;
end;
cluster i1 * i2 -> integer;
coherence
proof
consider l such that
A15: i2 = l or i2 = - l by Th2;
consider k such that
A16: i1 = k or i1 = - k by Th2;
A17: now
assume that
A18: i1 = - k and
A19: i2 = - l;
i1 * i2 = k * l by A18,A19;
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 Th1;
end;
hence thesis by A16,A15,A17;
end;
end;
registration
let i0 be Integer;
cluster - i0 -> integer;
coherence
proof
ex k st i0 = k or i0 = - k by Th2;
hence thesis by Th1;
end;
end;
registration
let i1,i2 be Integer;
cluster i1 - i2 -> integer;
coherence
proof
i1 - i2 = i1 + (- i2);
hence thesis;
end;
end;
:: Some basic theorems about integers
theorem Th3:
0 <= i0 implies i0 in NAT
proof
consider k such that
A1: i0 = k or i0 = - k by Th2;
assume 0 <= i0;
then i0 = - k implies i0 is Element of NAT;
hence thesis by A1, ORDINAL1:def 12;
end;
theorem
r is Integer implies r + 1 is Integer & r - 1 is Integer;
theorem Th5:
i2 <= i1 implies i1 - i2 in NAT
proof
assume i2 <= i1;
then i2 - i2 <= i1 - i2 by XREAL_1:9;
hence thesis by Th3;
end;
theorem Th6:
i1 + k = i2 implies i1 <= i2
proof
reconsider i0 = k as Integer;
assume i1 + k = i2;
then 0 + (i1 + k) <= k + i2 by XREAL_1:6;
then i1 + i0 - i0 <= i2 + i0 - i0 by XREAL_1:9;
hence thesis;
end;
Lm3: 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;
hence thesis by NAT_1:13;
end;
Lm4: 0 < i1 implies 1 <= i1
proof
assume
A1: 0 < i1;
then reconsider i2 = i1 as Element of NAT by Th3;
0 <> i2 by A1;
hence thesis by Lm3;
end;
theorem Th7:
i0 < i1 implies i0 + 1 <= i1
proof
assume i0 < i1;
then i0 + (- i0) < i1 + (- i0) by XREAL_1:6;
then 1 <= i1 + (- i0) by Lm4;
then 1 + i0 <= i1 + (- i0) + i0 by XREAL_1:6;
hence thesis;
end;
registration
cluster non integer for Real;
existence
proof
1/2 < 0+1; then
not 1/2 is integer by Th7;
hence thesis;
end;
end;
theorem Th8:
i1 < 0 implies i1 <= - 1
proof
assume i1 < 0;
then 0 < - i1 by XREAL_1:58;
then 1 <= - i1 by Lm4;
then - - i1 <= - 1 by XREAL_1:24;
hence thesis;
end;
theorem Th9:
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 i2 = 0;
A3: now
A4: (- i1) * (- i2) = i1 * i2;
assume that
A5: i1 < 0 and
A6: i2 < 0;
A7: -i2 is Element of NAT by A6,Th3;
-i1 is Element of NAT by A5,Th3;
then - (- i1) = - 1 by A1,A7,A4,NAT_1:15;
hence i1 = - 1 & i2 = - 1 by A1;
end;
A8: now
assume that
A9: 0 < i1 and
A10: 0 < i2;
A11: i2 is Element of NAT by A10,Th3;
i1 is Element of NAT by A9,Th3;
hence i1 = 1 & i2 = 1 by A1,A11,NAT_1:15;
end;
not i1 = 0 by A1;
hence thesis by A1,A2,A8,A3;
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 i1 * i2 = - 1;
then (- i1) * i2 = 1;
then - (- i1) = - 1 & i2 = 1 or - i1 = - 1 & i2 = - 1 by Th9;
hence thesis;
end;
assume i1 = - 1 & i2 = 1 or i1 = 1 & i2 = - 1;
hence thesis;
end;
Lm5: i0 <= i1 implies ex k st i0 + k = i1
proof
assume i0 <= i1;
then reconsider k = i1 - i0 as Element of NAT by Th5;
i0 + k = i1;
hence thesis;
end;
Lm6: i0 <= i1 implies ex k st i1 - k = i0
proof
assume i0 <= i1;
then reconsider k = i1 - i0 as Element of NAT by Th5;
i1 - k = i0;
hence thesis;
end;
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[object] means ex i0 st i0 = $1 & P[i0];
consider X such that
A1: for y being object holds y in X iff y in INT & P1[y] from XBOOLE_0:sch 1;
for y being object holds y in X implies y in INT by A1;
then reconsider X as Subset of INT by TARSKI:def 3;
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 by Def2,A1;
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
defpred Q[Nat] means for i2 st $1 = i2 - F() holds P[i2];
A3: for k st Q[k] holds Q[k + 1]
proof
let k;
reconsider i8 = k as Integer;
assume
A4: Q[k];
let i2;
assume
A5: k + 1 = i2 - F();
then i2 - 1 = i8 + F();
then
A6: F() <= i2 - 1 by Th6;
k = i2 - 1 - F() by A5;
then P[i2 - 1 + 1] by A2,A4,A6;
hence thesis;
end;
let i0;
assume F() <= i0;
then reconsider l = i0 - F() as Element of NAT by Th5;
A7: l = i0 - F();
A8: Q[0] by A1;
for k holds Q[k] from NAT_1:sch 2(A8,A3);
hence thesis by A7;
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
defpred Q[Integer] means for i2 st $1 = - i2 holds P[i2];
A3: for i2 st - F() <= i2 holds Q[i2] implies Q[i2 + 1]
proof
let i2;
assume that
A4: - F() <= i2 and
A5: Q[i2];
let i3;
assume
A6: i2 + 1 = - i3; then
A7: i2 = - (i3 + 1);
- (- i3 - 1) <= - (- F()) by A4,A6,XREAL_1:24;
then P[i3 + 1 - 1] by A2,A5,A7;
hence thesis;
end;
let i0;
assume i0 <= F();
then
A8: - F() <= - i0 by XREAL_1:24;
A9: Q[- F()] by A1;
for i2 st - F() <= i2 holds Q[i2] from IntIndUp(A9,A3);
hence thesis by A8;
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
let i0;
A3: P[F()] by A1;
A4: now
A5: for i2 st i2 <= F() holds P[i2] implies P[i2 - 1] by A2;
A6: for i2 st i2 <= F() holds P[i2] from IntIndDown(A3,A5);
assume i0 <= F();
hence thesis by A6;
end;
now
A7: for i2 st F() <= i2 holds P[i2] implies P[i2 + 1] by A2;
A8: for i2 st F() <= i2 holds P[i2] from IntIndUp(A3,A7);
assume F() <= i0;
hence thesis by A8;
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
defpred Q[Nat] means P[F() + $1];
consider i1 such that
A3: P[i1] by A2;
ex k st F() + k = i1 by A1,A3,Lm5;
then
A4: ex k be Nat st Q[k] by A3;
consider l be Nat such that
A5: Q[l] & for n be Nat st Q[n] holds l <= n from NAT_1:sch 5(A4);
take i0 = F() + l;
for i1 st P[i1] holds i0 <= i1
proof
let i1;
assume
A6: P[i1];
then ex n st F() + n = i1 by A1,Lm5;
then i0 - F() <= i1 - F() by A5,A6;
hence thesis by XREAL_1:9;
end;
hence thesis by A5;
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
defpred Q[Nat] means P[F() - $1];
consider i1 such that
A3: P[i1] by A2;
ex k st i1 = F() - k by A1,A3,Lm6;
then
A4: ex k be Nat st Q[k] by A3;
consider l be Nat such that
A5: Q[l] & for n be Nat st Q[n] holds l <= n from NAT_1:sch 5(A4);
take i0 = F() - l;
for i1 st P[i1] holds i1 <= i0
proof
let i1;
assume
A6: P[i1];
then consider n such that
A7: F() - n = i1 by A1,Lm6;
l <= n by A5,A6,A7;
then F() + (- i0) - F() <= F() - i1 - F() by A7,XREAL_1:9;
then - i0 <= F() + (- i1) - F();
hence thesis by XREAL_1:24;
end;
hence thesis by A5;
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;
take 1;
thus thesis;
end;
end;
definition
let i1,i2,i3 be Integer;
pred i1,i2 are_congruent_mod i3 means
i3 divides i1 - i2;
end;
definition
let i1,i2,i3 be Integer;
redefine pred i1,i2 are_congruent_mod i3 means :: redefines are_congruent_mod (INT_1, definition)
ex i4 st i3 * i4 = i1 - i2;
compatibility
proof
thus i1,i2 are_congruent_mod i3 implies
ex i4 st i3 * i4 = i1 - i2
proof
assume i3 divides i1-i2;
hence thesis;
end;
given i4 such that
A1: i3 * i4 = i1 - i2;
take i4;
thus thesis by A1;
end;
end;
theorem
i1,i1 are_congruent_mod i2
proof
i2 * 0 = i1 - i1;
hence thesis;
end;
theorem
i1,0 are_congruent_mod i1 & 0,i1 are_congruent_mod i1
proof
A1: i1 * (- 1) = 0 - i1;
thus thesis by A1;
end;
theorem
i1,i2 are_congruent_mod 1
proof
i1 - i2 = 1 * (i1 - i2);
hence thesis;
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;
i2 - i1 = i3 * (- i0) by A1;
hence thesis;
end;
theorem
i1,i2 are_congruent_mod i5 & i2,i3 are_congruent_mod i5 implies
i1,i3 are_congruent_mod i5
proof
assume that
A1: i1,i2 are_congruent_mod i5 and
A2: i2,i3 are_congruent_mod i5;
consider i8 such that
A3: i5 * i8 = i1 - i2 by A1;
consider i9 such that
A4: i5 * i9 = i2 - i3 by A2;
i5 * (i8 + i9) = i1 - i3 by A3,A4;
hence thesis;
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 that
A1: i1,i2 are_congruent_mod i5 and
A2: i3,i4 are_congruent_mod i5;
consider i8 such that
A3: i5 * i8 = i1 - i2 by A1;
consider i9 such that
A4: i5 * i9 = i3 - i4 by A2;
i5 * (i8 + i9) = (i1 + i3) - (i2 + i4) by A3,A4;
hence thesis;
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 that
A1: i1,i2 are_congruent_mod i5 and
A2: i3,i4 are_congruent_mod i5;
consider i8 such that
A3: i5 * i8 = i1 - i2 by A1;
consider i9 such that
A4: i5 * i9 = i3 - i4 by A2;
(i1 - i3) - (i2 - i4) = i5 * (i8 - i9) by A3,A4;
hence thesis;
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 that
A1: i1,i2 are_congruent_mod i5 and
A2: i3,i4 are_congruent_mod i5;
consider i8 such that
A3: i5 * i8 = i1 - i2 by A1;
consider i9 such that
A4: i5 * i9 = i3 - i4 by A2;
(i1 * i3) - (i2 * i4) = (i1 - i2) * i3 + (i3 - i4) * i2
.= (i5 * i8) * i3 + (i5 * i9) * i2 by A3,A4
.= i5 * ((i8 * i3) + (i9 * i2));
hence thesis;
end;
theorem
(i1 + i2),i3 are_congruent_mod i5 iff i1, (i3 - i2) are_congruent_mod i5;
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;
i1 - i2 = i4 * (i5 * i0) by A1,A2;
hence thesis;
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;
i5 * (i0 + 1) = (i1 + i5) - i2 by A1;
hence thesis;
end;
assume (i1 + i5),i2 are_congruent_mod i5;
then consider i0 such that
A2: i5 * i0 = (i1 + i5) - i2;
i5 * (i0 - 1) = i1 - i2 by A2;
hence thesis;
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;
i5 * (i0 - 1) = (i1 - i5) - i2 by A1;
hence thesis;
end;
assume (i1 - i5),i2 are_congruent_mod i5;
then consider i0 such that
A2: i5 * i0 = (i1 - i5) - i2;
i5 * (i0 + 1) = i1 - i2 by A2;
hence thesis;
end;
theorem Th23:
i1 <= r & r - 1 < i1 & i2 <= r & r - 1 < i2 implies i1 = i2
proof
assume that
A1: i1 <= r and
A2: r - 1 < i1 and
A3: i2 <= r and
A4: r - 1 < i2;
i2 = i1 + (i2 - i1);
then consider i0 such that
A5: i2 = i1 + i0;
A6: now
assume that
A7: 0 < i0 and
i1 <> i2;
1 <= i0 by A7,Lm4;
then r - 1 + 1 < i1 + i0 by A2,XREAL_1:8;
hence contradiction by A3,A5;
end;
A8: now
assume that
A9: i0 < 0 and
i1 <> i2;
i0 <= - 1 by A9,Th8;
then i1 + i0 <= r + (- 1) by A1,XREAL_1:7;
hence contradiction by A4,A5;
end;
i0 = 0 implies i2 = i1 by A5;
hence thesis by A8,A6;
end;
theorem Th24:
r <= i1 & i1 < r + 1 & r <= i2 & i2 < r + 1 implies i1 = i2
proof
assume that
A1: r <= i1 and
A2: i1 < r + 1 and
A3: r <= i2 and
A4: i2 < r + 1;
i2 = i1 + (i2 - i1);
then consider i0 such that
A5: i2 = i1 + i0;
A6: now
assume that
A7: i0 < 0 and
i1 <> i2;
i0 <= - 1 by A7,Th8;
then i1 + i0 < r + 1 + (- 1) by A2,XREAL_1:8;
hence contradiction by A3,A5;
end;
A8: now
assume that
A9: 0 < i0 and
i1 <> i2;
1 <= i0 by A9,Lm4;
hence contradiction by A1,A4,A5,XREAL_1:7;
end;
i0 = 0 implies i2 = i1 by A5;
hence thesis by A6,A8;
end;
reserve r1,p,p1,g,g1,g2 for Real,
Y for Subset of REAL;
Lm7: for r ex n st r<n
proof
defpred P[Real] means for r st r in NAT holds not $1<r;
let r;
consider Y such that
A1: for p1 being Element of REAL holds p1 in Y iff P[p1] from SUBSET_1:sch 3;
reconsider N =NAT as Subset of REAL by NUMBERS:19;
for r,p1 st r in N & p1 in Y holds r <= p1 by A1;
then consider g2 such that
A2: for r,p st r in N & p in Y holds r <= g2 & g2 <= p by AXIOMS:1;
A3: g2+-1<g2+0 by XREAL_1:6;
for g ex r st r in NAT & g<r
proof
given g1 such that
A4: for r st r in NAT holds not g1<r;
g1 in REAL by XREAL_0:def 1;
then
A5: g1 in Y by A1,A4;
now
reconsider g21 = g2 - 1 as Element of REAL by XREAL_0:def 1;
assume not g2-1 in Y;
then not P[g21] by A1;
then consider r1 being Real such that
A6: r1 in NAT and
A7: g2-1<r1;
A8: r1+1 in NAT by A6,AXIOMS:2;
g2-1+1<r1+1 by A7,XREAL_1:6;
hence contradiction by A2,A5,A8;
end;
hence contradiction by A2,A3;
end;
then consider p such that
A9: p in NAT and
A10: r<p;
reconsider p as Element of NAT by A9;
take p;
thus thesis by A10;
end;
definition
let r be Real;
func [\ r /] -> Integer means
:Def6:
it <= r & r - 1 < it;
existence
proof
defpred P[Integer] means r < $1;
consider n such that
A1: - r < n by Lm7;
A2: - n < -- r by A1,XREAL_1:24;
A3: for i1 st P[i1] holds -n <= i1
proof
let i1;
assume r < i1;
then r + -n < i1 + r by A2,XREAL_1:8;
hence thesis by XREAL_1:6;
end;
ex n st r < n by Lm7;
then
A4: ex i0 st P[i0];
consider i1 such that
A5: P[i1] & for i2 st P[i2] holds i1 <= i2 from IntMin(A3,A4);
A6: r - 1 < i1 - 1 by A5,XREAL_1:9;
r < i1 - 1 implies i1 <= i1-1 by A5;
hence thesis by A6,XREAL_1:146;
end;
uniqueness by Th23;
projectivity by XREAL_1:44;
end;
theorem Th25:
[\ r /] = r iff r is integer
proof
r is Integer implies [\ r /] = r
proof
r + 0 < r + 1 by XREAL_1:6;
then r - 1 < r + 1 - 1 by XREAL_1:9;
hence thesis by Def6;
end;
hence thesis;
end;
registration
let i be Integer;
reduce [\ i /] to i;
reducibility by Th25;
end;
theorem Th26:
[\ r /] < r iff r is not integer
proof
now
assume
A1: not r is Integer;
[\ r /] <= r by Def6;
hence [\ r /] < r by A1,XXREAL_0:1;
end;
hence thesis;
end;
theorem
[\ r /] - 1 < r & [\ r /] < r + 1
proof
[\ r /] <= r by Def6; then
A1: [\ r /] + 0 < r + 1 by XREAL_1:8;
then [\ r /] + (- 1) < r + 1 + (- 1) by XREAL_1:6;
hence thesis by A1;
end;
theorem Th28:
[\ r /] + i0 = [\ r + i0 /]
proof
r - 1 < [\ r /] by Def6;
then r - 1 + i0 < [\ r /] + i0 by XREAL_1:6;
then
A1: r + i0 - 1 < [\ r /] + i0;
[\ r /] + i0 <= r + i0 by Def6,XREAL_1:6;
hence thesis by A1,Def6;
end;
theorem Th29:
r < [\ r /] + 1
proof
r - 1 < [\ r /] by Def6;
then r - 1 + 1 < [\ r /] + 1 by XREAL_1:6;
hence thesis;
end;
definition
let r be Real;
func [/ r \] -> Integer means :Def7:
r <= it & it < r + 1;
existence
proof
A1: now
A2: r + 0 < r + 1 by XREAL_1:6;
assume r is Integer;
hence r <= [\ r /] & [\ r /] < r + 1 by A2;
end;
r is not Integer implies
r <= [\ r /] + 1 & [\ r /] + 1 < r + 1 by Th29,XREAL_1:6,Th26;
hence thesis by A1;
end;
uniqueness by Th24;
projectivity by XREAL_1:29;
end;
theorem Th30:
[/ r \] = r iff r is integer
proof
r + 0 < r + 1 by XREAL_1:6;
hence thesis by Def7;
end;
registration
let i be Integer;
reduce [/ i \] to i;
reducibility by Th30;
end;
theorem Th31:
r < [/ r \] iff r is not integer
proof
now
assume
A1: not r is Integer;
r <= [/ r \] by Def7;
hence r < [/ r \] by A1,XXREAL_0:1;
end;
hence thesis;
end;
theorem
r - 1 < [/ r \] & r < [/ r \] + 1
proof
r <= [/ r \] by Def7; then
A1: r + 0 < [/ r \] + 1 by XREAL_1:8;
then r + (- 1) < [/ r \] + 1 + (- 1) by XREAL_1:6;
hence thesis by A1;
end;
theorem
[/ r \] + i0 = [/ r + i0 \]
proof
[/ r \] < r + 1 by Def7;
then [/ r \] + i0 < r + 1 + i0 by XREAL_1:6;
then
A1: [/ r \] + i0 < r + i0 + 1;
r <= [/ r \] by Def7;
then r + i0 <= [/ r \] + i0 by XREAL_1:6;
hence thesis by A1,Def7;
end;
theorem
[\ r /] = [/ r \] iff r is integer
proof
now
assume
A2: not r is Integer;
then [\ r /] < r by Th26;
hence [\ r /] <> [/ r \] by A2,Th31;
end;
hence thesis;
end;
theorem Th35:
[\ r /] < [/ r \] iff r is not integer
proof
now
assume
A1: not r is Integer;
then
A2: r < [/ r \] by Th31;
[\ r /] < r by A1,Th26;
hence [\ r /] < [/ r \] by A2,XXREAL_0:2;
end;
hence thesis;
end;
theorem
[\ r /] <= [/ r \]
proof
A1: r <= [/ r \] by Def7;
[\ r /] <= r by Def6;
hence thesis by A1,XXREAL_0:2;
end;
theorem
[\ ([/ r \]) /] = [/ r \];
::$CT 2
theorem
[/ ([\ r /]) \] = [\ r /];
theorem
[\ r /] = [/ r \] iff not [\ r /] + 1 = [/ r \]
proof
set Diff = [/ r \] + (- [\ r /]);
now
assume not r is Integer;
then [\ r /] < [/ r \] by Th35;
then [\ r /] + (- [\ r /]) < Diff by XREAL_1:6;
then
A2: 1 <= Diff by Lm4;
r - 1 < [\ r /] by Def6;
then
A3: - [\ r /] < - (r - 1) by XREAL_1:24;
[/ r \] < r + 1 by Def7;
then Diff < r + 1 + (- (r - 1)) by A3,XREAL_1:8;
then Diff + 1 + (- 1) <= 1 + 1 + (- 1) by Th7;
then [\ r /] + 1 = [\ r /] + Diff by A2,XXREAL_0:1;
hence [\ r /] + 1 = [/ r \] & [\ r /] <> [/ r \];
end;
hence thesis;
end;
definition
let r be Real;
func frac r -> number equals
r - [\ r /];
coherence;
end;
registration
let r be Real;
cluster frac r -> real;
coherence;
end;
theorem
r = [\ r /] + frac r;
theorem Th41:
frac r < 1 & 0 <= frac r
proof
r - 1 < [\ r /] by Def6;
then frac r + (r - 1) < r - [\ r /] + [\ r /] by XREAL_1:6;
then frac r + (- 1) + r - r < r - r by XREAL_1:9;
then
A1: frac r - 1 + 1 < 0 + 1 by XREAL_1:6;
[\ r /] <= r by Def6;
then [\ r /] + (r - [\ r /]) <= r + frac r by XREAL_1:6;
then r - r <= r + frac r - r by XREAL_1:9;
hence thesis by A1;
end;
theorem
[\ frac r /] = 0
proof
thus [\ frac r /] = [\ (r + (- [\ r /])) /] .= [\ r /] + (- [\ r /]) by Th28
.= 0;
end;
theorem Th43:
frac r = 0 iff r is integer;
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 Th41;
end;
hence thesis;
end;
registration
let a be integer Real;
cluster frac a -> zero;
coherence by Th43;
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
:Def10:
i1 - (i1 div i2) * i2 if i2 <> 0
otherwise 0;
correctness;
end;
theorem Th45:
for r being Real st r <> 0 holds [\ r / r /] = 1
proof
let r be Real;
assume r <> 0;
hence [\ r / r /] = [\ 1 /] by XCMPLX_1:60
.= 1;
end;
theorem Th46:
for i being Integer holds i div 0 = 0
proof
let i be Integer;
i / 0 = i * 0" by XCMPLX_0:def 9
.= i * 0;
hence thesis;
end;
registration
let i be Integer;
reduce i div 0 to 0;
reducibility by Th46;
reduce 0 div i to 0;
reducibility;
end;
theorem
for i being Integer st i <> 0 holds i div i = 1 by Th45;
theorem
for i being Integer holds i mod i = 0
proof
let i be Integer;
per cases;
suppose
i = 0;
hence thesis by Def10;
end;
suppose
A1: i <> 0;
hence i mod i = i - (i div i) * i by Def10
.= i - 1 * i by A1,Th45
.= 0;
end;
end;
begin :: Addenda
:: from FSM_1
theorem
for k, i being Integer holds
k < i implies ex j being Element of NAT st j = i-k & 1 <= j
proof
let k,i be Integer;
assume k < i;
then
A1: k - k < i - k by XREAL_1:9;
then reconsider j = i - k as Element of NAT by Th3;
reconsider j9 = j, Z9 = 0 as Integer;
take j;
thus j = i - k;
Z9 + 1 <= j9 by A1,Th7;
hence thesis;
end;
:: from SCMFSA_7, 2005.02.05, A.T.
theorem Th50:
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:9;
then a - 1 + 1 <= b - 1 by Th7;
hence thesis;
end;
:: from UNIFORM1, 2005.08.22, A.T.
theorem Th51:
for r being Real st r>=0 holds [/ r \]>=0 & [\ r /]>=0 &
[/ r \] is Element of NAT & [\ r /] is Element of NAT
proof
let r be Real;
assume
A1: r>=0;
A2: r<=[/ r \] by Def7;
r-1<[\ r /] by Def6;
then r-1+1<[\ r /]+1 by XREAL_1:6;
then 0-1<[\ r /]+1-1 by A1,XREAL_1:9;
then [\ r /]>=0 by Th8;
hence thesis by A1,A2,Th3;
end;
:: from SCMFSA9A, 2005.11.16, A.T.
theorem Th52:
for i being Integer, r being Real st i <= r holds i <= [\ r /]
proof
let i be Integer;
let r be Real;
assume i <= r;
then
A1: i-1 <= r-1 by XREAL_1:9;
r-1 < [\ r /] by Def6;
then i-1 < [\ r /] by A1,XXREAL_0:2;
then i-1+1 <= [\ r /] by Th7;
hence thesis;
end;
theorem
for m,n being Nat holds 0 <= m qua Integer div n by Th52;
:: 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;
assume
A3: i <= i div j;
i div j <= i/j by Def6;
then j * (i div j) <= j * (i/j) by A2,XREAL_1:64;
then j * (i div j) <= i by A2,XCMPLX_1:87;
then j * (i div j) <= i div j by A3,XXREAL_0:2;
then j * (i div j) * (i div j)" <= (i div j) * (i div j)" by A1,A3,XREAL_1:64
;
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,A3,XCMPLX_0:def 7;
hence contradiction by A1,A2,A3,XCMPLX_0:def 7;
end;
:: from NEWTON, 2007.01.02, AK
theorem Th57:
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 Def6;
then (i1 div i2)*i2 <= (i1/i2)*i2 by A2,XREAL_1:64;
then (i1 div i2)*i2 <= i1 by A2,XCMPLX_1:87;
then i1 - (i1 div i2)*i2 >= 0 by XREAL_1:48;
hence thesis by Def10;
end;
suppose
i2 = 0;
hence thesis by Def10;
end;
end;
theorem
i2 > 0 implies i1 mod i2 < i2
proof
assume
A1: i2 > 0;
i1/i2 -1 < [\ i1/i2 /] by Def6;
then (i1/i2 -1)*i2 < (i1 div i2)*i2 by A1,XREAL_1:68;
then i1/i2*i2 -1*i2 < (i1 div i2)*i2;
then i1 -i2 < (i1 div i2)*i2-0 by A1,XCMPLX_1:87;
then i1 -(i1 div i2)*i2 < i2-0 by XREAL_1:17;
hence thesis by A1,Def10;
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 Def10
.= i1;
hence thesis;
end;
:: from AMI_3, 2007.06.14, A.T.
theorem
for m,j being Integer holds m*j, 0 are_congruent_mod m;
:: from AMI_4, 2007.06.14, A.T.
theorem
i >= 0 & j >= 0 implies i div j >= 0
proof
assume that
A1: i >= 0 and
A2: j >= 0;
A3: i / j - 1 < [\ i / j /] by Def6;
i / j - 1 >= 0-1 by A1,A2,XREAL_1:9;
then - 1 < [\ i / j /] by A3,XXREAL_0:2;
hence thesis by Th8;
end;
:: from INT_3, 2007.07.27, A.T.
theorem Th62:
for n being Integer holds
n > 0 implies for a being Integer holds a mod n = 0 iff n divides a
proof
let n be Integer;
assume
A1: n > 0;
let a be Integer;
A2: now
A3: a mod n = a - (a div n) * n by A1,Def10
.= a - ([\ a/n /]) * n;
assume n divides a;
then consider k being Integer such that
A4: n * k = a;
-n <> 0 by A1;
then -n + a < 0 + a by A1,XREAL_1:6;
then (-n + a) * n" < (n * k) * n" by A1,A4,XREAL_1:68;
then (-n) * n" + a * n" < (n * k) * n";
then (-n) * n" + a/n < (n * n") * k by XCMPLX_0:def 9;
then (-n) * n" + a/n < 1 * k by A1,XCMPLX_0:def 7;
then -n * n" + a/n < k;
then -1 + a/n < k by A1,XCMPLX_0:def 7;
then
A5: a/n - 1 < k;
k <= a/n
proof
assume k > a/n;
then k * n > a/n * n by A1,XREAL_1:68;
then k * n > (a * n") * n by XCMPLX_0:def 9;
then k * n > a * (n" * n);
then n * k > a * 1 by A1,XCMPLX_0:def 7;
hence thesis by A4;
end;
then ([\ a/n /]) = k by A5,Def6;
hence a mod n = 0 by A4,A3;
end;
now
assume a mod n = 0;
then 0 = a - (a div n) * n by A1,Def10;
hence n divides a;
end;
hence thesis by A2;
end;
:: from JORDAN1D, 2007.07.27, A.T.
reserve r, s for Real;
theorem
r/s is not Integer implies - [\ r/s /] = [\ (-r) / s /] + 1
proof
r/s - 1 < [\ r/s /] by Def6;
then - (r/s - 1) > - [\ r/s /] by XREAL_1:24;
then -r/s + 1 > - [\ r/s /];
then - [\ r/s /] <= (-r) / s + 1 by XCMPLX_1:187;
then
A1: - [\ r/s /] - 1 <= (-r) / s + 1 - 1 by XREAL_1:9;
assume r/s is not Integer;
then [\ r/s /] < r/s by Th26;
then -r/s < - [\ r/s /] by XREAL_1:24;
then -r/s - 1 < - [\ r/s /] - 1 by XREAL_1:9;
then (-r)/s - 1 < - [\ r/s /] - 1 by XCMPLX_1:187;
then - [\ r/s /] - 1 + 1 = [\ (-r) / s /] + 1 by A1,Def6;
hence thesis;
end;
theorem
r/s is Integer implies - [\ r/s /] = [\ (-r) / s /]
proof
assume r/s is Integer;
then
A1: [\ r/s /] = r/s;
-r/s = (-r)/s by XCMPLX_1:187;
hence thesis by A1;
end;
:: missing, 2008.05.16, A.T.
theorem Th63:
r <= i implies [/ r \] <= i
proof
assume r <= i;
then
A1: r+1 <= i+1 by XREAL_1:6;
[/ r \] < r+1 by Def7;
then [/ r \] < i+1 by A1,XXREAL_0:2;
then [/ r \] <= i+1-1 by Th50;
hence thesis;
end;
:: from POLYNOM2, 2010.02.13, A.T.
scheme
FinInd{M, N() -> Element of NAT, P[Nat]} :
for i being Element of NAT st M() <= i & i <= N() holds P[i]
provided
A1: P[M()] and
A2: for j being Element of NAT st M() <= j & j < N() holds P[j] implies P[j+1]
proof
defpred Q[Nat] means M() <= $1 & $1 <= N() & not(P[$1]);
assume not(for i being Element of NAT st M() <= i & i <= N() holds P[i]);
then
A3: ex i being Nat st Q[i];
consider k being Nat such that
A4: Q[k] & for k9 being Nat st Q[k9] holds k <= k9 from NAT_1:sch 5(A3);
per cases;
suppose
k = M();
hence thesis by A1,A4;
end;
suppose
k <> M();
then M() < k by A4,XXREAL_0:1;
then M() + 1 <= k by NAT_1:13;
then
A5: (M() + 1) - 1 <= k - 1 by XREAL_1:9;
then reconsider k9 = k - 1 as Element of NAT by Th3;
A6: k9 <> k9 + 1;
k9 <= k9 + 1 by NAT_1:11;
then
A7: k9 < k by A6,XXREAL_0:1;
then
A8: k9 < N() by A4,XXREAL_0:2;
A9: (k - 1) + 1 = k + 0;
not(Q[k9]) by A4,A7;
hence thesis by A2,A4,A5,A9,A8;
end;
end;
scheme
FinInd2{M,N() -> Element of NAT, P[Nat]} :
for i being Element of NAT st M() <= i & i <= N() holds P[i]
provided
A1: P[M()] and
A2: 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]
proof
defpred Q[Element of NAT] means for j being Element of NAT st M() <= j & j
<= ($1) holds P[j];
A3: for j being Element of NAT st M() <= j & j < N() holds Q[j] implies Q[j+ 1]
proof
let j be Element of NAT;
assume that
A4: M() <= j and
A5: j < N();
assume
A6: Q[j];
thus Q[j+1]
proof
let i be Element of NAT;
assume that
A7: M() <= i and
A8: i <= j + 1;
per cases;
suppose
i = j + 1;
hence thesis by A2,A4,A5,A6;
end;
suppose
i <> j + 1;
then i < j + 1 by A8,XXREAL_0:1;
then i <= j by NAT_1:13;
hence thesis by A6,A7;
end;
end;
end;
A9: Q[M()] by A1,XXREAL_0:1;
for i being Element of NAT st M() <= i & i <= N() holds Q[i] from
FinInd(A9,A3);
hence thesis;
end;
:: from TOPREALA, 2011.04.27, A.T.
reserve i for Integer,
a, b, r, s for Real;
theorem Th64:
frac(r+i) = frac r
proof
thus frac(r+i) = r+i-([\r/]+i) by Th28
.= frac r;
end;
theorem Th65:
r <= a & a < [\r/]+1 implies [\a/] = [\r/]
proof
assume
A1: r <= a;
assume a < [\r/]+1;
then
A2: a-1 < [\r/]+1-1 by XREAL_1:9;
[\r/] <= r by Def6;
then [\r/] <= a by A1,XXREAL_0:2;
hence thesis by A2,Def6;
end;
theorem Th66:
r <= a & a < [\r/]+1 implies frac r <= frac a
proof
assume
A1: r <= a;
assume a < [\r/]+1;
then [\a/] = [\r/] by A1,Th65;
hence thesis by A1,XREAL_1:9;
end;
theorem
r < a & a < [\r/]+1 implies frac r < frac a
proof
assume
A1: r < a;
assume a < [\r/]+1;
then [\a/] = [\r/] by A1,Th65;
hence thesis by A1,XREAL_1:9;
end;
theorem Th68:
a >= [\r/]+1 & a <= r+1 implies [\a/] = [\r/] + 1
proof
assume
A1: a >= [\r/]+1;
assume a <= r+1;
then a-1 <= r+1-1 by XREAL_1:9;
then a-1 < [\r/]+1 by Th29,XXREAL_0:2;
hence thesis by A1,Def6;
end;
theorem Th69:
a >= [\r/]+1 & a < r+1 implies frac a < frac r
proof
assume
A1: a >= [\r/]+1;
assume
A2: a < r+1;
then a-1 < r by XREAL_1:19;
then
A3: frac a = a-[\a/] & a-1-[\r/] < r-[\r/] by XREAL_1:14;
[\a/] = [\r/]+1 by A1,A2,Th68;
hence thesis by A3;
end;
theorem
r <= a & a < r+1 & r <= b & b < r+1 & frac a = frac b implies a = b
proof
assume that
A1: r <= a and
A2: a < r+1 and
A3: r <= b and
A4: b < r+1 and
A5: frac a = frac b;
A6: [\r/] <= r by Def6;
then
A7: [\r/] <= a by A1,XXREAL_0:2;
A8: [\r/] <= b by A3,A6,XXREAL_0:2;
per cases;
suppose
A9: a < [\r/]+1 & b >= [\r/]+1;
then frac a >= frac r by A1,Th66;
hence thesis by A4,A5,A9,Th69;
end;
suppose
A10: a >= [\r/]+1 & b < [\r/]+1;
then frac a < frac r by A2,Th69;
hence thesis by A3,A5,A10,Th66;
end;
suppose
A11: a < [\r/]+1 & b < [\r/]+1;
then b-1 < [\r/]+1-1 by XREAL_1:9;
then
A12: [\b/] = [\r/] by A8,Def6;
a-1 < [\r/]+1-1 by A11,XREAL_1:9;
then [\a/] = [\r/] by A7,Def6;
hence thesis by A5,A12;
end;
suppose
a >= [\r/]+1 & b >= [\r/]+1;
then [\a/] = [\r/]+1 & [\b/] = [\r/]+1 by A2,A4,Th68;
hence thesis by A5;
end;
end;
:: 28.05.2012, A.T.
registration
let i be Integer;
reduce In(i,INT) to i;
reducibility by Def2,SUBSET_1:def 8;
end;
registration
let i,j be Integer;
reduce In([i,j],[:INT,INT:]) to [i,j];
reducibility
proof
[In(i,INT),In(j,INT)] in [:INT,INT:] by ZFMISC_1:87;
hence thesis by SUBSET_1:def 8;
end;
end;
definition let x be Number;
attr x is dim-like means :Def11:
x = -1 or x is natural;
end;
registration
cluster natural -> dim-like for object;
coherence;
cluster dim-like -> integer for object;
coherence;
cluster -1 -> dim-like for object;
coherence;
end;
registration
cluster dim-like for set;
existence
proof
reconsider x = -1 as set by TARSKI:1;
take x;
thus thesis;
end;
end;
registration let d be dim-like object;
cluster d + 1 -> natural;
coherence
proof
per cases by Def11;
suppose d = -1;
then d + 1 = 0;
hence thesis;
end;
suppose d is natural;
hence thesis;
end;
end;
end;
registration let k be dim-like object, n be non zero natural Number;
cluster k+n -> natural;
coherence
proof
per cases by Def11;
suppose
A1: k = -1;
consider i being Nat such that
A2: n =i+1 by NAT_1:6;
k + n = i by A2,A1;
hence thesis;
end;
suppose k is natural;
hence thesis;
end;
end;
end;
theorem ::: INT_4:12
for i being Integer holds 0 = 0 mod i
proof
let i be Integer;
per cases;
suppose
i=0;
hence thesis by Def10;
end;
suppose
A1: i<>0;
0 div i = 0;
then 0 mod i = 0-i*(0 qua Nat) by A1,Def10;
hence thesis;
end;
end;
theorem :: moved from CHORD:1
for n being non zero Nat holds n-1 is Nat & 1 <= n
proof
let n be non zero Nat;
A1: 0+1 <= n by NAT_1:13;
then 0+1-1 <= n-1 by XREAL_1:9;
then n-1 in NAT by Th3;
hence n-1 is Nat;
thus thesis by A1;
end;
theorem
for m,n being natural Number holds
m^2 <= n < (m+1)^2 implies [\ sqrt n /] = m
proof
let m,n be natural Number;
assume m^2 <= n;
then
A1: sqrt (m^2) <= sqrt n by SQUARE_1:26;
assume n < (m+1)^2;
then
A2: sqrt n < sqrt ((m+1)^2) by SQUARE_1:27;
A3: sqrt (m^2) = m by SQUARE_1:def 2;
sqrt ((m+1)^2) = m+1 by SQUARE_1:def 2;
then sqrt n - 1 < m+1-1 by A2,XREAL_1:14;
hence thesis by A1,A3,Def6;
end;
registration let r be Real;
reduce frac (frac r) to frac r;
reducibility
proof
frac r = frac ([\r/] + frac r)
.= frac (frac r) by Th64;
hence thesis;
end;
end;
registration
let a be negative Real;
cluster [\a/] -> negative;
coherence by Def6;
end;
registration
let a be positive Real;
cluster [\a/] -> non negative;
coherence
proof
[\a/] >= 0 by Th52;
hence thesis;
end;
cluster [/a\] -> positive;
coherence by Th31,Th30;
end;
registration
let a be negative Real;
cluster [/a\] -> non positive;
coherence
proof
[/a\] <= 0 by Th63;
hence thesis;
end;
end;
registration
let a be Integer;
cluster a mod 1 -> zero;
coherence
proof
1 divides (a*1);
hence thesis by Th62;
end;
cluster a mod 0 -> zero;
coherence by Def10;
end;
registration
let a be Integer;
reduce a div 1 to a;
reducibility;
end;
registration
let a be Integer, b be non negative Integer;
cluster a mod b -> natural;
coherence
proof
a mod b >= 0 by Th57; then
a mod b in NAT by Th3;
hence thesis;
end;
end;
registration
let a be non integer Complex;
cluster -a -> non integer;
coherence
proof
assume not thesis; then
(-1)*(-a) is integer;
hence contradiction;
end;
end;
registration
let a be non zero Integer, b be Integer;
reduce a*b div a to b;
reducibility
proof
a*b div a = [\b/] by XCMPLX_1:89;
hence thesis;
end;
end;
LmX:
for a being non zero Integer, b being Integer holds
a*b mod a = 0
proof
let a be non zero Integer, b be Integer;
a*b mod a = a*b - (a*b div a)*a by Def10
.= 0;
hence thesis;
end;
registration
let a, b be Integer;
cluster a*b mod a -> zero;
coherence
proof
per cases;
suppose a = 0;
hence thesis;
end;
suppose a <> 0;
hence thesis by LmX;
end;
end;
end;
registration
cluster non integer for positive Real;
existence
proof
set a = 1/2;
a > 0; then
reconsider a as positive Real;
take a;
assume a is integer; then
a > 0 implies a >= 0 + 1 by Th7;
hence contradiction;
end;
end;
registration
let a be non negative Real;
cluster [\a/] -> natural;
coherence by Th51;
cluster [/a\] -> natural;
coherence by Th51;
end;
registration
let a be Integer, b be Nat;
cluster a mod b -> natural;
coherence;
end;
registration
let a,b be Nat;
cluster a div b -> natural;
coherence;
end;
registration
cluster non zero for Integer;
existence
proof
take 1;
thus thesis;
end;
cluster non zero positive for Integer;
existence
proof
take 1;
thus thesis;
end;
cluster non zero negative for Integer;
existence
proof
take -1;
thus thesis;
end;
end;