:: NAT_1 semantic presentation

definition

mode Nat is Element of NAT ;

end;

theorem :: NAT_1:1

canceled;

theorem Th2: :: NAT_1:2

for X being Subset of REAL st 0 in X & ( for x being Real st x in X holds
x + 1 in X ) holds
for k being Nat holds k in X

proof end;

definition

let n, k be Nat;
:: original: +
redefine func n + k -> Nat;
coherence

proof end;

end;

registration

let n, k be natural number ;
cluster n + k -> natural ;
coherence

proof end;

end;

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

for k being Nat holds P₁[k]

provided

A1: P₁[0] and
A2: for k being Nat st P₁[k] holds
P₁[k + 1]

proof end;

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

for k being natural number holds P₁[k]

provided

A1: P₁[0] and
A2: for k being natural number st P₁[k] holds
P₁[k + 1]

proof end;

definition

let n, k be Nat;
:: original: *
redefine func n * k -> Nat;
coherence

proof end;

end;

registration

let n, k be natural number ;
cluster n * k -> natural ;
coherence

proof end;

end;

theorem :: NAT_1:3

canceled;

theorem :: NAT_1:4

canceled;

theorem :: NAT_1:5

canceled;

theorem :: NAT_1:6

canceled;

theorem :: NAT_1:7

canceled;

theorem :: NAT_1:8

canceled;

theorem :: NAT_1:9

canceled;

theorem :: NAT_1:10

canceled;

theorem :: NAT_1:11

canceled;

theorem :: NAT_1:12

canceled;

theorem :: NAT_1:13

canceled;

theorem :: NAT_1:14

canceled;

theorem :: NAT_1:15

canceled;

theorem :: NAT_1:16

canceled;

theorem :: NAT_1:17

canceled;

theorem Th18: :: NAT_1:18

for i being natural number holds 0 <= i

proof end;

theorem :: NAT_1:19

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

theorem Th20: :: NAT_1:20

for i, j, h being natural number st i <= j holds
i * h <= j * h

proof end;

theorem :: NAT_1:21

for i being natural number holds 0 < i + 1

proof end;

theorem Th22: :: NAT_1:22

for i being natural number holds
( i = 0 or ex k being Nat st i = k + 1 )

proof end;

theorem Th23: :: NAT_1:23

for i, j being natural number st i + j = 0 holds
( i = 0 & j = 0 )

proof end;

registration

cluster non zero natural set ;
existence

proof end;

end;

registration

let m be natural number ;
let n be non zero natural number ;
cluster m + n -> non zero natural ;
coherence by Th23;
cluster n + m -> non zero natural ;
coherence ;

end;

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

( ( for k being Nat ex n being Nat st P₁[k,n] ) & ( for k, n, m being Nat st P₁[k,n] & P₁[k,m] holds
n = m ) )

provided

A1: for k, n being Nat holds
( P₁[k,n] iff ( ( k = 0 & n = F₁() ) or ex m, l being Nat st
( k = m + 1 & P₁[m,l] & n = F₂(k,l) ) ) )

proof end;

theorem :: NAT_1:24

canceled;

theorem :: NAT_1:25

canceled;

theorem Th26: :: NAT_1:26

for i, j being natural number holds
( not i <= j + 1 or i <= j or i = j + 1 )

proof end;

theorem :: NAT_1:27

for i, j being natural number st i <= j & j <= i + 1 & not i = j holds
j = i + 1

proof end;

theorem Th28: :: NAT_1:28

for i, j being natural number st i <= j holds
ex k being Nat st j = i + k

proof end;

theorem Th29: :: NAT_1:29

for i, j being natural number holds i <= i + j

proof end;

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

for k being Nat holds P₁[k]

provided

A1: for k being Nat st ( for n being Nat st n < k holds
P₁[n] ) holds
P₁[k]

proof end;

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

ex k being Nat st
( P₁[k] & ( for n being Nat st P₁[n] holds
k <= n ) )

provided

A1: ex k being Nat st P₁[k]

proof end;

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

ex k being Nat st
( P₁[k] & ( for n being Nat st P₁[n] holds
n <= k ) )

provided

A1: for k being Nat st P₁[k] holds
k <= F₁() and
A2: ex k being Nat st P₁[k]

proof end;

theorem :: NAT_1:30

canceled;

theorem :: NAT_1:31

canceled;

theorem :: NAT_1:32

canceled;

theorem :: NAT_1:33

canceled;

theorem :: NAT_1:34

canceled;

theorem :: NAT_1:35

canceled;

theorem :: NAT_1:36

canceled;

theorem Th37: :: NAT_1:37

for i, j, h being natural number st i <= j holds
i <= j + h

proof end;

theorem Th38: :: NAT_1:38

for i, j being natural number holds
( i < j + 1 iff i <= j )

proof end;

theorem Th39: :: NAT_1:39

for j being natural number st j < 1 holds
j = 0

proof end;

theorem Th40: :: NAT_1:40

for i, j being natural number st i * j = 1 holds
( i = 1 & j = 1 )

proof end;

theorem Th41: :: NAT_1:41

for k, n being natural number st k <> 0 holds
n < n + k

proof end;

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

P₁[0]

provided

A1: ex k being Nat st P₁[k] and
A2: for k being Nat st k <> 0 & P₁[k] holds
ex n being Nat st
( n < k & P₁[n] )

proof end;

theorem Th42: :: NAT_1:42

for m being Nat st 0 < m holds
for n being Nat ex k, t being Nat st
( n = (m * k) + t & t < m )

proof end;

theorem Th43: :: NAT_1:43

for n, m, k, k1, t, t1 being natural number st n = (m * k) + t & t < m & n = (m * k1) + t1 & t1 < m holds
( k = k1 & t = t1 )

