:: The Fundamental Properties of Natural Numbers :: by Grzegorz Bancerek :: :: Received January 11, 1989 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, ORDINAL1, REAL_1, SUBSET_1, CARD_1, ARYTM_3, TARSKI, RELAT_1, XXREAL_0, XCMPLX_0, ARYTM_1, XBOOLE_0, FINSET_1, FUNCT_1, NAT_1, FUNCOP_1, PBOOLE, PARTFUN1, FUNCT_7, SETFAM_1, ZFMISC_1; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, FINSET_1, CARD_1, PBOOLE, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCOP_1, FUNCT_2, BINOP_1; constructors NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, CARD_1, WELLORD2, FUNCT_2, PARTFUN1, FUNCOP_1, FUNCT_4, ENUMSET1, RELSET_1, PBOOLE, ORDINAL1, SETFAM_1, ZFMISC_1, BINOP_1; registrations SUBSET_1, ORDINAL1, XXREAL_0, XREAL_0, CARD_1, RELSET_1, FUNCT_2, PBOOLE; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin registration cluster natural for object; end; reserve x for Real, p,k,l,m,n,s,h,i,j,k1,t,t1 for Nat, X for Subset of REAL; :: The results of axioms of Nats theorem :: NAT_1:1 for X st 0 in X & for x st x in X holds x + 1 in X for n holds n in X; :: Addition and multiplication :: The Nats are real numbers therefore some theorems of real :: numbers are translated for Nats. registration let n,k be natural Number; cluster n + k -> natural; end; definition let n be natural Number, k be Element of NAT; redefine func n + k -> Element of NAT; end; ::$CS ::$N The Principle of Mathematical Induction scheme :: NAT_1:sch 2 NatInd { P[Nat] } : for k being Nat holds P[k] provided P[0] and for k be Nat st P[k] holds P[k + 1]; :: Like addition, the result of multiplication of two Nats is a Nat. registration let n,k be natural Number; cluster n * k -> natural; end; definition let n, k be Element of NAT; redefine func n * k -> Element of NAT; end; :: Order relation :: :: Some theorems of not great relation "<=" in real numbers are translated :: to Nat easy and it is necessary to have them here. theorem :: NAT_1:2 for i being natural Number holds 0 <= i; theorem :: NAT_1:3 for i being natural Number holds 0 <> i implies 0 < i; theorem :: NAT_1:4 for i,j,h being natural Number holds i <= j implies i * h <= j * h; theorem :: NAT_1:5 for i being natural Number holds 0 < i + 1; theorem :: NAT_1:6 for i being natural Number holds i = 0 or ex k st i = k + 1; theorem :: NAT_1:7 for i,j being natural Number holds i + j = 0 implies i = 0 & j = 0; registration cluster zero natural for object; cluster non zero natural for object; end; registration let m be natural Number, n be non zero natural Number; cluster m + n -> non zero; cluster n + m -> non zero; end; scheme :: NAT_1:sch 3 DefbyInd { N()->Nat, F(Nat,Nat)->Nat, P[Nat,Nat] } : (for k being Nat ex n being Nat st P[k,n]) & for k,n,m being Nat st P[k,n] & P[k,m] holds n = m provided for k,n being Nat holds P[k,n] iff k = 0 & n = N() or ex m,l being Nat st k = m + 1 & P[m,l] & n = F(k,l); theorem :: NAT_1:8 for i,j being natural Number holds i <= j + 1 implies i <= j or i = j + 1; theorem :: NAT_1:9 for i,j being natural Number holds i <= j & j <= i + 1 implies i = j or j = i + 1; theorem :: NAT_1:10 for i,j being natural Number holds i <= j implies ex k st j = i + k; theorem :: NAT_1:11 for i,j being natural Number holds i <= i + j; scheme :: NAT_1:sch 4 CompInd { P[Nat] } : for k being Nat holds P[k] provided for k being Nat st for n being Nat st n < k holds P[n] holds P[k]; :: Principle of minimum scheme :: NAT_1:sch 5 Min { P[Nat] } : ex k being Nat st P[k] & for n being Nat st P[n] holds k <= n provided ex k being Nat st P[k]; :: Principle of maximum scheme :: NAT_1:sch 6 Max { P[Nat], N()->Nat } : ex k being Nat st P[k] & for n being Nat st P[n] holds n <= k provided for k being Nat st P[k] holds k <= N() and ex k being Nat st P[k]; theorem :: NAT_1:12 for i,j,h being natural Number holds i <= j implies i <= j + h; theorem :: NAT_1:13 for i,j being natural Number holds i < j + 1 iff i <= j; theorem :: NAT_1:14 for i being natural Number holds i < 1 implies i = 0; theorem :: NAT_1:15 for i,j being natural Number holds i * j = 1 implies i = 1; theorem :: NAT_1:16 for n,k being natural Number holds k <> 0 implies n < n + k; scheme :: NAT_1:sch 7 Regr { P[Nat] } : P[0] provided ex k being Nat st P[k] and for k being Nat st k <> 0 & P[k] ex n being Nat st n < k & P[n]; :: Exact division and rest of division theorem :: NAT_1:17 0 < m implies for n ex k,t st n = (m*k)+t & t < m; theorem :: NAT_1:18 for n,m,k,t,k1,t1 being natural Number holds n = m*k+t & t < m & n = m*k1+t1 & t1 < m implies k = k1 & t = t1; registration cluster -> ordinal for natural Number; end; registration cluster non empty ordinal for Subset of REAL; end; theorem :: NAT_1:19 for k,n being natural Number holds k < k + n iff 1 <= n; theorem :: NAT_1:20 for k,n being natural Number holds k < n implies n - 1 is Element of NAT; theorem :: NAT_1:21 for k,n being natural Number holds k <= n implies n - k is Element of NAT; begin :: Addenda :: from ALGSEQ_1 theorem :: NAT_1:22 for m,n being natural Number holds m < n+1 implies m < n or m = n; theorem :: NAT_1:23 for k being natural Number holds k < 2 implies k = 0 or k = 1; registration cluster non zero for Element of NAT; end; registration cluster -> non negative for Element of NAT; end; registration cluster -> non negative for natural Number; end; :: from JORDAN4 theorem :: NAT_1:24 for i,j,h being natural Number holds i <> 0 & h = j*i implies j <= h; :: from BINOM, 2006.05.28, A.T. scheme :: NAT_1:sch 8 Ind1{M() -> Nat, P[Nat]} : for i being Nat st M() <= i holds P[i] provided P[M()] and for j being Nat st M() <= j holds P[j] implies P[j+1]; :: from INT_2, 2006.05.30, AG scheme :: NAT_1:sch 9 CompInd1 { a() -> Nat, P[Nat] } : for k being Nat st k >= a() holds P[k] provided for k being Nat st k>=a() & (for n being Nat st n>=a() & n Element of NAT means :: NAT_1:def 1 it in A & for k st k in A holds it <= k if A is non empty Subset of NAT otherwise it = 0; end; :: from CARD_1, 2007.10.28,A.T. reserve x for object, X,Y,Z for set; ::$CT 12 theorem :: NAT_1:38 for n being Nat holds succ Segm n = Segm(n + 1); theorem :: NAT_1:39 n <= m iff Segm n c= Segm m; theorem :: NAT_1:40 card Segm n c= card Segm m iff n <= m; theorem :: NAT_1:41 card Segm n in card Segm m iff n < m; reserve M,N for Cardinal; theorem :: NAT_1:42 nextcard card Segm n = card Segm(n+1); ::$CD theorem :: NAT_1:43 for X,Y being finite set holds X c= Y implies card X <= card Y; theorem :: NAT_1:44 for k,n being natural Number holds k in Segm n iff k < n; theorem :: NAT_1:45 for n being natural Number holds n in Segm(n+1); ::$CT :: from MODELC_2, 2008.08.18, A.T. definition let X be set; mode sequence of X is Function of NAT,X; end; :: from RECDEF_1, 2008.02.21, A.T. scheme :: NAT_1:sch 11 LambdaRecEx{A() -> object,G(object,object) -> object}: ex f being Function st dom f = NAT & f.0 = A() & for n being Nat holds f.(n+1) = G(n,f.n); scheme :: NAT_1:sch 12 LambdaRecExD{D() -> non empty set, A() -> Element of D(), G(object,object) -> Element of D()}: ex f being sequence of D() st f.0 = A() & for n being Nat holds f.(n+1) = G(n,f.n); scheme :: NAT_1:sch 13 RecUn{A() -> object, F, G() -> Function, P[object,object,object]}: F() = G() provided dom F() = NAT and F().0 = A() and for n holds P[n,F().n,F().(n+1)] and dom G() = NAT and G().0 = A() and for n holds P[n,G().n,G().(n+1)] and for n for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2; scheme :: NAT_1:sch 14 RecUnD{D() -> non empty set,A() -> Element of D(), P[object,object,object], F, G() -> sequence of D()} : F() = G() provided F().0 = A() and for n holds P[n,F().n,F().(n+1)] and G().0 = A() and for n holds P[n,G().n,G().(n+1)] and for n being Nat,x,y1,y2 being Element of D() st P[n,x,y1] & P[n,x,y2 ] holds y1=y2; scheme :: NAT_1:sch 15 LambdaRecUn{A() -> object, RecFun(object,object) -> object, F, G() -> Function}: F() = G() provided dom F() = NAT and F().0 = A() and for n holds F().(n+1) = RecFun(n,F().n) and dom G() = NAT and G().0 = A() and for n holds G().(n+1) = RecFun(n,G().n); scheme :: NAT_1:sch 16 LambdaRecUnD{D() -> non empty set,A() -> Element of D(), RecFun(object,object) -> Element of D(), F, G() -> sequence of D()}: F() = G() provided F().0 = A() and for n holds F().(n+1) = RecFun(n,F().n) and G().0 = A() and for n holds G().(n+1) = RecFun(n,G().n); :: missing, 2008.02.22, A.T. registration let x,y be natural Number; cluster min(x,y) -> natural; cluster max(x,y) -> natural; end; definition let x,y be Element of NAT; redefine func min(x,y) -> Element of NAT; redefine func max(x,y) -> Element of NAT; end; :: from SCMFSA_9, 2008.02.25, A.T. scheme :: NAT_1:sch 17 MinIndex { F(Nat)->Nat} : ex k st F(k)=0 & for n st F(n)=0 holds k <= n provided for k holds (F(k+1) < F(k) or F(k) = 0); :: from SEQM_3, BHSP_3, COMSEQ_3, KURATO_2, LOPBAN_3, CLVECT_2, CLOPBAN3 :: (generalized), 2008.08.23, A.T. definition let s be ManySortedSet of NAT, k be natural Number; func s ^\ k -> ManySortedSet of NAT means :: NAT_1:def 3 for n being Nat holds it.n=s.(n+k); end; registration let X be non empty set, s be X-valued ManySortedSet of NAT, k be natural Number; cluster s ^\ k -> X-valued; end; definition let X be non empty set, s be sequence of X, k be Nat; redefine func s ^\ k -> sequence of X; end; reserve X for non empty set, s for sequence of X; theorem :: NAT_1:47 s^\0 =s; theorem :: NAT_1:48 s ^\k^\m = s^\(k+m); theorem :: NAT_1:49 s^\k^\m = s^\m^\k; registration let N be sequence of NAT; let X,s; cluster s * N -> Function-like NAT-defined X-valued; end; registration let N be sequence of NAT; let X,s; cluster s * N -> total; end; theorem :: NAT_1:50 for N being sequence of NAT holds (s * N) ^\k = s * (N ^\k); theorem :: NAT_1:51 s.n in rng s; theorem :: NAT_1:52 (for n holds s.n in Y) implies rng s c= Y; :: from UPROOTS, 2009.07.21, A.T. theorem :: NAT_1:53 for n being natural Number holds n is non zero implies n = 1 or n > 1; theorem :: NAT_1:54 succ Segm n = {l where l is Nat : l <= n}; registration let n be natural Number; reduce In(n,NAT) to n; end; scheme :: NAT_1:sch 18 MinPred { F(Nat) -> Nat, P[object]} : ex k be Nat st P[k] & for n be Nat st P[n] holds k <= n provided for k be Nat holds F(k+1) < F(k) or P[k]; registration let k be Ordinal, x be object; cluster k --> x -> Sequence-like; end; theorem :: NAT_1:55 for s be ManySortedSet of NAT, k be natural Number holds rng(s ^\ k) c= rng s; :: from GLIB_002, 2011.07.30, A.T. ::$CT 3 theorem :: NAT_1:59 for X being finite set st 1 < card X holds ex x1,x2 being set st x1 in X & x2 in X & x1 <> x2; theorem :: NAT_1:60 k <= n implies k = 0 or ... or k = n; theorem :: NAT_1:61 x in Segm(n+1) implies x = 0 or ... or x = n; theorem :: NAT_1:62 m <= i & i <= m+k implies i = m+0 or ... or i = m+k; definition let D be set; let s be sequence of D, n be natural Number; redefine func s.n -> Element of D; end; registration cluster zero -> non positive for natural Number; end; registration let A be non zero object; cluster { A } -> with_non-empty_elements; let B be non zero object; cluster { A, B } -> with_non-empty_elements; let C be non zero object; cluster { A, B, C } -> with_non-empty_elements; let D be non zero object; cluster { A, B, C, D } -> with_non-empty_elements; let E be non zero object; cluster { A, B, C, D, E } -> with_non-empty_elements; let F be non zero object; cluster { A, B, C, D, E, F } -> with_non-empty_elements; let G be non zero object; cluster { A, B, C, D, E, F, G } -> with_non-empty_elements; let H be non zero object; cluster { A, B, C, D, E, F, G, H } -> with_non-empty_elements; let I be non zero object; cluster { A, B, C, D, E, F, G, H, I } -> with_non-empty_elements; let J be non zero object; cluster { A, B, C, D, E, F, G, H, I, J } -> with_non-empty_elements; end; registration cluster empty -> zero for set; cluster non zero -> non empty for set; end; definition let G be non empty set; let B be Function of [:G,NAT:], G; let g be Element of G, i be Nat; redefine func B.(g,i) -> Element of G; end; definition let G be non empty set; let B be Function of [:NAT,G:], G; let i be Nat, g be Element of G; redefine func B.(i,g) -> Element of G; end; scheme :: NAT_1:sch 19 SeqEx2D{X,Z() -> non empty set, P[set,set,set]}: ex f being Function of [:X(),NAT:],Z() st for x being Element of X(), y being Nat holds P[x,y,f.(x,y)] provided for x being Element of X(), y being Nat ex z being Element of Z() st P[x,y,z]; theorem :: NAT_1:63 for n being Nat holds Segm n c= Segm(n+1);