:: INT_1 semantic presentation

begin

        Lm1:  for z being set st z in [:{0},NAT:] \ {[0,0]} holds
ex k being Element of NAT st z = - k
proof
let z be set ; ::_thesis: ( z in [:{0},NAT:] \ {[0,0]} implies ex k being Element of NAT st z = - k )
A1: [:{0},NAT:] c= [:{0},REAL+:] by ARYTM_2:2, ZFMISC_1:95;
assume A2: z in [:{0},NAT:] \ {[0,0]} ; ::_thesis: ex k being Element of NAT st z = - k
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 set  such that
 x in {0} and
A4: y in NAT and
A5: z = [x,y] by A2, ZFMISC_1:84;
reconsider y = y as Element of NAT by A4;
 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;
take  y ; ::_thesis: z = - 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, ARYTM_0: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  z = - y ; ::_thesis: verum
end;

Lm2:  for x being set
for k being Element of NAT st x = - k & k <> x holds
x in [:{0},NAT:] \ {[0,0]}
proof
let x be set ; ::_thesis: for k being Element of NAT st x = - k & k <> x holds
x in [:{0},NAT:] \ {[0,0]}
let k be Element of NAT ; ::_thesis: ( x = - k & k <> x implies x in [:{0},NAT:] \ {[0,0]} )
assume that
A1: x = - k and
A2: k <> x ; ::_thesis: x in [:{0},NAT:] \ {[0,0]}
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: y2 = 0 by A4, ARYTM_0:24;
then A7: y1 = k by A4, ARYTM_0:def_5;
 + (x2,y2) = 0 by A5, ARYTM_0:24;
then A8: + (x1,y1) = 0 by A5, ARYTM_0:def_5;
A9: k in omega ;
A10: now__::_thesis:_not_x1_in_REAL+
assume  x1 in REAL+ ; ::_thesis: contradiction
then consider x9, y9 being Element of REAL+  such that
A11: x1 = x9 and
A12: y1 = y9 and
A13: 0 = x9 + y9 by A9, A7, A8, 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, A6, A11, A12, A14, ARYTM_0:24; ::_thesis: verum
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 A9, A15, A7, A8, 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, A7, A16, A17, A19, ZFMISC_1:87;
hence  x in [:{0},NAT:] \ {[0,0]} by A20, XBOOLE_0:def_5; ::_thesis: verum
end;

definition
redefine func INT  means :Def1: :: INT_1:def 1
 for x being set holds
( x in it iff ex k being Element of NAT st
( x = k or x = - k ) );
compatibility
 for b1 being set holds
( b1 = INT iff for x being set holds
( x in b1 iff ex k being Element of NAT st
( x = k or x = - k ) ) )
proof
let I be set ; ::_thesis: ( I = INT iff for x being set holds
( x in I iff ex k being Element of NAT st
( x = k or x = - k ) ) )
thus  ( I = INT implies for x being set holds
( x in I iff ex k being Element of NAT st
( x = k or x = - k ) ) ) ::_thesis: ( ( for x being set holds
( x in I iff ex k being Element of NAT st
( x = k or x = - k ) ) ) implies I = INT )
proof
assume A1: I = INT ; ::_thesis: for x being set holds
( x in I iff ex k being Element of NAT st
( x = k or x = - k ) )
let x be set ; ::_thesis: ( x in I iff ex k being Element of NAT st
( x = k or x = - k ) )
thus  ( x in I implies ex k being Element of NAT st
( x = k or x = - k ) ) ::_thesis: ( ex k being Element of NAT st
( x = k or x = - k ) implies x in I )
proof
assume A2: x in I ; ::_thesis: ex k being Element of NAT st
( x = k or x = - k )
then A3: not x in {[0,0]} by A1, NUMBERS:def_4, XBOOLE_0:def_5;
percases ( x in NAT or x in [:{0},NAT:] ) by A1, A2, NUMBERS:def_4, XBOOLE_0:def_3;
suppose x in NAT ; ::_thesis: ex k being Element of NAT st
( x = k or x = - k )
hence  ex k being Element of NAT st
( x = k or x = - k ) ; ::_thesis: verum
end;
suppose x in [:{0},NAT:] ; ::_thesis: ex k being Element of NAT st
( x = k or x = - k )
then  x in [:{0},NAT:] \ {[0,0]} by A3, XBOOLE_0:def_5;
hence  ex k being Element of NAT st
( x = k or x = - k ) by Lm1; ::_thesis: verum
end;
end;
end;
given k being Element of NAT  such that A4: ( x = k or x = - k ) ; ::_thesis: x in I
percases ( x = k or ( x = - k & k <> x ) ) by A4;
supposeA5: x = k ; ::_thesis: x in I
then A6: not x in {[0,0]} by NUMBERS:def_1, XBOOLE_0:def_5;
 x in NAT \/ [:{0},NAT:] by A5, XBOOLE_0:def_3;
hence  x in I by A1, A6, NUMBERS:def_4, XBOOLE_0:def_5; ::_thesis: verum
end;
suppose ( x = - k & k <> x ) ; ::_thesis: x in I
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  x in I by A1, A8, NUMBERS:def_4, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
assume A9: for x being set holds
( x in I iff ex k being Element of NAT st
( x = k or x = - k ) ) ; ::_thesis: I = INT
thus  I c= INT :: according to XBOOLE_0:def_10 ::_thesis: INT c= I
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in I or x in INT )
assume  x in I ; ::_thesis: x in INT
then consider k being Element of NAT  such that
A10: ( x = k or x = - k ) by A9;
percases ( x = k or ( x = - k & k <> x ) ) by A10;
supposeA11: x = k ; ::_thesis: x in INT
then A12: not x in {[0,0]} by NUMBERS:def_1, XBOOLE_0:def_5;
 x in NAT \/ [:{0},NAT:] by A11, XBOOLE_0:def_3;
hence  x in INT by A12, NUMBERS:def_4, XBOOLE_0:def_5; ::_thesis: verum
end;
suppose ( x = - k & k <> x ) ; ::_thesis: x in INT
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  x in INT by A14, NUMBERS:def_4, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in INT or x in I )
assume A15: x in INT ; ::_thesis: x in I
then A16: not x in {[0,0]} by NUMBERS:def_4, XBOOLE_0:def_5;
percases ( x in NAT or x in [:{0},NAT:] ) by A15, NUMBERS:def_4, XBOOLE_0:def_3;
suppose x in NAT ; ::_thesis: x in I
hence  x in I by A9; ::_thesis: verum
end;
suppose x in [:{0},NAT:] ; ::_thesis: x in I
then  x in [:{0},NAT:] \ {[0,0]} by A16, XBOOLE_0:def_5;
then  ex k being Element of NAT st
( x = k or x = - k ) by Lm1;
hence  x in I by A9; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem Def1 defines INT INT_1:def_1_:_
 for b1 being set holds
( b1 = INT iff for x being set holds
( x in b1 iff ex k being Element of NAT st
( x = k or x = - k ) ) );

definition
let i be number ;
attri is integer  means :Def2: :: INT_1:def 2
i in INT ;
end;

:: deftheorem Def2 defines integer INT_1:def_2_:_
 for i being number holds
( i is integer iff i in INT );

registration
cluster ext-real V31() real integer for Element of REAL ;
existence
 ex b1 being Real st b1 is integer
proof
take  0 ; ::_thesis: 0 is integer
thus  0 in INT by Def1; :: according to INT_1:def_2 ::_thesis: verum
end;
cluster integer for set ;
existence
 ex b1 being number st b1 is integer
proof
take  0 ; ::_thesis: 0 is integer
thus  0 in INT by Def1; :: according to INT_1:def_2 ::_thesis: verum
end;
cluster  ->  integer for Element of INT ;
coherence
 for b1 being Element of INT holds b1 is integer by Def2;
end;

definition
mode Integer is integer number ;
end;

theorem Th1: :: INT_1:1
for r being real number
for k being Nat st ( r = k or r = - k ) holds
r is Integer
proof
let r be real number ; ::_thesis: for k being Nat st ( r = k or r = - k ) holds
r is Integer
let k be Nat; ::_thesis: ( ( r = k or r = - k ) implies r is Integer )
assume A1: ( r = k or r = - k ) ; ::_thesis: r is Integer
 k in NAT by ORDINAL1:def_12;
then  r in INT by A1, Def1;
hence  r is Integer ; ::_thesis: verum
end;

theorem Th2: :: INT_1:2
for r being real number st r is Integer holds
ex k being Element of NAT st
( r = k or r = - k )
proof
let r be real number ; ::_thesis: ( r is Integer implies ex k being Element of NAT st
( r = k or r = - k ) )
assume  r is Integer ; ::_thesis: ex k being Element of NAT st
( r = k or r = - k )
then  r is Element of INT by Def2;
hence  ex k being Element of NAT st
( r = k or r = - k ) by Def1; ::_thesis: verum
end;

registration
cluster natural  ->  integer for set ;
coherence
 for b1 being number st b1 is natural holds
b1 is integer by Th1;
end;

Lm3:  for x being set st x in INT holds
x in REAL
by NUMBERS:15;

registration
cluster integer  ->  real for set ;
coherence
 for b1 being number st b1 is integer holds
b1 is real
proof
let n be number ; ::_thesis: ( n is integer implies n is real )
assume  n is integer ; ::_thesis: n is real
then  n is Element of INT by Def2;
then reconsider n = n as Element of REAL by Lm3;
 n is real ;
hence  n is real ; ::_thesis: verum
end;
end;


registration
let i1, i2 be Integer;
clusteri1 + i2 ->  integer ;
coherence
 i1 + i2 is integer
