:: INT_1 semantic presentation

Lemma1: for b₁ being set st b₁ in [:{0},NAT :] \ {[0,0]} holds
ex b₂ being Element of NAT st b₁ = - b₂

proof end;

Lemma2: for b₁ being set
for b₂ being Element of NAT st b₁ = - b₂ & b₂ <> b₁ holds
b₁ in [:{0},NAT :] \ {[0,0]}

proof end;

definition

redefine func INT -> set means :Def1: :: INT_1:def 1
for b₁ being set holds
( b₁ in a₁ iff ex b₂ being Element of NAT st
( b₁ = b₂ or b₁ = - b₂ ) );
compatibility

proof end;

end;

:: deftheorem Def1 defines INT INT_1:def 1 :

definition

let c₁ be number ;
attr a₁ is integer means :Def2: :: INT_1:def 2
a₁ in INT ;

end;

:: deftheorem Def2 defines integer INT_1:def 2 :

registration

cluster integer Element of REAL ;
existence

proof end;

cluster integer set ;
existence

proof end;

cluster -> integer Element of INT ;
coherence by Def2;

end;

definition

mode Integer is integer number ;

end;

theorem Th1: :: INT_1:1

canceled;

theorem Th2: :: INT_1:2

canceled;

theorem Th3: :: INT_1:3

canceled;

theorem Th4: :: INT_1:4

canceled;

theorem Th5: :: INT_1:5

canceled;

theorem Th6: :: INT_1:6

canceled;

theorem Th7: :: INT_1:7

for b₁ being real number
for b₂ being natural number st ( b₁ = b₂ or b₁ = - b₂ ) holds
b₁ is Integer

proof end;

theorem Th8: :: INT_1:8

for b₁ being real number st b₁ is Integer holds
ex b₂ being Element of NAT st
( b₁ = b₂ or b₁ = - b₂ )

proof end;

registration

cluster -> integer Element of NAT ;
coherence by Th7;
cluster natural -> integer set ;
coherence

proof end;

end;

Lemma7: for b₁ being set st b₁ in INT holds
b₁ in REAL
by NUMBERS:15;

registration

cluster integer -> real set ;
coherence

proof end;

end;

registration

let c₁, c₂ be Integer;
cluster a₁ + a₂ -> integer ;
coherence

proof end;

cluster a₁ * a₂ -> integer ;
coherence

proof end;

end;

registration

let c₁ be Integer;
cluster - a₁ -> integer ;
coherence

proof end;

end;

registration

let c₁, c₂ be Integer;
cluster a₁ - a₂ -> integer ;
coherence

proof end;

end;

registration

let c₁ be Element of NAT ;
cluster - a₁ -> integer ;
coherence ;
let c₂ be Integer;
cluster a₂ + a₁ -> integer ;
coherence ;
cluster a₂ * a₁ -> integer ;
coherence ;
cluster a₂ - a₁ -> integer ;
coherence ;

end;

registration

let c₁, c₂ be Element of NAT ;
cluster a₁ - a₂ -> integer ;
coherence ;

end;

theorem Th9: :: INT_1:9

canceled;

theorem Th10: :: INT_1:10

canceled;

theorem Th11: :: INT_1:11

canceled;

theorem Th12: :: INT_1:12

canceled;

theorem Th13: :: INT_1:13

canceled;

theorem Th14: :: INT_1:14

canceled;

theorem Th15: :: INT_1:15

canceled;

theorem Th16: :: INT_1:16

for b₁ being Integer st 0 <= b₁ holds
b₁ in NAT

proof end;

theorem Th17: :: INT_1:17

for b₁ being real number st b₁ is Integer holds
( b₁ + 1 is Integer & b₁ - 1 is Integer )

proof end;

theorem Th18: :: INT_1:18

for b₁, b₂ being Integer st b₁ <= b₂ holds
b₂ - b₁ in NAT

proof end;

theorem Th19: :: INT_1:19

for b₁ being Element of NAT
for b₂, b₃ being Integer st b₂ + b₁ = b₃ holds
b₂ <= b₃

proof end;

Lemma11: for b₁ being Element of NAT st b₁ < 1 holds
b₁ = 0

proof end;

Lemma12: for b₁ being Integer st 0 < b₁ holds
1 <= b₁

proof end;

theorem Th20: :: INT_1:20

for b₁, b₂ being Integer st b₁ < b₂ holds
b₁ + 1 <= b₂

proof end;

theorem Th21: :: INT_1:21

for b₁ being Integer st b₁ < 0 holds
b₁ <= - 1

proof end;

theorem Th22: :: INT_1:22

