:: The Fundamental Properties of Natural Numbers
:: by Grzegorz Bancerek
::
:: Received January 11, 1989
:: Copyright (c) 1990-2026 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;
definitions TARSKI, XBOOLE_0, RELAT_1;
equalities ORDINAL1, XBOOLE_0;
expansions SETFAM_1, ORDINAL1, TARSKI, XBOOLE_0;
theorems AXIOMS, ORDINAL1, XCMPLX_1, XREAL_1, XXREAL_0, TARSKI, ORDINAL2,
XBOOLE_0, CARD_1, FUNCT_2, FUNCT_1, FUNCOP_1, PBOOLE, RELSET_1, RELAT_1,
PARTFUN1, SUBSET_1, NUMBERS, ENUMSET1, XBOOLE_1;
schemes SUBSET_1, ORDINAL2, FUNCT_2, PBOOLE, BINOP_1;
begin
registration
cluster natural for object;
existence
proof
take 0;
thus thesis;
end;
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 natural numbers
theorem Th1:
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 such that
A1: 0 in A;
assume x in A implies x + 1 in A;
then NAT c= A by A1,AXIOMS:3;
hence thesis by ORDINAL1:def 12;
end;
scheme
RealInd { X() -> Subset of REAL } :
for n being Nat holds n in X()
provided
A1: 0 in X() and
A2: for x being Real st x in X() holds x + 1 in X()
proof
let n be Nat;
NAT c= X() by A1,A2,AXIOMS:3;
hence thesis by ORDINAL1:def 12;
end;
:: Addition and multiplication
:: The natural numbers are real numbers, therefore some theorems
:: of real numbers are translated for natural numbers.
registration
let n,k be natural Number;
cluster n + k -> natural;
coherence
proof
n in NAT & k in NAT by ORDINAL1:def 12;
hence thesis by AXIOMS:2;
end;
end;
definition
let n be natural Number, k be Element of NAT;
redefine func n + k -> Element of NAT; :: redefines + (XCMPLX_0, definition)
coherence by ORDINAL1:def 12;
end;
::$N The Principle of Mathematical Induction
::$L https://en.wikipedia.org/wiki/Mathematical_induction The Principle of Mathematical Induction
scheme
NatInd { P[Nat] } : for k being Nat holds P[k]
provided
A1: P[0] and
A2: for k be Nat st P[k] holds P[k + 1]
proof
let k be Nat;
consider X being Subset of NAT such that
A3: for x being Element of NAT holds x in X iff P[x] from SUBSET_1:sch 3;
A4: for x st x in X holds x + 1 in X
proof
let x;
assume x in X;
then consider k such that
A5: P[k] and
A6: k = x by A3;
P[k+1] by A2,A5;
hence thesis by A3,A6;
end;
X c= NAT & NAT c= REAL by NUMBERS:19;
then X is Subset of REAL by XBOOLE_1:1;
then k in X by A1,A3,A4,Th1;
hence thesis by A3;
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
proof
A0: k is Nat by TARSKI:1;
defpred P[Nat] means n*$1 is natural;
A1: for m be Nat holds P[m] implies P[m+1]
proof
let m be Nat;
assume P[m];
then reconsider k = n * m as Nat;
k + n is Nat;
hence thesis;
end;
A2: P[0];
for m be Nat holds P[m] from NatInd(A2,A1);
hence thesis by A0;
end;
end;
definition
let n, k be Element of NAT;
redefine func n * k -> Element of NAT; :: redefines * (XCMPLX_0, definition)
coherence by ORDINAL1:def 12;
end;
:: Order relation
:: Some theorems of "greater or equal" relation "<=" in real numbers are translated
:: to natural numbers easily and it is necessary to have them here.
theorem Th2:
for i being natural Number holds 0 <= i
proof
let i be natural Number;
A0: i is Nat by TARSKI:1;
defpred P[natural Number] means 0 <= $1;
A1: for n st P[n] holds P[n+1];
A2: P[0];
for k holds P[k] from NatInd(A2,A1);
hence thesis by A0;
end;
theorem
for i being natural Number holds 0 <> i implies 0 < i by Th2;
theorem
for i,j,h being natural Number holds i <= j implies i * h <= j * h
proof
let i,j,h be natural Number;
0 <= h by Th2;
hence thesis by XREAL_1:64;
end;
theorem
for i being natural Number holds 0 < i + 1
proof
let i be natural Number;
0 <= i by Th2;
hence thesis;
end;
theorem Th6:
for i being natural Number holds i = 0 or ex k st i = k + 1
proof
let i be natural Number;
A0: i is Nat by TARSKI:1;
defpred P[natural Number] means $1 = 0 or ex k st $1 = k + 1;
A1: P[h] implies P[h + 1];
A2: P[0];
for i holds P[i] from NatInd(A2,A1);
hence thesis by A0;
end;
theorem Th7:
for i,j being natural Number holds i + j = 0 implies i = 0 & j = 0
proof
let i,j be natural Number;
0 <= i & 0 <= j by Th2;
hence thesis;
end;
registration
cluster zero natural for object;
existence
proof
take 0;
thus thesis;
end;
cluster non zero natural for object;
existence
proof
take 1;
thus thesis;
end;
end;
registration
let m be natural Number, n be non zero natural Number;
cluster m + n -> non zero;
coherence by Th7;
cluster n + m -> non zero;
coherence;
end;
scheme
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
A1: 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)
proof
reconsider N = N() as Element of NAT by ORDINAL1:def 12;
defpred P[Nat] means ex n being Nat st P[$1,n];
A2: for k being Nat holds P[k] implies P[k+1]
proof
let k be Nat;
given n being Nat such that
A3: P[k,n];
reconsider F = F(k+1,n) as Element of NAT by ORDINAL1:def 12;
take F;
thus thesis by A1,A3;
end;
P[0,N] by A1; then
A4: P[0];
thus for k being Nat holds P[k] from NatInd(A4,A2);
defpred P[Nat] means for n,m being Nat st P[$1,n] & P[$1,m] holds n = m;
A5: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A6: for n,m being Nat st P[k,n] & P[k,m] holds n = m;
let n,m be Nat;
assume P[k+1,n] & P[k+1,m];
then (ex l,u being Nat st k + 1 = l + 1 & P[l,u] & n = F(k + 1,u) )&
ex v,w being Nat st k + 1 = v + 1 & P[v,w] & m = F(k + 1,w) by A1;
hence thesis by A6;
end;
A7: P[0]
proof
let n,m be Nat such that
A8: P[0,n] and
A9: P[0,m];
not ex m,l being Nat st 0 = m + 1 & P[m,l] & n = F(0,l);
then ( not ex n,l being Nat st 0 = n + 1 & P[n,l] & m = F(0,l))& n = N()
by A1,A8;
hence thesis by A1,A9;
end;
thus for k being Nat holds P[k] from NatInd(A7,A5);
end;
theorem Th8:
for i,j being natural Number holds i <= j + 1 implies i <= j or i = j + 1
proof
let i,j be natural Number;
A0: i is Nat & j is Nat by TARSKI:1;
defpred P[natural Number] means
for j holds $1 <= j + 1 implies $1 <= j or $1 = j+1;
A1: for i st P[i] holds P[i+1]
proof
let i such that
A2: for j holds i <= j + 1 implies i <= j or i = j + 1;
let j;
assume
A3: i + 1 <= j + 1;
A4: now
given k such that
A5: j = k + 1;
i <= k + 1 by A3,A5,XREAL_1:6;
hence thesis by A2,A5,XREAL_1:6;
end;
now
A6: 0 <= i by Th2;
assume
A7: j = 0;
then i <= 0 by A3,XREAL_1:6;
hence thesis by A7,A6;
end;
hence thesis by A4,Th6;
end;
A8: P[0] by Th2;
for i holds P[i] from NatInd(A8,A1);
hence thesis by A0;
end;
theorem
for i,j being natural Number holds
i <= j & j <= i + 1 implies i = j or j = i + 1
proof
let i,j be natural Number;
assume that
A1: i <= j and
A2: j <= i + 1;
j <= i or j = i + 1 by A2,Th8;
hence thesis by A1,XXREAL_0:1;
end;
theorem Th10:
for i,j being natural Number holds
i <= j implies ex k st j = i + k
proof
let i,j be natural Number;
A0: j is Nat by TARSKI:1;
defpred P[Nat] means i <= $1 implies ex k st $1 = i + k;
A1: for j st P[j] holds P[j+1]
proof
let j such that
A2: i <= j implies ex k st j = i + k;
A3: now
assume i <= j;
then consider k such that
A4: j = i + k by A2;
i + k + 1 = i + (k + 1);
hence thesis by A4;
end;
A5: now
assume i = j + 1;
then j + 1 = i + 0;
hence thesis;
end;
assume i <= j + 1;
hence thesis by A3,A5,Th8;
end;
A6: P[0]
proof
assume
A7: i <= 0;
take 0;
thus thesis by A7,Th2;
end;
for j holds P[j] from NatInd(A6,A1);
hence thesis by A0;
end;
theorem Th11:
for i,j being natural Number holds i <= i + j
proof
let i,j be natural Number;
0 + i = i & 0 <= j by Th2;
hence thesis by XREAL_1:7;
end;
scheme
CompInd { P[Nat] } : for k being Nat holds P[k]
provided
A1: for k being Nat st for n being Nat st n < k holds P[n] holds P[k]
proof
let k be Nat;
defpred P1[Nat] means for n being Nat st n < $1 holds P[n];
A2: for k be Nat holds P1[k] implies P1[k+1]
proof
let k be Nat;
assume
A3: for n being Nat st n < k holds P[n];
let n be Nat;
assume n < k + 1;
then n <= k by Th8;
then n < k or n = k & n <= k by XXREAL_0:1;
hence thesis by A1,A3;
end;
A4: P1[0] by Th2;
for k being Nat holds P1[k] from NatInd(A4,A2);
then for n being Nat st n < k holds P[n];
hence thesis by A1;
end;
:: Principle of minimum
scheme
Min { P[Nat] } : ex k being Nat st P[k] &
for n being Nat st P[n] holds k <= n
provided
A1: ex k being Nat st P[k]
proof
defpred P1[Nat] means not P[$1];
assume
A2: not thesis;
A3: for k being Nat st for n being Nat st n < k holds P1[n] holds P1[k]
proof
let k be Nat;
assume
A4: for n being Nat st n < k holds not P[n];
not (ex n being Nat st P[n] & not k <= n) implies not P[k] by A2;
hence thesis by A4;
end;
for k be Nat holds P1[k] from CompInd(A3);
hence contradiction by A1;
end;
:: Principle of maximum
scheme
Max { P[Nat], N()->Nat } : ex k being Nat st P[k] & for n being Nat st P[n]
holds n <= k
provided
A1: for k being Nat st P[k] holds k <= N() and
A2: ex k being Nat st P[k]
proof
defpred P1[Nat] means for n being Nat st P[n] holds n <= $1;
A3: ex k being Nat st P1[k] by A1;
consider k being Nat such that
A4: P1[k] and
A5: for m being Nat st P1[m] holds k <= m from Min(A3);
take k;
thus P[k]
proof
consider n being Nat such that
A6: P[n] by A2;
A7: n <= k by A4,A6;
assume
A8: not P[k];
then n <> k by A6;
then k <> 0 by A7,Th2;
then consider m such that
A9: k = m + 1 by Th6;
A10: for n being Nat st P[n] holds n <= m by A4,A8,A9,Th8;
-m + m + 1 = -m + (m + 1);
hence contradiction by A5,A9,A10,XREAL_1:6;
end;
thus thesis by A4;
end;
theorem Th12:
for i,j,h being natural Number holds i <= j implies i <= j + h
proof
let i,j,h be natural Number;
assume i <= j; then
A1: i + h <= j + h by XREAL_1:7;
0 <= h by Th2;
then i + 0 <= i + h by XREAL_1:7;
hence thesis by A1,XXREAL_0:2;
end;
theorem Th13:
for i,j being natural Number holds i < j + 1 iff i <= j
proof
let i,j be natural Number;
thus i < j + 1 implies i <= j by Th8;
assume
A1: i <= j;
A2: now
A3: j + (- j) = 0 & j + 1 + (- j) = 1;
assume i = j + 1;
hence contradiction by A1,A3,XREAL_1:6;
end;
i <= j + 1 by A1,Th12;
hence thesis by A2,XXREAL_0:1;
end;
theorem Th14:
for i being natural Number holds i < 1 implies i = 0
proof
let i be natural Number;
assume i < 1;
then i < 0 + 1;
then i <= 0 by Th13;
hence thesis by Th2;
end;
theorem
for i,j being natural Number holds i * j = 1 implies i = 1
proof
let i,j be natural Number;
assume
A1: i * j = 1;
then i <> 0;
then consider m such that
A2: i = m + 1 by Th6;
j <> 0 by A1;
then consider l 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 thesis by A2,A4;
end;
theorem Th16:
for n,k being natural Number holds k <> 0 implies n < n + k
proof
let n,k be natural Number;
assume k <> 0;
then
A1: n <> n + k;
n <= n + k by Th12;
hence thesis by A1,XXREAL_0:1;
end;
scheme
Regr { P[Nat] } : P[0]
provided
A1: ex k being Nat st P[k] and
A2: for k being Nat st k <> 0 & P[k] ex n being Nat st n < k & P[n]
proof
consider k being Nat such that
A3: P[k] & for n being Nat st P[n] holds k <= n from Min(A1);
now
assume k <> 0;
then ex n being Nat st n < k & P[n] by A2,A3;
hence contradiction by A3;
end;
hence thesis by A3;
end;
:: Exact division and rest of division
theorem
0 < m implies for n ex k,t st n = (m*k)+t & t < m
proof
defpred P[Nat] means ex k,t st $1 = (m*k)+t & t < m;
assume
A1: 0 < m;
A2: for n st P[n] holds P[n+1]
proof
let n;
given k1,t1 such that
A3: n = (m*k1)+t1 and
A4: t1 < m;
A5: t1+1 < m implies ex k,t st n+1 = (m*k)+t & t < m
proof
assume
A6: t1+1 < m;
take k = k1, t = t1+1;
thus n+1 = m*k+t by A3;
thus thesis by A6;
end;
A7: t1+1 = m implies ex k,t st n+1 = (m*k)+t & t < m
proof
assume
A8: t1+1 = m;
take k = k1+1, t = 0;
thus n+1 = m*k+t by A3,A8;
thus thesis by A1;
end;
t1+1 <= m by A4,Th13;
hence thesis by A5,A7,XXREAL_0:1;
end;
0 = m*0+0;
then
A9: P[0] by A1;
thus for n holds P[n] from NatInd(A9,A2);
end;
theorem
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
proof
let n,m,k,t,k1,t1 be natural Number;
assume that
A1: n = m*k+t and
A2: t < m and
A3: n = m*k1+t1 and
A4: t1 < m;
A5: now
assume k1 <= k;
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
given w being Nat such that
A8: u = w + 1;
m * u + t = m + (m * w + t) by A8;
hence contradiction by A4,A7,Th11;
end;
then
A9: u = 0 by Th6;
hence k = k1 by A6;
thus t = t1 by A1,A3,A6,A9,XCMPLX_1:2;
end;
now
assume k <= k1;
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
given w being Nat such that
A12: u = w + 1;
m * u + t1 = m + (m * w + t1) by A12;
hence contradiction by A2,A11,Th11;
end;
then
A13: u = 0 by Th6;
hence k = k1 by A10;
thus t = t1 by A1,A3,A10,A13,XCMPLX_1:2;
end;
hence thesis by A5;
end;
registration
cluster -> ordinal for natural number;
coherence;
end;
registration
cluster non empty ordinal for Subset of REAL;
existence by NUMBERS:19;
end;
theorem
for k,n being natural Number holds k < k + n iff 1 <= n
proof
let k,n be natural Number;
thus k < k + n implies 1 <= n
proof
assume
A1: k < k + n;
assume not 1 <= n;
then n = 0 by Th14;
hence thesis by A1;
end;
assume 1 <= n;
hence thesis by Th16;
end;
theorem
for k,n being natural Number holds k < n implies n - 1 is Element of NAT
proof
let k,n be natural Number;
assume k < n;
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 thesis by ORDINAL1:def 12;
end;
theorem
for k,n being natural Number holds k <= n implies n - k is Element of NAT
proof
let k,n be natural Number;
assume
A1: k <= n;
per cases by A1,XXREAL_0:1;
suppose
k < n;
then k + 1 <= n by Th13;
then consider j being Nat such that
A2: n = k + 1 + j by Th10;
reconsider j as Element of NAT by ORDINAL1:def 12;
n - k = 1 + j by A2;
hence thesis;
end;
suppose
k = n;
then n - k = 0;
hence thesis;
end;
end;
begin :: Addenda
:: from ALGSEQ_1
theorem Th22:
for m,n being natural Number st m < n+1 holds m < n or m = n
proof
let m,n be natural Number;
assume m<n+1;
then m<=n by Th13;
hence thesis by XXREAL_0:1;
end;
theorem
for k being natural Number st k < 2 holds k = 0 or k = 1
proof
let k be natural Number;
assume k<2;
then k<1+1;
hence thesis by Th14,Th22;
end;
registration
cluster non zero for Element of NAT;
existence
proof
take 1;
thus thesis;
end;
end;
registration
cluster -> non negative for Nat;
coherence by Th2;
end;
registration
cluster -> non negative for natural Number;
coherence by Th2;
end;
:: from JORDAN4
theorem
for i,j,h being natural Number st i <> 0 & h = j*i holds j <= h
proof
let i,j,h be natural Number;
assume i<>0;
then consider k such that
A1: i = k+1 by Th6;
assume h=j*i;
then h=j*k+j*1 by A1;
hence thesis by Th11;
end;
:: from BINOM, 2006.05.28, A.T.
scheme
Ind1{M() -> Nat, P[Nat]} : for i being Nat st M() <= i holds P[i]
provided
A1: P[M()] and
A2: for j being Nat st M() <= j holds P[j] implies P[j+1]
proof
defpred Q[Nat] means P[M() + $1];
A3: now
let m be Nat;
assume Q[m];
then P[M()+m+1] by A2,Th11;
hence Q[m+1];
end;
let i;
assume M() <= i;
then consider m being Nat such that
A4: i = M() + m by Th10;
A5: Q[0] by A1;
for m being Nat holds Q[m] from NatInd(A5,A3);
hence thesis by A4;
end;
:: from INT_2, 2006.05.30, AG
scheme
CompInd1 { a() -> Nat, P[Nat] } : for k being Nat st k >= a() holds P[k]
provided
A1: for k being Nat st k>=a() & (for n being Nat st n>=a() & n<k holds P
[n]) holds P[k]
proof
defpred P1[Nat] means for n being Nat st (n>=a() & n<$1) holds P[n];
A2: for k being Nat st k>=a() holds P1[k] implies P1[k+1]
proof
let k be Nat;
assume k>=a();
assume
A3: for n being Nat st n>=a() & n<k holds P[n];
let n be Nat;
assume that
A4: n>=a() and
A5: n<k+1;
n<=k by A5,Th13;
then n<k or n = k by XXREAL_0:1;
hence thesis by A1,A3,A4;
end;
let k be Nat;
assume
A6: k>=a();
A7: P1[a()];
for k being Nat st k>=a() holds P1[k] from Ind1(A7,A2);
then for n being Nat st n>=a() & n<k holds P[n] by A6;
hence thesis by A1,A6;
end;
:: Moved from CQC_THE1 on 07.07.2006 by AK
theorem
for n being natural Number holds n <= 1 implies n = 0 or n = 1
proof
let n be natural Number;
assume
A1: n <= 1;
assume that
A2: not n = 0 and
A3: not n = 1;
n < 0+1 by A1,A3,XXREAL_0:1;
hence contradiction by A2,Th13;
end;
scheme
Indfrom1 { P[Nat] } : for k being non zero Nat holds P[k]
provided
A1: P[1] and
A2: for k being non zero Nat st P[k] holds P[k + 1]
proof
defpred P[Nat] means $1 is non zero implies P[$1];
A3: now
let k be Nat;
assume
A4: P[k];
now
assume k+1 is non zero;
k = 0 or k is non zero;
hence P[k+1] by A1,A2,A4;
end;
hence P[k+1];
end;
A5: P[0];
for k being Nat holds P[k] from NatInd(A5,A3);
hence thesis;
end;
:: from HENMODEL, 2007.03.15, A.T.
definition
let A be set;
func min* A -> Element of NAT means :Def1:
it in A & for k st k in A holds it <= k
if A is non empty Subset of NAT otherwise it = 0;
existence
proof
A is non empty Subset of NAT implies ex i st i in A & for k be Nat st
k in A holds i <= k
proof
defpred P[Nat] means $1 in A;
set x = the Element of A;
assume
A1: A is non empty Subset of NAT;
then x is Element of NAT by TARSKI:def 3;
then
A2: ex k be Nat st P[k] by A1;
ex k be Nat st P[k] & for i be Nat st P[i] holds k <= i from Min( A2
);
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let i,n be Element of NAT;
A is non empty Subset of NAT & (i in A & for k st k in A holds i <= k)
& (n in A & for k 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 st k in A holds i <= k)& n in A & for k st k in
A holds n <= k;
i <= n & n <= i by A3;
hence thesis by XXREAL_0:1;
end;
hence thesis;
end;
consistency;
end;
:: from CARD_1, 2007.10.28,A.T.
reserve x for object, X,Y,Z for set;
::$CT 12
theorem Th26:
for n being Nat holds succ Segm n = Segm(n + 1)
proof
let n be Nat;
A1: n+1 = {L where L is Nat: L < n+1} by AXIOMS:4;
A2: n = {K where K is Nat: K < n} by AXIOMS:4;
thus succ Segm n c= Segm(n+1)
proof
let x be object such that
A3: x in succ Segm n;
per cases by A3,ORDINAL1:8;
suppose
x in Segm n;
then consider K being Nat such that
A4: x = K and
A5: K < n by A2;
K < n+1 by A5,Th13;
hence thesis by A1,A4;
end;
suppose
A6: x = n;
reconsider n as Element of NAT by ORDINAL1:def 12;
n < n+1 by Th13;
hence thesis by A1,A6;
end;
end;
let x be object;
assume x in Segm(n+1);
then consider K being 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 Segm n by A2,A7;
hence thesis by ORDINAL1:8;
end;
theorem Th27:
n <= m iff Segm n c= Segm m
proof
defpred P[Nat] means for m holds $1 <= m iff Segm $1 c= Segm m;
A1: for n st P[n] holds P[n+1]
proof
let n such that
A2: P[n];
let m;
thus n+1 <= m implies Segm(n+1) c= Segm m
proof
assume n+1 <= m;
then consider k being Nat such that
A3: m = n+1+k by Th10;
reconsider k as Element of NAT by ORDINAL1:def 12;
Segm n c= Segm(n+k) by A2,Th11;
then
A4: succ Segm n c= succ Segm(n+k) by ORDINAL2:1;
Segm(n+k+1) = succ Segm(n+k) by Th26;
hence thesis by A3,A4,Th26;
end;
assume
A5: Segm(n+1) c= Segm m;
Segm (n+1) = succ Segm n by Th26;
then
A6: n in Segm m by A5,ORDINAL1:21;
then
A7: n <= m by A2,ORDINAL1:def 2;
reconsider nn = n as set;
n <> m by A6;
then n < m by A7,XXREAL_0:1;
hence thesis by Th13;
end;
A8: P[0];
for n holds P[n] from NatInd(A8,A1);
hence thesis;
end;
theorem
card Segm n c= card Segm m iff n <= m by Th27;
theorem Th29:
card Segm n in card Segm m iff n < m
proof
card Segm n c< card Segm m iff
card Segm n c= card Segm m & card Segm n <> card Segm m;
hence thesis by Th27,ORDINAL1:11,def 2;
end;
reserve M,N for Cardinal;
theorem
nextcard card Segm n = card Segm(n+1)
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
A1: for M st card card n in M holds card(n+1) c= M
proof
let M;
assume
A2: card card n in M;
Segm(n+1) = succ Segm n by Th26;
hence thesis by A2,ORDINAL1:21;
end;
n < n+1 by Th13;
hence thesis by A1,Th29,CARD_1:def 3;
end;
::$CD
theorem
for X,Y being finite set st X c= Y holds card X <= card Y
proof let X,Y be finite set;
assume X c= Y;
then Segm card X c= Segm card Y by CARD_1:11;
hence card X <= card Y by Th27;
end;
theorem Th32:
for k,n being natural Number holds
k in Segm n iff k < n
proof
let k,n be natural Number;
hereby
assume k in Segm n;
then k in { l where l is Nat : l < n } by AXIOMS:4;
then ex l being Nat st k = l & l < n;
hence k < n;
end;
assume
A1: k < n;
reconsider k as Element of NAT by ORDINAL1:def 12;
k in { l where l is Nat : l < n } by A1;
hence thesis by AXIOMS:4;
end;
theorem
for n being natural Number holds n in Segm(n+1)
proof
let n be natural Number;
A1: n is Nat by TARSKI:1;
n<n+1 by XREAL_1:29;
then n in {l where l is Nat:l<n+1} by A1;
hence thesis by AXIOMS:4;
end;
::$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
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);
deffunc D(set,set) = {};
consider L being Sequence such that
A1: dom L = NAT and
A2: 0 in NAT implies L.0 = A() and
A3: for A being Ordinal st succ A in NAT holds L.(succ A) = G(A,L.A) and
for A being Ordinal st A in NAT & A <> 0 & A is limit_ordinal holds L.A
= D(A,L|A) from ORDINAL2:sch 5;
take L;
thus dom L = NAT by A1;
thus L.0 = A() by A2;
let n be Nat;
thus L.(n+1) = L.Segm(n+1)
.= L.succ Segm n by Th26
.= G(n,L.n) by A3,ORDINAL1:def 12;
end;
scheme
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) proof
consider f being Function such that
A1: dom f = NAT and
A2: f.0 = A() and
A3: for n being Nat holds f.(n+1) = G(n,f.n) from LambdaRecEx;
for x being object st x in NAT holds f.x in D()
proof
let x be object;
assume x in NAT;
then reconsider n = x as Nat;
per cases by Th6;
suppose
n = 0;
hence thesis by A2;
end;
suppose
ex k st n = k + 1;
then consider k such that
A4: n = k+1;
f.n = G(k,f.k) by A3,A4;
hence thesis;
end;
end;
then reconsider f as sequence of D() by A1,FUNCT_2:3;
take f;
thus thesis by A2,A3;
end;
scheme
RecUn{A() -> object, F, G() -> Function, P[object,object,object]}:
F() = G()
provided
A1: dom F() = NAT and
A2: F().0 = A() and
A3: for n holds P[n,F().n,F().(n+1)] and
A4: dom G() = NAT and
A5: G().0 = A() and
A6: for n holds P[n,G().n,G().(n+1)] and
A7: for n for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2
proof
defpred P[Nat] means F().$1 = G().$1;
A8: for n st P[n] holds P[n+1]
proof
let n;
assume F().n = G().n;
then
A9: P[n,F().n,G().(n+1)] by A6;
P[n,F().n,F().(n+1)] by A3;
hence thesis by A7,A9;
end;
A10: P[0] by A2,A5;
for n holds P[n] from NatInd(A10,A8);
then for x being object st x in NAT holds F().x = G().x;
hence thesis by A1,A4,FUNCT_1:2;
end;
scheme
RecUnD{D() -> non empty set,A() -> Element of D(),
P[object,object,object], F, G() -> sequence of D()} :
F() = G()
provided
A1: F().0 = A() and
A2: for n holds P[n,F().n,F().(n+1)] and
A3: G().0 = A() and
A4: for n holds P[n,G().n,G().(n+1)] and
A5: for n being Nat,x,y1,y2 being Element of D() st
P[n,x,y1] & P[n,x,y2] holds y1=y2
proof
defpred Q[Nat] means F().$1 <> G().$1;
A6: dom F() = NAT & dom G() = NAT by FUNCT_2:def 1;
assume F() <> G();
then ex x being object st x in NAT & F().x <> G().x by A6,FUNCT_1:2;
then
A7: ex k be Nat st Q[k];
consider m be Nat such that
A8: Q[m] & for n be Nat st Q[n] holds m <= n from Min(A7);
now
assume m<>0;
then consider k being Nat such that
A9: m=k+1 by Th6;
reconsider k as Element of NAT by ORDINAL1:def 12;
k < m by A9,Th13;
then
A10: F().k = G().k by A8;
P[k,F().k,F().(k+1)] & P[k,G().k,G().(k+1)] by A2,A4;
hence contradiction by A5,A8,A9,A10;
end;
hence contradiction by A1,A3,A8;
end;
scheme
LambdaRecUn{A() -> object, RecFun(object,object) -> object,
F, G() -> Function}:
F() = G()
provided
A1: dom F() = NAT and
A2: F().0 = A() and
A3: for n holds F().(n+1) = RecFun(n,F().n) and
A4: dom G() = NAT and
A5: G().0 = A() and
A6: for n holds G().(n+1) = RecFun(n,G().n)
proof
defpred P[Nat,set,set] means $3=RecFun($1,$2);
A7: for n holds P[n,G().n,G().(n+1)] by A6;
A8: for n being Nat,x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1=y2;
A9: for n holds P[n,F().n,F().(n+1)] by A3;
thus F() = G() from RecUn(A1,A2,A9,A4,A5,A7,A8);
end;
scheme
LambdaRecUnD{D() -> non empty set,A() -> Element of D(),
RecFun(object,object) -> Element of D(), F, G() -> sequence of D()}:
F() = G()
provided
A1: F().0 = A() and
A2: for n holds F().(n+1) = RecFun(n,F().n) and
A3: G().0 = A() and
A4: for n holds G().(n+1) = RecFun(n,G().n)
proof
defpred P[Nat,set,set] means $3=RecFun($1,$2);
A5: for n holds P[n,G().n,G().(n+1)] by A4;
A6: for n being Nat,x,y1,y2 being Element of D() st P[n,x,y1] & P[n,x,y2]
holds y1=y2;
A7: for n holds P[n,F().n,F().(n+1)] by A2;
thus F() = G() from RecUnD(A1,A7,A3,A5,A6);
end;
:: missing, 2008.02.22, A.T.
registration
let x,y be natural Number;
cluster min(x,y) -> natural;
coherence by XXREAL_0:15;
cluster max(x,y) -> natural;
coherence by XXREAL_0:16;
end;
definition
let x,y be Element of NAT;
redefine func min(x,y) -> Element of NAT; :: redefines min (XXREAL_0, definition)
coherence by XXREAL_0:15;
redefine func max(x,y) -> Element of NAT; :: redefines max (XXREAL_0, definition)
coherence by XXREAL_0:16;
end;
:: from SCMFSA_9, 2008.02.25, A.T.
scheme
MinIndex { F(Nat)->Nat} : ex k st F(k)=0 & for n st F(n)=0 holds k <= n
provided
A1: for k holds (F(k+1) < F(k) or F(k) = 0)
proof
defpred X[Nat] means F($1)=0;
defpred P[Nat] means ex n being Nat st $1 = F(n);
A2: for k be Nat st k <> 0 & P[k] ex m be Nat st m < k & P[m]
proof
let k be Nat;
assume that
A3: k <> 0 and
A4: P[k];
consider n being Nat such that
A5: k = F(n) by A4;
take IT=F(n + 1);
thus thesis by A1,A3,A5;
end;
F(0) is Nat;
then
A6: ex k be Nat st P[k];
P[0] from Regr(A6,A2);
then
A7: ex k be Nat st X[k];
consider k be Nat such that
A8: ( X[k])& for n be Nat st X[n] holds k <= n from Min(A7);
take k;
thus thesis by A8;
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, k be natural Number;
func s ^\ k -> ManySortedSet of NAT means
:Def2:
for n being Nat holds it.n = s.(n+k);
existence
proof
defpred P[object,object] means
ex n being Element of NAT st n=$1 & $2=s.(n+k);
A1: for i being object st i in NAT ex j being object st P[i,j]
proof let i be object;
assume
i in NAT;
then reconsider n=i as Element of NAT;
take j = s.(n+k);
thus P[i,j];
end;
consider f being ManySortedSet of NAT such that
A2: for i being object st i in NAT holds P[i,f.i] from PBOOLE:sch 3(A1);
take f;
let n be Nat;
P[n,f.n] by A2,ORDINAL1:def 12;
hence thesis;
end;
uniqueness
proof
let s1,s2 be ManySortedSet of NAT;
assume that
A3: for n holds s1.n=s.(n+k) and
A4: for n holds s2.n=s.(n+k);
now
let n be object;
assume n in NAT;
then reconsider nn = n as Element of NAT;
thus s1.n=s.(nn+k) by A3
.=s2.n by A4;
end;
hence s1=s2 by PBOOLE:3;
end;
end;
Lm1:
for s be ManySortedSet of NAT, k be natural Number
holds rng(s ^\ k) c= rng s
proof
let s be ManySortedSet of NAT, k be natural Number;
let i be object;
assume i in rng(s ^\ k);
then consider u being object 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,Def2;
hence i in rng s by A3,FUNCT_1:3,ORDINAL1:def 12;
end;
registration
let X be non empty set, s be X-valued ManySortedSet of NAT,
k be natural Number;
cluster s ^\ k -> X-valued;
coherence
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;
end;
end;
definition
let X be non empty set, s be sequence of X, k be Nat;
redefine func s ^\ k -> sequence of X; :: redefines ^\ (NAT_1, definition)
coherence
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;
end;
end;
reserve X for non empty set,
s for sequence of X;
theorem
s^\0 =s
proof
now
let n be Element of NAT;
thus (s ^\0).n=s.(n+0) by Def2
.=s.n;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th35:
s ^\k^\m = s^\(k+m)
proof
now
let n be Element of NAT;
thus (s ^\k^\m).n=(s ^\k).(n+m) by Def2
.=s.(n+m+k) by Def2
.=s.(n+(k+m))
.=(s ^\(k+m)).n by Def2;
end;
hence thesis by FUNCT_2:63;
end;
theorem
s^\k^\m = s^\m^\k
proof
thus s^\k^\m = s^\(k+m) by Th35
.= s^\m^\k by Th35;
end;
registration let N be sequence of NAT; let X,s;
cluster s * N -> Function-like NAT-defined X-valued;
coherence;
end;
registration let N be sequence of NAT; let X,s;
cluster s * N -> total;
coherence;
end;
theorem
for N being sequence of NAT holds (s * N) ^\k = s * (N ^\k)
proof
let N be sequence of NAT;
now
let n be Element of NAT;
thus ((s * N) ^\k).n = (s * N).(n + k) by Def2
.= s.(N.(n + k)) by FUNCT_2:15,ORDINAL1:def 12
.= s.((N ^\k).n) by Def2
.= (s * (N ^\k)).n by FUNCT_2:15;
end;
hence thesis by FUNCT_2:63;
end;
theorem
s.n in rng s
proof
n in NAT by ORDINAL1:def 12;
then n in dom s by FUNCT_2:def 1;
hence thesis by FUNCT_1:3;
end;
theorem
(for n holds s.n in Y) implies rng s c= Y
proof
assume
A1: for n holds s.n in Y;
let y be object;
assume y in rng s;
then consider x being object 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 thesis by A1,A3;
end;
:: from UPROOTS, 2009.07.21, A.T.
theorem
for n being natural Number holds n is non zero implies n = 1 or n > 1
proof
let n be natural Number;
assume n is non zero;
then 0+1 <= n by Th13;
hence n = 1 or n > 1 by XXREAL_0:1;
end;
theorem
succ Segm n = {l where l is Nat : l <= n}
proof
thus succ Segm n c= { k : k <= n}
proof let x be object;
assume
A1: x in succ Segm n;
then x in Segm succ Segm n;
then reconsider k = x as Nat;
x in Segm n or x in {n} by A1,XBOOLE_0:def 3;
then k < n or k = n by Th32,TARSKI:def 1;
hence thesis;
end;
let x be object;
assume x in { k : k <= n};
then consider k such that
A2: x = k and
A3: k <= n;
k < n or k = n by A3,XXREAL_0:1;
then k in Segm n or k in {n} by Th32,TARSKI:def 1;
hence thesis by A2,XBOOLE_0:def 3;
end;
registration let n be natural Number;
reduce In(n,NAT) to n;
reducibility by ORDINAL1:def 12,SUBSET_1:def 8;
end;
scheme MinPred { F(Nat) -> Nat, P[object]} :
ex k be Nat st P[k] &
for n be Nat st P[n] holds k <= n
provided
A1: for k be Nat holds F(k+1) < F(k) or P[k]
proof
now
deffunc G(Nat) = In(F($1),NAT);
consider f being sequence of NAT such that
A2: for k be Element of NAT holds f.k = G(k) from FUNCT_2:sch 4;
A3: f.0 in rng f by FUNCT_2:4;
rng f c= NAT
proof
let x be object; assume x in rng f; then
consider y being object 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 = G(y1) by A4,A2;
hence thesis;
end; then
reconsider rf = rng f as non empty Subset of NAT by A3;
set m = min* rf;
m in rf by Def1;
then consider x being object such that
A5: x in dom f and
A6: m = f.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A5,FUNCT_2:def 1;
f.x = G(x) & f.(x+1) = G(x+1) by A2; then
A7: f.(x+1) < f.x or P[x] by A1;
assume
A8: for k holds not P[k];
f.(x+1) in rf by FUNCT_2:4;
hence contradiction by Def1,A8,A6,A7;
end; then
A9: ex k be Nat st P[k];
consider k be Nat such that
A10: P[k] & for n be Nat st P[n] holds k <= n from Min(A9);
take k;
thus thesis by A10;
end;
registration let k be Ordinal, x be object;
cluster k --> x -> Sequence-like;
coherence by FUNCOP_1:13;
end;
theorem
for s be ManySortedSet of NAT, k be natural Number
holds rng(s ^\ k) c= rng s by Lm1;
:: from GLIB_002, 2011.07.30, A.T.
::$CT 3
theorem
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;
set x1 = the Element of X;
assume
A1: 1 < card X;
then X <> {};
then
A2: x1 in X;
now
assume
A3: for x2 being set st x2 in X holds x2 = x1;
now
let x be object;
hereby
assume x in X;
then x = x1 by A3;
hence x in {x1} by TARSKI:def 1;
end;
assume x in {x1};
hence x in X by A2,TARSKI:def 1;
end;
then X = {x1} by TARSKI:2;
hence contradiction by A1,CARD_1:30;
end;
hence thesis;
end;
theorem
k <= n implies k = 0 or ... or k = n
proof
thus thesis;
end;
theorem
x in Segm(n+1) implies x = 0 or ... or x = n
proof
assume
A1: x in Segm(n+1);
then reconsider k = x as Nat;
k < n+1 by A1,Th32;
then k <= n by Th13;
hence thesis;
end;
theorem
m <= i & i <= m+k implies i = m+0 or ... or i = m+k
proof assume that
A1: m <= i and
A2: i <= m+k;
take j = i;
thus thesis by A1,A2;
end;
definition let D be set;
let s be sequence of D, n be natural Number;
redefine func s.n -> Element of D; :: redefines . (FUNCT_1, definition)
coherence
proof reconsider n as Element of NAT by ORDINAL1:def 12;
s.n is Element of D;
hence thesis;
end;
end;
registration
cluster zero -> non positive for natural Number;
coherence;
end;
registration
let A be non zero object;
cluster { A } -> with_non-empty_elements;
coherence by TARSKI:def 1;
let B be non zero object;
cluster { A, B } -> with_non-empty_elements;
coherence by TARSKI:def 2;
let C be non zero object;
cluster { A, B, C } -> with_non-empty_elements;
coherence by ENUMSET1:def 1;
let D be non zero object;
cluster { A, B, C, D } -> with_non-empty_elements;
coherence by ENUMSET1:def 2;
let E be non zero object;
cluster { A, B, C, D, E } -> with_non-empty_elements;
coherence by ENUMSET1:def 3;
let F be non zero object;
cluster { A, B, C, D, E, F } -> with_non-empty_elements;
coherence by ENUMSET1:def 4;
let G be non zero object;
cluster { A, B, C, D, E, F, G } -> with_non-empty_elements;
coherence by ENUMSET1:def 5;
let H be non zero object;
cluster { A, B, C, D, E, F, G, H } -> with_non-empty_elements;
coherence 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 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 by ENUMSET1:def 8;
end;
registration
cluster empty -> zero for set;
coherence;
cluster non zero -> non empty for set;
coherence;
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; :: redefines . (BINOP_1, definition)
coherence
proof
reconsider i as Element of NAT by ORDINAL1:def 12;
B.(g,i) is Element of G;
hence thesis;
end;
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; :: redefines . (BINOP_1, definition)
coherence
proof
reconsider i as Element of NAT by ORDINAL1:def 12;
B.(i,g) is Element of G;
hence thesis;
end;
end;
scheme 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
A1: for x being Element of X(), y being Nat
ex z being Element of Z() st P[x,y,z];
A2: for x being Element of X(), y being Element of NAT
ex z being Element of Z() st P[x,y,z] by A1;
consider f being Function of [:X(),NAT:],Z() such that
A3: for x being Element of X(), y being Element of NAT holds P[x,y,f.(x,y)]
from BINOP_1:sch 3(A2);
take f;
let x be Element of X(), y be Nat;
y in NAT by ORDINAL1:def 12;
hence thesis by A3;
end;
theorem
for n being Nat holds Segm n c= Segm(n+1) by Th11,Th27;
registration
cluster positive for Nat;
existence
proof
take 1;
thus thesis;
end;
cluster non zero for Nat;
existence
proof
take 1;
thus thesis;
end;
end;