:: The Fundamental Properties of Natural Numbers
:: by Grzegorz Bancerek
::
:: Received January 11, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ORDINAL1, REAL_1, SUBSET_1, CARD_1, ARYTM_3, TARSKI,
RELAT_1, XXREAL_0, XCMPLX_0, ARYTM_1, XBOOLE_0, FINSET_1, FUNCT_1, NAT_1,
FUNCOP_1, PBOOLE, PARTFUN1, FUNCT_7, SETFAM_1, ZFMISC_1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1,
FINSET_1, CARD_1, PBOOLE, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, RELAT_1,
FUNCT_1, PARTFUN1, FUNCOP_1, FUNCT_2, BINOP_1;
constructors NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, CARD_1, WELLORD2, FUNCT_2,
PARTFUN1, FUNCOP_1, FUNCT_4, ENUMSET1, RELSET_1, PBOOLE, ORDINAL1,
SETFAM_1, ZFMISC_1, BINOP_1;
registrations SUBSET_1, ORDINAL1, XXREAL_0, XREAL_0, CARD_1, RELSET_1,
FUNCT_2, PBOOLE;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin
registration
cluster natural for object;
end;
reserve x for Real,
p,k,l,m,n,s,h,i,j,k1,t,t1 for Nat,
X for Subset of REAL;
:: The results of axioms of Nats
theorem :: NAT_1:1
for X st 0 in X & for x st x in X holds x + 1 in X for n holds n in X;
:: Addition and multiplication
:: 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;
end;
definition
let n be natural Number, k be Element of NAT;
redefine func n + k -> Element of NAT;
end;
::$CS
::$N The Principle of Mathematical Induction
scheme :: NAT_1:sch 2
NatInd { P[Nat] } : for k being Nat holds P[k]
provided
P[0] and
for k be Nat st P[k] holds P[k + 1];
:: Like addition, the result of multiplication of two Nats is a Nat.
registration
let n,k be natural Number;
cluster n * k -> natural;
end;
definition
let n, k be Element of NAT;
redefine func n * k -> Element of NAT;
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 :: NAT_1:2
for i being natural Number holds 0 <= i;
theorem :: NAT_1:3
for i being natural Number holds 0 <> i implies 0 < i;
theorem :: NAT_1:4
for i,j,h being natural Number holds i <= j implies i * h <= j * h;
theorem :: NAT_1:5
for i being natural Number holds 0 < i + 1;
theorem :: NAT_1:6
for i being natural Number holds i = 0 or ex k st i = k + 1;
theorem :: NAT_1:7
for i,j being natural Number holds i + j = 0 implies i = 0 & j = 0;
registration
cluster zero natural for object;
cluster non zero natural for object;
end;
registration
let m be natural Number, n be non zero natural Number;
cluster m + n -> non zero;
cluster n + m -> non zero;
end;
scheme :: NAT_1:sch 3
DefbyInd { N()->Nat, F(Nat,Nat)->Nat, P[Nat,Nat] } : (for k being Nat ex n
being Nat st P[k,n]) & for k,n,m being Nat st P[k,n] & P[k,m] holds n = m
provided
for k,n being Nat holds P[k,n] iff k = 0 & n = N() or ex m,l being
Nat st k = m + 1 & P[m,l] & n = F(k,l);
theorem :: NAT_1:8
for i,j being natural Number holds i <= j + 1 implies i <= j or i = j + 1;
theorem :: NAT_1:9
for i,j being natural Number holds
i <= j & j <= i + 1 implies i = j or j = i + 1;
theorem :: NAT_1:10
for i,j being natural Number holds
i <= j implies ex k st j = i + k;
theorem :: NAT_1:11
for i,j being natural Number holds i <= i + j;
scheme :: NAT_1:sch 4
CompInd { P[Nat] } : for k being Nat holds P[k]
provided
for k being Nat st for n being Nat st n < k holds P[n] holds P[k];
:: Principle of minimum
scheme :: NAT_1:sch 5
Min { P[Nat] } : ex k being Nat st P[k] & for n being Nat st P[n] holds k <= n
provided
ex k being Nat st P[k];
:: Principle of maximum
scheme :: NAT_1:sch 6
Max { P[Nat], N()->Nat } : ex k being Nat st P[k] & for n being Nat st P[n]
holds n <= k
provided
for k being Nat st P[k] holds k <= N() and
ex k being Nat st P[k];
theorem :: NAT_1:12
for i,j,h being natural Number holds i <= j implies i <= j + h;
theorem :: NAT_1:13
for i,j being natural Number holds i < j + 1 iff i <= j;
theorem :: NAT_1:14
for i being natural Number holds i < 1 implies i = 0;
theorem :: NAT_1:15
for i,j being natural Number holds i * j = 1 implies i = 1;
theorem :: NAT_1:16
for n,k being natural Number holds k <> 0 implies n < n + k;
scheme :: NAT_1:sch 7
Regr { P[Nat] } : P[0]
provided
ex k being Nat st P[k] and
for k being Nat st k <> 0 & P[k] ex n being Nat st n < k & P[n];
:: Exact division and rest of division
theorem :: NAT_1:17
0 < m implies for n ex k,t st n = (m*k)+t & t < m;
theorem :: NAT_1:18
for n,m,k,t,k1,t1 being natural Number holds
n = m*k+t & t < m & n = m*k1+t1 & t1 < m implies k = k1 & t = t1;
registration
cluster -> ordinal for natural Number;
end;
registration
cluster non empty ordinal for Subset of REAL;
end;
theorem :: NAT_1:19
for k,n being natural Number holds k < k + n iff 1 <= n;
theorem :: NAT_1:20
for k,n being natural Number holds k < n implies n - 1 is Element of NAT;
theorem :: NAT_1:21
for k,n being natural Number holds k <= n implies n - k is Element of NAT;
begin :: Addenda
:: from ALGSEQ_1
theorem :: NAT_1:22
for m,n being natural Number holds m < n+1 implies m < n or m = n;
theorem :: NAT_1:23
for k being natural Number holds k < 2 implies k = 0 or k = 1;
registration
cluster non zero for Element of NAT;
end;
registration
cluster -> non negative for Element of NAT;
end;
registration
cluster -> non negative for natural Number;
end;
:: from JORDAN4
theorem :: NAT_1:24
for i,j,h being natural Number holds i <> 0 & h = j*i implies j <= h;
:: from BINOM, 2006.05.28, A.T.
scheme :: NAT_1:sch 8
Ind1{M() -> Nat, P[Nat]} : for i being Nat st M() <= i holds P[i]
provided
P[M()] and
for j being Nat st M() <= j holds P[j] implies P[j+1];
:: from INT_2, 2006.05.30, AG
scheme :: NAT_1:sch 9
CompInd1 { a() -> Nat, P[Nat] } : for k being Nat st k >= a() holds P[k]
provided
for k being Nat st k>=a() & (for n being Nat st n>=a() & n Element of NAT means
:: NAT_1:def 1
it in A & for k st k in A holds it <= k
if A is non empty Subset of NAT otherwise it = 0;
end;
:: from CARD_1, 2007.10.28,A.T.
reserve x for object, X,Y,Z for set;
::$CT 12
theorem :: NAT_1:38
for n being Nat holds succ Segm n = Segm(n + 1);
theorem :: NAT_1:39
n <= m iff Segm n c= Segm m;
theorem :: NAT_1:40
card Segm n c= card Segm m iff n <= m;
theorem :: NAT_1:41
card Segm n in card Segm m iff n < m;
reserve M,N for Cardinal;
theorem :: NAT_1:42
nextcard card Segm n = card Segm(n+1);
::$CD
theorem :: NAT_1:43
for X,Y being finite set holds X c= Y implies card X <= card Y;
theorem :: NAT_1:44
for k,n being natural Number holds
k in Segm n iff k < n;
theorem :: NAT_1:45
for n being natural Number holds n in Segm(n+1);
::$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{A() -> object,G(object,object) -> object}:
ex f being Function st dom f = NAT & f.0 = A() &
for n being Nat holds f.(n+1) = G(n,f.n);
scheme :: NAT_1:sch 12
LambdaRecExD{D() -> non empty set, A() -> Element of D(),
G(object,object) -> Element of D()}:
ex f being sequence of D() st f.0 = A() & for n being Nat
holds f.(n+1) = G(n,f.n);
scheme :: NAT_1:sch 13
RecUn{A() -> object, F, G() -> Function, P[object,object,object]}:
F() = G()
provided
dom F() = NAT and
F().0 = A() and
for n holds P[n,F().n,F().(n+1)] and
dom G() = NAT and
G().0 = A() and
for n holds P[n,G().n,G().(n+1)] and
for n for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2;
scheme :: NAT_1:sch 14
RecUnD{D() -> non empty set,A() -> Element of D(),
P[object,object,object], F, G() -> sequence of D()} :
F() = G()
provided
F().0 = A() and
for n holds P[n,F().n,F().(n+1)] and
G().0 = A() and
for n holds P[n,G().n,G().(n+1)] and
for n being Nat,x,y1,y2 being Element of D() st P[n,x,y1] & P[n,x,y2
] holds y1=y2;
scheme :: NAT_1:sch 15
LambdaRecUn{A() -> object, RecFun(object,object) -> object,
F, G() -> Function}:
F() = G()
provided
dom F() = NAT and
F().0 = A() and
for n holds F().(n+1) = RecFun(n,F().n) and
dom G() = NAT and
G().0 = A() and
for n holds G().(n+1) = RecFun(n,G().n);
scheme :: NAT_1:sch 16
LambdaRecUnD{D() -> non empty set,A() -> Element of D(),
RecFun(object,object) -> Element of D(), F, G() -> sequence of D()}:
F() = G()
provided
F().0 = A() and
for n holds F().(n+1) = RecFun(n,F().n) and
G().0 = A() and
for n holds G().(n+1) = RecFun(n,G().n);
:: missing, 2008.02.22, A.T.
registration
let x,y be natural Number;
cluster min(x,y) -> natural;
cluster max(x,y) -> natural;
end;
definition
let x,y be Element of NAT;
redefine func min(x,y) -> Element of NAT;
redefine func max(x,y) -> Element of NAT;
end;
:: from SCMFSA_9, 2008.02.25, A.T.
scheme :: NAT_1:sch 17
MinIndex { F(Nat)->Nat} : ex k st F(k)=0 & for n st F(n)=0 holds k <= n
provided
for k holds (F(k+1) < F(k) or F(k) = 0);
:: 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, k be natural Number;
func s ^\ k -> ManySortedSet of NAT means
:: NAT_1:def 3
for n being Nat holds it.n=s.(n+k);
end;
registration
let X be non empty set, s be X-valued ManySortedSet of NAT,
k be natural Number;
cluster s ^\ k -> X-valued;
end;
definition
let X be non empty set, s be sequence of X, k be Nat;
redefine func s ^\ k -> sequence of X;
end;
reserve X for non empty set,
s for sequence of X;
theorem :: NAT_1:47
s^\0 =s;
theorem :: NAT_1:48
s ^\k^\m = s^\(k+m);
theorem :: NAT_1:49
s^\k^\m = s^\m^\k;
registration let N be sequence of NAT; let X,s;
cluster s * N -> Function-like NAT-defined X-valued;
end;
registration let N be sequence of NAT; let X,s;
cluster s * N -> total;
end;
theorem :: NAT_1:50
for N being sequence of NAT holds (s * N) ^\k = s * (N ^\k);
theorem :: NAT_1:51
s.n in rng s;
theorem :: NAT_1:52
(for n holds s.n in Y) implies rng s c= Y;
:: from UPROOTS, 2009.07.21, A.T.
theorem :: NAT_1:53
for n being natural Number holds n is non zero implies n = 1 or n > 1;
theorem :: NAT_1:54
succ Segm n = {l where l is Nat : l <= n};
registration let n be natural Number;
reduce In(n,NAT) to n;
end;
scheme :: NAT_1:sch 18
MinPred { F(Nat) -> Nat, P[object]} :
ex k be Nat st P[k] &
for n be Nat st P[n] holds k <= n
provided
for k be Nat holds F(k+1) < F(k) or P[k];
registration let k be Ordinal, x be object;
cluster k --> x -> Sequence-like;
end;
theorem :: NAT_1:55
for s be ManySortedSet of NAT, k be natural Number
holds rng(s ^\ k) c= rng s;
:: 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;
theorem :: NAT_1:60
k <= n implies k = 0 or ... or k = n;
theorem :: NAT_1:61
x in Segm(n+1) implies x = 0 or ... or x = n;
theorem :: NAT_1:62
m <= i & i <= m+k implies i = m+0 or ... or i = m+k;
definition let D be set;
let s be sequence of D, n be natural Number;
redefine func s.n -> Element of D;
end;
registration
cluster zero -> non positive for natural Number;
end;
registration
let A be non zero object;
cluster { A } -> with_non-empty_elements;
let B be non zero object;
cluster { A, B } -> with_non-empty_elements;
let C be non zero object;
cluster { A, B, C } -> with_non-empty_elements;
let D be non zero object;
cluster { A, B, C, D } -> with_non-empty_elements;
let E be non zero object;
cluster { A, B, C, D, E } -> with_non-empty_elements;
let F be non zero object;
cluster { A, B, C, D, E, F } -> with_non-empty_elements;
let G be non zero object;
cluster { A, B, C, D, E, F, G } -> with_non-empty_elements;
let H be non zero object;
cluster { A, B, C, D, E, F, G, H } -> with_non-empty_elements;
let I be non zero object;
cluster { A, B, C, D, E, F, G, H, I } -> with_non-empty_elements;
let J be non zero object;
cluster { A, B, C, D, E, F, G, H, I, J } -> with_non-empty_elements;
end;
registration
cluster empty -> zero for set;
cluster non zero -> non empty for set;
end;
definition
let G be non empty set;
let B be Function of [:G,NAT:], G;
let g be Element of G, i be Nat;
redefine func B.(g,i) -> Element of G;
end;
definition
let G be non empty set;
let B be Function of [:NAT,G:], G;
let i be Nat, g be Element of G;
redefine func B.(i,g) -> Element of G;
end;
scheme :: NAT_1:sch 19
SeqEx2D{X,Z() -> non empty set, P[set,set,set]}:
ex f being Function of [:X(),NAT:],Z()
st for x being Element of X(), y being Nat holds P[x,y,f.(x,y)]
provided
for x being Element of X(), y being Nat
ex z being Element of Z() st P[x,y,z];
theorem :: NAT_1:63
for n being Nat holds Segm n c= Segm(n+1);