for b₁, b₂ being Integer holds
( b₁ * b₂ = 1 iff ( ( b₁ = 1 & b₂ = 1 ) or ( b₁ = - 1 & b₂ = - 1 ) ) )

proof end;

theorem Th23: :: INT_1:23

for b₁, b₂ being Integer holds
( b₁ * b₂ = - 1 iff ( ( b₁ = - 1 & b₂ = 1 ) or ( b₁ = 1 & b₂ = - 1 ) ) )

proof end;

Lemma16: for b₁, b₂ being Integer st b₁ <= b₂ holds
ex b₃ being Element of NAT st b₁ + b₃ = b₂

proof end;

Lemma17: for b₁, b₂ being Integer st b₁ <= b₂ holds
ex b₃ being Element of NAT st b₂ - b₃ = b₁

proof end;

Lemma18: for b₁ being real number holds b₁ - 1 < b₁
by XREAL_1:148;

scheme :: INT_1:sch 1
s1{ P₁[ Integer] } :

ex b₁ being Subset of INT st
for b₂ being Integer holds
( b₂ in b₁ iff P₁[b₂] )

proof end;

scheme :: INT_1:sch 2
s2{ F₁() -> Integer, P₁[ Integer] } :

for b₁ being Integer st F₁() <= b₁ holds
P₁[b₁]

provided

E19: P₁[F₁()] and
E20: for b₁ being Integer st F₁() <= b₁ & P₁[b₁] holds
P₁[b₁ + 1]

proof end;

scheme :: INT_1:sch 3
s3{ F₁() -> Integer, P₁[ Integer] } :

for b₁ being Integer st b₁ <= F₁() holds
P₁[b₁]

provided

E19: P₁[F₁()] and
E20: for b₁ being Integer st b₁ <= F₁() & P₁[b₁] holds
P₁[b₁ - 1]

proof end;

scheme :: INT_1:sch 4
s4{ F₁() -> Integer, P₁[ Integer] } :

for b₁ being Integer holds P₁[b₁]

provided

E19: P₁[F₁()] and
E20: for b₁ being Integer st P₁[b₁] holds
( P₁[b₁ - 1] & P₁[b₁ + 1] )

proof end;

scheme :: INT_1:sch 5
s5{ F₁() -> Integer, P₁[ Integer] } :

ex b₁ being Integer st
( P₁[b₁] & ( for b₂ being Integer st P₁[b₂] holds
b₁ <= b₂ ) )

provided

E19: for b₁ being Integer st P₁[b₁] holds
F₁() <= b₁ and
E20: ex b₁ being Integer st P₁[b₁]

proof end;

scheme :: INT_1:sch 6
s6{ F₁() -> Integer, P₁[ Integer] } :

ex b₁ being Integer st
( P₁[b₁] & ( for b₂ being Integer st P₁[b₂] holds
b₂ <= b₁ ) )

provided

E19: for b₁ being Integer st P₁[b₁] holds
b₁ <= F₁() and
E20: ex b₁ being Integer st P₁[b₁]

proof end;

definition

let c₁, c₂, c₃ be Integer;
pred c₁,c₂ are_congruent_mod c₃ means :Def3: :: INT_1:def 3
ex b₁ being Integer st a₃ * b₁ = a₁ - a₂;

end;

:: deftheorem Def3 defines are_congruent_mod INT_1:def 3 :

theorem Th24: :: INT_1:24

canceled;

theorem Th25: :: INT_1:25

canceled;

theorem Th26: :: INT_1:26

canceled;

theorem Th27: :: INT_1:27

canceled;

theorem Th28: :: INT_1:28

canceled;

theorem Th29: :: INT_1:29

canceled;

theorem Th30: :: INT_1:30

canceled;

theorem Th31: :: INT_1:31

canceled;

theorem Th32: :: INT_1:32

for b₁, b₂ being Integer holds b₁,b₁ are_congruent_mod b₂

proof end;

theorem Th33: :: INT_1:33

for b₁ being Integer holds
( b₁,0 are_congruent_mod b₁ & 0,b₁ are_congruent_mod b₁ )

proof end;

theorem Th34: :: INT_1:34

for b₁, b₂ being Integer holds b₁,b₂ are_congruent_mod 1

proof end;

theorem Th35: :: INT_1:35

for b₁, b₂, b₃ being Integer st b₁,b₂ are_congruent_mod b₃ holds
b₂,b₁ are_congruent_mod b₃

proof end;

theorem Th36: :: INT_1:36

for b₁, b₂, b₃, b₄ being Integer st b₁,b₂ are_congruent_mod b₃ & b₂,b₄ are_congruent_mod b₃ holds
b₁,b₄ are_congruent_mod b₃

proof end;

