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


begin

:: The results of axioms of Nats
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
proofend;

:: Addition and multiplication
:: The Nats are real numbers therefore some theorems of real
:: numbers are translated for Nats.
registration
let n, k be Nat;
clustern + k ->  natural ;
coherence
 n + k is natural
proofend;
end;

definition
let n be Nat;
let k be Element of NAT ;
:: original:+
redefine funcn + k ->  Element of NAT ;
coherence
 n + k is Element of NAT by ORDINAL1:def_12;
end;

definition
let n be Element of NAT ;
let k be Nat;
:: original:+
redefine funcn + k ->  Element of NAT ;
coherence
 n + k is Element of NAT by ORDINAL1:def_12;
end;

scheme :: NAT_1:sch 1
Ind{ P1[ Nat] } :
 for k being Element of NAT holds P1[k]
provided
A1: P1[ 0 ] and
A2: for k being Element of NAT st P1[k] holds
P1[k + 1]
proofend;

scheme :: NAT_1:sch 2
NatInd{ P1[ Nat] } :
 for k being Nat holds P1[k]
provided
A1: P1[ 0 ] and
A2: for k being Nat st P1[k] holds
P1[k + 1]
proofend;

:: Like addition, the result of multiplication of two Nats is
:: a Nat.
registration
let n, k be Nat;
clustern * k ->  natural ;
coherence
 n * k is natural
proofend;
end;

definition
let n be Nat;
let k be Element of NAT ;
:: original:*
redefine funcn * k ->  Element of NAT ;
coherence
 n * k is Element of NAT by ORDINAL1:def_12;
end;

definition
let n be Element of NAT ;
let k be Nat;
:: original:*
redefine funcn * k ->  Element of NAT ;
coherence
 n * k is Element of NAT by ORDINAL1:def_12;
end;

:: Order relation ::
:: Some theorems of not great relation "<=" in real numbers are translated
:: to Nat easy and it is necessary to have them here.
theorem Th2: :: NAT_1:2
for i being Nat holds 0 <= i
proofend;

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

theorem :: NAT_1:5
for i being Nat holds 0 < i + 1
proofend;

theorem Th6: :: NAT_1:6
for i being Nat holds
( i = 0 or ex k being Nat st i = k + 1 )
proofend;

theorem Th7: :: NAT_1:7
for i, j being Nat st i + j = 0 holds
( i = 0 &amp; j = 0 )
proofend;

registration
cluster non zero epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal for set ;
existence
 not for b1 being Nat holds b1 is zero
proofend;
end;

registration
let m be Nat;
let n be non zero Nat;
clusterm + n ->  non zero ;
coherence
 not m + n is empty by Th7;
clustern + m ->  non zero ;
coherence
 not n + m is empty ;
end;

scheme :: NAT_1:sch 3
DefbyInd{ F1() ->  Nat, F2( Nat, Nat) ->  Nat, P1[ Nat, Nat] } :
 ( ( for k being Nat ex n being Nat st P1[k,n] ) &amp; ( for k, n, m being Nat st P1[k,n] &amp; P1[k,m] holds
n = m ) )
provided
A1: for k, n being Nat holds
( P1[k,n] iff ( ( k = 0 &amp; n = F1() ) or ex m, l being Nat st
( k = m + 1 &amp; P1[m,l] &amp; n = F2(k,l) ) ) )
proofend;

theorem Th8: :: NAT_1:8
for i, j being Nat holds
( not i <= j + 1 or i <= j or i = j + 1 )
proofend;

theorem Th9: :: NAT_1:9
for i, j being Nat st i <= j &amp; j <= i + 1 &amp; not i = j holds
j = i + 1
proofend;

theorem Th10: :: NAT_1:10
for i, j being Nat st i <= j holds
ex k being Nat st j = i + k
proofend;

theorem Th11: :: NAT_1:11
for i, j being Nat holds i <= i + j
proofend;

scheme :: NAT_1:sch 4
CompInd{ P1[ Nat] } :
 for k being Nat holds P1[k]
provided
A1: for k being Nat st ( for n being Nat st n < k holds
P1[n] ) holds
P1[k]
proofend;

