:: NUMERAL1 semantic presentation
begin
theorem Th1: :: NUMERAL1:1
for k, l, m being Nat holds (k (#) (l GeoSeq)) | m is XFinSequence of NAT
proof
let k, l, m be Nat; ::_thesis: (k (#) (l GeoSeq)) | m is XFinSequence of 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 ((k (#) (l GeoSeq)) | m) = m by RELAT_1:62;
then reconsider g9 = (k (#) (l GeoSeq)) | m as XFinSequence by ORDINAL1:def_7;
rng g9 c= NAT
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng g9 or a in NAT )
assume a in rng g9 ; ::_thesis: a in NAT
then consider o being set such that
A2: o in dom ((k (#) (l GeoSeq)) | m) and
A3: a = ((k (#) (l GeoSeq)) | m) . o by FUNCT_1:def_3;
o in dom (k (#) (l GeoSeq)) by A2, RELAT_1:57;
then reconsider o = o as Element of NAT ;
((k (#) (l GeoSeq)) | m) . 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 a in NAT by A3; ::_thesis: verum
end;
hence (k (#) (l GeoSeq)) | m is XFinSequence of NAT by RELAT_1:def_19; ::_thesis: verum
end;
theorem Th2: :: NUMERAL1:2
for d being XFinSequence of NAT
for 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 ; ::_thesis: for n being Nat st ( for i being Nat st i in dom d holds
n divides d . i ) holds
n divides Sum d
let n be Nat; ::_thesis: ( ( for i being Nat st i in dom d holds
n divides d . i ) implies n divides Sum d )
assume A1: for i being Nat st i in dom d holds
n divides d . i ; ::_thesis: n divides Sum d
percases ( len d = 0 or len d > 0 ) ;
suppose len d = 0 ; ::_thesis: n divides Sum d
then d = {} ;
then Sum d = 0 ;
hence n divides Sum d by NAT_D:6; ::_thesis: verum
end;
supposeA2: len d > 0 ; ::_thesis: n divides Sum d
then consider f being Function of NAT,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 S1[ Element of NAT ] means ( $1 < len d implies n divides f . $1 );
A6: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A7: S1[k] ; ::_thesis: S1[k + 1]
thus S1[k + 1] ::_thesis: verum
proof
assume A8: k + 1 < len d ; ::_thesis: n divides f . (k + 1)
then k + 1 in 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 n divides f . (k + 1) by A7, A8, A9, NAT_1:13, NAT_D:8; ::_thesis: verum
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 len d by A2, NAT_1:44;
then A11: S1[ 0 ] by A1, A3;
A12: addnat "**" d = Sum d by AFINSQ_2:51;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A11, A6);
hence n divides Sum d by A5, A10, A12; ::_thesis: verum
end;
end;
end;
theorem Th3: :: NUMERAL1:3
for d, e being XFinSequence of NAT
for 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 ; ::_thesis: for 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
let n be Nat; ::_thesis: ( dom d = dom e & ( for i being Nat st i in dom d holds
e . i = (d . i) mod n ) implies (Sum d) mod n = (Sum e) mod n )
assume A1: ( dom d = dom e & ( for i being Nat st i in dom d holds
e . i = (d . i) mod n ) ) ; ::_thesis: (Sum d) mod n = (Sum e) mod n
defpred S1[ 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
for l being Element of NAT st S1[p] holds
S1[p ^ <%l%>]
proof
let p be XFinSequence of NAT ; ::_thesis: for l being Element of NAT st S1[p] holds
S1[p ^ <%l%>]
let l be Element of NAT ; ::_thesis: ( S1[p] implies S1[p ^ <%l%>] )
assume A3: S1[p] ; ::_thesis: S1[p ^ <%l%>]
thus S1[p ^ <%l%>] ::_thesis: verum
proof
reconsider dop = dom p as Element of NAT by ORDINAL1:def_12;
defpred S2[ set , set ] means $2 = (p . $1) mod n;
let e be XFinSequence of NAT ; ::_thesis: ( dom (p ^ <%l%>) = dom e & ( for i being Nat st i in dom (p ^ <%l%>) holds
e . i = ((p ^ <%l%>) . i) mod n ) implies (Sum (p ^ <%l%>)) mod n = (Sum e) mod n )
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 ; ::_thesis: (Sum (p ^ <%l%>)) mod n = (Sum e) mod n
A6: for k being Nat st k in dop holds
ex x being Element of NAT st S2[k,x] ;
consider p9 being XFinSequence of NAT such that
A7: ( dom p9 = dop & ( for k being Nat st k in dop holds
S2[k,p9 . k] ) ) from STIRL2_1:sch_5(A6);
A8: now__::_thesis:_for_k_being_Nat_st_k_in_dom_p9_holds_
e_._k_=_p9_._k
let k be Nat; ::_thesis: ( k in dom p9 implies e . k = p9 . k )
assume A9: k in dom p9 ; ::_thesis: e . k = p9 . k
then k < dom p9 by NAT_1:44;
then k < (len p) + 1 by A7, NAT_1:13;
then k < (len p) + (len <%l%>) by AFINSQ_1:33;
then k in (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 ;
::_thesis: verum
end;
A10: now__::_thesis:_for_k_being_Nat_st_k_in_dom_<%(l_mod_n)%>_holds_
e_._((len_p9)_+_k)_=_<%(l_mod_n)%>_._k
let k be Nat; ::_thesis: ( k in dom <%(l mod n)%> implies e . ((len p9) + k) = <%(l mod n)%> . k )
assume k in dom <%(l mod n)%> ; ::_thesis: e . ((len p9) + k) = <%(l mod n)%> . k
then A11: k in 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, AFINSQ_1:34 ;
::_thesis: verum
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 ; ::_thesis: verum
end;
end;
A14: S1[ <%> NAT]
proof
let e be XFinSequence of NAT ; ::_thesis: ( dom (<%> NAT) = dom e & ( for i being Nat st i in dom (<%> NAT) holds
e . i = ((<%> NAT) . i) mod n ) implies (Sum (<%> NAT)) mod n = (Sum e) mod n )
assume that
A15: dom (<%> NAT) = dom e and
for i being Nat st i in dom (<%> NAT) holds
e . i = ((<%> NAT) . i) mod n ; ::_thesis: (Sum (<%> NAT)) mod n = (Sum e) mod n
len e = 0 by A15;
hence (Sum (<%> NAT)) mod n = (Sum e) mod n by AFINSQ_1:15; ::_thesis: verum
end;
for p being XFinSequence of NAT holds S1[p] from AFINSQ_2:sch_2(A14, A2);
hence (Sum d) mod n = (Sum e) mod n by A1; ::_thesis: verum
end;
begin
definition
let d be XFinSequence of NAT ;
let b be Nat;
func value (d,b) -> Nat means :Def1: :: 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 );
existence
ex b1 being Nat 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) ) & b1 = Sum d9 )
proof
deffunc H1( Nat) -> Element of 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 = H1(i) ) ) from AFINSQ_1:sch_2();
rng d9 c= NAT
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng d9 or a in NAT )
assume a in rng d9 ; ::_thesis: a in NAT
then consider i being set such that
A2: i in dom d9 and
A3: d9 . i = a by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A2;
a = H1(i) by A1, A2, A3;
hence a in NAT ; ::_thesis: verum
end;
then reconsider d9 = d9 as XFinSequence of NAT by RELAT_1:def_19;
take Sum d9 ; ::_thesis: 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) ) & Sum d9 = Sum d9 )
thus 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) ) & Sum d9 = Sum d9 ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Nat st 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) ) & b1 = Sum d9 ) & 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) ) & b2 = Sum d9 ) holds
b1 = b2
proof
let k, l be Nat; ::_thesis: ( 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) ) & k = Sum d9 ) & 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) ) & l = Sum d9 ) implies k = l )
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 ; ::_thesis: ( for d9 being XFinSequence of NAT holds
( not dom d9 = dom d or ex i being Nat st
( i in dom d9 & not d9 . i = (d . i) * (b |^ i) ) or not l = Sum d9 ) or k = l )
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 ; ::_thesis: k = l
now__::_thesis:_for_i_being_Nat_st_i_in_dom_d_holds_
k9_._i_=_l9_._i
let i be Nat; ::_thesis: ( i in dom d implies k9 . i = l9 . i )
assume A10: i in dom d ; ::_thesis: k9 . i = l9 . i
hence k9 . i = (d . i) * (b |^ i) by A4, A5
.= l9 . i by A7, A8, A10 ;
::_thesis: verum
end;
hence k = l by A4, A6, A7, A9, AFINSQ_1:8; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines value NUMERAL1:def_1_:_
for d being XFinSequence of NAT
for b, b3 being Nat holds
( b3 = value (d,b) iff 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) ) & b3 = Sum d9 ) );
definition
let n, b be Nat;
assume A1: b > 1 ;
func digits (n,b) -> XFinSequence of NAT means :Def2: :: 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%>;
consistency
for b1 being XFinSequence of NAT holds verum ;
existence
( ( n <> 0 implies ex b1 being XFinSequence of NAT st
( value (b1,b) = n & b1 . ((len b1) - 1) <> 0 & ( for i being Nat st i in dom b1 holds
( 0 <= b1 . i & b1 . i < b ) ) ) ) & ( not n <> 0 implies ex b1 being XFinSequence of NAT st b1 = <%0%> ) )
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 ) ) ) ) ::_thesis: ( not n <> 0 implies ex b1 being XFinSequence of NAT st b1 = <%0%> )
proof
deffunc H1( Nat, Element of NAT ) -> Element of NAT = $2 div B;
consider f being Function of NAT,NAT such that
A2: ( f . 0 = N & ( for i being Nat holds f . (i + 1) = H1(i,f . i) ) ) from NAT_1:sch_12();
defpred S1[ Nat] means f . $1 = 0 ;
defpred S2[ Nat] means ex i being Element of NAT st f . i = $1;
A3: for k being Nat st k <> 0 & S2[k] holds
ex l being Nat st
( l < k & S2[l] )
proof
let k be Nat; ::_thesis: ( k <> 0 & S2[k] implies ex l being Nat st
( l < k & S2[l] ) )
assume that
A4: k <> 0 and
A5: S2[k] ; ::_thesis: ex l being Nat st
( l < k & S2[l] )
take l = k div b; ::_thesis: ( l < k & S2[l] )
thus l < k by A1, A4, INT_1:56; ::_thesis: S2[l]
consider i being Element of NAT such that
A6: f . i = k by A5;
take i + 1 ; ::_thesis: f . (i + 1) = l
thus f . (i + 1) = l by A2, A6; ::_thesis: verum
end;
A7: ex k being Nat st S2[k] by A2;
S2[ 0 ] from NAT_1:sch_7(A7, A3);
then A8: ex l being Nat st S1[l] ;
consider l being Nat such that
A9: ( S1[l] & ( for i being Nat st S1[i] holds
l <= i ) ) from NAT_1:sch_5(A8);
assume n <> 0 ; ::_thesis: 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 ) ) )
then consider m being Nat such that
A10: m + 1 = l by A2, A9, NAT_1:6;
reconsider m = 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 S3[ Nat, Nat] means $2 = (g . $1) mod b;
A11: for i being Nat st i in m + 1 holds
ex x being Element of NAT st S3[i,x] ;
consider d being XFinSequence of NAT such that
A12: ( dom d = m + 1 & ( for i being Nat st i in m + 1 holds
S3[i,d . i] ) ) from STIRL2_1:sch_5(A11);
A13: now__::_thesis:_for_i_being_Nat_st_l_<=_i_&_S1[i]_holds_
S1[i_+_1]
let i be Nat; ::_thesis: ( l <= i & S1[i] implies S1[i + 1] )
assume l <= i ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume S1[i] ; ::_thesis: S1[i + 1]
then f . (i + 1) = 0 div b by A2;
hence S1[i + 1] by NAT_2:2; ::_thesis: verum
end;
A14: S1[l] by A9;
A15: for i being Nat st l <= i holds
S1[i] from NAT_1:sch_8(A14, A13);
A16: now__::_thesis:_for_i_being_Element_of_NAT_st_m_<_i_holds_
f_._i_=_0
let i be Element of NAT ; ::_thesis: ( m < i implies f . i = 0 )
assume m < i ; ::_thesis: f . i = 0
then l <= i by A10, NAT_1:13;
hence f . i = 0 by A15; ::_thesis: verum
end;
deffunc H2( Nat) -> Element of NAT = (d . $1) * (b |^ $1);
consider d9 being XFinSequence such that
A17: ( len d9 = len d & ( for i being Nat st i in len d holds
d9 . i = H2(i) ) ) from AFINSQ_1:sch_2();
rng d9 c= NAT
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng d9 or a in NAT )
assume a in rng d9 ; ::_thesis: a in NAT
then consider i being set such that
A18: i in dom d9 and
A19: d9 . i = a by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A18;
a = H2(i) by A17, A18, A19;
hence a in NAT ; ::_thesis: verum
end;
then reconsider d9 = d9 as XFinSequence of NAT by RELAT_1:def_19;
consider s being Function of NAT,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 S4[ Element of NAT ] means ( $1 < len d9 implies s . $1 = n - ((f . ($1 + 1)) * (b |^ ($1 + 1))) );
A23: now__::_thesis:_for_i_being_Element_of_NAT_st_S4[i]_holds_
S4[i_+_1]
let i be Element of NAT ; ::_thesis: ( S4[i] implies S4[i + 1] )
assume A24: S4[i] ; ::_thesis: S4[i + 1]
now__::_thesis:_(_i_+_1_<_len_d9_implies_s_._(i_+_1)_=_n_-_((f_._((i_+_1)_+_1))_*_(b_|^_((i_+_1)_+_1)))_)
assume A25: i + 1 < len d9 ; ::_thesis: s . (i + 1) = n - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1)))
then A26: i + 1 in dom d9 by NAT_1:44;
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))) ; ::_thesis: verum
end;
hence S4[i + 1] ; ::_thesis: verum
end;
reconsider ld = (len d9) - 1 as Element of NAT by A12, A17;
A27: 0 in 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)) by NEWTON:5
.= n - ((f . (0 + 1)) * (b |^ (0 + 1))) by A2 ;
then A28: S4[ 0 ] by A20;
for i being Element of NAT holds S4[i] from NAT_1:sch_1(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 ; ::_thesis: ( 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 ) ) )
thus value (d,b) = n by A17, A29, Def1; ::_thesis: ( d . ((len d) - 1) <> 0 & ( for i being Nat st i in dom d holds
( 0 <= d . i & d . i < b ) ) )
g . m = f . m by FUNCT_1:49, NAT_1:45;
then ( m < m + 1 & f . (m + 1) = (g . m) div b ) by A2, NAT_1:13;
then A31: (g . m) div b = 0 by A16;
d . ((len d) - 1) = (g . m) mod b by A12, NAT_1:45
.= g . m by A1, A31, NAT_2:12, NAT_D:24 ;
hence d . ((len d) - 1) <> 0 by A30, FUNCT_1:49, NAT_1:45; ::_thesis: for i being Nat st i in dom d holds
( 0 <= d . i & d . i < b )
let i be Nat; ::_thesis: ( i in dom d implies ( 0 <= d . i & d . i < b ) )
assume i in dom d ; ::_thesis: ( 0 <= d . i & d . i < b )
then d . i = (g . i) mod b by A12;
hence ( 0 <= d . i & d . i < b ) by A1, NAT_D:1; ::_thesis: verum
end;
assume n = 0 ; ::_thesis: ex b1 being XFinSequence of NAT st b1 = <%0%>
take d ; ::_thesis: d = <%0%>
thus d = <%0%> ; ::_thesis: verum
end;
uniqueness
for b1, b2 being XFinSequence of NAT holds
( ( n <> 0 & value (b1,b) = n & b1 . ((len b1) - 1) <> 0 & ( for i being Nat st i in dom b1 holds
( 0 <= b1 . i & b1 . i < b ) ) & value (b2,b) = n & b2 . ((len b2) - 1) <> 0 & ( for i being Nat st i in dom b2 holds
( 0 <= b2 . i & b2 . i < b ) ) implies b1 = b2 ) & ( not n <> 0 & b1 = <%0%> & b2 = <%0%> implies b1 = b2 ) )
proof
reconsider b1 = b - 1 as Element of NAT by A1, NAT_1:20;
let d, e be XFinSequence of NAT ; ::_thesis: ( ( 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 ) & ( not n <> 0 & d = <%0%> & e = <%0%> implies d = e ) )
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 ) ::_thesis: ( not n <> 0 & d = <%0%> & e = <%0%> implies d = e )
proof
log (2,b) > log (2,1) by A1, POWER:57;
then A32: log (2,b) > 0 by POWER:51;
log (2,b) > log (2,1) by A1, POWER:57;
then A33: log (2,b) > 0 by POWER:51;
A34: 1 - b <> 0 by A1;
A35: 1 - b <> 0 by A1;
reconsider g = (b1 (#) (b GeoSeq)) | (len d) as XFinSequence of NAT by Th1;
assume A36: n <> 0 ; ::_thesis: ( not value (d,b) = n or not d . ((len d) - 1) <> 0 or ex i being Nat st
( i in dom d & not ( 0 <= d . i & d . i < b ) ) or not value (e,b) = n or not e . ((len e) - 1) <> 0 or ex i being Nat st
( i in dom e & not ( 0 <= e . i & e . i < b ) ) or d = e )
assume that
A37: value (d,b) = n and
A38: d . ((len d) - 1) <> 0 and
A39: for i being Nat st i in dom d holds
( 0 <= d . i & d . i < b ) ; ::_thesis: ( not value (e,b) = n or not e . ((len e) - 1) <> 0 or ex i being Nat st
( i in dom e & not ( 0 <= e . i & e . i < b ) ) or d = e )
consider D being XFinSequence of NAT such that
A40: dom D = dom d and
A41: for i being Nat st i in dom D holds
D . i = (d . i) * (b |^ i) and
A42: n = Sum D by A37, Def1;
A43: len D > 0 by A38, A40, FUNCT_1:def_2;
A44: (len d) - 1 in dom d by A38, FUNCT_1:def_2;
then reconsider k = (len d) - 1 as Element of NAT ;
A45: 1 * (b |^ k) <= (d . k) * (b |^ k) by A38, NAT_1:4, NAT_1:14;
A46: b |^ k > 0 by A1, PREPOWER:6;
D . k = (d . k) * (b |^ k) by A40, A41, A44;
then (d . k) * (b |^ k) <= n by A40, A42, A44, A43, AFINSQ_2:61;
then b |^ k <= n by A45, XXREAL_0:2;
then log (2,(b to_power k)) <= log (2,n) by A46, 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 A33, XREAL_1:72;
then A47: k <= (log (2,n)) / (log (2,b)) by A33, XCMPLX_1:89;
g = ((b - 1) (#) (b GeoSeq)) | (k + 1) ;
then A48: 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 A35, XCMPLX_1:87
.= (b |^ (k + 1)) - 1 ;
A49: dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def_1;
then A50: len D = len g by A40, RELAT_1:62;
len d c= dom ((b - 1) (#) (b GeoSeq)) by A49, ORDINAL1:def_2;
then A51: dom g = len d by RELAT_1:62;
A52: for i being Nat st i in dom D holds
D . i <= g . i
proof
let i be Nat; ::_thesis: ( i in dom D implies D . i <= g . i )
reconsider I = i as Element of NAT by ORDINAL1:def_12;
assume A53: i in dom D ; ::_thesis: D . i <= g . i
then A54: D . i = (d . i) * (b |^ i) by A41;
d . i < b1 + 1 by A39, A40, A53;
then A55: d . i <= b1 by NAT_1:13;
g . I = ((b - 1) (#) (b GeoSeq)) . I by A40, A51, A53, FUNCT_1:47
.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def_1 ;
hence D . i <= g . i by A55, A54, XREAL_1:64; ::_thesis: verum
end;
assume that
A56: value (e,b) = n and
A57: e . ((len e) - 1) <> 0 and
A58: for i being Nat st i in dom e holds
( 0 <= e . i & e . i < b ) ; ::_thesis: d = e
consider E being XFinSequence of NAT such that
A59: dom E = dom e and
A60: for i being Nat st i in dom E holds
E . i = (e . i) * (b |^ i) and
A61: n = Sum E by A56, Def1;
A62: (len e) - 1 in dom e by A57, FUNCT_1:def_2;
then reconsider l = (len e) - 1 as Element of NAT ;
A63: 1 * (b |^ l) <= (e . l) * (b |^ l) by A57, NAT_1:4, NAT_1:14;
reconsider g = (b1 (#) (b GeoSeq)) | (len e) as XFinSequence of NAT by Th1;
g = ((b - 1) (#) (b GeoSeq)) | (l + 1) ;
then A64: 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 A34, XCMPLX_1:87
.= (b |^ (l + 1)) - 1 ;
A65: 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 A66: dom g = len e by RELAT_1:62;
A67: for i being Nat st i in dom E holds
E . i <= g . i
proof
let i be Nat; ::_thesis: ( i in dom E implies E . i <= g . i )
reconsider I = i as Element of NAT by ORDINAL1:def_12;
assume A68: i in dom E ; ::_thesis: E . i <= g . i
then A69: E . i = (e . i) * (b |^ i) by A60;
e . i < b1 + 1 by A58, A59, A68;
then A70: e . i <= b1 by NAT_1:13;
g . I = ((b - 1) (#) (b GeoSeq)) . I by A59, A66, A68, FUNCT_1:47
.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def_1 ;
hence E . i <= g . i by A70, A69, XREAL_1:64; ::_thesis: verum
end;
A71: len E > 0 by A57, A59, FUNCT_1:def_2;
A72: b |^ l > 0 by A1, PREPOWER:6;
E . l = (e . l) * (b |^ l) by A59, A60, A62;
then (e . l) * (b |^ l) <= n by A59, A61, A62, A71, AFINSQ_2:61;
then b |^ l <= n by A63, XXREAL_0:2;
then log (2,(b to_power l)) <= log (2,n) by A72, 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 A32, XREAL_1:72;
then A73: l <= (log (2,n)) / (log (2,b)) by A32, XCMPLX_1:89;
len E = len g by A59, A65, RELAT_1:62;
then n < ((b |^ (l + 1)) - 1) + 1 by A61, A64, A67, AFINSQ_2:57, XREAL_1:39;
then log (2,n) < log (2,(b to_power (l + 1))) by A36, 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 A32, XREAL_1:74;
then (log (2,n)) / (log (2,b)) < l + 1 by A32, XCMPLX_1:89;
then k < l + 1 by A47, XXREAL_0:2;
then A74: k <= l by NAT_1:13;
n < ((b |^ (k + 1)) - 1) + 1 by A42, A48, A50, A52, AFINSQ_2:57, XREAL_1:39;
then log (2,n) < log (2,(b to_power (k + 1))) by A36, 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 A33, XREAL_1:74;
then (log (2,n)) / (log (2,b)) < k + 1 by A33, XCMPLX_1:89;
then l < k + 1 by A73, XXREAL_0:2;
then l <= k by NAT_1:13;
then A75: k = l by A74, XXREAL_0:1;
now__::_thesis:_for_a_being_set_st_a_in_dom_d_holds_
d_._a_=_e_._a
let a be set ; ::_thesis: ( a in dom d implies d . b1 = e . b1 )
assume A76: a in dom d ; ::_thesis: d . b1 = e . b1
then reconsider o = a as Element of NAT ;
o < k + 1 by A76, NAT_1:44;
then A77: o <= k by NAT_1:13;
A78: o < len d by A76, NAT_1:44;
then reconsider oo = (len d) - o as Element of NAT by NAT_1:21;
percases ( ( o = 0 & o = k ) or ( o = 0 & o < k ) or ( o > 0 & o = k ) or ( o > 0 & o < k ) ) by A77, XXREAL_0:1;
supposeA79: ( o = 0 & o = k ) ; ::_thesis: d . b1 = e . b1
then len E = 1 by A59, A75;
then A80: E = <%(E . 0)%> by AFINSQ_1:34
.= <%((e . 0) * (b |^ 0))%> by A59, A60, A75, A76, A79
.= <%((e . 0) * 1)%> by NEWTON:4 ;
len D = 1 by A40, A79;
then D = <%(D . 0)%> by AFINSQ_1:34
.= <%((d . 0) * (b |^ 0))%> by A40, A41, A76, A79
.= <%((d . 0) * 1)%> by NEWTON:4 ;
hence d . a = n by A42, A79, AFINSQ_2:53
.= e . a by A61, A79, A80, AFINSQ_2:53 ;
::_thesis: verum
end;
supposeA81: ( o = 0 & o < k ) ; ::_thesis: d . b1 = e . b1
reconsider do = <%> NAT as XFinSequence of NAT ;
A82: len do = o by A81;
Sum do = 0 ;
then A83: (Sum do) div (b |^ o) = 0 by NAT_2:2;
set d9 = D;
A84: for x being Nat st x in dom do holds
D . x = do . x ;
( dom D = (len do) + (len D) & ( for x being Nat st x in dom D holds
D . ((len do) + x) = D . x ) ) by A81, A82;
then D = do ^ D by A84, AFINSQ_1:def_3;
then A85: n = (Sum do) + (Sum D) by A42, AFINSQ_2:55;
reconsider bo = b |^ o as Element of NAT by ORDINAL1:def_12;
A86: bo <> 0 by A1, PREPOWER:5;
A87: now__::_thesis:_for_k_being_Nat_st_k_in_dom_<%(D_._o)%>_holds_
D_._k_=_<%(D_._o)%>_._k
let k be Nat; ::_thesis: ( k in dom <%(D . o)%> implies D . k = <%(D . o)%> . k )
assume k in dom <%(D . o)%> ; ::_thesis: D . k = <%(D . o)%> . k
then k in 1 by AFINSQ_1:33;
then k < 1 by NAT_1:44;
then k = 0 by NAT_1:14;
hence D . k = <%(D . o)%> . k by A81, AFINSQ_1:def_4; ::_thesis: verum
end;
reconsider o1 = o + 1 as Element of NAT ;
o1 <= k by A81, NAT_1:13;
then A88: o1 < len d by XREAL_1:147;
reconsider oo1 = (len d) - o1 as Element of NAT by A81;
defpred S1[ Nat, set ] means $2 = D . ($1 + o1);
reconsider do1 = D | o1 as XFinSequence of NAT ;
A89: for u being Nat st u in oo1 holds
ex x being Element of NAT st S1[u,x] ;
consider d91 being XFinSequence of NAT such that
A90: ( dom d91 = oo1 & ( for x being Nat st x in oo1 holds
S1[x,d91 . x] ) ) from STIRL2_1:sch_5(A89);
A91: len d = len D by A40;
then A92: len do1 = o1 by A88, AFINSQ_1:11;
then A93: dom D = (len do1) + (len d91) by A40, A90;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_d91_holds_
b_|^_o1_divides_d91_._k
let k be Nat; ::_thesis: ( k in dom d91 implies b |^ o1 divides d91 . k )
reconsider K = k as Element of NAT by ORDINAL1:def_12;
assume A94: k in dom d91 ; ::_thesis: b |^ o1 divides d91 . k
then k < len d91 by NAT_1:44;
then o1 + k < dom D by A92, A93, XREAL_1:8;
then o1 + k in dom D by NAT_1:44;
then D . (o1 + k) = (d . (o1 + k)) * (b |^ (o1 + k)) by A41;
then d91 . K = (d . (o1 + k)) * (b |^ (o1 + k)) by A90, A94
.= (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; ::_thesis: verum
end;
then A95: b |^ o1 divides Sum d91 by Th2;
A96: now__::_thesis:_for_k_being_Nat_st_k_in_dom_d91_holds_
D_._((len_<%(D_._o)%>)_+_k)_=_d91_._k
let k be Nat; ::_thesis: ( k in dom d91 implies D . ((len <%(D . o)%>) + k) = d91 . k )
assume A97: k in dom d91 ; ::_thesis: D . ((len <%(D . o)%>) + k) = d91 . k
thus D . ((len <%(D . o)%>) + k) = D . ((len do1) + k) by A81, A92, AFINSQ_1:33
.= d91 . k by A90, A92, A97 ; ::_thesis: verum
end;
dom D = 1 + (dom d91) by A40, A81, A90
.= (len <%(D . o)%>) + (len d91) by AFINSQ_1:34 ;
then D = <%(D . o)%> ^ d91 by A87, A96, AFINSQ_1:def_3;
then A98: Sum D = (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 A90, A92, FUNCT_1:47;
then D = do1 ^ d91 by A93, AFINSQ_1:def_3;
then A99: n = (Sum do1) + (Sum d91) by A42, AFINSQ_2:55;
reconsider bo1 = b |^ o1 as Element of NAT by ORDINAL1:def_12;
consider ok1 being Nat such that
A100: ok1 + 1 = o1 ;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_D_holds_
b_|^_o_divides_D_._k
let k be Nat; ::_thesis: ( k in dom D implies b |^ o divides D . k )
reconsider K = k as Element of NAT by ORDINAL1:def_12;
assume k in dom D ; ::_thesis: b |^ o divides D . k
then D . K = (d . (o + k)) * (b |^ (o + k)) by A41, A81
.= (d . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8
.= ((d . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides D . k by NAT_D:def_3; ::_thesis: verum
end;
then A101: b |^ o divides Sum D by Th2;
then (Sum D) mod (b |^ o) = 0 by A86, PEPIN:6;
then n div (b |^ o) = ((Sum D) div (b |^ o)) + ((Sum do) div (b |^ o)) by A85, NAT_D:19;
then A102: (n div (b |^ o)) * (b |^ o) = Sum D by A83, A101, NAT_D:3;
reconsider do = <%> NAT as XFinSequence of NAT ;
A103: len do = o by A81;
Sum do = 0 ;
then A104: (Sum do) div (b |^ o) = 0 by NAT_2:2;
set d9 = E;
A105: for x being Nat st x in dom do holds
E . x = do . x ;
( dom E = (len do) + (len E) & ( for x being Nat st x in dom E holds
E . ((len do) + x) = E . x ) ) by A81, A103;
then E = do ^ E by A105, AFINSQ_1:def_3;
then A106: n = (Sum do) + (Sum E) by A61, AFINSQ_2:55;
reconsider bo = b |^ o as Element of NAT by ORDINAL1:def_12;
A107: bo <> 0 by A1, PREPOWER:5;
reconsider ok1 = ok1 as Element of NAT by ORDINAL1:def_12;
reconsider g1 = (b1 (#) (b GeoSeq)) | (ok1 + 1) as XFinSequence of NAT by Th1;
A108: 1 - b <> 0 by A1;
dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def_1;
then A109: o1 c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def_2;
then A110: len do1 = len g1 by A92, A100, RELAT_1:62;
A111: dom g1 = o1 by A100, A109, RELAT_1:62;
A112: for i being Nat st i in dom do1 holds
do1 . i <= g1 . i
proof
let i be Nat; ::_thesis: ( i in dom do1 implies do1 . i <= g1 . i )
reconsider I = i as Element of NAT by ORDINAL1:def_12;
assume A113: i in dom do1 ; ::_thesis: do1 . i <= g1 . i
then i in o1 by A88, A91, AFINSQ_1:11;
then A114: g1 . I = ((b - 1) (#) (b GeoSeq)) . I by A111, FUNCT_1:47
.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def_1 ;
A115: dom do1 c= dom D by RELAT_1:60;
then d . i < b1 + 1 by A39, A40, A113;
then A116: d . i <= b1 by NAT_1:13;
do1 . i = D . i by A113, FUNCT_1:47
.= (d . i) * (b |^ i) by A41, A113, A115 ;
hence do1 . i <= g1 . i by A114, A116, XREAL_1:64; ::_thesis: verum
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 A100
.= - (1 - (b |^ o1)) by A108, XCMPLX_1:87
.= (b |^ o1) - 1 ;
then Sum do1 < ((b |^ o1) - 1) + 1 by A110, A112, AFINSQ_2:57, XREAL_1:145;
then A117: (Sum do1) div (b |^ o1) = 0 by NAT_D:27;
bo1 <> 0 by A1, PREPOWER:5;
then (Sum d91) mod (b |^ o1) = 0 by A95, PEPIN:6;
then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by A99, NAT_D:19;
then (n div (b |^ o1)) * (b |^ o1) = Sum d91 by A117, A95, NAT_D:3;
then D . o = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A102, A98, AFINSQ_2:53;
then (d . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A40, A41, A76;
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) by NEWTON:5;
then A118: d . o = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o) by A86, XCMPLX_1:89;
reconsider o1 = o + 1 as Element of NAT ;
reconsider do1 = E | o1 as XFinSequence of NAT ;
A119: len e = len E by A59;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_E_holds_
b_|^_o_divides_E_._k
let k be Nat; ::_thesis: ( k in dom E implies b |^ o divides E . k )
reconsider K = k as Element of NAT by ORDINAL1:def_12;
assume k in dom E ; ::_thesis: b |^ o divides E . k
then E . K = (e . (o + k)) * (b |^ (o + k)) by A60, A81
.= (e . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8
.= ((e . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides E . k by NAT_D:def_3; ::_thesis: verum
end;
then A120: b |^ o divides Sum E by Th2;
then (Sum E) mod (b |^ o) = 0 by A107, PEPIN:6;
then n div (b |^ o) = ((Sum E) div (b |^ o)) + ((Sum do) div (b |^ o)) by A106, NAT_D:19;
then A121: (n div (b |^ o)) * (b |^ o) = Sum E by A104, A120, NAT_D:3;
A122: now__::_thesis:_for_k_being_Nat_st_k_in_dom_<%(E_._o)%>_holds_
E_._k_=_<%(E_._o)%>_._k
let k be Nat; ::_thesis: ( k in dom <%(E . o)%> implies E . k = <%(E . o)%> . k )
assume k in dom <%(E . o)%> ; ::_thesis: E . k = <%(E . o)%> . k
then k in 1 by AFINSQ_1:33;
then k < 1 by NAT_1:44;
then k = 0 by NAT_1:14;
hence E . k = <%(E . o)%> . k by A81, AFINSQ_1:def_4; ::_thesis: verum
end;
reconsider oo1 = (len d) - o1 as Element of NAT by A81;
defpred S2[ Nat, set ] means $2 = E . ($1 + o1);
A123: for u being Nat st u in oo1 holds
ex x being Element of NAT st S2[u,x] ;
consider d91 being XFinSequence of NAT such that
A124: ( dom d91 = oo1 & ( for x being Nat st x in oo1 holds
S2[x,d91 . x] ) ) from STIRL2_1:sch_5(A123);
o1 <= k by A81, NAT_1:13;
then A125: o1 < len d by XREAL_1:147;
then A126: len do1 = o1 by A75, A119, AFINSQ_1:11;
A127: now__::_thesis:_for_k_being_Nat_st_k_in_dom_d91_holds_
E_._((len_<%(E_._o)%>)_+_k)_=_d91_._k
let k be Nat; ::_thesis: ( k in dom d91 implies E . ((len <%(E . o)%>) + k) = d91 . k )
assume A128: k in dom d91 ; ::_thesis: E . ((len <%(E . o)%>) + k) = d91 . k
thus E . ((len <%(E . o)%>) + k) = E . ((len do1) + k) by A81, A126, AFINSQ_1:33
.= d91 . k by A124, A126, A128 ; ::_thesis: verum
end;
reconsider bo1 = b |^ o1 as Element of NAT by ORDINAL1:def_12;
consider ok1 being Nat such that
A129: ok1 + 1 = o1 ;
A130: dom E = (len do1) + (len d91) by A59, A75, A124, A126;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_d91_holds_
b_|^_o1_divides_d91_._k
let k be Nat; ::_thesis: ( k in dom d91 implies b |^ o1 divides d91 . k )
reconsider K = k as Element of NAT by ORDINAL1:def_12;
assume A131: k in dom d91 ; ::_thesis: b |^ o1 divides d91 . k
then k < len d91 by NAT_1:44;
then o1 + k < dom E by A126, A130, XREAL_1:8;
then o1 + k in dom E by NAT_1:44;
then E . (o1 + k) = (e . (o1 + k)) * (b |^ (o1 + k)) by A60;
then d91 . K = (e . (o1 + k)) * (b |^ (o1 + k)) by A124, A131
.= (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; ::_thesis: verum
end;
then A132: b |^ o1 divides Sum d91 by Th2;
reconsider ok1 = ok1 as Element of NAT by ORDINAL1:def_12;
reconsider g1 = (b1 (#) (b GeoSeq)) | (ok1 + 1) as XFinSequence of NAT by Th1;
A133: 1 - b <> 0 by A1;
dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def_1;
then A134: o1 c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def_2;
then A135: len do1 = len g1 by A126, A129, RELAT_1:62;
A136: dom g1 = o1 by A129, A134, RELAT_1:62;
A137: for i being Nat st i in dom do1 holds
do1 . i <= g1 . i
proof
let i be Nat; ::_thesis: ( i in dom do1 implies do1 . i <= g1 . i )
reconsider I = i as Element of NAT by ORDINAL1:def_12;
assume A138: i in dom do1 ; ::_thesis: do1 . i <= g1 . i
then i in o1 by A75, A125, A119, AFINSQ_1:11;
then A139: g1 . I = ((b - 1) (#) (b GeoSeq)) . I by A136, FUNCT_1:47
.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def_1 ;
A140: dom do1 c= dom E by RELAT_1:60;
then e . i < b1 + 1 by A58, A59, A138;
then A141: e . i <= b1 by NAT_1:13;
do1 . i = E . i by A138, FUNCT_1:47
.= (e . i) * (b |^ i) by A60, A138, A140 ;
hence do1 . i <= g1 . i by A139, A141, XREAL_1:64; ::_thesis: verum
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 A129
.= - (1 - (b |^ o1)) by A133, XCMPLX_1:87
.= (b |^ o1) - 1 ;
then Sum do1 < ((b |^ o1) - 1) + 1 by A135, A137, AFINSQ_2:57, XREAL_1:145;
then A142: (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 A124, A126, FUNCT_1:47;
then E = do1 ^ d91 by A130, AFINSQ_1:def_3;
then A143: n = (Sum do1) + (Sum d91) by A61, AFINSQ_2:55;
bo1 <> 0 by A1, PREPOWER:5;
then (Sum d91) mod (b |^ o1) = 0 by A132, PEPIN:6;
then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by A143, NAT_D:19;
then A144: (n div (b |^ o1)) * (b |^ o1) = Sum d91 by A142, A132, NAT_D:3;
dom E = 1 + (dom d91) by A59, A75, A81, A124
.= (len <%(E . o)%>) + (len d91) by AFINSQ_1:34 ;
then E = <%(E . o)%> ^ d91 by A122, A127, AFINSQ_1:def_3;
then Sum E = (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 A121, A144, AFINSQ_2:53;
then (e . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A59, A60, A75, A76;
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) by NEWTON:5;
hence d . a = e . a by A118, A107, XCMPLX_1:89; ::_thesis: verum
end;
supposeA145: ( o > 0 & o = k ) ; ::_thesis: d . b1 = e . b1
set d9 = <%(D . o)%>;
reconsider do = D | o as XFinSequence of NAT ;
A146: len d = len D by A40;
then A147: len do = o by A78, AFINSQ_1:11;
A148: len <%(D . o)%> = oo by A145, AFINSQ_1:34;
then A149: dom D = (len do) + (len <%(D . o)%>) by A40, A147;
A150: for x being Nat st x in dom <%(D . o)%> holds
D . ((len do) + x) = <%(D . o)%> . x
proof
let x be Nat; ::_thesis: ( x in dom <%(D . o)%> implies D . ((len do) + x) = <%(D . o)%> . x )
assume x in dom <%(D . o)%> ; ::_thesis: D . ((len do) + x) = <%(D . o)%> . x
then x < 1 by A145, A148, NAT_1:44;
then x = 0 by NAT_1:14;
hence D . ((len do) + x) = <%(D . o)%> . x by A147, AFINSQ_1:34; ::_thesis: verum
end;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_<%(D_._o)%>_holds_
b_|^_o_divides_<%(D_._o)%>_._k
let k be Nat; ::_thesis: ( k in dom <%(D . o)%> implies b |^ o divides <%(D . o)%> . k )
reconsider K = k as Element of NAT by ORDINAL1:def_12;
assume A151: k in dom <%(D . o)%> ; ::_thesis: b |^ o divides <%(D . o)%> . k
then k < len <%(D . o)%> by NAT_1:44;
then o + k < dom D by A147, A149, XREAL_1:8;
then o + k in dom D by NAT_1:44;
then D . (o + k) = (d . (o + k)) * (b |^ (o + k)) by A41;
then <%(D . o)%> . K = (d . (o + k)) * (b |^ (o + k)) by A147, A150, A151
.= (d . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8
.= ((d . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides <%(D . o)%> . k by NAT_D:def_3; ::_thesis: verum
end;
then A152: b |^ o divides Sum <%(D . o)%> by Th2;
reconsider bo = b |^ o as Element of NAT by ORDINAL1:def_12;
A153: 1 - b <> 0 by A1;
consider ok being Nat such that
A154: ok + 1 = o by A145, NAT_1:6;
reconsider ok = ok as Element of NAT by ORDINAL1:def_12;
reconsider g = (b1 (#) (b GeoSeq)) | (ok + 1) as XFinSequence of NAT by Th1;
A155: 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 A154
.= - (1 - (b |^ o)) by A153, XCMPLX_1:87
.= (b |^ o) - 1 ;
consider ok being Nat such that
A156: ok + 1 = o by A145, NAT_1:6;
dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def_1;
then A157: o c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def_2;
then A158: dom g = o by A154, RELAT_1:62;
A159: for i being Nat st i in dom do holds
do . i <= g . i
proof
let i be Nat; ::_thesis: ( i in dom do implies do . i <= g . i )
reconsider I = i as Element of NAT by ORDINAL1:def_12;
assume A160: i in dom do ; ::_thesis: do . i <= g . i
then i in o by A78, A146, AFINSQ_1:11;
then A161: g . I = ((b - 1) (#) (b GeoSeq)) . I by A158, FUNCT_1:47
.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def_1 ;
A162: dom do c= dom D by RELAT_1:60;
then d . i < b1 + 1 by A39, A40, A160;
then A163: d . i <= b1 by NAT_1:13;
do . i = D . i by A160, FUNCT_1:47
.= (d . i) * (b |^ i) by A41, A160, A162 ;
hence do . i <= g . i by A161, A163, XREAL_1:64; ::_thesis: verum
end;
len do = len g by A147, A154, A157, RELAT_1:62;
then Sum do < ((b |^ o) - 1) + 1 by A155, A159, AFINSQ_2:57, XREAL_1:145;
then A164: (Sum do) div (b |^ o) = 0 by NAT_D:27;
for x being Nat st x in dom do holds
D . x = do . x by FUNCT_1:47;
then D = do ^ <%(D . o)%> by A149, A150, AFINSQ_1:def_3;
then A165: n = (Sum do) + (Sum <%(D . o)%>) by A42, AFINSQ_2:55;
A166: bo <> 0 by A1, PREPOWER:5;
then (Sum <%(D . o)%>) mod (b |^ o) = 0 by A152, PEPIN:6;
then n div (b |^ o) = ((Sum <%(D . o)%>) div (b |^ o)) + ((Sum do) div (b |^ o)) by A165, NAT_D:19;
then (n div (b |^ o)) * (b |^ o) = Sum <%(D . o)%> by A164, A152, 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 A40, A41, A76;
then A167: d . o = ((n div (b |^ o)) * (b |^ o)) / (b |^ o) by A166, XCMPLX_1:89;
set d9 = <%(E . o)%>;
reconsider do = E | o as XFinSequence of NAT ;
A168: len e = len E by A59;
then A169: len do = o by A75, A78, AFINSQ_1:11;
A170: len <%(E . o)%> = oo by A145, AFINSQ_1:34;
then A171: dom E = (len do) + (len <%(E . o)%>) by A59, A75, A169;
A172: for x being Nat st x in dom <%(E . o)%> holds
E . ((len do) + x) = <%(E . o)%> . x
proof
let x be Nat; ::_thesis: ( x in dom <%(E . o)%> implies E . ((len do) + x) = <%(E . o)%> . x )
assume x in dom <%(E . o)%> ; ::_thesis: E . ((len do) + x) = <%(E . o)%> . x
then x < 1 by A145, A170, NAT_1:44;
then x = 0 by NAT_1:14;
hence E . ((len do) + x) = <%(E . o)%> . x by A169, AFINSQ_1:34; ::_thesis: verum
end;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_<%(E_._o)%>_holds_
b_|^_o_divides_<%(E_._o)%>_._k
let k be Nat; ::_thesis: ( k in dom <%(E . o)%> implies b |^ o divides <%(E . o)%> . k )
reconsider K = k as Element of NAT by ORDINAL1:def_12;
assume A173: k in dom <%(E . o)%> ; ::_thesis: b |^ o divides <%(E . o)%> . k
then k < len <%(E . o)%> by NAT_1:44;
then o + k < dom E by A169, A171, XREAL_1:8;
then o + k in dom E by NAT_1:44;
then E . (o + k) = (e . (o + k)) * (b |^ (o + k)) by A60;
then <%(E . o)%> . K = (e . (o + k)) * (b |^ (o + k)) by A169, A172, A173
.= (e . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8
.= ((e . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides <%(E . o)%> . k by NAT_D:def_3; ::_thesis: verum
end;
then A174: b |^ o divides Sum <%(E . o)%> by Th2;
reconsider ok = 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;
A175: 1 - b <> 0 by A1;
dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def_1;
then A176: o c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def_2;
then A177: len do = len g by A169, A156, RELAT_1:62;
A178: dom g = o by A156, A176, RELAT_1:62;
A179: for i being Nat st i in dom do holds
do . i <= g . i
proof
let i be Nat; ::_thesis: ( i in dom do implies do . i <= g . i )
reconsider I = i as Element of NAT by ORDINAL1:def_12;
assume A180: i in dom do ; ::_thesis: do . i <= g . i
then i in o by A75, A78, A168, AFINSQ_1:11;
then A181: g . I = ((b - 1) (#) (b GeoSeq)) . I by A178, FUNCT_1:47
.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def_1 ;
A182: dom do c= dom E by RELAT_1:60;
then e . i < b1 + 1 by A58, A59, A180;
then A183: e . i <= b1 by NAT_1:13;
do . i = E . i by A180, FUNCT_1:47
.= (e . i) * (b |^ i) by A60, A180, A182 ;
hence do . i <= g . i by A181, A183, XREAL_1:64; ::_thesis: verum
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 A156
.= - (1 - (b |^ o)) by A175, XCMPLX_1:87
.= (b |^ o) - 1 ;
then Sum do < ((b |^ o) - 1) + 1 by A177, A179, AFINSQ_2:57, XREAL_1:145;
then A184: (Sum do) div (b |^ o) = 0 by NAT_D:27;
for x being Nat st x in dom do holds
E . x = do . x by FUNCT_1:47;
then E = do ^ <%(E . o)%> by A171, A172, AFINSQ_1:def_3;
then A185: n = (Sum do) + (Sum <%(E . o)%>) by A61, AFINSQ_2:55;
A186: bo <> 0 by A1, PREPOWER:5;
then (Sum <%(E . o)%>) mod (b |^ o) = 0 by A174, PEPIN:6;
then n div (b |^ o) = ((Sum <%(E . o)%>) div (b |^ o)) + ((Sum do) div (b |^ o)) by A185, NAT_D:19;
then (n div (b |^ o)) * (b |^ o) = Sum <%(E . o)%> by A184, A174, 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 A59, A60, A75, A76;
hence d . a = e . a by A167, A186, XCMPLX_1:89; ::_thesis: verum
end;
supposeA187: ( o > 0 & o < k ) ; ::_thesis: d . b1 = e . b1
reconsider o1 = o + 1 as Element of NAT ;
A188: o1 <= k by A187, NAT_1:13;
then A189: 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 S1[ Nat, set ] means $2 = D . ($1 + o);
consider ok1 being Nat such that
A190: ok1 + 1 = o1 ;
reconsider ok1 = ok1 as Element of NAT by ORDINAL1:def_12;
reconsider g1 = (b1 (#) (b GeoSeq)) | (ok1 + 1) as XFinSequence of NAT by Th1;
A191: len d = len D by A40;
then A192: len do1 = o1 by A189, AFINSQ_1:11;
dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def_1;
then A193: o1 c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def_2;
then A194: len do1 = len g1 by A192, A190, RELAT_1:62;
A195: dom g1 = o1 by A190, A193, RELAT_1:62;
A196: for i being Nat st i in dom do1 holds
do1 . i <= g1 . i
proof
let i be Nat; ::_thesis: ( i in dom do1 implies do1 . i <= g1 . i )
reconsider I = i as Element of NAT by ORDINAL1:def_12;
assume A197: i in dom do1 ; ::_thesis: do1 . i <= g1 . i
then i in o1 by A189, A191, AFINSQ_1:11;
then A198: g1 . I = ((b - 1) (#) (b GeoSeq)) . I by A195, FUNCT_1:47
.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def_1 ;
A199: dom do1 c= dom D by RELAT_1:60;
then d . i < b1 + 1 by A39, A40, A197;
then A200: d . i <= b1 by NAT_1:13;
do1 . i = D . i by A197, FUNCT_1:47
.= (d . i) * (b |^ i) by A41, A197, A199 ;
hence do1 . i <= g1 . i by A198, A200, XREAL_1:64; ::_thesis: verum
end;
k < len d by XREAL_1:147;
then reconsider oo1 = (len d) - o1 as Element of NAT by A188, NAT_1:21, XXREAL_0:2;
A201: for u being Nat st u in oo holds
ex x being Element of NAT st S1[u,x] ;
consider d9 being XFinSequence of NAT such that
A202: ( dom d9 = oo & ( for x being Nat st x in oo holds
S1[x,d9 . x] ) ) from STIRL2_1:sch_5(A201);
A203: now__::_thesis:_for_k_being_Nat_st_k_in_dom_<%(D_._o)%>_holds_
d9_._k_=_<%(D_._o)%>_._k
let k be Nat; ::_thesis: ( k in dom <%(D . o)%> implies d9 . k = <%(D . o)%> . k )
assume k in dom <%(D . o)%> ; ::_thesis: d9 . k = <%(D . o)%> . k
then k in 1 by AFINSQ_1:33;
then k < 1 by NAT_1:44;
then A204: k = 0 by NAT_1:14;
oo > 0 by A78, XREAL_1:50;
then k in dom d9 by A202, A204, NAT_1:44;
hence d9 . k = D . (k + o) by A202
.= <%(D . o)%> . k by A204, AFINSQ_1:def_4 ;
::_thesis: verum
end;
defpred S2[ Nat, set ] means $2 = D . ($1 + o1);
A205: for u being Nat st u in oo1 holds
ex x being Element of NAT st S2[u,x] ;
consider d91 being XFinSequence of NAT such that
A206: ( dom d91 = oo1 & ( for x being Nat st x in oo1 holds
S2[x,d91 . x] ) ) from STIRL2_1:sch_5(A205);
reconsider do = D | o as XFinSequence of NAT ;
A207: len d = len D by A40;
then A208: len do = o by A78, AFINSQ_1:11;
then A209: dom D = (len do) + (len d9) by A40, A202;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_d9_holds_
b_|^_o_divides_d9_._k
let k be Nat; ::_thesis: ( k in dom d9 implies b |^ o divides d9 . k )
reconsider K = k as Element of NAT by ORDINAL1:def_12;
assume A210: k in dom d9 ; ::_thesis: b |^ o divides d9 . k
then k < len d9 by NAT_1:44;
then o + k < dom D by A208, A209, XREAL_1:8;
then o + k in dom D by NAT_1:44;
then D . (o + k) = (d . (o + k)) * (b |^ (o + k)) by A41;
then d9 . K = (d . (o + k)) * (b |^ (o + k)) by A202, A210
.= (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; ::_thesis: verum
end;
then A211: b |^ o divides Sum d9 by Th2;
( ( for x being Nat st x in dom do holds
D . x = do . x ) & ( for x being Nat st x in dom d9 holds
D . ((len do) + x) = d9 . x ) ) by A202, A208, FUNCT_1:47;
then D = do ^ d9 by A209, AFINSQ_1:def_3;
then A212: n = (Sum do) + (Sum d9) by A42, AFINSQ_2:55;
consider ok being Nat such that
A213: ok + 1 = o by A187, NAT_1:6;
reconsider ok = ok as Element of NAT by ORDINAL1:def_12;
reconsider g = (b1 (#) (b GeoSeq)) | (ok + 1) as XFinSequence of NAT by Th1;
A214: 1 - b <> 0 by A1;
A215: 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 A213
.= - (1 - (b |^ o)) by A214, XCMPLX_1:87
.= (b |^ o) - 1 ;
dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def_1;
then A216: o c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def_2;
then A217: dom g = o by A213, RELAT_1:62;
A218: for i being Nat st i in dom do holds
do . i <= g . i
proof
let i be Nat; ::_thesis: ( i in dom do implies do . i <= g . i )
reconsider I = i as Element of NAT by ORDINAL1:def_12;
assume A219: i in dom do ; ::_thesis: do . i <= g . i
then i in o by A78, A207, AFINSQ_1:11;
then A220: g . I = ((b - 1) (#) (b GeoSeq)) . I by A217, FUNCT_1:47
.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def_1 ;
A221: dom do c= dom D by RELAT_1:60;
then d . i < b1 + 1 by A39, A40, A219;
then A222: d . i <= b1 by NAT_1:13;
do . i = D . i by A219, FUNCT_1:47
.= (d . i) * (b |^ i) by A41, A219, A221 ;
hence do . i <= g . i by A220, A222, XREAL_1:64; ::_thesis: verum
end;
A223: now__::_thesis:_for_k_being_Nat_st_k_in_dom_d91_holds_
d9_._((len_<%(D_._o)%>)_+_k)_=_d91_._k
let k be Nat; ::_thesis: ( k in dom d91 implies d9 . ((len <%(D . o)%>) + k) = d91 . k )
assume A224: k in dom d91 ; ::_thesis: d9 . ((len <%(D . o)%>) + k) = d91 . k
then k < oo1 by A206, NAT_1:44;
then k + 1 < oo1 + 1 by XREAL_1:8;
then A225: k + 1 in dom d9 by A202, NAT_1:44;
thus d9 . ((len <%(D . o)%>) + k) = d9 . (1 + k) by AFINSQ_1:33
.= D . ((len do) + (k + 1)) by A202, A208, A225
.= D . ((len do1) + k) by A208, A192
.= d91 . k by A206, A192, A224 ; ::_thesis: verum
end;
dom d9 = 1 + (dom d91) by A202, A206
.= (len <%(D . o)%>) + (len d91) by AFINSQ_1:34 ;
then d9 = <%(D . o)%> ^ d91 by A203, A223, AFINSQ_1:def_3;
then A226: Sum d9 = (Sum <%(D . o)%>) + (Sum d91) by AFINSQ_2:55;
defpred S3[ Nat, set ] means $2 = E . ($1 + o);
A227: 1 - b <> 0 by A1;
consider ok being Nat such that
A228: ok + 1 = o by A187, NAT_1:6;
A229: dom D = (len do1) + (len d91) by A40, A206, A192;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_d91_holds_
b_|^_o1_divides_d91_._k
let k be Nat; ::_thesis: ( k in dom d91 implies b |^ o1 divides d91 . k )
reconsider K = k as Element of NAT by ORDINAL1:def_12;
assume A230: k in dom d91 ; ::_thesis: b |^ o1 divides d91 . k
then k < len d91 by NAT_1:44;
then o1 + k < dom D by A192, A229, XREAL_1:8;
then o1 + k in dom D by NAT_1:44;
then D . (o1 + k) = (d . (o1 + k)) * (b |^ (o1 + k)) by A41;
then d91 . K = (d . (o1 + k)) * (b |^ (o1 + k)) by A206, A230
.= (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; ::_thesis: verum
end;
then A231: b |^ o1 divides Sum d91 by Th2;
len do = len g by A208, A213, A216, RELAT_1:62;
then Sum do < ((b |^ o) - 1) + 1 by A215, A218, AFINSQ_2:57, XREAL_1:145;
then A232: (Sum do) div (b |^ o) = 0 by NAT_D:27;
A233: 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 A190
.= - (1 - (b |^ o1)) by A233, XCMPLX_1:87
.= (b |^ o1) - 1 ;
then Sum do1 < ((b |^ o1) - 1) + 1 by A194, A196, AFINSQ_2:57, XREAL_1:145;
then A234: (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 A206, A192, FUNCT_1:47;
then D = do1 ^ d91 by A229, AFINSQ_1:def_3;
then A235: n = (Sum do1) + (Sum d91) by A42, AFINSQ_2:55;
bo1 <> 0 by A1, PREPOWER:5;
then (Sum d91) mod (b |^ o1) = 0 by A231, PEPIN:6;
then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by A235, NAT_D:19;
then A236: (n div (b |^ o1)) * (b |^ o1) = Sum d91 by A234, A231, NAT_D:3;
A237: bo <> 0 by A1, PREPOWER:5;
then (Sum d9) mod (b |^ o) = 0 by A211, PEPIN:6;
then n div (b |^ o) = ((Sum d9) div (b |^ o)) + ((Sum do) div (b |^ o)) by A212, NAT_D:19;
then ( (n div (b |^ o)) * (b |^ o) = Sum d9 & Sum <%(D . o)%> = D . o ) by A232, A211, AFINSQ_2:53, NAT_D:3;
then (d . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A40, A41, A76, A236, A226;
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) by NEWTON:5;
then A238: d . o = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o) by A237, XCMPLX_1:89;
reconsider o1 = o + 1 as Element of NAT ;
A239: o1 <= k by A187, NAT_1:13;
then A240: o1 < len d by XREAL_1:147;
reconsider ok = ok as Element of NAT by ORDINAL1:def_12;
reconsider g = (b1 (#) (b GeoSeq)) | (ok + 1) as XFinSequence of NAT by Th1;
A241: 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
A242: ok1 + 1 = o1 ;
reconsider ok1 = ok1 as Element of NAT by ORDINAL1:def_12;
reconsider g1 = (b1 (#) (b GeoSeq)) | (ok1 + 1) as XFinSequence of NAT by Th1;
A243: len e = len E by A59;
then A244: len do1 = o1 by A75, A240, AFINSQ_1:11;
dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def_1;
then A245: o1 c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def_2;
then A246: len do1 = len g1 by A244, A242, RELAT_1:62;
A247: dom g1 = o1 by A242, A245, RELAT_1:62;
A248: for i being Nat st i in dom do1 holds
do1 . i <= g1 . i
proof
let i be Nat; ::_thesis: ( i in dom do1 implies do1 . i <= g1 . i )
reconsider I = i as Element of NAT by ORDINAL1:def_12;
assume A249: i in dom do1 ; ::_thesis: do1 . i <= g1 . i
then i in o1 by A75, A240, A243, AFINSQ_1:11;
then A250: g1 . I = ((b - 1) (#) (b GeoSeq)) . I by A247, FUNCT_1:47
.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def_1 ;
A251: dom do1 c= dom E by RELAT_1:60;
then e . i < b1 + 1 by A58, A59, A249;
then A252: e . i <= b1 by NAT_1:13;
do1 . i = E . i by A249, FUNCT_1:47
.= (e . i) * (b |^ i) by A60, A249, A251 ;
hence do1 . i <= g1 . i by A250, A252, XREAL_1:64; ::_thesis: verum
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 A242
.= - (1 - (b |^ o1)) by A241, XCMPLX_1:87
.= (b |^ o1) - 1 ;
then Sum do1 < ((b |^ o1) - 1) + 1 by A246, A248, AFINSQ_2:57, XREAL_1:145;
then A253: (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 A239, NAT_1:21, XXREAL_0:2;
A254: for u being Nat st u in oo holds
ex x being Element of NAT st S3[u,x] ;
consider d9 being XFinSequence of NAT such that
A255: ( dom d9 = oo & ( for x being Nat st x in oo holds
S3[x,d9 . x] ) ) from STIRL2_1:sch_5(A254);
A256: now__::_thesis:_for_k_being_Nat_st_k_in_dom_<%(E_._o)%>_holds_
d9_._k_=_<%(E_._o)%>_._k
let k be Nat; ::_thesis: ( k in dom <%(E . o)%> implies d9 . k = <%(E . o)%> . k )
assume k in dom <%(E . o)%> ; ::_thesis: d9 . k = <%(E . o)%> . k
then k in 1 by AFINSQ_1:33;
then k < 1 by NAT_1:44;
then A257: k = 0 by NAT_1:14;
oo > 0 by A78, XREAL_1:50;
then k in dom d9 by A255, A257, NAT_1:44;
hence d9 . k = E . (k + o) by A255
.= <%(E . o)%> . k by A257, AFINSQ_1:def_4 ;
::_thesis: verum
end;
defpred S4[ Nat, set ] means $2 = E . ($1 + o1);
A258: for u being Nat st u in oo1 holds
ex x being Element of NAT st S4[u,x] ;
consider d91 being XFinSequence of NAT such that
A259: ( dom d91 = oo1 & ( for x being Nat st x in oo1 holds
S4[x,d91 . x] ) ) from STIRL2_1:sch_5(A258);
A260: dom E = (len do1) + (len d91) by A59, A75, A259, A244;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_d91_holds_
b_|^_o1_divides_d91_._k
let k be Nat; ::_thesis: ( k in dom d91 implies b |^ o1 divides d91 . k )
reconsider K = k as Element of NAT by ORDINAL1:def_12;
assume A261: k in dom d91 ; ::_thesis: b |^ o1 divides d91 . k
then k < len d91 by NAT_1:44;
then o1 + k < dom E by A244, A260, XREAL_1:8;
then o1 + k in dom E by NAT_1:44;
then E . (o1 + k) = (e . (o1 + k)) * (b |^ (o1 + k)) by A60;
then d91 . K = (e . (o1 + k)) * (b |^ (o1 + k)) by A259, A261
.= (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; ::_thesis: verum
end;
then A262: 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 A259, A244, FUNCT_1:47;
then E = do1 ^ d91 by A260, AFINSQ_1:def_3;
then A263: n = (Sum do1) + (Sum d91) by A61, AFINSQ_2:55;
bo1 <> 0 by A1, PREPOWER:5;
then (Sum d91) mod (b |^ o1) = 0 by A262, PEPIN:6;
then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by A263, NAT_D:19;
then A264: (n div (b |^ o1)) * (b |^ o1) = Sum d91 by A253, A262, NAT_D:3;
reconsider do = E | o as XFinSequence of NAT ;
A265: len e = len E by A59;
then A266: len do = o by A75, A78, AFINSQ_1:11;
then A267: dom E = (len do) + (len d9) by A59, A75, A255;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_d9_holds_
b_|^_o_divides_d9_._k
let k be Nat; ::_thesis: ( k in dom d9 implies b |^ o divides d9 . k )
reconsider K = k as Element of NAT by ORDINAL1:def_12;
assume A268: k in dom d9 ; ::_thesis: b |^ o divides d9 . k
then k < len d9 by NAT_1:44;
then o + k < dom E by A266, A267, XREAL_1:8;
then o + k in dom E by NAT_1:44;
then E . (o + k) = (e . (o + k)) * (b |^ (o + k)) by A60;
then d9 . K = (e . (o + k)) * (b |^ (o + k)) by A255, A268
.= (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; ::_thesis: verum
end;
then A269: b |^ o divides Sum d9 by Th2;
dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def_1;
then A270: o c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def_2;
then A271: len do = len g by A266, A228, RELAT_1:62;
A272: dom g = o by A228, A270, RELAT_1:62;
A273: for i being Nat st i in dom do holds
do . i <= g . i
proof
let i be Nat; ::_thesis: ( i in dom do implies do . i <= g . i )
reconsider I = i as Element of NAT by ORDINAL1:def_12;
assume A274: i in dom do ; ::_thesis: do . i <= g . i
then i in o by A75, A78, A265, AFINSQ_1:11;
then A275: g . I = ((b - 1) (#) (b GeoSeq)) . I by A272, FUNCT_1:47
.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def_1 ;
A276: dom do c= dom E by RELAT_1:60;
then e . i < b1 + 1 by A58, A59, A274;
then A277: e . i <= b1 by NAT_1:13;
do . i = E . i by A274, FUNCT_1:47
.= (e . i) * (b |^ i) by A60, A274, A276 ;
hence do . i <= g . i by A275, A277, XREAL_1:64; ::_thesis: verum
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 A228
.= - (1 - (b |^ o)) by A227, XCMPLX_1:87
.= (b |^ o) - 1 ;
then Sum do < ((b |^ o) - 1) + 1 by A271, A273, AFINSQ_2:57, XREAL_1:145;
then A278: (Sum do) div (b |^ o) = 0 by NAT_D:27;
A279: now__::_thesis:_for_k_being_Nat_st_k_in_dom_d91_holds_
d9_._((len_<%(E_._o)%>)_+_k)_=_d91_._k
let k be Nat; ::_thesis: ( k in dom d91 implies d9 . ((len <%(E . o)%>) + k) = d91 . k )
assume A280: k in dom d91 ; ::_thesis: d9 . ((len <%(E . o)%>) + k) = d91 . k
then k < oo1 by A259, NAT_1:44;
then k + 1 < oo1 + 1 by XREAL_1:8;
then A281: k + 1 in oo by NAT_1:44;
thus d9 . ((len <%(E . o)%>) + k) = d9 . (1 + k) by AFINSQ_1:33
.= E . ((len do) + (k + 1)) by A255, A266, A281
.= E . ((len do1) + k) by A266, A244
.= d91 . k by A259, A244, A280 ; ::_thesis: verum
end;
dom d9 = 1 + (dom d91) by A255, A259
.= (len <%(E . o)%>) + (len d91) by AFINSQ_1:34 ;
then d9 = <%(E . o)%> ^ d91 by A256, A279, AFINSQ_1:def_3;
then A282: Sum d9 = (Sum <%(E . o)%>) + (Sum d91) by AFINSQ_2:55;
( ( for x being Nat st x in dom do holds
E . x = do . x ) & ( for x being Nat st x in dom d9 holds
E . ((len do) + x) = d9 . x ) ) by A255, A266, FUNCT_1:47;
then E = do ^ d9 by A267, AFINSQ_1:def_3;
then A283: n = (Sum do) + (Sum d9) by A61, AFINSQ_2:55;
A284: bo <> 0 by A1, PREPOWER:5;
then (Sum d9) mod (b |^ o) = 0 by A269, PEPIN:6;
then n div (b |^ o) = ((Sum d9) div (b |^ o)) + ((Sum do) div (b |^ o)) by A283, NAT_D:19;
then (n div (b |^ o)) * (b |^ o) = Sum d9 by A278, A269, NAT_D:3;
then E . o = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A264, A282, AFINSQ_2:53;
then (e . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A59, A60, A75, A76;
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) by NEWTON:5;
hence d . a = e . a by A238, A284, XCMPLX_1:89; ::_thesis: verum
end;
end;
end;
hence d = e by A75, FUNCT_1:2; ::_thesis: verum
end;
assume that
n = 0 and
A285: ( d = <%0%> & e = <%0%> ) ; ::_thesis: d = e
thus d = e by A285; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines digits NUMERAL1:def_2_:_
for n, b being Nat st b > 1 holds
for b3 being XFinSequence of NAT holds
( ( n <> 0 implies ( b3 = digits (n,b) iff ( value (b3,b) = n & b3 . ((len b3) - 1) <> 0 & ( for i being Nat st i in dom b3 holds
( 0 <= b3 . i & b3 . i < b ) ) ) ) ) & ( not n <> 0 implies ( b3 = digits (n,b) iff b3 = <%0%> ) ) );
theorem Th4: :: NUMERAL1:4
for n, b being Nat st b > 1 holds
len (digits (n,b)) >= 1
proof
let n, b be Nat; ::_thesis: ( b > 1 implies len (digits (n,b)) >= 1 )
assume A1: b > 1 ; ::_thesis: len (digits (n,b)) >= 1
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: len (digits (n,b)) >= 1
then digits (n,b) = <%0%> by A1, Def2;
hence len (digits (n,b)) >= 1 by AFINSQ_1:33; ::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: len (digits (n,b)) >= 1
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 len (digits (n,b)) >= 1 by NAT_1:14; ::_thesis: verum
end;
end;
end;
theorem Th5: :: NUMERAL1:5
for n, b being Nat st b > 1 holds
value ((digits (n,b)),b) = n
proof
let n, b be Nat; ::_thesis: ( b > 1 implies value ((digits (n,b)),b) = n )
assume A1: b > 1 ; ::_thesis: value ((digits (n,b)),b) = n
percases ( n <> 0 or n = 0 ) ;
suppose n <> 0 ; ::_thesis: value ((digits (n,b)),b) = n
hence value ((digits (n,b)),b) = n by A1, Def2; ::_thesis: verum
end;
supposeA2: n = 0 ; ::_thesis: value ((digits (n,b)),b) = n
then A3: digits (n,b) = <%0%> by A1, Def2;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_<%0%>_holds_
<%0%>_._i_=_((digits_(n,b))_._i)_*_(b_|^_i)
let i be Nat; ::_thesis: ( i in dom <%0%> implies <%0%> . i = ((digits (n,b)) . i) * (b |^ i) )
assume i in dom <%0%> ; ::_thesis: <%0%> . i = ((digits (n,b)) . i) * (b |^ i)
then i in {0} by AFINSQ_1:def_4, CARD_1:49;
then A4: i = 0 by TARSKI:def_1;
hence <%0%> . i = 0 * (b |^ i) by AFINSQ_1:def_4
.= ((digits (n,b)) . i) * (b |^ i) by A3, A4, AFINSQ_1:def_4 ;
::_thesis: verum
end;
then value ((digits (n,b)),b) = Sum <%0%> by A3, Def1;
hence value ((digits (n,b)),b) = n by A2, AFINSQ_2:53; ::_thesis: verum
end;
end;
end;
begin
theorem Th6: :: NUMERAL1:6
for n, k being Nat st k = (10 |^ n) - 1 holds
9 divides k
proof
defpred S1[ Nat] means ex k being Nat st
( k = (10 |^ $1) - 1 & 9 divides k );
let n, k be Nat; ::_thesis: ( k = (10 |^ n) - 1 implies 9 divides k )
A1: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; ::_thesis: S1[k + 1]
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 S1[k + 1] by A5; ::_thesis: verum
end;
(10 |^ 0) - 1 = 1 - 1 by NEWTON:4
.= 0 ;
then A6: S1[ 0 ] by NAT_D:6;
for k being Nat holds S1[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 ; ::_thesis: 9 divides k
hence 9 divides k by A7; ::_thesis: verum
end;
theorem :: NUMERAL1:7
for n, b being Nat st b > 1 holds
( b divides n iff (digits (n,b)) . 0 = 0 )
proof
let n, b be Nat; ::_thesis: ( b > 1 implies ( b divides n iff (digits (n,b)) . 0 = 0 ) )
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 ; ::_thesis: ( b divides n iff (digits (n,b)) . 0 = 0 )
thus ( b divides n implies (digits (n,b)) . 0 = 0 ) ::_thesis: ( (digits (n,b)) . 0 = 0 implies b divides n )
proof
A4: len (digits (n,b)) >= 1 by A3, Th4;
assume A5: b divides n ; ::_thesis: (digits (n,b)) . 0 = 0
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;
percases ( len (digits (n,b)) = 1 or len (digits (n,b)) > 1 ) by A4, XXREAL_0:1;
supposeA9: len (digits (n,b)) = 1 ; ::_thesis: (digits (n,b)) . 0 = 0
A10: b divides Sum d by A3, A5, A8, Th5;
A11: 0 in dom (digits (n,b)) by A9, NAT_1:44;
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;
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: (digits (n,b)) . 0 = 0
then digits (n,b) = <%0%> by A3, Def2;
hence (digits (n,b)) . 0 = 0 by AFINSQ_1:34; ::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: (digits (n,b)) . 0 = 0
then (digits (n,b)) . 0 < b by A3, A11, Def2;
hence (digits (n,b)) . 0 = 0 by A12, NAT_D:7; ::_thesis: verum
end;
end;
end;
supposeA13: len (digits (n,b)) > 1 ; ::_thesis: (digits (n,b)) . 0 = 0
then reconsider k = (len (digits (n,b))) - 1 as Element of NAT by NAT_1:21;
defpred S1[ Nat, set ] means $2 = d . ($1 + 1);
A14: now__::_thesis:_for_l_being_Nat_st_l_in_dom_<%(d_._0)%>_holds_
d_._l_=_<%(d_._0)%>_._l
let l be Nat; ::_thesis: ( l in dom <%(d . 0)%> implies d . l = <%(d . 0)%> . l )
assume l in dom <%(d . 0)%> ; ::_thesis: d . l = <%(d . 0)%> . l
then l in 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 by AFINSQ_1:34; ::_thesis: verum
end;
A15: for u being Nat st u in k holds
ex x being Element of NAT st S1[u,x] ;
consider d9 being XFinSequence of NAT such that
A16: ( dom d9 = k & ( for x being Nat st x in k holds
S1[x,d9 . x] ) ) from STIRL2_1:sch_5(A15);
now__::_thesis:_for_i_being_Nat_st_i_in_dom_d9_holds_
b_divides_d9_._i
let i be Nat; ::_thesis: ( i in dom d9 implies b divides d9 . i )
assume A17: i in dom d9 ; ::_thesis: b divides d9 . i
then i < k by A16, NAT_1:44;
then i + 1 < k + 1 by XREAL_1:8;
then A18: i + 1 in dom d by A6, NAT_1:44;
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; ::_thesis: verum
end;
then b divides Sum d9 by Th2;
then A19: (Sum d9) mod B = 0 by A3, PEPIN:6;
A20: now__::_thesis:_for_l_being_Nat_st_l_in_dom_d9_holds_
d_._((len_<%(d_._0)%>)_+_l)_=_d9_._l
let l be Nat; ::_thesis: ( l in dom d9 implies d . ((len <%(d . 0)%>) + l) = d9 . l )
A21: (len <%(d . 0)%>) + l = l + 1 by AFINSQ_1:34;
assume l in dom d9 ; ::_thesis: d . ((len <%(d . 0)%>) + l) = d9 . l
hence d . ((len <%(d . 0)%>) + l) = d9 . l by A16, A21; ::_thesis: verum
end;
A22: 0 in dom (digits (n,b)) by A13, NAT_1:44;
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;
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: (digits (n,b)) . 0 = 0
then digits (n,b) = <%0%> by A3, Def2;
hence (digits (n,b)) . 0 = 0 by AFINSQ_1:34; ::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: (digits (n,b)) . 0 = 0
then (digits (n,b)) . 0 < b by A3, A22, Def2;
hence (digits (n,b)) . 0 = 0 by A23, NAT_D:7; ::_thesis: verum
end;
end;
end;
end;
end;
assume A24: (digits (n,b)) . 0 = 0 ; ::_thesis: b divides n
now__::_thesis:_for_i_being_Nat_st_i_in_dom_d_holds_
b_divides_d_._i
let i be Nat; ::_thesis: ( i in dom d implies b divides d . b1 )
assume A25: i in dom d ; ::_thesis: b divides d . b1
percases ( i = 0 or i > 0 ) ;
suppose i = 0 ; ::_thesis: b divides d . b1
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; ::_thesis: verum
end;
suppose i > 0 ; ::_thesis: b divides d . b1
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; ::_thesis: verum
end;
end;
end;
then b divides value ((digits (n,b)),b) by A2, Th2;
hence b divides n by A3, Th5; ::_thesis: verum
end;
theorem :: NUMERAL1:8
for n being Nat holds
( 2 divides n iff 2 divides (digits (n,10)) . 0 )
proof
let n be Nat; ::_thesis: ( 2 divides n iff 2 divides (digits (n,10)) . 0 )
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 ) ::_thesis: ( 2 divides (digits (n,10)) . 0 implies 2 divides n )
proof
A3: len (digits (n,10)) >= 1 by Th4;
assume A4: 2 divides n ; ::_thesis: 2 divides (digits (n,10)) . 0
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;
percases ( len (digits (n,10)) = 1 or len (digits (n,10)) > 1 ) by A3, XXREAL_0:1;
supposeA8: len (digits (n,10)) = 1 ; ::_thesis: 2 divides (digits (n,10)) . 0
then A9: 0 in dom (digits (n,10)) by NAT_1:44;
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 2 divides (digits (n,10)) . 0 ; ::_thesis: verum
end;
supposeA11: len (digits (n,10)) > 1 ; ::_thesis: 2 divides (digits (n,10)) . 0
then reconsider k = (len (digits (n,10))) - 1 as Element of NAT by NAT_1:21;
defpred S1[ Nat, set ] means $2 = d . ($1 + 1);
A12: now__::_thesis:_for_l_being_Nat_st_l_in_dom_<%(d_._0)%>_holds_
d_._l_=_<%(d_._0)%>_._l
let l be Nat; ::_thesis: ( l in dom <%(d . 0)%> implies d . l = <%(d . 0)%> . l )
assume l in dom <%(d . 0)%> ; ::_thesis: d . l = <%(d . 0)%> . l
then l in 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 by AFINSQ_1:34; ::_thesis: verum
end;
A13: for u being Nat st u in k holds
ex x being Element of NAT st S1[u,x] ;
consider d9 being XFinSequence of NAT such that
A14: ( dom d9 = k & ( for x being Nat st x in k holds
S1[x,d9 . x] ) ) from STIRL2_1:sch_5(A13);
now__::_thesis:_for_i_being_Nat_st_i_in_dom_d9_holds_
2_divides_d9_._i
let i be Nat; ::_thesis: ( i in dom d9 implies 2 divides d9 . i )
assume A15: i in dom d9 ; ::_thesis: 2 divides d9 . i
then i < k by A14, NAT_1:44;
then i + 1 < k + 1 by XREAL_1:8;
then A16: i + 1 in dom d by A5, NAT_1:44;
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; ::_thesis: verum
end;
then 2 divides Sum d9 by Th2;
then A17: (Sum d9) mod 2 = 0 by PEPIN:6;
A18: now__::_thesis:_for_l_being_Nat_st_l_in_dom_d9_holds_
d_._((len_<%(d_._0)%>)_+_l)_=_d9_._l
let l be Nat; ::_thesis: ( l in dom d9 implies d . ((len <%(d . 0)%>) + l) = d9 . l )
A19: (len <%(d . 0)%>) + l = l + 1 by AFINSQ_1:34;
assume l in dom d9 ; ::_thesis: d . ((len <%(d . 0)%>) + l) = d9 . l
hence d . ((len <%(d . 0)%>) + l) = d9 . l by A14, A19; ::_thesis: verum
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, NAT_1:44;
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 2 divides (digits (n,10)) . 0 ; ::_thesis: verum
end;
end;
end;
assume A21: 2 divides (digits (n,10)) . 0 ; ::_thesis: 2 divides n
now__::_thesis:_for_i_being_Nat_st_i_in_dom_d_holds_
2_divides_d_._i
let i be Nat; ::_thesis: ( i in dom d implies 2 divides d . b1 )
assume A22: i in dom d ; ::_thesis: 2 divides d . b1
percases ( i = 0 or i > 0 ) ;
suppose i = 0 ; ::_thesis: 2 divides d . b1
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; ::_thesis: verum
end;
suppose i > 0 ; ::_thesis: 2 divides d . b1
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; ::_thesis: verum
end;
end;
end;
then 2 divides value ((digits (n,10)),10) by A2, Th2;
hence 2 divides n by Th5; ::_thesis: verum
end;
theorem :: NUMERAL1:9
for n being Nat holds
( 3 divides n iff 3 divides Sum (digits (n,10)) )
proof
let n be Nat; ::_thesis: ( 3 divides n iff 3 divides Sum (digits (n,10)) )
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 S1[ set , set ] means $2 = (p . $1) mod 3;
A4: for k being Nat st k in dop holds
ex x being Element of NAT st S1[k,x] ;
consider p9 being XFinSequence of NAT such that
A5: ( dom p9 = dop & ( for k being Nat st k in dop holds
S1[k,p9 . k] ) ) from STIRL2_1:sch_5(A4);
A6: now__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_
p9_._i_=_((digits_(n,10))_._i)_mod_3
let i be Nat; ::_thesis: ( i in dom p implies p9 . i = ((digits (n,10)) . i) mod 3 )
reconsider dz = (10 |^ i) - 1 as Nat by NAT_1:20, NEWTON:83;
reconsider dz = 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 ; ::_thesis: p9 . i = ((digits (n,10)) . i) mod 3
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 + ((digits (n,10)) . i)) mod 3 by A7, NAT_D:22
.= ((digits (n,10)) . i) mod 3 ;
::_thesis: verum
end;
thus ( 3 divides n implies 3 divides Sum (digits (n,10)) ) ::_thesis: ( 3 divides Sum (digits (n,10)) implies 3 divides n )
proof
assume 3 divides n ; ::_thesis: 3 divides Sum (digits (n,10))
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 3 divides Sum (digits (n,10)) by PEPIN:6; ::_thesis: verum
end;
assume 3 divides Sum (digits (n,10)) ; ::_thesis: 3 divides n
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 3 divides n by A3, Th5; ::_thesis: verum
end;
theorem :: NUMERAL1:10
for n being Nat holds
( 5 divides n iff 5 divides (digits (n,10)) . 0 )
proof
let n be Nat; ::_thesis: ( 5 divides n iff 5 divides (digits (n,10)) . 0 )
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 ) ::_thesis: ( 5 divides (digits (n,10)) . 0 implies 5 divides n )
proof
A3: len (digits (n,10)) >= 1 by Th4;
assume A4: 5 divides n ; ::_thesis: 5 divides (digits (n,10)) . 0
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;
percases ( len (digits (n,10)) = 1 or len (digits (n,10)) > 1 ) by A3, XXREAL_0:1;
supposeA8: len (digits (n,10)) = 1 ; ::_thesis: 5 divides (digits (n,10)) . 0
then A9: 0 in dom (digits (n,10)) by NAT_1:44;
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 5 divides (digits (n,10)) . 0 ; ::_thesis: verum
end;
supposeA11: len (digits (n,10)) > 1 ; ::_thesis: 5 divides (digits (n,10)) . 0
then reconsider k = (len (digits (n,10))) - 1 as Element of NAT by NAT_1:21;
defpred S1[ Nat, set ] means $2 = d . ($1 + 1);
A12: now__::_thesis:_for_l_being_Nat_st_l_in_dom_<%(d_._0)%>_holds_
d_._l_=_<%(d_._0)%>_._l
let l be Nat; ::_thesis: ( l in dom <%(d . 0)%> implies d . l = <%(d . 0)%> . l )
assume l in dom <%(d . 0)%> ; ::_thesis: d . l = <%(d . 0)%> . l
then l in 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 by AFINSQ_1:34; ::_thesis: verum
end;
A13: for u being Nat st u in k holds
ex x being Element of NAT st S1[u,x] ;
consider d9 being XFinSequence of NAT such that
A14: ( dom d9 = k & ( for x being Nat st x in k holds
S1[x,d9 . x] ) ) from STIRL2_1:sch_5(A13);
now__::_thesis:_for_i_being_Nat_st_i_in_dom_d9_holds_
5_divides_d9_._i
let i be Nat; ::_thesis: ( i in dom d9 implies 5 divides d9 . i )
assume A15: i in dom d9 ; ::_thesis: 5 divides d9 . i
then i < k by A14, NAT_1:44;
then i + 1 < k + 1 by XREAL_1:8;
then A16: i + 1 in dom d by A5, NAT_1:44;
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; ::_thesis: verum
end;
then 5 divides Sum d9 by Th2;
then A17: (Sum d9) mod 5 = 0 by PEPIN:6;
A18: now__::_thesis:_for_l_being_Nat_st_l_in_dom_d9_holds_
d_._((len_<%(d_._0)%>)_+_l)_=_d9_._l
let l be Nat; ::_thesis: ( l in dom d9 implies d . ((len <%(d . 0)%>) + l) = d9 . l )
A19: (len <%(d . 0)%>) + l = l + 1 by AFINSQ_1:34;
assume l in dom d9 ; ::_thesis: d . ((len <%(d . 0)%>) + l) = d9 . l
hence d . ((len <%(d . 0)%>) + l) = d9 . l by A14, A19; ::_thesis: verum
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, NAT_1:44;
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 5 divides (digits (n,10)) . 0 ; ::_thesis: verum
end;
end;
end;
assume A21: 5 divides (digits (n,10)) . 0 ; ::_thesis: 5 divides n
now__::_thesis:_for_i_being_Nat_st_i_in_dom_d_holds_
5_divides_d_._i
let i be Nat; ::_thesis: ( i in dom d implies 5 divides d . b1 )
assume A22: i in dom d ; ::_thesis: 5 divides d . b1
percases ( i = 0 or i > 0 ) ;
suppose i = 0 ; ::_thesis: 5 divides d . b1
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; ::_thesis: verum
end;
suppose i > 0 ; ::_thesis: 5 divides d . b1
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; ::_thesis: verum
end;
end;
end;
then 5 divides value ((digits (n,10)),10) by A2, Th2;
hence 5 divides n by Th5; ::_thesis: verum
end;