reconsider b1 = b - 1 as Element of NAT by A1, NAT_1:20;
let d, e be XFinSequence of NAT ; ( ( 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 )
( not n <> 0 & d = <%0%> & e = <%0%> 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
;
( 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 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 )
;
( 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 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, NAT_1: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
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 )
;
d = e
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, NAT_1: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
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 for a being object st a in dom d holds
d . a = e . alet a be
object ;
( a in dom d implies d . b1 = e . b1 )assume A77:
a in dom d
;
d . b1 = e . b1then 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
( ( o = 0 & o = k ) or ( o = 0 & o < k ) or ( o > 0 & o = k ) or ( o > 0 & o < k ) )
by A78, XXREAL_0:1;
suppose A80:
(
o = 0 &
o = k )
;
d . b1 = e . b1then
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
;
verum end; suppose A82:
(
o = 0 &
o < k )
;
d . b1 = e . b1reconsider co =
<%> NAT as
XFinSequence of
NAT ;
Sum co = 0
;
then A83:
(Sum co) div (b |^ o) = 0
by NAT_2:2;
set d9 =
D;
D = co ^ D
;
then A84:
n = (Sum co) + (Sum D)
by A43, AFINSQ_2:55;
reconsider bo =
b |^ o as
Element of
NAT by ORDINAL1:def 12;
A85:
bo <> 0
by A1, PREPOWER:5;
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 S1[
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 holds
ex
x being
Element of
NAT st
S1[
u,
x]
;
consider d91 being
XFinSequence of
NAT such that A89:
(
dom d91 = Segm oo1 & ( for
x being
Nat st
x in Segm oo1 holds
S1[
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;
then A94:
b |^ o1 divides Sum d91
by Th2;
dom D =
1
+ (dom d91)
by A41, A82, A89
.=
(len <%(D . o)%>) + (len d91)
by AFINSQ_1:34
;
then
D = <%(D . o)%> ^ d91
by A86, A95, AFINSQ_1:def 3;
then A97:
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 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
;
then A100:
b |^ o divides Sum D
by Th2;
then
(Sum D) mod (b |^ o) = 0
by A85, PEPIN:6;
then
n div (b |^ o) = ((Sum D) div (b |^ o)) + ((Sum co) div (b |^ o))
by A84, NAT_D:19;
then A101:
(n div (b |^ o)) * (b |^ o) = Sum D
by A83, A100, NAT_D:3;
reconsider co =
<%> NAT as
XFinSequence of
NAT ;
Sum co = 0
;
then A102:
(Sum co) div (b |^ o) = 0
by NAT_2:2;
set d9 =
E;
E = co ^ E
;
then A103:
n = (Sum co) + (Sum E)
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 =
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;
( i in dom do1 implies do1 . i <= g1 . i )
reconsider I =
i as
Element of
NAT by ORDINAL1:def 12;
assume A110:
i in dom do1
;
do1 . i <= g1 . i
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
do1 . i <= g1 . i
by A111, A113, XREAL_1:64;
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 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;
then A117:
b |^ o divides Sum E
by Th2;
then
(Sum E) mod (b |^ o) = 0
by A104, PEPIN:6;
then
n div (b |^ o) = ((Sum E) div (b |^ o)) + ((Sum co) div (b |^ o))
by A103, NAT_D:19;
then A118:
(n div (b |^ o)) * (b |^ o) = Sum E
by A102, A117, NAT_D:3;
reconsider oo1 =
(len d) - o1 as
Element of
NAT by A82;
defpred S2[
Nat,
set ]
means $2
= E . ($1 + o1);
A120:
for
u being
Nat st
u in Segm oo1 holds
ex
x being
Element of
NAT st
S2[
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
S2[
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;
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;
then A129:
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;
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;
( i in dom do1 implies do1 . i <= g1 . i )
reconsider I =
i as
Element of
NAT by ORDINAL1:def 12;
assume A135:
i in dom do1
;
do1 . i <= g1 . i
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
do1 . i <= g1 . i
by A136, A138, XREAL_1:64;
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 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 E =
1
+ (dom d91)
by A60, A76, A82, A121
.=
(len <%(E . o)%>) + (len d91)
by AFINSQ_1:34
;
then
E = <%(E . o)%> ^ d91
by A119, A124, 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 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;
verum end; suppose A142:
(
o > 0 &
o = k )
;
d . b1 = e . b1set 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 <%(D . o)%> = oo
by A142, AFINSQ_1:34;
then A146:
dom D = (len co) + (len <%(D . o)%>)
by A41, A144;
A147:
for
x being
Nat st
x in dom <%(D . o)%> holds
D . ((len co) + x) = <%(D . o)%> . x
then A149:
b |^ o divides Sum <%(D . o)%>
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 =
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;
( i in dom co implies co . i <= g . i )
reconsider I =
i as
Element of
NAT by ORDINAL1:def 12;
assume A157:
i in dom co
;
co . i <= g . i
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
co . i <= g . i
by A158, A160, XREAL_1:64;
verum
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 ^ <%(D . o)%>
by A146, A147, AFINSQ_1:def 3;
then A162:
n = (Sum co) + (Sum <%(D . o)%>)
by A43, AFINSQ_2:55;
A163:
bo <> 0
by A1, PREPOWER:5;
then
(Sum <%(D . o)%>) mod (b |^ o) = 0
by A149, PEPIN:6;
then
n div (b |^ o) = ((Sum <%(D . o)%>) div (b |^ o)) + ((Sum co) div (b |^ o))
by A162, NAT_D:19;
then
(n div (b |^ o)) * (b |^ o) = Sum <%(D . o)%>
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 <%(E . o)%> = oo
by A142, AFINSQ_1:34;
then A168:
dom E = (len co) + (len <%(E . o)%>)
by A60, A76, A166;
A169:
for
x being
Nat st
x in dom <%(E . o)%> holds
E . ((len co) + x) = <%(E . o)%> . x
then A171:
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;
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;
( i in dom co implies co . i <= g . i )
reconsider I =
i as
Element of
NAT by ORDINAL1:def 12;
assume A177:
i in dom co
;
co . i <= g . i
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
co . i <= g . i
by A178, A180, XREAL_1:64;
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 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 ^ <%(E . o)%>
by A168, A169, AFINSQ_1:def 3;
then A182:
n = (Sum co) + (Sum <%(E . o)%>)
by A62, AFINSQ_2:55;
A183:
bo <> 0
by A1, PREPOWER:5;
then
(Sum <%(E . o)%>) mod (b |^ o) = 0
by A171, PEPIN:6;
then
n div (b |^ o) = ((Sum <%(E . o)%>) div (b |^ o)) + ((Sum co) div (b |^ o))
by A182, NAT_D:19;
then
(n div (b |^ o)) * (b |^ o) = Sum <%(E . o)%>
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;
verum end; suppose A184:
(
o > 0 &
o < k )
;
d . b1 = e . b1reconsider 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 S1[
Nat,
set ]
means $2
= D . ($1 + o);
consider ok1 being
Nat such that A187:
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;
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;
( i in dom do1 implies do1 . i <= g1 . i )
reconsider I =
i as
Element of
NAT by ORDINAL1:def 12;
assume A194:
i in dom do1
;
do1 . i <= g1 . i
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
do1 . i <= g1 . i
by A195, A197, XREAL_1:64;
verum
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 being
Nat st
u in Segm oo holds
ex
x being
Element of
NAT st
S1[
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
S1[
x,
d9 . x] ) )
from STIRL2_1:sch 5(A198);
defpred S2[
Nat,
set ]
means $2
= D . ($1 + o1);
A202:
for
u being
Nat st
u in Segm oo1 holds
ex
x being
Element of
NAT st
S2[
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
S2[
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;
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 =
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;
( i in dom co implies co . i <= g . i )
reconsider I =
i as
Element of
NAT by ORDINAL1:def 12;
assume A216:
i in dom co
;
co . i <= g . i
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
co . i <= g . i
by A217, A219, XREAL_1:64;
verum
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 S3[
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;
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 =
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 =
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;
( i in dom do1 implies do1 . i <= g1 . i )
reconsider I =
i as
Element of
NAT by ORDINAL1:def 12;
assume A246:
i in dom do1
;
do1 . i <= g1 . i
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
do1 . i <= g1 . i
by A247, A249, XREAL_1:64;
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 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 holds
ex
x being
Element of
NAT st
S3[
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
S3[
x,
d9 . x] ) )
from STIRL2_1:sch 5(A251);
defpred S4[
Nat,
set ]
means $2
= E . ($1 + o1);
A255:
for
u being
Nat st
u in Segm oo1 holds
ex
x being
Element of
NAT st
S4[
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
S4[
x,
d91 . x] ) )
from STIRL2_1:sch 5(A255);
A257:
dom E = (len do1) + (len d91)
by A60, A76, A256, A241;
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;
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;
( i in dom co implies co . i <= g . i )
reconsider I =
i as
Element of
NAT by ORDINAL1:def 12;
assume A271:
i in dom co
;
co . i <= g . i
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
co . i <= g . i
by A272, A274, XREAL_1:64;
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 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;
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;
verum end; end; end;
hence
d = e
by A76, FUNCT_1:2;
verum
end;
assume that
n = 0
and
A282:
( d = <%0%> & e = <%0%> )
; d = e
thus
d = e
by A282; verum