Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### The Fundamental Properties of Natural Numbers

**by****Grzegorz Bancerek**- Received January 11, 1989
- MML identifier: NAT_1

- [ Mizar article, MML identifier index ]

environ vocabulary ORDINAL2, ARYTM, ARYTM_1, ARYTM_3, ORDINAL1, NAT_1, XREAL_0; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, NUMBERS, XCMPLX_0, XREAL_0, REAL_1; constructors REAL_1, XREAL_0, XCMPLX_0, XBOOLE_0; clusters REAL_1, NUMBERS, ORDINAL2, XREAL_0, ARYTM_3, ZFMISC_1, XBOOLE_0; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin definition mode Nat is Element of NAT; end; reserve x for Real, k,l,m,n for Nat, h,i,j for natural number, X for Subset of REAL; :: The results of axioms of natural numbers canceled; theorem :: NAT_1:2 :: axiom of induction for X st 0 in X & for x st x in X holds x + 1 in X for k holds k in X; :: Addition and multiplication :: The natural numbers are real numbers therefore some theorems of real :: numbers are translated for natural numbers. definition let n,k be Nat; redefine func n + k -> Nat; end; definition let n,k be natural number; cluster n + k -> natural; end; :: Now we can form and prove the scheme of induction. 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]; :: Like addition, the result of multiplication of two natural numbers is :: a natural number. definition let n,k be Nat; redefine func n * k -> Nat; end; definition let n,k be natural number; cluster n * k -> natural; end; :::::::::::::::::::: :: Order relation :: :::::::::::::::::::: :: Some theorems of not great relation "<=" in real numbers are translated :: to natural number easy and it is necessary to have them here. canceled 15; theorem :: NAT_1:18 0 <= i; theorem :: NAT_1:19 0 <> i implies 0 < i; theorem :: NAT_1:20 i <= j implies i * h <= j * h; theorem :: NAT_1:21 0 <> i + 1; theorem :: NAT_1:22 i = 0 or ex k st i = k + 1; theorem :: NAT_1:23 i + j = 0 implies i = 0 & j = 0; definition cluster non zero (natural number); end; definition let m be natural number, n be non zero (natural number); cluster m + n -> non zero; cluster n + m -> non zero; end; 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); canceled 2; theorem :: NAT_1:26 for i,j st i <= j + 1 holds i <= j or i = j + 1; theorem :: NAT_1:27 i <= j & j <= i + 1 implies i = j or j = i + 1; theorem :: NAT_1:28 for i,j st i <= j ex k st j = i + k; theorem :: NAT_1: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]; :: Principle of minimum scheme Min { P[Nat] } : ex k st P[k] & for n st P[n] holds k <= n provided ex k st P[k]; :: Principle of maximum 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]; canceled 7; theorem :: NAT_1:37 i <= j implies i <= j + h; theorem :: NAT_1:38 i < j + 1 iff i <= j; canceled; theorem :: NAT_1: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]; :: Exact division and rest of division reserve k1,t,t1 for Nat; canceled; theorem :: NAT_1:42 for m st 0 < m for n ex k,t st n = (m*k)+t & t < m; theorem :: NAT_1: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; definition let k,l be natural number; func k div l -> Nat means :: NAT_1:def 1 :: the exact division ( ex t st k = l * it + t & t < l ) or it = 0 & l = 0; func k mod l -> Nat means :: NAT_1:def 2 :: the rest of division ( ex t st k = l * t + it & it < l ) or it = 0 & l = 0; end; canceled 2; theorem :: NAT_1:46 0 < i implies j mod i < i; theorem :: NAT_1:47 0 < i implies j = i * (j div i) + (j mod i); :: The divisibility relation definition let k,l be natural number; pred k divides l means :: NAT_1:def 3 ex t st l = k * t; reflexivity; end; canceled; theorem :: NAT_1:49 j divides i iff i = j * (i div j); canceled; theorem :: NAT_1:51 i divides j & j divides h implies i divides h; theorem :: NAT_1:52 i divides j & j divides i implies i = j; theorem :: NAT_1:53 i divides 0 & 1 divides i; theorem :: NAT_1:54 0 < j & i divides j implies i <= j; theorem :: NAT_1:55 i divides j & i divides h implies i divides j+h; theorem :: NAT_1:56 i divides j implies i divides j * h; theorem :: NAT_1:57 i divides j & i divides j + h implies i divides h; theorem :: NAT_1:58 i divides j & i divides h implies i divides j mod h; :: The least common multiple and the greatest common divisor definition let k,n be Nat; func k lcm n -> Nat means :: NAT_1:def 4 k divides it & n divides it & for m st k divides m & n divides m holds it divides m; idempotence; commutativity; end; definition let k,n be Nat; func k hcf n -> Nat means :: NAT_1:def 5 it divides k & it divides n & for m st m divides k & m divides n holds m divides it; idempotence; commutativity; end; 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); definition cluster -> ordinal Nat; end; definition cluster non empty ordinal Subset of REAL; end;

Back to top