:: NAT_1 semantic presentation

definition

end;

theorem Th1: :: NAT_1:1

canceled;

theorem Th2: :: NAT_1:2

for b₁ being Subset of REAL st 0 in b₁ & ( for b₂ being Real st b₂ in b₁ holds
b₂ + 1 in b₁ ) holds
for b₂ being Nat holds b₂ in b₁

proof end;

definition

let c₁, c₂ be Nat;
redefine func + as c₁ + c₂ -> Nat;
coherence

proof end;

end;

registration

let c₁, c₂ be natural number ;
cluster a₁ + a₂ -> natural ;
coherence

proof end;

end;

scheme :: NAT_1:sch 1
s1{ P₁[ Nat] } :

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

provided

E2: P₁[0] and
E3: for b₁ being Nat st P₁[b₁] holds
P₁[b₁ + 1]

proof end;

scheme :: NAT_1:sch 2
s2{ P₁[ natural number ] } :

for b₁ being natural number holds P₁[b₁]

provided

E2: P₁[0] and
E3: for b₁ being natural number st P₁[b₁] holds
P₁[b₁ + 1]

proof end;

definition

let c₁, c₂ be Nat;
redefine func * as c₁ * c₂ -> Nat;
coherence

proof end;

end;

registration

let c₁, c₂ be natural number ;
cluster a₁ * a₂ -> natural ;
coherence

proof end;

end;

theorem Th3: :: NAT_1:3

canceled;

theorem Th4: :: NAT_1:4

canceled;

theorem Th5: :: NAT_1:5

canceled;

theorem Th6: :: NAT_1:6

canceled;

theorem Th7: :: NAT_1:7

canceled;

theorem Th8: :: NAT_1:8

canceled;

theorem Th9: :: NAT_1:9

canceled;

theorem Th10: :: NAT_1:10

canceled;

theorem Th11: :: NAT_1:11

canceled;

theorem Th12: :: NAT_1:12

canceled;

theorem Th13: :: NAT_1:13

canceled;

theorem Th14: :: NAT_1:14

canceled;

theorem Th15: :: NAT_1:15

canceled;

theorem Th16: :: NAT_1:16

canceled;

theorem Th17: :: NAT_1:17

canceled;

theorem Th18: :: NAT_1:18

for b₁ being natural number holds 0 <= b₁

proof end;

theorem Th19: :: NAT_1:19

for b₁ being natural number st 0 <> b₁ holds
0 < b₁ by Th18;

theorem Th20: :: NAT_1:20

for b₁, b₂, b₃ being natural number st b₁ <= b₂ holds
b₁ * b₃ <= b₂ * b₃

proof end;

theorem Th21: :: NAT_1:21

for b₁ being natural number holds 0 < b₁ + 1

proof end;

theorem Th22: :: NAT_1:22

for b₁ being natural number holds
( b₁ = 0 or ex b₂ being Nat st b₁ = b₂ + 1 )

proof end;

theorem Th23: :: NAT_1:23

for b₁, b₂ being natural number st b₁ + b₂ = 0 holds
( b₁ = 0 & b₂ = 0 )

proof end;

registration

cluster non zero natural set ;
existence

proof end;

end;

registration

let c₁ be natural number ;
let c₂ be non zero natural number ;
cluster a₁ + a₂ -> non zero natural ;
coherence by Th23;
cluster a₂ + a₁ -> non zero natural ;
coherence ;

end;

scheme :: NAT_1:sch 3
s3{ F₁() -> Nat, F₂( Nat, Nat) -> Nat, P₁[ Nat, Nat] } :

( ( for b₁ being Nat ex b₂ being Nat st P₁[b₁,b₂] ) & ( for b₁, b₂, b₃ being Nat st P₁[b₁,b₂] & P₁[b₁,b₃] holds
b₂ = b₃ ) )

provided

E6: for b₁, b₂ being Nat holds
( P₁[b₁,b₂] iff ( ( b₁ = 0 & b₂ = F₁() ) or ex b₃, b₄ being Nat st
( b₁ = b₃ + 1 & P₁[b₃,b₄] & b₂ = F₂(b₁,b₄) ) ) )

