:: NAT_1 semantic presentation

begin


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
let A be Subset of REAL; ::_thesis: ( 0 in A & ( for x being Real st x in A holds
x + 1 in A ) implies for n being Nat holds n in A )
assume A1: 0 in A ; ::_thesis: ( ex x being Real st
( x in A & not x + 1 in A ) or for n being Nat holds n in A )
assume  for x being Real st x in A holds
x + 1 in A ; ::_thesis: for n being Nat holds n in A
then  for x being real number st x in A holds
x + 1 in A ;
then A2: NAT c= A by A1, AXIOMS:3;
let n be Nat; ::_thesis: n in A
 n in NAT by ORDINAL1:def_12;
hence  n in A by A2; ::_thesis: verum
end;

registration
let n, k be Nat;
clustern + k ->  natural ;
coherence
 n + k is natural
proof
defpred S1[ Real] means  ex k being Nat st
( n = k & n + k is natural );
consider X being Subset of REAL such that
A1: for x being Real holds
( x in X iff S1[x] ) from SUBSET_1:sch_3();
A2: now__::_thesis:_for_x_being_Real_st_x_in_X_holds_
x_+_1_in_X
let x be Real; ::_thesis: ( x in X implies x + 1 in X )
assume  x in X ; ::_thesis: x + 1 in X
then consider k being Nat such that
A3: x = k and
A4: n + k is natural by A1;
A5: (n + k) + 1 = n + (k + 1) ;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 n + k is Element of NAT by A4, ORDINAL1:def_12;
then  ( k + 1 is Element of NAT & (n + k) + 1 is Element of NAT ) by AXIOMS:2;
hence  x + 1 in X by A1, A3, A5; ::_thesis: verum
end;
 n + 0 = n ;
then  0 in X by A1;
then  k in X by A2, Th1;
then  ex m being Nat st
( k = m & n + m is natural ) by A1;
hence  n + k is natural ; ::_thesis: verum
end;
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]
proof
let k be Nat; ::_thesis: ( k is Element of REAL & k is Element of NAT implies P1[k] )
defpred S1[ Real] means  ex k being Nat st
( P1[k] & k = $1 );
consider X being Subset of REAL such that
A3: for x being Real holds
( x in X iff S1[x] ) from SUBSET_1:sch_3();
A4: for x being Real st x in X holds
x + 1 in X
proof
let x be Real; ::_thesis: ( x in X implies x + 1 in X )
assume  x in X ; ::_thesis: x + 1 in X
then consider k being Nat such that
A5: P1[k] and
A6: k = x by A3;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 P1[k + 1] by A2, A5;
hence  x + 1 in X by A3, A6; ::_thesis: verum
end;
 0 in X by A1, A3;
then  k in X by A4, Th1;
then  ex n being Nat st
( P1[n] & n = k ) by A3;
hence  ( k is Element of REAL & k is Element of NAT implies P1[k] ) ; ::_thesis: verum
end;

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]
proof
A3: for k being Element of NAT st P1[k] holds
P1[k + 1] by A2;
let k be Nat; ::_thesis: P1[k]
A4: k is Element of NAT by ORDINAL1:def_12;
A5: P1[ 0 ] by A1;
 for k being Element of NAT holds P1[k] from NAT_1:sch_1(A5, A3);
hence  P1[k] by A4; ::_thesis: verum
end;

registration
let n, k be Nat;
clustern * k ->  natural ;
coherence
 n * k is natural
proof
defpred S1[ Nat] means n * n is natural ;
A1: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume  S1[m] ; ::_thesis: S1[m + 1]
then reconsider k = n * m as Nat ;
 k + n is Nat ;
hence  S1[m + 1] ; ::_thesis: verum
end;
A2: S1[ 0 ] ;
 for m being Nat holds S1[m] from NAT_1:sch_2(A2, A1);
hence  n * k is natural ; ::_thesis: verum
end;
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;

theorem Th2: :: NAT_1:2
for i being Nat holds 0 <= i
proof
let i be Nat; ::_thesis: 0 <= i
defpred S1[ Nat] means  0 <= $1;
A1: for n being Nat st S1[n] holds
S1[n + 1] ;
A2: S1[ 0 ] ;
 for k being Nat holds S1[k] from NAT_1:sch_2(A2, A1);
hence  0 <= i ; ::_thesis: verum
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
let i, j, h be Nat; ::_thesis: ( i <= j implies i * h <= j * h )
assume A1: i <= j ; ::_thesis: i * h <= j * h
 0 <= h by Th2;
hence  i * h <= j * h by A1, XREAL_1:64; ::_thesis: verum
end;

theorem :: NAT_1:5
for i being Nat holds 0 < i + 1
proof
let i be Nat; ::_thesis: 0 < i + 1
assume A1: 0 >= i + 1 ; ::_thesis: contradiction
 0 <= i by Th2;
hence  contradiction by A1; ::_thesis: verum
end;

theorem Th6: :: NAT_1:6
for i being Nat holds
( i = 0 or ex k being Nat st i = k + 1 )
proof
let i be Nat; ::_thesis: ( i = 0 or ex k being Nat st i = k + 1 )
defpred S1[ Nat] means ( $1 = 0 or ex k being Nat st $1 = k + 1 );
A1: for h being Nat st S1[h] holds
S1[h + 1] ;
A2: S1[ 0 ] ;
 for i being Nat holds S1[i] from NAT_1:sch_2(A2, A1);
hence  ( i = 0 or ex k being Nat st i = k + 1 ) ; ::_thesis: verum
end;

theorem Th7: :: NAT_1:7
for i, j being Nat st i + j = 0 holds
( i = 0 & j = 0 )
proof
let i, j be Nat; ::_thesis: ( i + j = 0 implies ( i = 0 & j = 0 ) )
assume A1: i + j = 0 ; ::_thesis: ( i = 0 & j = 0 )
 ( 0 <= i & 0 <= j ) by Th2;
hence  ( i = 0 & j = 0 ) by A1; ::_thesis: verum
end;

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
proof
take  1 ; ::_thesis: not 1 is zero
thus  not 1 is zero ; ::_thesis: verum
end;
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] ) & ( for k, n, m being Nat st P1[k,n] & P1[k,m] holds
n = m ) )
provided
A1: for k, n being Nat holds
( P1[k,n] iff ( ( k = 0 & n = F1() ) or ex m, l being Nat st
( k = m + 1 & P1[m,l] & n = F2(k,l) ) ) )
proof
reconsider N = F1() as Element of NAT by ORDINAL1:def_12;
defpred S1[ Nat] means  ex n being Nat st P1[$1,n];
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
given n being Nat such that A3: P1[k,n] ; ::_thesis: S1[k + 1]
reconsider F = F2((k + 1),n) as Element of NAT by ORDINAL1:def_12;
take  F ; ::_thesis: P1[k + 1,F]
thus  P1[k + 1,F] by A1, A3; ::_thesis: verum
end;
 P1[ 0 ,N] by A1;
then A4: S1[ 0 ] ;
thus  for k being Nat holds S1[k] from NAT_1:sch_2(A4, A2); ::_thesis: for k, n, m being Nat st P1[k,n] & P1[k,m] holds
n = m
defpred S2[ Nat] means  for n, m being Nat st P1[$1,n] & P1[$1,m] holds
n = m;
A5: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A6: for n, m being Nat st P1[k,n] & P1[k,m] holds
n = m ; ::_thesis: S2[k + 1]
let n, m be Nat; ::_thesis: ( P1[k + 1,n] & P1[k + 1,m] implies n = m )
assume  ( P1[k + 1,n] & P1[k + 1,m] ) ; ::_thesis: n = m
then  ( ex l, u being Nat st
( k + 1 = l + 1 & P1[l,u] & n = F2((k + 1),u) ) & ex v, w being Nat st
( k + 1 = v + 1 & P1[v,w] & m = F2((k + 1),w) ) ) by A1;
hence  n = m by A6; ::_thesis: verum
end;
A7: S2[ 0 ]
proof
let n, m be Nat; ::_thesis: ( P1[ 0 ,n] & P1[ 0 ,m] implies n = m )
assume that
A8: P1[ 0 ,n] and
A9: P1[ 0 ,m] ; ::_thesis: n = m
 for m, l being Nat holds
( not 0 = m + 1 or not P1[m,l] or not n = F2(0,l) ) ;
then  ( ( for n, l being Nat holds
( not 0 = n + 1 or not P1[n,l] or not m = F2(0,l) ) ) & n = F1() ) by A1, A8;
hence  n = m by A1, A9; ::_thesis: verum
end;
thus  for k being Nat holds S2[k] from NAT_1:sch_2(A7, A5); ::_thesis: verum
end;

