:: The Fundamental Properties of Natural Numbers
:: by Grzegorz Bancerek
::
:: Received January 11, 1989
:: Copyright (c) 1990 Association of Mizar Users

begin

definition

mode Nat is natural number ;

end;

theorem Th1: :: NAT_1:1

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 n being Nat holds n in X

proof end;

registration

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

proof end;

end;

definition

let n be Nat;
let k be Element of NAT ;
:: original: +
redefine func n + k -> Element of NAT ;
coherence
n + k is Element of NAT by ORDINAL1:def 13;

end;

definition

let n be Element of NAT ;
let k be Nat;
:: original: +
redefine func n + k -> Element of NAT ;
coherence
n + k is Element of NAT by ORDINAL1:def 13;

end;

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

for k being Element of NAT holds P₁[k]

provided

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

proof end;

scheme :: NAT_1:sch 2
NatInd{ 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;

registration

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

proof end;

end;

definition

let n be Nat;
let k be Element of NAT ;
:: original: *
redefine func n * k -> Element of NAT ;
coherence
n * k is Element of NAT by ORDINAL1:def 13;

end;

definition

let n be Element of NAT ;
let k be Nat;
:: original: *
redefine func n * k -> Element of NAT ;
coherence
n * k is Element of NAT by ORDINAL1:def 13;

end;

theorem Th2: :: NAT_1:2

for i being Nat holds 0 <= i

proof end;

theorem :: NAT_1:3

for i being Nat st 0 <> i holds
0 < i by Th2;

theorem :: NAT_1:4

for i, j, h being Nat st i <= j holds
i * h <= j * h

proof end;

theorem :: NAT_1:5

for i being Nat holds 0 < i + 1

proof end;

theorem Th6: :: NAT_1:6

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

proof end;

theorem Th7: :: NAT_1:7

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

proof end;

registration

cluster non zero epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set ;
existence
not for b₁ being Nat holds b₁ is empty

proof end;

end;

registration

let m be Nat;
let n be non zero Nat;
cluster m + n -> non zero ;
coherence
not m + n is empty by Th7;
cluster n + m -> non zero ;
coherence
not n + m is empty ;

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 Th8: :: NAT_1:8

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

proof end;

theorem :: NAT_1:9

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

proof end;

theorem Th10: :: NAT_1:10

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

proof end;

theorem Th11: :: NAT_1:11

for i, j being Nat 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 Th12: :: NAT_1:12

for i, j, h being Nat st i <= j holds
i <= j + h

proof end;

theorem Th13: :: NAT_1:13

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

proof end;

theorem Th14: :: NAT_1:14

for j being Nat st j < 1 holds
j = 0

proof end;

theorem :: NAT_1:15

for i, j being Nat st i * j = 1 holds
i = 1

proof end;

theorem Th16: :: NAT_1:16

for k, n being Nat 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 :: NAT_1:17

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 :: NAT_1:18

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

proof end;

registration

cluster natural -> ordinal set ;
coherence
for b₁ being Nat holds b₁ is ordinal ;

end;

registration

cluster non empty ordinal Element of K6(REAL);
existence
ex b₁ being Subset of REAL st
( not b₁ is empty & b₁ is ordinal )

proof end;

end;

theorem :: NAT_1:19

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

proof end;

theorem :: NAT_1:20

for k, n being Nat st k < n holds
n - 1 is Element of NAT

proof end;

theorem :: NAT_1:21

for k, n being Nat st k <= n holds
n - k is Element of NAT

proof end;

begin

theorem Th22: :: NAT_1:22

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

proof end;

theorem :: NAT_1:23

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

proof end;

registration

cluster non zero epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT ;
existence
not for b₁ being Element of NAT holds b₁ is empty

proof end;

end;

registration

cluster -> non negative Element of NAT ;
coherence
for b₁ being Element of NAT holds not b₁ is negative by Th2;

end;

registration

cluster natural -> non negative set ;
coherence
for b₁ being Nat holds not b₁ is negative by Th2;

end;

theorem :: NAT_1:24

for i, h, j being Nat st i <> 0 & h = j * i holds
j <= h

proof end;

theorem :: NAT_1:25

canceled;

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

for i being Nat st F₁() <= i holds
P₁[i]

provided

A1: P₁[F₁()] and
A2: for j being Nat st F₁() <= j & P₁[j] holds
P₁[j + 1]

proof end;

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

for k being Nat st k >= F₁() holds
P₁[k]

provided

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

proof end;

theorem Th26: :: NAT_1:26

for n being Nat holds
( not n <= 1 or n = 0 or n = 1 )

proof end;

theorem Th27: :: NAT_1:27

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

proof end;

theorem Th28: :: NAT_1:28

for n being Nat holds
( not n <= 3 or n = 0 or n = 1 or n = 2 or n = 3 )

proof end;

theorem Th29: :: NAT_1:29

for n being Nat holds
( not n <= 4 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 )

proof end;

theorem Th30: :: NAT_1:30

for n being Nat holds
( not n <= 5 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 )

proof end;

theorem Th31: :: NAT_1:31

for n being Nat holds
( not n <= 6 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 )

proof end;

theorem Th32: :: NAT_1:32

for n being Nat holds
( not n <= 7 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 or n = 7 )

proof end;

theorem Th33: :: NAT_1:33

for n being Nat holds
( not n <= 8 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 or n = 7 or n = 8 )

proof end;

theorem Th34: :: NAT_1:34

for n being Nat holds
( not n <= 9 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 or n = 7 or n = 8 or n = 9 )

proof end;

theorem Th35: :: NAT_1:35

for n being Nat holds
( not n <= 10 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 or n = 7 or n = 8 or n = 9 or n = 10 )

proof end;

theorem Th36: :: NAT_1:36

for n being Nat holds
( not n <= 11 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 or n = 7 or n = 8 or n = 9 or n = 10 or n = 11 )

proof end;

theorem Th37: :: NAT_1:37

for n being Nat holds
( not n <= 12 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 or n = 7 or n = 8 or n = 9 or n = 10 or n = 11 or n = 12 )

proof end;

theorem :: NAT_1:38

for n being Nat holds
( not n <= 13 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 or n = 7 or n = 8 or n = 9 or n = 10 or n = 11 or n = 12 or n = 13 )

proof end;

scheme :: NAT_1:sch 10
Indfrom1{ P₁[ Nat] } :

for k being non empty Nat holds P₁[k]

provided

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

proof end;

definition

let A be set ;
func min* A -> Element of NAT means :Def1: :: NAT_1:def 1
( it in A & ( for k being Nat st k in A holds
it <= k ) ) if A is non empty Subset of NAT
otherwise it = 0 ;
existence
( ( A is non empty Subset of NAT implies ex b₁ being Element of NAT st
( b₁ in A & ( for k being Nat st k in A holds
b₁ <= k ) ) ) & ( A is not non empty Subset of NAT implies ex b₁ being Element of NAT st b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT holds
( ( A is non empty Subset of NAT & b₁ in A & ( for k being Nat st k in A holds
b₁ <= k ) & b₂ in A & ( for k being Nat st k in A holds
b₂ <= k ) implies b₁ = b₂ ) & ( A is not non empty Subset of NAT & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being Element of NAT holds verum ;

end;

:: deftheorem Def1 defines min* NAT_1:def 1 :
for A being set
for b₂ being Element of NAT holds
( ( A is non empty Subset of NAT implies ( b₂ = min* A iff ( b₂ in A & ( for k being Nat st k in A holds
b₂ <= k ) ) ) ) & ( A is not non empty Subset of NAT implies ( b₂ = min* A iff b₂ = 0 ) ) );

theorem Th39: :: NAT_1:39

for n being natural number holds succ n = n + 1

proof end;

theorem Th40: :: NAT_1:40

for n, m being Nat holds
( n <= m iff n c= m )

proof end;

theorem Th41: :: NAT_1:41

for n, m being Nat holds
( card n c= card m iff n <= m )

proof end;

theorem Th42: :: NAT_1:42

for n, m being Nat holds
( card n in card m iff n < m )

proof end;

theorem :: NAT_1:43

for n being Nat holds nextcard (card n) = card (n + 1)

proof end;

definition

let n be natural number ;
redefine func succ n equals :: NAT_1:def 2
n + 1;
compatibility
for b₁ being set holds
( b₁ = succ n iff b₁ = n + 1 ) by Th39;

end;

:: deftheorem defines succ NAT_1:def 2 :
for n being natural number holds succ n = n + 1;

theorem :: NAT_1:44

for X, Y being finite set st X c= Y holds
card X <= card Y

proof end;

theorem :: NAT_1:45

for k, n being Nat holds
( k in n iff k < n )

proof end;

theorem :: NAT_1:46

for n being Nat holds n in n + 1

proof end;

theorem :: NAT_1:47

for k, n being Nat st k <= n holds
k = k /\ n

proof end;

scheme :: NAT_1:sch 11
LambdaRecEx{ F₁() -> set , F₂( set , set ) -> set } :

ex f being Function st
( dom f = NAT & f . 0 = F₁() & ( for n being Nat holds f . (n + 1) = F₂(n,(f . n)) ) )

proof end;

scheme :: NAT_1:sch 12
LambdaRecExD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃( set , set ) -> Element of F₁() } :

ex f being Function of NAT,F₁() st
( f . 0 = F₂() & ( for n being Nat holds f . (n + 1) = F₃(n,(f . n)) ) )

proof end;

scheme :: NAT_1:sch 13
RecUn{ F₁() -> set , F₂() -> Function, F₃() -> Function, P₁[ set , set , set ] } :

F₂() = F₃()

provided

A1: dom F₂() = NAT and
A2: F₂() . 0 = F₁() and
A3: for n being Nat holds P₁[n,F₂() . n,F₂() . (n + 1)] and
A4: dom F₃() = NAT and
A5: F₃() . 0 = F₁() and
A6: for n being Nat holds P₁[n,F₃() . n,F₃() . (n + 1)] and
A7: for n being Nat
for x, y1, y2 being set st P₁[n,x,y1] & P₁[n,x,y2] holds
y1 = y2

proof end;

scheme :: NAT_1:sch 14
RecUnD{ F₁() -> non empty set , F₂() -> Element of F₁(), P₁[ set , set , set ], F₃() -> Function of NAT,F₁(), F₄() -> Function of NAT,F₁() } :

F₃() = F₄()

provided

A1: F₃() . 0 = F₂() and
A2: for n being Nat holds P₁[n,F₃() . n,F₃() . (n + 1)] and
A3: F₄() . 0 = F₂() and
A4: for n being Nat holds P₁[n,F₄() . n,F₄() . (n + 1)] and
A5: for n being Nat
for x, y1, y2 being Element of F₁() st P₁[n,x,y1] & P₁[n,x,y2] holds
y1 = y2

proof end;

scheme :: NAT_1:sch 15
LambdaRecUn{ F₁() -> set , F₂( set , set ) -> set , F₃() -> Function, F₄() -> Function } :

F₃() = F₄()

provided

A1: dom F₃() = NAT and
A2: F₃() . 0 = F₁() and
A3: for n being Nat holds F₃() . (n + 1) = F₂(n,(F₃() . n)) and
A4: dom F₄() = NAT and
A5: F₄() . 0 = F₁() and
A6: for n being Nat holds F₄() . (n + 1) = F₂(n,(F₄() . n))

proof end;

scheme :: NAT_1:sch 16
LambdaRecUnD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃( set , set ) -> Element of F₁(), F₄() -> Function of NAT,F₁(), F₅() -> Function of NAT,F₁() } :

F₄() = F₅()

provided

A1: F₄() . 0 = F₂() and
A2: for n being Nat holds F₄() . (n + 1) = F₃(n,(F₄() . n)) and
A3: F₅() . 0 = F₂() and
A4: for n being Nat holds F₅() . (n + 1) = F₃(n,(F₅() . n))

proof end;

registration

let x, y be Nat;
cluster min (x,y) -> natural ;
coherence
min (x,y) is natural by XXREAL_0:15;
cluster max (x,y) -> natural ;
coherence
max (x,y) is natural by XXREAL_0:16;

end;

scheme :: NAT_1:sch 17
MinIndex{ F₁( Nat) -> Nat } :

ex k being Nat st
( F₁(k) = 0 & ( for n being Nat st F₁(n) = 0 holds
k <= n ) )

provided

A1: for k being Nat holds
( F₁((k + 1)) < F₁(k) or F₁(k) = 0 )

proof end;

definition

let D be set ;
let f be Function of NAT,D;
let n be Nat;
:: original: .
redefine func f . n -> Element of D;
coherence
f . n is Element of D

proof end;

end;

definition

let X be set ;
mode sequence of X is Function of NAT,X;

end;

definition

let X be non empty set ;
let s be sequence of X;
let k be Nat;
func s ^\ k -> sequence of X means :Def3: :: NAT_1:def 3
for n being Nat holds it . n = s . (n + k);
existence
ex b₁ being sequence of X st
for n being Nat holds b₁ . n = s . (n + k)

proof end;

uniqueness
for b₁, b₂ being sequence of X st ( for n being Nat holds b₁ . n = s . (n + k) ) & ( for n being Nat holds b₂ . n = s . (n + k) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines ^\ NAT_1:def 3 :
for X being non empty set
for s being sequence of X
for k being Nat
for b₄ being sequence of X holds
( b₄ = s ^\ k iff for n being Nat holds b₄ . n = s . (n + k) );

theorem :: NAT_1:48

for X being non empty set
for s being sequence of X holds s ^\ 0 = s

proof end;

theorem Th49: :: NAT_1:49

for X being non empty set
for s being sequence of X
for k, m being Nat holds (s ^\ k) ^\ m = s ^\ (k + m)

proof end;

theorem :: NAT_1:50

for X being non empty set
for s being sequence of X
for k, m being Nat holds (s ^\ k) ^\ m = (s ^\ m) ^\ k

proof end;

theorem :: NAT_1:51

for X being non empty set
for s being sequence of X
for k being Nat
for N being sequence of NAT holds (s * N) ^\ k = s * (N ^\ k)

proof end;

theorem :: NAT_1:52

for n being Nat
for X being non empty set
for s being sequence of X holds s . n in rng s

proof end;

theorem :: NAT_1:53

for Y being set
for X being non empty set
for s being sequence of X st ( for n being Nat holds s . n in Y ) holds
rng s c= Y

proof end;

theorem :: NAT_1:54

for n being natural number holds
( n is empty or n = 1 or n > 1 )

proof end;

theorem :: NAT_1:55

for n being Nat holds succ n = { l where l is Element of NAT : l <= n }

proof end;

scheme :: NAT_1:sch 18
MinPred{ F₁( Element of NAT ) -> Element of NAT , P₁[ set ] } :

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

provided

A1: for k being Element of NAT holds
( F₁((k + 1)) < F₁(k) or P₁[k] )

proof end;

registration

let k be Ordinal;
let x be set ;
cluster k --> x -> T-Sequence-like ;
coherence
k --> x is T-Sequence-like

proof end;

end;