:: On the Representation of Natural Numbers in Positional Numeral Systems :: by Adam Naumowicz :: :: Received December 31, 2006 :: Copyright (c) 2006-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, SUBSET_1, FUNCT_1, NAT_1, TARSKI, RELAT_1, AFINSQ_1, ARYTM_1, ARYTM_3, FINSEQ_1, XXREAL_0, CARD_1, XBOOLE_0, ORDINAL4, CARD_3, FINSOP_1, BINOP_2, INT_1, SERIES_1, VALUED_1, PREPOWER, NEWTON, POWER, NUMERAL1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, CARD_1, XCMPLX_0, XXREAL_0, AFINSQ_1, VALUED_1, RELSET_1, FUNCT_2, BINOP_1, NAT_1, BINOP_2, RECDEF_1, SERIES_1, NEWTON, PREPOWER, POWER, AFINSQ_2, NAT_D; constructors PREPOWER, SERIES_1, PARTFUN3, BINOM, SETWISEO, REAL_1, NAT_D, RECDEF_1, BINOP_2, RELSET_1, AFINSQ_2, BINOP_1, NEWTON; registrations XBOOLE_0, RELAT_1, ORDINAL1, XXREAL_0, XREAL_0, NAT_1, CARD_1, NUMBERS, INT_1, BINOP_2, MEMBERED, NEWTON, AFINSQ_1, VALUED_1, FUNCT_2, POWER, FINSET_1, AFINSQ_2, RELSET_1, VALUED_0, FUNCT_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Preliminaries theorem :: NUMERAL1:1 for k,l,m being Nat holds (k(#)(l GeoSeq))|m is XFinSequence of NAT; theorem :: NUMERAL1:2 for d being XFinSequence of NAT, n being Nat st for i being Nat st i in dom d holds n divides d.i holds n divides Sum d; theorem :: NUMERAL1:3 for d,e being XFinSequence of NAT, n being Nat st dom d = dom e & for i being Nat st i in dom d holds e.i = d.i mod n holds Sum d mod n = Sum e mod n; begin :: Representation of numbers in the base-$b$ numeral system definition let d be XFinSequence of NAT; let b be Nat; func value(d,b) -> Nat means :: NUMERAL1:def 1 ex d9 being XFinSequence of NAT st (dom d9 = dom d & for i being Nat st i in dom d9 holds d9.i = (d.i)*(b|^i)) & it = Sum d9; end; definition let n,b be Nat; assume b>1; ::$N Unique Representation of Natural Numbers in Positional Numeral Systems func digits(n,b) -> XFinSequence of NAT means :: NUMERAL1:def 2 value(it,b)=n & it.(len (it)-1) <> 0 & for i being Nat st i in dom it holds 0 <= it.i & it.i < b if n <> 0 otherwise it = <%0%>; end; theorem :: NUMERAL1:4 for n,b being Nat st b > 1 holds len digits(n,b) >= 1; theorem :: NUMERAL1:5 for n,b being Nat st b > 1 holds value(digits(n,b),b)=n; begin :: Selected divisibility criteria theorem :: NUMERAL1:6 for n,k being Nat st k=10|^n - 1 holds 9 divides k; theorem :: NUMERAL1:7 for n,b being Nat st b>1 holds b divides n iff digits(n,b).0 = 0; theorem :: NUMERAL1:8 for n being Nat holds 2 divides n iff 2 divides digits(n,10).0; ::$N Divisibility by 3 Rule theorem :: NUMERAL1:9 for n being Nat holds 3 divides n iff 3 divides Sum digits(n,10); theorem :: NUMERAL1:10 for n being Nat holds 5 divides n iff 5 divides digits(n,10).0;