theorem Th8: :: NAT_1:8
for i, j being Nat holds
( not i <= j + 1 or i <= j or i = j + 1 )
proof
let i, j be Nat; ::_thesis: ( not i <= j + 1 or i <= j or i = j + 1 )
defpred S1[ Nat] means  for j being Nat holds
( not $1 <= j + 1 or $1 <= j or $1 = j + 1 );
A1: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A2: for j being Nat holds
( not i <= j + 1 or i <= j or i = j + 1 ) ; ::_thesis: S1[i + 1]
let j be Nat; ::_thesis: ( not i + 1 <= j + 1 or i + 1 <= j or i + 1 = j + 1 )
assume A3: i + 1 <= j + 1 ; ::_thesis: ( i + 1 <= j or i + 1 = j + 1 )
A4: now__::_thesis:_(_for_k_being_Nat_holds_not_j_=_k_+_1_or_i_+_1_<=_j_or_i_+_1_=_j_+_1_)
given k being Nat such that A5: j = k + 1 ; ::_thesis: ( i + 1 <= j or i + 1 = j + 1 )
 i <= k + 1 by A3, A5, XREAL_1:6;
then  ( i <= k or i = k + 1 ) by A2;
hence  ( i + 1 <= j or i + 1 = j + 1 ) by A5, XREAL_1:6; ::_thesis: verum
end;
now__::_thesis:_(_not_j_=_0_or_i_+_1_<=_j_or_i_+_1_=_j_+_1_)
A6: 0 <= i by Th2;
assume A7: j = 0 ; ::_thesis: ( i + 1 <= j or i + 1 = j + 1 )
then  i <= 0 by A3, XREAL_1:6;
hence  ( i + 1 <= j or i + 1 = j + 1 ) by A7, A6; ::_thesis: verum
end;
hence  ( i + 1 <= j or i + 1 = j + 1 ) by A4, Th6; ::_thesis: verum
end;
A8: S1[ 0 ] by Th2;
 for i being Nat holds S1[i] from NAT_1:sch_2(A8, A1);
hence  ( not i <= j + 1 or i <= j or i = j + 1 ) ; ::_thesis: verum
end;

theorem Th9: :: NAT_1:9
for i, j being Nat st i <= j & j <= i + 1 & not i = j holds
j = i + 1
proof
let i, j be Nat; ::_thesis: ( i <= j & j <= i + 1 & not i = j implies j = i + 1 )
assume that
A1: i <= j and
A2: j <= i + 1 ; ::_thesis: ( i = j or j = i + 1 )
 ( j <= i or j = i + 1 ) by A2, Th8;
hence  ( i = j or j = i + 1 ) by A1, XXREAL_0:1; ::_thesis: verum
end;

theorem Th10: :: NAT_1:10
for i, j being Nat st i <= j holds
ex k being Nat st j = i + k
proof
let i, j be Nat; ::_thesis: ( i <= j implies ex k being Nat st j = i + k )
defpred S1[ Nat] means ( i <= $1 implies ex k being Nat st $1 = i + k );
A1: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; ::_thesis: ( S1[j] implies S1[j + 1] )
assume A2: ( i <= j implies ex k being Nat st j = i + k ) ; ::_thesis: S1[j + 1]
A3: now__::_thesis:_(_i_<=_j_implies_S1[j_+_1]_)
assume  i <= j ; ::_thesis: S1[j + 1]
then consider k being Nat such that
A4: j = i + k by A2;
 (i + k) + 1 = i + (k + 1) ;
hence  S1[j + 1] by A4; ::_thesis: verum
end;
A5: now__::_thesis:_(_i_=_j_+_1_implies_S1[j_+_1]_)
assume  i = j + 1 ; ::_thesis: S1[j + 1]
then  j + 1 = i + 0 ;
hence  S1[j + 1] ; ::_thesis: verum
end;
assume  i <= j + 1 ; ::_thesis: ex k being Nat st j + 1 = i + k
hence  ex k being Nat st j + 1 = i + k by A3, A5, Th8; ::_thesis: verum
end;
A6: S1[ 0 ]
proof
assume A7: i <= 0 ; ::_thesis: ex k being Nat st 0 = i + k
take  0 ; ::_thesis: 0 = i + 0
thus  0 = i + 0 by A7, Th2; ::_thesis: verum
end;
 for j being Nat holds S1[j] from NAT_1:sch_2(A6, A1);
hence  ( i <= j implies ex k being Nat st j = i + k ) ; ::_thesis: verum
end;

theorem Th11: :: NAT_1:11
for i, j being Nat holds i <= i + j
proof
let i, j be Nat; ::_thesis: i <= i + j
 ( 0 + i = i & 0 <= j ) by Th2;
hence  i <= i + j by XREAL_1:7; ::_thesis: verum
end;

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]
proof
let k be Nat; ::_thesis: P1[k]
defpred S1[ Nat] means  for n being Nat st n < $1 holds
P1[n];
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: for n being Nat st n < k holds
P1[n] ; ::_thesis: S1[k + 1]
let n be Nat; ::_thesis: ( n < k + 1 implies P1[n] )
assume  n < k + 1 ; ::_thesis: P1[n]
then  n <= k by Th8;
then  ( n < k or ( n = k & n <= k ) ) by XXREAL_0:1;
hence  P1[n] by A1, A3; ::_thesis: verum
end;
A4: S1[ 0 ] by Th2;
 for k being Nat holds S1[k] from NAT_1:sch_2(A4, A2);
then  for n being Nat st n < k holds
P1[n] ;
hence  P1[k] by A1; ::_thesis: verum
end;

scheme :: NAT_1:sch 5
Min{ P1[ Nat] } :
 ex k being Nat st
( P1[k] & ( for n being Nat st P1[n] holds
k <= n ) )
provided
A1: ex k being Nat st P1[k]
proof
defpred S1[ Nat] means P1[$1];
assume A2: for k being Nat holds
( not P1[k] or ex n being Nat st
( P1[n] & not k <= n ) ) ; ::_thesis: contradiction
A3: for k being Nat st ( for n being Nat st n < k holds
S1[n] ) holds
S1[k]
proof
let k be Nat; ::_thesis: ( ( for n being Nat st n < k holds
S1[n] ) implies S1[k] )
assume A4: for n being Nat st n < k holds
not P1[n] ; ::_thesis: S1[k]
 ( ( for n being Nat holds
( not P1[n] or k <= n ) ) implies not P1[k] ) by A2;
hence  S1[k] by A4; ::_thesis: verum
end;
 for k being Nat holds S1[k] from NAT_1:sch_4(A3);
hence  contradiction by A1; ::_thesis: verum
end;

scheme :: NAT_1:sch 6
Max{ P1[ Nat], F1() ->  Nat } :
 ex k being Nat st