proof end;

theorem Th24: :: NAT_1:24

canceled;

theorem Th25: :: NAT_1:25

canceled;

theorem Th26: :: NAT_1:26

for b₁, b₂ being natural number holds
( not b₁ <= b₂ + 1 or b₁ <= b₂ or b₁ = b₂ + 1 )

proof end;

theorem Th27: :: NAT_1:27

for b₁, b₂ being natural number st b₁ <= b₂ & b₂ <= b₁ + 1 & not b₁ = b₂ holds
b₂ = b₁ + 1

proof end;

theorem Th28: :: NAT_1:28

for b₁, b₂ being natural number st b₁ <= b₂ holds
ex b₃ being Nat st b₂ = b₁ + b₃

proof end;

theorem Th29: :: NAT_1:29

for b₁, b₂ being natural number holds b₁ <= b₁ + b₂

proof end;

scheme :: NAT_1:sch 4
s4{ P₁[ Nat] } :

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

provided

E9: for b₁ being Nat st ( for b₂ being Nat st b₂ < b₁ holds
P₁[b₂] ) holds
P₁[b₁]

proof end;

scheme :: NAT_1:sch 5
s5{ P₁[ Nat] } :

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

provided

E9: ex b₁ being Nat st P₁[b₁]

proof end;

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

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

provided

E9: for b₁ being Nat st P₁[b₁] holds
b₁ <= F₁() and
E10: ex b₁ being Nat st P₁[b₁]

proof end;

theorem Th30: :: NAT_1:30

canceled;

theorem Th31: :: NAT_1:31

canceled;

theorem Th32: :: NAT_1:32

canceled;

theorem Th33: :: NAT_1:33

canceled;

theorem Th34: :: NAT_1:34

canceled;

theorem Th35: :: NAT_1:35

canceled;

theorem Th36: :: NAT_1:36

canceled;

theorem Th37: :: NAT_1:37

for b₁, b₂, b₃ being natural number st b₁ <= b₂ holds
b₁ <= b₂ + b₃

proof end;

theorem Th38: :: NAT_1:38

for b₁, b₂ being natural number holds
( b₁ < b₂ + 1 iff b₁ <= b₂ )

proof end;

theorem Th39: :: NAT_1:39

for b₁ being natural number st b₁ < 1 holds
b₁ = 0

proof end;

theorem Th40: :: NAT_1:40

for b₁, b₂ being natural number st b₁ * b₂ = 1 holds
( b₁ = 1 & b₂ = 1 )

proof end;

theorem Th41: :: NAT_1:41

for b₁, b₂ being natural number st b₁ <> 0 holds
b₂ < b₂ + b₁

proof end;

scheme :: NAT_1:sch 7
s7{ P₁[ Nat] } :

P₁[0]

provided

E14: ex b₁ being Nat st P₁[b₁] and
E15: for b₁ being Nat st b₁ <> 0 & P₁[b₁] holds
ex b₂ being Nat st
( b₂ < b₁ & P₁[b₂] )

proof end;

theorem Th42: :: NAT_1:42

for b₁ being Nat st 0 < b₁ holds
for b₂ being Nat ex b₃, b₄ being Nat st
( b₂ = (b₁ * b₃) + b₄ & b₄ < b₁ )

proof end;

theorem Th43: :: NAT_1:43

for b₁, b₂, b₃, b₄, b₅, b₆ being natural number st b₁ = (b₂ * b₃) + b₅ & b₅ < b₂ & b₁ = (b₂ * b₄) + b₆ & b₆ < b₂ holds
( b₃ = b₄ & b₅ = b₆ )

proof end;

definition

let c₁, c₂ be natural number ;
E16: ( c₁ is Nat & c₂ is Nat ) by ORDINAL2:def 21;
func c₁ div c₂ -> Nat means :Def1: :: NAT_1:def 1
( ex b₁ being Nat st
( a₁ = (a₂ * a₃) + b₁ & b₁ < a₂ ) or ( a₃ = 0 & a₂ = 0 ) );
existence

proof end;

uniqueness

proof end;