scheme :: NAT_1:sch 5
Min{ P1[ Nat] } :
 ex k being Nat st
( P1[k] &amp; ( for n being Nat st P1[n] holds
k <= n ) )
provided
A1: ex k being Nat st P1[k]
proofend;

scheme :: NAT_1:sch 6
Max{ P1[ Nat], F1() ->  Nat } :
 ex k being Nat st
( P1[k] &amp; ( for n being Nat st P1[n] holds
n <= k ) )
provided
A1: for k being Nat st P1[k] holds
k <= F1() and
A2: ex k being Nat st P1[k]
proofend;

theorem Th12: :: NAT_1:12
for i, j, h being Nat st i <= j holds
i <= j + h
proofend;

theorem Th13: :: NAT_1:13
for i, j being Nat holds
( i < j + 1 iff i <= j )
proofend;

theorem Th14: :: NAT_1:14
for j being Nat st j < 1 holds
j = 0
proofend;

theorem :: NAT_1:15
for i, j being Nat st i * j = 1 holds
i = 1
proofend;

theorem Th16: :: NAT_1:16
for k, n being Nat st k <> 0 holds
n < n + k
proofend;

scheme :: NAT_1:sch 7
Regr{ P1[ Nat] } :
 P1[ 0 ]
provided
A1: ex k being Nat st P1[k] and
A2: for k being Nat st k <> 0 &amp; P1[k] holds
ex n being Nat st
( n < k &amp; P1[n] )
proofend;

:: Exact division and rest of division
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 &amp; t < m )
proofend;

theorem :: NAT_1:18
for n, m, k, t, k1, t1 being Nat st n = (m * k) + t &amp; t < m &amp; n = (m * k1) + t1 &amp; t1 < m holds
( k = k1 &amp; t = t1 )
proofend;

registration
cluster natural  ->  ordinal for set ;
coherence
 for b1 being Nat holds b1 is ordinal ;
end;

registration
cluster non empty ordinal for Element of K6(REAL);
existence
 ex b1 being Subset of REAL st
( not b1 is empty &amp; b1 is ordinal )
proofend;
end;

theorem :: NAT_1:19
for k, n being Nat holds
( k < k + n iff 1 <= n )
proofend;

theorem :: NAT_1:20
for k, n being Nat st k < n holds
n - 1 is Element of NAT
proofend;

theorem :: NAT_1:21
for k, n being Nat st k <= n holds
n - k is Element of NAT
proofend;

begin

:: from ALGSEQ_1
theorem Th22: :: NAT_1:22
for m, n being Nat holds
( not m < n + 1 or m < n or m = n )
proofend;

theorem :: NAT_1:23
for k being Nat holds
( not k < 2 or k = 0 or k = 1 )
proofend;

registration
cluster non zero epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal for Element of NAT ;
existence
 not for b1 being Element of NAT holds b1 is zero
proofend;
end;

registration
cluster  ->  non negative for Element of NAT ;
coherence
 for b1 being Element of NAT holds not b1 is negative by Th2;
end;

registration
cluster natural  ->  non negative for set ;
coherence
 for b1 being Nat holds not b1 is negative by Th2;
end;

:: from JORDAN4
theorem :: NAT_1:24
for i, h, j being Nat st i <> 0 &amp; h = j * i holds
j <= h
proofend;

scheme :: NAT_1:sch 8
Ind1{ F1() ->  Nat, P1[ Nat] } :
 for i being Nat st F1() <= i holds
P1[i]
provided
A1: P1[F1()] and
A2: for j being Nat st F1() <= j &amp; P1[j] holds
P1[j + 1]
proofend;

scheme :: NAT_1:sch 9
CompInd1{ F1() ->  Nat, P1[ Nat] } :
 for k being Nat st k >= F1() holds
P1[k]
provided
A1: for k being Nat st k >= F1() &amp; ( for n being Nat st n >= F1() &amp; n < k holds
P1[n] ) holds
P1[k]
proofend;

:: Moved from CQC_THE1 on 07.07.2006 by AK
theorem Th25: :: NAT_1:25
for n being Nat holds
( not n <= 1 or n = 0 or n = 1 )
proofend;