( P1[k] & ( 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]
proof
defpred S1[ Nat] means  for n being Nat st P1[n] holds
n <= $1;
A3: ex k being Nat st S1[k] by A1;
consider k being Nat such that
A4: S1[k] and
A5: for m being Nat st S1[m] holds
k <= m from NAT_1:sch_5(A3);
take  k ; ::_thesis: ( P1[k] & ( for n being Nat st P1[n] holds
n <= k ) )
thus  P1[k] ::_thesis: for n being Nat st P1[n] holds
n <= k
proof
consider n being Nat such that
A6: P1[n] by A2;
A7: n <= k by A4, A6;
assume A8: P1[k] ; ::_thesis: contradiction
then  n <> k by A6;
then  k <> 0 by A7, Th2;
then consider m being Nat such that
A9: k = m + 1 by Th6;
 for n being Nat st P1[n] holds
n <= m by A4, A8, A9, Th8;
then A10: k <= m by A5;
 ((- m) + m) + 1 = (- m) + (m + 1) ;
hence  contradiction by A9, A10, XREAL_1:6; ::_thesis: verum
end;
thus  for n being Nat st P1[n] holds
n <= k by A4; ::_thesis: verum
end;

theorem Th12: :: NAT_1:12
for i, j, h being Nat st i <= j holds
i <= j + h
proof
let i, j, h be Nat; ::_thesis: ( i <= j implies i <= j + h )
assume  i <= j ; ::_thesis: i <= j + h
then A1: i + h <= j + h by XREAL_1:7;
 0 <= h by Th2;
then  i + 0 <= i + h by XREAL_1:7;
hence  i <= j + h by A1, XXREAL_0:2; ::_thesis: verum
end;

theorem Th13: :: NAT_1:13
for i, j being Nat holds
( i < j + 1 iff i <= j )
proof
let i, j be Nat; ::_thesis: ( i < j + 1 iff i <= j )
thus  ( i < j + 1 implies i <= j ) by Th8; ::_thesis: ( i <= j implies i < j + 1 )
assume A1: i <= j ; ::_thesis: i < j + 1
A2: now__::_thesis:_not_i_=_j_+_1
A3: ( j + (- j) = 0 & (j + 1) + (- j) = 1 ) ;
assume  i = j + 1 ; ::_thesis: contradiction
hence  contradiction by A1, A3, XREAL_1:6; ::_thesis: verum
end;
 i <= j + 1 by A1, Th12;
hence  i < j + 1 by A2, XXREAL_0:1; ::_thesis: verum
end;

theorem Th14: :: NAT_1:14
for j being Nat st j < 1 holds
j = 0
proof
let j be Nat; ::_thesis: ( j < 1 implies j = 0 )
assume  j < 1 ; ::_thesis: j = 0
then  j < 0 + 1 ;
then A1: j <= 0 by Th13;
assume  j <> 0 ; ::_thesis: contradiction
hence  contradiction by A1, Th2; ::_thesis: verum
end;

theorem :: NAT_1:15
for i, j being Nat st i * j = 1 holds
i = 1
proof
let i, j be Nat; ::_thesis: ( i * j = 1 implies i = 1 )
assume A1: i * j = 1 ; ::_thesis: i = 1
then  i <> 0 ;
then consider m being Nat such that
A2: i = m + 1 by Th6;
 j <> 0 by A1;
then consider l being Nat such that
A3: j = l + 1 by Th6;
A4: (((m * l) + m) + l) + 1 = 0 + 1 by A1, A2, A3;
then  (m * l) + m = 0 ;
hence  i = 1 by A2, A4; ::_thesis: verum
end;

theorem Th16: :: NAT_1:16
for k, n being Nat st k <> 0 holds
n < n + k
proof
let k, n be Nat; ::_thesis: ( k <> 0 implies n < n + k )
assume  k <> 0 ; ::_thesis: n < n + k
then A1: n <> n + k ;
 n <= n + k by Th12;
hence  n < n + k by A1, XXREAL_0:1; ::_thesis: verum
end;

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 & P1[k] holds
ex n being Nat st
( n < k & P1[n] )
proof
consider k being Nat such that
A3: ( P1[k] & ( for n being Nat st P1[n] holds
k <= n ) ) from NAT_1:sch_5(A1);
now__::_thesis:_not_k_<>_0
assume  k <> 0 ; ::_thesis: contradiction
then  ex n being Nat st
( n < k & P1[n] ) by A2, A3;
hence  contradiction by A3; ::_thesis: verum
end;
hence  P1[ 0 ] by A3; ::_thesis: verum
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
let m be Nat; ::_thesis: ( 0 < m implies for n being Nat ex k, t being Nat st
( n = (m * k) + t & t < m ) )
defpred S1[ Nat] means  ex k, t being Nat st
( $1 = (m * k) + t & t < m );
assume A1: 0 < m ; ::_thesis: for n being Nat ex k, t being Nat st
( n = (m * k) + t & t < m )
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
given k1, t1 being Nat such that A3: n = (m * k1) + t1 and
A4: t1 < m ; ::_thesis: S1[n + 1]
A5: ( t1 + 1 < m implies ex k, t being Nat st
( n + 1 = (m * k) + t & t < m ) )
proof
assume A6: t1 + 1 < m ; ::_thesis: ex k, t being Nat st
( n + 1 = (m * k) + t & t < m )
take k = k1; ::_thesis: ex t being Nat st
( n + 1 = (m * k) + t & t < m )
take t = t1 + 1; ::_thesis: ( n + 1 = (m * k) + t & t < m )
thus  n + 1 = (m * k) + t by A3; ::_thesis: t < m
thus  t < m by A6; ::_thesis: verum
end;
A7: ( t1 + 1 = m implies ex k, t being Nat st
( n + 1 = (m * k) + t & t < m ) )
proof
assume A8: t1 + 1 = m ; ::_thesis: ex k, t being Nat st
( n + 1 = (m * k) + t & t < m )
take k = k1 + 1; ::_thesis: ex t being Nat st
( n + 1 = (m * k) + t & t < m )
take t = 0 ; ::_thesis: ( n + 1 = (m * k) + t & t < m )
thus  n + 1 = (m * k) + t by A3, A8; ::_thesis: t < m
thus  t < m by A1; ::_thesis: verum
end;
 t1 + 1 <= m by A4, Th13;
hence  S1[n + 1] by A5, A7, XXREAL_0:1; ::_thesis: verum
end;
 0 = (m * 0) + 0 ;
then A9: S1[ 0 ] by A1;
thus  for n being Nat holds S1[n] from NAT_1:sch_2(A9, A2); ::_thesis: verum
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
let n, m, k, t, k1, t1 be Nat; ::_thesis: ( n = (m * k) + t & t < m & n = (m * k1) + t1 & t1 < m implies ( k = k1 & t = t1 ) )
assume that
A1: n = (m * k) + t and
A2: t < m and
A3: n = (m * k1) + t1 and
A4: t1 < m ; ::_thesis: ( k = k1 & t = t1 )
A5: now__::_thesis:_(_k1_<=_k_implies_(_k_=_k1_&_t_=_t1_)_)
assume  k1 <= k ; ::_thesis: ( k = k1 & t = t1 )
then consider u being Nat such that
A6: k = k1 + u by Th10;
 (m * (k1 + u)) + t = (m * k1) + ((m * u) + t) ;
then A7: (m * u) + t = t1 by A1, A3, A6, XCMPLX_1:2;
now__::_thesis:_for_w_being_Nat_holds_not_u_=_w_+_1
given w being Nat such that A8: u = w + 1 ; ::_thesis: contradiction
 (m * u) + t = m + ((m * w) + t) by A8;
hence  contradiction by A4, A7, Th11; ::_thesis: verum
end;
then A9: u = 0 by Th6;
hence  k = k1 by A6; ::_thesis: t = t1
thus  t = t1 by A1, A3, A6, A9, XCMPLX_1:2; ::_thesis: verum
end;
now__::_thesis:_(_k_<=_k1_implies_(_k_=_k1_&_t_=_t1_)_)
assume  k <= k1 ; ::_thesis: ( k = k1 & t = t1 )
then consider u being Nat such that
A10: k1 = k + u by Th10;
 (m * (k + u)) + t1 = (m * k) + ((m * u) + t1) ;
then A11: (m * u) + t1 = t by A1, A3, A10, XCMPLX_1:2;
now__::_thesis:_for_w_being_Nat_holds_not_u_=_w_+_1
given w being Nat such that A12: u = w + 1 ; ::_thesis: contradiction
 (m * u) + t1 = m + ((m * w) + t1) by A12;
hence  contradiction by A2, A11, Th11; ::_thesis: verum
end;
then A13: u = 0 by Th6;
hence  k = k1 by A10; ::_thesis: t = t1
thus  t = t1 by A1, A3, A10, A13, XCMPLX_1:2; ::_thesis: verum
end;
hence  ( k = k1 & t = t1 ) by A5; ::_thesis: verum
end;

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 & b1 is ordinal )
proof
take  NAT ; ::_thesis: ( not NAT is empty & NAT is ordinal )
thus  ( not NAT is empty & NAT is ordinal ) ; ::_thesis: verum
end;
end;

theorem :: NAT_1:19
for k, n being Nat holds
( k < k + n iff 1 <= n )
proof
let k, n be Nat; ::_thesis: ( k < k + n iff 1 <= n )
thus  ( k < k + n implies 1 <= n ) ::_thesis: ( 1 <= n implies k < k + n )
proof
assume A1: k < k + n ; ::_thesis: 1 <= n
assume  not 1 <= n ; ::_thesis: contradiction
then  n = 0 by Th14;
hence  contradiction by A1; ::_thesis: verum
end;
assume  1 <= n ; ::_thesis: k < k + n
hence  k < k + n by Th16; ::_thesis: verum
end;

theorem :: NAT_1:20
for k, n being Nat st k < n holds
n - 1 is Element of NAT
proof
let k, n be Nat; ::_thesis: ( k < n implies n - 1 is Element of NAT )
assume  k < n ; ::_thesis: n - 1 is Element of NAT
then  k + 1 <= n by Th13;
then consider j being Nat such that
A1: n = (k + 1) + j by Th10;
 n - 1 = k + j by A1;
hence  n - 1 is Element of NAT by ORDINAL1:def_12; ::_thesis: verum
end;