proof end;

definition

let k, l be natural number ;
A1: ( k is Nat & l is Nat ) by ORDINAL2:def 21;
func k div l -> Nat means :Def1: :: NAT_1:def 1
( ex t being Nat st
( k = (l * it) + t & t < l ) or ( it = 0 & l = 0 ) );
existence

proof end;

uniqueness

proof end;

func k mod l -> Nat means :Def2: :: NAT_1:def 2
( ex t being Nat st
( k = (l * t) + it & it < l ) or ( it = 0 & l = 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 :: NAT_1:44

canceled;

theorem :: NAT_1:45

canceled;

theorem Th46: :: NAT_1:46

for i, j being natural number st 0 < i holds
j mod i < i

proof end;

theorem Th47: :: NAT_1:47

for i, j being natural number st 0 < i holds
j = (i * (j div i)) + (j mod i)

proof end;

definition

let k, l be natural number ;
pred k divides l means :Def3: :: NAT_1:def 3
ex t being Nat st l = k * t;
reflexivity

proof end;

end;

:: deftheorem Def3 defines divides NAT_1:def 3 :

theorem :: NAT_1:48

canceled;

theorem Th49: :: NAT_1:49

for j, i being natural number holds
( j divides i iff i = j * (i div j) )

proof end;

theorem :: NAT_1:50

canceled;

theorem :: NAT_1:51

for i, j, h being natural number st i divides j & j divides h holds
i divides h

proof end;

theorem Th52: :: NAT_1:52

for i, j being natural number st i divides j & j divides i holds
i = j

proof end;

theorem Th53: :: NAT_1:53

for i being natural number holds
( i divides 0 & 1 divides i )

proof end;

theorem Th54: :: NAT_1:54

for j, i being natural number st 0 < j & i divides j holds
i <= j

proof end;

theorem Th55: :: NAT_1:55

for i, j, h being natural number st i divides j & i divides h holds
i divides j + h

proof end;

theorem Th56: :: NAT_1:56

for i, j, h being natural number st i divides j holds
i divides j * h

proof end;

theorem Th57: :: NAT_1:57

for i, j, h being natural number st i divides j & i divides j + h holds
i divides h

proof end;

theorem Th58: :: NAT_1:58

for i, j, h being natural number st i divides j & i divides h holds
i divides j mod h

proof end;

definition

let k, n be Nat;
func k lcm n -> Nat means :Def4: :: NAT_1:def 4
( k divides it & n divides it & ( for m being Nat st k divides m & n divides m holds
it divides m ) );
existence

proof end;

uniqueness

proof end;

idempotence ;
commutativity ;

end;

:: deftheorem Def4 defines lcm NAT_1:def 4 :

definition

let k, n be Nat;
func k hcf n -> Nat means :Def5: :: NAT_1:def 5
( it divides k & it divides n & ( for m being Nat st m divides k & m divides n holds
m divides it ) );
existence

proof end;

uniqueness

proof end;

idempotence ;
commutativity ;

end;

:: deftheorem Def5 defines hcf NAT_1:def 5 :

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

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

provided

A1: ( 0 < F₃() & F₃() < F₂() ) and
A2: ( F₁(0) = F₂() & F₁(1) = F₃() ) and
A3: for n being Nat holds F₁((n + 2)) = F₁(n) mod F₁((n + 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 :: NAT_1:59

for k, n being natural number holds
( k < k + n iff 1 <= n )

proof end;

theorem :: NAT_1:60

for k, n being natural number st k < n holds
n - 1 is Nat

proof end;

theorem Th61: :: NAT_1:61

for k, n being natural number st k <= n holds
n - k is Nat

proof end;

theorem :: NAT_1:62

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

proof end;

theorem :: NAT_1:63

for k, n being natural number holds (k * n) mod k = 0

proof end;

theorem :: NAT_1:64

for k, l being natural number st k > 1 holds
1 mod k = 1

proof end;

theorem :: NAT_1:65

for k, l, n, m being natural number st k mod n = 0 & l = k - (m * n) holds
l mod n = 0

proof end;

theorem :: NAT_1:66

for k, l, n being natural number st n <> 0 & k mod n = 0 & l < n holds
(k + l) mod n = l

proof end;

theorem :: NAT_1:67

for k, l, n being natural number st k mod n = 0 holds
(k + l) mod n = l mod n

proof end;

theorem :: NAT_1:68

for k, n being natural number st k <> 0 holds
(k * n) div k = n

proof end;

theorem :: NAT_1:69

for k, n, l being natural number st k mod n = 0 holds
(k + l) div n = (k div n) + (l div n)

proof end;

theorem Th70: :: NAT_1:70

for m, n being Nat holds
( not m < n + 1 or m < n or m = n )

proof end;

theorem :: NAT_1:71

for k being Nat holds
( not k < 2 or k = 0 or k = 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 :: NAT_1:72

for m, k being Nat st k <> 0 holds
(m * k) div k = m

proof end;

theorem Th1: :: NAT_1:73

for m, n, k being natural number holds m mod n = ((n * k) + m) mod n

proof end;

theorem Th2: :: NAT_1:74

for p, s, n being natural number holds (p + s) mod n = ((p mod n) + s) mod n

proof end;

theorem :: NAT_1:75

for p, s, n being natural number holds (p + s) mod n = (p + (s mod n)) mod n by Th2;

theorem Th4: :: NAT_1:76

for n, k being natural number st k < n holds
k mod n = k

proof end;

theorem Th5: :: NAT_1:77

for n being natural number holds n mod n = 0

proof end;

theorem Th6: :: NAT_1:78

for n being natural number holds 0 = 0 mod n

proof end;