theorem Th37: :: INT_1:37

for b₁, b₂, b₃, b₄, b₅ being Integer st b₁,b₂ are_congruent_mod b₃ & b₄,b₅ are_congruent_mod b₃ holds
b₁ + b₄,b₂ + b₅ are_congruent_mod b₃

proof end;

theorem Th38: :: INT_1:38

for b₁, b₂, b₃, b₄, b₅ being Integer st b₁,b₂ are_congruent_mod b₃ & b₄,b₅ are_congruent_mod b₃ holds
b₁ - b₄,b₂ - b₅ are_congruent_mod b₃

proof end;

theorem Th39: :: INT_1:39

for b₁, b₂, b₃, b₄, b₅ being Integer st b₁,b₂ are_congruent_mod b₃ & b₄,b₅ are_congruent_mod b₃ holds
b₁ * b₄,b₂ * b₅ are_congruent_mod b₃

proof end;

theorem Th40: :: INT_1:40

for b₁, b₂, b₃, b₄ being Integer holds
( b₁ + b₂,b₃ are_congruent_mod b₄ iff b₁,b₃ - b₂ are_congruent_mod b₄ )

proof end;

theorem Th41: :: INT_1:41

for b₁, b₂, b₃, b₄, b₅ being Integer st b₁ * b₂ = b₃ & b₄,b₅ are_congruent_mod b₃ holds
b₄,b₅ are_congruent_mod b₁

proof end;

theorem Th42: :: INT_1:42

for b₁, b₂, b₃ being Integer holds
( b₁,b₂ are_congruent_mod b₃ iff b₁ + b₃,b₂ are_congruent_mod b₃ )

proof end;

theorem Th43: :: INT_1:43

for b₁, b₂, b₃ being Integer holds
( b₁,b₂ are_congruent_mod b₃ iff b₁ - b₃,b₂ are_congruent_mod b₃ )

proof end;

theorem Th44: :: INT_1:44

for b₁ being real number
for b₂, b₃ being Integer st b₂ <= b₁ & b₁ - 1 < b₂ & b₃ <= b₁ & b₁ - 1 < b₃ holds
b₂ = b₃

proof end;

theorem Th45: :: INT_1:45

for b₁ being real number
for b₂, b₃ being Integer st b₁ <= b₂ & b₂ < b₁ + 1 & b₁ <= b₃ & b₃ < b₁ + 1 holds
b₂ = b₃

proof end;

Lemma22: for b₁ being real number ex b₂ being Element of NAT st b₁ < b₂

proof end;

definition

let c₁ be real number ;
func [\c₁/] -> Integer means :Def4: :: INT_1:def 4
( a₂ <= a₁ & a₁ - 1 < a₂ );
existence

proof end;

uniqueness by Th44;

end;

