Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998 Association of Mizar Users

### Natural Numbers

by
Robert Milewski

MML identifier: NAT_2
[ Mizar article, MML identifier index ]

```environ

vocabulary FINSEQ_1, FUNCT_1, INT_1, ARYTM_1, ARYTM_3, NAT_1, POWER, MATRIX_2,
FINSEQ_4, ORDINAL2, REALSET1, ARYTM;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XCMPLX_0, XREAL_0, REALSET1,
INT_1, NAT_1, POWER, ABIAN, SERIES_1, FUNCT_1, FINSEQ_1, FINSEQ_4,
BINARITH, ORDINAL2;
constructors ABIAN, SERIES_1, BINARITH, FINSEQ_4, INT_1, REALSET1, MEMBERED;
clusters XREAL_0, RELSET_1, ABIAN, BINARITH, INT_1, REALSET1, MEMBERED, NAT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin :: Preliminaries

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
for n be Nat st 1 <= n & n < N() holds for x be Element of D()
ex y be Element of D() st P[n,x,y];

theorem :: NAT_2:1
for x be real number holds
x < [\ x /] + 1;

theorem :: NAT_2:2
for x,y be real number st x >= 0 & y > 0 holds
x / ( [\ x / y /] + 1 ) < y;

begin :: Division and Rest of Division

canceled;

theorem :: NAT_2:4
for n be natural number holds
0 div n = 0;

theorem :: NAT_2:5
for n be non empty Nat holds n div n = 1;

theorem :: NAT_2:6
for n be Nat holds n div 1 = n;

theorem :: NAT_2:7
for i,j,k,l be natural number st i <= j & k <= j holds
i = j -' k + l implies k = j -' i + l;

theorem :: NAT_2:8
for i,n be natural number holds
i in Seg n implies n -' i + 1 in Seg n;

theorem :: NAT_2:9
for i,j be natural number st j < i holds
i -' (j + 1) + 1 = i -' j;

theorem :: NAT_2:10
for i,j be natural number st i >= j holds
j -' i = 0;

theorem :: NAT_2:11
for i,j be non empty natural number holds
i -' j < i;

theorem :: NAT_2:12
for n,k be natural number st k <= n holds
2 to_power n = (2 to_power k) * (2 to_power (n-'k));

theorem :: NAT_2:13
for n,k be Nat st k <= n holds
2 to_power k divides 2 to_power n;

theorem :: NAT_2:14
for n,k be natural number st k > 0 & n div k = 0 holds n < k;

reserve n, k, i for natural number;

theorem :: NAT_2:15
k > 0 & k <= n implies n div k >= 1;

theorem :: NAT_2:16
k <> 0 implies (n+k) div k = (n div k) + 1;

theorem :: NAT_2:17
k divides n & 1 <= n & 1 <= i & i <= k implies
(n -' i) div k = (n div k) - 1;

theorem :: NAT_2:18
for n,k be Nat st k <= n holds
(2 to_power n) div (2 to_power k) = 2 to_power (n -' k);

theorem :: NAT_2:19
for n be Nat st n > 0 holds
2 to_power n mod 2 = 0;

theorem :: NAT_2:20
for n be Nat st n > 0 holds
n mod 2 = 0 iff (n -' 1) mod 2 = 1;

theorem :: NAT_2:21
for n be non empty natural number st n <> 1 holds
n > 1;

theorem :: NAT_2:22
for n, k be natural number st n <= k & k < n + n holds
k div n = 1;

theorem :: NAT_2:23
for n be Nat holds n is even iff n mod 2 = 0;

theorem :: NAT_2:24
for n be Nat holds n is odd iff n mod 2 = 1;

theorem :: NAT_2:25
for n,k,t be Nat st 1 <= t & k <= n & 2*t divides k holds
n div t is even iff (n-'k) div t is even;

theorem :: NAT_2:26
for n,m,k be Nat st n <= m holds
n div k <= m div k;

theorem :: NAT_2:27
for n,k be Nat st k <= 2 * n holds
(k+1) div 2 <= n;

theorem :: NAT_2:28
for n be even Nat holds
n div 2 = (n + 1) div 2;

theorem :: NAT_2:29
for n,k,i be Nat holds
(n div k) div i = n div (k*i);

definition
let n be natural number;
redefine attr n is trivial means
:: NAT_2:def 1
n = 0 or n = 1;
end;

definition
cluster non trivial Nat;
cluster non trivial natural number;
end;

theorem :: NAT_2:30
for k be natural number holds
k is non trivial iff k is non empty & k <> 1;

theorem :: NAT_2:31
for k be non trivial natural number holds
k >= 2;

scheme Ind_from_2 { P[Nat] } :
for k be non trivial Nat holds P[k]
provided
P[2] and
for k be non trivial Nat st P[k] holds P[k + 1];
```