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 )

n = 0 and

A282: ( d = <%0%> & e = <%0%> ) ; :: thesis: d = e

thus d = e by A282; :: thesis: verum

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

assume that
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 ; :: 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

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 ) ; :: 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

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

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 ) ; :: thesis: 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

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;

end;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 ; :: 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

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 ) ; :: 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

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

proof

assume that
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 A54: i in dom D ; :: thesis: D . i <= g . i

then A55: D . i = (d . i) * (b |^ i) by A42;

d . i < b1 + 1 by A40, A41, A54;

then A56: d . i <= b1 by NAT_1:13;

g . I = ((b - 1) (#) (b GeoSeq)) . I by A41, A52, A54, FUNCT_1:47

.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9

.= b1 * (b |^ I) by PREPOWER:def 1 ;

hence D . i <= g . i by A56, A55, XREAL_1:64; :: thesis: verum

end;reconsider I = i as Element of NAT by ORDINAL1:def 12;

assume A54: i in dom D ; :: thesis: D . i <= g . i

then A55: D . i = (d . i) * (b |^ i) by A42;

d . i < b1 + 1 by A40, A41, A54;

then A56: d . i <= b1 by NAT_1:13;

g . I = ((b - 1) (#) (b GeoSeq)) . I by A41, A52, A54, FUNCT_1:47

.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9

.= b1 * (b |^ I) by PREPOWER:def 1 ;

hence D . i <= g . i by A56, A55, XREAL_1:64; :: thesis: verum

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 ) ; :: thesis: 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

proof

A73:
b |^ l > 0
by A1, PREPOWER:6;
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 A70: i in dom E ; :: thesis: E . i <= g . i

then A71: E . i = (e . i) * (b |^ i) by A61;

e . i < b1 + 1 by A59, A60, A70;

then A72: e . i <= b1 by NAT_1:13;

g . I = ((b - 1) (#) (b GeoSeq)) . I by A60, A68, A70, FUNCT_1:47

.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9

.= b1 * (b |^ I) by PREPOWER:def 1 ;

hence E . i <= g . i by A72, A71, XREAL_1:64; :: thesis: verum

end;reconsider I = i as Element of NAT by ORDINAL1:def 12;

assume A70: i in dom E ; :: thesis: E . i <= g . i

then A71: E . i = (e . i) * (b |^ i) by A61;

e . i < b1 + 1 by A59, A60, A70;

then A72: e . i <= b1 by NAT_1:13;

g . I = ((b - 1) (#) (b GeoSeq)) . I by A60, A68, A70, FUNCT_1:47

.= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9

.= b1 * (b |^ I) by PREPOWER:def 1 ;

hence E . i <= g . i by A72, A71, XREAL_1:64; :: thesis: verum

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 :: thesis: for a being object st a in dom d holds

d . a = e . a

hence
d = e
by A76, FUNCT_1:2; :: thesis: verumd . a = e . a

let a be object ; :: thesis: ( a in dom d implies d . b_{1} = e . b_{1} )

assume A77: a in dom d ; :: thesis: d . b_{1} = e . b_{1}

then reconsider o = a as Element of NAT ;

o < k + 1 by A77, AFINSQ_1:86;

then A78: o <= k by NAT_1:13;

A79: o < len d by A77, AFINSQ_1:86;

then reconsider oo = (len d) - o as Element of NAT by NAT_1:21;

end;assume A77: a in dom d ; :: thesis: d . b

then reconsider o = a as Element of NAT ;

o < k + 1 by A77, AFINSQ_1:86;

then A78: o <= k by NAT_1:13;

A79: o < len d by A77, AFINSQ_1:86;

then reconsider oo = (len d) - o as Element of NAT by NAT_1:21;

per cases
( ( o = 0 & o = k ) or ( o = 0 & o < k ) or ( o > 0 & o = k ) or ( o > 0 & o < k ) )
by A78, XXREAL_0:1;

end;

suppose A80:
( o = 0 & o = k )
; :: thesis: d . b_{1} = e . b_{1}

then
len E = 1
by A60, A76;

then A81: E = <%(E . 0)%> by AFINSQ_1:34

.= <%((e . 0) * (b |^ 0))%> by A60, A61, A76, A77, A80

.= <%((e . 0) * 1)%> by NEWTON:4 ;

len D = 1 by A41, A80;

then D = <%(D . 0)%> by AFINSQ_1:34

.= <%((d . 0) * (b |^ 0))%> by A41, A42, A77, A80

.= <%((d . 0) * 1)%> by NEWTON:4 ;

hence d . a = n by A43, A80, AFINSQ_2:53

.= e . a by A62, A80, A81, AFINSQ_2:53 ;

:: thesis: verum

end;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 ;

:: thesis: verum

suppose A82:
( o = 0 & o < k )
; :: thesis: d . b_{1} = e . b_{1}

reconsider 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;

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 S_{1}[ 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 S_{1}[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

S_{1}[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;

.= (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 (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

.= ((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 (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;

defpred S_{2}[ 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 S_{2}[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

S_{2}[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;

consider ok1 being Nat such that

A126: ok1 + 1 = o1 ;

A127: dom E = (len do1) + (len d91) by A60, A76, A121, A123;

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

.= ((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; :: thesis: verum

end;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;

A86: now :: thesis: for k being Nat st k in dom <%(D . o)%> holds

D . k = <%(D . o)%> . k

reconsider o1 = o + 1 as Element of NAT ;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 Segm 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 A82; :: thesis: verum

end;assume k in dom <%(D . o)%> ; :: thesis: D . k = <%(D . o)%> . k

then k in Segm 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 A82; :: thesis: verum

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 S

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 S

consider d91 being XFinSequence of NAT such that

A89: ( dom d91 = Segm oo1 & ( for x being Nat st x in Segm oo1 holds

S

A90: len d = len D by A41;

then A91: len do1 = o1 by A87, AFINSQ_1:11;

then A92: dom D = (len do1) + (len d91) by A41, A89;

now :: thesis: for k being Nat st k in dom d91 holds

b |^ o1 divides d91 . k

then A94:
b |^ o1 divides Sum d91
by Th2;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 A93: k in dom d91 ; :: thesis: b |^ o1 divides d91 . k

then k < len d91 by AFINSQ_1:86;

then o1 + k < len D by A91, A92, XREAL_1:8;

then o1 + k in dom D by AFINSQ_1:86;

then D . (o1 + k) = (d . (o1 + k)) * (b |^ (o1 + k)) by A42;

then d91 . K = (d . (o1 + k)) * (b |^ (o1 + k)) by A89, A93

.= (d . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:8

.= ((d . (o1 + k)) * (b |^ k)) * (b |^ o1) ;

hence b |^ o1 divides d91 . k by NAT_D:def 3; :: thesis: verum

end;reconsider K = k as Element of NAT by ORDINAL1:def 12;

assume A93: k in dom d91 ; :: thesis: b |^ o1 divides d91 . k

then k < len d91 by AFINSQ_1:86;

then o1 + k < len D by A91, A92, XREAL_1:8;

then o1 + k in dom D by AFINSQ_1:86;

then D . (o1 + k) = (d . (o1 + k)) * (b |^ (o1 + k)) by A42;

then d91 . K = (d . (o1 + k)) * (b |^ (o1 + k)) by A89, A93

.= (d . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:8

.= ((d . (o1 + k)) * (b |^ k)) * (b |^ o1) ;

hence b |^ o1 divides d91 . k by NAT_D:def 3; :: thesis: verum

A95: now :: thesis: for k being Nat st k in dom d91 holds

D . ((len <%(D . o)%>) + k) = d91 . k

dom D =
1 + (dom d91)
by A41, A82, A89
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 A96: k in dom d91 ; :: thesis: D . ((len <%(D . o)%>) + k) = d91 . k

thus D . ((len <%(D . o)%>) + k) = D . ((len do1) + k) by A82, A91, AFINSQ_1:33

.= d91 . k by A89, A91, A96 ; :: thesis: verum

end;assume A96: k in dom d91 ; :: thesis: D . ((len <%(D . o)%>) + k) = d91 . k

thus D . ((len <%(D . o)%>) + k) = D . ((len do1) + k) by A82, A91, AFINSQ_1:33

.= d91 . k by A89, A91, A96 ; :: thesis: verum

.= (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 ;

now :: thesis: for k being Nat st k in dom D holds

b |^ o divides D . k

then A100:
b |^ o divides Sum D
by Th2;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 A42, A82

.= (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;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 A42, A82

.= (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

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

Sum g1 =
(Partial_Sums ((b - 1) (#) (b GeoSeq))) . ok1
by AFINSQ_2:56
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 A110: i in dom do1 ; :: thesis: 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; :: thesis: verum

end;reconsider I = i as Element of NAT by ORDINAL1:def 12;

assume A110: i in dom do1 ; :: thesis: 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; :: thesis: verum

.= ((b - 1) (#) (Partial_Sums (b GeoSeq))) . ok1 by SERIES_1:9

.= (b - 1) * ((Partial_Sums (b GeoSeq)) . ok1) by SEQ_1:9

.= (b - 1) * ((1 - (b to_power (ok1 + 1))) / (1 - b)) by A1, SERIES_1:22

.= - ((1 - b) * ((1 - (b |^ o1)) / (1 - b))) by A99

.= - (1 - (b |^ o1)) by A105, XCMPLX_1:87

.= (b |^ o1) - 1 ;

then Sum do1 < ((b |^ o1) - 1) + 1 by A107, A109, AFINSQ_2:57, XREAL_1:145;

then A114: (Sum do1) div (b |^ o1) = 0 by NAT_D:27;

bo1 <> 0 by A1, PREPOWER:5;

then (Sum d91) mod (b |^ o1) = 0 by A94, PEPIN:6;

then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by A98, NAT_D:19;

then (n div (b |^ o1)) * (b |^ o1) = Sum d91 by A114, A94, NAT_D:3;

then D . o = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A101, A97, AFINSQ_2:53;

then (d . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A41, A42, A77;

then (d . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * ((b |^ o) * (b |^ 1))) by NEWTON:8;

then (d . o) * (b |^ o) = (b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * (b |^ 1))) ;

then ((b |^ o) * (d . o)) / (b |^ o) = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o) ;

then A115: d . o = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o) by A85, XCMPLX_1:89;

reconsider o1 = o + 1 as Element of NAT ;

reconsider do1 = E | o1 as XFinSequence of NAT ;

A116: len e = len E by A60;

now :: thesis: for k being Nat st k in dom E holds

b |^ o divides E . k

then A117:
b |^ o divides Sum E
by Th2;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 A61, A82

.= (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;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 A61, A82

.= (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

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;

A119: now :: thesis: for k being Nat st k in dom <%(E . o)%> holds

E . k = <%(E . o)%> . k

reconsider oo1 = (len d) - o1 as Element of NAT by A82;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 Segm 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 A82; :: thesis: verum

end;assume k in dom <%(E . o)%> ; :: thesis: E . k = <%(E . o)%> . k

then k in Segm 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 A82; :: thesis: verum

defpred S

A120: for u being Nat st u in Segm oo1 holds

ex x being Element of NAT st S

consider d91 being XFinSequence of NAT such that

A121: ( dom d91 = Segm oo1 & ( for x being Nat st x in Segm oo1 holds

S

o1 <= k by A82, NAT_1:13;

then A122: o1 < len d by XREAL_1:147;

then A123: len do1 = o1 by A76, A116, AFINSQ_1:11;

A124: now :: thesis: for k being Nat st k in dom d91 holds

E . ((len <%(E . o)%>) + k) = d91 . k

reconsider bo1 = b |^ o1 as Element of NAT by ORDINAL1:def 12;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 A125: k in dom d91 ; :: thesis: E . ((len <%(E . o)%>) + k) = d91 . k

thus E . ((len <%(E . o)%>) + k) = E . ((len do1) + k) by A82, A123, AFINSQ_1:33

.= d91 . k by A121, A123, A125 ; :: thesis: verum

end;assume A125: k in dom d91 ; :: thesis: E . ((len <%(E . o)%>) + k) = d91 . k

thus E . ((len <%(E . o)%>) + k) = E . ((len do1) + k) by A82, A123, AFINSQ_1:33

.= d91 . k by A121, A123, A125 ; :: thesis: verum

consider ok1 being Nat such that

A126: ok1 + 1 = o1 ;

A127: dom E = (len do1) + (len d91) by A60, A76, A121, A123;

now :: thesis: for k being Nat st k in dom d91 holds

b |^ o1 divides d91 . k

then A129:
b |^ o1 divides Sum d91
by Th2;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 A128: k in dom d91 ; :: thesis: b |^ o1 divides d91 . k

then k < len d91 by AFINSQ_1:86;

then o1 + k < len E by A123, A127, XREAL_1:8;

then o1 + k in dom E by AFINSQ_1:86;

then E . (o1 + k) = (e . (o1 + k)) * (b |^ (o1 + k)) by A61;

then d91 . K = (e . (o1 + k)) * (b |^ (o1 + k)) by A121, A128

.= (e . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:8

.= ((e . (o1 + k)) * (b |^ k)) * (b |^ o1) ;

hence b |^ o1 divides d91 . k by NAT_D:def 3; :: thesis: verum

end;reconsider K = k as Element of NAT by ORDINAL1:def 12;

assume A128: k in dom d91 ; :: thesis: b |^ o1 divides d91 . k

then k < len d91 by AFINSQ_1:86;

then o1 + k < len E by A123, A127, XREAL_1:8;

then o1 + k in dom E by AFINSQ_1:86;

then E . (o1 + k) = (e . (o1 + k)) * (b |^ (o1 + k)) by A61;

then d91 . K = (e . (o1 + k)) * (b |^ (o1 + k)) by A121, A128

.= (e . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:8

.= ((e . (o1 + k)) * (b |^ k)) * (b |^ o1) ;

hence b |^ o1 divides d91 . k by NAT_D:def 3; :: thesis: verum

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

Sum g1 =
(Partial_Sums ((b - 1) (#) (b GeoSeq))) . ok1
by AFINSQ_2:56
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 A135: i in dom do1 ; :: thesis: 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; :: thesis: verum

end;reconsider I = i as Element of NAT by ORDINAL1:def 12;

assume A135: i in dom do1 ; :: thesis: 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; :: thesis: verum

.= ((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; :: thesis: verum

suppose A142:
( o > 0 & o = k )
; :: thesis: d . b_{1} = e . b_{1}

set d9 = <%(D . o)%>;

reconsider co = D | o as XFinSequence of NAT ;

A143: len d = len D by A41;

then A144: len co = o by A79, AFINSQ_1:11;

A145: len <%(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

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

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

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

.= ((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; :: thesis: verum

end;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

proof

let x be Nat; :: thesis: ( x in dom <%(D . o)%> implies D . ((len co) + x) = <%(D . o)%> . x )

assume x in dom <%(D . o)%> ; :: thesis: D . ((len co) + x) = <%(D . o)%> . x

then x < 1 by A142, A145, AFINSQ_1:86;

then x = 0 by NAT_1:14;

hence D . ((len co) + x) = <%(D . o)%> . x by A144; :: thesis: verum

end;assume x in dom <%(D . o)%> ; :: thesis: D . ((len co) + x) = <%(D . o)%> . x

then x < 1 by A142, A145, AFINSQ_1:86;

then x = 0 by NAT_1:14;

hence D . ((len co) + x) = <%(D . o)%> . x by A144; :: thesis: verum

now :: thesis: for k being Nat st k in dom <%(D . o)%> holds

b |^ o divides <%(D . o)%> . k

then A149:
b |^ o divides Sum <%(D . o)%>
by Th2;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 A148: k in dom <%(D . o)%> ; :: thesis: b |^ o divides <%(D . o)%> . k

then k < len <%(D . o)%> by AFINSQ_1:86;

then o + k < len D by A144, A146, XREAL_1:8;

then o + k in dom D by AFINSQ_1:86;

then D . (o + k) = (d . (o + k)) * (b |^ (o + k)) by A42;

then <%(D . o)%> . K = (d . (o + k)) * (b |^ (o + k)) by A144, A147, A148

.= (d . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8

.= ((d . (o + k)) * (b |^ k)) * (b |^ o) ;

hence b |^ o divides <%(D . o)%> . k by NAT_D:def 3; :: thesis: verum

end;reconsider K = k as Element of NAT by ORDINAL1:def 12;

assume A148: k in dom <%(D . o)%> ; :: thesis: b |^ o divides <%(D . o)%> . k

then k < len <%(D . o)%> by AFINSQ_1:86;

then o + k < len D by A144, A146, XREAL_1:8;

then o + k in dom D by AFINSQ_1:86;

then D . (o + k) = (d . (o + k)) * (b |^ (o + k)) by A42;

then <%(D . o)%> . K = (d . (o + k)) * (b |^ (o + k)) by A144, A147, A148

.= (d . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8

.= ((d . (o + k)) * (b |^ k)) * (b |^ o) ;

hence b |^ o divides <%(D . o)%> . k by NAT_D:def 3; :: thesis: verum

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

len co = len g
by A144, A151, A154, RELAT_1:62;
let i be Nat; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;reconsider I = i as Element of NAT by ORDINAL1:def 12;

assume A157: i in dom co ; :: thesis: 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; :: thesis: verum

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

proof

let x be Nat; :: thesis: ( x in dom <%(E . o)%> implies E . ((len co) + x) = <%(E . o)%> . x )

assume x in dom <%(E . o)%> ; :: thesis: E . ((len co) + x) = <%(E . o)%> . x

then x < 1 by A142, A167, AFINSQ_1:86;

then x = 0 by NAT_1:14;

hence E . ((len co) + x) = <%(E . o)%> . x by A166; :: thesis: verum

end;assume x in dom <%(E . o)%> ; :: thesis: E . ((len co) + x) = <%(E . o)%> . x

then x < 1 by A142, A167, AFINSQ_1:86;

then x = 0 by NAT_1:14;

hence E . ((len co) + x) = <%(E . o)%> . x by A166; :: thesis: verum

now :: thesis: for k being Nat st k in dom <%(E . o)%> holds

b |^ o divides <%(E . o)%> . k

then A171:
b |^ o divides Sum <%(E . o)%>
by Th2;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 A170: k in dom <%(E . o)%> ; :: thesis: b |^ o divides <%(E . o)%> . k

then k < len <%(E . o)%> by AFINSQ_1:86;

then o + k < len E by A166, A168, XREAL_1:8;

then o + k in dom E by AFINSQ_1:86;

then E . (o + k) = (e . (o + k)) * (b |^ (o + k)) by A61;

then <%(E . o)%> . K = (e . (o + k)) * (b |^ (o + k)) by A166, A169, A170

.= (e . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8

.= ((e . (o + k)) * (b |^ k)) * (b |^ o) ;

hence b |^ o divides <%(E . o)%> . k by NAT_D:def 3; :: thesis: verum

end;reconsider K = k as Element of NAT by ORDINAL1:def 12;

assume A170: k in dom <%(E . o)%> ; :: thesis: b |^ o divides <%(E . o)%> . k

then k < len <%(E . o)%> by AFINSQ_1:86;

then o + k < len E by A166, A168, XREAL_1:8;

then o + k in dom E by AFINSQ_1:86;

then E . (o + k) = (e . (o + k)) * (b |^ (o + k)) by A61;

then <%(E . o)%> . K = (e . (o + k)) * (b |^ (o + k)) by A166, A169, A170

.= (e . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8

.= ((e . (o + k)) * (b |^ k)) * (b |^ o) ;

hence b |^ o divides <%(E . o)%> . k by NAT_D:def 3; :: thesis: verum

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

Sum g =
(Partial_Sums ((b - 1) (#) (b GeoSeq))) . ok
by AFINSQ_2:56
let i be Nat; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;reconsider I = i as Element of NAT by ORDINAL1:def 12;

assume A177: i in dom co ; :: thesis: 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; :: thesis: verum

.= ((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; :: thesis: verum

suppose A184:
( o > 0 & o < k )
; :: thesis: d . b_{1} = e . b_{1}

reconsider o1 = o + 1 as Element of NAT ;

A185: o1 <= k by A184, NAT_1:13;

then A186: o1 < len d by XREAL_1:147;

reconsider bo1 = b |^ o1 as Element of NAT by ORDINAL1:def 12;

reconsider do1 = D | o1 as XFinSequence of NAT ;

reconsider bo = b |^ o as Element of NAT by ORDINAL1:def 12;

defpred S_{1}[ 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

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 S_{1}[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

S_{1}[x,d9 . x] ) )
from STIRL2_1:sch 5(A198);

_{2}[ 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 S_{2}[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

S_{2}[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;

( ( 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

.= (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 S_{3}[ 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;

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

.= ((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 S_{3}[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

S_{3}[x,d9 . x] ) )
from STIRL2_1:sch 5(A251);

_{4}[ 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 S_{4}[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

S_{4}[x,d91 . x] ) )
from STIRL2_1:sch 5(A255);

A257: dom E = (len do1) + (len d91) by A60, A76, A256, A241;

( ( 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;

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

.= ((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;

.= (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; :: thesis: verum

end;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 S

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

k < len d
by XREAL_1:147;
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 A194: i in dom do1 ; :: thesis: 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; :: thesis: verum

end;reconsider I = i as Element of NAT by ORDINAL1:def 12;

assume A194: i in dom do1 ; :: thesis: 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; :: thesis: verum

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 S

consider d9 being XFinSequence of NAT such that

A199: ( dom d9 = Segm oo & ( for x being Nat st x in Segm oo holds

S

A200: now :: thesis: for k being Nat st k in dom <%(D . o)%> holds

d9 . k = <%(D . o)%> . k

defpred Sd9 . 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 Segm 1 by AFINSQ_1:33;

then k < 1 by NAT_1:44;

then A201: k = 0 by NAT_1:14;

then len d9 > k by A79, XREAL_1:50, A199;

then k in dom d9 by A199, NAT_1:44;

hence d9 . k = D . (k + o) by A199

.= <%(D . o)%> . k by A201 ;

:: thesis: verum

end;assume k in dom <%(D . o)%> ; :: thesis: d9 . k = <%(D . o)%> . k

then k in Segm 1 by AFINSQ_1:33;

then k < 1 by NAT_1:44;

then A201: k = 0 by NAT_1:14;

then len d9 > k by A79, XREAL_1:50, A199;

then k in dom d9 by A199, NAT_1:44;

hence d9 . k = D . (k + o) by A199

.= <%(D . o)%> . k by A201 ;

:: thesis: verum

A202: for u being Nat st u in Segm oo1 holds

ex x being Element of NAT st S

consider d91 being XFinSequence of NAT such that

A203: ( dom d91 = Segm oo1 & ( for x being Nat st x in Segm oo1 holds

S

reconsider co = D | o as XFinSequence of NAT ;

A204: len d = len D by A41;

then A205: len co = o by A79, AFINSQ_1:11;

then A206: dom D = (len co) + (len d9) by A41, A199;

now :: thesis: for k being Nat st k in dom d9 holds

b |^ o divides d9 . k

then A208:
b |^ o divides Sum d9
by Th2;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 A207: k in dom d9 ; :: thesis: b |^ o divides d9 . k

then k < len d9 by AFINSQ_1:86;

then o + k < len D by A205, A206, XREAL_1:8;

then o + k in dom D by AFINSQ_1:86;

then D . (o + k) = (d . (o + k)) * (b |^ (o + k)) by A42;

then d9 . K = (d . (o + k)) * (b |^ (o + k)) by A199, A207

.= (d . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8

.= ((d . (o + k)) * (b |^ k)) * (b |^ o) ;

hence b |^ o divides d9 . k by NAT_D:def 3; :: thesis: verum

end;reconsider K = k as Element of NAT by ORDINAL1:def 12;

assume A207: k in dom d9 ; :: thesis: b |^ o divides d9 . k

then k < len d9 by AFINSQ_1:86;

then o + k < len D by A205, A206, XREAL_1:8;

then o + k in dom D by AFINSQ_1:86;

then D . (o + k) = (d . (o + k)) * (b |^ (o + k)) by A42;

then d9 . K = (d . (o + k)) * (b |^ (o + k)) by A199, A207

.= (d . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8

.= ((d . (o + k)) * (b |^ k)) * (b |^ o) ;

hence b |^ o divides d9 . k by NAT_D:def 3; :: thesis: verum

( ( 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;reconsider I = i as Element of NAT by ORDINAL1:def 12;

assume A216: i in dom co ; :: thesis: 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; :: thesis: verum

A220: now :: thesis: for k being Nat st k in dom d91 holds

d9 . ((len <%(D . o)%>) + k) = d91 . k

dom d9 =
1 + (dom d91)
by A199, A203
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 A221: k in dom d91 ; :: thesis: d9 . ((len <%(D . o)%>) + k) = d91 . k

then k < len d91 by A203, NAT_1:44;

then k + 1 < oo1 + 1 by XREAL_1:8, A203;

then k + 1 < len d9 by A199;

then A222: k + 1 in dom d9 by A199, NAT_1:44;

thus d9 . ((len <%(D . o)%>) + k) = d9 . (1 + k) by AFINSQ_1:33

.= D . ((len co) + (k + 1)) by A199, A205, A222

.= D . ((len do1) + k) by A205, A189

.= d91 . k by A203, A189, A221 ; :: thesis: verum

end;assume A221: k in dom d91 ; :: thesis: d9 . ((len <%(D . o)%>) + k) = d91 . k

then k < len d91 by A203, NAT_1:44;

then k + 1 < oo1 + 1 by XREAL_1:8, A203;

then k + 1 < len d9 by A199;

then A222: k + 1 in dom d9 by A199, NAT_1:44;

thus d9 . ((len <%(D . o)%>) + k) = d9 . (1 + k) by AFINSQ_1:33

.= D . ((len co) + (k + 1)) by A199, A205, A222

.= D . ((len do1) + k) by A205, A189

.= d91 . k by A203, A189, A221 ; :: thesis: verum

.= (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 S

A224: 1 - b <> 0 by A1;

consider ok being Nat such that

A225: ok + 1 = o by A184, NAT_1:6;

A226: dom D = (len do1) + (len d91) by A41, A203, A189;

now :: thesis: for k being Nat st k in dom d91 holds

b |^ o1 divides d91 . k

then A228:
b |^ o1 divides Sum d91
by Th2;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 A227: k in dom d91 ; :: thesis: b |^ o1 divides d91 . k

then k < len d91 by AFINSQ_1:86;

then o1 + k < len D by A189, A226, XREAL_1:8;

then o1 + k in dom D by AFINSQ_1:86;

then D . (o1 + k) = (d . (o1 + k)) * (b |^ (o1 + k)) by A42;

then d91 . K = (d . (o1 + k)) * (b |^ (o1 + k)) by A203, A227

.= (d . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:8

.= ((d . (o1 + k)) * (b |^ k)) * (b |^ o1) ;

hence b |^ o1 divides d91 . k by NAT_D:def 3; :: thesis: verum

end;reconsider K = k as Element of NAT by ORDINAL1:def 12;

assume A227: k in dom d91 ; :: thesis: b |^ o1 divides d91 . k

then k < len d91 by AFINSQ_1:86;

then o1 + k < len D by A189, A226, XREAL_1:8;

then o1 + k in dom D by AFINSQ_1:86;

then D . (o1 + k) = (d . (o1 + k)) * (b |^ (o1 + k)) by A42;

then d91 . K = (d . (o1 + k)) * (b |^ (o1 + k)) by A203, A227

.= (d . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:8

.= ((d . (o1 + k)) * (b |^ k)) * (b |^ o1) ;

hence b |^ o1 divides d91 . k by NAT_D:def 3; :: thesis: verum

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

Sum g1 =
(Partial_Sums ((b - 1) (#) (b GeoSeq))) . ok1
by AFINSQ_2:56
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 A246: i in dom do1 ; :: thesis: 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; :: thesis: verum

end;reconsider I = i as Element of NAT by ORDINAL1:def 12;

assume A246: i in dom do1 ; :: thesis: 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; :: thesis: verum

.= ((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 S

consider d9 being XFinSequence of NAT such that

A252: ( dom d9 = Segm oo & ( for x being Nat st x in Segm oo holds

S

A253: now :: thesis: for k being Nat st k in dom <%(E . o)%> holds

d9 . k = <%(E . o)%> . k

defpred Sd9 . 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 Segm 1 by AFINSQ_1:33;

then k < 1 by NAT_1:44;

then A254: k = 0 by NAT_1:14;

oo > 0 by A79, XREAL_1:50;

then k < len d9 by A252, A254;

then k in dom d9 by A252, NAT_1:44;

hence d9 . k = E . (k + o) by A252

.= <%(E . o)%> . k by A254 ;

:: thesis: verum

end;assume k in dom <%(E . o)%> ; :: thesis: d9 . k = <%(E . o)%> . k

then k in Segm 1 by AFINSQ_1:33;

then k < 1 by NAT_1:44;

then A254: k = 0 by NAT_1:14;

oo > 0 by A79, XREAL_1:50;

then k < len d9 by A252, A254;

then k in dom d9 by A252, NAT_1:44;

hence d9 . k = E . (k + o) by A252

.= <%(E . o)%> . k by A254 ;

:: thesis: verum

A255: for u being Nat st u in Segm oo1 holds

ex x being Element of NAT st S

consider d91 being XFinSequence of NAT such that

A256: ( dom d91 = Segm oo1 & ( for x being Nat st x in Segm oo1 holds

S

A257: dom E = (len do1) + (len d91) by A60, A76, A256, A241;

now :: thesis: for k being Nat st k in dom d91 holds

b |^ o1 divides d91 . k

then A259:
b |^ o1 divides Sum d91
by Th2;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 A258: k in dom d91 ; :: thesis: b |^ o1 divides d91 . k

then k < len d91 by AFINSQ_1:86;

then o1 + k < len E by A241, A257, XREAL_1:8;

then o1 + k in dom E by AFINSQ_1:86;

then E . (o1 + k) = (e . (o1 + k)) * (b |^ (o1 + k)) by A61;

then d91 . K = (e . (o1 + k)) * (b |^ (o1 + k)) by A256, A258

.= (e . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:8

.= ((e . (o1 + k)) * (b |^ k)) * (b |^ o1) ;

hence b |^ o1 divides d91 . k by NAT_D:def 3; :: thesis: verum

end;reconsider K = k as Element of NAT by ORDINAL1:def 12;

assume A258: k in dom d91 ; :: thesis: b |^ o1 divides d91 . k

then k < len d91 by AFINSQ_1:86;

then o1 + k < len E by A241, A257, XREAL_1:8;

then o1 + k in dom E by AFINSQ_1:86;

then E . (o1 + k) = (e . (o1 + k)) * (b |^ (o1 + k)) by A61;

then d91 . K = (e . (o1 + k)) * (b |^ (o1 + k)) by A256, A258

.= (e . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:8

.= ((e . (o1 + k)) * (b |^ k)) * (b |^ o1) ;

hence b |^ o1 divides d91 . k by NAT_D:def 3; :: thesis: verum

( ( for x being Nat st x in dom do1 holds

E . x = do1 . x ) & ( for x being Nat st x in dom d91 holds

E . ((len do1) + x) = d91 . x ) ) by A256, A241, FUNCT_1:47;

then E = do1 ^ d91 by A257, AFINSQ_1:def 3;

then A260: n = (Sum do1) + (Sum d91) by A62, AFINSQ_2:55;

bo1 <> 0 by A1, PREPOWER:5;

then (Sum d91) mod (b |^ o1) = 0 by A259, PEPIN:6;

then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by A260, NAT_D:19;

then A261: (n div (b |^ o1)) * (b |^ o1) = Sum d91 by A250, A259, NAT_D:3;

reconsider co = E | o as XFinSequence of NAT ;

A262: len e = len E by A60;

then A263: len co = o by A76, A79, AFINSQ_1:11;

then A264: dom E = (len co) + (len d9) by A60, A76, A252;

now :: thesis: for k being Nat st k in dom d9 holds

b |^ o divides d9 . k

then A266:
b |^ o divides Sum d9
by Th2;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 A265: k in dom d9 ; :: thesis: b |^ o divides d9 . k

then k < len d9 by AFINSQ_1:86;

then o + k < len E by A263, A264, XREAL_1:8;

then o + k in dom E by AFINSQ_1:86;

then E . (o + k) = (e . (o + k)) * (b |^ (o + k)) by A61;

then d9 . K = (e . (o + k)) * (b |^ (o + k)) by A252, A265

.= (e . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8

.= ((e . (o + k)) * (b |^ k)) * (b |^ o) ;

hence b |^ o divides d9 . k by NAT_D:def 3; :: thesis: verum

end;reconsider K = k as Element of NAT by ORDINAL1:def 12;

assume A265: k in dom d9 ; :: thesis: b |^ o divides d9 . k

then k < len d9 by AFINSQ_1:86;

then o + k < len E by A263, A264, XREAL_1:8;

then o + k in dom E by AFINSQ_1:86;

then E . (o + k) = (e . (o + k)) * (b |^ (o + k)) by A61;

then d9 . K = (e . (o + k)) * (b |^ (o + k)) by A252, A265

.= (e . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8

.= ((e . (o + k)) * (b |^ k)) * (b |^ o) ;

hence b |^ o divides d9 . k by NAT_D:def 3; :: thesis: verum

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

Sum g =
(Partial_Sums ((b - 1) (#) (b GeoSeq))) . ok
by AFINSQ_2:56
let i be Nat; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;reconsider I = i as Element of NAT by ORDINAL1:def 12;

assume A271: i in dom co ; :: thesis: 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; :: thesis: verum

.= ((b - 1) (#) (Partial_Sums (b GeoSeq))) . ok by SERIES_1:9

.= (b - 1) * ((Partial_Sums (b GeoSeq)) . ok) by SEQ_1:9

.= (b - 1) * ((1 - (b to_power (ok + 1))) / (1 - b)) by A1, SERIES_1:22

.= - ((1 - b) * ((1 - (b |^ o)) / (1 - b))) by A225

.= - (1 - (b |^ o)) by A224, XCMPLX_1:87

.= (b |^ o) - 1 ;

then Sum co < ((b |^ o) - 1) + 1 by A268, A270, AFINSQ_2:57, XREAL_1:145;

then A275: (Sum co) div (b |^ o) = 0 by NAT_D:27;

A276: now :: thesis: for k being Nat st k in dom d91 holds

d9 . ((len <%(E . o)%>) + k) = d91 . k

dom d9 =
1 + (dom d91)
by A252, A256
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 A277: k in dom d91 ; :: thesis: d9 . ((len <%(E . o)%>) + k) = d91 . k

then k < len d91 by A256, NAT_1:44;

then k + 1 < oo1 + 1 by XREAL_1:8, A256;

then A278: k + 1 in Segm oo by NAT_1:44;

thus d9 . ((len <%(E . o)%>) + k) = d9 . (1 + k) by AFINSQ_1:33

.= E . ((len co) + (k + 1)) by A252, A263, A278

.= E . ((len do1) + k) by A263, A241

.= d91 . k by A256, A241, A277 ; :: thesis: verum

end;assume A277: k in dom d91 ; :: thesis: d9 . ((len <%(E . o)%>) + k) = d91 . k

then k < len d91 by A256, NAT_1:44;

then k + 1 < oo1 + 1 by XREAL_1:8, A256;

then A278: k + 1 in Segm oo by NAT_1:44;

thus d9 . ((len <%(E . o)%>) + k) = d9 . (1 + k) by AFINSQ_1:33

.= E . ((len co) + (k + 1)) by A252, A263, A278

.= E . ((len do1) + k) by A263, A241

.= d91 . k by A256, A241, A277 ; :: thesis: verum

.= (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; :: thesis: verum

n = 0 and

A282: ( d = <%0%> & e = <%0%> ) ; :: thesis: d = e

thus d = e by A282; :: thesis: verum