proof
consider l being Element of NAT  such that
A1: ( i2 = l or i2 = - l ) by Th2;
consider k being Element of NAT  such that
A2: ( i1 = k or i1 = - k ) by Th2;
A3: now__::_thesis:_(_i1_=_-_k_&_i2_=_l_implies_i1_+_i2_is_Integer_)
A4: now__::_thesis:_(_l_-_k_<=_0_implies_l_-_k_is_Integer_)
assume  l - k <= 0 ; ::_thesis: l - k is Integer
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; ::_thesis: verum
end;
assume that
A6: i1 = - k and
A7: i2 = l ; ::_thesis: i1 + i2 is Integer
now__::_thesis:_(_0_<=_l_-_k_implies_l_-_k_is_Integer_)
assume  0 <= l - k ; ::_thesis: l - k is Integer
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 ; ::_thesis: verum
end;
hence  i1 + i2 is Integer by A6, A7, A4; ::_thesis: verum
end;
A8: now__::_thesis:_(_i1_=_k_&_i2_=_-_l_implies_i1_+_i2_is_Integer_)
A9: now__::_thesis:_(_k_-_l_<=_0_implies_k_-_l_is_Integer_)
assume  k - l <= 0 ; ::_thesis: k - l is Integer
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; ::_thesis: verum
end;
assume that
A11: i1 = k and
A12: i2 = - l ; ::_thesis: i1 + i2 is Integer
now__::_thesis:_(_0_<=_k_-_l_implies_k_-_l_is_Integer_)
assume  0 <= k - l ; ::_thesis: k - l is Integer
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 ; ::_thesis: verum
end;
hence  i1 + i2 is Integer by A11, A12, A9; ::_thesis: verum
end;
now__::_thesis:_(_i1_=_-_k_&_i2_=_-_l_implies_i1_+_i2_is_Integer_)
assume that
A13: i1 = - k and
A14: i2 = - l ; ::_thesis: i1 + i2 is Integer
 i1 + i2 = - (k + l) by A13, A14;
hence  i1 + i2 is Integer by Th1; ::_thesis: verum
end;
hence  i1 + i2 is integer by A2, A1, A8, A3; ::_thesis: verum
end;
clusteri1 * i2 ->  integer ;
coherence
 i1 * i2 is integer
proof
consider l being Element of NAT  such that
A15: ( i2 = l or i2 = - l ) by Th2;
consider k being Element of NAT  such that
A16: ( i1 = k or i1 = - k ) by Th2;
A17: now__::_thesis:_(_i1_=_-_k_&_i2_=_-_l_implies_i1_*_i2_is_Integer_)
assume that
A18: i1 = - k and
A19: i2 = - l ; ::_thesis: i1 * i2 is Integer
 i1 * i2 = k * l by A18, A19;
hence  i1 * i2 is Integer ; ::_thesis: verum
end;
now__::_thesis:_(_(_(_i1_=_-_k_&_i2_=_l_)_or_(_i1_=_k_&_i2_=_-_l_)_)_implies_i1_*_i2_is_Integer_)
assume  ( ( i1 = - k & i2 = l ) or ( i1 = k & i2 = - l ) ) ; ::_thesis: i1 * i2 is Integer
then  i1 * i2 = - (k * l) ;
hence  i1 * i2 is Integer by Th1; ::_thesis: verum
end;
hence  i1 * i2 is integer by A16, A15, A17; ::_thesis: verum
end;
end;

registration
let i0 be Integer;
cluster - i0 ->  integer ;
coherence
 - i0 is integer
proof
 ex k being Element of NAT st
( i0 = k or i0 = - k ) by Th2;
hence  - i0 is integer by Th1; ::_thesis: verum
end;
end;

registration
let i1, i2 be Integer;
clusteri1 - i2 ->  integer ;
coherence
 i1 - i2 is integer
proof
 i1 - i2 = i1 + (- i2) ;
hence  i1 - i2 is integer ; ::_thesis: verum
end;
end;

theorem Th3: :: INT_1:3
for i0 being Integer st 0 <= i0 holds
i0 in NAT
proof
let i0 be Integer; ::_thesis: ( 0 <= i0 implies i0 in NAT )
consider k being Element of NAT  such that
A1: ( i0 = k or i0 = - k ) by Th2;
assume  0 <= i0 ; ::_thesis: i0 in NAT
then  ( i0 = - k implies i0 is Element of NAT ) ;
hence  i0 in NAT by A1; ::_thesis: verum
end;

theorem :: INT_1:4
for r being real number st r is Integer holds
( r + 1 is Integer & r - 1 is Integer ) ;

theorem Th5: :: INT_1:5
for i2, i1 being Integer st i2 <= i1 holds
i1 - i2 in NAT
proof
let i2, i1 be Integer; ::_thesis: ( i2 <= i1 implies i1 - i2 in NAT )
assume  i2 <= i1 ; ::_thesis: i1 - i2 in NAT
then  i2 - i2 <= i1 - i2 by XREAL_1:9;
hence  i1 - i2 in NAT by Th3; ::_thesis: verum
end;

theorem Th6: :: INT_1:6
for k being Element of NAT
for i1, i2 being Integer st i1 + k = i2 holds
i1 <= i2
proof
let k be Element of NAT ; ::_thesis: for i1, i2 being Integer st i1 + k = i2 holds
i1 <= i2
let i1, i2 be Integer; ::_thesis: ( i1 + k = i2 implies i1 <= i2 )
reconsider i0 = k as Integer ;
assume  i1 + k = i2 ; ::_thesis: i1 <= i2
then  0 + (i1 + k) <= k + i2 by XREAL_1:6;
then  (i1 + i0) - i0 <= (i2 + i0) - i0 by XREAL_1:9;
hence  i1 <= i2 ; ::_thesis: verum
end;

Lm4:  for j being Element of NAT st j < 1 holds
j = 0
proof
let j be Element of NAT ; ::_thesis: ( j < 1 implies j = 0 )
assume  j < 1 ; ::_thesis: j = 0
then  j < 0 + 1 ;
hence  j = 0 by NAT_1:13; ::_thesis: verum
end;

Lm5:  for i1 being Integer st 0 < i1 holds
1 <= i1
proof
let i1 be Integer; ::_thesis: ( 0 < i1 implies 1 <= i1 )
assume A1: 0 < i1 ; ::_thesis: 1 <= i1
then reconsider i2 = i1 as Element of NAT by Th3;
 0 <> i2 by A1;
hence  1 <= i1 by Lm4; ::_thesis: verum
end;

theorem Th7: :: INT_1:7
for i0, i1 being Integer st i0 < i1 holds
i0 + 1 <= i1
proof
let i0, i1 be Integer; ::_thesis: ( i0 < i1 implies i0 + 1 <= i1 )
assume  i0 < i1 ; ::_thesis: i0 + 1 <= i1
then  i0 + (- i0) < i1 + (- i0) by XREAL_1:6;
then  1 <= i1 + (- i0) by Lm5;
then  1 + i0 <= (i1 + (- i0)) + i0 by XREAL_1:6;
hence  i0 + 1 <= i1 ; ::_thesis: verum
end;

theorem Th8: :: INT_1:8
for i1 being Integer st i1 < 0 holds
i1 <= - 1
proof
let i1 be Integer; ::_thesis: ( i1 < 0 implies i1 <= - 1 )
assume  i1 < 0 ; ::_thesis: i1 <= - 1
then  0 < - i1 by XREAL_1:58;
then  1 <= - i1 by Lm5;
then  - (- i1) <= - 1 by XREAL_1:24;
hence  i1 <= - 1 ; ::_thesis: verum
end;

theorem Th9: :: INT_1:9
for i1, i2 being Integer holds
( i1 * i2 = 1 iff ( ( i1 = 1 & i2 = 1 ) or ( i1 = - 1 & i2 = - 1 ) ) )
proof
let i1, i2 be Integer; ::_thesis: ( i1 * i2 = 1 iff ( ( i1 = 1 & i2 = 1 ) or ( i1 = - 1 & i2 = - 1 ) ) )
thus  ( not i1 * i2 = 1 or ( i1 = 1 & i2 = 1 ) or ( i1 = - 1 & i2 = - 1 ) ) ::_thesis: ( ( ( i1 = 1 & i2 = 1 ) or ( i1 = - 1 & i2 = - 1 ) ) implies i1 * i2 = 1 )
proof
assume A1: i1 * i2 = 1 ; ::_thesis: ( ( i1 = 1 & i2 = 1 ) or ( i1 = - 1 & i2 = - 1 ) )
then A2: not i2 = 0 ;
A3: now__::_thesis:_(_i1_<_0_&_i2_<_0_implies_(_i1_=_-_1_&_i2_=_-_1_)_)
A4: (- i1) * (- i2) = i1 * i2 ;
assume that
A5: i1 < 0 and
A6: i2 < 0 ; ::_thesis: ( i1 = - 1 & i2 = - 1 )
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; ::_thesis: verum
end;
A8: now__::_thesis:_(_0_<_i1_&_0_<_i2_implies_(_i1_=_1_&_i2_=_1_)_)
assume that
A9: 0 < i1 and
A10: 0 < i2 ; ::_thesis: ( i1 = 1 & i2 = 1 )
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; ::_thesis: verum
end;
 not i1 = 0 by A1;
hence  ( ( i1 = 1 & i2 = 1 ) or ( i1 = - 1 & i2 = - 1 ) ) by A1, A2, A8, A3; ::_thesis: verum
end;
thus  ( ( ( i1 = 1 & i2 = 1 ) or ( i1 = - 1 & i2 = - 1 ) ) implies i1 * i2 = 1 ) ; ::_thesis: verum
end;

theorem :: INT_1:10
for i1, i2 being Integer holds
( i1 * i2 = - 1 iff ( ( i1 = - 1 & i2 = 1 ) or ( i1 = 1 & i2 = - 1 ) ) )
proof
let i1, i2 be Integer; ::_thesis: ( i1 * i2 = - 1 iff ( ( i1 = - 1 & i2 = 1 ) or ( i1 = 1 & i2 = - 1 ) ) )
thus  ( not i1 * i2 = - 1 or ( i1 = - 1 & i2 = 1 ) or ( i1 = 1 & i2 = - 1 ) ) ::_thesis: ( ( ( i1 = - 1 & i2 = 1 ) or ( i1 = 1 & i2 = - 1 ) ) implies i1 * i2 = - 1 )
proof
assume  i1 * i2 = - 1 ; ::_thesis: ( ( i1 = - 1 & i2 = 1 ) or ( i1 = 1 & i2 = - 1 ) )
then  (- i1) * i2 = 1 ;
then  ( ( - (- i1) = - 1 & i2 = 1 ) or ( - i1 = - 1 & i2 = - 1 ) ) by Th9;
hence  ( ( i1 = - 1 & i2 = 1 ) or ( i1 = 1 & i2 = - 1 ) ) ; ::_thesis: verum
end;
assume  ( ( i1 = - 1 & i2 = 1 ) or ( i1 = 1 & i2 = - 1 ) ) ; ::_thesis: i1 * i2 = - 1
hence  i1 * i2 = - 1 ; ::_thesis: verum
end;