theorem :: NAT_1:21
for k, n being Nat st k <= n holds
n - k is Element of NAT
proof
let k, n be Nat; ::_thesis: ( k <= n implies n - k is Element of NAT )
assume A1: k <= n ; ::_thesis: n - k is Element of NAT
percases ( k < n or k = n ) by A1, XXREAL_0:1;
suppose k < n ; ::_thesis: n - k is Element of NAT
then  k + 1 <= n by Th13;
then consider j being Nat such that
A2: n = (k + 1) + j by Th10;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
 n - k = 1 + j by A2;
hence  n - k is Element of NAT ; ::_thesis: verum
end;
suppose k = n ; ::_thesis: n - k is Element of NAT
then  n - k = 0 ;
hence  n - k is Element of NAT ; ::_thesis: verum
end;
end;
end;

begin

theorem Th22: :: NAT_1:22
for m, n being Nat holds
( not m < n + 1 or m < n or m = n )
proof
let m, n be Nat; ::_thesis: ( not m < n + 1 or m < n or m = n )
assume  m < n + 1 ; ::_thesis: ( m < n or m = n )
then  m <= n by Th13;
hence  ( m < n or m = n ) by XXREAL_0:1; ::_thesis: verum
end;

theorem :: NAT_1:23
for k being Nat holds
( not k < 2 or k = 0 or k = 1 )
proof
let k be Nat; ::_thesis: ( not k < 2 or k = 0 or k = 1 )
assume  k < 2 ; ::_thesis: ( k = 0 or k = 1 )
then  k < 1 + 1 ;
hence  ( k = 0 or k = 1 ) by Th14, Th22; ::_thesis: verum
end;

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
proof
take  1 ; ::_thesis: not 1 is zero
thus  not 1 is zero ; ::_thesis: verum
end;
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;

theorem :: NAT_1:24
for i, h, j being Nat st i <> 0 & h = j * i holds
j <= h
proof
let i, h, j be Nat; ::_thesis: ( i <> 0 & h = j * i implies j <= h )
assume  i <> 0 ; ::_thesis: ( not h = j * i or j <= h )
then consider k being Nat such that
A1: i = k + 1 by Th6;
assume  h = j * i ; ::_thesis: j <= h
then  h = (j * k) + (j * 1) by A1;
hence  j <= h by Th11; ::_thesis: verum
end;

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 & P1[j] holds
P1[j + 1]
proof
reconsider M = F1() as Element of NAT by ORDINAL1:def_12;
defpred S1[ Nat] means P1[F1() + $1];
A3: now__::_thesis:_for_m_being_Element_of_NAT_st_S1[m]_holds_
S1[m_+_1]
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume  S1[m] ; ::_thesis: S1[m + 1]
then  P1[(M + m) + 1] by A2, Th11;
hence  S1[m + 1] ; ::_thesis: verum
end;
let i be Nat; ::_thesis: ( F1() <= i implies P1[i] )
assume  F1() <= i ; ::_thesis: P1[i]
then consider m being Nat such that
A4: i = F1() + m by Th10;
A5: S1[ 0 ] by A1;
A6: for m being Element of NAT holds S1[m] from NAT_1:sch_1(A5, A3);
 m in NAT by ORDINAL1:def_12;
hence  P1[i] by A6, A4; ::_thesis: verum
end;

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() & ( for n being Nat st n >= F1() & n < k holds
P1[n] ) holds
P1[k]
proof
defpred S1[ Nat] means  for n being Nat st n >= F1() & n < $1 holds
P1[n];
A2: for k being Nat st k >= F1() & S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( k >= F1() & S1[k] implies S1[k + 1] )
assume  k >= F1() ; ::_thesis: ( not S1[k] or S1[k + 1] )
assume A3: for n being Nat st n >= F1() & n < k holds
P1[n] ; ::_thesis: S1[k + 1]
let n be Nat; ::_thesis: ( n >= F1() & n < k + 1 implies P1[n] )
assume that
A4: n >= F1() and
A5: n < k + 1 ; ::_thesis: P1[n]
 n <= k by A5, Th13;
then  ( n < k or n = k ) by XXREAL_0:1;
hence  P1[n] by A1, A3, A4; ::_thesis: verum
end;
let k be Nat; ::_thesis: ( k >= F1() implies P1[k] )
assume A6: k >= F1() ; ::_thesis: P1[k]
A7: S1[F1()] ;
 for k being Nat st k >= F1() holds
S1[k] from NAT_1:sch_8(A7, A2);
then  for n being Nat st n >= F1() & n < k holds
P1[n] by A6;
hence  P1[k] by A1, A6; ::_thesis: verum
end;

theorem Th25: :: NAT_1:25
for n being Nat holds
( not n <= 1 or n = 0 or n = 1 )
proof
let n be Nat; ::_thesis: ( not n <= 1 or n = 0 or n = 1 )
assume A1: n <= 1 ; ::_thesis: ( n = 0 or n = 1 )
assume that
A2: not n = 0 and
A3: not n = 1 ; ::_thesis: contradiction
 n < 0 + 1 by A1, A3, XXREAL_0:1;
hence  contradiction by A2, Th13; ::_thesis: verum
end;

theorem Th26: :: NAT_1:26
for n being Nat holds
( not n <= 2 or n = 0 or n = 1 or n = 2 )
proof
let n be Nat; ::_thesis: ( not n <= 2 or n = 0 or n = 1 or n = 2 )
assume  n <= 2 ; ::_thesis: ( n = 0 or n = 1 or n = 2 )
then  n <= 1 + 1 ;
hence  ( n = 0 or n = 1 or n = 2 ) by Th8, Th25; ::_thesis: verum
end;

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 )
proof
let n be Nat; ::_thesis: ( not n <= 3 or n = 0 or n = 1 or n = 2 or n = 3 )
assume  n <= 3 ; ::_thesis: ( n = 0 or n = 1 or n = 2 or n = 3 )
then  n <= 2 + 1 ;
hence  ( n = 0 or n = 1 or n = 2 or n = 3 ) by Th8, Th26; ::_thesis: verum
end;

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 )
proof
let n be Nat; ::_thesis: ( not n <= 4 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 )
assume  n <= 4 ; ::_thesis: ( n = 0 or n = 1 or n = 2 or n = 3 or n = 4 )
then  n <= 3 + 1 ;
hence  ( n = 0 or n = 1 or n = 2 or n = 3 or n = 4 ) by Th8, Th27; ::_thesis: verum
end;

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 )
proof
let n be Nat; ::_thesis: ( not n <= 5 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 )
assume  n <= 5 ; ::_thesis: ( n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 )
then  n <= 4 + 1 ;
hence  ( n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by Th8, Th28; ::_thesis: verum
end;

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 )
proof
let n be Nat; ::_thesis: ( not n <= 6 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 )
assume  n <= 6 ; ::_thesis: ( n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 )
then  n <= 5 + 1 ;
hence  ( n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 ) by Th8, Th29; ::_thesis: verum
end;

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 )
proof
let n be Nat; ::_thesis: ( 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 )
assume  n <= 7 ; ::_thesis: ( n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 or n = 7 )
then  n <= 6 + 1 ;
hence  ( n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 or n = 7 ) by Th8, Th30; ::_thesis: verum
end;

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 )
proof
let n be Nat; ::_thesis: ( 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 )
assume  n <= 8 ; ::_thesis: ( 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 )
then  n <= 7 + 1 ;
hence  ( 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 ) by Th8, Th31; ::_thesis: verum
end;

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 )
proof
let n be Nat; ::_thesis: ( 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 )
assume  n <= 9 ; ::_thesis: ( 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 )
then  n <= 8 + 1 ;
hence  ( 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 ) by Th8, Th32; ::_thesis: verum
end;

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 )
proof
let n be Nat; ::_thesis: ( 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 )
assume  n <= 10 ; ::_thesis: ( 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 )
then  n <= 9 + 1 ;
hence  ( 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 ) by Th8, Th33; ::_thesis: verum
end;

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 )
proof
let n be Nat; ::_thesis: ( 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 )
assume  n <= 11 ; ::_thesis: ( 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 )
then  n <= 10 + 1 ;
hence  ( 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 ) by Th8, Th34; ::_thesis: verum
end;

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 )
proof
let n be Nat; ::_thesis: ( 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 )
assume  n <= 12 ; ::_thesis: ( 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 )
then  n <= 11 + 1 ;
hence  ( 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 ) by Th8, Th35; ::_thesis: verum
end;

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 )
proof
let n be Nat; ::_thesis: ( 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 )
assume  n <= 13 ; ::_thesis: ( 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 )
then  n <= 12 + 1 ;
hence  ( 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 ) by Th8, Th36; ::_thesis: verum
end;

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]
proof
defpred S1[ Nat] means ( not $1 is empty implies P1[$1] );
A3: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_(_not_k_+_1_is_empty_implies_S1[k_+_1]_)
assume  not k + 1 is empty ; ::_thesis: S1[k + 1]
 ( k is empty or not k is empty ) ;
