:: The Fundamental Properties of Natural Numbers
:: by Grzegorz Bancerek
::
:: Copyright (c) 1990-2021 Association of Mizar Users

registration
existence
ex b1 being object st b1 is natural
proof end;
end;

:: 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
proof end;

:: The Nats are real numbers therefore some theorems of real
:: numbers are translated for Nats.
registration
let n, k be natural Number ;
cluster n + k -> natural ;
coherence
n + k is natural
proof end;
end;

definition
let n be natural Number ;
let k be Element of NAT ;
:: original: +
redefine func n + k -> Element of NAT ;
coherence
n + k is Element of NAT
by ORDINAL1:def 12;
end;

canceled;

::$CS :: The Principle of Mathematical Induction 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 end; :: Like addition, the result of multiplication of two Nats is a Nat. registration let n, k be natural Number ; cluster n * k -> natural ; coherence n * k is natural proof end; end; definition let n, k be Element of NAT ; :: original: * redefine func n * 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 natural Number holds 0 <= i proof end; theorem :: NAT_1:3 for i being natural Number st 0 <> i holds 0 < i by Th2; theorem :: NAT_1:4 for i, j, h being natural Number st i <= j holds i * h <= j * h proof end; theorem :: NAT_1:5 for i being natural Number holds 0 < i + 1 proof end; theorem Th6: :: NAT_1:6 for i being natural Number holds ( i = 0 or ex k being Nat st i = k + 1 ) proof end; theorem Th7: :: NAT_1:7 for i, j being natural Number st i + j = 0 holds ( i = 0 & j = 0 ) proof end; registration existence ex b1 being object st ( b1 is zero & b1 is natural ) proof end; cluster natural non zero for object ; existence ex b1 being object st ( not b1 is zero & b1 is natural ) proof end; end; registration let m be natural Number ; let n be natural non zero Number ; cluster m + n -> non zero ; coherence not m + n is zero by Th7; cluster n + m -> non zero ; coherence not n + m is zero ; 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 end; theorem Th8: :: NAT_1:8 for i, j being natural Number holds ( not i <= j + 1 or i <= j or i = j + 1 ) proof end; theorem :: NAT_1:9 for i, j being natural Number st i <= j & j <= i + 1 & not i = j holds j = i + 1 proof end; theorem Th10: :: NAT_1:10 for i, j being natural Number st i <= j holds ex k being Nat st j = i + k proof end; theorem Th11: :: NAT_1:11 for i, j being natural Number holds i <= i + j proof 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 end; :: Principle of minimum 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 end; :: Principle of maximum 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 end; theorem Th12: :: NAT_1:12 for i, j, h being natural Number st i <= j holds i <= j + h proof end; theorem Th13: :: NAT_1:13 for i, j being natural Number holds ( i < j + 1 iff i <= j ) proof end; theorem Th14: :: NAT_1:14 for i being natural Number st i < 1 holds i = 0 proof end; theorem :: NAT_1:15 for i, j being natural Number st i * j = 1 holds i = 1 proof end; theorem Th16: :: NAT_1:16 for n, k being natural Number st k <> 0 holds n < n + k proof 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 end; :: 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 & t < m ) proof end; theorem :: NAT_1:18 for n, m, k, t, k1, t1 being natural Number st n = (m * k) + t & t < m & n = (m * k1) + t1 & t1 < m holds ( k = k1 & t = t1 ) proof end; registration coherence for b1 being natural Number holds b1 is ordinal proof end; end; registration cluster non empty ordinal for Element of bool REAL; existence ex b1 being Subset of REAL st ( not b1 is empty & b1 is ordinal ) by NUMBERS:19; end; theorem :: NAT_1:19 for k, n being natural Number holds ( k < k + n iff 1 <= n ) proof end; theorem :: NAT_1:20 for k, n being natural Number st k < n holds n - 1 is Element of NAT proof end; theorem :: NAT_1:21 for k, n being natural Number st k <= n holds n - k is Element of NAT proof end; :: from ALGSEQ_1 theorem Th22: :: NAT_1:22 for m, n being natural Number holds ( not m < n + 1 or m < n or m = n ) proof end; theorem :: NAT_1:23 for k being natural Number holds ( not k < 2 or k = 0 or k = 1 ) proof end; registration existence not for b1 being Element of NAT holds b1 is zero proof 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 -> natural non negative for object ; coherence for b1 being natural Number holds not b1 is negative by Th2; end; :: from JORDAN4 theorem :: NAT_1:24 for i, j, h being natural Number st i <> 0 & h = j * i holds j <= h proof end; :: from BINOM, 2006.05.28, A.T. 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 end; :: from INT_2, 2006.05.30, AG 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 end; :: Moved from CQC_THE1 on 07.07.2006 by AK theorem :: NAT_1:25 for n being natural Number holds ( not n <= 1 or n = 0 or n = 1 ) proof end; scheme :: NAT_1:sch 10 Indfrom1{ P1[ Nat] } : for k being non zero Nat holds P1[k] provided A1: P1[1] and A2: for k being non zero Nat st P1[k] holds P1[k + 1] proof end; :: 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 & ( 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 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 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 ) ) ); :: from CARD_1, 2007.10.28,A.T. theorem :: NAT_1:26 canceled; :: from CARD_1, 2007.10.28,A.T. theorem :: NAT_1:27 canceled; :: from CARD_1, 2007.10.28,A.T. theorem :: NAT_1:28 canceled; :: from CARD_1, 2007.10.28,A.T. theorem :: NAT_1:29 canceled; :: from CARD_1, 2007.10.28,A.T. theorem :: NAT_1:30 canceled; :: from CARD_1, 2007.10.28,A.T. theorem :: NAT_1:31 canceled; :: from CARD_1, 2007.10.28,A.T. theorem :: NAT_1:32 canceled; :: from CARD_1, 2007.10.28,A.T. theorem :: NAT_1:33 canceled; :: from CARD_1, 2007.10.28,A.T. theorem :: NAT_1:34 canceled; :: from CARD_1, 2007.10.28,A.T. theorem :: NAT_1:35 canceled; :: from CARD_1, 2007.10.28,A.T. theorem :: NAT_1:36 canceled; :: from CARD_1, 2007.10.28,A.T. theorem :: NAT_1:37 canceled; ::$CT 12
theorem Th26: :: NAT_1:38
for n being Nat holds succ (Segm n) = Segm (n + 1)
proof end;

