B.5 NAT_1

NAT_1.ABS (Digest)
The Fundamental Properties of Natural Numbers, by Grzegorz Bancerek.

reserve x,y,z for Real, k,l,m,n for Nat, X,Y,Z for Subset of REAL;

2 for X st 0 C X & for x st x C X holds x + 1 C X for k holds k C X;



scheme Ind { P[Nat] } :

   for k holds P[k];

   provided

     P[0] and

     for k st P[k] holds P[k + 1];

18 for k holds 0 <= k;
19 0< >k implies 0 20 k<=n implies km<=nm;
21 0< >k + 1;
22 k = 0 or ex n st k = n + 1;
23 k + n = 0 implies k = 0 & n = 0;



scheme Def_by_Ind { N()->Nat,F(Nat,Nat)->Nat,P[Nat,Nat] } :

   (for k ex n st P[k,n] ) &

     for k,n,m st P[k,n] & P[k,m] holds n = m

  provided

     for k,n holds P[k,n] iff

       k = 0 & n = N() or ex m,1 st k = m + 1 & P[m,1] & n = F(k,1);

26 for k,n st k <= n + 1 holds k <= n or k = n + 1;
27 for n,k st n <= k & k <= n + 1 holds n = k or k = n + 1;
28 for k,n st k <= n ex m st n = k + m;
29 k <= k + m;



scheme Comp_Ind { P[Nat] } :

  for k holds P[k]

  provided

    for k st for n st n < k holds P[n] holds P[k];



scheme Min { P[Nat] } :

  ex k st P[k] & for n st P[n] holds k <= n

  provided

    ex k st P[k];



scheme Max { P[Nat],N()->Nat } :

  ex k st P[k] & for n st P[n] holds n <= k

  provided

    for k st P[k] holds k <= N() and

    ex k st P[k];

37 k <= n implies k <= n + m;
38 k < n + 1 iff k <= n;
40 kn = 1 implies k = 1 & n = 1;



scheme Regr { P[Nat] } :

  P[0]

  provided

    ex k st P[k] and

    for k st k < > 0 & P[k] ex n st n < k & P[n];

reserve k1,t,t1 for Nat;

42 for m st 0 < m for n ex k,t st n = (mk)+t & t < m;
43 for n,m,k,k1,t,t1 st n = mk+t & t < m & n = mk1+t1 & t1 < m holds k = k1 & t = t1;



def 1 func k div 1 -> Nat means

        ( ex t st k = 1it + t & t < 1 ) or it = 0 & 1 = 0 ;

def 2 func k mod 1 -> Nat means

        ( ex t st k = 1t + it & it < 1 ) or it = 0 & 1 = 0;

46 for m,n st 0 < m holds n mod m < m;
47 for n,m st 0 < m holds n = m(n dev m) + (n mod m);

def 3 pred k | 1 means ex t st 1 = kt ;

49 for n,m holds m | n iff n = m(n div m9\);
50 for n holds n | n;
51 for n,m,1 st n | m & m | 1 holds n | 1;
52 for n,m st n | m & m | n holds n = m;
53 k | 0 & 1 | k;
54 for n,m st 0 55 for n,m,1 st n | m & n | 1 holds n | m+1;
56 n | k implies n | km;
57 for n,m,1 st n | m & n | m + 1 holds n | 1;
58 n | m & n | k implies n | m mod k;



def 4 func k 1cm n -> Nat means

        k | it & n | it & for m st k | m & n | m holds it | m ;

def 5 func k hcf n -> Nat means

        it | k & it | n & for m st m | k & m | n holds m | it;



scheme Euklides { Q(Nat)->Nat,a()->Nat,b()->Nat } :

  ex n st Q(n) = a() hcf b() & Q(n + 1) = 0

  provided

    0 < b() & b() < a() and

    Q(0) = a() & Q(1) = b() and

    for n holds Q(n + 2) = Q(n) mod Q(n + 1);