hence  S1[k + 1] by A1, A2, A4; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
A5: S1[ 0 ] ;
 for k being Nat holds S1[k] from NAT_1:sch_2(A5, A3);
hence  for k being non empty Nat holds P1[k] ; ::_thesis: verum
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 b1 being Element of NAT st
( b1 in A & ( for k being Nat st k in A holds
b1 <= k ) ) ) & ( A is not non empty Subset of NAT implies ex b1 being Element of NAT st b1 = 0 ) )
proof
 ( A is non empty Subset of NAT implies ex i being Nat st
( i in A & ( for k being Nat st k in A holds
i <= k ) ) )
proof
defpred S1[ Nat] means $1 in A;
set x = the Element of A;
assume A1: A is non empty Subset of NAT ; ::_thesis: ex i being Nat st
( i in A & ( for k being Nat st k in A holds
i <= k ) )
then  the Element of A is Element of NAT by TARSKI:def_3;
then A2: ex k being Nat st S1[k] by A1;
 ex k being Nat st
( S1[k] & ( for i being Nat st S1[i] holds
k <= i ) ) from NAT_1:sch_5(A2);
hence  ex i being Nat st
( i in A & ( for k being Nat st k in A holds
i <= k ) ) ; ::_thesis: verum
end;
hence  ( ( A is non empty Subset of NAT implies ex b1 being Element of NAT st
( b1 in A & ( for k being Nat st k in A holds
b1 <= k ) ) ) & ( A is not non empty Subset of NAT implies ex b1 being Element of NAT st b1 = 0 ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of NAT holds
( ( A is non empty Subset of NAT & b1 in A & ( for k being Nat st k in A holds
b1 <= k ) & b2 in A & ( for k being Nat st k in A holds
b2 <= k ) implies b1 = b2 ) & ( A is not non empty Subset of NAT & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof
let i, n be Element of NAT ; ::_thesis: ( ( A is non empty Subset of NAT & i in A & ( for k being Nat st k in A holds
i <= k ) & n in A & ( for k being Nat st k in A holds
n <= k ) implies i = n ) & ( A is not non empty Subset of NAT & i = 0 & n = 0 implies i = n ) )
 ( A is non empty Subset of NAT & i in A & ( for k being Nat st k in A holds
i <= k ) & n in A & ( for k being Nat st k in A holds
n <= k ) implies i = n )
proof
assume that
 A is non empty Subset of NAT and
A3: ( i in A & ( for k being Nat st k in A holds
i <= k ) & n in A & ( for k being Nat st k in A holds
n <= k ) ) ; ::_thesis: i = n
 ( i <= n & n <= i ) by A3;
hence  i = n by XXREAL_0:1; ::_thesis: verum
end;
hence  ( ( A is non empty Subset of NAT & i in A & ( for k being Nat st k in A holds
i <= k ) & n in A & ( for k being Nat st k in A holds
n <= k ) implies i = n ) & ( A is not non empty Subset of NAT & i = 0 & n = 0 implies i = n ) ) ; ::_thesis: verum
end;
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 & ( for k being Nat st k in A holds
b2 <= k ) ) ) ) & ( 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
proof
let n be Nat; ::_thesis: succ n = n + 1
A1: n + 1 =  {  L where L is Element of NAT : L < n + 1  }  by AXIOMS:4;
A2: n =  {  K where K is Element of NAT : K < n  }  by AXIOMS:4;
thus  succ n c= n + 1 :: according to XBOOLE_0:def_10 ::_thesis: n + 1 c= succ n
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in succ n or x in n + 1 )
assume A3: x in succ n ; ::_thesis: x in n + 1
percases ( x in n or x = n ) by A3, ORDINAL1:8;
suppose x in n ; ::_thesis: x in n + 1
then consider K being Element of NAT  such that
A4: x = K and
A5: K < n by A2;
 K < n + 1 by A5, Th13;
hence  x in n + 1 by A1, A4; ::_thesis: verum
end;
supposeA6: x = n ; ::_thesis: x in n + 1
reconsider n = n as Element of NAT by ORDINAL1:def_12;
 n < n + 1 by Th13;
hence  x in n + 1 by A1, A6; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in n + 1 or x in succ n )
assume  x in n + 1 ; ::_thesis: x in succ n
then consider K being Element of NAT  such that
A7: x = K and
A8: K < n + 1 by A1;
 K <= n by A8, Th13;
then  ( K = n or K < n ) by XXREAL_0:1;
then  ( x = n or x in n ) by A2, A7;
hence  x in succ n by ORDINAL1:8; ::_thesis: verum
end;

theorem Th39: :: NAT_1:39
for n, m being Nat holds
( n <= m iff n c= m )
proof
let n, m be Nat; ::_thesis: ( n <= m iff n c= m )
defpred S1[ Nat] means  for m being Nat holds
( $1 <= m iff $1 c= m );
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
let m be Nat; ::_thesis: ( n + 1 <= m iff n + 1 c= m )
thus  ( n + 1 <= m implies n + 1 c= m ) ::_thesis: ( n + 1 c= m implies n + 1 <= m )
proof
assume  n + 1 <= m ; ::_thesis: n + 1 c= m
then consider k being Nat such that
A3: m = (n + 1) + k by Th10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 n <= n + k by Th11;
then  n c= n + k by A2;
then A4: succ n c= succ (n + k) by ORDINAL2:1;
 (n + k) + 1 = succ (n + k) by Th38;
hence  n + 1 c= m by A3, A4, Th38; ::_thesis: verum
end;
assume A5: n + 1 c= m ; ::_thesis: n + 1 <= m
 n + 1 = succ n by Th38;
then A6: n in m by A5, ORDINAL1:21;
then  n c= m by ORDINAL1:def_2;
then A7: n <= m by A2;
 n <> m by A6;
then  n < m by A7, XXREAL_0:1;
hence  n + 1 <= m by Th13; ::_thesis: verum
end;
A8: S1[ 0 ] ;
 for n being Nat holds S1[n] from NAT_1:sch_2(A8, A1);
hence  ( n <= m iff n c= m ) ; ::_thesis: verum
end;

theorem Th40: :: NAT_1:40
for n, m being Nat holds
( card n c= card m iff n <= m )
proof
let n, m be Nat; ::_thesis: ( card n c= card m iff n <= m )
reconsider n = n, m = m as Element of NAT by ORDINAL1:def_12;
 ( card n = n & card m = m ) by CARD_1:def_2;
hence  ( card n c= card m iff n <= m ) by Th39; ::_thesis: verum
end;

theorem Th41: :: NAT_1:41
for n, m being Nat holds
( card n in card m iff n < m )
proof
let n, m be Nat; ::_thesis: ( card n in card m iff n < m )
A1: ( ( n <= m & n <> m ) iff n < m ) by XXREAL_0:1;
 ( card n c< card m iff ( card n c= card m & card n <> card m ) ) by XBOOLE_0:def_8;
hence  ( card n in card m iff n < m ) by A1, Th40, ORDINAL1:11, ORDINAL1:def_2; ::_thesis: verum
end;


theorem :: NAT_1:42
for n being Nat holds nextcard (card n) = card (n + 1)
proof
let n be Nat; ::_thesis: nextcard (card n) = card (n + 1)
reconsider n = n as Element of NAT by ORDINAL1:def_12;
A1: for M being Cardinal st card (card n) in M holds
card (n + 1) c= M
proof
A2: card n = n by CARD_1:def_2;
let M be Cardinal; ::_thesis: ( card (card n) in M implies card (n + 1) c= M )
assume  card (card n) in M ; ::_thesis: card (n + 1) c= M
then A3: succ n c= M by A2, ORDINAL1:21;
 n + 1 = succ n by Th38;
hence  card (n + 1) c= M by A3, CARD_1:def_2; ::_thesis: verum
end;
 n < n + 1 by Th13;
then  card (card n) in card (n + 1) by Th41;
hence  nextcard (card n) = card (n + 1) by A1, CARD_1:def_3; ::_thesis: verum
end;

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
proof
let X, Y be finite set ; ::_thesis: ( X c= Y implies card X <= card Y )
assume  X c= Y ; ::_thesis: card X <= card Y
then  card X c= card Y by CARD_1:11;
hence  card X <= card Y by Th39; ::_thesis: verum
end;