theorem Th26: :: NAT_1:26
for n being Nat holds
( not n <= 2 or n = 0 or n = 1 or n = 2 )
proofend;

theorem Th27: :: NAT_1:27
for n being Nat holds
( not n <= 3 or n = 0 or n = 1 or n = 2 or n = 3 )
proofend;

theorem Th28: :: NAT_1:28
for n being Nat holds
( not n <= 4 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 )
proofend;

theorem Th29: :: NAT_1:29
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 )
proofend;

theorem Th30: :: NAT_1:30
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 )
proofend;

theorem Th31: :: NAT_1:31
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 )
proofend;

theorem Th32: :: NAT_1:32
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 )
proofend;

theorem Th33: :: NAT_1:33
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 )
proofend;

theorem Th34: :: NAT_1:34
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 )
proofend;

theorem Th35: :: NAT_1:35
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 )
proofend;

theorem Th36: :: NAT_1:36
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 )
proofend;

theorem Th37: :: NAT_1:37
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 )
proofend;

scheme :: NAT_1:sch 10
Indfrom1{ P1[ Nat] } :
 for k being non empty Nat holds P1[k]
provided
A1: P1[1] and
A2: for k being non empty Nat st P1[k] holds
P1[k + 1]
proofend;

:: from HENMODEL, 2007.03.15, A.T.
definition
let A be set ;
func min* A ->  Element of NAT  means :Def1: :: NAT_1:def 1
( it in A &amp; ( 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 b1 being Element of NAT st
( b1 in A &amp; ( for k being Nat st k in A holds
b1 <= k ) ) ) &amp; ( A is not non empty Subset of NAT implies ex b1 being Element of NAT st b1 = 0 ) )
proofend;
uniqueness
 for b1, b2 being Element of NAT holds
( ( A is non empty Subset of NAT &amp; b1 in A &amp; ( for k being Nat st k in A holds
b1 <= k ) &amp; b2 in A &amp; ( for k being Nat st k in A holds
b2 <= k ) implies b1 = b2 ) &amp; ( A is not non empty Subset of NAT &amp; b1 = 0 &amp; b2 = 0 implies b1 = b2 ) )
proofend;
consistency
 for b1 being Element of NAT holds verum ;
end;

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

theorem Th38: :: NAT_1:38
for n being Nat holds succ n = n + 1
proofend;

theorem Th39: :: NAT_1:39
for n, m being Nat holds
( n <= m iff n c= m )
proofend;

theorem Th40: :: NAT_1:40
for n, m being Nat holds
( card n c= card m iff n <= m )
proofend;

theorem Th41: :: NAT_1:41
for n, m being Nat holds
( card n in card m iff n < m )
proofend;

theorem :: NAT_1:42
for n being Nat holds nextcard (card n) = card (n + 1)
proofend;

definition
let n be Nat;
redefine func succ n equals :: NAT_1:def 2
n + 1;
compatibility
 for b1 being set holds
( b1 = succ n iff b1 = n + 1 ) by Th38;
end;

:: deftheorem  defines succ NAT_1:def_2_:_
 for n being Nat holds succ n = n + 1;

theorem :: NAT_1:43
for X, Y being finite set st X c= Y holds
card X <= card Y
proofend;

theorem :: NAT_1:44
for k, n being Nat holds
( k in n iff k < n )
proofend;

theorem :: NAT_1:45
for n being Nat holds n in n + 1
proofend;

theorem :: NAT_1:46
for k, n being Nat st k <= n holds
k = k /\ n
proofend;

scheme :: NAT_1:sch 11
LambdaRecEx{ F1() ->  set , F2( set , set ) ->  set } :
 ex f being Function st
( dom f = NAT &amp; f . 0 = F1() &amp; ( for n being Nat holds f . (n + 1) = F2(n,(f . n)) ) )
proofend;

scheme :: NAT_1:sch 12
LambdaRecExD{ F1() ->  non empty set , F2() ->  Element of F1(), F3( set , set ) ->  Element of F1() } :
 ex f being Function of NAT,F1() st
( f . 0 = F2() &amp; ( for n being Nat holds f . (n + 1) = F3(n,(f . n)) ) )
proofend;