theorem Th27: :: NAT_1:39
for m, n being Nat holds
( n <= m iff Segm n c= Segm m )
proof end;

theorem :: NAT_1:40
for m, n being Nat holds
( card (Segm n) c= card (Segm m) iff n <= m ) by Th27;

theorem Th29: :: NAT_1:41
for m, n being Nat holds
( card (Segm n) in card (Segm m) iff n < m )
proof end;

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

canceled;

::$CD theorem :: NAT_1:43 for X, Y being finite set st X c= Y holds card X <= card Y proof end; theorem Th32: :: NAT_1:44 for k, n being natural Number holds ( k in Segm n iff k < n ) proof end; theorem :: NAT_1:45 for n being natural Number holds n in Segm (n + 1) proof end; theorem :: NAT_1:46 canceled; ::$CT
:: from MODELC_2, 2008.08.18, A.T.
definition
let X be set ;
mode sequence of X is Function of NAT,X;
end;

:: from RECDEF_1, 2008.02.21, A.T.
scheme :: NAT_1:sch 11
LambdaRecEx{ F1() -> object , F2( object , object ) -> object } :
ex f being Function st
( dom f = NAT & f . 0 = F1() & ( for n being Nat holds f . (n + 1) = F2(n,(f . n)) ) )
proof end;

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

scheme :: NAT_1:sch 13
RecUn{ F1() -> object , F2() -> Function, F3() -> Function, P1[ object , object , object ] } :
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 end;