theorem :: NAT_1:44
for k, n being Nat holds
( k in n iff k < n )
proof
let k, n be Nat; ::_thesis: ( k in n iff k < n )
hereby  ::_thesis: ( k < n implies k in n )
assume  k in n ; ::_thesis: k < n
then  k in  {  l where l is Element of NAT : l < n  }  by AXIOMS:4;
then  ex l being Element of NAT st
( k = l & l < n ) ;
hence  k < n ; ::_thesis: verum
end;
assume A1: k < n ; ::_thesis: k in n
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 k in  {  l where l is Element of NAT : l < n  }  by A1;
hence  k in n by AXIOMS:4; ::_thesis: verum
end;

theorem :: NAT_1:45
for n being Nat holds n in n + 1
proof
let n be Nat; ::_thesis: n in n + 1
reconsider n = n as Element of NAT by ORDINAL1:def_12;
 n < n + 1 by XREAL_1:29;
then  n in  {  l where l is Element of NAT : l < n + 1  }  ;
hence  n in n + 1 by AXIOMS:4; ::_thesis: verum
end;

theorem :: NAT_1:46
for k, n being Nat st k <= n holds
k = k /\ n
proof
let k, n be Nat; ::_thesis: ( k <= n implies k = k /\ n )
assume  k <= n ; ::_thesis: k = k /\ n
then  Segm k c= Segm n by Th39;
hence  k = k /\ n by XBOOLE_1:28; ::_thesis: verum
end;

scheme :: NAT_1:sch 11
LambdaRecEx{ F1() ->  set , F2( set , set ) ->  set } :
 ex f being Function st
( dom f = NAT & f . 0 = F1() & ( for n being Nat holds f . (n + 1) = F2(n,(f . n)) ) )
proof
deffunc H1( set , set ) ->  set = {} ;
consider L being T-Sequence such that
A1: dom L = NAT and
A2: ( {} in NAT implies L . {} = F1() ) and
A3: for A being Ordinal st succ A in NAT holds
L . (succ A) = F2(A,(L . A)) and
 for A being Ordinal st A in NAT & A <> {} & A is limit_ordinal holds
L . A = H1(A,L | A) from ORDINAL2:sch_5();
take  L ; ::_thesis: ( dom L = NAT & L . 0 = F1() & ( for n being Nat holds L . (n + 1) = F2(n,(L . n)) ) )
thus  dom L = NAT by A1; ::_thesis: ( L . 0 = F1() & ( for n being Nat holds L . (n + 1) = F2(n,(L . n)) ) )
thus  L . 0 = F1() by A2; ::_thesis: for n being Nat holds L . (n + 1) = F2(n,(L . n))
let n be Nat; ::_thesis: L . (n + 1) = F2(n,(L . n))
 succ n in NAT ;
hence  L . (n + 1) = F2(n,(L . n)) by A3; ::_thesis: verum
end;

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() & ( for n being Nat holds f . (n + 1) = F3(n,(f . n)) ) )
proof
consider f being Function such that
A1: dom f = NAT and
A2: f . 0 = F2() and
A3: for n being Nat holds f . (n + 1) = F3(n,(f . n)) from NAT_1:sch_11();
 for x being set st x in NAT holds
f . x in F1()
proof
let x be set ; ::_thesis: ( x in NAT implies f . x in F1() )
assume  x in NAT ; ::_thesis: f . x in F1()
then reconsider n = x as Nat ;
percases ( n = 0 or ex k being Nat st n = k + 1 ) by Th6;
suppose n = 0 ; ::_thesis: f . x in F1()
hence  f . x in F1() by A2; ::_thesis: verum
end;
suppose ex k being Nat st n = k + 1 ; ::_thesis: f . x in F1()
then consider k being Nat such that
A4: n = k + 1 ;
 f . n = F3(k,(f . k)) by A3, A4;
hence  f . x in F1() ; ::_thesis: verum
end;
end;
end;
then reconsider f = f as Function of NAT,F1() by A1, FUNCT_2:3;
take  f ; ::_thesis: ( f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F3(n,(f . n)) ) )
thus  ( f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F3(n,(f . n)) ) ) by A2, A3; ::_thesis: verum
end;

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] & P1[n,x,y2] holds
y1 = y2
proof
defpred S1[ Nat] means F2() . $1 = F3() . $1;
A8: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  F2() . n = F3() . n ; ::_thesis: S1[n + 1]
then A9: P1[n,F2() . n,F3() . (n + 1)] by A6;
 P1[n,F2() . n,F2() . (n + 1)] by A3;
hence  S1[n + 1] by A7, A9; ::_thesis: verum
end;
A10: S1[ 0 ] by A2, A5;
 for n being Nat holds S1[n] from NAT_1:sch_2(A10, A8);
then  for x being set st x in NAT holds
F2() . x = F3() . x ;
hence  F2() = F3() by A1, A4, FUNCT_1:2; ::_thesis: verum
end;

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] & P1[n,x,y2] holds
y1 = y2
proof
defpred S1[ Nat] means F3() . $1 <> F4() . $1;
A6: ( dom F3() = NAT & dom F4() = NAT ) by FUNCT_2:def_1;
assume  F3() <> F4() ; ::_thesis: contradiction
then  ex x being set st
( x in NAT & F3() . x <> F4() . x ) by A6, FUNCT_1:2;
then A7: ex k being Nat st S1[k] ;
consider m being Nat such that
A8: ( S1[m] & ( for n being Nat st S1[n] holds
m <= n ) ) from NAT_1:sch_5(A7);
now__::_thesis:_not_m_<>_0
assume  m <> 0 ; ::_thesis: contradiction
then consider k being Nat such that
A9: m = k + 1 by Th6;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 k < m by A9, Th13;
then A10: F3() . k = F4() . k by A8;
 ( P1[k,F3() . k,F3() . (k + 1)] & P1[k,F4() . k,F4() . (k + 1)] ) by A2, A4;
hence  contradiction by A5, A8, A9, A10; ::_thesis: verum
end;
hence  contradiction by A1, A3, A8; ::_thesis: verum
end;

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))
proof
defpred S1[ Nat, set , set ] means $3 = F2($1,$2);
A7: for n being Nat holds S1[n,F4() . n,F4() . (n + 1)] by A6;
A8: for n being Nat
for x, y1, y2 being set st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2 ;
A9: for n being Nat holds S1[n,F3() . n,F3() . (n + 1)] by A3;
thus  F3() = F4() from NAT_1:sch_13(A1, A2, A9, A4, A5, A7, A8); ::_thesis: verum
end;

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))
proof
defpred S1[ Nat, set , set ] means $3 = F3($1,$2);
A5: for n being Nat holds S1[n,F5() . n,F5() . (n + 1)] by A4;
A6: for n being Nat
for x, y1, y2 being Element of F1() st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2 ;
A7: for n being Nat holds S1[n,F4() . n,F4() . (n + 1)] by A2;
thus  F4() = F5() from NAT_1:sch_14(A1, A7, A3, A5, A6); ::_thesis: verum
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;

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 & ( 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 )
proof
defpred S1[ Nat] means F1($1) = 0 ;
defpred S2[ Nat] means  ex n being Nat st $1 = F1(n);
A2: for k being Nat st k <> 0 & S2[k] holds
ex m being Nat st
( m < k & S2[m] )
proof
let k be Nat; ::_thesis: ( k <> 0 & S2[k] implies ex m being Nat st
( m < k & S2[m] ) )
assume that
A3: k <> 0 and
A4: S2[k] ; ::_thesis: ex m being Nat st
( m < k & S2[m] )
consider n being Nat such that
A5: k = F1(n) by A4;
take  F1((n + 1)) ; ::_thesis: ( F1((n + 1)) < k & S2[F1((n + 1))] )
thus  ( F1((n + 1)) < k & S2[F1((n + 1))] ) by A1, A3, A5; ::_thesis: verum
end;
 F1(0) is Nat ;
then A6: ex k being Nat st S2[k] ;
 S2[ 0 ] from NAT_1:sch_7(A6, A2);
then A7: ex k being Nat st S1[k] ;
consider k being Nat such that
A8: ( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) from NAT_1:sch_5(A7);
take  k ; ::_thesis: ( F1(k) = 0 & ( for n being Nat st F1(n) = 0 holds
k <= n ) )
thus  ( F1(k) = 0 & ( for n being Nat st F1(n) = 0 holds
k <= n ) ) by A8; ::_thesis: verum
end;

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
proof
reconsider n = n as Element of NAT by ORDINAL1:def_12;
 f . n is Element of D ;
