The abstract of the Mizar article:

Natural Numbers

by

Robert Milewski

Received February 23, 1998

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];