func c₁ mod c₂ -> Nat means :Def2: :: NAT_1:def 2
( ex b₁ being Nat st
( a₁ = (a₂ * b₁) + a₃ & a₃ < a₂ ) or ( a₃ = 0 & a₂ = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines div NAT_1:def 1 :

:: deftheorem Def2 defines mod NAT_1:def 2 :

theorem Th44: :: NAT_1:44

canceled;

theorem Th45: :: NAT_1:45

canceled;

theorem Th46: :: NAT_1:46

for b₁, b₂ being natural number st 0 < b₁ holds
b₂ mod b₁ < b₁

proof end;

theorem Th47: :: NAT_1:47

for b₁, b₂ being natural number st 0 < b₁ holds
b₂ = (b₁ * (b₂ div b₁)) + (b₂ mod b₁)

proof end;

definition

let c₁, c₂ be natural number ;
pred c₁ divides c₂ means :Def3: :: NAT_1:def 3
ex b₁ being Nat st a₂ = a₁ * b₁;
reflexivity

proof end;

end;

:: deftheorem Def3 defines divides NAT_1:def 3 :

theorem Th48: :: NAT_1:48

canceled;

theorem Th49: :: NAT_1:49

for b₁, b₂ being natural number holds
( b₁ divides b₂ iff b₂ = b₁ * (b₂ div b₁) )

proof end;

theorem Th50: :: NAT_1:50

canceled;

theorem Th51: :: NAT_1:51

for b₁, b₂, b₃ being natural number st b₁ divides b₂ & b₂ divides b₃ holds
b₁ divides b₃

proof end;

theorem Th52: :: NAT_1:52

for b₁, b₂ being natural number st b₁ divides b₂ & b₂ divides b₁ holds
b₁ = b₂

proof end;

theorem Th53: :: NAT_1:53

for b₁ being natural number holds
( b₁ divides 0 & 1 divides b₁ )

proof end;

theorem Th54: :: NAT_1:54

for b₁, b₂ being natural number st 0 < b₁ & b₂ divides b₁ holds
b₂ <= b₁

proof end;

theorem Th55: :: NAT_1:55

for b₁, b₂, b₃ being natural number st b₁ divides b₂ & b₁ divides b₃ holds
b₁ divides b₂ + b₃

proof end;

theorem Th56: :: NAT_1:56

for b₁, b₂, b₃ being natural number st b₁ divides b₂ holds
b₁ divides b₂ * b₃

proof end;

theorem Th57: :: NAT_1:57

for b₁, b₂, b₃ being natural number st b₁ divides b₂ & b₁ divides b₂ + b₃ holds
b₁ divides b₃

proof end;

theorem Th58: :: NAT_1:58

for b₁, b₂, b₃ being natural number st b₁ divides b₂ & b₁ divides b₃ holds
b₁ divides b₂ mod b₃

proof end;

definition

let c₁, c₂ be Nat;
func c₁ lcm c₂ -> Nat means :Def4: :: NAT_1:def 4
( a₁ divides a₃ & a₂ divides a₃ & ( for b₁ being Nat st a₁ divides b₁ & a₂ divides b₁ holds
a₃ divides b₁ ) );
existence

proof end;

uniqueness

proof end;

idempotence ;
commutativity ;

end;

:: deftheorem Def4 defines lcm NAT_1:def 4 :

definition

let c₁, c₂ be Nat;
func c₁ hcf c₂ -> Nat means :Def5: :: NAT_1:def 5
( a₃ divides a₁ & a₃ divides a₂ & ( for b₁ being Nat st b₁ divides a₁ & b₁ divides a₂ holds
b₁ divides a₃ ) );
existence

proof end;

uniqueness

proof end;

idempotence ;
commutativity ;

end;

:: deftheorem Def5 defines hcf NAT_1:def 5 :

scheme :: NAT_1:sch 8
s8{ F₁( Nat) -> Nat, F₂() -> Nat, F₃() -> Nat } :

ex b₁ being Nat st
( F₁(b₁) = F₂() hcf F₃() & F₁((b₁ + 1)) = 0 )

provided

E31: ( 0 < F₃() & F₃() < F₂() ) and
E32: ( F₁(0) = F₂() & F₁(1) = F₃() ) and
E33: for b₁ being Nat holds F₁((b₁ + 2)) = F₁(b₁) mod F₁((b₁ + 1))

proof end;

registration

cluster -> ordinal Element of NAT ;
coherence ;

end;

registration

cluster non empty ordinal Element of K40(REAL );
existence

proof end;

end;

theorem Th59: :: NAT_1:59

for b₁, b₂ being natural number holds
( b₁ < b₁ + b₂ iff 1 <= b₂ )

proof end;

theorem Th60: :: NAT_1:60

for b₁, b₂ being natural number st b₁ < b₂ holds
b₂ - 1 is Nat

proof end;

theorem Th61: :: NAT_1:61

for b₁, b₂ being natural number st b₁ <= b₂ holds
b₂ - b₁ is Nat

proof end;

theorem Th62: :: NAT_1:62

for b₁ being natural number holds
( b₁ mod 2 = 0 or b₁ mod 2 = 1 )

proof end;

theorem Th63: :: NAT_1:63

for b₁, b₂ being natural number holds (b₁ * b₂) mod b₁ = 0

proof end;

theorem Th64: :: NAT_1:64

for b₁, b₂ being natural number st b₁ > 1 holds
1 mod b₁ = 1

proof end;

theorem Th65: :: NAT_1:65

for b₁, b₂, b₃, b₄ being natural number st b₁ mod b₃ = 0 & b₂ = b₁ - (b₄ * b₃) holds
b₂ mod b₃ = 0

proof end;

theorem Th66: :: NAT_1:66

for b₁, b₂, b₃ being natural number st b₃ <> 0 & b₁ mod b₃ = 0 & b₂ < b₃ holds
(b₁ + b₂) mod b₃ = b₂

proof end;

theorem Th67: :: NAT_1:67

for b₁, b₂, b₃ being natural number st b₁ mod b₃ = 0 holds
(b₁ + b₂) mod b₃ = b₂ mod b₃

proof end;

theorem Th68: :: NAT_1:68

for b₁, b₂ being natural number st b₁ <> 0 holds
(b₁ * b₂) div b₁ = b₂

proof end;

theorem Th69: :: NAT_1:69

for b₁, b₂, b₃ being natural number st b₁ mod b₂ = 0 holds
(b₁ + b₃) div b₂ = (b₁ div b₂) + (b₃ div b₂)

proof end;

theorem Th70: :: NAT_1:70

for b₁, b₂ being Nat holds
( not b₁ < b₂ + 1 or b₁ < b₂ or b₁ = b₂ )

proof end;

theorem Th71: :: NAT_1:71

for b₁ being Nat holds
( not b₁ < 2 or b₁ = 0 or b₁ = 1 )

proof end;

registration

cluster non zero Element of NAT ;
existence

proof end;

end;

registration

cluster -> ordinal non negative Element of NAT ;
coherence by Th18;

end;

registration

cluster natural -> natural non negative set ;
coherence by Th18;

end;

theorem Th72: :: NAT_1:72

for b₁, b₂ being Nat st b₂ <> 0 holds
(b₁ * b₂) div b₂ = b₁

proof end;

theorem Th73: :: NAT_1:73

for b₁, b₂, b₃ being natural number holds b₁ mod b₂ = ((b₂ * b₃) + b₁) mod b₂

proof end;

theorem Th74: :: NAT_1:74

for b₁, b₂, b₃ being natural number holds (b₁ + b₂) mod b₃ = ((b₁ mod b₃) + b₂) mod b₃

proof end;

theorem Th75: :: NAT_1:75

for b₁, b₂, b₃ being natural number holds (b₁ + b₂) mod b₃ = (b₁ + (b₂ mod b₃)) mod b₃ by Th74;

theorem Th76: :: NAT_1:76

for b₁, b₂ being natural number st b₂ < b₁ holds
b₂ mod b₁ = b₂

proof end;

theorem Th77: :: NAT_1:77

for b₁ being natural number holds b₁ mod b₁ = 0

proof end;

theorem Th78: :: NAT_1:78

for b₁ being natural number holds 0 = 0 mod b₁

proof end;