hence  f . n is Element of D ; ::_thesis: verum
end;
end;

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

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)
proof
defpred S1[ set , set ] means  ex n being Element of NAT st
( n = $1 & $2 = s . (n + k) );
A1: for i being set st i in NAT holds
ex j being set st S1[i,j]
proof
let i be set ; ::_thesis: ( i in NAT implies ex j being set st S1[i,j] )
assume  i in NAT ; ::_thesis: ex j being set st S1[i,j]
then reconsider n = i as Element of NAT ;
take j = s . (n + k); ::_thesis: S1[i,j]
thus  S1[i,j] ; ::_thesis: verum
end;
consider f being ManySortedSet of NAT  such that
A2: for i being set st i in NAT holds
S1[i,f . i] from PBOOLE:sch_3(A1);
take  f ; ::_thesis: for n being Nat holds f . n = s . (n + k)
let n be Nat; ::_thesis: f . n = s . (n + k)
 n in NAT by ORDINAL1:def_12;
then  S1[n,f . n] by A2;
hence  f . n = s . (n + k) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedSet of NAT st ( for n being Nat holds b1 . n = s . (n + k) ) & ( for n being Nat holds b2 . n = s . (n + k) ) holds
b1 = b2
proof
let s1, s2 be ManySortedSet of NAT ; ::_thesis: ( ( for n being Nat holds s1 . n = s . (n + k) ) & ( for n being Nat holds s2 . n = s . (n + k) ) implies s1 = s2 )
assume that
A3: for n being Nat holds s1 . n = s . (n + k) and
A4: for n being Nat holds s2 . n = s . (n + k) ; ::_thesis: s1 = s2
now__::_thesis:_for_n_being_set_st_n_in_NAT_holds_
s1_._n_=_s2_._n
let n be set ; ::_thesis: ( n in NAT implies s1 . n = s2 . n )
assume  n in NAT ; ::_thesis: s1 . n = s2 . n
then reconsider nn = n as Element of NAT ;
thus s1 . n = s . (nn + k) by A3
.= s2 . n by A4 ; ::_thesis: verum
end;
hence  s1 = s2 by PBOOLE:3; ::_thesis: verum
end;
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
proof
let s be ManySortedSet of NAT ; ::_thesis: for k being Nat holds rng (s ^\ k) c= rng s
let k be Nat; ::_thesis: rng (s ^\ k) c= rng s
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in rng (s ^\ k) or i in rng s )
assume  i in rng (s ^\ k) ; ::_thesis: i in rng s
then consider u being set  such that
A1: u in dom (s ^\ k) and
A2: i = (s ^\ k) . u by FUNCT_1:def_3;
reconsider n = u as Element of NAT by A1, PARTFUN1:def_2;
A3: dom s = NAT by PARTFUN1:def_2;
 i = s . (n + k) by A2, Def3;
hence  i in rng s by A3, FUNCT_1:3; ::_thesis: verum
end;

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
proof
A1: rng (s ^\ k) c= rng s by Lm1;
 rng s c= X by RELAT_1:def_19;
hence  rng (s ^\ k) c= X by A1, XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum
end;
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
proof
 ( rng (s ^\ k) c= X & dom (s ^\ k) = NAT ) by PARTFUN1:def_2, RELAT_1:def_19;
hence  s ^\ k is sequence of X by RELSET_1:4; ::_thesis: verum
end;
end;


theorem :: NAT_1:47
for X being non empty set
for s being sequence of X holds s ^\ 0 = s
proof
let X be non empty set ; ::_thesis: for s being sequence of X holds s ^\ 0 = s
let s be sequence of X; ::_thesis: s ^\ 0 = s
now__::_thesis:_for_n_being_Element_of_NAT_holds_(s_^\_0)_._n_=_s_._n
let n be Element of NAT ; ::_thesis: (s ^\ 0) . n = s . n
thus (s ^\ 0) . n = s . (n + 0) by Def3
.= s . n ; ::_thesis: verum
end;
hence  s ^\ 0 = s by FUNCT_2:63; ::_thesis: verum
end;

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)
proof
let X be non empty set ; ::_thesis: for s being sequence of X
for k, m being Nat holds (s ^\ k) ^\ m = s ^\ (k + m)
let s be sequence of X; ::_thesis: for k, m being Nat holds (s ^\ k) ^\ m = s ^\ (k + m)
let k, m be Nat; ::_thesis: (s ^\ k) ^\ m = s ^\ (k + m)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((s_^\_k)_^\_m)_._n_=_(s_^\_(k_+_m))_._n
let n be Element of NAT ; ::_thesis: ((s ^\ k) ^\ m) . n = (s ^\ (k + m)) . n
thus ((s ^\ k) ^\ m) . n = (s ^\ k) . (n + m) by Def3
.= s . ((n + m) + k) by Def3
.= s . (n + (k + m))
.= (s ^\ (k + m)) . n by Def3 ; ::_thesis: verum
end;
hence  (s ^\ k) ^\ m = s ^\ (k + m) by FUNCT_2:63; ::_thesis: verum
end;

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
proof
let X be non empty set ; ::_thesis: for s being sequence of X
for k, m being Nat holds (s ^\ k) ^\ m = (s ^\ m) ^\ k
let s be sequence of X; ::_thesis: for k, m being Nat holds (s ^\ k) ^\ m = (s ^\ m) ^\ k
let k, m be Nat; ::_thesis: (s ^\ k) ^\ m = (s ^\ m) ^\ k
thus (s ^\ k) ^\ m = s ^\ (k + m) by Th48
.= (s ^\ m) ^\ k by Th48 ; ::_thesis: verum
end;

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 & s * N is NAT -defined & 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;

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)
proof
let X be non empty set ; ::_thesis: for s being sequence of X
for k being Nat
for N being sequence of NAT holds (s * N) ^\ k = s * (N ^\ k)
let s be sequence of X; ::_thesis: for k being Nat
for N being sequence of NAT holds (s * N) ^\ k = s * (N ^\ k)
let k be Nat; ::_thesis: for N being sequence of NAT holds (s * N) ^\ k = s * (N ^\ k)
let N be sequence of NAT; ::_thesis: (s * N) ^\ k = s * (N ^\ k)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((s_*_N)_^\_k)_._n_=_(s_*_(N_^\_k))_._n
let n be Element of NAT ; ::_thesis: ((s * N) ^\ k) . n = (s * (N ^\ k)) . n
thus ((s * N) ^\ k) . n = (s * N) . (n + k) by Def3
.= s . (N . (n + k)) by FUNCT_2:15
.= s . ((N ^\ k) . n) by Def3
.= (s * (N ^\ k)) . n by FUNCT_2:15 ; ::_thesis: verum
end;
hence  (s * N) ^\ k = s * (N ^\ k) by FUNCT_2:63; ::_thesis: verum
end;

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
proof
let n be Nat; ::_thesis: for X being non empty set
for s being sequence of X holds s . n in rng s
let X be non empty set ; ::_thesis: for s being sequence of X holds s . n in rng s
let s be sequence of X; ::_thesis: s . n in rng s
 n in NAT by ORDINAL1:def_12;
then  n in dom s by FUNCT_2:def_1;
hence  s . n in rng s by FUNCT_1:3; ::_thesis: verum
end;

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
proof
let Y be set ; ::_thesis: 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
let X be non empty set ; ::_thesis: for s being sequence of X st ( for n being Nat holds s . n in Y ) holds
rng s c= Y
let s be sequence of X; ::_thesis: ( ( for n being Nat holds s . n in Y ) implies rng s c= Y )
assume A1: for n being Nat holds s . n in Y ; ::_thesis: rng s c= Y
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng s or y in Y )
assume  y in rng s ; ::_thesis: y in Y
then consider x being set  such that
A2: x in dom s and
A3: y = s . x by FUNCT_1:def_3;
 x in NAT by A2, FUNCT_2:def_1;
hence  y in Y by A1, A3; ::_thesis: verum
end;

theorem :: NAT_1:53
for n being Nat holds
( n is zero or n = 1 or n > 1 )
proof
let n be Nat; ::_thesis: ( n is zero or n = 1 or n > 1 )
assume  not n is zero ; ::_thesis: ( n = 1 or n > 1 )
then  0 + 1 <= n by Th13;
hence  ( n = 1 or n > 1 ) by XXREAL_0:1; ::_thesis: verum
end;

