:: Natural Numbers
:: by Robert Milewski
::
:: Received February 23, 1998
:: Copyright (c) 1998-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, NAT_1, XBOOLE_0, SUBSET_1, FINSEQ_1, PARTFUN1, CARD_1,
XXREAL_0, ARYTM_3, FUNCT_1, INT_1, RELAT_1, ARYTM_1, POWER, ABIAN,
ZFMISC_1, REAL_1, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, XCMPLX_0, XREAL_0,
NUMBERS, INT_1, NAT_1, NAT_D, POWER, ABIAN, FUNCT_1, PARTFUN1, FINSEQ_1,
XXREAL_0;
constructors XXREAL_0, REAL_1, NAT_1, NAT_D, MEMBERED, SERIES_1, BINARITH,
ABIAN;
registrations RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, ABIAN, SERIES_1,
XBOOLE_0, ZFMISC_1, ORDINAL1;
requirements REAL, NUMERALS, SUBSET, ARITHM;
definitions NAT_D;
equalities ORDINAL1;
theorems AXIOMS, INT_1, NAT_1, ABIAN, POWER, FINSEQ_1, FINSEQ_4, XREAL_1,
TARSKI, XCMPLX_1, ORDINAL1, NAT_D, XXREAL_0, XREAL_0, ZFMISC_1, CARD_1;
schemes NAT_1, RECDEF_1;
begin :: Preliminaries
reserve i, j, k, l, m, n, t for Nat;
scheme
NonUniqPiFinRecExD{D() -> non empty set, A() -> Element of D(), N() -> Nat,
P[set,set,set]}: ex p be FinSequence of D() st len p = N() & (p/.1 = A() or N()
= 0) & for n be Nat st 1 <= n & n < N() holds P[n,p/.n,p/.(n+1)]
provided
A1: for n be Nat st 1 <= n & n < N() for x be Element of D() ex y be
Element of D() st P[n,x,y]
proof
consider p be FinSequence of D() such that
A2: len p = N() and
A3: p.1 = A() or N() = 0 and
A4: for n be Nat st 1 <= n & n < N() holds P[n,p.n,p.(n+1)]
from RECDEF_1:sch 4(A1);
take p;
thus len p = N() by A2;
now
assume N() <> 0;
then N() >= 0 + 1 by NAT_1:13;
hence p/.1 = A() by A2,A3,FINSEQ_4:15;
end;
hence p/.1 = A() or N() = 0;
let n be Nat;
assume that
A5: 1 <= n and
A6: n < N();
n + 1 <= N() by A6,NAT_1:13;
then
A7: p.(n+1) = p/.(n+1) by A2,FINSEQ_4:15,NAT_1:11;
n in NAT & p.n = p/.n by A2,A5,A6,FINSEQ_4:15,ORDINAL1:def 12;
hence thesis by A4,A5,A6,A7;
end;
theorem
for x,y be Real st x >= 0 & y > 0 holds x / ( [\ x / y /] + 1 ) < y
proof
let x,y be Real such that
A1: x >= 0 and
A2: y > 0;
(x / y) * y < ( [\ x / y /] + 1 ) * y by A2,INT_1:29,XREAL_1:68;
then
A3: x < ( [\ x / y /] + 1 ) * y by A2,XCMPLX_1:87;
[\ x / y /] >= 0 by A1,A2;
hence thesis by A3,XREAL_1:83;
end;
begin :: Division and Rest of Division
theorem
0 div n = 0;
theorem
for n be non zero Nat holds n div n = 1
proof
let n be non zero Nat;
n*1 div n = 1;
hence thesis;
end;
theorem
n div 1 = n
proof
n = 1 * n + 0;
thus thesis;
end;
theorem
i <= j & k <= j & i = j -' k + l implies k = j -' i + l
proof
assume that
A1: i <= j and
A2: k <= j & i = j -' k + l;
i - l = j - k by A2,XREAL_1:233;
hence k = j - i + l .= j -' i + l by A1,XREAL_1:233;
end;
theorem
i in Seg n implies n -' i + 1 in Seg n
proof
A1: 1 <= n -' i + 1 by NAT_1:11;
assume
A2: i in Seg n;
then 1 <= i by FINSEQ_1:1;
then n - i <= n - 1 by XREAL_1:13;
then
A3: n - i + 1 <= n by XREAL_1:19;
i <= n by A2,FINSEQ_1:1;
then n -' i + 1 <= n by A3,XREAL_1:233;
hence thesis by A1,FINSEQ_1:1;
end;
theorem
j < i implies i -' (j + 1) + 1 = i -' j
proof
assume
A1: j < i;
then j + 1 <= i by NAT_1:13;
hence i -' (j + 1) + 1 = i - (j + 1) + 1 by XREAL_1:233
.= i - j
.= i -' j by A1,XREAL_1:233;
end;
theorem Th8:
i >= j implies j -' i = 0
proof
assume
A1: i >= j;
per cases by A1,XXREAL_0:1;
suppose
i = j;
hence thesis by XREAL_1:232;
end;
suppose
i > j;
then j - i < 0 by XREAL_1:49;
hence thesis by XREAL_0:def 2;
end;
end;
theorem Th9:
for i,j be non zero Nat holds i -' j < i
proof
let i,j be non zero Nat;
per cases;
suppose
A1: j <= i;
i - j < i - 0 by XREAL_1:15;
hence thesis by A1,XREAL_1:233;
end;
suppose
j > i;
hence thesis by Th8;
end;
end;
theorem Th10:
k <= n implies 2 to_power n = (2 to_power k) * (2 to_power (n-'k ))
proof
assume k <= n;
then n = k + (n -' k) by XREAL_1:235;
hence thesis by POWER:27;
end;
theorem
k <= n implies 2 to_power k divides 2 to_power n
proof
assume k <= n;
then
A2: 2 to_power n = (2 to_power k) * (2 to_power (n-'k)) by Th10;
reconsider a = 2 to_power (n-'k) as Nat by TARSKI:1;
take a;
thus thesis by A2;
end;
theorem Th12:
k > 0 & n div k = 0 implies n < k
proof
assume that
A1: k > 0 and
A2: n div k = 0;
ex t be Nat st n = k * (n div k) + t & t < k by A1,NAT_D:def 1;
hence thesis by A2;
end;
theorem
k > 0 & k <= n implies n div k >= 1
proof
assume k > 0 & k <= n;
then n div k <> 0 by Th12;
then n div k >= 0 + 1 by NAT_1:13;
hence thesis;
end;
theorem
k <> 0 implies (n+k) div k = (n div k) + 1
proof
assume k <> 0;
then consider t be Nat such that
A1: n = k * (n div k) + t and
A2: t < k by NAT_D:def 1;
n + k = k * ((n div k) + 1) + t by A1;
hence thesis by A2,NAT_D:def 1;
end;
theorem
k divides n & 1 <= n & 1 <= i & i <= k implies (n -' i) div k = (n div k) - 1
proof
assume that
A1: k divides n and
A2: 1 <= n and
A3: 1 <= i and
A4: i <= k;
A5: k-'i < k by A3,A4,Th9;
A6: k <= n by A1,A2,NAT_D:7;
then i + k <= k + n by A4,XREAL_1:7;
then
A7: i <= n by XREAL_1:6;
n div k > 0
proof
assume not n div k > 0;
then n div k = 0;
hence contradiction by A3,A4,A6,Th12;
end;
then n div k >= 0 + 1 by NAT_1:13;
then
A8: (n div k)-'1 = (n div k) - 1 by XREAL_1:233;
n = k * (n div k) by A1,NAT_D:3;
then n -' i = k * (n div k) - k * 1 + k - i by A7,XREAL_1:233
.= k * ((n div k)-'1) + (k - i) by A8
.= k * ((n div k)-'1) + (k-'i) by A4,XREAL_1:233;
hence thesis by A8,A5,NAT_D:def 1;
end;
theorem
k <= n implies (2 to_power n) div (2 to_power k) = 2 to_power (n -' k)
proof
assume k <= n;
then 2 to_power k > 0 & 2 to_power n = (2 to_power k) * (2 to_power (n-'k))
by Th10,POWER:34;
hence thesis by NAT_D:18;
end;
theorem
n > 0 implies 2 to_power n mod 2 = 0
proof
assume n > 0;
then
A1: n >= 0 + 1 by NAT_1:13;
2 to_power n = 2 to_power (n - 1 + 1)
.= 2 to_power (n-'1 + 1) by A1,XREAL_1:233
.= 2 to_power (n-'1) * (2 to_power 1) by POWER:27
.= 2 to_power (n-'1) * 2 by POWER:25;
hence thesis;
end;
theorem
n > 0 implies (n mod 2 = 0 iff (n -' 1) mod 2 = 1)
proof
assume
A1: n > 0;
thus n mod 2 = 0 implies (n -' 1) mod 2 = 1
proof
consider t be Nat such that
A2: n = 2 * t + (n mod 2) and
(n mod 2) < 2 by NAT_D:def 2;
assume
A3: n mod 2 = 0;
then t > 0 by A1,A2;
then
A4: t >= 0 + 1 by NAT_1:13;
n >= 0 + 1 by A1,NAT_1:13;
then n -' 1 = 2 * (t - 1 + 1) - 1 by A3,A2,XREAL_1:233
.= 2 * (t - 1) + (1 + 1 - 1)
.= 2 * (t-'1) + 1 by A4,XREAL_1:233;
hence thesis by NAT_D:def 2;
end;
assume (n -' 1) mod 2 = 1;
then consider t be Nat such that
A5: n -' 1 = 2 * t + 1 and
1 < 2 by NAT_D:def 2;
n >= 0 + 1 by A1,NAT_1:13;
then n = 2 * t + 1 + 1 by A5,XREAL_1:235
.= 2 * (t + 1) + 0;
hence thesis;
end;
theorem
for n be non zero Nat st n <> 1 holds n > 1
proof
let n be non zero Nat;
A1: n >= 1 by NAT_1:14;
assume n <> 1;
hence thesis by A1,XXREAL_0:1;
end;
theorem
n <= k & k < n + n implies k div n = 1
proof
assume that
A1: n <= k and
A2: k < n + n;
A3: k = n + (k - n) .= n * 1 + (k-'n) by A1,XREAL_1:233;
k - n < n + n - n by A2,XREAL_1:9;
hence thesis by A3,NAT_D:def 1;
end;
A5: 1 mod 2 = 1 by NAT_D:24;
theorem Th21:
for n being Integer holds n is even iff n mod 2 = 0
proof
let n be Integer;
thus n is even implies n mod 2 = 0
proof
assume n is even;
then ex k being Integer st n = 2*k by ABIAN:11;
hence thesis;
end;
assume
A2: n mod 2 = 0;
assume n is odd;
then consider k being Integer such that
A3: n = 2*k+1 by ABIAN:1;
A4: 2*k mod 2 = 0;
2*k+1 mod 2 = ((2*k mod 2) + (1 mod 2)) mod 2 by NAT_D:66
.= 1 by A5;
hence thesis by A2,A3;
end;
theorem
for n being Integer holds n is odd iff n mod 2 = 1
proof
let n be Integer;
thus n is odd implies n mod 2 = 1
proof
assume n is odd;
then consider k being Integer such that
A1: n = 2*k+1 by ABIAN:1;
2*k+1 mod 2 = ((2*k mod 2) + (1 mod 2)) mod 2 by NAT_D:66
.= (0+1) mod 2 by A5
.= 1 by NAT_D:24;
hence thesis by A1;
end;
assume
A2: n mod 2 = 1;
assume n is even;
then ex k being Integer st n = 2*k by ABIAN:11;
hence thesis by A2;
end;
theorem
1 <= t & k <= n & 2*t divides k implies
(n div t is even iff (n-'k) div t is even)
proof
assume that
A1: 1 <= t and
A2: k <= n and
A3: 2*t divides k;
consider r be Nat such that
A4: k = 2 * t * r by A3,NAT_D:def 3;
thus n div t is even implies (n-'k) div t is even
proof
assume n div t is even;
then consider p be Nat such that
A5: n div t = 2 * p by ABIAN:def 2;
consider q be Nat such that
A6: n = t * (2 * p) + q and
A7: q < t by A1,A5,NAT_D:def 1;
1 * t < 2 * t by A1,XREAL_1:68;
then t + q < 2 * t + t by A7,XREAL_1:8;
then
q < 2 * t by XREAL_1:6;
then q / (2 * t) < 1 by XREAL_1:189;
then
A8: p + q / (2 * t) < p + 1 by XREAL_1:6;
consider r be Nat such that
A9: k = 2 * t * r by A3,NAT_D:def 3;
A10: 2 * t <> 0 by A1;
then 2 * t * r <= 2 * t * p + q / (2 * t) * (2 * t) by A2,A6,A9,XCMPLX_1:87
;
then 2 * t * r <= 2 * t * (p + q / (2 * t));
then r <= p + q / (2 * t) by A10,XREAL_1:68;
then p + q / (2 * t) + r < p + 1 + (p + q / (2 * t)) by A8,XREAL_1:8;
then r < p + 1 by XREAL_1:6;
then
A11: r <= p by NAT_1:13;
(n-'k) = t * (2 * p) + q - 2 * t * r by A2,A6,A9,XREAL_1:233
.= t * (2 * (p - r)) + q
.= t * (2 * (p-'r)) + q by A11,XREAL_1:233;
hence thesis by A7,NAT_D:def 1;
end;
assume (n-'k) div t is even;
then consider p be Nat such that
A12: (n-'k) div t = 2 * p by ABIAN:def 2;
consider q be Nat such that
A13: n-'k = t * (2 * p) + q and
A14: q < t by A1,A12,NAT_D:def 1;
n - k = t * (2 * p) + q by A2,A13,XREAL_1:233;
then n = t * (2 * (p + r)) + q by A4;
hence thesis by A14,NAT_D:def 1;
end;
theorem Th24:
n <= m implies n div k <= m div k
proof
assume that
A1: n <= m and
A2: n div k > m div k;
set r = (n div k) -' (m div k);
A3: r = (n div k) - (m div k) by A2,XREAL_1:233;
then r > (m div k) - (m div k) by A2,XREAL_1:9;
then r >= 0 + 1 by NAT_1:13;
then k * r >= k * 1 by XREAL_1:64;
then
A4: k * r + k * (m div k) >= k + k * (m div k) by XREAL_1:6;
per cases;
suppose
A5: k <> 0;
then ex t2 be Nat st m = k * (m div k) + t2 & t2 < k by NAT_D:def 1;
then m < k + k * (m div k) by XREAL_1:6;
then
m - (k * (n div k)) < (k + k * (m div k)) - (k + k * (m div k)) by A3,A4,
XREAL_1:14;
then
A6: m - (k * (n div k)) < 0;
ex t1 be Nat st n = k * (n div k) + t1 & t1 < k by A5,NAT_D:def 1;
then k * (n div k) <= n by NAT_1:11;
then m - n < (k * (n div k)) - (k * (n div k)) by A6,XREAL_1:13;
then m < 0 + n by XREAL_1:19;
hence contradiction by A1;
end;
suppose
k = 0;
hence contradiction by A2;
end;
end;
theorem
k <= 2 * n implies (k+1) div 2 <= n
proof
assume k <= 2 * n;
then k + 1 <= 2 * n + 1 by XREAL_1:6;
then (k + 1) div 2 <= (2 * n + 1) div 2 by Th24;
hence thesis by NAT_D:def 1;
end;
theorem
n is even implies n div 2 = (n + 1) div 2
proof
assume
A1: n is even;
n = 2 * (n div 2) + (n mod 2) by NAT_D:2
.= 2 * (n div 2) + 0 by A1,Th21;
hence thesis by NAT_D:def 1;
end;
theorem
(n div k) div i = n div (k*i)
proof
now
per cases;
suppose i = 0;
hence (n div k) div i = n div (k*i);
end;
suppose
A2: i <> 0;
now
per cases;
suppose k = 0;
hence thesis;
end;
suppose
A4: k <> 0;
consider t2 be Nat such that
A5: n div k = i * ((n div k) div i) + t2 and
A6: t2 < i by A2,NAT_D:def 1;
t2 + 1 <= i by A6,NAT_1:13;
then
A7: k * (t2 + 1) <= k * i by XREAL_1:64;
consider t1 be Nat such that
A8: n = k * (n div k) + t1 and
A9: t1 < k by A4,NAT_D:def 1;
k * t2 + t1 < k * t2 + k * 1 by A9,XREAL_1:6;
then (k * t2 + t1) - (k * i) < (k * (t2 + 1)) - (k * (t2 + 1)) by A7,
XREAL_1:14;
then
A10: k * t2 + t1 < 0 + k * i by XREAL_1:19;
n = k * i * ((n div k) div i) + (k * t2 + t1) by A8,A5;
hence thesis by A10,NAT_D:def 1;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
definition
let n be Nat;
redefine attr n is trivial means :: redefines trivial (SUBSET_1, redefinition) → trivial (ZFMISC_1, definition)
:Def1:
n = 0 or n = 1;
compatibility
proof
thus n is trivial implies n = 0 or n = 1
proof
assume
A1: n is trivial;
assume that
A2: n <> 0 and
A3: n <> 1;
A4: n > 1+0 by A2,A3,NAT_1:25;
reconsider n as Nat;
consider x being object such that
A5: n = {x} by A1,A2,ZFMISC_1:131;
A6: n = { k where k is Nat : k < n } by AXIOMS:4;
then
A7: 1 in n by A4;
0 in n by A2,A6;
then 0 = x by A5,TARSKI:def 1;
hence contradiction by A7,A5,TARSKI:def 1;
end;
assume n = 0 or n = 1;
hence thesis by CARD_1:49;
end;
end;
registration
cluster non trivial for Nat;
existence
proof
take 2;
thus thesis;
end;
end;
theorem
k is non trivial iff k is non empty & k <> 1;
theorem
for k be non trivial Nat holds k >= 2
proof
let k be non trivial Nat;
k >= 1 by NAT_1:14;
then k > 1 or k = 1 by XXREAL_0:1;
then k >= 1 + 1 by Def1,NAT_1:13;
hence thesis;
end;
scheme
Indfrom2 { P[set] } : for k be non trivial Nat holds P[k]
provided
A1: P[2] and
A2: for k be non trivial Nat st P[k] holds P[k + 1]
proof
defpred P[non zero Nat] means $1 is non trivial implies P[$1];
A3: now
let k be non zero Nat;
assume
A4: P[k];
now
assume k + 1 is non trivial;
per cases;
suppose
k = 1;
hence P[k + 1] by A1;
end;
suppose
k <> 1;
then k is non trivial;
hence P[k + 1] by A2,A4;
end;
end;
hence P[k+1];
end;
A5: P[1] by Def1;
for k be non zero Nat holds P[k] from NAT_1:sch 10(A5,A3);
hence thesis;
end;
begin :: Addenda
:: from POLYNOM1, 2007.03.18, A.T.
theorem
i-'j-'k = i-'(j+k)
proof
per cases;
suppose
A1: i <= j;
hence i-'j-'k = 0-'k by Th8
.= 0 by Th8
.= i-'(j+k) by A1,Th8,NAT_1:12;
end;
suppose
A2: j <= i & i-j <= k;
then
A3: i <= j+k by XREAL_1:20;
i-'j = i-j by A2,XREAL_1:233;
hence i-'j-'k = 0 by A2,Th8
.= i-'(j+k) by A3,Th8;
end;
suppose
A4: j <= i & k <= i-j;
then
A5: k+j <= i by XREAL_1:19;
i-'j = i-j by A4,XREAL_1:233;
hence i-'j-'k = i-j-k by A4,XREAL_1:233
.= i-(j+k)
.= i-'(j+k) by A5,XREAL_1:233;
end;
end;