Lm6:  for i0, i1 being Integer st i0 <= i1 holds
ex k being Element of NAT st i0 + k = i1
proof
let i0, i1 be Integer; ::_thesis: ( i0 <= i1 implies ex k being Element of NAT st i0 + k = i1 )
assume  i0 <= i1 ; ::_thesis: ex k being Element of NAT st i0 + k = i1
then reconsider k = i1 - i0 as Element of NAT by Th5;
 i0 + k = i1 ;
hence  ex k being Element of NAT st i0 + k = i1 ; ::_thesis: verum
end;

Lm7:  for i0, i1 being Integer st i0 <= i1 holds
ex k being Element of NAT st i1 - k = i0
proof
let i0, i1 be Integer; ::_thesis: ( i0 <= i1 implies ex k being Element of NAT st i1 - k = i0 )
assume  i0 <= i1 ; ::_thesis: ex k being Element of NAT st i1 - k = i0
then reconsider k = i1 - i0 as Element of NAT by Th5;
 i1 - k = i0 ;
hence  ex k being Element of NAT st i1 - k = i0 ; ::_thesis: verum
end;

scheme :: INT_1:sch 1
SepInt{ P1[ Integer] } :
 ex X being Subset of INT st
for x being Integer holds
( x in X iff P1[x] )
proof
defpred S1[ set ] means  ex i0 being Integer st
( i0 = $1 & P1[i0] );
consider X being set  such that
A1: for y being set holds
( y in X iff ( y in INT & S1[y] ) ) from XBOOLE_0:sch_1();
 for y being set st y in X holds
y in INT by A1;
then reconsider X = X as Subset of INT by TARSKI:def_3;
take  X ; ::_thesis: for x being Integer holds
( x in X iff P1[x] )
let i0 be Integer; ::_thesis: ( i0 in X iff P1[i0] )
A2: ( i0 in X implies P1[i0] )
proof
assume  i0 in X ; ::_thesis: P1[i0]
then  ex i1 being Integer st
( i0 = i1 & P1[i1] ) by A1;
hence  P1[i0] ; ::_thesis: verum
end;
 ( P1[i0] implies i0 in X )
proof
assume A3: P1[i0] ; ::_thesis: i0 in X
 i0 in INT by Def2;
hence  i0 in X by A1, A3; ::_thesis: verum
end;
hence  ( i0 in X iff P1[i0] ) by A2; ::_thesis: verum
end;

scheme :: INT_1:sch 2
IntIndUp{ F1() ->  Integer, P1[ Integer] } :
 for i0 being Integer st F1() <= i0 holds
P1[i0]
provided
A1: P1[F1()] and
A2: for i2 being Integer st F1() <= i2 & P1[i2] holds
P1[i2 + 1]
proof
defpred S1[ Nat] means  for i2 being Integer st $1 = i2 - F1() holds
P1[i2];
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
reconsider i8 = k as Integer ;
assume A4: S1[k] ; ::_thesis: S1[k + 1]
let i2 be Integer; ::_thesis: ( k + 1 = i2 - F1() implies P1[i2] )
assume A5: k + 1 = i2 - F1() ; ::_thesis: P1[i2]
then  i2 - 1 = i8 + F1() ;
then A6: F1() <= i2 - 1 by Th6;
 k = (i2 - 1) - F1() by A5;
then  P1[(i2 - 1) + 1] by A2, A4, A6;
hence  P1[i2] ; ::_thesis: verum
end;
let i0 be Integer; ::_thesis: ( F1() <= i0 implies P1[i0] )
assume  F1() <= i0 ; ::_thesis: P1[i0]
then reconsider l = i0 - F1() as Element of NAT by Th5;
A7: l = i0 - F1() ;
A8: S1[ 0 ] by A1;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A8, A3);
hence  P1[i0] by A7; ::_thesis: verum
end;

scheme :: INT_1:sch 3
IntIndDown{ F1() ->  Integer, P1[ Integer] } :
 for i0 being Integer st i0 <= F1() holds
P1[i0]
provided
A1: P1[F1()] and
A2: for i2 being Integer st i2 <= F1() & P1[i2] holds
P1[i2 - 1]
proof
defpred S1[ Integer] means  for i2 being Integer st $1 = - i2 holds
P1[i2];
A3: for i2 being Integer st - F1() <= i2 & S1[i2] holds
S1[i2 + 1]
proof
let i2 be Integer; ::_thesis: ( - F1() <= i2 & S1[i2] implies S1[i2 + 1] )
assume that
A4: - F1() <= i2 and
A5: S1[i2] ; ::_thesis: S1[i2 + 1]
let i3 be Integer; ::_thesis: ( i2 + 1 = - i3 implies P1[i3] )
assume A6: i2 + 1 = - i3 ; ::_thesis: P1[i3]
then A7: i2 = - (i3 + 1) ;
 - ((- i3) - 1) <= - (- F1()) by A4, A6, XREAL_1:24;
then  P1[(i3 + 1) - 1] by A2, A5, A7;
hence  P1[i3] ; ::_thesis: verum
end;
let i0 be Integer; ::_thesis: ( i0 <= F1() implies P1[i0] )
assume  i0 <= F1() ; ::_thesis: P1[i0]
then A8: - F1() <= - i0 by XREAL_1:24;
A9: S1[ - F1()] by A1;
 for i2 being Integer st - F1() <= i2 holds
S1[i2] from INT_1:sch_2(A9, A3);
hence  P1[i0] by A8; ::_thesis: verum
end;

scheme :: INT_1:sch 4
IntIndFull{ F1() ->  Integer, P1[ Integer] } :
 for i0 being Integer holds P1[i0]
provided
A1: P1[F1()] and
A2: for i2 being Integer st P1[i2] holds
( P1[i2 - 1] & P1[i2 + 1] )
proof
let i0 be Integer; ::_thesis: P1[i0]
A3: P1[F1()] by A1;
A4: now__::_thesis:_(_i0_<=_F1()_implies_P1[i0]_)
A5: for i2 being Integer st i2 <= F1() & P1[i2] holds
P1[i2 - 1] by A2;
A6: for i2 being Integer st i2 <= F1() holds
P1[i2] from INT_1:sch_3(A3, A5);
assume  i0 <= F1() ; ::_thesis: P1[i0]
hence  P1[i0] by A6; ::_thesis: verum
end;
now__::_thesis:_(_F1()_<=_i0_implies_P1[i0]_)
A7: for i2 being Integer st F1() <= i2 & P1[i2] holds
P1[i2 + 1] by A2;
A8: for i2 being Integer st F1() <= i2 holds
P1[i2] from INT_1:sch_2(A3, A7);
assume  F1() <= i0 ; ::_thesis: P1[i0]
hence  P1[i0] by A8; ::_thesis: verum
end;
hence  P1[i0] by A4; ::_thesis: verum
end;

scheme :: INT_1:sch 5
IntMin{ F1() ->  Integer, P1[ Integer] } :
 ex i0 being Integer st
( P1[i0] & ( for i1 being Integer st P1[i1] holds
i0 <= i1 ) )
provided
A1: for i1 being Integer st P1[i1] holds
F1() <= i1 and
A2: ex i1 being Integer st P1[i1]
proof
defpred S1[ Nat] means P1[F1() + $1];
consider i1 being Integer such that
A3: P1[i1] by A2;
 ex k being Element of NAT st F1() + k = i1 by A1, A3, Lm6;
then A4: ex k being Nat st S1[k] by A3;
consider l being Nat such that
A5: ( S1[l] & ( for n being Nat st S1[n] holds
l <= n ) ) from NAT_1:sch_5(A4);
take i0 = F1() + l; ::_thesis: ( P1[i0] & ( for i1 being Integer st P1[i1] holds
i0 <= i1 ) )
 for i1 being Integer st P1[i1] holds
i0 <= i1
proof
let i1 be Integer; ::_thesis: ( P1[i1] implies i0 <= i1 )
assume A6: P1[i1] ; ::_thesis: i0 <= i1
then  ex n being Element of NAT st F1() + n = i1 by A1, Lm6;
then  i0 - F1() <= i1 - F1() by A5, A6;
hence  i0 <= i1 by XREAL_1:9; ::_thesis: verum
end;
hence  ( P1[i0] & ( for i1 being Integer st P1[i1] holds
i0 <= i1 ) ) by A5; ::_thesis: verum
end;

scheme :: INT_1:sch 6
IntMax{ F1() ->  Integer, P1[ Integer] } :
 ex i0 being Integer st
( P1[i0] & ( for i1 being Integer st P1[i1] holds
i1 <= i0 ) )
provided
A1: for i1 being Integer st P1[i1] holds
i1 <= F1() and
A2: ex i1 being Integer st P1[i1]
proof
defpred S1[ Nat] means P1[F1() - $1];
consider i1 being Integer such that
A3: P1[i1] by A2;
 ex k being Element of NAT st i1 = F1() - k by A1, A3, Lm7;
then A4: ex k being Nat st S1[k] by A3;
consider l being Nat such that
A5: ( S1[l] & ( for n being Nat st S1[n] holds
l <= n ) ) from NAT_1:sch_5(A4);
take i0 = F1() - l; ::_thesis: ( P1[i0] & ( for i1 being Integer st P1[i1] holds
i1 <= i0 ) )
 for i1 being Integer st P1[i1] holds
i1 <= i0
proof
let i1 be Integer; ::_thesis: ( P1[i1] implies i1 <= i0 )
assume A6: P1[i1] ; ::_thesis: i1 <= i0
then consider n being Element of NAT  such that
A7: F1() - n = i1 by A1, Lm7;
 l <= n by A5, A6, A7;
then  (F1() + (- i0)) - F1() <= (F1() - i1) - F1() by A7, XREAL_1:9;
then  - i0 <= (F1() + (- i1)) - F1() ;
hence  i1 <= i0 by XREAL_1:24; ::_thesis: verum
end;
hence  ( P1[i0] & ( for i1 being Integer st P1[i1] holds
i1 <= i0 ) ) by A5; ::_thesis: verum
end;

definition
let i1, i2 be Integer;
predi1 divides i2 means :Def3: :: INT_1:def 3
 ex i3 being Integer st i2 = i1 * i3;
reflexivity
 for i1 being Integer ex i3 being Integer st i1 = i1 * i3
proof
let a be Integer; ::_thesis: ex i3 being Integer st a = a * i3
take  1 ; ::_thesis: a = a * 1
thus  a = a * 1 ; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines divides INT_1:def_3_:_
 for i1, i2 being Integer holds