theorem :: NAT_1:54
for n being Nat holds succ n =  {  l where l is Element of NAT : l <= n  }
proof
let n be Nat; ::_thesis: succ n =  {  l where l is Element of NAT : l <= n  }
defpred S1[ Nat] means $1 <= n;
defpred S2[ Nat] means $1 < n + 1;
deffunc H1( Nat) ->  Nat = $1;
A1: for l being Element of NAT holds
( S2[l] iff S1[l] ) by Th13;
thus  succ n = n + 1
.=  {  H1(l) where l is Element of NAT : S2[l]  }  by AXIOMS:4
.=  {  H1(l) where l is Element of NAT : S1[l]  }  from FRAENKEL:sch_3(A1) ; ::_thesis: verum
end;

scheme :: NAT_1:sch 18
MinPred{ F1( Element of NAT ) ->  Element of NAT , P1[ set ] } :
 ex k being Element of NAT st
( P1[k] & ( 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] )
proof
now__::_thesis:_ex_k_being_Nat_st_P1[k]
consider f being Function of NAT,NAT such that
A2: for k being Element of NAT holds f . k = F1(k) from FUNCT_2:sch_4();
A3: f . 0 in rng f by FUNCT_2:4;
 rng f c= NAT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in NAT )
assume  x in rng f ; ::_thesis: x in NAT
then consider y being set  such that
A4: ( y in dom f & x = f . y ) by FUNCT_1:def_3;
reconsider y1 = y as Element of NAT by A4, FUNCT_2:def_1;
 x = F1(y1) by A4, A2;
hence  x in NAT ; ::_thesis: verum
end;
then reconsider rf = rng f as non empty Subset of NAT by A3;
set m = min* rf;
 min* rf in rf by Def1;
then consider x being set  such that
A5: x in dom f and
A6: min* rf = f . x by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A5, FUNCT_2:def_1;
 ( f . x = F1(x) & f . (x + 1) = F1((x + 1)) ) by A2;
then A7: ( f . (x + 1) < f . x or P1[x] ) by A1;
assume A8: for k being Nat holds P1[k] ; ::_thesis: contradiction
 f . (x + 1) in rf by FUNCT_2:4;
hence  contradiction by Def1, A8, A6, A7; ::_thesis: verum
end;
then A9: ex k being Nat st P1[k] ;
consider k being Nat such that
A10: P1[k] and
A11: for n being Nat st P1[n] holds
k <= n from NAT_1:sch_5(A9);
 ( k in NAT & ( for n being Element of NAT st P1[n] holds
k <= n ) ) by A11, ORDINAL1:def_12;
hence  ex k being Element of NAT st
( P1[k] & ( for n being Element of NAT st P1[n] holds
k <= n ) ) by A10; ::_thesis: verum
end;

registration
let k be Ordinal;
let x be set ;
clusterk --> x ->  T-Sequence-like ;
coherence
 k --> x is T-Sequence-like
proof
 dom (k --> x) = k by FUNCOP_1:13;
hence  k --> x is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum
end;
end;

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

theorem Th56: :: NAT_1:56
for n being Nat
for m being Nat st n <= m & m <= n + 2 & not m = n & not m = n + 1 holds
m = n + 2
proof
let n be Nat; ::_thesis: for m being Nat st n <= m & m <= n + 2 & not m = n & not m = n + 1 holds
m = n + 2
let m be Nat; ::_thesis: ( n <= m & m <= n + 2 & not m = n & not m = n + 1 implies m = n + 2 )
assume that
A1: n <= m and
A2: m <= n + 2 ; ::_thesis: ( m = n or m = n + 1 or m = n + 2 )
percases ( m <= n + 1 or m > n + 1 ) ;
suppose m <= n + 1 ; ::_thesis: ( m = n or m = n + 1 or m = n + 2 )
hence  ( m = n or m = n + 1 or m = n + 2 ) by A1, Th9; ::_thesis: verum
end;
suppose m > n + 1 ; ::_thesis: ( m = n or m = n + 1 or m = n + 2 )
then  ( m = n + 1 or m = (n + 1) + 1 ) by A2, Th9;
hence  ( m = n or m = n + 1 or m = n + 2 ) ; ::_thesis: verum
end;
end;
end;

theorem Th57: :: NAT_1:57
for n being Nat
for m being Nat st n <= m & m <= n + 3 & not m = n & not m = n + 1 & not m = n + 2 holds
m = n + 3
proof
let n be Nat; ::_thesis: for m being Nat st n <= m & m <= n + 3 & not m = n & not m = n + 1 & not m = n + 2 holds
m = n + 3
let m be Nat; ::_thesis: ( n <= m & m <= n + 3 & not m = n & not m = n + 1 & not m = n + 2 implies m = n + 3 )
assume that
A1: n <= m and
A2: m <= n + 3 ; ::_thesis: ( m = n or m = n + 1 or m = n + 2 or m = n + 3 )
percases ( m <= n + 2 or m > n + 2 ) ;
suppose m <= n + 2 ; ::_thesis: ( m = n or m = n + 1 or m = n + 2 or m = n + 3 )
hence  ( m = n or m = n + 1 or m = n + 2 or m = n + 3 ) by A1, Th56; ::_thesis: verum
end;
suppose m > n + 2 ; ::_thesis: ( m = n or m = n + 1 or m = n + 2 or m = n + 3 )
then  ( m = n + 2 or m = (n + 2) + 1 ) by A2, Th9;
hence  ( m = n or m = n + 1 or m = n + 2 or m = n + 3 ) ; ::_thesis: verum
end;
end;
end;

theorem :: NAT_1:58
for n being Nat
for m being Nat st n <= m & m <= n + 4 & not m = n & not m = n + 1 & not m = n + 2 & not m = n + 3 holds
m = n + 4
proof
let n be Nat; ::_thesis: for m being Nat st n <= m & m <= n + 4 & not m = n & not m = n + 1 & not m = n + 2 & not m = n + 3 holds
m = n + 4
let m be Nat; ::_thesis: ( n <= m & m <= n + 4 & not m = n & not m = n + 1 & not m = n + 2 & not m = n + 3 implies m = n + 4 )
assume that
A1: n <= m and
A2: m <= n + 4 ; ::_thesis: ( m = n or m = n + 1 or m = n + 2 or m = n + 3 or m = n + 4 )
percases ( m <= n + 3 or m > n + 3 ) ;
suppose m <= n + 3 ; ::_thesis: ( m = n or m = n + 1 or m = n + 2 or m = n + 3 or m = n + 4 )
hence  ( m = n or m = n + 1 or m = n + 2 or m = n + 3 or m = n + 4 ) by A1, Th57; ::_thesis: verum
end;
suppose m > n + 3 ; ::_thesis: ( m = n or m = n + 1 or m = n + 2 or m = n + 3 or m = n + 4 )
then  ( m = n + 3 or m = (n + 3) + 1 ) by A2, Th9;
hence  ( m = n or m = n + 1 or m = n + 2 or m = n + 3 or m = n + 4 ) ; ::_thesis: verum
end;
end;
end;

theorem :: NAT_1:59
for X being finite set st 1 < card X holds
ex x1, x2 being set st
( x1 in X & x2 in X & x1 <> x2 )
proof
let X be finite set ; ::_thesis: ( 1 < card X implies ex x1, x2 being set st
( x1 in X & x2 in X & x1 <> x2 ) )
set x1 = choose X;
assume A1: 1 < card X ; ::_thesis: ex x1, x2 being set st
( x1 in X & x2 in X & x1 <> x2 )
then  X <> {} ;
then A2: choose X in X ;
now__::_thesis:_ex_x2_being_set_st_
(_x2_in_X_&_not_x2_=_choose_X_)
assume A3: for x2 being set st x2 in X holds
x2 = choose X ; ::_thesis: contradiction
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_X_implies_x_in_{(choose_X)}_)_&_(_x_in_{(choose_X)}_implies_x_in_X_)_)
let x be set ; ::_thesis: ( ( x in X implies x in {(choose X)} ) & ( x in {(choose X)} implies x in X ) )
hereby  ::_thesis: ( x in {(choose X)} implies x in X )
assume  x in X ; ::_thesis: x in {(choose X)}
then  x = choose X by A3;
hence  x in {(choose X)} by TARSKI:def_1; ::_thesis: verum
end;
assume  x in {(choose X)} ; ::_thesis: x in X
hence  x in X by A2, TARSKI:def_1; ::_thesis: verum
end;
then  X = {(choose X)} by TARSKI:1;
hence  contradiction by A1, CARD_1:30; ::_thesis: verum
end;
hence  ex x1, x2 being set st
( x1 in X & x2 in X & x1 <> x2 ) ; ::_thesis: verum
end;

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 )
proof
let n be Nat; ::_thesis: ( 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 )
assume  n <= 14 ; ::_thesis: ( 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 )
then  n <= 13 + 1 ;
hence  ( 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 ) by Th8, Th37; ::_thesis: verum
end;