B.7 NAT_1

The Fundamental Properties of Natural Numbers by Grzegorz Bancerek

mode Nat is Element of NAT;

reserve x for Real,
   k,l,m,n for Nat,
   h,i,j,p for natural number,
   X for Subset of REAL;

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

redefine func n + k -> Nat;

cluster n + k -> natural;

scheme Ind { P[Nat] } :
  for k being Nat holds P[k]
  provided
  P[0] and
  for k being Nat st P[k] holds P[k + 1];

scheme Nat_Ind { P[natural number] } :
  for k being natural number holds P[k]
  provided
  P[0] and
  for k be natural number st P[k] holds P[k + 1];

redefine func n * k -> Nat;

cluster n * k -> natural;

18 0 <= i;
19 0 <> i implies 0 < i;
20 i <= j implies i * h <= j * h;
21 0 <> i + 1;
22 i = 0 or ex k st i = k + 1;
23 i + j = 0 implies i = 0 & j = 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,l st k = m + 1 & P[m,l] & n = F(k,l);

26 for i,j st i <= j + 1 holds i <= j or i = j + 1;
27 i <= j & j <= i + 1 implies i = j or j = i + 1;
28 for i,j st i <= j ex k st j = i + k;
29 i <= i + j;

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 i <= j implies i <= j + h;
38 i < j + 1 iff i <= j;
40 i * j = 1 implies i = 1 & j = 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 = (m*k)+t & t < m;
43 for n,m,k,k1,t,t1 being natural number
st n = m*k+t & t < m & n = m*k1+t1 & t1 < m holds
k = k1 & t = t1;

def 1 func k div l -> Nat means
 ( ex t st k = l * it + t & t < l ) or it = 0 & l = 0;
def 2 func k mod l -> Nat means
 ( ex t st k = l * t + it & it < l ) or it = 0 & l = 0;

46 0 < i implies j mod i < i;
47 0 < i implies j = i * (j div i) + (j mod i);

def 3 pred k divides l means ex t st l = k * t;

49 j divides i iff i = j * (i div j);
51 i divides j & j divides h implies i divides h;
52 i divides j & j divides i implies i = j;
53 i divides 0 & 1 divides i;
54 0 < j & i divides j implies i <= j;
55 i divides j & i divides h implies i divides j+h;
56 i divides j implies i divides j * h;
57 i divides j & i divides j + h implies i divides h;
58 i divides j & i divides h implies i divides j mod h;

def 4 func k lcm n -> Nat means
  k divides it & n divides it & for m st k divides m & n divides
  m holds it divides m;
def 5 func k hcf n -> Nat means
  it divides k & it divides n & for m st m divides k & m divides
  n holds m divides it;

scheme Euklides { Q(Nat)->Nat, a,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);

cluster -> ordinal Nat;
cluster non empty ordinal Subset of REAL;