:: deftheorem Def4 defines [\ INT_1:def 4 :

theorem Th46: :: INT_1:46

canceled;

theorem Th47: :: INT_1:47

for b₁ being real number holds
( [\b₁/] = b₁ iff b₁ is integer )

proof end;

theorem Th48: :: INT_1:48

for b₁ being real number holds
( [\b₁/] < b₁ iff not b₁ is integer )

proof end;

theorem Th49: :: INT_1:49

canceled;

theorem Th50: :: INT_1:50

for b₁ being real number holds
( [\b₁/] - 1 < b₁ & [\b₁/] < b₁ + 1 )

proof end;

theorem Th51: :: INT_1:51

for b₁ being real number
for b₂ being Integer holds [\b₁/] + b₂ = [\(b₁ + b₂)/]

proof end;

theorem Th52: :: INT_1:52

for b₁ being real number holds b₁ < [\b₁/] + 1

proof end;

definition

let c₁ be real number ;
func [/c₁\] -> Integer means :Def5: :: INT_1:def 5
( a₁ <= a₂ & a₂ < a₁ + 1 );
existence

proof end;

uniqueness by Th45;

end;

:: deftheorem Def5 defines [/ INT_1:def 5 :

theorem Th53: :: INT_1:53

canceled;

theorem Th54: :: INT_1:54

for b₁ being real number holds
( [/b₁\] = b₁ iff b₁ is integer )

proof end;

theorem Th55: :: INT_1:55

for b₁ being real number holds
( b₁ < [/b₁\] iff not b₁ is integer )

proof end;

theorem Th56: :: INT_1:56

canceled;

theorem Th57: :: INT_1:57

for b₁ being real number holds
( b₁ - 1 < [/b₁\] & b₁ < [/b₁\] + 1 )

proof end;

theorem Th58: :: INT_1:58

for b₁ being real number
for b₂ being Integer holds [/b₁\] + b₂ = [/(b₁ + b₂)\]

proof end;

theorem Th59: :: INT_1:59

for b₁ being real number holds
( [\b₁/] = [/b₁\] iff b₁ is integer )

proof end;

theorem Th60: :: INT_1:60

for b₁ being real number holds
( [\b₁/] < [/b₁\] iff not b₁ is integer )

proof end;

theorem Th61: :: INT_1:61

for b₁ being real number holds [\b₁/] <= [/b₁\]

proof end;

theorem Th62: :: INT_1:62

for b₁ being real number holds [\[/b₁\]/] = [/b₁\] by Th47;

theorem Th63: :: INT_1:63

for b₁ being real number holds [\[\b₁/]/] = [\b₁/] by Th47;

theorem Th64: :: INT_1:64

for b₁ being real number holds [/[/b₁\]\] = [/b₁\] by Th54;

theorem Th65: :: INT_1:65

for b₁ being real number holds [/[\b₁/]\] = [\b₁/] by Th54;

theorem Th66: :: INT_1:66

for b₁ being real number holds
( [\b₁/] = [/b₁\] iff not [\b₁/] + 1 = [/b₁\] )

proof end;

definition

let c₁ be real number ;
func frac c₁ -> set equals :: INT_1:def 6
a₁ - [\a₁/];
coherence ;

end;

:: deftheorem Def6 defines frac INT_1:def 6 :

registration

let c₁ be real number ;
cluster frac a₁ -> real ;
coherence ;

end;

definition

let c₁ be real number ;
redefine func frac as frac c₁ -> Real;
coherence by XREAL_0:def 1;

end;

theorem Th67: :: INT_1:67

canceled;

theorem Th68: :: INT_1:68

for b₁ being real number holds b₁ = [\b₁/] + (frac b₁) ;

theorem Th69: :: INT_1:69

for b₁ being real number holds
( frac b₁ < 1 & 0 <= frac b₁ )

proof end;

theorem Th70: :: INT_1:70

for b₁ being real number holds [\(frac b₁)/] = 0

proof end;

theorem Th71: :: INT_1:71

for b₁ being real number holds
( frac b₁ = 0 iff b₁ is integer )

proof end;

theorem Th72: :: INT_1:72

for b₁ being real number holds
( 0 < frac b₁ iff not b₁ is integer )

proof end;

definition

let c₁, c₂ be Integer;
func c₁ div c₂ -> Integer equals :Def7: :: INT_1:def 7
[\(a₁ / a₂)/];
correctness ;

end;

:: deftheorem Def7 defines div INT_1:def 7 :

definition

let c₁, c₂ be Integer;
func c₁ mod c₂ -> Integer equals :Def8: :: INT_1:def 8
a₁ - ((a₁ div a₂) * a₂) if a₂ <> 0
otherwise 0;
correctness ;

end;

:: deftheorem Def8 defines mod INT_1:def 8 :

definition

let c₁, c₂ be Integer;
pred c₁ divides c₂ means :: INT_1:def 9
ex b₁ being Integer st a₂ = a₁ * b₁;
reflexivity

proof end;

end;

:: deftheorem Def9 defines divides INT_1:def 9 :

theorem Th73: :: INT_1:73

canceled;

theorem Th74: :: INT_1:74

for b₁ being real number st b₁ <> 0 holds
[\(b₁ / b₁)/] = 1

proof end;

theorem Th75: :: INT_1:75

for b₁ being Integer holds b₁ div 0 = 0

proof end;

theorem Th76: :: INT_1:76

for b₁ being Integer st b₁ <> 0 holds
b₁ div b₁ = 1 by Th74;

theorem Th77: :: INT_1:77

for b₁ being Integer holds b₁ mod b₁ = 0

proof end;

theorem Th78: :: INT_1:78

for b₁ being Element of NAT
for b₂ being Integer st b₁ < b₂ holds
ex b₃ being Element of NAT st
( b₃ = b₂ - b₁ & 1 <= b₃ )

proof end;

theorem Th79: :: INT_1:79

for b₁, b₂ being Integer st b₁ < b₂ holds
b₁ <= b₂ - 1

proof end;

theorem Th80: :: INT_1:80

for b₁ being real number st b₁ >= 0 holds
( [/b₁\] >= 0 & [\b₁/] >= 0 & [/b₁\] is Nat & [\b₁/] is Nat )

proof end;

theorem Th81: :: INT_1:81

for b₁ being Integer
for b₂ being real number st b₁ <= b₂ holds
b₁ <= [\b₂/]

proof end;

theorem Th82: :: INT_1:82

for b₁, b₂ being natural number holds 0 <= b₁ div b₂

proof end;