( i1 divides i2 iff ex i3 being Integer st i2 = i1 * i3 );

definition
let i1, i2, i3 be Integer;
predi1,i2 are_congruent_mod i3 means :: INT_1:def 4
i3 divides i1 - i2;
end;

:: deftheorem  defines are_congruent_mod INT_1:def_4_:_
 for i1, i2, i3 being Integer holds
( i1,i2 are_congruent_mod i3 iff i3 divides i1 - i2 );

definition
let i1, i2, i3 be Integer;
redefine pred i1,i2 are_congruent_mod i3 means :Def5: :: INT_1:def 5
 ex i4 being Integer st i3 * i4 = i1 - i2;
compatibility
 ( i1,i2 are_congruent_mod i3 iff ex i4 being Integer st i3 * i4 = i1 - i2 )
proof
thus  ( i1,i2 are_congruent_mod i3 implies ex i4 being Integer st i3 * i4 = i1 - i2 ) ::_thesis: ( ex i4 being Integer st i3 * i4 = i1 - i2 implies i1,i2 are_congruent_mod i3 )
proof
assume  i3 divides i1 - i2 ; :: according to INT_1:def_4 ::_thesis: ex i4 being Integer st i3 * i4 = i1 - i2
hence  ex i4 being Integer st i3 * i4 = i1 - i2 by Def3; ::_thesis: verum
end;
given i4 being Integer such that A1: i3 * i4 = i1 - i2 ; ::_thesis: i1,i2 are_congruent_mod i3
take  i4 ; :: according to INT_1:def_3,INT_1:def_4 ::_thesis: i1 - i2 = i3 * i4
thus  i1 - i2 = i3 * i4 by A1; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines are_congruent_mod INT_1:def_5_:_
 for i1, i2, i3 being Integer holds
( i1,i2 are_congruent_mod i3 iff ex i4 being Integer st i3 * i4 = i1 - i2 );

theorem :: INT_1:11
for i1, i2 being Integer holds i1,i1 are_congruent_mod i2
proof
let i1, i2 be Integer; ::_thesis: i1,i1 are_congruent_mod i2
 i2 * 0 = i1 - i1 ;
hence  i1,i1 are_congruent_mod i2 by Def5; ::_thesis: verum
end;

theorem :: INT_1:12
for i1 being Integer holds
( i1, 0 are_congruent_mod i1 & 0 ,i1 are_congruent_mod i1 )
proof
let i1 be Integer; ::_thesis: ( i1, 0 are_congruent_mod i1 & 0 ,i1 are_congruent_mod i1 )
A1: i1 * (- 1) = 0 - i1 ;
 i1 * 1 = i1 - 0 ;
hence  ( i1, 0 are_congruent_mod i1 & 0 ,i1 are_congruent_mod i1 ) by A1, Def5; ::_thesis: verum
end;

theorem :: INT_1:13
for i1, i2 being Integer holds i1,i2 are_congruent_mod 1
proof
let i1, i2 be Integer; ::_thesis: i1,i2 are_congruent_mod 1
 i1 - i2 = 1 * (i1 - i2) ;
hence  i1,i2 are_congruent_mod 1 by Def5; ::_thesis: verum
end;

theorem :: INT_1:14
for i1, i2, i3 being Integer st i1,i2 are_congruent_mod i3 holds
i2,i1 are_congruent_mod i3
proof
let i1, i2, i3 be Integer; ::_thesis: ( i1,i2 are_congruent_mod i3 implies i2,i1 are_congruent_mod i3 )
assume  i1,i2 are_congruent_mod i3 ; ::_thesis: i2,i1 are_congruent_mod i3
then consider i0 being Integer such that
A1: i1 - i2 = i3 * i0 by Def5;
 i2 - i1 = i3 * (- i0) by A1;
hence  i2,i1 are_congruent_mod i3 by Def5; ::_thesis: verum
end;

theorem :: INT_1:15
for i1, i2, i5, i3 being Integer st i1,i2 are_congruent_mod i5 & i2,i3 are_congruent_mod i5 holds
i1,i3 are_congruent_mod i5
proof
let i1, i2, i5, i3 be Integer; ::_thesis: ( i1,i2 are_congruent_mod i5 & i2,i3 are_congruent_mod i5 implies i1,i3 are_congruent_mod i5 )
assume that
A1: i1,i2 are_congruent_mod i5 and
A2: i2,i3 are_congruent_mod i5 ; ::_thesis: i1,i3 are_congruent_mod i5
consider i8 being Integer such that
A3: i5 * i8 = i1 - i2 by A1, Def5;
consider i9 being Integer such that
A4: i5 * i9 = i2 - i3 by A2, Def5;
 i5 * (i8 + i9) = i1 - i3 by A3, A4;
hence  i1,i3 are_congruent_mod i5 by Def5; ::_thesis: verum
end;

theorem :: INT_1:16
for i1, i2, i5, i3, i4 being Integer st i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 holds
i1 + i3,i2 + i4 are_congruent_mod i5
proof
let i1, i2, i5, i3, i4 be Integer; ::_thesis: ( i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 implies i1 + i3,i2 + i4 are_congruent_mod i5 )
assume that
A1: i1,i2 are_congruent_mod i5 and
A2: i3,i4 are_congruent_mod i5 ; ::_thesis: i1 + i3,i2 + i4 are_congruent_mod i5
consider i8 being Integer such that
A3: i5 * i8 = i1 - i2 by A1, Def5;
consider i9 being Integer such that
A4: i5 * i9 = i3 - i4 by A2, Def5;
 i5 * (i8 + i9) = (i1 + i3) - (i2 + i4) by A3, A4;
hence  i1 + i3,i2 + i4 are_congruent_mod i5 by Def5; ::_thesis: verum
end;

theorem :: INT_1:17
for i1, i2, i5, i3, i4 being Integer st i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 holds
i1 - i3,i2 - i4 are_congruent_mod i5
proof
let i1, i2, i5, i3, i4 be Integer; ::_thesis: ( i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 implies i1 - i3,i2 - i4 are_congruent_mod i5 )
assume that
A1: i1,i2 are_congruent_mod i5 and
A2: i3,i4 are_congruent_mod i5 ; ::_thesis: i1 - i3,i2 - i4 are_congruent_mod i5
consider i8 being Integer such that
A3: i5 * i8 = i1 - i2 by A1, Def5;
consider i9 being Integer such that
A4: i5 * i9 = i3 - i4 by A2, Def5;
 (i1 - i3) - (i2 - i4) = i5 * (i8 - i9) by A3, A4;
hence  i1 - i3,i2 - i4 are_congruent_mod i5 by Def5; ::_thesis: verum
end;

