:: INT_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for z being set st z in [:{0},NAT :] \ {[0,0]} holds
ex k being Element of NAT st z = - k
proof 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 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 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 ;
attr i 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 integer Element of REAL ;
existence
ex b1 being Real st b1 is integer
proof end;
cluster integer set ;
existence
ex b1 being number st b1 is integer
proof end;
cluster -> integer 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 :: INT_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th7: :: INT_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number
for k being natural number st ( r = k or r = - k ) holds
r is Integer
proof end;

theorem Th8: :: INT_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number st r is Integer holds
ex k being Element of NAT st
( r = k or r = - k )
proof end;

registration
cluster -> integer Element of NAT ;
coherence
for b1 being Element of NAT holds b1 is integer
by Th7;
cluster natural -> integer set ;
coherence
for b1 being number st b1 is natural holds
b1 is integer
proof end;
end;

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

registration
cluster integer -> real set ;
coherence
for b1 being number st b1 is integer holds
b1 is real
proof end;
end;

registration
let i1, i2 be Integer;
cluster i1 + i2 -> integer ;
coherence
i1 + i2 is integer
proof end;
cluster i1 * i2 -> integer ;
coherence
i1 * i2 is integer
proof end;
end;

registration
let i0 be Integer;
cluster - i0 -> integer ;
coherence
- i0 is integer
proof end;
end;

registration
let i1, i2 be Integer;
cluster i1 - i2 -> integer ;
coherence
i1 - i2 is integer
proof end;
end;

registration
let n be Element of NAT ;
cluster - n -> integer ;
coherence
- n is integer
;
let i1 be Integer;
cluster i1 + n -> integer ;
coherence
i1 + n is integer
;
cluster i1 * n -> integer ;
coherence
i1 * n is integer
;
cluster i1 - n -> integer ;
coherence
i1 - n is integer
;
end;

registration
let n1, n2 be Element of NAT ;
cluster n1 - n2 -> integer ;
coherence
n1 - n2 is integer
;
end;

theorem :: INT_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th16: :: INT_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i0 being Integer st 0 <= i0 holds
i0 in NAT
proof end;

theorem :: INT_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number st r is Integer holds
( r + 1 is Integer & r - 1 is Integer )
proof end;

theorem Th18: :: INT_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i2, i1 being Integer st i2 <= i1 holds
i1 - i2 in NAT
proof end;

theorem Th19: :: INT_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Element of NAT
for i1, i2 being Integer st i1 + k = i2 holds
i1 <= i2
proof end;

Lm4: for j being Element of NAT st j < 1 holds
j = 0
proof end;

Lm5: for i1 being Integer st 0 < i1 holds
1 <= i1
proof end;

theorem Th20: :: INT_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i0, i1 being Integer st i0 < i1 holds
i0 + 1 <= i1
proof end;

theorem Th21: :: INT_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1 being Integer st i1 < 0 holds
i1 <= - 1
proof end;

theorem Th22: :: INT_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, i2 being Integer holds
( i1 * i2 = 1 iff ( ( i1 = 1 & i2 = 1 ) or ( i1 = - 1 & i2 = - 1 ) ) )
proof end;

theorem :: INT_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, i2 being Integer holds
( i1 * i2 = - 1 iff ( ( i1 = - 1 & i2 = 1 ) or ( i1 = 1 & i2 = - 1 ) ) )
proof end;

Lm6: for i0, i1 being Integer st i0 <= i1 holds
ex k being Element of NAT st i0 + k = i1
proof end;

Lm7: for i0, i1 being Integer st i0 <= i1 holds
ex k being Element of NAT st i1 - k = i0
proof end;

Lm8: for r being real number holds r - 1 < r
by XREAL_1:148;

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 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 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 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 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 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 end;

definition
let i1, i2, i3 be Integer;
pred i1,i2 are_congruent_mod i3 means :Def3: :: INT_1:def 3
ex i4 being Integer st i3 * i4 = i1 - i2;
end;

:: deftheorem Def3 defines are_congruent_mod INT_1:def 3 :
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:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, i2 being Integer holds i1,i1 are_congruent_mod i2
proof end;

theorem :: INT_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1 being Integer holds
( i1,0 are_congruent_mod i1 & 0,i1 are_congruent_mod i1 )
proof end;

theorem :: INT_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, i2 being Integer holds i1,i2 are_congruent_mod 1
proof end;

theorem :: INT_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, i2, i3 being Integer st i1,i2 are_congruent_mod i3 holds
i2,i1 are_congruent_mod i3
proof end;

theorem :: INT_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: INT_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: INT_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: INT_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: INT_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, i2, i3, i5 being Integer holds
( i1 + i2,i3 are_congruent_mod i5 iff i1,i3 - i2 are_congruent_mod i5 )
proof end;

theorem :: INT_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: INT_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, i2, i5 being Integer holds
( i1,i2 are_congruent_mod i5 iff i1 + i5,i2 are_congruent_mod i5 )
proof end;