scheme :: NAT_1:sch 14
RecUnD{ F1() -> non empty set , F2() -> Element of F1(), P1[ object , object , object ], F3() -> sequence of F1(), F4() -> sequence of 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 end;

scheme :: NAT_1:sch 15
LambdaRecUn{ F1() -> object , F2( object , object ) -> object , 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 end;

scheme :: NAT_1:sch 16
LambdaRecUnD{ F1() -> non empty set , F2() -> Element of F1(), F3( object , object ) -> Element of F1(), F4() -> sequence of F1(), F5() -> sequence of 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 end;

:: missing, 2008.02.22, A.T.
registration
let x, y be natural Number ;
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;

:: from SCMFSA_9, 2008.02.25, A.T.
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 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 natural Number ;
func s ^\ k -> ManySortedSet of NAT means :Def2: :: NAT_1:def 2
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 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 end;
end;

:: deftheorem Def2 defines ^\ NAT_1:def 2 :
for s being ManySortedSet of NAT
for k being natural Number
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 natural Number holds rng (s ^\ k) c= rng s

proof end;

registration
let X be non empty set ;
let s be X -valued ManySortedSet of NAT ;
let k be natural Number ;
cluster s ^\ k -> X -valued ;
coherence
s ^\ k is X -valued
proof end;
end;

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

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

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

theorem :: NAT_1:49
for k, m being Nat
for X being non empty set
for s being sequence of X holds (s ^\ k) ^\ m = (s ^\ m) ^\ k
proof end;

registration
let N be sequence of NAT;
let X be non empty set ;
let s be sequence of X;
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;
cluster N * s -> total ;
coherence
s * N is total
;
end;

theorem :: NAT_1:50
for k being Nat
for X being non empty set
for s being sequence of X
for N being sequence of NAT holds (s * N) ^\ k = s * (N ^\ k)
proof 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 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 end;

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

theorem :: NAT_1:54
for n being Nat holds succ (Segm n) = { l where l is Nat : l <= n }
proof end;

registration
let n be natural Number ;
reduce In (n,NAT) to n;
reducibility
In (n,NAT) = n
by ;
end;

scheme :: NAT_1:sch 18
MinPred{ F1( Nat) -> Nat, P1[ object ] } :
ex k being Nat st
( P1[k] & ( for n being Nat st P1[n] holds
k <= n ) )
provided
A1: for k being Nat holds
( F1((k + 1)) < F1(k) or P1[k] )
proof end;

registration
let k be Ordinal;
let x be object ;
coherence
k --> x is Sequence-like
by FUNCOP_1:13;
end;

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

theorem :: NAT_1:56
canceled;

theorem :: NAT_1:57
canceled;

theorem :: NAT_1:58
canceled;

:: from GLIB_002, 2011.07.30, A.T.
::\$CT 3
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 end;

theorem :: NAT_1:60
for k, n being Nat st k <= n holds
not not k = 0 & ... & not k = n
proof end;

theorem :: NAT_1:61
for n being Nat
for x being object st x in Segm (n + 1) holds
not not x = 0 & ... & not x = n
proof end;

theorem :: NAT_1:62
for k, m, i being Nat st m <= i & i <= m + k holds
not not i = m + 0 & ... & not i = m + k
proof end;

definition
let D be set ;
let s be sequence of D;
let n be natural Number ;
:: original: .
redefine func s . n -> Element of D;
coherence
s . n is Element of D
proof end;
end;

registration
coherence
for b1 being natural Number st b1 is zero holds
not b1 is positive
;
end;

registration
let A be non zero object ;
coherence by TARSKI:def 1;
let B be non zero object ;
coherence by TARSKI:def 2;
let C be non zero object ;
cluster {A,B,C} -> with_non-empty_elements ;
coherence
{A,B,C} is with_non-empty_elements
by ENUMSET1:def 1;
let D be non zero object ;
cluster {A,B,C,D} -> with_non-empty_elements ;
coherence
{A,B,C,D} is with_non-empty_elements
by ENUMSET1:def 2;
let E be non zero object ;
cluster {A,B,C,D,E} -> with_non-empty_elements ;
coherence
{A,B,C,D,E} is with_non-empty_elements
by ENUMSET1:def 3;
let F be non zero object ;
cluster {A,B,C,D,E,F} -> with_non-empty_elements ;
coherence
{A,B,C,D,E,F} is with_non-empty_elements
by ENUMSET1:def 4;
let G be non zero object ;
cluster {A,B,C,D,E,F,G} -> with_non-empty_elements ;
coherence
{A,B,C,D,E,F,G} is with_non-empty_elements
by ENUMSET1:def 5;
let H be non zero object ;
cluster {A,B,C,D,E,F,G,H} -> with_non-empty_elements ;
coherence
{A,B,C,D,E,F,G,H} is with_non-empty_elements
by ENUMSET1:def 6;
let I be non zero object ;
cluster {A,B,C,D,E,F,G,H,I} -> with_non-empty_elements ;
coherence
{A,B,C,D,E,F,G,H,I} is with_non-empty_elements
by ENUMSET1:def 7;
let J be non zero object ;
cluster {A,B,C,D,E,F,G,H,I,J} -> with_non-empty_elements ;
coherence
{A,B,C,D,E,F,G,H,I,J} is with_non-empty_elements
by ENUMSET1:def 8;
end;

registration
cluster empty -> zero for set ;
coherence
for b1 being set st b1 is empty holds
b1 is zero
;
cluster non zero -> non empty for set ;
coherence
for b1 being set st not b1 is zero holds
not b1 is empty
;
end;

definition
let G be non empty set ;
let B be Function of [:G,NAT:],G;
let g be Element of G;
let i be Nat;
:: original: .
redefine func B . (g,i) -> Element of G;
coherence
B . (g,i) is Element of G
proof end;
end;

definition
let G be non empty set ;
let B be Function of [:NAT,G:],G;
let i be Nat;
let g be Element of G;
:: original: .
redefine func B . (i,g) -> Element of G;
coherence
B . (i,g) is Element of G
proof end;
end;

scheme :: NAT_1:sch 19
SeqEx2D{ F1() -> non empty set , F2() -> non empty set , P1[ set , set , set ] } :
ex f being Function of [:F1(),NAT:],F2() st
for x being Element of F1()
for y being Nat holds P1[x,y,f . (x,y)]
provided
A1: for x being Element of F1()
for y being Nat ex z being Element of F2() st P1[x,y,z]
proof end;

theorem :: NAT_1:63
for n being Nat holds Segm n c= Segm (n + 1) by ;