reconsider b1 = b - 1 as Element of NAT by ;
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 = & e = 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 = & e = implies d = e )
proof
log (2,b) > log (2,1) by ;
then A33: log (2,b) > 0 by POWER:51;
log (2,b) > log (2,1) by ;
then A34: log (2,b) > 0 by POWER:51;
A35: 1 - b <> 0 by A1;
A36: 1 - b <> 0 by A1;
reconsider g = (b1 (#) ()) | (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 ;
dom d <> {} by ;
then A44: len D > 0 by A41;
A45: (len d) - 1 in dom d by ;
then reconsider k = (len d) - 1 as Element of NAT ;
A46: 1 * (b |^ k) <= (d . k) * (b |^ k) by ;
A47: b |^ k > 0 by ;
D . k = (d . k) * (b |^ k) by ;
then (d . k) * (b |^ k) <= n by ;
then b |^ k <= n by ;
then log (2,(b to_power k)) <= log (2,n) by ;
then k * (log (2,b)) <= log (2,n) by ;
then (k * (log (2,b))) / (log (2,b)) <= (log (2,n)) / (log (2,b)) by ;
then A48: k <= (log (2,n)) / (log (2,b)) by ;
g = ((b - 1) (#) ()) | (k + 1) ;
then A49: Sum g = (Partial_Sums ((b - 1) (#) ())) . k by AFINSQ_2:56
.= ((b - 1) (#) ()) . k by SERIES_1:9
.= (b - 1) * (() . k) by SEQ_1:9
.= (b - 1) * ((1 - (b to_power (k + 1))) / (1 - b)) by
.= - ((1 - b) * ((1 - (b |^ (k + 1))) / (1 - b)))
.= - (1 - (b |^ (k + 1))) by
.= (b |^ (k + 1)) - 1 ;
A50: dom ((b - 1) (#) ()) = NAT by FUNCT_2:def 1;
then A51: len D = len g by ;
len d c= dom ((b - 1) (#) ()) by ;
then A52: dom g = len d by RELAT_1:62;
A53: for i being Nat st i in dom D holds
D . i <= g . i
proof
let i be Nat; :: 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 ;
then A56: d . i <= b1 by NAT_1:13;
g . I = ((b - 1) (#) ()) . I by
.= (b - 1) * (() . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def 1 ;
hence D . i <= g . i by ; :: thesis: verum
end;
assume that
A57: value (e,b) = n and
A58: e . ((len e) - 1) <> 0 and
A59: for i being Nat st i in dom e holds
( 0 <= e . i & e . i < b ) ; :: 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 ;
A63: (len e) - 1 in dom e by ;
then reconsider l = (len e) - 1 as Element of NAT ;
A64: 1 * (b |^ l) <= (e . l) * (b |^ l) by ;
reconsider g = (b1 (#) ()) | (len e) as XFinSequence of NAT by Th1;
g = ((b - 1) (#) ()) | (l + 1) ;
then A65: Sum g = (Partial_Sums ((b - 1) (#) ())) . l by AFINSQ_2:56
.= ((b - 1) (#) ()) . l by SERIES_1:9
.= (b - 1) * (() . l) by SEQ_1:9
.= (b - 1) * ((1 - (b to_power (l + 1))) / (1 - b)) by
.= - ((1 - b) * ((1 - (b |^ (l + 1))) / (1 - b)))
.= - (1 - (b |^ (l + 1))) by
.= (b |^ (l + 1)) - 1 ;
dom E <> {} by ;
then A66: len E > 0 ;
A67: dom ((b - 1) (#) ()) = NAT by FUNCT_2:def 1;
then len e c= dom ((b - 1) (#) ()) by ORDINAL1:def 2;
then A68: dom g = len e by RELAT_1:62;
A69: for i being Nat st i in dom E holds
E . i <= g . i
proof
let i be Nat; :: 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 ;
then A72: e . i <= b1 by NAT_1:13;
g . I = ((b - 1) (#) ()) . I by
.= (b - 1) * (() . I) by SEQ_1:9
.= b1 * (b |^ I) by PREPOWER:def 1 ;
hence E . i <= g . i by ; :: thesis: verum
end;
A73: b |^ l > 0 by ;
E . l = (e . l) * (b |^ l) by ;
then (e . l) * (b |^ l) <= n by ;
then b |^ l <= n by ;
then log (2,(b to_power l)) <= log (2,n) by ;
then l * (log (2,b)) <= log (2,n) by ;
then (l * (log (2,b))) / (log (2,b)) <= (log (2,n)) / (log (2,b)) by ;
then A74: l <= (log (2,n)) / (log (2,b)) by ;
len E = len g by ;
then n < ((b |^ (l + 1)) - 1) + 1 by ;
then log (2,n) < log (2,(b to_power (l + 1))) by ;
then log (2,n) < (l + 1) * (log (2,b)) by ;
then (log (2,n)) / (log (2,b)) < ((l + 1) * (log (2,b))) / (log (2,b)) by ;
then (log (2,n)) / (log (2,b)) < l + 1 by ;
then k < l + 1 by ;
then A75: k <= l by NAT_1:13;
n < ((b |^ (k + 1)) - 1) + 1 by ;
then log (2,n) < log (2,(b to_power (k + 1))) by ;
then log (2,n) < (k + 1) * (log (2,b)) by ;
then (log (2,n)) / (log (2,b)) < ((k + 1) * (log (2,b))) / (log (2,b)) by ;
then (log (2,n)) / (log (2,b)) < k + 1 by ;
then l < k + 1 by ;
then l <= k by NAT_1:13;
then A76: k = l by ;
now :: thesis: for a being object st a in dom d holds
d . a = e . a
let a be object ; :: thesis: ( a in dom d implies d . b1 = e . b1 )
assume A77: a in dom d ; :: thesis: d . b1 = e . b1
then reconsider o = a as Element of NAT ;
o < k + 1 by ;
then A78: o <= k by NAT_1:13;
A79: o < len d by ;
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 ;
suppose A80: ( o = 0 & o = k ) ; :: thesis: d . b1 = e . b1
then len E = 1 by ;
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 ;
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
.= e . a by ;
:: thesis: verum
end;
suppose A82: ( o = 0 & o < k ) ; :: thesis: d . b1 = e . b1
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 ;
reconsider bo = b |^ o as Element of NAT by ORDINAL1:def 12;
A85: bo <> 0 by ;
A86: now :: thesis: for k being Nat st k in dom <%(D . o)%> holds
D . k = <%(D . o)%> . k
let k be Nat; :: thesis: ( k in dom <%(D . o)%> implies D . k = <%(D . o)%> . k )
assume k in dom <%(D . o)%> ; :: thesis: D . k = <%(D . o)%> . k
then k in 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;
reconsider o1 = o + 1 as Element of NAT ;
o1 <= k by ;
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 A90: len d = len D by A41;
then A91: len do1 = o1 by ;
then A92: dom D = (len do1) + (len d91) by ;
now :: thesis: for k being Nat st k in dom d91 holds
b |^ o1 divides d91 . k
let k be Nat; :: thesis: ( k in dom d91 implies b |^ o1 divides d91 . k )
reconsider K = k as Element of NAT by ORDINAL1:def 12;
assume 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 ;
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
.= (d . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:8
.= ((d . (o1 + k)) * (b |^ k)) * (b |^ o1) ;
hence b |^ o1 divides d91 . k by NAT_D:def 3; :: thesis: verum
end;
then A94: b |^ o1 divides Sum d91 by Th2;
A95: now :: thesis: for k being Nat st k in dom d91 holds
D . ((len <%(D . o)%>) + k) = d91 . k
let k be Nat; :: thesis: ( k in dom d91 implies D . ((len <%(D . o)%>) + k) = d91 . k )
assume A96: k in dom d91 ; :: thesis: D . ((len <%(D . o)%>) + k) = d91 . k
thus D . ((len <%(D . o)%>) + k) = D . ((len do1) + k) by
.= d91 . k by ; :: thesis: verum
end;
dom D = 1 + (dom d91) by
.= (len <%(D . o)%>) + (len d91) by AFINSQ_1:34 ;
then D = <%(D . o)%> ^ d91 by ;
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 ;
then D = do1 ^ d91 by ;
then A98: n = (Sum do1) + (Sum d91) by ;
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
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
.= (d . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8
.= ((d . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides D . k by NAT_D:def 3; :: thesis: verum
end;
then A100: b |^ o divides Sum D by Th2;
then (Sum D) mod (b |^ o) = 0 by ;
then n div (b |^ o) = ((Sum D) div (b |^ o)) + ((Sum co) div (b |^ o)) by ;
then A101: (n div (b |^ o)) * (b |^ o) = Sum D by ;
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 ;
reconsider bo = b |^ o as Element of NAT by ORDINAL1:def 12;
A104: bo <> 0 by ;
reconsider ok1 = ok1 as Element of NAT by ORDINAL1:def 12;
reconsider g1 = (b1 (#) ()) | (ok1 + 1) as XFinSequence of NAT by Th1;
A105: 1 - b <> 0 by A1;
dom ((b - 1) (#) ()) = NAT by FUNCT_2:def 1;
then A106: o1 c= dom ((b - 1) (#) ()) by ORDINAL1:def 2;
then A107: len do1 = len g1 by ;
A108: dom g1 = o1 by ;
A109: for i being Nat st i in dom do1 holds
do1 . i <= g1 . i
proof
let i be Nat; :: thesis: ( i in dom do1 implies do1 . i <= g1 . i )
reconsider I = i as Element of NAT by ORDINAL1:def 12;
assume A110: i in dom do1 ; :: thesis: do1 . i <= g1 . i
then i in o1 by ;
then A111: g1 . I = ((b - 1) (#) ()) . I by
.= (b - 1) * (() . 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 ;
then A113: d . i <= b1 by NAT_1:13;
do1 . i = D . i by
.= (d . i) * (b |^ i) by ;
hence do1 . i <= g1 . i by ; :: thesis: verum
end;
Sum g1 = (Partial_Sums ((b - 1) (#) ())) . ok1 by AFINSQ_2:56
.= ((b - 1) (#) ()) . ok1 by SERIES_1:9
.= (b - 1) * (() . ok1) by SEQ_1:9
.= (b - 1) * ((1 - (b to_power (ok1 + 1))) / (1 - b)) by
.= - ((1 - b) * ((1 - (b |^ o1)) / (1 - b))) by A99
.= - (1 - (b |^ o1)) by
.= (b |^ o1) - 1 ;
then Sum do1 < ((b |^ o1) - 1) + 1 by ;
then A114: (Sum do1) div (b |^ o1) = 0 by NAT_D:27;
bo1 <> 0 by ;
then (Sum d91) mod (b |^ o1) = 0 by ;
then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by ;
then (n div (b |^ o1)) * (b |^ o1) = Sum d91 by ;
then D . o = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by ;
then (d . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by ;
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 ;
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
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
.= (e . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8
.= ((e . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides E . k by NAT_D:def 3; :: thesis: verum
end;
then A117: b |^ o divides Sum E by Th2;
then (Sum E) mod (b |^ o) = 0 by ;
then n div (b |^ o) = ((Sum E) div (b |^ o)) + ((Sum co) div (b |^ o)) by ;
then A118: (n div (b |^ o)) * (b |^ o) = Sum E by ;
A119: now :: thesis: for k being Nat st k in dom <%(E . o)%> holds
E . k = <%(E . o)%> . k
let k be Nat; :: thesis: ( k in dom <%(E . o)%> implies E . k = <%(E . o)%> . k )
assume k in dom <%(E . o)%> ; :: thesis: E . k = <%(E . o)%> . k
then k in 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;
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 o1 <= k by ;
then A122: o1 < len d by XREAL_1:147;
then A123: len do1 = o1 by ;
A124: now :: thesis: for k being Nat st k in dom d91 holds
E . ((len <%(E . o)%>) + k) = d91 . k
let k be Nat; :: thesis: ( k in dom d91 implies E . ((len <%(E . o)%>) + k) = d91 . k )
assume A125: k in dom d91 ; :: thesis: E . ((len <%(E . o)%>) + k) = d91 . k
thus E . ((len <%(E . o)%>) + k) = E . ((len do1) + k) by
.= d91 . k by ; :: thesis: verum
end;
reconsider bo1 = b |^ o1 as Element of NAT by ORDINAL1:def 12;
consider ok1 being Nat such that
A126: ok1 + 1 = o1 ;
A127: dom E = (len do1) + (len d91) by ;
now :: thesis: for k being Nat st k in dom d91 holds
b |^ o1 divides d91 . k
let k be Nat; :: thesis: ( k in dom d91 implies b |^ o1 divides d91 . k )
reconsider K = k as Element of NAT by ORDINAL1:def 12;
assume 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 ;
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
.= (e . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:8
.= ((e . (o1 + k)) * (b |^ k)) * (b |^ o1) ;
hence b |^ o1 divides d91 . k by NAT_D:def 3; :: thesis: verum
end;
then A129: b |^ o1 divides Sum d91 by Th2;
reconsider ok1 = ok1 as Element of NAT by ORDINAL1:def 12;
reconsider g1 = (b1 (#) ()) | (ok1 + 1) as XFinSequence of NAT by Th1;
A130: 1 - b <> 0 by A1;
dom ((b - 1) (#) ()) = NAT by FUNCT_2:def 1;
then A131: o1 c= dom ((b - 1) (#) ()) by ORDINAL1:def 2;
then A132: len do1 = len g1 by ;
A133: dom g1 = o1 by ;
A134: for i being Nat st i in dom do1 holds
do1 . i <= g1 . i
proof
let i be Nat; :: thesis: ( i in dom do1 implies do1 . i <= g1 . i )
reconsider I = i as Element of NAT by ORDINAL1:def 12;
assume A135: i in dom do1 ; :: thesis: do1 . i <= g1 . i
then i in o1 by ;
then A136: g1 . I = ((b - 1) (#) ()) . I by
.= (b - 1) * (() . 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 ;
then A138: e . i <= b1 by NAT_1:13;
do1 . i = E . i by
.= (e . i) * (b |^ i) by ;
hence do1 . i <= g1 . i by ; :: thesis: verum
end;
Sum g1 = (Partial_Sums ((b - 1) (#) ())) . ok1 by AFINSQ_2:56
.= ((b - 1) (#) ()) . ok1 by SERIES_1:9
.= (b - 1) * (() . ok1) by SEQ_1:9
.= (b - 1) * ((1 - (b to_power (ok1 + 1))) / (1 - b)) by
.= - ((1 - b) * ((1 - (b |^ o1)) / (1 - b))) by A126
.= - (1 - (b |^ o1)) by
.= (b |^ o1) - 1 ;
then Sum do1 < ((b |^ o1) - 1) + 1 by ;
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 ;
then E = do1 ^ d91 by ;
then A140: n = (Sum do1) + (Sum d91) by ;
bo1 <> 0 by ;
then (Sum d91) mod (b |^ o1) = 0 by ;
then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by ;
then A141: (n div (b |^ o1)) * (b |^ o1) = Sum d91 by ;
dom E = 1 + (dom d91) by
.= (len <%(E . o)%>) + (len d91) by AFINSQ_1:34 ;
then E = <%(E . o)%> ^ d91 by ;
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 ;
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 ; :: thesis: verum
end;
suppose A142: ( o > 0 & o = k ) ; :: thesis: d . b1 = e . b1
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 ;
A145: len <%(D . o)%> = oo by ;
then A146: dom D = (len co) + (len <%(D . o)%>) by ;
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 ;
then x = 0 by NAT_1:14;
hence D . ((len co) + x) = <%(D . o)%> . x by A144; :: thesis: verum
end;
now :: thesis: for k being Nat st k in dom <%(D . o)%> holds
b |^ o divides <%(D . o)%> . k
let k be Nat; :: thesis: ( k in dom <%(D . o)%> implies b |^ o divides <%(D . o)%> . k )
reconsider K = k as Element of NAT by ORDINAL1:def 12;
assume 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 ;
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
.= (d . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8
.= ((d . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides <%(D . o)%> . k by NAT_D:def 3; :: thesis: verum
end;
then 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 ;
reconsider ok = ok as Element of NAT by ORDINAL1:def 12;
reconsider g = (b1 (#) ()) | (ok + 1) as XFinSequence of NAT by Th1;
A152: Sum g = (Partial_Sums ((b - 1) (#) ())) . ok by AFINSQ_2:56
.= ((b - 1) (#) ()) . ok by SERIES_1:9
.= (b - 1) * (() . ok) by SEQ_1:9
.= (b - 1) * ((1 - (b to_power (ok + 1))) / (1 - b)) by
.= - ((1 - b) * ((1 - (b |^ o)) / (1 - b))) by A151
.= - (1 - (b |^ o)) by
.= (b |^ o) - 1 ;
consider ok being Nat such that
A153: ok + 1 = o by ;
dom ((b - 1) (#) ()) = NAT by FUNCT_2:def 1;
then A154: o c= dom ((b - 1) (#) ()) by ORDINAL1:def 2;
then A155: dom g = o by ;
A156: 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 A157: i in dom co ; :: thesis: co . i <= g . i
then i in o by ;
then A158: g . I = ((b - 1) (#) ()) . I by
.= (b - 1) * (() . 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 ;
then A160: d . i <= b1 by NAT_1:13;
co . i = D . i by
.= (d . i) * (b |^ i) by ;
hence co . i <= g . i by ; :: thesis: verum
end;
len co = len g by ;
then Sum co < ((b |^ o) - 1) + 1 by ;
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 ;
then A162: n = (Sum co) + (Sum <%(D . o)%>) by ;
A163: bo <> 0 by ;
then (Sum <%(D . o)%>) mod (b |^ o) = 0 by ;
then n div (b |^ o) = ((Sum <%(D . o)%>) div (b |^ o)) + ((Sum co) div (b |^ o)) by ;
then (n div (b |^ o)) * (b |^ o) = Sum <%(D . o)%> by ;
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 ;
then A164: d . o = ((n div (b |^ o)) * (b |^ o)) / (b |^ o) by ;
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 ;
A167: len <%(E . o)%> = oo by ;
then A168: dom E = (len co) + (len <%(E . o)%>) by ;
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 ;
then x = 0 by NAT_1:14;
hence E . ((len co) + x) = <%(E . o)%> . x by A166; :: thesis: verum
end;
now :: thesis: for k being Nat st k in dom <%(E . o)%> holds
b |^ o divides <%(E . o)%> . k
let k be Nat; :: thesis: ( k in dom <%(E . o)%> implies b |^ o divides <%(E . o)%> . k )
reconsider K = k as Element of NAT by ORDINAL1:def 12;
assume 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 ;
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
.= (e . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8
.= ((e . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides <%(E . o)%> . k by NAT_D:def 3; :: thesis: verum
end;
then A171: b |^ o divides Sum <%(E . o)%> by Th2;
reconsider ok = ok as Element of NAT by ORDINAL1:def 12;
reconsider g = (b1 (#) ()) | (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) (#) ()) = NAT by FUNCT_2:def 1;
then A173: o c= dom ((b - 1) (#) ()) by ORDINAL1:def 2;
then A174: len co = len g by ;
A175: dom g = o by ;
A176: 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 A177: i in dom co ; :: thesis: co . i <= g . i
then i in o by ;
then A178: g . I = ((b - 1) (#) ()) . I by
.= (b - 1) * (() . 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 ;
then A180: e . i <= b1 by NAT_1:13;
co . i = E . i by
.= (e . i) * (b |^ i) by ;
hence co . i <= g . i by ; :: thesis: verum
end;
Sum g = (Partial_Sums ((b - 1) (#) ())) . ok by AFINSQ_2:56
.= ((b - 1) (#) ()) . ok by SERIES_1:9
.= (b - 1) * (() . ok) by SEQ_1:9
.= (b - 1) * ((1 - (b to_power (ok + 1))) / (1 - b)) by
.= - ((1 - b) * ((1 - (b |^ o)) / (1 - b))) by A153
.= - (1 - (b |^ o)) by
.= (b |^ o) - 1 ;
then Sum co < ((b |^ o) - 1) + 1 by ;
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 ;
then A182: n = (Sum co) + (Sum <%(E . o)%>) by ;
A183: bo <> 0 by ;
then (Sum <%(E . o)%>) mod (b |^ o) = 0 by ;
then n div (b |^ o) = ((Sum <%(E . o)%>) div (b |^ o)) + ((Sum co) div (b |^ o)) by ;
then (n div (b |^ o)) * (b |^ o) = Sum <%(E . o)%> by ;
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 ; :: thesis: verum
end;
suppose A184: ( o > 0 & o < k ) ; :: thesis: d . b1 = e . b1
reconsider o1 = o + 1 as Element of NAT ;
A185: o1 <= k by ;
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 (#) ()) | (ok1 + 1) as XFinSequence of NAT by Th1;
A188: len d = len D by A41;
then A189: len do1 = o1 by ;
dom ((b - 1) (#) ()) = NAT by FUNCT_2:def 1;
then A190: o1 c= dom ((b - 1) (#) ()) by ORDINAL1:def 2;
then A191: len do1 = len g1 by ;
A192: dom g1 = o1 by ;
A193: for i being Nat st i in dom do1 holds
do1 . i <= g1 . i
proof
let i be Nat; :: thesis: ( i in dom do1 implies do1 . i <= g1 . i )
reconsider I = i as Element of NAT by ORDINAL1:def 12;
assume A194: i in dom do1 ; :: thesis: do1 . i <= g1 . i
then i in o1 by ;
then A195: g1 . I = ((b - 1) (#) ()) . I by
.= (b - 1) * (() . 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 ;
then A197: d . i <= b1 by NAT_1:13;
do1 . i = D . i by
.= (d . i) * (b |^ i) by ;
hence do1 . i <= g1 . i by ; :: thesis: verum
end;
k < len d by XREAL_1:147;
then reconsider oo1 = (len d) - o1 as Element of NAT by ;
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
A200: now :: thesis: for k being Nat st k in dom <%(D . o)%> holds
d9 . k = <%(D . o)%> . k
let k be Nat; :: thesis: ( k in dom <%(D . o)%> implies d9 . k = <%(D . o)%> . k )
assume k in dom <%(D . o)%> ; :: thesis: d9 . k = <%(D . o)%> . k
then k in 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 ;
then k in dom d9 by ;
hence d9 . k = D . (k + o) by A199
.= <%(D . o)%> . k by A201 ;
:: thesis: verum
end;
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 reconsider co = D | o as XFinSequence of NAT ;
A204: len d = len D by A41;
then A205: len co = o by ;
then A206: dom D = (len co) + (len d9) by ;
now :: thesis: for k being Nat st k in dom d9 holds
b |^ o divides d9 . k
let k be Nat; :: thesis: ( k in dom d9 implies b |^ o divides d9 . k )
reconsider K = k as Element of NAT by ORDINAL1:def 12;
assume 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 ;
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
.= (d . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8
.= ((d . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides d9 . k by NAT_D:def 3; :: thesis: verum
end;
then 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 ;
then D = co ^ d9 by ;
then A209: n = (Sum co) + (Sum d9) by ;
consider ok being Nat such that
A210: ok + 1 = o by ;
reconsider ok = ok as Element of NAT by ORDINAL1:def 12;
reconsider g = (b1 (#) ()) | (ok + 1) as XFinSequence of NAT by Th1;
A211: 1 - b <> 0 by A1;
A212: Sum g = (Partial_Sums ((b - 1) (#) ())) . ok by AFINSQ_2:56
.= ((b - 1) (#) ()) . ok by SERIES_1:9
.= (b - 1) * (() . ok) by SEQ_1:9
.= (b - 1) * ((1 - (b to_power (ok + 1))) / (1 - b)) by
.= - ((1 - b) * ((1 - (b |^ o)) / (1 - b))) by A210
.= - (1 - (b |^ o)) by
.= (b |^ o) - 1 ;
dom ((b - 1) (#) ()) = NAT by FUNCT_2:def 1;
then A213: o c= dom ((b - 1) (#) ()) by ORDINAL1:def 2;
then A214: dom g = o by ;
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 ;
then A217: g . I = ((b - 1) (#) ()) . I by
.= (b - 1) * (() . 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 ;
then A219: d . i <= b1 by NAT_1:13;
co . i = D . i by
.= (d . i) * (b |^ i) by ;
hence co . i <= g . i by ; :: thesis: verum
end;
A220: now :: thesis: for k being Nat st k in dom d91 holds
d9 . ((len <%(D . o)%>) + k) = d91 . k
let k be Nat; :: thesis: ( k in dom d91 implies d9 . ((len <%(D . o)%>) + k) = d91 . k )
assume A221: k in dom d91 ; :: thesis: d9 . ((len <%(D . o)%>) + k) = d91 . k
then k < len d91 by ;
then k + 1 < oo1 + 1 by ;
then k + 1 < len d9 by A199;
then A222: k + 1 in dom d9 by ;
thus d9 . ((len <%(D . o)%>) + k) = d9 . (1 + k) by AFINSQ_1:33
.= D . ((len co) + (k + 1)) by
.= D . ((len do1) + k) by
.= d91 . k by ; :: thesis: verum
end;
dom d9 = 1 + (dom d91) by
.= (len <%(D . o)%>) + (len d91) by AFINSQ_1:34 ;
then d9 = <%(D . o)%> ^ d91 by ;
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 ;
A226: dom D = (len do1) + (len d91) by ;
now :: thesis: for k being Nat st k in dom d91 holds
b |^ o1 divides d91 . k
let k be Nat; :: thesis: ( k in dom d91 implies b |^ o1 divides d91 . k )
reconsider K = k as Element of NAT by ORDINAL1:def 12;
assume 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 ;
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
.= (d . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:8
.= ((d . (o1 + k)) * (b |^ k)) * (b |^ o1) ;
hence b |^ o1 divides d91 . k by NAT_D:def 3; :: thesis: verum
end;
then A228: b |^ o1 divides Sum d91 by Th2;
len co = len g by ;
then Sum co < ((b |^ o) - 1) + 1 by ;
then A229: (Sum co) div (b |^ o) = 0 by NAT_D:27;
A230: 1 - b <> 0 by A1;
Sum g1 = (Partial_Sums ((b - 1) (#) ())) . ok1 by AFINSQ_2:56
.= ((b - 1) (#) ()) . ok1 by SERIES_1:9
.= (b - 1) * (() . ok1) by SEQ_1:9
.= (b - 1) * ((1 - (b to_power (ok1 + 1))) / (1 - b)) by
.= - ((1 - b) * ((1 - (b |^ o1)) / (1 - b))) by A187
.= - (1 - (b |^ o1)) by
.= (b |^ o1) - 1 ;
then Sum do1 < ((b |^ o1) - 1) + 1 by ;
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 ;
then D = do1 ^ d91 by ;
then A232: n = (Sum do1) + (Sum d91) by ;
bo1 <> 0 by ;
then (Sum d91) mod (b |^ o1) = 0 by ;
then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by ;
then A233: (n div (b |^ o1)) * (b |^ o1) = Sum d91 by ;
A234: bo <> 0 by ;
then (Sum d9) mod (b |^ o) = 0 by ;
then n div (b |^ o) = ((Sum d9) div (b |^ o)) + ((Sum co) div (b |^ o)) by ;
then ( (n div (b |^ o)) * (b |^ o) = Sum d9 & Sum <%(D . o)%> = D . o ) by ;
then (d . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by ;
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 ;
reconsider o1 = o + 1 as Element of NAT ;
A236: o1 <= k by ;
then A237: o1 < len d by XREAL_1:147;
reconsider ok = ok as Element of NAT by ORDINAL1:def 12;
reconsider g = (b1 (#) ()) | (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 (#) ()) | (ok1 + 1) as XFinSequence of NAT by Th1;
A240: len e = len E by A60;
then A241: len do1 = o1 by ;
dom ((b - 1) (#) ()) = NAT by FUNCT_2:def 1;
then A242: o1 c= dom ((b - 1) (#) ()) by ORDINAL1:def 2;
then A243: len do1 = len g1 by ;
A244: dom g1 = o1 by ;
A245: for i being Nat st i in dom do1 holds
do1 . i <= g1 . i
proof
let i be Nat; :: thesis: ( i in dom do1 implies do1 . i <= g1 . i )
reconsider I = i as Element of NAT by ORDINAL1:def 12;
assume A246: i in dom do1 ; :: thesis: do1 . i <= g1 . i
then i in o1 by ;
then A247: g1 . I = ((b - 1) (#) ()) . I by
.= (b - 1) * (() . 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 ;
then A249: e . i <= b1 by NAT_1:13;
do1 . i = E . i by
.= (e . i) * (b |^ i) by ;
hence do1 . i <= g1 . i by ; :: thesis: verum
end;
Sum g1 = (Partial_Sums ((b - 1) (#) ())) . ok1 by AFINSQ_2:56
.= ((b - 1) (#) ()) . ok1 by SERIES_1:9
.= (b - 1) * (() . ok1) by SEQ_1:9
.= (b - 1) * ((1 - (b to_power (ok1 + 1))) / (1 - b)) by
.= - ((1 - b) * ((1 - (b |^ o1)) / (1 - b))) by A239
.= - (1 - (b |^ o1)) by
.= (b |^ o1) - 1 ;
then Sum do1 < ((b |^ o1) - 1) + 1 by ;
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 ;
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
A253: now :: thesis: for k being Nat st k in dom <%(E . o)%> holds
d9 . k = <%(E . o)%> . k
let k be Nat; :: thesis: ( k in dom <%(E . o)%> implies d9 . k = <%(E . o)%> . k )
assume k in dom <%(E . o)%> ; :: thesis: d9 . k = <%(E . o)%> . k
then k in Segm 1 by AFINSQ_1:33;
then k < 1 by NAT_1:44;
then A254: k = 0 by NAT_1:14;
oo > 0 by ;
then k < len d9 by ;
then k in dom d9 by ;
hence d9 . k = E . (k + o) by A252
.= <%(E . o)%> . k by A254 ;
:: thesis: verum
end;
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 A257: dom E = (len do1) + (len d91) by ;
now :: thesis: for k being Nat st k in dom d91 holds
b |^ o1 divides d91 . k
let k be Nat; :: thesis: ( k in dom d91 implies b |^ o1 divides d91 . k )
reconsider K = k as Element of NAT by ORDINAL1:def 12;
assume 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 ;
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
.= (e . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:8
.= ((e . (o1 + k)) * (b |^ k)) * (b |^ o1) ;
hence b |^ o1 divides d91 . k by NAT_D:def 3; :: thesis: verum
end;
then 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 ;
then E = do1 ^ d91 by ;
then A260: n = (Sum do1) + (Sum d91) by ;
bo1 <> 0 by ;
then (Sum d91) mod (b |^ o1) = 0 by ;
then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by ;
then A261: (n div (b |^ o1)) * (b |^ o1) = Sum d91 by ;
reconsider co = E | o as XFinSequence of NAT ;
A262: len e = len E by A60;
then A263: len co = o by ;
then A264: dom E = (len co) + (len d9) by ;
now :: thesis: for k being Nat st k in dom d9 holds
b |^ o divides d9 . k
let k be Nat; :: thesis: ( k in dom d9 implies b |^ o divides d9 . k )
reconsider K = k as Element of NAT by ORDINAL1:def 12;
assume 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 ;
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
.= (e . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8
.= ((e . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides d9 . k by NAT_D:def 3; :: thesis: verum
end;
then A266: b |^ o divides Sum d9 by Th2;
dom ((b - 1) (#) ()) = NAT by FUNCT_2:def 1;
then A267: o c= dom ((b - 1) (#) ()) by ORDINAL1:def 2;
then A268: len co = len g by ;
A269: dom g = o by ;
A270: 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 A271: i in dom co ; :: thesis: co . i <= g . i
then i in o by ;
then A272: g . I = ((b - 1) (#) ()) . I by
.= (b - 1) * (() . 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 ;
then A274: e . i <= b1 by NAT_1:13;
co . i = E . i by
.= (e . i) * (b |^ i) by ;
hence co . i <= g . i by ; :: thesis: verum
end;
Sum g = (Partial_Sums ((b - 1) (#) ())) . ok by AFINSQ_2:56
.= ((b - 1) (#) ()) . ok by SERIES_1:9
.= (b - 1) * (() . ok) by SEQ_1:9
.= (b - 1) * ((1 - (b to_power (ok + 1))) / (1 - b)) by
.= - ((1 - b) * ((1 - (b |^ o)) / (1 - b))) by A225
.= - (1 - (b |^ o)) by
.= (b |^ o) - 1 ;
then Sum co < ((b |^ o) - 1) + 1 by ;
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
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 ;
then k + 1 < oo1 + 1 by ;
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
.= E . ((len do1) + k) by
.= d91 . k by ; :: thesis: verum
end;
dom d9 = 1 + (dom d91) by
.= (len <%(E . o)%>) + (len d91) by AFINSQ_1:34 ;
then d9 = <%(E . o)%> ^ d91 by ;
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 ;
then E = co ^ d9 by ;
then A280: n = (Sum co) + (Sum d9) by ;
A281: bo <> 0 by ;
then (Sum d9) mod (b |^ o) = 0 by ;
then n div (b |^ o) = ((Sum d9) div (b |^ o)) + ((Sum co) div (b |^ o)) by ;
then (n div (b |^ o)) * (b |^ o) = Sum d9 by ;
then E . o = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by ;
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 ; :: thesis: verum
end;
end;
end;
hence d = e by ; :: thesis: verum
end;
assume that
n = 0 and
A282: ( d = & e = ) ; :: thesis: d = e
thus d = e by A282; :: thesis: verum