theorem :: INT_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, i2, i5 being Integer holds
( i1,i2 are_congruent_mod i5 iff i1 - i5,i2 are_congruent_mod i5 )
proof end;

theorem Th44: :: INT_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th45: :: INT_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

Lm9: for r being real number ex n being Element of NAT st r < n
proof end;

definition
let r be real number ;
func [\r/] -> Integer means :Def4: :: INT_1:def 4
( it <= r & r - 1 < it );
existence
ex b1 being Integer st
( b1 <= r & r - 1 < b1 )
proof end;
uniqueness
for b1, b2 being Integer st b1 <= r & r - 1 < b1 & b2 <= r & r - 1 < b2 holds
b1 = b2
by Th44;
end;

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

theorem :: INT_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th47: :: INT_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds
( [\r/] = r iff r is integer )
proof end;

theorem Th48: :: INT_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds
( [\r/] < r iff not r is integer )
proof end;

theorem :: INT_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds
( [\r/] - 1 < r & [\r/] < r + 1 )
proof end;

theorem Th51: :: INT_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number
for i0 being Integer holds [\r/] + i0 = [\(r + i0)/]
proof end;

theorem Th52: :: INT_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds r < [\r/] + 1
proof end;

definition
let r be real number ;
func [/r\] -> Integer means :Def5: :: INT_1:def 5
( r <= it & it < r + 1 );
existence
ex b1 being Integer st
( r <= b1 & b1 < r + 1 )
proof end;
uniqueness
for b1, b2 being Integer st r <= b1 & b1 < r + 1 & r <= b2 & b2 < r + 1 holds
b1 = b2
by Th45;
end;

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

theorem :: INT_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th54: :: INT_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds
( [/r\] = r iff r is integer )
proof end;

theorem Th55: :: INT_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds
( r < [/r\] iff not r is integer )
proof end;

theorem :: INT_1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds
( r - 1 < [/r\] & r < [/r\] + 1 )
proof end;

theorem :: INT_1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number
for i0 being Integer holds [/r\] + i0 = [/(r + i0)\]
proof end;

theorem Th59: :: INT_1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds
( [\r/] = [/r\] iff r is integer )
proof end;

theorem Th60: :: INT_1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds
( [\r/] < [/r\] iff not r is integer )
proof end;

theorem :: INT_1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds [\r/] <= [/r\]
proof end;

theorem :: INT_1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds [\[/r\]/] = [/r\] by Th47;

theorem :: INT_1:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds [\[\r/]/] = [\r/] by Th47;

theorem :: INT_1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds [/[/r\]\] = [/r\] by Th54;

theorem :: INT_1:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds [/[\r/]\] = [\r/] by Th54;

theorem :: INT_1:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds
( [\r/] = [/r\] iff not [\r/] + 1 = [/r\] )
proof end;

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

:: deftheorem defines frac INT_1:def 6 :
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:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: INT_1:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds r = [\r/] + (frac r) ;

theorem Th69: :: INT_1:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds
( frac r < 1 & 0 <= frac r )
proof end;

theorem :: INT_1:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds [\(frac r)/] = 0
proof end;

theorem Th71: :: INT_1:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds
( frac r = 0 iff r is integer )
proof end;

theorem :: INT_1:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds
( 0 < frac r iff not r is integer )
proof end;

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

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

definition
let i1, i2 be Integer;
func i1 mod i2 -> Integer equals :Def8: :: INT_1:def 8
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 Def8 defines mod INT_1:def 8 :
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 ) );

definition
let i1, i2 be Integer;
pred i1 divides i2 means :: INT_1:def 9
ex i3 being Integer st i2 = i1 * i3;
reflexivity
for i1 being Integer ex i3 being Integer st i1 = i1 * i3
proof end;
end;

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

theorem :: INT_1:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th74: :: INT_1:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number st r <> 0 holds
[\(r / r)/] = 1
proof end;

theorem :: INT_1:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Integer holds i div 0 = 0
proof end;

theorem Th76: :: INT_1:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Integer st i <> 0 holds
i div i = 1 by Th74;

theorem :: INT_1:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Integer holds i mod i = 0
proof end;

theorem :: INT_1:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Element of NAT
for i being Integer st k < i holds
ex j being Element of NAT st
( j = i - k & 1 <= j )
proof end;

theorem :: INT_1:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Integer st a < b holds
a <= b - 1
proof end;

theorem :: INT_1:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number st r >= 0 holds
( [/r\] >= 0 & [\r/] >= 0 & [/r\] is Nat & [\r/] is Nat )
proof end;

theorem Th2: :: INT_1:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Integer
for r being real number st i <= r holds
i <= [\r/]
proof end;

theorem :: INT_1:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n being natural number holds 0 <= m div n
proof end;