:: On the Representation of Natural Numbers in Positional Numeral Systems
:: by Adam Naumowicz
::
:: Received December 31, 2006
:: Copyright (c) 2006-2026 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;
definitions TARSKI;
equalities ORDINAL1;
theorems TARSKI, FUNCT_1, NAT_1, RELAT_1, ORDINAL1, CARD_1, XREAL_1, XXREAL_0,
AFINSQ_2, AFINSQ_1, FUNCT_2, NAT_2, INT_1, NEWTON, BINOP_2, SERIES_1,
SEQ_1, PREPOWER, POWER, XCMPLX_1, PEPIN, PRE_FF, NAT_D;
schemes NAT_1, AFINSQ_2, AFINSQ_1, STIRL2_1;
begin :: Preliminaries
theorem Th1:
for k,l,m being Nat holds (k(#)(l GeoSeq))|m is XFinSequence of NAT
proof
let k,l,m be Nat;
set g=(k(#)(l GeoSeq))|m;
A1: dom (k(#)(l GeoSeq)) = NAT by FUNCT_2:def 1;
then m in dom (k(#)(l GeoSeq)) by ORDINAL1:def 12;
then m c= dom (k(#)(l GeoSeq)) by A1,ORDINAL1:def 2;
then dom g = m by RELAT_1:62;
then reconsider g9=g as XFinSequence by ORDINAL1:def 7;
rng g9 c= NAT
proof
let a be object;
assume a in rng g9;
then consider o being object such that
A2: o in dom g and
A3: a=g.o by FUNCT_1:def 3;
o in dom (k(#)(l GeoSeq)) by A2,RELAT_1:57;
then reconsider o as Element of NAT;
A4: k*(l|^o) in NAT by ORDINAL1:def 12;
g.o = (k(#)(l GeoSeq)).o by A2,FUNCT_1:47
.= k*((l GeoSeq).o) by SEQ_1:9
.= k*(l|^o) by PREPOWER:def 1;
hence thesis by A3,A4;
end;
hence thesis by RELAT_1:def 19;
end;
theorem Th2:
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
proof
let d be XFinSequence of NAT, n be Nat such that
A1: for i being Nat st i in dom d holds n divides d.i;
per cases;
suppose
len d=0;
then d={};
then Sum d = 0;
hence thesis by NAT_D:6;
end;
suppose
A2: len d > 0;
then consider f being sequence of NAT such that
A3: f.0 = d.0 and
A4: for n being Nat st n+1 < len d holds f.(n + 1) = addnat
. (f.n,d.(n + 1)) and
A5: addnat"**" d = f.(len d-1) by AFINSQ_2:def 8;
defpred P[Nat] means $1 < len d implies n divides f.$1;
A6: now
let k be Nat;
assume
A7: P[k];
thus P[k+1]
proof
assume
A8: k+1 < len d;
then k+1 in Segm len d by NAT_1:44;
then
A9: n divides d.(k+1) by A1;
f.(k+1) = addnat.(f.k,d.(k+1)) by A4,A8
.= f.k + d.(k+1) by BINOP_2:def 23;
hence thesis by A7,A8,A9,NAT_1:13,NAT_D:8;
end;
end;
reconsider ld=len d-1 as Element of NAT by A2,NAT_1:20;
A10: ld < len d by XREAL_1:147;
0 in Segm len d by A2,NAT_1:44;
then
A11: P[0] by A1,A3;
A12: addnat"**" d = Sum d by AFINSQ_2:51;
for k being Nat holds P[k] from NAT_1:sch 2(A11,A6);
hence thesis by A5,A10,A12;
end;
end;
theorem Th3:
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
proof
let d,e be XFinSequence of NAT, n be Nat such that
A1: dom d = dom e & for i being Nat st i in dom d holds e.i = d.i mod n;
defpred P[XFinSequence of NAT] means for e being XFinSequence of NAT st dom
$1=dom e & for i being Nat st i in dom $1 holds e.i = $1.i mod n holds (Sum $1)
mod n = (Sum e) mod n;
A2: for p being XFinSequence of NAT,l being Element of NAT st P[p] holds P[p
^<%l%>]
proof
let p be XFinSequence of NAT,l be Element of NAT;
assume
A3: P[p];
thus P[p^<%l%>]
proof
reconsider dop=dom p as Element of NAT by ORDINAL1:def 12;
defpred Q[set,set] means $2=p.$1 mod n;
let e be XFinSequence of NAT;
assume that
A4: dom (p^<%l%>)=dom e and
A5: for i being Nat st i in dom (p^<%l%>) holds e.i = (p^<%l%>).i mod n;
A6: for k being Nat st k in Segm dop ex x being Element of NAT st Q[k,x];
consider p9 being XFinSequence of NAT such that
A7: dom p9 = Segm dop & for k be Nat st k in Segm dop holds Q[k
,p9.k] from STIRL2_1:sch 5(A6);
A8: now
let k be Nat;
assume
A9: k in dom p9;
then k < len p9 by AFINSQ_1:86;
then k < len p + 1 by A7,NAT_1:13;
then k < len p + len <%l%> by AFINSQ_1:33;
then k in Segm(len p + len <%l%>) by NAT_1:44;
then k in dom (p^<%l%>) by AFINSQ_1:def 3;
hence e.k = (p^<%l%>).k mod n by A5
.= p.k mod n by A7,A9,AFINSQ_1:def 3
.= p9.k by A7,A9;
end;
A10: now
let k be Nat;
assume k in dom <%l mod n%>;
then
A11: k in Segm 1 by AFINSQ_1:33;
then k < 1 by NAT_1:44;
then
A12: k = 0 by NAT_1:14;
k in dom <%l%> by A11,AFINSQ_1:33;
hence e.(len p9 + k) = (p^<%l%>).len p mod n by A5,A7,A12,AFINSQ_1:23
.= l mod n by AFINSQ_1:36
.= <%l mod n%>.k by A12;
end;
dom e=len p + len <%l%> by A4,AFINSQ_1:def 3
.= dom p + 1 by AFINSQ_1:33
.= len p9 + len <%l mod n%> by A7,AFINSQ_1:33;
then
A13: e=p9^<%l mod n%> by A8,A10,AFINSQ_1:def 3;
thus Sum (p^<%l%>) mod n = (Sum p + Sum <%l%>) mod n by AFINSQ_2:55
.= (Sum p + l) mod n by AFINSQ_2:53
.= ((Sum p) mod n + l) mod n by NAT_D:22
.= ((Sum p) mod n + (l mod n)) mod n by NAT_D:23
.= ((Sum p9) mod n + (l mod n)) mod n by A3,A7
.= (Sum p9 + (l mod n)) mod n by NAT_D:22
.= (Sum p9 + Sum <%l mod n%>) mod n by AFINSQ_2:53
.= (Sum e) mod n by A13,AFINSQ_2:55;
end;
end;
A14: P[<%>NAT] by AFINSQ_1:15;
for p being XFinSequence of NAT holds P[p] from AFINSQ_2:sch 2(A14,A2 );
hence thesis by A1;
end;
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
:Def1:
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;
existence
proof
deffunc F(Nat)=(d.$1)*(b|^$1);
consider d9 being XFinSequence such that
A1: len d9 = len d & for i being Nat st i in len d holds d9
.i = F(i) from AFINSQ_1:sch 2;
rng d9 c= NAT
proof
let a be object;
assume a in rng d9;
then consider i being object such that
A2: i in dom d9 and
A3: d9.i=a by FUNCT_1:def 3;
reconsider i as Element of NAT by A2;
a=F(i) by A1,A2,A3;
hence thesis by ORDINAL1:def 12;
end;
then reconsider d9 as XFinSequence of NAT by RELAT_1:def 19;
take Sum d9;
thus thesis by A1;
end;
uniqueness
proof
let k,l be Nat;
given k9 being XFinSequence of NAT such that
A4: dom k9 = dom d and
A5: for i being Nat st i in dom k9 holds k9.i = (d.i)*(b|^ i) and
A6: k = Sum k9;
given l9 being XFinSequence of NAT such that
A7: dom l9 = dom d and
A8: for i being Nat st i in dom l9 holds l9.i = (d.i)*(b |^i) and
A9: l = Sum l9;
now
let i be Nat;
assume
A10: i in dom d;
hence k9.i=(d.i)*(b|^i) by A4,A5
.= l9.i by A7,A8,A10;
end;
hence thesis by A4,A6,A7,A9,AFINSQ_1:8;
end;
end;
definition
let n,b be Nat;
assume
A1: b>1;
::$N Unique Representation of Natural Numbers in Positional Numeral Systems
func digits(n,b) -> XFinSequence of NAT means
:Def2:
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%>;
consistency;
existence
proof
reconsider d=<%0%> as XFinSequence of NAT;
reconsider N=n,B=b as Element of NAT by ORDINAL1:def 12;
thus n<>0 implies ex d being XFinSequence of NAT st value(d,b)=n & d.(len(
d)-1) <> 0 & for i being Nat st i in dom d holds 0 <= d.i & d.i < b
proof
deffunc G(Nat,Element of NAT)=$2 div B;
consider f being sequence of NAT such that
A2: f.0=N & for i being Nat holds f.(i+1)=G(i,(f.i) qua Element of
NAT) from NAT_1:sch 12;
defpred R[Nat] means f.$1 = 0;
defpred Q[Nat] means ex i being Nat st f.i = $1;
A3: for k being Nat st k <> 0 & Q[k] ex l being Nat st l < k & Q[l]
proof
let k be Nat;
assume that
A4: k <> 0 and
A5: Q[k];
take l=k div b;
thus l<k by A1,A4,INT_1:56;
consider i being Nat such that
A6: f.i=k by A5;
take i+1;
thus thesis by A2,A6;
end;
A7: ex k being Nat st Q[k] by A2;
Q[0] from NAT_1:sch 7(A7,A3);
then
A8: ex l being Nat st R[l];
consider l being Nat such that
A9: R[l] & for i being Nat st R[i] holds l<=i from NAT_1:sch 5(A8);
assume n<>0;
then consider m being Nat such that
A10: m+1=l by A2,A9,NAT_1:6;
reconsider m as Element of NAT by ORDINAL1:def 12;
dom f=NAT by FUNCT_2:def 1;
then m+1 c= dom f by ORDINAL1:def 2;
then
dom (f|(m+1)) = m+1 by RELAT_1:62;
then reconsider g=f|(m+1) as XFinSequence of NAT by ORDINAL1:def 7;
defpred P[Nat,Nat] means $2=g.$1 mod b;
A11: for i being Nat st i in Segm(m+1) ex x being Element of NAT st P[i,x];
consider d being XFinSequence of NAT such that
A12: dom d = Segm(m+1) & for i be Nat st i in Segm(m+1) holds P[i,
(d.i)] from STIRL2_1:sch 5(A11);
A13: now
let i be Nat such that
l <= i;
assume R[i];
then f.(i+1)=0 div b by A2;
hence R[i+1];
end;
A14: R[l] by A9;
A15: for i being Nat st l <= i holds R[i] from NAT_1:sch 8(A14,A13);
A16: now
let i be Element of NAT;
assume m < i;
then l<=i by A10,NAT_1:13;
hence f.i=0 by A15;
end;
deffunc F(Nat)=(d.$1)*(b|^$1);
consider d9 being XFinSequence such that
A17: len d9 = len d & for i be Nat st i in len d holds
d9.i = F(i) from AFINSQ_1:sch 2;
rng d9 c= NAT
proof
let a be object;
assume a in rng d9;
then consider i being object such that
A18: i in dom d9 and
A19: d9.i=a by FUNCT_1:def 3;
reconsider i as Element of NAT by A18;
a=F(i) by A17,A18,A19;
hence thesis by ORDINAL1:def 12;
end;
then reconsider d9 as XFinSequence of NAT by RELAT_1:def 19;
consider s being sequence of NAT such that
A20: s.0 = d9.0 and
A21: for i being Nat st i+1 < len d9 holds s.(i + 1) =
addnat.(s.i,d9.(i + 1)) and
A22: addnat "**" d9 = s.(len d9-1) by A12,A17,AFINSQ_2:def 8;
defpred I[Nat] means $1<len d9 implies s.$1=n-f.($1+1)*b|^($1+1);
A23: now
let i be Nat;
assume
A24: I[i];
now
assume
A25: i+1<len d9;
then
A26: i+1 in dom d9 by AFINSQ_1:86;
thus s.(i+1)=addnat.(s.i,d9.(i + 1)) by A21,A25
.= n-f.(i+1)*b|^(i+1) + d9.(i+1) by A24,A25,BINOP_2:def 23,NAT_1:13
.= n-f.(i+1)*b|^(i+1) + (d.(i+1)*(b|^(i+1))) by A17,A26
.= n-f.(i+1)*b|^(i+1) + ((g.(i+1) mod b)*(b|^(i+1))) by A12,A17,A26
.= n-f.(i+1)*b|^(i+1) + ((f.(i+1) mod b)*(b|^(i+1))) by A12,A17,A26
,FUNCT_1:49
.= n-f.(i+1)*b|^(i+1) + ((f.(i+1) - b*(f.(i+1) div B))*(b|^(i+1)
)) by A1,NEWTON:63
.= n-f.(i+1)*b|^(i+1) + ((f.(i+1) - b*(f.(i+1+1)))*(b|^(i+1)))
by A2
.= n-f.(i+1)*b|^(i+1) + ((f.(i+1)*(b|^(i+1)) - (f.(i+1+1))*(b*(b
|^(i+1)))))
.= n-f.(i+1)*b|^(i+1) + ((f.(i+1)*(b|^(i+1)) - (f.(i+1+1))*((b|^
(i+1+1))))) by NEWTON:6
.= n-f.(i+1+1)*b|^(i+1+1);
end;
hence I[i+1];
end;
reconsider ld=len d9-1 as Element of NAT by A12,A17;
A27: 0 in Segm(m+1) by NAT_1:44;
then d9.0=(d.0)*(b|^0) by A12,A17
.= (g.0 mod b)*(b|^0) by A12,A27
.= (f.0 mod b)*(b|^0) by A27,FUNCT_1:49
.= (n mod b)*1 by A2,NEWTON:4
.= N-B*(N div B) by A1,NEWTON:63
.= n-(n div b)*b|^1
.= n-f.(0 qua Nat+1)*b|^(0 qua Nat+1) by A2;
then
A28: I[0] by A20;
for i being Nat holds I[i] from NAT_1:sch 2(A28,A23);
then s.(ld)= n-f.(m+1)*b|^(m+1) by A12,A17,XREAL_1:44
.=n by A9,A10;
then
A29: n=Sum d9 by A22,AFINSQ_2:51;
m < l by A10,NAT_1:13;
then
A30: f.m<>0 by A9;
take d;
thus value(d,b)=n by A17,A29,Def1;
m in Segm(m+1) by NAT_1:45;
then
A31: g.m = f.m by FUNCT_1:49;
then m<m+1 & f.(m+1)=g.m div b by A2,NAT_1:13;
then
A32: g.m div b = 0 by A16;
d.(len(d)-1) = g.m mod b by A12,NAT_1:45
.= g.m by A1,A32,NAT_2:12,NAT_D:24;
hence d.(len(d)-1) <> 0 by A30,A31;
let i be Nat;
assume i in dom d;
then d.i=g.i mod b by A12;
hence thesis by A1,NAT_D:1;
end;
assume n=0;
take d;
thus thesis;
end;
uniqueness
proof
reconsider b1=b-1 as Element of NAT by A1,NAT_1:20;
let d,e be XFinSequence of NAT;
thus n<>0 & (value(d,b)=n & d.(len(d)-1) <> 0 & for i being Nat st i in
dom d holds 0 <= d.i & d.i < b) & (value(e,b)=n & e.(len(e)-1) <> 0 & for i
being Nat st i in dom e holds 0 <= e.i & e.i < b) implies d=e
proof
log(2,b)>log(2,1) by A1,POWER:57;
then
A33: log(2,b)>0 by POWER:51;
log(2,b)>log(2,1) by A1,POWER:57;
then
A34: log(2,b)>0 by POWER:51;
A35: 1-b <> 0 by A1;
A36: 1-b <> 0 by A1;
reconsider g=((b1)(#)(b GeoSeq))|len d as XFinSequence of NAT by Th1;
assume
A37: n<>0;
assume that
A38: value(d,b)=n and
A39: d.(len(d)-1) <> 0 and
A40: for i being Nat st i in dom d holds 0 <= d.i & d.i < b;
consider D being XFinSequence of NAT such that
A41: dom D = dom d and
A42: for i being Nat st i in dom D holds D.i = (d.i)*(b|^i) and
A43: n = Sum D by A38,Def1;
dom d <> {} by A39,FUNCT_1:def 2;
then
A44: len D > 0 by A41;
A45: len(d)-1 in dom d by A39,FUNCT_1:def 2;
then reconsider k=len(d)-1 as Element of NAT;
A46: 1*(b|^k)<=(d.k)*(b|^k) by A39,NAT_1:4,14;
A47: b|^k>0 by A1,PREPOWER:6;
D.k = (d.k)*(b|^k) by A41,A42,A45;
then (d.k)*(b|^k) <= n by A41,A43,A45,A44,AFINSQ_2:61;
then b|^k <= n by A46,XXREAL_0:2;
then log(2,b to_power k) <= log(2,n) by A47,PRE_FF:10;
then k*log(2,b) <= log(2,n) by A1,POWER:55;
then k*log(2,b)/log(2,b) <= log(2,n)/log(2,b) by A34,XREAL_1:72;
then
A48: k <= log(2,n)/log(2,b) by A34,XCMPLX_1:89;
g=((b-1)(#)(b GeoSeq))|(k+1);
then
A49: Sum g = Partial_Sums((b-1)(#)(b GeoSeq)).k by AFINSQ_2:56
.= ((b-1)(#)Partial_Sums(b GeoSeq)).k by SERIES_1:9
.= (b-1)*(Partial_Sums(b GeoSeq).k) by SEQ_1:9
.= (b-1)*((1 - (b to_power (k+1)))/(1-b)) by A1,SERIES_1:22
.= -((1-b)*((1 - (b |^ (k+1)))/(1-b)))
.= -(1 - (b |^ (k+1))) by A36,XCMPLX_1:87
.= b|^(k+1)-1;
A50: dom ((b-1)(#)(b GeoSeq)) = NAT by FUNCT_2:def 1;
then
A51: len D = len g by A41,RELAT_1:62;
len d c= dom ((b-1)(#)(b GeoSeq)) by A50,ORDINAL1:def 2;
then
A52: dom g = len d by RELAT_1:62;
A53: for i being Nat st i in dom D holds D.i <= g.i
proof
let i be Nat;
reconsider I=i as Element of NAT by ORDINAL1:def 12;
assume
A54: i in dom D;
then
A55: D.i = (d.i)*(b|^i) by A42;
d.i < b1+1 by A40,A41,A54;
then
A56: d.i <= b1 by NAT_1:13;
g.I = ((b-1)(#)(b GeoSeq)).I by A41,A52,A54,FUNCT_1:47
.= (b-1)*((b GeoSeq).I) by SEQ_1:9
.= b1*(b|^I) by PREPOWER:def 1;
hence thesis by A56,A55,XREAL_1:64;
end;
assume that
A57: value(e,b)=n and
A58: e.(len(e)-1) <> 0 and
A59: for i being Nat st i in dom e holds 0 <= e.i & e.i < b;
consider E being XFinSequence of NAT such that
A60: dom E = dom e and
A61: for i being Nat st i in dom E holds E.i = (e.i)*(b|^i) and
A62: n = Sum E by A57,Def1;
A63: len(e)-1 in dom e by A58,FUNCT_1:def 2;
then reconsider l=len(e)-1 as Element of NAT;
A64: 1*(b|^l)<=(e.l)*(b|^l) by A58,NAT_1:4,14;
reconsider g=((b1)(#)(b GeoSeq))|len e as XFinSequence of NAT by Th1;
g=((b-1)(#)(b GeoSeq))|(l+1);
then
A65: Sum g = Partial_Sums((b-1)(#)(b GeoSeq)).l by AFINSQ_2:56
.= ((b-1)(#)Partial_Sums(b GeoSeq)).l by SERIES_1:9
.= (b-1)*(Partial_Sums(b GeoSeq).l) by SEQ_1:9
.= (b-1)*((1 - (b to_power (l+1)))/(1-b)) by A1,SERIES_1:22
.= -((1-b)*((1 - (b |^ (l+1)))/(1-b)))
.= -(1 - (b |^ (l+1))) by A35,XCMPLX_1:87
.= b|^(l+1)-1;
dom E <> {} by A58,A60,FUNCT_1:def 2;
then
A66: len E > 0;
A67: dom ((b-1)(#)(b GeoSeq)) = NAT by FUNCT_2:def 1;
then len e c= dom ((b-1)(#)(b GeoSeq)) by ORDINAL1:def 2;
then
A68: dom g = len e by RELAT_1:62;
A69: for i being Nat st i in dom E holds E.i <= g.i
proof
let i be Nat;
reconsider I=i as Element of NAT by ORDINAL1:def 12;
assume
A70: i in dom E;
then
A71: E.i = (e.i)*(b|^i) by A61;
e.i < b1+1 by A59,A60,A70;
then
A72: e.i <= b1 by NAT_1:13;
g.I = ((b-1)(#)(b GeoSeq)).I by A60,A68,A70,FUNCT_1:47
.= (b-1)*((b GeoSeq).I) by SEQ_1:9
.= b1*(b|^I) by PREPOWER:def 1;
hence thesis by A72,A71,XREAL_1:64;
end;
A73: b|^l>0 by A1,PREPOWER:6;
E.l = (e.l)*(b|^l) by A60,A61,A63;
then (e.l)*(b|^l) <= n by A60,A62,A63,A66,AFINSQ_2:61;
then b|^l <= n by A64,XXREAL_0:2;
then log(2,b to_power l) <= log(2,n) by A73,PRE_FF:10;
then l*log(2,b) <= log(2,n) by A1,POWER:55;
then l*log(2,b)/log(2,b) <= log(2,n)/log(2,b) by A33,XREAL_1:72;
then
A74: l <= log(2,n)/log(2,b) by A33,XCMPLX_1:89;
len E = len g by A60,A67,RELAT_1:62;
then n < b|^(l+1)-1+1 by A62,A65,A69,AFINSQ_2:57,XREAL_1:39;
then log(2,n) < log(2,b to_power (l+1)) by A37,POWER:57;
then log(2,n) < (l+1)*log(2,b) by A1,POWER:55;
then log(2,n)/log(2,b) < (l+1)*log(2,b)/log(2,b) by A33,XREAL_1:74;
then log(2,n)/log(2,b) < l+1 by A33,XCMPLX_1:89;
then k<l+1 by A48,XXREAL_0:2;
then
A75: k<=l by NAT_1:13;
n < b|^(k+1)-1+1 by A43,A49,A51,A53,AFINSQ_2:57,XREAL_1:39;
then log(2,n) < log(2,b to_power (k+1)) by A37,POWER:57;
then log(2,n) < (k+1)*log(2,b) by A1,POWER:55;
then log(2,n)/log(2,b) < (k+1)*log(2,b)/log(2,b) by A34,XREAL_1:74;
then log(2,n)/log(2,b) < k+1 by A34,XCMPLX_1:89;
then l<k+1 by A74,XXREAL_0:2;
then l<=k by NAT_1:13;
then
A76: k=l by A75,XXREAL_0:1;
now
let a be object;
assume
A77: a in dom d;
then reconsider o=a as Element of NAT;
o<k+1 by A77,AFINSQ_1:86;
then
A78: o<=k by NAT_1:13;
A79: o < len d by A77,AFINSQ_1:86;
then reconsider oo=len d - o as Element of NAT by NAT_1:21;
per cases by A78,XXREAL_0:1;
suppose
A80: o = 0 & o = k;
then len E = 1 by A60,A76;
then
A81: E = <%E.0%> by AFINSQ_1:34
.= <%e.0*b|^0%> by A60,A61,A76,A77,A80
.= <%e.0*1%> by NEWTON:4;
len D = 1 by A41,A80;
then D = <%D.0%> by AFINSQ_1:34
.= <%d.0*b|^0%> by A41,A42,A77,A80
.= <%d.0*1%> by NEWTON:4;
hence d.a = n by A43,A80,AFINSQ_2:53
.= e.a by A62,A80,A81,AFINSQ_2:53;
end;
suppose
A82: o = 0 & o < k;
reconsider co=<%>NAT as XFinSequence of NAT;
Sum co = 0;
then
A83: Sum co div (b|^o) = 0;
set d9=D;
D=co^d9;
then
A84: n = Sum co + Sum d9 by A43,AFINSQ_2:55;
reconsider bo=b|^o as Element of NAT by ORDINAL1:def 12;
A85: bo <> 0 by A1,PREPOWER:5;
A86: now
let k be Nat;
assume k in dom <%D.o%>;
then k in Segm 1 by AFINSQ_1:33;
then k < 1 by NAT_1:44;
then k=0 by NAT_1:14;
hence d9.k = <%D.o%>.k by A82;
end;
reconsider o1=o+1 as Element of NAT;
o1 <= k by A82,NAT_1:13;
then
A87: o1 < len d by XREAL_1:147;
reconsider oo1=len d - o1 as Element of NAT by A82;
defpred P[Nat,set] means $2=D.($1+o1);
reconsider do1=D|o1 as XFinSequence of NAT;
A88: for u being Nat st u in Segm oo1 ex x be Element of NAT st P[u,x];
consider d91 being XFinSequence of NAT such that
A89: dom d91=Segm oo1 & for x be Nat st x in Segm oo1 holds
P[x,d91.x] from STIRL2_1:sch 5(A88);
A90: len d = len D by A41;
then
A91: len do1=o1 by A87,AFINSQ_1:11;
then A92: dom D = len do1 + len d91 by A41,A89;
now
let k be Nat;
reconsider K=k as Element of NAT by ORDINAL1:def 12;
assume
A93: k in dom d91;
then k < len d91 by AFINSQ_1:86;
then o1+k < len D by A91,A92,XREAL_1:8;
then o1+k in dom D by AFINSQ_1:86;
then D.(o1+k) = d.(o1+k)*b|^(o1+k) by A42;
then d91.K = d.(o1+k)*b|^(o1+k) by A89,A93
.= d.(o1+k)*(b|^o1*b|^k) by NEWTON:8
.= (d.(o1+k)*(b|^k))*(b|^o1);
hence b|^o1 divides d91.k by NAT_D:def 3;
end;
then
A94: b|^o1 divides Sum d91 by Th2;
A95: now
let k be Nat;
assume
A96: k in dom d91;
thus d9.(len <%D.o%> + k) = D.(len do1 + k) by A82,A91,AFINSQ_1:33
.= d91.k by A89,A91,A96;
end;
dom d9= 1 + dom d91 by A41,A82,A89
.= len <%D.o%> + len d91 by AFINSQ_1:34;
then d9=<%D.o%>^d91 by A86,A95,AFINSQ_1:def 3;
then
A97: Sum d9 = Sum <%D.o%> + Sum d91 by AFINSQ_2:55;
( for x being Nat st x in dom do1 holds D.x=do1.x)&
for x being Nat st x in dom d91 holds D.(len do1+x)=d91.x by A89,A91,FUNCT_1:47
;
then D=do1^d91 by A92,AFINSQ_1:def 3;
then
A98: n = Sum do1 + Sum d91 by A43,AFINSQ_2:55;
reconsider bo1=b|^o1 as Element of NAT by ORDINAL1:def 12;
consider ok1 being Nat such that
A99: ok1+1=o1;
now
let k be Nat;
reconsider K=k as Element of NAT by ORDINAL1:def 12;
assume k in dom d9;
then d9.K = d.(o+k)*b|^(o+k) by A42,A82
.= d.(o+k)*(b|^o*b|^k) by NEWTON:8
.= (d.(o+k)*(b|^k))*(b|^o);
hence b|^o divides d9.k by NAT_D:def 3;
end;
then
A100: b|^o divides Sum d9 by Th2;
then Sum d9 mod (b|^o) = 0 by A85,PEPIN:6;
then n div (b|^o) = (Sum d9 div (b|^o)) + (Sum co div (b|^o)) by A84,
NAT_D:19;
then
A101: (n div (b|^o)) * b|^o = Sum d9 by A83,A100,NAT_D:3;
reconsider co=<%>NAT as XFinSequence of NAT;
Sum co = 0;
then
A102: Sum co div (b|^o) = 0;
set d9=E;
E=co^d9;
then
A103: n = Sum co + Sum d9 by A62,AFINSQ_2:55;
reconsider bo=b|^o as Element of NAT by ORDINAL1:def 12;
A104: bo <> 0 by A1,PREPOWER:5;
reconsider ok1 as Element of NAT by ORDINAL1:def 12;
reconsider g1=((b1)(#)(b GeoSeq))|(ok1+1) as XFinSequence of NAT by
Th1;
A105: 1-b <> 0 by A1;
dom ((b-1)(#)(b GeoSeq)) = NAT by FUNCT_2:def 1;
then
A106: o1 c= dom ((b-1)(#)(b GeoSeq)) by ORDINAL1:def 2;
then
A107: len do1 = len g1 by A91,A99,RELAT_1:62;
A108: dom g1 = o1 by A99,A106,RELAT_1:62;
A109: for i being Nat st i in dom do1 holds do1.i <= g1.i
proof
let i be Nat;
reconsider I=i as Element of NAT by ORDINAL1:def 12;
assume
A110: i in dom do1;
then i in o1 by A87,A90,AFINSQ_1:11;
then
A111: g1.I = ((b-1)(#)(b GeoSeq)).I by A108,FUNCT_1:47
.= (b-1)*((b GeoSeq).I) by SEQ_1:9
.= b1*(b|^I) by PREPOWER:def 1;
A112: dom do1 c= dom D by RELAT_1:60;
then d.i < b1+1 by A40,A41,A110;
then
A113: d.i <= b1 by NAT_1:13;
do1.i = D.i by A110,FUNCT_1:47
.= (d.i)*(b|^i) by A42,A110,A112;
hence thesis by A111,A113,XREAL_1:64;
end;
Sum g1 = Partial_Sums((b-1)(#)(b GeoSeq)).ok1 by AFINSQ_2:56
.= ((b-1)(#)Partial_Sums(b GeoSeq)).ok1 by SERIES_1:9
.= (b-1)*(Partial_Sums(b GeoSeq).ok1) by SEQ_1:9
.= (b-1)*((1 - (b to_power (ok1+1)))/(1-b)) by A1,SERIES_1:22
.= -((1-b)*((1 - (b |^ o1))/(1-b))) by A99
.= -(1 - (b |^ o1)) by A105,XCMPLX_1:87
.= b|^o1-1;
then Sum do1 < b|^o1 -1 + 1 by A107,A109,AFINSQ_2:57,XREAL_1:145;
then
A114: Sum do1 div (b|^o1) = 0 by NAT_D:27;
bo1 <> 0 by A1,PREPOWER:5;
then Sum d91 mod (b|^o1) = 0 by A94,PEPIN:6;
then n div (b|^o1) = (Sum d91 div (b|^o1)) + (Sum do1 div (b|^o1))
by A98,NAT_D:19;
then (n div (b|^o1)) * b|^o1 = Sum d91 by A114,A94,NAT_D:3;
then D.o = (n div (b|^o)) * b|^o - (n div (b|^o1)) * b|^o1 by A101
,A97,AFINSQ_2:53;
then d.o*b|^o = (n div (b|^o)) * b|^o - (n div (b|^o1)) * b|^o1 by
A41,A42,A77;
then d.o*b|^o = (n div (b|^o)) * b|^o - (n div (b|^o1)) * (b|^o*b|^
1 ) by NEWTON:8;
then d.o*b|^o = b|^o*((n div (b|^o)) - (n div (b|^o1)) * b|^1);
then (b|^o*d.o)/b|^o = (b|^o*((n div (b|^o)) - (n div (b|^o1)) * b)
) /b|^o;
then
A115: d.o = (b|^o*((n div (b|^o)) - (n div (b|^o1)) * b))/b |^o by A85,
XCMPLX_1:89;
reconsider o1=o+1 as Element of NAT;
reconsider do1=E|o1 as XFinSequence of NAT;
A116: len e = len E by A60;
now
let k be Nat;
reconsider K=k as Element of NAT by ORDINAL1:def 12;
assume k in dom d9;
then d9.K = e.(o+k)*b|^(o+k) by A61,A82
.= e.(o+k)*(b|^o*b|^k) by NEWTON:8
.= (e.(o+k)*(b|^k))*(b|^o);
hence b|^o divides d9.k by NAT_D:def 3;
end;
then
A117: b|^o divides Sum d9 by Th2;
then Sum d9 mod (b|^o) = 0 by A104,PEPIN:6;
then n div (b|^o) = (Sum d9 div (b|^o)) + (Sum co div (b|^o)) by A103
,NAT_D:19;
then
A118: (n div (b|^o)) * b|^o = Sum d9 by A102,A117,NAT_D:3;
A119: now
let k be Nat;
assume k in dom <%E.o%>;
then k in Segm 1 by AFINSQ_1:33;
then k < 1 by NAT_1:44;
then k=0 by NAT_1:14;
hence d9.k = <%E.o%>.k by A82;
end;
reconsider oo1=len d - o1 as Element of NAT by A82;
defpred P[Nat,set] means $2=E.($1+o1);
A120: for u being Nat st u in Segm oo1 ex x be Element of NAT st P[u,x];
consider d91 being XFinSequence of NAT such that
A121: dom d91=Segm oo1 & for x being Nat st x in Segm oo1 holds
P[x,d91.x] from STIRL2_1:sch 5(A120);
o1 <= k by A82,NAT_1:13;
then
A122: o1 < len d by XREAL_1:147;
then
A123: len do1=o1 by A76,A116,AFINSQ_1:11;
A124: now
let k be Nat;
assume
A125: k in dom d91;
thus d9.(len <%E.o%> + k) = E.(len do1 + k) by A82,A123,AFINSQ_1:33
.= d91.k by A121,A123,A125;
end;
reconsider bo1=b|^o1 as Element of NAT by ORDINAL1:def 12;
consider ok1 being Nat such that
A126: ok1+1=o1;
A127: dom E = len do1 + len d91 by A60,A76,A121,A123;
now
let k be Nat;
reconsider K=k as Element of NAT by ORDINAL1:def 12;
assume
A128: k in dom d91;
then k < len d91 by AFINSQ_1:86;
then o1+k < len E by A123,A127,XREAL_1:8;
then o1+k in dom E by AFINSQ_1:86;
then E.(o1+k) = e.(o1+k)*b|^(o1+k) by A61;
then d91.K = e.(o1+k)*b|^(o1+k) by A121,A128
.= e.(o1+k)*(b|^o1*b|^k) by NEWTON:8
.= (e.(o1+k)*(b|^k))*(b|^o1);
hence b|^o1 divides d91.k by NAT_D:def 3;
end;
then
A129: b|^o1 divides Sum d91 by Th2;
reconsider ok1 as Element of NAT by ORDINAL1:def 12;
reconsider g1=((b1)(#)(b GeoSeq))|(ok1+1) as XFinSequence of NAT by
Th1;
A130: 1-b <> 0 by A1;
dom ((b-1)(#)(b GeoSeq)) = NAT by FUNCT_2:def 1;
then
A131: o1 c= dom ((b-1)(#)(b GeoSeq)) by ORDINAL1:def 2;
then
A132: len do1 = len g1 by A123,A126,RELAT_1:62;
A133: dom g1 = o1 by A126,A131,RELAT_1:62;
A134: for i being Nat st i in dom do1 holds do1.i <= g1.i
proof
let i be Nat;
reconsider I=i as Element of NAT by ORDINAL1:def 12;
assume
A135: i in dom do1;
then i in o1 by A76,A122,A116,AFINSQ_1:11;
then
A136: g1.I = ((b-1)(#)(b GeoSeq)).I by A133,FUNCT_1:47
.= (b-1)*((b GeoSeq).I) by SEQ_1:9
.= b1*(b|^I) by PREPOWER:def 1;
A137: dom do1 c= dom E by RELAT_1:60;
then e.i < b1+1 by A59,A60,A135;
then
A138: e.i <= b1 by NAT_1:13;
do1.i = E.i by A135,FUNCT_1:47
.= (e.i)*(b|^i) by A61,A135,A137;
hence thesis by A136,A138,XREAL_1:64;
end;
Sum g1 = Partial_Sums((b-1)(#)(b GeoSeq)).ok1 by AFINSQ_2:56
.= ((b-1)(#)Partial_Sums(b GeoSeq)).ok1 by SERIES_1:9
.= (b-1)*(Partial_Sums(b GeoSeq).ok1) by SEQ_1:9
.= (b-1)*((1 - (b to_power (ok1+1)))/(1-b)) by A1,SERIES_1:22
.= -((1-b)*((1 - (b |^ o1))/(1-b))) by A126
.= -(1 - (b |^ o1)) by A130,XCMPLX_1:87
.= b|^o1-1;
then Sum do1 < b|^o1 -1 + 1 by A132,A134,AFINSQ_2:57,XREAL_1:145;
then
A139: Sum do1 div (b|^o1) = 0 by NAT_D:27;
( for x being Nat st x in dom do1 holds E.x=do1.x)&
for x being Nat st x in dom d91 holds E.(len do1+x)=d91.x by A121,A123,
FUNCT_1:47;
then E=do1^d91 by A127,AFINSQ_1:def 3;
then
A140: n = Sum do1 + Sum d91 by A62,AFINSQ_2:55;
bo1 <> 0 by A1,PREPOWER:5;
then Sum d91 mod (b|^o1) = 0 by A129,PEPIN:6;
then n div (b|^o1) = (Sum d91 div (b|^o1)) + (Sum do1 div (b|^o1))
by A140,NAT_D:19;
then
A141: (n div (b|^o1)) * b|^o1 = Sum d91 by A139,A129,NAT_D:3;
dom d9= 1 + dom d91 by A60,A76,A82,A121
.= len <%E.o%> + len d91 by AFINSQ_1:34;
then d9=<%E.o%>^d91 by A119,A124,AFINSQ_1:def 3;
then Sum d9 = Sum <%E.o%> + Sum d91 by AFINSQ_2:55;
then E.o = (n div (b|^o)) * b|^o - (n div (b|^o1)) * b|^o1 by A118
,A141,AFINSQ_2:53;
then e.o*b|^o = (n div (b|^o)) * b|^o - (n div (b|^o1)) * b|^o1 by
A60,A61,A76,A77;
then e.o*b|^o = (n div (b|^o)) * b|^o - (n div (b|^o1)) * (b|^o*b|^
1 ) by NEWTON:8;
then e.o*b|^o = b|^o*((n div (b|^o)) - (n div (b|^o1)) * b|^1);
then (b|^o*e.o)/b|^o = (b|^o*((n div (b|^o)) - (n div (b|^o1)) * b)
) /b|^o;
hence d.a=e.a by A115,A104,XCMPLX_1:89;
end;
suppose
A142: o>0 & o = k;
set d9=<%D.o%>;
reconsider co=D|o as XFinSequence of NAT;
A143: len d = len D by A41;
then
A144: len co=o by A79,AFINSQ_1:11;
A145: len d9=oo by A142,AFINSQ_1:34;
then
A146: dom D = len co + len d9 by A41,A144;
A147: for x being Nat st x in dom d9 holds D.(len co+x)= d9 .x
proof
let x be Nat;
assume x in dom d9;
then x < 1 by A142,A145,AFINSQ_1:86;
then x = 0 by NAT_1:14;
hence thesis by A144;
end;
now
let k be Nat;
reconsider K=k as Element of NAT by ORDINAL1:def 12;
assume
A148: k in dom d9;
then k < len d9 by AFINSQ_1:86;
then o+k < len D by A144,A146,XREAL_1:8;
then o+k in dom D by AFINSQ_1:86;
then D.(o+k) = d.(o+k)*b|^(o+k) by A42;
then d9.K = d.(o+k)*b|^(o+k) by A144,A147,A148
.= d.(o+k)*(b|^o*b|^k) by NEWTON:8
.= (d.(o+k)*(b|^k))*(b|^o);
hence b|^o divides d9.k by NAT_D:def 3;
end;
then
A149: b|^o divides Sum d9 by Th2;
reconsider bo=b|^o as Element of NAT by ORDINAL1:def 12;
A150: 1-b <> 0 by A1;
consider ok being Nat such that
A151: ok+1=o by A142,NAT_1:6;
reconsider ok as Element of NAT by ORDINAL1:def 12;
reconsider g=((b1)(#)(b GeoSeq))|(ok+1) as XFinSequence of NAT by Th1
;
A152: Sum g = Partial_Sums((b-1)(#)(b GeoSeq)).ok by AFINSQ_2:56
.= ((b-1)(#)Partial_Sums(b GeoSeq)).ok by SERIES_1:9
.= (b-1)*(Partial_Sums(b GeoSeq).ok) by SEQ_1:9
.= (b-1)*((1 - (b to_power (ok+1)))/(1-b)) by A1,SERIES_1:22
.= -((1-b)*((1 - (b |^ o))/(1-b))) by A151
.= -(1 - (b |^ o)) by A150,XCMPLX_1:87
.= b|^o-1;
consider ok being Nat such that
A153: ok+1=o by A142,NAT_1:6;
dom ((b-1)(#)(b GeoSeq)) = NAT by FUNCT_2:def 1;
then
A154: o c= dom ((b-1)(#)(b GeoSeq)) by ORDINAL1:def 2;
then
A155: dom g = o by A151,RELAT_1:62;
A156: for i being Nat st i in dom co holds co.i <= g.i
proof
let i be Nat;
reconsider I=i as Element of NAT by ORDINAL1:def 12;
assume
A157: i in dom co;
then i in o by A79,A143,AFINSQ_1:11;
then
A158: g.I = ((b-1)(#)(b GeoSeq)).I by A155,FUNCT_1:47
.= (b-1)*((b GeoSeq).I) by SEQ_1:9
.= b1*(b|^I) by PREPOWER:def 1;
A159: dom co c= dom D by RELAT_1:60;
then d.i < b1+1 by A40,A41,A157;
then
A160: d.i <= b1 by NAT_1:13;
co.i = D.i by A157,FUNCT_1:47
.= (d.i)*(b|^i) by A42,A157,A159;
hence thesis by A158,A160,XREAL_1:64;
end;
len co = len g by A144,A151,A154,RELAT_1:62;
then Sum co < b|^o -1 + 1 by A152,A156,AFINSQ_2:57,XREAL_1:145;
then
A161: Sum co div (b|^o) = 0 by NAT_D:27;
for x being Nat st x in dom co holds D.x=co.x by FUNCT_1:47;
then D=co^d9 by A146,A147,AFINSQ_1:def 3;
then
A162: n = Sum co + Sum d9 by A43,AFINSQ_2:55;
A163: bo <> 0 by A1,PREPOWER:5;
then Sum d9 mod (b|^o) = 0 by A149,PEPIN:6;
then n div (b|^o) = (Sum d9 div (b|^o)) + (Sum co div (b|^o)) by A162
,NAT_D:19;
then (n div (b|^o)) * b|^o = Sum d9 by A161,A149,NAT_D:3;
then D.o = (n div (b|^o)) * b|^o by AFINSQ_2:53;
then d.o*b|^o/b|^o = (n div (b|^o)) * b|^o/b|^o by A41,A42,A77;
then
A164: d.o = (n div (b|^o)) * b|^o/b|^o by A163,XCMPLX_1:89;
set d9=<%E.o%>;
reconsider co=E|o as XFinSequence of NAT;
A165: len e = len E by A60;
then
A166: len co=o by A76,A79,AFINSQ_1:11;
A167: len d9=oo by A142,AFINSQ_1:34;
then
A168: dom E = len co + len d9 by A60,A76,A166;
A169: for x being Nat st x in dom d9 holds E.(len co+x)= d9 .x
proof
let x be Nat;
assume x in dom d9;
then x < 1 by A142,A167,AFINSQ_1:86;
then x = 0 by NAT_1:14;
hence thesis by A166;
end;
now
let k be Nat;
reconsider K=k as Element of NAT by ORDINAL1:def 12;
assume
A170: k in dom d9;
then k < len d9 by AFINSQ_1:86;
then o+k < len E by A166,A168,XREAL_1:8;
then o+k in dom E by AFINSQ_1:86;
then E.(o+k) = e.(o+k)*b|^(o+k) by A61;
then d9.K = e.(o+k)*b|^(o+k) by A166,A169,A170
.= e.(o+k)*(b|^o*b|^k) by NEWTON:8
.= (e.(o+k)*(b|^k))*(b|^o);
hence b|^o divides d9.k by NAT_D:def 3;
end;
then
A171: b|^o divides Sum d9 by Th2;
reconsider ok as Element of NAT by ORDINAL1:def 12;
reconsider g=((b1)(#)(b GeoSeq))|(ok+1) as XFinSequence of NAT by Th1
;
reconsider bo=b|^o as Element of NAT by ORDINAL1:def 12;
A172: 1-b <> 0 by A1;
dom ((b-1)(#)(b GeoSeq)) = NAT by FUNCT_2:def 1;
then
A173: o c= dom ((b-1)(#)(b GeoSeq)) by ORDINAL1:def 2;
then
A174: len co = len g by A166,A153,RELAT_1:62;
A175: dom g = o by A153,A173,RELAT_1:62;
A176: for i being Nat st i in dom co holds co.i <= g.i
proof
let i be Nat;
reconsider I=i as Element of NAT by ORDINAL1:def 12;
assume
A177: i in dom co;
then i in o by A76,A79,A165,AFINSQ_1:11;
then
A178: g.I = ((b-1)(#)(b GeoSeq)).I by A175,FUNCT_1:47
.= (b-1)*((b GeoSeq).I) by SEQ_1:9
.= b1*(b|^I) by PREPOWER:def 1;
A179: dom co c= dom E by RELAT_1:60;
then e.i < b1+1 by A59,A60,A177;
then
A180: e.i <= b1 by NAT_1:13;
co.i = E.i by A177,FUNCT_1:47
.= (e.i)*(b|^i) by A61,A177,A179;
hence thesis by A178,A180,XREAL_1:64;
end;
Sum g = Partial_Sums((b-1)(#)(b GeoSeq)).ok by AFINSQ_2:56
.= ((b-1)(#)Partial_Sums(b GeoSeq)).ok by SERIES_1:9
.= (b-1)*(Partial_Sums(b GeoSeq).ok) by SEQ_1:9
.= (b-1)*((1 - (b to_power (ok+1)))/(1-b)) by A1,SERIES_1:22
.= -((1-b)*((1 - (b |^ o))/(1-b))) by A153
.= -(1 - (b |^ o)) by A172,XCMPLX_1:87
.= b|^o-1;
then Sum co < b|^o -1 + 1 by A174,A176,AFINSQ_2:57,XREAL_1:145;
then
A181: Sum co div (b|^o) = 0 by NAT_D:27;
for x being Nat st x in dom co holds E.x=co.x by FUNCT_1:47;
then E=co^d9 by A168,A169,AFINSQ_1:def 3;
then
A182: n = Sum co + Sum d9 by A62,AFINSQ_2:55;
A183: bo <> 0 by A1,PREPOWER:5;
then Sum d9 mod (b|^o) = 0 by A171,PEPIN:6;
then n div (b|^o) = (Sum d9 div (b|^o)) + (Sum co div (b|^o)) by A182
,NAT_D:19;
then (n div (b|^o)) * b|^o = Sum d9 by A181,A171,NAT_D:3;
then E.o = (n div (b|^o)) * b|^o by AFINSQ_2:53;
then e.o*b|^o/b|^o = (n div (b|^o)) * b|^o/b|^o by A60,A61,A76,A77;
hence d.a=e.a by A164,A183,XCMPLX_1:89;
end;
suppose
A184: o>0 & o < k;
reconsider o1=o+1 as Element of NAT;
A185: o1 <= k by A184,NAT_1:13;
then
A186: o1 < len d by XREAL_1:147;
reconsider bo1=b|^o1 as Element of NAT by ORDINAL1:def 12;
reconsider do1=D|o1 as XFinSequence of NAT;
reconsider bo=b|^o as Element of NAT by ORDINAL1:def 12;
defpred P[Nat,set] means $2=D.($1+o);
consider ok1 being Nat such that
A187: ok1+1=o1;
reconsider ok1 as Element of NAT by ORDINAL1:def 12;
reconsider g1=((b1)(#)(b GeoSeq))|(ok1+1) as XFinSequence of NAT by
Th1;
A188: len d = len D by A41;
then
A189: len do1=o1 by A186,AFINSQ_1:11;
dom ((b-1)(#)(b GeoSeq)) = NAT by FUNCT_2:def 1;
then
A190: o1 c= dom ((b-1)(#)(b GeoSeq)) by ORDINAL1:def 2;
then
A191: len do1 = len g1 by A189,A187,RELAT_1:62;
A192: dom g1 = o1 by A187,A190,RELAT_1:62;
A193: for i being Nat st i in dom do1 holds do1.i <= g1.i
proof
let i be Nat;
reconsider I=i as Element of NAT by ORDINAL1:def 12;
assume
A194: i in dom do1;
then i in o1 by A186,A188,AFINSQ_1:11;
then
A195: g1.I = ((b-1)(#)(b GeoSeq)).I by A192,FUNCT_1:47
.= (b-1)*((b GeoSeq).I) by SEQ_1:9
.= b1*(b|^I) by PREPOWER:def 1;
A196: dom do1 c= dom D by RELAT_1:60;
then d.i < b1+1 by A40,A41,A194;
then
A197: d.i <= b1 by NAT_1:13;
do1.i = D.i by A194,FUNCT_1:47
.= (d.i)*(b|^i) by A42,A194,A196;
hence thesis by A195,A197,XREAL_1:64;
end;
k < len d by XREAL_1:147;
then reconsider oo1=len d - o1 as Element of NAT by A185,NAT_1:21
,XXREAL_0:2;
A198: for u be Nat st u in Segm oo ex x be Element of NAT st P[u,x];
consider d9 being XFinSequence of NAT such that
A199: dom d9=Segm oo & for x being Nat st x in Segm oo holds P[
x,d9.x] from STIRL2_1:sch 5(A198);
A200: now
let k be Nat;
assume k in dom <%D.o%>;
then k in Segm 1 by AFINSQ_1:33;
then k < 1 by NAT_1:44;
then
A201: k=0 by NAT_1:14;
then len d9 > k by A79,XREAL_1:50,A199;
then k in dom d9 by A199,NAT_1:44;
hence d9.k=D.(k+o) by A199
.= <%D.o%>.k by A201;
end;
defpred P[Nat,set] means $2=D.($1+o1);
A202: for u being Nat st u in Segm oo1 ex x be Element of NAT st P[u,x];
consider d91 being XFinSequence of NAT such that
A203: dom d91=Segm oo1 & for x being Nat st x in Segm oo1 holds
P[x,d91.x] from STIRL2_1:sch 5(A202);
reconsider co=D|o as XFinSequence of NAT;
A204: len d = len D by A41;
then
A205: len co=o by A79,AFINSQ_1:11;
then A206: dom D = len co + len d9 by A41,A199;
now
let k be Nat;
reconsider K=k as Element of NAT by ORDINAL1:def 12;
assume
A207: k in dom d9;
then k < len d9 by AFINSQ_1:86;
then o+k < len D by A205,A206,XREAL_1:8;
then o+k in dom D by AFINSQ_1:86;
then D.(o+k) = d.(o+k)*b|^(o+k) by A42;
then d9.K = d.(o+k)*b|^(o+k) by A199,A207
.= d.(o+k)*(b|^o*b|^k) by NEWTON:8
.= (d.(o+k)*(b|^k))*(b|^o);
hence b|^o divides d9.k by NAT_D:def 3;
end;
then
A208: b|^o divides Sum d9 by Th2;
( for x being Nat st x in dom co holds D.x=co.x)&
for x being Nat st x in dom d9 holds D.(len co+x)=d9 .x by A199,A205,FUNCT_1:47
;
then D=co^d9 by A206,AFINSQ_1:def 3;
then
A209: n = Sum co + Sum d9 by A43,AFINSQ_2:55;
consider ok being Nat such that
A210: ok+1=o by A184,NAT_1:6;
reconsider ok as Element of NAT by ORDINAL1:def 12;
reconsider g=((b1)(#)(b GeoSeq))|(ok+1) as XFinSequence of NAT by Th1
;
A211: 1-b <> 0 by A1;
A212: Sum g = Partial_Sums((b-1)(#)(b GeoSeq)).ok by AFINSQ_2:56
.= ((b-1)(#)Partial_Sums(b GeoSeq)).ok by SERIES_1:9
.= (b-1)*(Partial_Sums(b GeoSeq).ok) by SEQ_1:9
.= (b-1)*((1 - (b to_power (ok+1)))/(1-b)) by A1,SERIES_1:22
.= -((1-b)*((1 - (b |^ o))/(1-b))) by A210
.= -(1 - (b |^ o)) by A211,XCMPLX_1:87
.= b|^o-1;
dom ((b-1)(#)(b GeoSeq)) = NAT by FUNCT_2:def 1;
then
A213: o c= dom ((b-1)(#)(b GeoSeq)) by ORDINAL1:def 2;
then
A214: dom g = o by A210,RELAT_1:62;
A215: for i being Nat st i in dom co holds co.i <= g.i
proof
let i be Nat;
reconsider I=i as Element of NAT by ORDINAL1:def 12;
assume
A216: i in dom co;
then i in o by A79,A204,AFINSQ_1:11;
then
A217: g.I = ((b-1)(#)(b GeoSeq)).I by A214,FUNCT_1:47
.= (b-1)*((b GeoSeq).I) by SEQ_1:9
.= b1*(b|^I) by PREPOWER:def 1;
A218: dom co c= dom D by RELAT_1:60;
then d.i < b1+1 by A40,A41,A216;
then
A219: d.i <= b1 by NAT_1:13;
co.i = D.i by A216,FUNCT_1:47
.= (d.i)*(b|^i) by A42,A216,A218;
hence thesis by A217,A219,XREAL_1:64;
end;
A220: now
let k be Nat;
assume
A221: k in dom d91;
then k < len d91 by A203,NAT_1:44;
then k+1 < oo1+1 by XREAL_1:8,A203;
then k+1 < len d9 by A199;
then
A222: k+1 in dom d9 by A199,NAT_1:44;
thus d9.(len <%D.o%> + k) = d9.(1 + k) by AFINSQ_1:33
.= D.(len co+(k+1)) by A199,A205,A222
.= D.(len do1 + k) by A205,A189
.= d91.k by A203,A189,A221;
end;
dom d9 = 1 + dom d91 by A199,A203
.= len <%D.o%> + len d91 by AFINSQ_1:34;
then d9=<%D.o%>^d91 by A200,A220,AFINSQ_1:def 3;
then
A223: Sum d9 = Sum <%D.o%> + Sum d91 by AFINSQ_2:55;
defpred P[Nat,set] means $2=E.($1+o);
A224: 1-b <> 0 by A1;
consider ok being Nat such that
A225: ok+1=o by A184,NAT_1:6;
A226: dom D = len do1 + len d91 by A41,A203,A189;
now
let k be Nat;
reconsider K=k as Element of NAT by ORDINAL1:def 12;
assume
A227: k in dom d91;
then k < len d91 by AFINSQ_1:86;
then o1+k < len D by A189,A226,XREAL_1:8;
then o1+k in dom D by AFINSQ_1:86;
then D.(o1+k) = d.(o1+k)*b|^(o1+k) by A42;
then d91.K = d.(o1+k)*b|^(o1+k) by A203,A227
.= d.(o1+k)*(b|^o1*b|^k) by NEWTON:8
.= (d.(o1+k)*(b|^k))*(b|^o1);
hence b|^o1 divides d91.k by NAT_D:def 3;
end;
then
A228: b|^o1 divides Sum d91 by Th2;
len co = len g by A205,A210,A213,RELAT_1:62;
then Sum co < b|^o -1 + 1 by A212,A215,AFINSQ_2:57,XREAL_1:145;
then
A229: Sum co div (b|^o) = 0 by NAT_D:27;
A230: 1-b <> 0 by A1;
Sum g1 = Partial_Sums((b-1)(#)(b GeoSeq)).ok1 by AFINSQ_2:56
.= ((b-1)(#)Partial_Sums(b GeoSeq)).ok1 by SERIES_1:9
.= (b-1)*(Partial_Sums(b GeoSeq).ok1) by SEQ_1:9
.= (b-1)*((1 - (b to_power (ok1+1)))/(1-b)) by A1,SERIES_1:22
.= -((1-b)*((1 - (b |^ o1))/(1-b))) by A187
.= -(1 - (b |^ o1)) by A230,XCMPLX_1:87
.= b|^o1-1;
then Sum do1 < b|^o1 -1 + 1 by A191,A193,AFINSQ_2:57,XREAL_1:145;
then
A231: Sum do1 div (b|^o1) = 0 by NAT_D:27;
( for x being Nat st x in dom do1 holds D.x=do1.x)&
for x being Nat st x in dom d91 holds D.(len do1+x)=d91.x by A203,A189,
FUNCT_1:47;
then D=do1^d91 by A226,AFINSQ_1:def 3;
then
A232: n = Sum do1 + Sum d91 by A43,AFINSQ_2:55;
bo1 <> 0 by A1,PREPOWER:5;
then Sum d91 mod (b|^o1) = 0 by A228,PEPIN:6;
then n div (b|^o1) = (Sum d91 div (b|^o1)) + (Sum do1 div (b|^o1))
by A232,NAT_D:19;
then
A233: (n div (b|^o1)) * b|^o1 = Sum d91 by A231,A228,NAT_D:3;
A234: bo <> 0 by A1,PREPOWER:5;
then Sum d9 mod (b|^o) = 0 by A208,PEPIN:6;
then n div (b|^o) = (Sum d9 div (b|^o)) + (Sum co div (b|^o)) by A209
,NAT_D:19;
then (n div (b|^o)) * b|^o = Sum d9 & Sum <%D.o%>=D.o
by A229,A208,AFINSQ_2:53,NAT_D:3;
then d.o*b|^o = (n div (b|^o)) * b|^o - (n div (b|^o1)) * b|^o1 by
A41,A42,A77,A233,A223;
then d.o*b|^o = (n div (b|^o)) * b|^o - (n div (b|^o1)) * (b|^o*b|^
1 ) by NEWTON:8;
then d.o*b|^o = b|^o*((n div (b|^o)) - (n div (b|^o1)) * b|^1);
then (b|^o*d.o)/b|^o = (b|^o*((n div (b|^o)) - (n div (b|^o1)) * b)
) /b|^o;
then
A235: d.o = (b|^o*((n div (b|^o)) - (n div (b|^o1)) * b))/b |^o by A234,
XCMPLX_1:89;
reconsider o1=o+1 as Element of NAT;
A236: o1 <= k by A184,NAT_1:13;
then
A237: o1 < len d by XREAL_1:147;
reconsider ok as Element of NAT by ORDINAL1:def 12;
reconsider g=((b1)(#)(b GeoSeq))|(ok+1) as XFinSequence of NAT by Th1
;
A238: 1-b <> 0 by A1;
reconsider bo1=b|^o1 as Element of NAT by ORDINAL1:def 12;
reconsider do1=E|o1 as XFinSequence of NAT;
reconsider bo=b|^o as Element of NAT by ORDINAL1:def 12;
consider ok1 being Nat such that
A239: ok1+1=o1;
reconsider ok1 as Element of NAT by ORDINAL1:def 12;
reconsider g1=((b1)(#)(b GeoSeq))|(ok1+1) as XFinSequence of NAT by
Th1;
A240: len e = len E by A60;
then
A241: len do1=o1 by A76,A237,AFINSQ_1:11;
dom ((b-1)(#)(b GeoSeq)) = NAT by FUNCT_2:def 1;
then
A242: o1 c= dom ((b-1)(#)(b GeoSeq)) by ORDINAL1:def 2;
then
A243: len do1 = len g1 by A241,A239,RELAT_1:62;
A244: dom g1 = o1 by A239,A242,RELAT_1:62;
A245: for i being Nat st i in dom do1 holds do1.i <= g1.i
proof
let i be Nat;
reconsider I=i as Element of NAT by ORDINAL1:def 12;
assume
A246: i in dom do1;
then i in o1 by A76,A237,A240,AFINSQ_1:11;
then
A247: g1.I = ((b-1)(#)(b GeoSeq)).I by A244,FUNCT_1:47
.= (b-1)*((b GeoSeq).I) by SEQ_1:9
.= b1*(b|^I) by PREPOWER:def 1;
A248: dom do1 c= dom E by RELAT_1:60;
then e.i < b1+1 by A59,A60,A246;
then
A249: e.i <= b1 by NAT_1:13;
do1.i = E.i by A246,FUNCT_1:47
.= (e.i)*(b|^i) by A61,A246,A248;
hence thesis by A247,A249,XREAL_1:64;
end;
Sum g1 = Partial_Sums((b-1)(#)(b GeoSeq)).ok1 by AFINSQ_2:56
.= ((b-1)(#)Partial_Sums(b GeoSeq)).ok1 by SERIES_1:9
.= (b-1)*(Partial_Sums(b GeoSeq).ok1) by SEQ_1:9
.= (b-1)*((1 - (b to_power (ok1+1)))/(1-b)) by A1,SERIES_1:22
.= -((1-b)*((1 - (b |^ o1))/(1-b))) by A239
.= -(1 - (b |^ o1)) by A238,XCMPLX_1:87
.= b|^o1-1;
then Sum do1 < b|^o1 -1 + 1 by A243,A245,AFINSQ_2:57,XREAL_1:145;
then
A250: Sum do1 div (b|^o1) = 0 by NAT_D:27;
k < len d by XREAL_1:147;
then reconsider oo1=len d - o1 as Element of NAT by A236,NAT_1:21
,XXREAL_0:2;
A251: for u being Nat st u in Segm oo ex x be Element of NAT st P[u,x];
consider d9 being XFinSequence of NAT such that
A252: dom d9=Segm oo & for x being Nat st x in Segm oo holds P[
x,d9.x] from STIRL2_1:sch 5(A251);
A253: now
let k be Nat;
assume k in dom <%E.o%>;
then k in Segm 1 by AFINSQ_1:33;
then k < 1 by NAT_1:44;
then
A254: k=0 by NAT_1:14;
oo > 0 by A79,XREAL_1:50;
then k < len d9 by A252,A254;
then k in dom d9 by A252,NAT_1:44;
hence d9.k=E.(k+o) by A252
.= <%E.o%>.k by A254;
end;
defpred P[Nat,set] means $2=E.($1+o1);
A255: for u being Nat st u in Segm oo1 ex x be Element of NAT st P[u,x];
consider d91 being XFinSequence of NAT such that
A256: dom d91=Segm oo1 & for x being Nat st x in Segm oo1 holds
P[x,d91.x] from STIRL2_1:sch 5(A255);
A257: dom E = len do1 + len d91 by A60,A76,A256,A241;
now
let k be Nat;
reconsider K=k as Element of NAT by ORDINAL1:def 12;
assume
A258: k in dom d91;
then k < len d91 by AFINSQ_1:86;
then o1+k < len E by A241,A257,XREAL_1:8;
then o1+k in dom E by AFINSQ_1:86;
then E.(o1+k) = e.(o1+k)*b|^(o1+k) by A61;
then d91.K = e.(o1+k)*b|^(o1+k) by A256,A258
.= e.(o1+k)*(b|^o1*b|^k) by NEWTON:8
.= (e.(o1+k)*(b|^k))*(b|^o1);
hence b|^o1 divides d91.k by NAT_D:def 3;
end;
then
A259: b|^o1 divides Sum d91 by Th2;
( for x being Nat st x in dom do1 holds E.x=do1.x)&
for x being Nat st x in dom d91 holds E.(len do1+x)=d91.x by A256,A241,
FUNCT_1:47;
then E=do1^d91 by A257,AFINSQ_1:def 3;
then
A260: n = Sum do1 + Sum d91 by A62,AFINSQ_2:55;
bo1 <> 0 by A1,PREPOWER:5;
then Sum d91 mod (b|^o1) = 0 by A259,PEPIN:6;
then n div (b|^o1) = (Sum d91 div (b|^o1)) + (Sum do1 div (b|^o1))
by A260,NAT_D:19;
then
A261: (n div (b|^o1)) * b|^o1 = Sum d91 by A250,A259,NAT_D:3;
reconsider co=E|o as XFinSequence of NAT;
A262: len e = len E by A60;
then
A263: len co=o by A76,A79,AFINSQ_1:11;
then A264: dom E = len co + len d9 by A60,A76,A252;
now
let k be Nat;
reconsider K=k as Element of NAT by ORDINAL1:def 12;
assume
A265: k in dom d9;
then k < len d9 by AFINSQ_1:86;
then o+k < len E by A263,A264,XREAL_1:8;
then o+k in dom E by AFINSQ_1:86;
then E.(o+k) = e.(o+k)*b|^(o+k) by A61;
then d9.K = e.(o+k)*b|^(o+k) by A252,A265
.= e.(o+k)*(b|^o*b|^k) by NEWTON:8
.= (e.(o+k)*(b|^k))*(b|^o);
hence b|^o divides d9.k by NAT_D:def 3;
end;
then
A266: b|^o divides Sum d9 by Th2;
dom ((b-1)(#)(b GeoSeq)) = NAT by FUNCT_2:def 1;
then
A267: o c= dom ((b-1)(#)(b GeoSeq)) by ORDINAL1:def 2;
then
A268: len co = len g by A263,A225,RELAT_1:62;
A269: dom g = o by A225,A267,RELAT_1:62;
A270: for i being Nat st i in dom co holds co.i <= g.i
proof
let i be Nat;
reconsider I=i as Element of NAT by ORDINAL1:def 12;
assume
A271: i in dom co;
then i in o by A76,A79,A262,AFINSQ_1:11;
then
A272: g.I = ((b-1)(#)(b GeoSeq)).I by A269,FUNCT_1:47
.= (b-1)*((b GeoSeq).I) by SEQ_1:9
.= b1*(b|^I) by PREPOWER:def 1;
A273: dom co c= dom E by RELAT_1:60;
then e.i < b1+1 by A59,A60,A271;
then
A274: e.i <= b1 by NAT_1:13;
co.i = E.i by A271,FUNCT_1:47
.= (e.i)*(b|^i) by A61,A271,A273;
hence thesis by A272,A274,XREAL_1:64;
end;
Sum g = Partial_Sums((b-1)(#)(b GeoSeq)).ok by AFINSQ_2:56
.= ((b-1)(#)Partial_Sums(b GeoSeq)).ok by SERIES_1:9
.= (b-1)*(Partial_Sums(b GeoSeq).ok) by SEQ_1:9
.= (b-1)*((1 - (b to_power (ok+1)))/(1-b)) by A1,SERIES_1:22
.= -((1-b)*((1 - (b |^ o))/(1-b))) by A225
.= -(1 - (b |^ o)) by A224,XCMPLX_1:87
.= b|^o-1;
then Sum co < b|^o -1 + 1 by A268,A270,AFINSQ_2:57,XREAL_1:145;
then
A275: Sum co div (b|^o) = 0 by NAT_D:27;
A276: now
let k be Nat;
assume
A277: k in dom d91;
then k < len d91 by A256,NAT_1:44;
then k+1 < oo1+1 by XREAL_1:8,A256;
then
A278: k+1 in Segm oo by NAT_1:44;
thus d9.(len <%E.o%> + k) = d9.(1 + k) by AFINSQ_1:33
.= E.(len co+(k+1)) by A252,A263,A278
.= E.(len do1 + k) by A263,A241
.= d91.k by A256,A241,A277;
end;
dom d9 = 1 + dom d91 by A252,A256
.= len <%E.o%> + len d91 by AFINSQ_1:34;
then d9=<%E.o%>^d91 by A253,A276,AFINSQ_1:def 3;
then
A279: Sum d9 = Sum <%E.o%> + Sum d91 by AFINSQ_2:55;
( for x being Nat st x in dom co holds E.x=co.x)&
for x being Nat st x in dom d9 holds E.(len co+x)=d9 .x by A252,A263,FUNCT_1:47
;
then E=co^d9 by A264,AFINSQ_1:def 3;
then
A280: n = Sum co + Sum d9 by A62,AFINSQ_2:55;
A281: bo <> 0 by A1,PREPOWER:5;
then Sum d9 mod (b|^o) = 0 by A266,PEPIN:6;
then n div (b|^o) = (Sum d9 div (b|^o)) + (Sum co div (b|^o)) by A280
,NAT_D:19;
then (n div (b|^o)) * b|^o = Sum d9 by A275,A266,NAT_D:3;
then E.o = (n div (b|^o)) * b|^o - (n div (b|^o1)) * b|^o1 by A261
,A279,AFINSQ_2:53;
then e.o*b|^o = (n div (b|^o)) * b|^o - (n div (b|^o1)) * b|^o1 by
A60,A61,A76,A77;
then e.o*b|^o = (n div (b|^o)) * b|^o - (n div (b|^o1)) * (b|^o*b|^
1 ) by NEWTON:8;
then e.o*b|^o = b|^o*((n div (b|^o)) - (n div (b|^o1)) * b|^1);
then (b|^o*e.o)/b|^o = (b|^o*((n div (b|^o)) - (n div (b|^o1)) * b)
)/b|^o;
hence d.a=e.a by A235,A281,XCMPLX_1:89;
end;
end;
hence thesis by A76,FUNCT_1:2;
end;
assume that
n=0 and
A282: d=<%0%> & e=<%0%>;
thus thesis by A282;
end;
end;
theorem Th4:
for n,b being Nat st b > 1 holds len digits(n,b) >= 1
proof
let n,b be Nat;
assume
A1: b > 1;
per cases;
suppose
n=0;
then digits(n,b)=<%0%> by A1,Def2;
hence thesis by AFINSQ_1:33;
end;
suppose
n<>0;
then digits(n,b).(len digits(n,b) -1) <> 0 by A1,Def2;
then len digits(n,b) -1 in dom digits(n,b) by FUNCT_1:def 2;
hence thesis by NAT_1:14;
end;
end;
theorem Th5:
for n,b being Nat st b > 1 holds value(digits(n,b),b)=n
proof
let n,b be Nat;
assume
A1: b>1;
per cases;
suppose
n<>0;
hence thesis by A1,Def2;
end;
suppose
A2: n=0;
then
A3: digits(n,b)= <%0%> by A1,Def2;
now
let i be Nat;
assume i in dom <%0%>;
then i in {0} by AFINSQ_1:def 4,CARD_1:49;
then
A4: i=0 by TARSKI:def 1;
thus <%0%>.i = 0*(b|^i)
.= (digits(n,b).i)*(b|^i) by A3;
end;
then
value(digits(n,b),b)=Sum <%0%> by A3,Def1;
hence thesis by A2,AFINSQ_2:53;
end;
end;
begin :: Selected divisibility criteria
theorem Th6:
for n,k being Nat st k=10|^n - 1 holds 9 divides k
proof
defpred P[Nat] means ex k being Nat st k=(10|^$1)-1 & 9 divides k;
let n,k be Nat;
A1: now
let k be Nat;
assume P[k];
then consider l being Nat such that
A2: l=(10|^k)-1 and
A3: 9 divides l;
consider m being Nat such that
A4: l = 9 * m by A3,NAT_D:def 3;
A5: 9 divides 9*(m*10+1) by NAT_D:def 3;
10|^(k+1)-1 = (9*m+1)*10 -1 by A2,A4,NEWTON:6
.= 9*(m*10+1);
hence P[k+1] by A5;
end;
(10|^0) -1 = 1-1 by NEWTON:4
.= 0;
then
A6: P[0] by NAT_D:6;
for k being Nat holds P[k] from NAT_1:sch 2(A6,A1);
then
A7: ex l being Nat st l=10|^n -1 & 9 divides l;
assume k=10|^n - 1;
hence thesis by A7;
end;
theorem
for n,b being Nat st b>1 holds b divides n iff digits(n,b).0 = 0
proof
let n,b be Nat;
reconsider B=b as Element of NAT by ORDINAL1:def 12;
consider d being XFinSequence of NAT such that
dom d = dom digits(n,b) and
A1: for i being Nat st i in dom d holds d.i = ( digits(n,b).i)*(b|^i) and
A2: value(digits(n,b),b) = Sum d by Def1;
assume
A3: b>1;
thus b divides n implies digits(n,b).0 = 0
proof
A4: len digits(n,b)>=1 by A3,Th4;
assume
A5: b divides n;
consider d being XFinSequence of NAT such that
A6: dom d = dom digits(n,b) and
A7: for i being Nat st i in dom d holds d.i = ( digits(n,b).i)*(b|^i) and
A8: value(digits(n,b),b) = Sum d by Def1;
per cases by A4,XXREAL_0:1;
suppose
A9: len digits(n,b)=1;
A10: b divides Sum d by A3,A5,A8,Th5;
A11: 0 in dom digits(n,b) by A9,AFINSQ_1:86;
len d = 1 by A6,A9;
then d=<%d.0%> by AFINSQ_1:34;
then Sum d = d.0 by AFINSQ_2:53
.= digits(n,b).0*(b|^0) by A6,A7,A11;
then
A12: b divides digits(n,b).0*1 by A10,NEWTON:4;
per cases;
suppose
n=0;
then digits(n,b) = <%0%> by A3,Def2;
hence thesis;
end;
suppose
n<>0;
then digits(n,b).0 < b by A3,A11,Def2;
hence thesis by A12,NAT_D:7;
end;
end;
suppose
A13: len digits(n,b)>1;
then reconsider k=len digits(n,b)-1 as Element of NAT by NAT_1:21;
defpred P[Nat,set] means $2=d.($1+1);
A14: now
let l be Nat;
assume l in dom <%d.0%>;
then l in Segm 1 by AFINSQ_1:def 4;
then l < 1 by NAT_1:44;
then l=0 by NAT_1:14;
hence d.l=<%d.0%>.l;
end;
A15: for u be Nat st u in Segm k ex x be Element of NAT st P[u, x];
consider d9 being XFinSequence of NAT such that
A16: dom d9=Segm k & for x being Nat st x in Segm k holds P[x,d9.x]
from STIRL2_1:sch 5(A15);
now
let i be Nat;
assume
A17: i in dom d9;
then i < len d9 by A16,NAT_1:44;
then i+1 < k+1 by XREAL_1:8,A16;
then
A18: i+1 in dom d by A6,AFINSQ_1:86;
d9.i=d.(i+1) by A16,A17
.= digits(n,b).(i+1)*b|^(i+1) by A7,A18
.= digits(n,b).(i+1)*(b|^i*b) by NEWTON:6
.= b*(digits(n,b).(i+1)*b|^i);
hence b divides d9.i by NAT_D:def 3;
end;
then b divides Sum d9 by Th2;
then
A19: Sum d9 mod B = 0 by A3,PEPIN:6;
A20: now
let l be Nat;
A21: len <%d.0%> + l = l+1 by AFINSQ_1:34;
assume l in dom d9;
hence d.(len <%d.0%> + l) = d9.l by A16,A21;
end;
A22: 0 in dom digits(n,b) by A13,AFINSQ_1:86;
dom d = k+1 by A6
.= len <%d.0%> + len d9 by A16,AFINSQ_1:33;
then d=<%d.0%>^d9 by A14,A20,AFINSQ_1:def 3;
then Sum d = Sum <%d.0%> + Sum d9 by AFINSQ_2:55;
then n = Sum <%d.0%> + Sum d9 by A3,A8,Th5;
then n = d.0 + Sum d9 by AFINSQ_2:53;
then (d.0 + Sum d9) mod B = 0 by A3,A5,PEPIN:6;
then d.0 mod b = 0 by A19,NAT_D:17;
then B divides d.0 by A3,PEPIN:6;
then b divides digits(n,b).0*(b|^0) by A6,A7,A22;
then
A23: b divides digits(n,b).0*1 by NEWTON:4;
per cases;
suppose
n=0;
then digits(n,b) = <%0%> by A3,Def2;
hence thesis;
end;
suppose
n<>0;
then digits(n,b).0 < b by A3,A22,Def2;
hence thesis by A23,NAT_D:7;
end;
end;
end;
assume
A24: digits(n,b).0=0;
now
let i be Nat;
assume
A25: i in dom d;
per cases;
suppose
i=0;
then d.i = (digits(n,b).0)*b|^0 by A1,A25
.= digits(n,b).0*1 by NEWTON:4;
hence b divides d.i by A24,NAT_D:6;
end;
suppose
i>0;
then consider j being Nat such that
A26: j+1=i by NAT_1:6;
d.i = digits(n,b).i*(b|^(j+1)) by A1,A25,A26
.= digits(n,b).i*((b|^j)*b) by NEWTON:6
.= b*(digits(n,b).i*(b|^j));
hence b divides d.i by NAT_D:def 3;
end;
end;
then b divides value(digits(n,b),b) by A2,Th2;
hence thesis by A3,Th5;
end;
theorem
for n being Nat holds 2 divides n iff 2 divides digits(n,10).0
proof
let n be Nat;
consider d being XFinSequence of NAT such that
dom d = dom digits(n,10) and
A1: for i being Nat st i in dom d holds d.i = ( digits(n,10).i)*(10|^i) and
A2: value(digits(n,10),10) = Sum d by Def1;
thus 2 divides n implies 2 divides digits(n,10).0
proof
A3: len digits(n,10)>=1 by Th4;
assume
A4: 2 divides n;
consider d being XFinSequence of NAT such that
A5: dom d = dom digits(n,10) and
A6: for i being Nat st i in dom d holds d.i = ( digits(n,10).i)*(10|^i ) and
A7: value(digits(n,10),10) = Sum d by Def1;
per cases by A3,XXREAL_0:1;
suppose
A8: len digits(n,10)=1;
then
A9: 0 in dom digits(n,10) by AFINSQ_1:86;
A10: 2 divides Sum d by A4,A7,Th5;
len d = 1 by A5,A8;
then d=<%d.0%> by AFINSQ_1:34;
then Sum d = d.0 by AFINSQ_2:53
.= digits(n,10).0*(10|^0) by A5,A6,A9;
then 2 divides digits(n,10).0*1 by A10,NEWTON:4;
hence thesis;
end;
suppose
A11: len digits(n,10)>1;
then reconsider k=len digits(n,10)-1 as Element of NAT by NAT_1:21;
defpred P[Nat,set] means $2=d.($1+1);
A12: now
let l be Nat;
assume l in dom <%d.0%>;
then l in Segm 1 by AFINSQ_1:def 4;
then l < 1 by NAT_1:44;
then l=0 by NAT_1:14;
hence d.l=<%d.0%>.l;
end;
A13: for u being Nat st u in Segm k ex x be Element of NAT st P[u, x];
consider d9 being XFinSequence of NAT such that
A14: dom d9=Segm k & for x being Nat st x in Segm k holds P[x,d9.x]
from STIRL2_1:sch 5(A13);
now
let i be Nat;
assume
A15: i in dom d9;
then i < len d9 by A14,NAT_1:44;
then i+1 < k+1 by XREAL_1:8,A14;
then
A16: i+1 in dom d by A5,AFINSQ_1:86;
d9.i=d.(i+1) by A14,A15
.= digits(n,10).(i+1)*10|^(i+1) by A6,A16
.= digits(n,10).(i+1)*(10|^i*10) by NEWTON:6
.= 2*(digits(n,10).(i+1)*10|^i*5);
hence 2 divides d9.i by NAT_D:def 3;
end;
then 2 divides Sum d9 by Th2;
then
A17: Sum d9 mod 2 = 0 by PEPIN:6;
A18: now
let l be Nat;
A19: len <%d.0%> + l = l+1 by AFINSQ_1:34;
assume l in dom d9;
hence d.(len <%d.0%> + l) = d9.l by A14,A19;
end;
dom d = k+1 by A5
.= len <%d.0%> + len d9 by A14,AFINSQ_1:33;
then d=<%d.0%>^d9 by A12,A18,AFINSQ_1:def 3;
then Sum d = Sum <%d.0%> + Sum d9 by AFINSQ_2:55;
then n = Sum <%d.0%> + Sum d9 by A7,Th5;
then n = d.0 + Sum d9 by AFINSQ_2:53;
then (d.0 + Sum d9) mod 2 = 0 by A4,PEPIN:6;
then d.0 mod 2 = 0 by A17,NAT_D:17;
then
A20: 2 divides d.0 by PEPIN:6;
0 in dom digits(n,10) by A11,AFINSQ_1:86;
then 2 divides digits(n,10).0*(10|^0) by A5,A6,A20;
then 2 divides digits(n,10).0*1 by NEWTON:4;
hence thesis;
end;
end;
assume
A21: 2 divides digits(n,10).0;
now
let i be Nat;
assume
A22: i in dom d;
per cases;
suppose
i=0;
then d.i = (digits(n,10).0)*10|^0 by A1,A22
.= digits(n,10).0*1 by NEWTON:4;
hence 2 divides d.i by A21;
end;
suppose
i>0;
then consider j being Nat such that
A23: j+1=i by NAT_1:6;
d.i = digits(n,10).i*(10|^(j+1)) by A1,A22,A23
.= digits(n,10).i*((10|^j)*10) by NEWTON:6
.= 2*(digits(n,10).i*(10|^j)*5);
hence 2 divides d.i by NAT_D:def 3;
end;
end;
then 2 divides value(digits(n,10),10) by A2,Th2;
hence thesis by Th5;
end;
::$N Divisibility by 3 Rule
::$L https://en.wikipedia.org/wiki/Divisibility_rule Divisibility rules
theorem
for n being Nat holds 3 divides n iff 3 divides Sum digits(n,10)
proof
let n be Nat;
consider p being XFinSequence of NAT such that
A1: dom p = dom digits(n,10) and
A2: for i being Nat st i in dom p holds p.i = ( digits(n,10).i)*(10|^i) and
A3: value(digits(n,10),10) = Sum p by Def1;
reconsider dop=dom p as Element of NAT by ORDINAL1:def 12;
defpred Q[set,set] means $2=p.$1 mod 3;
A4: for k being Nat st k in Segm dop ex x being Element of NAT st Q[k, x];
consider p9 being XFinSequence of NAT such that
A5: dom p9 = Segm dop & for k being Nat st k in Segm dop holds Q[k,p9.k
] from STIRL2_1:sch 5(A4);
A6: now
let i be Nat;
reconsider dz=10|^i - 1 as Nat by NAT_1:20,NEWTON:83;
reconsider dz as Element of NAT by ORDINAL1:def 12;
3 divides 3*3 & 9 divides dz by Th6,NAT_D:def 3;
then 3 divides dz by NAT_D:4;
then 3 divides (digits(n,10).i)*dz by NAT_D:9;
then
A7: (digits(n,10).i)*dz mod 3 = 0 by PEPIN:6;
assume
A8: i in dom p;
hence p9.i = p.i mod 3 by A5
.= (digits(n,10).i)*(dz+1) mod 3 by A2,A8
.= ((digits(n,10).i)*dz+ digits(n,10).i) mod 3
.= (0 qua Nat+digits(n,10).i) mod 3 by A7,NAT_D:22
.= digits(n,10).i mod 3;
end;
thus 3 divides n implies 3 divides Sum digits(n,10)
proof
assume 3 divides n;
then 3 divides Sum p by A3,Th5;
then Sum p mod 3 = 0 by PEPIN:6;
then Sum p9 mod 3 = 0 by A5,Th3;
then Sum digits(n,10) mod 3 = 0 by A1,A5,A6,Th3;
hence thesis by PEPIN:6;
end;
assume 3 divides Sum digits(n,10);
then Sum digits(n,10) mod 3 = 0 by PEPIN:6;
then Sum p9 mod 3 = 0 by A1,A5,A6,Th3;
then Sum p mod 3 = 0 by A5,Th3;
then 3 divides Sum p by PEPIN:6;
hence thesis by A3,Th5;
end;
theorem
for n being Nat holds 5 divides n iff 5 divides digits(n,10).0
proof
let n be Nat;
consider d being XFinSequence of NAT such that
dom d = dom digits(n,10) and
A1: for i being Nat st i in dom d holds d.i = ( digits(n,10).i)*(10|^i) and
A2: value(digits(n,10),10) = Sum d by Def1;
thus 5 divides n implies 5 divides digits(n,10).0
proof
A3: len digits(n,10)>=1 by Th4;
assume
A4: 5 divides n;
consider d being XFinSequence of NAT such that
A5: dom d = dom digits(n,10) and
A6: for i being Nat st i in dom d holds d.i = ( digits(n,10).i)*(10|^i ) and
A7: value(digits(n,10),10) = Sum d by Def1;
per cases by A3,XXREAL_0:1;
suppose
A8: len digits(n,10)=1;
then
A9: 0 in dom digits(n,10) by AFINSQ_1:86;
A10: 5 divides Sum d by A4,A7,Th5;
len d = 1 by A5,A8;
then d=<%d.0%> by AFINSQ_1:34;
then Sum d = d.0 by AFINSQ_2:53
.= digits(n,10).0*(10|^0) by A5,A6,A9;
then 5 divides digits(n,10).0*1 by A10,NEWTON:4;
hence thesis;
end;
suppose
A11: len digits(n,10)>1;
then reconsider k=len digits(n,10)-1 as Element of NAT by NAT_1:21;
defpred P[Nat,set] means $2=d.($1+1);
A12: now
let l be Nat;
assume l in dom <%d.0%>;
then l in Segm 1 by AFINSQ_1:def 4;
then l < 1 by NAT_1:44;
then l=0 by NAT_1:14;
hence d.l=<%d.0%>.l;
end;
A13: for u being Nat st u in Segm k ex x be Element of NAT st P[u, x];
consider d9 being XFinSequence of NAT such that
A14: dom d9=Segm k & for x being Nat st x in Segm k holds P[x,d9.x]
from STIRL2_1:sch 5(A13);
now
let i be Nat;
assume
A15: i in dom d9;
then i < len d9 by A14,NAT_1:44;
then i+1 < k+1 by XREAL_1:8,A14;
then
A16: i+1 in dom d by A5,AFINSQ_1:86;
d9.i=d.(i+1) by A14,A15
.= digits(n,10).(i+1)*10|^(i+1) by A6,A16
.= digits(n,10).(i+1)*(10|^i*10) by NEWTON:6
.= 5*(digits(n,10).(i+1)*10|^i*2);
hence 5 divides d9.i by NAT_D:def 3;
end;
then 5 divides Sum d9 by Th2;
then
A17: Sum d9 mod 5 = 0 by PEPIN:6;
A18: now
let l be Nat;
A19: len <%d.0%> + l = l+1 by AFINSQ_1:34;
assume l in dom d9;
hence d.(len <%d.0%> + l) = d9.l by A14,A19;
end;
dom d = k+1 by A5
.= len <%d.0%> + len d9 by A14,AFINSQ_1:33;
then d=<%d.0%>^d9 by A12,A18,AFINSQ_1:def 3;
then Sum d = Sum <%d.0%> + Sum d9 by AFINSQ_2:55;
then n = Sum <%d.0%> + Sum d9 by A7,Th5;
then n = d.0 + Sum d9 by AFINSQ_2:53;
then (d.0 + Sum d9) mod 5 = 0 by A4,PEPIN:6;
then d.0 mod 5 = 0 by A17,NAT_D:17;
then
A20: 5 divides d.0 by PEPIN:6;
0 in dom digits(n,10) by A11,AFINSQ_1:86;
then 5 divides digits(n,10).0*(10|^0) by A5,A6,A20;
then 5 divides digits(n,10).0*1 by NEWTON:4;
hence thesis;
end;
end;
assume
A21: 5 divides digits(n,10).0;
now
let i be Nat;
assume
A22: i in dom d;
per cases;
suppose
i=0;
then d.i = (digits(n,10).0)*10|^0 by A1,A22
.= digits(n,10).0*1 by NEWTON:4;
hence 5 divides d.i by A21;
end;
suppose
i>0;
then consider j being Nat such that
A23: j+1=i by NAT_1:6;
d.i = digits(n,10).i*(10|^(j+1)) by A1,A22,A23
.= digits(n,10).i*((10|^j)*10) by NEWTON:6
.= 5*(digits(n,10).i*(10|^j)*2);
hence 5 divides d.i by NAT_D:def 3;
end;
end;
then 5 divides value(digits(n,10),10) by A2,Th2;
hence thesis by Th5;
end;