scheme :: NAT_1:sch 13
RecUn{ F1() ->  set , F2() ->  Function, F3() ->  Function, P1[ set , set , set ] } :
 F2() = F3()
provided
A1: dom F2() = NAT and
A2: F2() . 0 = F1() and
A3: for n being Nat holds P1[n,F2() . n,F2() . (n + 1)] and
A4: dom F3() = NAT and
A5: F3() . 0 = F1() and
A6: for n being Nat holds P1[n,F3() . n,F3() . (n + 1)] and
A7: for n being Nat
for x, y1, y2 being set st P1[n,x,y1] &amp; P1[n,x,y2] holds
y1 = y2
proofend;

scheme :: NAT_1:sch 14
RecUnD{ F1() ->  non empty set , F2() ->  Element of F1(), P1[ set , set , set ], F3() ->  Function of NAT,F1(), F4() ->  Function of NAT,F1() } :
 F3() = F4()
provided
A1: F3() . 0 = F2() and
A2: for n being Nat holds P1[n,F3() . n,F3() . (n + 1)] and
A3: F4() . 0 = F2() and
A4: for n being Nat holds P1[n,F4() . n,F4() . (n + 1)] and
A5: for n being Nat
for x, y1, y2 being Element of F1() st P1[n,x,y1] &amp; P1[n,x,y2] holds
y1 = y2
proofend;

scheme :: NAT_1:sch 15
LambdaRecUn{ F1() ->  set , F2( set , set ) ->  set , F3() ->  Function, F4() ->  Function } :
 F3() = F4()
provided
A1: dom F3() = NAT and
A2: F3() . 0 = F1() and
A3: for n being Nat holds F3() . (n + 1) = F2(n,(F3() . n)) and
A4: dom F4() = NAT and
A5: F4() . 0 = F1() and
A6: for n being Nat holds F4() . (n + 1) = F2(n,(F4() . n))
proofend;

scheme :: NAT_1:sch 16
LambdaRecUnD{ F1() ->  non empty set , F2() ->  Element of F1(), F3( set , set ) ->  Element of F1(), F4() ->  Function of NAT,F1(), F5() ->  Function of NAT,F1() } :
 F4() = F5()
provided
A1: F4() . 0 = F2() and
A2: for n being Nat holds F4() . (n + 1) = F3(n,(F4() . n)) and
A3: F5() . 0 = F2() and
A4: for n being Nat holds F5() . (n + 1) = F3(n,(F5() . n))
proofend;

:: missing, 2008.02.22, A.T.
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;

definition
let x, y be Element of NAT ;
:: original:min
redefine func min (x,y) ->  Element of NAT ;
coherence
 min (x,y) is Element of NAT by XXREAL_0:15;
:: original:max
redefine func max (x,y) ->  Element of NAT ;
coherence
 max (x,y) is Element of NAT by XXREAL_0:16;
end;

scheme :: NAT_1:sch 17
MinIndex{ F1( Nat) ->  Nat } :
 ex k being Nat st
( F1(k) = 0 &amp; ( for n being Nat st F1(n) = 0 holds
k <= n ) )
provided
A1: for k being Nat holds
( F1((k + 1)) < F1(k) or F1(k) = 0 )
proofend;

:: Added by AK, 2007.10.09
definition
let D be set ;
let f be Function of NAT,D;
let n be Nat;
:: original:.
redefine funcf . n ->  Element of D;
coherence
 f . n is Element of D
proofend;
end;

:: from MODELC_2, 2008.08.18, A.T.
definition
let X be set ;
mode sequence of X is Function of NAT,X;
end;

:: from SEQM_3, BHSP_3, COMSEQ_3, KURATO_2, LOPBAN_3, CLVECT_2, CLOPBAN3
:: (generalized), 2008.08.23, A.T.
definition
let s be ManySortedSet of NAT ;
let k be Nat;
funcs ^\ k ->  ManySortedSet of NAT  means :Def3: :: NAT_1:def 3
 for n being Nat holds it . n = s . (n + k);
existence
 ex b1 being ManySortedSet of NAT st