theorem :: INT_1:18
for i1, i2, i5, i3, i4 being Integer st i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 holds
i1 * i3,i2 * i4 are_congruent_mod i5
proof
let i1, i2, i5, i3, i4 be Integer; ::_thesis: ( i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 implies i1 * i3,i2 * i4 are_congruent_mod i5 )
assume that
A1: i1,i2 are_congruent_mod i5 and
A2: i3,i4 are_congruent_mod i5 ; ::_thesis: i1 * i3,i2 * i4 are_congruent_mod i5
consider i8 being Integer such that
A3: i5 * i8 = i1 - i2 by A1, Def5;
consider i9 being Integer such that
A4: i5 * i9 = i3 - i4 by A2, Def5;
(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  i1 * i3,i2 * i4 are_congruent_mod i5 by Def5; ::_thesis: verum
end;

theorem :: INT_1:19
for i1, i2, i3, i5 being Integer holds
( i1 + i2,i3 are_congruent_mod i5 iff i1,i3 - i2 are_congruent_mod i5 )
proof
let i1, i2, i3, i5 be Integer; ::_thesis: ( i1 + i2,i3 are_congruent_mod i5 iff i1,i3 - i2 are_congruent_mod i5 )
thus  ( i1 + i2,i3 are_congruent_mod i5 implies i1,i3 - i2 are_congruent_mod i5 ) ::_thesis: ( i1,i3 - i2 are_congruent_mod i5 implies i1 + i2,i3 are_congruent_mod i5 )
proof
assume  i1 + i2,i3 are_congruent_mod i5 ; ::_thesis: i1,i3 - i2 are_congruent_mod i5
then A1: ex i0 being Integer st i5 * i0 = (i1 + i2) - i3 by Def5;
 (i1 + i2) - i3 = i1 - (i3 - i2) ;
hence  i1,i3 - i2 are_congruent_mod i5 by A1, Def5; ::_thesis: verum
end;
assume  i1,i3 - i2 are_congruent_mod i5 ; ::_thesis: i1 + i2,i3 are_congruent_mod i5
then A2: ex i0 being Integer st i5 * i0 = i1 - (i3 - i2) by Def5;
 i1 - (i3 - i2) = (i1 + i2) - i3 ;
hence  i1 + i2,i3 are_congruent_mod i5 by A2, Def5; ::_thesis: verum
end;

theorem :: INT_1:20
for i4, i5, i3, i1, i2 being Integer st i4 * i5 = i3 & i1,i2 are_congruent_mod i3 holds
i1,i2 are_congruent_mod i4
proof
let i4, i5, i3, i1, i2 be Integer; ::_thesis: ( i4 * i5 = i3 & i1,i2 are_congruent_mod i3 implies i1,i2 are_congruent_mod i4 )
assume A1: i4 * i5 = i3 ; ::_thesis: ( not i1,i2 are_congruent_mod i3 or i1,i2 are_congruent_mod i4 )
assume  i1,i2 are_congruent_mod i3 ; ::_thesis: i1,i2 are_congruent_mod i4
then consider i0 being Integer such that
A2: i3 * i0 = i1 - i2 by Def5;
 i1 - i2 = i4 * (i5 * i0) by A1, A2;
hence  i1,i2 are_congruent_mod i4 by Def5; ::_thesis: verum
end;

theorem :: INT_1:21
for i1, i2, i5 being Integer holds
( i1,i2 are_congruent_mod i5 iff i1 + i5,i2 are_congruent_mod i5 )
proof
let i1, i2, i5 be Integer; ::_thesis: ( i1,i2 are_congruent_mod i5 iff i1 + i5,i2 are_congruent_mod i5 )
thus  ( i1,i2 are_congruent_mod i5 implies i1 + i5,i2 are_congruent_mod i5 ) ::_thesis: ( i1 + i5,i2 are_congruent_mod i5 implies i1,i2 are_congruent_mod i5 )
proof
assume  i1,i2 are_congruent_mod i5 ; ::_thesis: i1 + i5,i2 are_congruent_mod i5
then consider i0 being Integer such that
A1: i5 * i0 = i1 - i2 by Def5;
 i5 * (i0 + 1) = (i1 + i5) - i2 by A1;
hence  i1 + i5,i2 are_congruent_mod i5 by Def5; ::_thesis: verum
end;
assume  i1 + i5,i2 are_congruent_mod i5 ; ::_thesis: i1,i2 are_congruent_mod i5
then consider i0 being Integer such that
A2: i5 * i0 = (i1 + i5) - i2 by Def5;
 i5 * (i0 - 1) = i1 - i2 by A2;
hence  i1,i2 are_congruent_mod i5 by Def5; ::_thesis: verum
end;

theorem :: INT_1:22
for i1, i2, i5 being Integer holds
( i1,i2 are_congruent_mod i5 iff i1 - i5,i2 are_congruent_mod i5 )
proof
let i1, i2, i5 be Integer; ::_thesis: ( i1,i2 are_congruent_mod i5 iff i1 - i5,i2 are_congruent_mod i5 )
thus  ( i1,i2 are_congruent_mod i5 implies i1 - i5,i2 are_congruent_mod i5 ) ::_thesis: ( i1 - i5,i2 are_congruent_mod i5 implies i1,i2 are_congruent_mod i5 )
proof
assume  i1,i2 are_congruent_mod i5 ; ::_thesis: i1 - i5,i2 are_congruent_mod i5
then consider i0 being Integer such that
A1: i5 * i0 = i1 - i2 by Def5;
 i5 * (i0 - 1) = (i1 - i5) - i2 by A1;
hence  i1 - i5,i2 are_congruent_mod i5 by Def5; ::_thesis: verum
end;
assume  i1 - i5,i2 are_congruent_mod i5 ; ::_thesis: i1,i2 are_congruent_mod i5
then consider i0 being Integer such that
A2: i5 * i0 = (i1 - i5) - i2 by Def5;
 i5 * (i0 + 1) = i1 - i2 by A2;
hence  i1,i2 are_congruent_mod i5 by Def5; ::_thesis: verum
end;

theorem Th23: :: INT_1:23
for r being real number
for i1, i2 being Integer st i1 <= r & r - 1 < i1 & i2 <= r & r - 1 < i2 holds
i1 = i2
proof
let r be real number ; ::_thesis: for i1, i2 being Integer st i1 <= r & r - 1 < i1 & i2 <= r & r - 1 < i2 holds
i1 = i2
let i1, i2 be Integer; ::_thesis: ( i1 <= r & r - 1 < i1 & i2 <= r & r - 1 < i2 implies i1 = i2 )
assume that
A1: i1 <= r and
A2: r - 1 < i1 and
A3: i2 <= r and
A4: r - 1 < i2 ; ::_thesis: i1 = i2
 i2 = i1 + (i2 - i1) ;
then consider i0 being Integer such that
A5: i2 = i1 + i0 ;
A6: now__::_thesis:_(_0_<_i0_implies_not_i1_<>_i2_)
assume that
A7: 0 < i0 and
 i1 <> i2 ; ::_thesis: contradiction
 1 <= i0 by A7, Lm5;
then  (r - 1) + 1 < i1 + i0 by A2, XREAL_1:8;
hence  contradiction by A3, A5; ::_thesis: verum
end;
A8: now__::_thesis:_(_i0_<_0_implies_not_i1_<>_i2_)
assume that
A9: i0 < 0 and
 i1 <> i2 ; ::_thesis: contradiction
 i0 <= - 1 by A9, Th8;
then  i1 + i0 <= r + (- 1) by A1, XREAL_1:7;
hence  contradiction by A4, A5; ::_thesis: verum
end;
 ( i0 = 0 implies i2 = i1 ) by A5;
hence  i1 = i2 by A8, A6; ::_thesis: verum
end;

theorem Th24: :: INT_1:24
for r being real number
for i1, i2 being Integer st r <= i1 & i1 < r + 1 & r <= i2 & i2 < r + 1 holds
i1 = i2
proof
let r be real number ; ::_thesis: for i1, i2 being Integer st r <= i1 & i1 < r + 1 & r <= i2 & i2 < r + 1 holds
i1 = i2
let i1, i2 be Integer; ::_thesis: ( r <= i1 & i1 < r + 1 & r <= i2 & i2 < r + 1 implies i1 = i2 )
assume that
A1: r <= i1 and
A2: i1 < r + 1 and
A3: r <= i2 and
A4: i2 < r + 1 ; ::_thesis: i1 = i2
 i2 = i1 + (i2 - i1) ;
then consider i0 being Integer such that
A5: i2 = i1 + i0 ;
A6: now__::_thesis:_(_i0_<_0_implies_not_i1_<>_i2_)
assume that
A7: i0 < 0 and
 i1 <> i2 ; ::_thesis: contradiction
 i0 <= - 1 by A7, Th8;
then  i1 + i0 < (r + 1) + (- 1) by A2, XREAL_1:8;
hence  contradiction by A3, A5; ::_thesis: verum
end;
A8: now__::_thesis:_(_0_<_i0_implies_not_i1_<>_i2_)
assume that
A9: 0 < i0 and
 i1 <> i2 ; ::_thesis: contradiction
 1 <= i0 by A9, Lm5;
hence  contradiction by A1, A4, A5, XREAL_1:7; ::_thesis: verum
end;
 ( i0 = 0 implies i2 = i1 ) by A5;
hence  i1 = i2 by A6, A8; ::_thesis: verum
end;

       Lm8:  for r being real number ex n being Element of NAT st r < n
proof
defpred S1[ Real] means  for r being real number st r in NAT holds
not $1 < r;
let r be real number ; ::_thesis: ex n being Element of NAT st r < n
consider Y being Subset of REAL such that
A1: for p1 being Real holds
( p1 in Y iff S1[p1] ) from SUBSET_1:sch_3();
 for r, p1 being real number st r in NAT & p1 in Y holds
r <= p1 by A1;
then consider g2 being real number  such that
A2: for r, p being real number st r in NAT & p in Y holds
( r <= g2 & g2 <= p ) by AXIOMS:1;
A3: g2 + (- 1) < g2 + 0 by XREAL_1:6;
 for g being real number ex r being real number st
( r in NAT & g < r )
proof
given g1 being real number  such that A4: for r being real number st r in NAT holds
not g1 < r ; ::_thesis: contradiction
 g1 is Real by XREAL_0:def_1;
then A5: g1 in Y by A1, A4;
now__::_thesis:_g2_-_1_in_Y
assume  not g2 - 1 in Y ; ::_thesis: contradiction
then consider r1 being real number  such that
A6: r1 in NAT and
A7: g2 - 1 < r1 by A1;
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; ::_thesis: verum
end;
hence  contradiction by A2, A3; ::_thesis: verum
end;
then consider p being real number  such that
A9: p in NAT and
A10: r < p ;
reconsider p = p as Element of NAT by A9;
take  p ; ::_thesis: r < p
thus  r < p by A10; ::_thesis: verum
end;

definition
let r be real number ;
func[\r/] ->  Integer means :Def6: :: INT_1:def 6
( it <= r & r - 1 < it );
existence
 ex b1 being Integer st
( b1 <= r & r - 1 < b1 )
proof
defpred S1[ Integer] means r < $1;
consider n being Element of NAT  such that
A1: - r < n by Lm8;
A2: - n < - (- r) by A1, XREAL_1:24;
A3: for i1 being Integer st S1[i1] holds
- n <= i1
proof
let i1 be Integer; ::_thesis: ( S1[i1] implies - n <= i1 )
assume  r < i1 ; ::_thesis: - n <= i1
then  r + (- n) < i1 + r by A2, XREAL_1:8;
hence  - n <= i1 by XREAL_1:6; ::_thesis: verum
end;
 ex n being Element of NAT st r < n by Lm8;
then A4: ex i0 being Integer st S1[i0] ;
consider i1 being Integer such that
A5: ( S1[i1] & ( for i2 being Integer st S1[i2] holds
i1 <= i2 ) ) from INT_1:sch_5(A3, A4);
A6: r - 1 < i1 - 1 by A5, XREAL_1:9;
 ( r < i1 - 1 implies i1 <= i1 - 1 ) by A5;
hence  ex b1 being Integer st
( b1 <= r & r - 1 < b1 ) by A6, XREAL_1:146; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Integer st b1 <= r & r - 1 < b1 & b2 <= r & r - 1 < b2 holds
b1 = b2 by Th23;
projectivity
 for b1 being Integer
for b2 being real number st b1 <= b2 & b2 - 1 < b1 holds
( b1 <= b1 & b1 - 1 < b1 ) by XREAL_1:44;
end;

:: deftheorem Def6 defines [\ INT_1:def_6_:_
 for r being real number
for b2 being Integer holds
( b2 = [\r/] iff ( b2 <= r & r - 1 < b2 ) );

theorem Th25: :: INT_1:25
for r being real number holds
( [\r/] = r iff r is integer )
proof
let r be real number ; ::_thesis: ( [\r/] = r iff r is integer )
 ( r is Integer implies [\r/] = r )
proof
 r + 0 < r + 1 by XREAL_1:6;
then A1: r - 1 < (r + 1) - 1 by XREAL_1:9;
assume  r is Integer ; ::_thesis: [\r/] = r
hence  [\r/] = r by A1, Def6; ::_thesis: verum
end;
hence  ( [\r/] = r iff r is integer ) ; ::_thesis: verum
end;

theorem Th26: :: INT_1:26
for r being real number holds
( [\r/] < r iff not r is integer )
proof
let r be real number ; ::_thesis: ( [\r/] < r iff not r is integer )
now__::_thesis:_(_r_is_not_Integer_implies_[\r/]_<_r_)
assume A1: r is not Integer ; ::_thesis: [\r/] < r
 [\r/] <= r by Def6;
hence  [\r/] < r by A1, XXREAL_0:1; ::_thesis: verum
end;
hence  ( [\r/] < r iff not r is integer ) by Th25; ::_thesis: verum
end;

theorem :: INT_1:27
for r being real number holds
( [\r/] - 1 < r & [\r/] < r + 1 )
proof
let r be real number ; ::_thesis: ( [\r/] - 1 < r & [\r/] < r + 1 )
 [\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  ( [\r/] - 1 < r & [\r/] < r + 1 ) by A1; ::_thesis: verum
end;

theorem Th28: :: INT_1:28
for r being real number
for i0 being Integer holds [\r/] + i0 = [\(r + i0)/]
proof
let r be real number ; ::_thesis: for i0 being Integer holds [\r/] + i0 = [\(r + i0)/]
let i0 be Integer; ::_thesis: [\r/] + i0 = [\(r + i0)/]
 r - 1 < [\r/] by Def6;
then  (r - 1) + i0 < [\r/] + i0 by XREAL_1:6;
then A1: (r + i0) - 1 < [\r/] + i0 ;
 [\r/] <= r by Def6;
then  [\r/] + i0 <= r + i0 by XREAL_1:6;
hence  [\r/] + i0 = [\(r + i0)/] by A1, Def6; ::_thesis: verum
end;

theorem Th29: :: INT_1:29
for r being real number holds r < [\r/] + 1
proof
let r be real number ; ::_thesis: r < [\r/] + 1
 r - 1 < [\r/] by Def6;
then  (r - 1) + 1 < [\r/] + 1 by XREAL_1:6;
hence  r < [\r/] + 1 ; ::_thesis: verum
end;

definition
let r be real number ;
func[/r\] ->  Integer means :Def7: :: INT_1:def 7
( r <= it & it < r + 1 );
existence
 ex b1 being Integer st
( r <= b1 & b1 < r + 1 )
proof
A1: now__::_thesis:_(_r_is_Integer_implies_(_r_<=_[\r/]_&_[\r/]_<_r_+_1_)_)
A2: r + 0 < r + 1 by XREAL_1:6;
assume  r is Integer ; ::_thesis: ( r <= [\r/] & [\r/] < r + 1 )
hence  ( r <= [\r/] & [\r/] < r + 1 ) by A2, Th25; ::_thesis: verum
end;
now__::_thesis:_(_r_is_not_Integer_implies_(_r_<=_[\r/]_+_1_&_[\r/]_+_1_<_r_+_1_)_)
assume  r is not Integer ; ::_thesis: ( r <= [\r/] + 1 & [\r/] + 1 < r + 1 )
then  [\r/] < r by Th26;
hence  ( r <= [\r/] + 1 & [\r/] + 1 < r + 1 ) by Th29, XREAL_1:6; ::_thesis: verum
end;
hence  ex b1 being Integer st
( r <= b1 & b1 < r + 1 ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Integer st r <= b1 & b1 < r + 1 & r <= b2 & b2 < r + 1 holds
b1 = b2 by Th24;
projectivity
 for b1 being Integer
for b2 being real number st b2 <= b1 & b1 < b2 + 1 holds
( b1 <= b1 & b1 < b1 + 1 ) by XREAL_1:29;
end;

:: deftheorem Def7 defines [/ INT_1:def_7_:_
 for r being real number
for b2 being Integer holds
( b2 = [/r\] iff ( r <= b2 & b2 < r + 1 ) );

theorem Th30: :: INT_1:30
for r being real number holds
( [/r\] = r iff r is integer )
proof
let r be real number ; ::_thesis: ( [/r\] = r iff r is integer )
 r + 0 < r + 1 by XREAL_1:6;
hence  ( [/r\] = r iff r is integer ) by Def7; ::_thesis: verum
end;

theorem Th31: :: INT_1:31
for r being real number holds
( r < [/r\] iff not r is integer )
proof
let r be real number ; ::_thesis: ( r < [/r\] iff not r is integer )
now__::_thesis:_(_r_is_not_Integer_implies_r_<_[/r\]_)
assume A1: r is not Integer ; ::_thesis: r < [/r\]
 r <= [/r\] by Def7;
hence  r < [/r\] by A1, XXREAL_0:1; ::_thesis: verum
end;
hence  ( r < [/r\] iff not r is integer ) by Th30; ::_thesis: verum
end;

theorem :: INT_1:32
for r being real number holds
( r - 1 < [/r\] & r < [/r\] + 1 )
proof
let r be real number ; ::_thesis: ( r - 1 < [/r\] & r < [/r\] + 1 )
 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  ( r - 1 < [/r\] & r < [/r\] + 1 ) by A1; ::_thesis: verum
end;

theorem :: INT_1:33
for r being real number
for i0 being Integer holds [/r\] + i0 = [/(r + i0)\]
proof
let r be real number ; ::_thesis: for i0 being Integer holds [/r\] + i0 = [/(r + i0)\]
let i0 be Integer; ::_thesis: [/r\] + i0 = [/(r + i0)\]
 [/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  [/r\] + i0 = [/(r + i0)\] by A1, Def7; ::_thesis: verum
end;

theorem Th34: :: INT_1:34
for r being real number holds
( [\r/] = [/r\] iff r is integer )
proof
let r be real number ; ::_thesis: ( [\r/] = [/r\] iff r is integer )
A1: now__::_thesis:_(_r_is_not_Integer_implies_[\r/]_<>_[/r\]_)
assume A2: r is not Integer ; ::_thesis: [\r/] <> [/r\]
then  [\r/] < r by Th26;
hence  [\r/] <> [/r\] by A2, Th31; ::_thesis: verum
end;
now__::_thesis:_(_r_is_Integer_implies_(_[\r/]_=_r_&_r_=_[/r\]_&_[\r/]_=_[/r\]_)_)
assume  r is Integer ; ::_thesis: ( [\r/] = r & r = [/r\] & [\r/] = [/r\] )
hence  ( [\r/] = r & r = [/r\] ) by Th25, Th30; ::_thesis: [\r/] = [/r\]
hence  [\r/] = [/r\] ; ::_thesis: verum
end;
hence  ( [\r/] = [/r\] iff r is integer ) by A1; ::_thesis: verum
end;

theorem Th35: :: INT_1:35
for r being real number holds
( [\r/] < [/r\] iff not r is integer )
proof
let r be real number ; ::_thesis: ( [\r/] < [/r\] iff not r is integer )
now__::_thesis:_(_r_is_not_Integer_implies_[\r/]_<_[/r\]_)
assume A1: r is not Integer ; ::_thesis: [\r/] < [/r\]
then A2: r < [/r\] by Th31;
 [\r/] < r by A1, Th26;
hence  [\r/] < [/r\] by A2, XXREAL_0:2; ::_thesis: verum
end;
hence  ( [\r/] < [/r\] iff not r is integer ) by Th34; ::_thesis: verum
end;

theorem :: INT_1:36
for r being real number holds [\r/] <= [/r\]
proof
let r be real number ; ::_thesis: [\r/] <= [/r\]
A1: r <= [/r\] by Def7;
 [\r/] <= r by Def6;
hence  [\r/] <= [/r\] by A1, XXREAL_0:2; ::_thesis: verum
end;

theorem :: INT_1:37
for r being real number holds [\[/r\]/] = [/r\] by Th25;

theorem :: INT_1:38
canceled;

theorem :: INT_1:39
canceled;

theorem :: INT_1:40
for r being real number holds [/[\r/]\] = [\r/] by Th30;

theorem :: INT_1:41
for r being real number holds
( [\r/] = [/r\] iff not [\r/] + 1 = [/r\] )
proof
let r be real number ; ::_thesis: ( [\r/] = [/r\] iff not [\r/] + 1 = [/r\] )
set Diff = [/r\] + (- [\r/]);
A1: now__::_thesis:_(_r_is_not_Integer_implies_(_[\r/]_+_1_=_[/r\]_&_[\r/]_<>_[/r\]_)_)
assume  r is not Integer ; ::_thesis: ( [\r/] + 1 = [/r\] & [\r/] <> [/r\] )
then  [\r/] < [/r\] by Th35;
then  [\r/] + (- [\r/]) < [/r\] + (- [\r/]) by XREAL_1:6;
then A2: 1 <= [/r\] + (- [\r/]) by Lm5;
 r - 1 < [\r/] by Def6;
then A3: - [\r/] < - (r - 1) by XREAL_1:24;
 [/r\] < r + 1 by Def7;
then  [/r\] + (- [\r/]) < (r + 1) + (- (r - 1)) by A3, XREAL_1:8;
then  (([/r\] + (- [\r/])) + 1) + (- 1) <= (1 + 1) + (- 1) by Th7;
then  [\r/] + 1 = [\r/] + ([/r\] + (- [\r/])) by A2, XXREAL_0:1;
hence  ( [\r/] + 1 = [/r\] & [\r/] <> [/r\] ) ; ::_thesis: verum
end;
now__::_thesis:_(_r_is_Integer_implies_(_[\r/]_=_[/r\]_&_[\r/]_+_1_<>_[/r\]_)_)
assume  r is Integer ; ::_thesis: ( [\r/] = [/r\] & [\r/] + 1 <> [/r\] )
then  [\r/] = [/r\] by Th34;
hence  ( [\r/] = [/r\] & [\r/] + 1 <> [/r\] ) ; ::_thesis: verum
end;
hence  ( [\r/] = [/r\] iff not [\r/] + 1 = [/r\] ) by A1; ::_thesis: verum
end;

definition
let r be real number ;
func frac r ->  set  equals :: INT_1:def 8
r - [\r/];
coherence
 r - [\r/] is set ;
end;

:: deftheorem  defines frac INT_1:def_8_:_
 for r being real number holds frac r = r - [\r/];

registration
let r be real number ;
cluster frac r ->  real ;
coherence
 frac r is real ;
end;

definition
let r be real number ;
:: original: frac
redefine func frac r ->  Real;
coherence
 frac r is Real by XREAL_0:def_1;
end;

theorem :: INT_1:42
for r being real number holds r = [\r/] + (frac r) ;

theorem Th43: :: INT_1:43
for r being real number holds
( frac r < 1 & 0 <= frac r )
proof
let r be real number ; ::_thesis: ( frac r < 1 & 0 <= frac r )
 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  ( frac r < 1 & 0 <= frac r ) by A1; ::_thesis: verum
end;

theorem :: INT_1:44
for r being real number holds [\(frac r)/] = 0
proof
let r be real number ; ::_thesis: [\(frac r)/] = 0
[\(frac r)/] = [\(r + (- [\r/]))/]
.= [\r/] + (- [\r/]) by Th28
.= 0 ;
hence  [\(frac r)/] = 0 ; ::_thesis: verum
end;

theorem Th45: :: INT_1:45
for r being real number holds
( frac r = 0 iff r is integer )
proof
let r be real number ; ::_thesis: ( frac r = 0 iff r is integer )
now__::_thesis:_(_r_is_Integer_implies_frac_r_=_0_)
assume  r is Integer ; ::_thesis: frac r = 0
then  r = [\r/] by Th25;
hence  frac r = 0 ; ::_thesis: verum
end;
hence  ( frac r = 0 iff r is integer ) ; ::_thesis: verum
end;

theorem :: INT_1:46
for r being real number holds
( 0 < frac r iff not r is integer )
proof
let r be real number ; ::_thesis: ( 0 < frac r iff not r is integer )
now__::_thesis:_(_r_is_not_Integer_implies_0_<_frac_r_)
assume  r is not Integer ; ::_thesis: 0 < frac r
then  0 <> frac r ;
hence  0 < frac r by Th43; ::_thesis: verum
end;
hence  ( 0 < frac r iff not r is integer ) by Th45; ::_thesis: verum
end;

definition
let i1, i2 be Integer;
funci1 div i2 ->  Integer equals :: INT_1:def 9
[\(i1 / i2)/];
correctness
coherence
[\(i1 / i2)/] is Integer;
;
end;

:: deftheorem  defines div INT_1:def_9_:_
 for i1, i2 being Integer holds i1 div i2 = [\(i1 / i2)/];

definition
let i1, i2 be Integer;
funci1 mod i2 ->  Integer equals :Def10: :: INT_1:def 10
i1 - ((i1 div i2) * i2) if i2 <> 0
otherwise  0 ;
correctness
coherence
( ( i2 <> 0 implies i1 - ((i1 div i2) * i2) is Integer ) & ( not i2 <> 0 implies 0 is Integer ) );
consistency
for b1 being Integer holds verum;
;
end;

:: deftheorem Def10 defines mod INT_1:def_10_:_
 for i1, i2 being Integer holds
( ( i2 <> 0 implies i1 mod i2 = i1 - ((i1 div i2) * i2) ) & ( not i2 <> 0 implies i1 mod i2 = 0 ) );

theorem Th47: :: INT_1:47
for r being real number st r <> 0 holds
[\(r / r)/] = 1
proof
let r be real number ; ::_thesis: ( r <> 0 implies [\(r / r)/] = 1 )
assume  r <> 0 ; ::_thesis: [\(r / r)/] = 1
hence [\(r / r)/] = [\1/] by XCMPLX_1:60
.= 1 by Th25 ;
::_thesis: verum
end;

theorem :: INT_1:48
for i being Integer holds i div 0 = 0
proof
let i be Integer; ::_thesis: i div 0 = 0
A1: i / 0 = i * (0 ") by XCMPLX_0:def_9
.= i * 0 ;
 0 - 1 < 0 ;
hence  i div 0 = 0 by A1, Def6; ::_thesis: verum
end;

theorem :: INT_1:49
for i being Integer st i <> 0 holds
i div i = 1 by Th47;

theorem :: INT_1:50
for i being Integer holds i mod i = 0
proof
let i be Integer; ::_thesis: i mod i = 0
percases ( i = 0 or i <> 0 ) ;
suppose i = 0 ; ::_thesis: i mod i = 0
hence  i mod i = 0 by Def10; ::_thesis: verum
end;
supposeA1: i <> 0 ; ::_thesis: i mod i = 0
hence i mod i = i - ((i div i) * i) by Def10
.= i - (1 * i) by A1, Th47
.= 0 ;
::_thesis: verum
end;
end;
end;

begin

theorem :: INT_1:51
for k, i being Integer st k < i holds
ex j being Element of NAT st
( j = i - k & 1 <= j )
proof
let k, i be Integer; ::_thesis: ( k < i implies ex j being Element of NAT st
( j = i - k & 1 <= j ) )
assume  k < i ; ::_thesis: ex j being Element of NAT st
( j = i - k & 1 <= j )
then A1: k - k < i - k by XREAL_1:9;
then reconsider j = i - k as Element of NAT by Th3;
reconsider j9 = j, 09 = 0 as Integer ;
take  j ; ::_thesis: ( j = i - k & 1 <= j )
thus  j = i - k ; ::_thesis: 1 <= j
 09 + 1 <= j9 by A1, Th7;
hence  1 <= j ; ::_thesis: verum
end;

theorem Th52: :: INT_1:52
for a, b being Integer st a < b holds
a <= b - 1
proof
let a, b be Integer; ::_thesis: ( a < b implies a <= b - 1 )
assume  a < b ; ::_thesis: a <= b - 1
then  a - 1 < b - 1 by XREAL_1:9;
then  (a - 1) + 1 <= b - 1 by Th7;
hence  a <= b - 1 ; ::_thesis: verum
end;

theorem :: INT_1:53
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 ; ::_thesis: ( r >= 0 implies ( [/r\] >= 0 & [\r/] >= 0 & [/r\] is Element of NAT & [\r/] is Element of NAT ) )
assume A1: r >= 0 ; ::_thesis: ( [/r\] >= 0 & [\r/] >= 0 & [/r\] is Element of NAT & [\r/] is Element of NAT )
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  ( [/r\] >= 0 & [\r/] >= 0 & [/r\] is Element of NAT & [\r/] is Element of NAT ) by A1, A2, Th3; ::_thesis: verum
end;

theorem Th54: :: INT_1:54
for i being Integer
for r being real number st i <= r holds
i <= [\r/]
proof
let i be Integer; ::_thesis: for r being real number st i <= r holds
i <= [\r/]
let r be real number ; ::_thesis: ( i <= r implies i <= [\r/] )
assume  i <= r ; ::_thesis: 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  i <= [\r/] ; ::_thesis: verum
end;

theorem :: INT_1:55
for m, n being Nat holds 0 <= m div n by Th54;

theorem :: INT_1:56
for i, j being Integer st 0 < i & 1 < j holds
i div j < i
proof
let i, j be Integer; ::_thesis: ( 0 < i & 1 < j implies i div j < i )
assume that
A1: 0 < i and
A2: 1 < j ; ::_thesis: i div j < i
assume A3: i <= i div j ; ::_thesis: contradiction
 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; ::_thesis: verum
end;

theorem :: INT_1:57
for i2, i1 being Integer st i2 >= 0 holds
i1 mod i2 >= 0
proof
let i2, i1 be Integer; ::_thesis: ( i2 >= 0 implies i1 mod i2 >= 0 )
assume A1: i2 >= 0 ; ::_thesis: i1 mod i2 >= 0
percases ( i2 > 0 or i2 = 0 ) by A1;
supposeA2: i2 > 0 ; ::_thesis: i1 mod 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  i1 mod i2 >= 0 by Def10; ::_thesis: verum
end;
suppose i2 = 0 ; ::_thesis: i1 mod i2 >= 0
hence  i1 mod i2 >= 0 by Def10; ::_thesis: verum
end;
end;
end;

theorem :: INT_1:58
for i2, i1 being Integer st i2 > 0 holds
i1 mod i2 < i2
proof
let i2, i1 be Integer; ::_thesis: ( i2 > 0 implies i1 mod i2 < i2 )
assume A1: i2 > 0 ; ::_thesis: i1 mod i2 < i2
 (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  i1 mod i2 < i2 by A1, Def10; ::_thesis: verum
end;

theorem :: INT_1:59
for i2, i1 being Integer st i2 <> 0 holds
i1 = ((i1 div i2) * i2) + (i1 mod i2)
proof
let i2, i1 be Integer; ::_thesis: ( i2 <> 0 implies i1 = ((i1 div i2) * i2) + (i1 mod i2) )
assume  i2 <> 0 ; ::_thesis: i1 = ((i1 div i2) * i2) + (i1 mod i2)
then ((i1 div i2) * i2) + (i1 mod i2) = ((i1 div i2) * i2) + (i1 - ((i1 div i2) * i2)) by Def10
.= i1 ;
hence  i1 = ((i1 div i2) * i2) + (i1 mod i2) ; ::_thesis: verum
end;

theorem :: INT_1:60
for m, j being Integer holds m * j, 0 are_congruent_mod m
proof
let m, j be Integer; ::_thesis: m * j, 0 are_congruent_mod m
take  j ; :: according to INT_1:def_5 ::_thesis: m * j = (m * j) - 0
thus  m * j = (m * j) - 0 ; ::_thesis: verum
end;

theorem :: INT_1:61
for i, j being Integer st i >= 0 & j >= 0 holds
i div j >= 0
proof
let i, j be Integer; ::_thesis: ( i >= 0 & j >= 0 implies i div j >= 0 )
assume that
A1: i >= 0 and
A2: j >= 0 ; ::_thesis: i div 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  i div j >= 0 by Th8; ::_thesis: verum
end;

theorem :: INT_1:62
for n being Nat st n > 0 holds
for a being Integer holds
( a mod n = 0 iff n divides a )
proof
let n be Nat; ::_thesis: ( n > 0 implies for a being Integer holds
( a mod n = 0 iff n divides a ) )
assume A1: n > 0 ; ::_thesis: for a being Integer holds
( a mod n = 0 iff n divides a )
let a be Integer; ::_thesis: ( a mod n = 0 iff n divides a )
A2: now__::_thesis:_(_n_divides_a_implies_a_mod_n_=_0_)
A3: a mod n = a - ((a div n) * n) by A1, Def10
.= a - ([\(a / n)/] * n) ;
assume  n divides a ; ::_thesis: a mod n = 0
then consider k being Integer such that
A4: n * k = a by Def3;
 - n <> 0 by A1;
then  (- n) + a < 0 + a by 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 ; ::_thesis: contradiction
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  contradiction by A4; ::_thesis: verum
end;
then  [\(a / n)/] = k by A5, Def6;
hence  a mod n = 0 by A4, A3; ::_thesis: verum
end;
now__::_thesis:_(_a_mod_n_=_0_implies_n_divides_a_)
assume  a mod n = 0 ; ::_thesis: n divides a
then  0 = a - ((a div n) * n) by A1, Def10;
hence  n divides a by Def3; ::_thesis: verum
end;
hence  ( a mod n = 0 iff n divides a ) by A2; ::_thesis: verum
end;


theorem :: INT_1:63
for r, s being real number st r / s is not Integer holds
- [\(r / s)/] = [\((- r) / s)/] + 1
proof
let r, s be real number ; ::_thesis: ( r / s is not Integer implies - [\(r / s)/] = [\((- r) / s)/] + 1 )
 (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 ; ::_thesis: - [\(r / s)/] = [\((- r) / s)/] + 1
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  - [\(r / s)/] = [\((- r) / s)/] + 1 ; ::_thesis: verum
end;

theorem :: INT_1:64
for r, s being real number st r / s is Integer holds
- [\(r / s)/] = [\((- r) / s)/]
proof
let r, s be real number ; ::_thesis: ( r / s is Integer implies - [\(r / s)/] = [\((- r) / s)/] )
assume  r / s is Integer ; ::_thesis: - [\(r / s)/] = [\((- r) / s)/]
then A1: [\(r / s)/] = r / s by Th25;
A2: - (r / s) = (- r) / s by XCMPLX_1:187;
then  ((- r) / s) - 1 < (- [\(r / s)/]) - 0 by A1, XREAL_1:15;
hence  - [\(r / s)/] = [\((- r) / s)/] by A1, A2, Def6; ::_thesis: verum
end;

theorem :: INT_1:65
for i being Integer
for r being real number st r <= i holds
[/r\] <= i
proof
let i be Integer; ::_thesis: for r being real number st r <= i holds
[/r\] <= i
let r be real number ; ::_thesis: ( r <= i implies [/r\] <= i )
assume  r <= i ; ::_thesis: [/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 Th52;
hence  [/r\] <= i ; ::_thesis: verum
end;

scheme :: INT_1:sch 7
FinInd{ F1() ->  Element of NAT , F2() ->  Element of NAT , P1[ Nat] } :
 for i being Element of NAT st F1() <= i & i <= F2() holds
P1[i]
provided
A1: P1[F1()] and
A2: for j being Element of NAT st F1() <= j & j < F2() & P1[j] holds
P1[j + 1]
proof
defpred S1[ Nat] means ( F1() <= $1 & $1 <= F2() & P1[$1] );
assume  ex i being Element of NAT st
( F1() <= i & i <= F2() & P1[i] ) ; ::_thesis: contradiction
then A3: ex i being Nat st S1[i] ;
consider k being Nat such that
A4: ( S1[k] & ( for k9 being Nat st S1[k9] holds
k <= k9 ) ) from NAT_1:sch_5(A3);
percases ( k = F1() or k <> F1() ) ;
suppose k = F1() ; ::_thesis: contradiction
hence  contradiction by A1, A4; ::_thesis: verum
end;
suppose k <> F1() ; ::_thesis: contradiction
then  F1() < k by A4, XXREAL_0:1;
then  F1() + 1 <= k by NAT_1:13;
then A5: (F1() + 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 < F2() by A4, XXREAL_0:2;
A9: (k - 1) + 1 = k + 0 ;
 not S1[k9] by A4, A7;
hence  contradiction by A2, A4, A5, A9, A8; ::_thesis: verum
end;
end;
end;

scheme :: INT_1:sch 8
FinInd2{ F1() ->  Element of NAT , F2() ->  Element of NAT , P1[ Nat] } :
 for i being Element of NAT st F1() <= i & i <= F2() holds
P1[i]
provided
A1: P1[F1()] and
A2: for j being Element of NAT st F1() <= j & j < F2() & ( for j9 being Element of NAT st F1() <= j9 & j9 <= j holds
P1[j9] ) holds
P1[j + 1]
proof
defpred S1[ Element of NAT ] means  for j being Element of NAT st F1() <= j & j <= $1 holds
P1[j];
A3: for j being Element of NAT st F1() <= j & j < F2() & S1[j] holds
S1[j + 1]
proof
let j be Element of NAT ; ::_thesis: ( F1() <= j & j < F2() & S1[j] implies S1[j + 1] )
assume that
A4: F1() <= j and
A5: j < F2() ; ::_thesis: ( not S1[j] or S1[j + 1] )
assume A6: S1[j] ; ::_thesis: S1[j + 1]
thus  S1[j + 1] ::_thesis: verum
proof
let i be Element of NAT ; ::_thesis: ( F1() <= i & i <= j + 1 implies P1[i] )
assume that
A7: F1() <= i and
A8: i <= j + 1 ; ::_thesis: P1[i]
percases ( i = j + 1 or i <> j + 1 ) ;
suppose i = j + 1 ; ::_thesis: P1[i]
hence  P1[i] by A2, A4, A5, A6; ::_thesis: verum
end;
suppose i <> j + 1 ; ::_thesis: P1[i]
then  i < j + 1 by A8, XXREAL_0:1;
then  i <= j by NAT_1:13;
hence  P1[i] by A6, A7; ::_thesis: verum
end;
end;
end;
end;
A9: S1[F1()] by A1, XXREAL_0:1;
 for i being Element of NAT st F1() <= i & i <= F2() holds
S1[i] from INT_1:sch_7(A9, A3);
hence  for i being Element of NAT st F1() <= i & i <= F2() holds
P1[i] ; ::_thesis: verum
end;


theorem :: INT_1:66
for i being Integer
for r being real number holds frac (r + i) = frac r
proof
let i be Integer; ::_thesis: for r being real number holds frac (r + i) = frac r
let r be real number ; ::_thesis: frac (r + i) = frac r
thus  frac (r + i) = (r + i) - [\(r + i)/]
.= (r + i) - ([\r/] + i) by Th28
.= ((r - [\r/]) + i) - i
.= frac r ; ::_thesis: verum
end;

theorem Th67: :: INT_1:67
for r, a being real number st r <= a & a < [\r/] + 1 holds
[\a/] = [\r/]
proof
let r, a be real number ; ::_thesis: ( r <= a & a < [\r/] + 1 implies [\a/] = [\r/] )
assume A1: r <= a ; ::_thesis: ( not a < [\r/] + 1 or [\a/] = [\r/] )
assume  a < [\r/] + 1 ; ::_thesis: [\a/] = [\r/]
then A2: a - 1 < ([\r/] + 1) - 1 by XREAL_1:9;
 [\r/] <= r by Def6;
then  [\r/] <= a by A1, XXREAL_0:2;
hence  [\a/] = [\r/] by A2, Def6; ::_thesis: verum
end;

theorem Th68: :: INT_1:68
for r, a being real number st r <= a & a < [\r/] + 1 holds
frac r <= frac a
proof
let r, a be real number ; ::_thesis: ( r <= a & a < [\r/] + 1 implies frac r <= frac a )
assume A1: r <= a ; ::_thesis: ( not a < [\r/] + 1 or frac r <= frac a )
assume  a < [\r/] + 1 ; ::_thesis: frac r <= frac a
then  [\a/] = [\r/] by A1, Th67;
hence  frac r <= frac a by A1, XREAL_1:9; ::_thesis: verum
end;

theorem :: INT_1:69
for r, a being real number st r < a & a < [\r/] + 1 holds
frac r < frac a
proof
let r, a be real number ; ::_thesis: ( r < a & a < [\r/] + 1 implies frac r < frac a )
assume A1: r < a ; ::_thesis: ( not a < [\r/] + 1 or frac r < frac a )
assume  a < [\r/] + 1 ; ::_thesis: frac r < frac a
then  [\a/] = [\r/] by A1, Th67;
hence  frac r < frac a by A1, XREAL_1:9; ::_thesis: verum
end;

theorem Th70: :: INT_1:70
for a, r being real number st a >= [\r/] + 1 & a <= r + 1 holds
[\a/] = [\r/] + 1
proof
let a, r be real number ; ::_thesis: ( a >= [\r/] + 1 & a <= r + 1 implies [\a/] = [\r/] + 1 )
assume A1: a >= [\r/] + 1 ; ::_thesis: ( not a <= r + 1 or [\a/] = [\r/] + 1 )
assume  a <= r + 1 ; ::_thesis: [\a/] = [\r/] + 1
then  a - 1 <= (r + 1) - 1 by XREAL_1:9;
then  a - 1 < [\r/] + 1 by Th29, XXREAL_0:2;
hence  [\a/] = [\r/] + 1 by A1, Def6; ::_thesis: verum
end;

theorem Th71: :: INT_1:71
for a, r being real number st a >= [\r/] + 1 & a < r + 1 holds
frac a < frac r
proof
let a, r be real number ; ::_thesis: ( a >= [\r/] + 1 & a < r + 1 implies frac a < frac r )
assume A1: a >= [\r/] + 1 ; ::_thesis: ( not a < r + 1 or frac a < frac r )
assume A2: a < r + 1 ; ::_thesis: frac a < frac r
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, Th70;
hence  frac a < frac r by A3; ::_thesis: verum
end;

theorem :: INT_1:72
for r, a, b being real number st r <= a & a < r + 1 & r <= b & b < r + 1 & frac a = frac b holds
a = b
proof
let r, a, b be real number ; ::_thesis: ( r <= a & a < r + 1 & r <= b & b < r + 1 & frac a = frac b implies a = b )
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 ; ::_thesis: a = b
A6: [\r/] <= r by Def6;
then A7: [\r/] <= a by A1, XXREAL_0:2;
A8: [\r/] <= b by A3, A6, XXREAL_0:2;
percases ( ( a < [\r/] + 1 & b >= [\r/] + 1 ) or ( a >= [\r/] + 1 & b < [\r/] + 1 ) or ( a < [\r/] + 1 & b < [\r/] + 1 ) or ( a >= [\r/] + 1 & b >= [\r/] + 1 ) ) ;
supposeA9: ( a < [\r/] + 1 & b >= [\r/] + 1 ) ; ::_thesis: a = b
then  frac a >= frac r by A1, Th68;
hence  a = b by A4, A5, A9, Th71; ::_thesis: verum
end;
supposeA10: ( a >= [\r/] + 1 & b < [\r/] + 1 ) ; ::_thesis: a = b
then  frac a < frac r by A2, Th71;
hence  a = b by A3, A5, A10, Th68; ::_thesis: verum
end;
supposeA11: ( a < [\r/] + 1 & b < [\r/] + 1 ) ; ::_thesis: a = b
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  a = b by A5, A12; ::_thesis: verum
end;
suppose ( a >= [\r/] + 1 & b >= [\r/] + 1 ) ; ::_thesis: a = b
then  ( [\a/] = [\r/] + 1 & [\b/] = [\r/] + 1 ) by A2, A4, Th70;
hence  a = b by A5; ::_thesis: verum
end;
end;
end;