for n being Nat holds b1 . n = s . (n + k)
proofend;
uniqueness
 for b1, b2 being ManySortedSet of NAT st ( for n being Nat holds b1 . n = s . (n + k) ) &amp; ( for n being Nat holds b2 . n = s . (n + k) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines ^\ NAT_1:def_3_:_
 for s being ManySortedSet of NAT
for k being Nat
for b3 being ManySortedSet of NAT holds
( b3 = s ^\ k iff for n being Nat holds b3 . n = s . (n + k) );

Lm1:  for s being ManySortedSet of NAT
for k being Nat holds rng (s ^\ k) c= rng s
proofend;

registration
let X be non empty set ;
let s be X -valued ManySortedSet of NAT ;
let k be Nat;
clusters ^\ k -> X -valued ;
coherence
 s ^\ k is X -valued
proofend;
end;

definition
let X be non empty set ;
let s be sequence of X;
let k be Nat;
:: original:^\
redefine funcs ^\ k ->  sequence of X;
coherence
 s ^\ k is sequence of X
proofend;
end;

theorem :: NAT_1:47
for X being non empty set
for s being sequence of X holds s ^\ 0 = s
proofend;

theorem Th48: :: NAT_1:48
for X being non empty set
for s being sequence of X
for k, m being Nat holds (s ^\ k) ^\ m = s ^\ (k + m)
proofend;

theorem :: 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 ^\ m) ^\ k
proofend;

registration
let N be sequence of NAT;
let X be non empty set ;
let s be sequence of X;
clusterN * s ->  NAT -defined X -valued Function-like ;
coherence
 ( s * N is Function-like &amp; s * N is NAT -defined &amp; s * N is X -valued ) ;
end;

registration
let N be sequence of NAT;
let X be non empty set ;
let s be sequence of X;
clusterN * s ->  total ;
coherence
 s * N is total ;
end;

:::definition
::: let X be non empty set;
::: mode sequence of X is X-valued ManySortedSet of NAT;
:::end;
theorem :: NAT_1:50
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)
proofend;

theorem :: NAT_1:51
for n being Nat
for X being non empty set
for s being sequence of X holds s . n in rng s
proofend;

theorem :: NAT_1:52
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
proofend;

:: from UPROOTS, 2009.07.21, A.T.
theorem :: NAT_1:53
for n being Nat holds
( n is zero or n = 1 or n > 1 )
proofend;

theorem :: NAT_1:54
for n being Nat holds succ n =  {  l where l is Element of NAT : l <= n  }
proofend;

scheme :: NAT_1:sch 18
MinPred{ F1( Element of NAT ) ->  Element of NAT , P1[ set ] } :
 ex k being Element of NAT st
( P1[k] &amp; ( for n being Element of NAT st P1[n] holds
k <= n ) )
provided
A1: for k being Element of NAT holds
( F1((k + 1)) < F1(k) or P1[k] )
proofend;

registration
let k be Ordinal;
let x be set ;
clusterk --> x ->  T-Sequence-like ;
coherence
 k --> x is T-Sequence-like
proofend;
end;

theorem :: NAT_1:55
for s being ManySortedSet of NAT
for k being Nat holds rng (s ^\ k) c= rng s by Lm1;

:: from JORDAN2C, 2011.07.03, A.T.
theorem Th56: :: NAT_1:56
for n being Nat
for m being Nat st n <= m &amp; m <= n + 2 &amp; not m = n &amp; not m = n + 1 holds
m = n + 2
proofend;

theorem Th57: :: NAT_1:57
for n being Nat
for m being Nat st n <= m &amp; m <= n + 3 &amp; not m = n &amp; not m = n + 1 &amp; not m = n + 2 holds
m = n + 3
proofend;

theorem :: NAT_1:58
for n being Nat
for m being Nat st n <= m &amp; m <= n + 4 &amp; not m = n &amp; not m = n + 1 &amp; not m = n + 2 &amp; not m = n + 3 holds
m = n + 4
proofend;

:: from GLIB_002, 2011.07.30, A.T.
theorem :: NAT_1:59
for X being finite set st 1 < card X holds
ex x1, x2 being set st
( x1 in X &amp; x2 in X &amp; x1 <> x2 )
proofend;

theorem :: NAT_1:60
for n being Nat holds
( not n <= 14 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 or n = 14 )
proofend;