reconsider b1 = b - 1 as Element of NAT by A1, NAT_1:20;
let d, e be XFinSequence of NAT ; :: thesis: ( ( n <> 0 & value d,b = n & d . ((len d) - 1) <> 0 & ( for i being Nat st i in dom d holds
( 0 <= d . i & d . i < b ) ) & value e,b = n & e . ((len e) - 1) <> 0 & ( for i being Nat st i in dom e holds
( 0 <= e . i & e . i < b ) ) implies d = e ) & ( not n <> 0 & d = <%0 %> & e = <%0 %> implies d = e ) )
thus ( n <> 0 & value d,b = n & d . ((len d) - 1) <> 0 & ( for i being Nat st i in dom d holds
( 0 <= d . i & d . i < b ) ) & value e,b = n & e . ((len e) - 1) <> 0 & ( for i being Nat st i in dom e holds
( 0 <= e . i & e . i < b ) ) implies d = e ) :: thesis: ( not n <> 0 & d = <%0 %> & e = <%0 %> implies d = e )
proof
log 2,b > log 2,1 by A1, POWER:65;
then A33: log 2,b > 0 by POWER:59;
log 2,b > log 2,1 by A1, POWER:65;
then A34: log 2,b > 0 by POWER:59;
A35: 1 - b <> 0 by A1;
A36: 1 - b <> 0 by A1;
reconsider g = (b1 (#) (b GeoSeq )) | (len d) as XFinSequence of NAT by Th3;
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;
A44: len D > 0 by A39, A41, FUNCT_1:def 4;
A45: (len d) - 1 in dom d by A39, FUNCT_1:def 4;
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:13;
D . k = (d . k) * (b |^ k) by A41, A42, A45;
then (d . k) * (b |^ k) <= n by A41, A43, A45, A44, AFINSQ_2:73;
then b |^ k <= n by A46, XXREAL_0:2;
then log 2,(b to_power k) <= log 2,n by A47, PRE_FF:12;
then k * (log 2,b) <= log 2,n by A1, POWER:63;
then (k * (log 2,b)) / (log 2,b) <= (log 2,n) / (log 2,b) by A34, XREAL_1:74;
then A48: k <= (log 2,n) / (log 2,b) by A34, XCMPLX_1:90;
g = ((b - 1) (#) (b GeoSeq )) | (k + 1) ;
then A49: Sum g = (Partial_Sums ((b - 1) (#) (b GeoSeq ))) . k by AFINSQ_2:68
.= ((b - 1) (#) (Partial_Sums (b GeoSeq ))) . k by SERIES_1:12
.= (b - 1) * ((Partial_Sums (b GeoSeq )) . k) by SEQ_1:13
.= (b - 1) * ((1 - (b to_power (k + 1))) / (1 - b)) by A1, SERIES_1:26
.= - ((1 - b) * ((1 - (b |^ (k + 1))) / (1 - b)))
.= - (1 - (b |^ (k + 1))) by A36, XCMPLX_1:88
.= (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:91;
len d c= dom ((b - 1) (#) (b GeoSeq )) by A50, ORDINAL1:def 2;
then A52: dom g = len d by RELAT_1:91;
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 13;
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:70
.= (b - 1) * ((b GeoSeq ) . I) by SEQ_1:13
.= b1 * (b |^ I) by PREPOWER:def 1 ;
hence D . i <= g . i by A56, A55, XREAL_1:66; :: 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 A57, Def1;
A63: (len e) - 1 in dom e by A58, FUNCT_1:def 4;
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 Th3;
g = ((b - 1) (#) (b GeoSeq )) | (l + 1) ;
then A65: Sum g = (Partial_Sums ((b - 1) (#) (b GeoSeq ))) . l by AFINSQ_2:68
.= ((b - 1) (#) (Partial_Sums (b GeoSeq ))) . l by SERIES_1:12
.= (b - 1) * ((Partial_Sums (b GeoSeq )) . l) by SEQ_1:13
.= (b - 1) * ((1 - (b to_power (l + 1))) / (1 - b)) by A1, SERIES_1:26
.= - ((1 - b) * ((1 - (b |^ (l + 1))) / (1 - b)))
.= - (1 - (b |^ (l + 1))) by A35, XCMPLX_1:88
.= (b |^ (l + 1)) - 1 ;
A66: 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 A67: dom g = len e by RELAT_1:91;
A68: 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 13;
assume A69: i in dom E ; :: thesis: E . i <= g . i
then A70: E . i = (e . i) * (b |^ i) by A61;
e . i < b1 + 1 by A59, A60, A69;
then A71: e . i <= b1 by NAT_1:13;
g . I = ((b - 1) (#) (b GeoSeq )) . I by A60, A67, A69, FUNCT_1:70
.= (b - 1) * ((b GeoSeq ) . I) by SEQ_1:13
.= b1 * (b |^ I) by PREPOWER:def 1 ;
hence E . i <= g . i by A71, A70, XREAL_1:66; :: thesis: verum
end;
A72: len E > 0 by A58, A60, FUNCT_1:def 4;
A74: b |^ l > 0 by A1, PREPOWER:13;
E . l = (e . l) * (b |^ l) by A60, A61, A63;
then (e . l) * (b |^ l) <= n by A60, A62, A63, A72, AFINSQ_2:73;
then b |^ l <= n by A64, XXREAL_0:2;
then log 2,(b to_power l) <= log 2,n by A74, PRE_FF:12;
then l * (log 2,b) <= log 2,n by A1, POWER:63;
then (l * (log 2,b)) / (log 2,b) <= (log 2,n) / (log 2,b) by A33, XREAL_1:74;
then A75: l <= (log 2,n) / (log 2,b) by A33, XCMPLX_1:90;
len E = len g by A60, A66, RELAT_1:91;
then n < ((b |^ (l + 1)) - 1) + 1 by A62, A65, A68, AFINSQ_2:69, XREAL_1:41;
then log 2,n < log 2,(b to_power (l + 1)) by A37, POWER:65;
then log 2,n < (l + 1) * (log 2,b) by A1, POWER:63;
then (log 2,n) / (log 2,b) < ((l + 1) * (log 2,b)) / (log 2,b) by A33, XREAL_1:76;
then (log 2,n) / (log 2,b) < l + 1 by A33, XCMPLX_1:90;
then k < l + 1 by A48, XXREAL_0:2;
then A76: k <= l by NAT_1:13;
n < ((b |^ (k + 1)) - 1) + 1 by A43, A49, A51, A53, AFINSQ_2:69, XREAL_1:41;
then log 2,n < log 2,(b to_power (k + 1)) by A37, POWER:65;
then log 2,n < (k + 1) * (log 2,b) by A1, POWER:63;
then (log 2,n) / (log 2,b) < ((k + 1) * (log 2,b)) / (log 2,b) by A34, XREAL_1:76;
then (log 2,n) / (log 2,b) < k + 1 by A34, XCMPLX_1:90;
then l < k + 1 by A75, XXREAL_0:2;
then l <= k by NAT_1:13;
then A77: k = l by A76, XXREAL_0:1;
now
let a be set ; :: thesis: ( a in dom d implies d . b1 = e . b1 )
assume A78: a in dom d ; :: thesis: d . b1 = e . b1
then reconsider o = a as Element of NAT ;
o < k + 1 by A78, NAT_1:45;
then A79: o <= k by NAT_1:13;
A80: o < len d by A78, NAT_1:45;
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 A79, XXREAL_0:1;
suppose A81: ( o = 0 & o = k ) ; :: thesis: d . b1 = e . b1
then len E = 1 by A60, A77;
then A82: E = <%(E . 0 )%> by AFINSQ_1:38
.= <%((e . 0 ) * (b |^ 0 ))%> by A60, A61, A77, A78, A81
.= <%((e . 0 ) * 1)%> by NEWTON:9 ;
len D = 1 by A41, A81;
then D = <%(D . 0 )%> by AFINSQ_1:38
.= <%((d . 0 ) * (b |^ 0 ))%> by A41, A42, A78, A81
.= <%((d . 0 ) * 1)%> by NEWTON:9 ;
hence d . a = n by A43, A81, AFINSQ_2:65
.= e . a by A62, A81, A82, AFINSQ_2:65 ;
:: thesis: verum
end;
suppose A83: ( o = 0 & o < k ) ; :: thesis: d . b1 = e . b1
reconsider do = <%> NAT as XFinSequence of NAT ;
A84: len do = o by A83;
Sum do = 0 ;
then A85: (Sum do) div (b |^ o) = 0 by NAT_2:4;
set d9 = D;
A86: for x being Nat st x in dom do holds
D . x = do . x ;
( dom D = (len do) + (len D) & ( for x being Nat st x in dom D holds
D . ((len do) + x) = D . x ) ) by A83, A84;
then D = do ^ D by A86, AFINSQ_1:def 4;
then A87: n = (Sum do) + (Sum D) by A43, AFINSQ_2:67;
reconsider bo = b |^ o as Element of NAT by ORDINAL1:def 13;
A88: bo <> 0 by A1, PREPOWER:12;
A89: now
let k be Nat; :: thesis: ( k in dom <%(D . o)%> implies D . k = <%(D . o)%> . k )
assume k in dom <%(D . o)%> ; :: thesis: D . k = <%(D . o)%> . k
then k in 1 by AFINSQ_1:36;
then k < 1 by NAT_1:45;
then k = 0 by NAT_1:14;
hence D . k = <%(D . o)%> . k by A83, AFINSQ_1:def 5; :: thesis: verum
end;
reconsider o1 = o + 1 as Element of NAT ;
o1 <= k by A83, NAT_1:13;
then A90: o1 < len d by XREAL_1:149;
reconsider oo1 = (len d) - o1 as Element of NAT by A83;
defpred S1[ Nat, set ] means $2 = D . ($1 + o1);
reconsider do1 = D | o1 as XFinSequence of NAT ;
A91: for u being Nat st u in oo1 holds
ex x being Element of NAT st S1[u,x] ;
consider d91 being XFinSequence of NAT such that
A92: ( dom d91 = oo1 & ( for x being Nat st x in oo1 holds
S1[x,d91 . x] ) ) from STIRL2_1:sch 5(A91);
A93: len d = len D by A41;
then A94: len do1 = o1 by A90, AFINSQ_1:14;
then A96: dom D = (len do1) + (len d91) by A41, A92;
now
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 13;
assume A97: k in dom d91 ; :: thesis: b |^ o1 divides d91 . k
then k < len d91 by NAT_1:45;
then o1 + k < dom D by A94, A96, XREAL_1:10;
then o1 + k in dom D by NAT_1:45;
then D . (o1 + k) = (d . (o1 + k)) * (b |^ (o1 + k)) by A42;
then d91 . K = (d . (o1 + k)) * (b |^ (o1 + k)) by A92, A97
.= (d . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:13
.= ((d . (o1 + k)) * (b |^ k)) * (b |^ o1) ;
hence b |^ o1 divides d91 . k by NAT_D:def 3; :: thesis: verum
end;
then A98: b |^ o1 divides Sum d91 by Th5;
A99: now
let k be Nat; :: thesis: ( k in dom d91 implies D . ((len <%(D . o)%>) + k) = d91 . k )
assume A100: k in dom d91 ; :: thesis: D . ((len <%(D . o)%>) + k) = d91 . k
thus D . ((len <%(D . o)%>) + k) = D . ((len do1) + k) by A83, A94, AFINSQ_1:36
.= d91 . k by A92, A94, A100 ; :: thesis: verum
end;
dom D = 1 + (dom d91) by A41, A83, A92
.= (len <%(D . o)%>) + (len d91) by AFINSQ_1:38 ;
then D = <%(D . o)%> ^ d91 by A89, A99, AFINSQ_1:def 4;
then A101: Sum D = (Sum <%(D . o)%>) + (Sum d91) by AFINSQ_2:67;
( ( 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 A92, A94, FUNCT_1:70;
then D = do1 ^ d91 by A96, AFINSQ_1:def 4;
then A102: n = (Sum do1) + (Sum d91) by A43, AFINSQ_2:67;
reconsider bo1 = b |^ o1 as Element of NAT by ORDINAL1:def 13;
consider ok1 being Nat such that
A103: ok1 + 1 = o1 ;
now
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 13;
assume k in dom D ; :: thesis: b |^ o divides D . k
then D . K = (d . (o + k)) * (b |^ (o + k)) by A42, A83
.= (d . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:13
.= ((d . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides D . k by NAT_D:def 3; :: thesis: verum
end;
then A104: b |^ o divides Sum D by Th5;
then (Sum D) mod (b |^ o) = 0 by A88, PEPIN:6;
then n div (b |^ o) = ((Sum D) div (b |^ o)) + ((Sum do) div (b |^ o)) by A87, NAT_D:19;
then A105: (n div (b |^ o)) * (b |^ o) = Sum D by A85, A104, NAT_D:3;
reconsider do = <%> NAT as XFinSequence of NAT ;
A106: len do = o by A83;
Sum do = 0 ;
then A107: (Sum do) div (b |^ o) = 0 by NAT_2:4;
set d9 = E;
A108: for x being Nat st x in dom do holds
E . x = do . x ;
( dom E = (len do) + (len E) & ( for x being Nat st x in dom E holds
E . ((len do) + x) = E . x ) ) by A83, A106;
then E = do ^ E by A108, AFINSQ_1:def 4;
then A109: n = (Sum do) + (Sum E) by A62, AFINSQ_2:67;
reconsider bo = b |^ o as Element of NAT by ORDINAL1:def 13;
A110: bo <> 0 by A1, PREPOWER:12;
reconsider ok1 = ok1 as Element of NAT by ORDINAL1:def 13;
reconsider g1 = (b1 (#) (b GeoSeq )) | (ok1 + 1) as XFinSequence of NAT by Th3;
A111: 1 - b <> 0 by A1;
dom ((b - 1) (#) (b GeoSeq )) = NAT by FUNCT_2:def 1;
then A112: o1 c= dom ((b - 1) (#) (b GeoSeq )) by ORDINAL1:def 2;
then A113: len do1 = len g1 by A94, A103, RELAT_1:91;
A114: dom g1 = o1 by A103, A112, RELAT_1:91;
A115: 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 13;
assume A116: i in dom do1 ; :: thesis: do1 . i <= g1 . i
then i in o1 by A90, A93, AFINSQ_1:14;
then A117: g1 . I = ((b - 1) (#) (b GeoSeq )) . I by A114, FUNCT_1:70
.= (b - 1) * ((b GeoSeq ) . I) by SEQ_1:13
.= b1 * (b |^ I) by PREPOWER:def 1 ;
A118: dom do1 c= dom D by RELAT_1:89;
then d . i < b1 + 1 by A40, A41, A116;
then A119: d . i <= b1 by NAT_1:13;
do1 . i = D . i by A116, FUNCT_1:70
.= (d . i) * (b |^ i) by A42, A116, A118 ;
hence do1 . i <= g1 . i by A117, A119, XREAL_1:66; :: thesis: verum
end;
Sum g1 = (Partial_Sums ((b - 1) (#) (b GeoSeq ))) . ok1 by AFINSQ_2:68
.= ((b - 1) (#) (Partial_Sums (b GeoSeq ))) . ok1 by SERIES_1:12
.= (b - 1) * ((Partial_Sums (b GeoSeq )) . ok1) by SEQ_1:13
.= (b - 1) * ((1 - (b to_power (ok1 + 1))) / (1 - b)) by A1, SERIES_1:26
.= - ((1 - b) * ((1 - (b |^ o1)) / (1 - b))) by A103
.= - (1 - (b |^ o1)) by A111, XCMPLX_1:88
.= (b |^ o1) - 1 ;
then Sum do1 < ((b |^ o1) - 1) + 1 by A113, A115, AFINSQ_2:69, XREAL_1:147;
then A120: (Sum do1) div (b |^ o1) = 0 by NAT_D:27;
bo1 <> 0 by A1, PREPOWER:12;
then (Sum d91) mod (b |^ o1) = 0 by A98, PEPIN:6;
then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by A102, NAT_D:19;
then (n div (b |^ o1)) * (b |^ o1) = Sum d91 by A120, A98, NAT_D:3;
then D . o = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A105, A101, AFINSQ_2:65;
then (d . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A41, A42, A78;
then (d . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * ((b |^ o) * (b |^ 1))) by NEWTON:13;
then (d . o) * (b |^ o) = (b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * (b |^ 1))) ;
then ((b |^ o) * (d . o)) / (b |^ o) = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o) by NEWTON:10;
then A121: d . o = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o) by A88, XCMPLX_1:90;
reconsider o1 = o + 1 as Element of NAT ;
reconsider do1 = E | o1 as XFinSequence of NAT ;
A122: len e = len E by A60;
now
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 13;
assume k in dom E ; :: thesis: b |^ o divides E . k
then E . K = (e . (o + k)) * (b |^ (o + k)) by A61, A83
.= (e . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:13
.= ((e . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides E . k by NAT_D:def 3; :: thesis: verum
end;
then A123: b |^ o divides Sum E by Th5;
then (Sum E) mod (b |^ o) = 0 by A110, PEPIN:6;
then n div (b |^ o) = ((Sum E) div (b |^ o)) + ((Sum do) div (b |^ o)) by A109, NAT_D:19;
then A124: (n div (b |^ o)) * (b |^ o) = Sum E by A107, A123, NAT_D:3;
A125: now
let k be Nat; :: thesis: ( k in dom <%(E . o)%> implies E . k = <%(E . o)%> . k )
assume k in dom <%(E . o)%> ; :: thesis: E . k = <%(E . o)%> . k
then k in 1 by AFINSQ_1:36;
then k < 1 by NAT_1:45;
then k = 0 by NAT_1:14;
hence E . k = <%(E . o)%> . k by A83, AFINSQ_1:def 5; :: thesis: verum
end;
reconsider oo1 = (len d) - o1 as Element of NAT by A83;
defpred S2[ Nat, set ] means $2 = E . ($1 + o1);
A126: for u being Nat st u in oo1 holds
ex x being Element of NAT st S2[u,x] ;
consider d91 being XFinSequence of NAT such that
A127: ( dom d91 = oo1 & ( for x being Nat st x in oo1 holds
S2[x,d91 . x] ) ) from STIRL2_1:sch 5(A126);
 o1 <= k by A83, NAT_1:13;
then A128: o1 < len d by XREAL_1:149;
then A129: len do1 = o1 by A77, A122, AFINSQ_1:14;
A131: now
let k be Nat; :: thesis: ( k in dom d91 implies E . ((len <%(E . o)%>) + k) = d91 . k )
assume A132: k in dom d91 ; :: thesis: E . ((len <%(E . o)%>) + k) = d91 . k
thus E . ((len <%(E . o)%>) + k) = E . ((len do1) + k) by A83, A129, AFINSQ_1:36
.= d91 . k by A127, A129, A132 ; :: thesis: verum
end;
reconsider bo1 = b |^ o1 as Element of NAT by ORDINAL1:def 13;
consider ok1 being Nat such that
A133: ok1 + 1 = o1 ;
A134: dom E = (len do1) + (len d91) by A60, A77, A127, A129;
now
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 13;
assume A135: k in dom d91 ; :: thesis: b |^ o1 divides d91 . k
then k < len d91 by NAT_1:45;
then o1 + k < dom E by A129, A134, XREAL_1:10;
then o1 + k in dom E by NAT_1:45;
then E . (o1 + k) = (e . (o1 + k)) * (b |^ (o1 + k)) by A61;
then d91 . K = (e . (o1 + k)) * (b |^ (o1 + k)) by A127, A135
.= (e . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:13
.= ((e . (o1 + k)) * (b |^ k)) * (b |^ o1) ;
hence b |^ o1 divides d91 . k by NAT_D:def 3; :: thesis: verum
end;
then A136: b |^ o1 divides Sum d91 by Th5;
reconsider ok1 = ok1 as Element of NAT by ORDINAL1:def 13;
reconsider g1 = (b1 (#) (b GeoSeq )) | (ok1 + 1) as XFinSequence of NAT by Th3;
A137: 1 - b <> 0 by A1;
dom ((b - 1) (#) (b GeoSeq )) = NAT by FUNCT_2:def 1;
then A138: o1 c= dom ((b - 1) (#) (b GeoSeq )) by ORDINAL1:def 2;
then A139: len do1 = len g1 by A129, A133, RELAT_1:91;
A140: dom g1 = o1 by A133, A138, RELAT_1:91;
A141: 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 13;
assume A142: i in dom do1 ; :: thesis: do1 . i <= g1 . i
then i in o1 by A77, A128, A122, AFINSQ_1:14;
then A143: g1 . I = ((b - 1) (#) (b GeoSeq )) . I by A140, FUNCT_1:70
.= (b - 1) * ((b GeoSeq ) . I) by SEQ_1:13
.= b1 * (b |^ I) by PREPOWER:def 1 ;
A144: dom do1 c= dom E by RELAT_1:89;
then e . i < b1 + 1 by A59, A60, A142;
then A145: e . i <= b1 by NAT_1:13;
do1 . i = E . i by A142, FUNCT_1:70
.= (e . i) * (b |^ i) by A61, A142, A144 ;
hence do1 . i <= g1 . i by A143, A145, XREAL_1:66; :: thesis: verum
end;
Sum g1 = (Partial_Sums ((b - 1) (#) (b GeoSeq ))) . ok1 by AFINSQ_2:68
.= ((b - 1) (#) (Partial_Sums (b GeoSeq ))) . ok1 by SERIES_1:12
.= (b - 1) * ((Partial_Sums (b GeoSeq )) . ok1) by SEQ_1:13
.= (b - 1) * ((1 - (b to_power (ok1 + 1))) / (1 - b)) by A1, SERIES_1:26
.= - ((1 - b) * ((1 - (b |^ o1)) / (1 - b))) by A133
.= - (1 - (b |^ o1)) by A137, XCMPLX_1:88
.= (b |^ o1) - 1 ;
then Sum do1 < ((b |^ o1) - 1) + 1 by A139, A141, AFINSQ_2:69, XREAL_1:147;
then A146: (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 A127, A129, FUNCT_1:70;
then E = do1 ^ d91 by A134, AFINSQ_1:def 4;
then A147: n = (Sum do1) + (Sum d91) by A62, AFINSQ_2:67;
bo1 <> 0 by A1, PREPOWER:12;
then (Sum d91) mod (b |^ o1) = 0 by A136, PEPIN:6;
then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by A147, NAT_D:19;
then A148: (n div (b |^ o1)) * (b |^ o1) = Sum d91 by A146, A136, NAT_D:3;
dom E = 1 + (dom d91) by A60, A77, A83, A127
.= (len <%(E . o)%>) + (len d91) by AFINSQ_1:38 ;
then E = <%(E . o)%> ^ d91 by A125, A131, AFINSQ_1:def 4;
then Sum E = (Sum <%(E . o)%>) + (Sum d91) by AFINSQ_2:67;
then E . o = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A124, A148, AFINSQ_2:65;
then (e . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A60, A61, A77, A78;
then (e . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * ((b |^ o) * (b |^ 1))) by NEWTON:13;
then (e . o) * (b |^ o) = (b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * (b |^ 1))) ;
then ((b |^ o) * (e . o)) / (b |^ o) = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o) by NEWTON:10;
hence d . a = e . a by A121, A110, XCMPLX_1:90; :: thesis: verum
end;
suppose A149: ( o > 0 & o = k ) ; :: thesis: d . b1 = e . b1
set d9 = <%(D . o)%>;
reconsider do = D | o as XFinSequence of NAT ;
A150: len d = len D by A41;
then A151: len do = o by A80, AFINSQ_1:14;
A153: len <%(D . o)%> = oo by A149, AFINSQ_1:38;
then A154: dom D = (len do) + (len <%(D . o)%>) by A41, A151;
A155: for x being Nat st x in dom <%(D . o)%> holds
D . ((len do) + x) = <%(D . o)%> . x
proof
let x be Nat; :: thesis: ( x in dom <%(D . o)%> implies D . ((len do) + x) = <%(D . o)%> . x )
assume x in dom <%(D . o)%> ; :: thesis: D . ((len do) + x) = <%(D . o)%> . x
then x < 1 by A149, A153, NAT_1:45;
then x = 0 by NAT_1:14;
hence D . ((len do) + x) = <%(D . o)%> . x by A151, AFINSQ_1:38; :: thesis: verum
end;
now
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 13;
assume A156: k in dom <%(D . o)%> ; :: thesis: b |^ o divides <%(D . o)%> . k
then k < len <%(D . o)%> by NAT_1:45;
then o + k < dom D by A151, A154, XREAL_1:10;
then o + k in dom D by NAT_1:45;
then D . (o + k) = (d . (o + k)) * (b |^ (o + k)) by A42;
then <%(D . o)%> . K = (d . (o + k)) * (b |^ (o + k)) by A151, A155, A156
.= (d . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:13
.= ((d . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides <%(D . o)%> . k by NAT_D:def 3; :: thesis: verum
end;
then A157: b |^ o divides Sum <%(D . o)%> by Th5;
reconsider bo = b |^ o as Element of NAT by ORDINAL1:def 13;
A158: 1 - b <> 0 by A1;
consider ok being Nat such that
A159: ok + 1 = o by A149, NAT_1:6;
reconsider ok = ok as Element of NAT by ORDINAL1:def 13;
reconsider g = (b1 (#) (b GeoSeq )) | (ok + 1) as XFinSequence of NAT by Th3;
A160: Sum g = (Partial_Sums ((b - 1) (#) (b GeoSeq ))) . ok by AFINSQ_2:68
.= ((b - 1) (#) (Partial_Sums (b GeoSeq ))) . ok by SERIES_1:12
.= (b - 1) * ((Partial_Sums (b GeoSeq )) . ok) by SEQ_1:13
.= (b - 1) * ((1 - (b to_power (ok + 1))) / (1 - b)) by A1, SERIES_1:26
.= - ((1 - b) * ((1 - (b |^ o)) / (1 - b))) by A159
.= - (1 - (b |^ o)) by A158, XCMPLX_1:88
.= (b |^ o) - 1 ;
consider ok being Nat such that
A161: ok + 1 = o by A149, NAT_1:6;
dom ((b - 1) (#) (b GeoSeq )) = NAT by FUNCT_2:def 1;
then A162: o c= dom ((b - 1) (#) (b GeoSeq )) by ORDINAL1:def 2;
then A163: dom g = o by A159, RELAT_1:91;
A164: for i being Nat st i in dom do holds
do . i <= g . i
proof
let i be Nat; :: thesis: ( i in dom do implies do . i <= g . i )
reconsider I = i as Element of NAT by ORDINAL1:def 13;
assume A165: i in dom do ; :: thesis: do . i <= g . i
then i in o by A80, A150, AFINSQ_1:14;
then A166: g . I = ((b - 1) (#) (b GeoSeq )) . I by A163, FUNCT_1:70
.= (b - 1) * ((b GeoSeq ) . I) by SEQ_1:13
.= b1 * (b |^ I) by PREPOWER:def 1 ;
A167: dom do c= dom D by RELAT_1:89;
then d . i < b1 + 1 by A40, A41, A165;
then A168: d . i <= b1 by NAT_1:13;
do . i = D . i by A165, FUNCT_1:70
.= (d . i) * (b |^ i) by A42, A165, A167 ;
hence do . i <= g . i by A166, A168, XREAL_1:66; :: thesis: verum
end;
len do = len g by A151, A159, A162, RELAT_1:91;
then Sum do < ((b |^ o) - 1) + 1 by A160, A164, AFINSQ_2:69, XREAL_1:147;
then A169: (Sum do) div (b |^ o) = 0 by NAT_D:27;
for x being Nat st x in dom do holds
D . x = do . x by FUNCT_1:70;
then D = do ^ <%(D . o)%> by A154, A155, AFINSQ_1:def 4;
then A170: n = (Sum do) + (Sum <%(D . o)%>) by A43, AFINSQ_2:67;
A171: bo <> 0 by A1, PREPOWER:12;
then (Sum <%(D . o)%>) mod (b |^ o) = 0 by A157, PEPIN:6;
then n div (b |^ o) = ((Sum <%(D . o)%>) div (b |^ o)) + ((Sum do) div (b |^ o)) by A170, NAT_D:19;
then (n div (b |^ o)) * (b |^ o) = Sum <%(D . o)%> by A169, A157, NAT_D:3;
then D . o = (n div (b |^ o)) * (b |^ o) by AFINSQ_2:65;
then ((d . o) * (b |^ o)) / (b |^ o) = ((n div (b |^ o)) * (b |^ o)) / (b |^ o) by A41, A42, A78;
then A172: d . o = ((n div (b |^ o)) * (b |^ o)) / (b |^ o) by A171, XCMPLX_1:90;
set d9 = <%(E . o)%>;
reconsider do = E | o as XFinSequence of NAT ;
A173: len e = len E by A60;
then A174: len do = o by A77, A80, AFINSQ_1:14;
A176: len <%(E . o)%> = oo by A149, AFINSQ_1:38;
then A177: dom E = (len do) + (len <%(E . o)%>) by A60, A77, A174;
A178: for x being Nat st x in dom <%(E . o)%> holds
E . ((len do) + x) = <%(E . o)%> . x
proof
let x be Nat; :: thesis: ( x in dom <%(E . o)%> implies E . ((len do) + x) = <%(E . o)%> . x )
assume x in dom <%(E . o)%> ; :: thesis: E . ((len do) + x) = <%(E . o)%> . x
then x < 1 by A149, A176, NAT_1:45;
then x = 0 by NAT_1:14;
hence E . ((len do) + x) = <%(E . o)%> . x by A174, AFINSQ_1:38; :: thesis: verum
end;
now
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 13;
assume A179: k in dom <%(E . o)%> ; :: thesis: b |^ o divides <%(E . o)%> . k
then k < len <%(E . o)%> by NAT_1:45;
then o + k < dom E by A174, A177, XREAL_1:10;
then o + k in dom E by NAT_1:45;
then E . (o + k) = (e . (o + k)) * (b |^ (o + k)) by A61;
then <%(E . o)%> . K = (e . (o + k)) * (b |^ (o + k)) by A174, A178, A179
.= (e . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:13
.= ((e . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides <%(E . o)%> . k by NAT_D:def 3; :: thesis: verum
end;
then A180: b |^ o divides Sum <%(E . o)%> by Th5;
reconsider ok = ok as Element of NAT by ORDINAL1:def 13;
reconsider g = (b1 (#) (b GeoSeq )) | (ok + 1) as XFinSequence of NAT by Th3;
reconsider bo = b |^ o as Element of NAT by ORDINAL1:def 13;
A181: 1 - b <> 0 by A1;
dom ((b - 1) (#) (b GeoSeq )) = NAT by FUNCT_2:def 1;
then A182: o c= dom ((b - 1) (#) (b GeoSeq )) by ORDINAL1:def 2;
then A183: len do = len g by A174, A161, RELAT_1:91;
A184: dom g = o by A161, A182, RELAT_1:91;
A185: for i being Nat st i in dom do holds
do . i <= g . i
proof
let i be Nat; :: thesis: ( i in dom do implies do . i <= g . i )
reconsider I = i as Element of NAT by ORDINAL1:def 13;
assume A186: i in dom do ; :: thesis: do . i <= g . i
then i in o by A77, A80, A173, AFINSQ_1:14;
then A187: g . I = ((b - 1) (#) (b GeoSeq )) . I by A184, FUNCT_1:70
.= (b - 1) * ((b GeoSeq ) . I) by SEQ_1:13
.= b1 * (b |^ I) by PREPOWER:def 1 ;
A188: dom do c= dom E by RELAT_1:89;
then e . i < b1 + 1 by A59, A60, A186;
then A189: e . i <= b1 by NAT_1:13;
do . i = E . i by A186, FUNCT_1:70
.= (e . i) * (b |^ i) by A61, A186, A188 ;
hence do . i <= g . i by A187, A189, XREAL_1:66; :: thesis: verum
end;
Sum g = (Partial_Sums ((b - 1) (#) (b GeoSeq ))) . ok by AFINSQ_2:68
.= ((b - 1) (#) (Partial_Sums (b GeoSeq ))) . ok by SERIES_1:12
.= (b - 1) * ((Partial_Sums (b GeoSeq )) . ok) by SEQ_1:13
.= (b - 1) * ((1 - (b to_power (ok + 1))) / (1 - b)) by A1, SERIES_1:26
.= - ((1 - b) * ((1 - (b |^ o)) / (1 - b))) by A161
.= - (1 - (b |^ o)) by A181, XCMPLX_1:88
.= (b |^ o) - 1 ;
then Sum do < ((b |^ o) - 1) + 1 by A183, A185, AFINSQ_2:69, XREAL_1:147;
then A190: (Sum do) div (b |^ o) = 0 by NAT_D:27;
for x being Nat st x in dom do holds
E . x = do . x by FUNCT_1:70;
then E = do ^ <%(E . o)%> by A177, A178, AFINSQ_1:def 4;
then A191: n = (Sum do) + (Sum <%(E . o)%>) by A62, AFINSQ_2:67;
A192: bo <> 0 by A1, PREPOWER:12;
then (Sum <%(E . o)%>) mod (b |^ o) = 0 by A180, PEPIN:6;
then n div (b |^ o) = ((Sum <%(E . o)%>) div (b |^ o)) + ((Sum do) div (b |^ o)) by A191, NAT_D:19;
then (n div (b |^ o)) * (b |^ o) = Sum <%(E . o)%> by A190, A180, NAT_D:3;
then E . o = (n div (b |^ o)) * (b |^ o) by AFINSQ_2:65;
then ((e . o) * (b |^ o)) / (b |^ o) = ((n div (b |^ o)) * (b |^ o)) / (b |^ o) by A60, A61, A77, A78;
hence d . a = e . a by A172, A192, XCMPLX_1:90; :: thesis: verum
end;
suppose A193: ( o > 0 & o < k ) ; :: thesis: d . b1 = e . b1
reconsider o1 = o + 1 as Element of NAT ;
A194: o1 <= k by A193, NAT_1:13;
then A195: o1 < len d by XREAL_1:149;
reconsider bo1 = b |^ o1 as Element of NAT by ORDINAL1:def 13;
reconsider do1 = D | o1 as XFinSequence of NAT ;
reconsider bo = b |^ o as Element of NAT by ORDINAL1:def 13;
defpred S1[ Nat, set ] means $2 = D . ($1 + o);
consider ok1 being Nat such that
A196: ok1 + 1 = o1 ;
reconsider ok1 = ok1 as Element of NAT by ORDINAL1:def 13;
reconsider g1 = (b1 (#) (b GeoSeq )) | (ok1 + 1) as XFinSequence of NAT by Th3;
A197: len d = len D by A41;
then A198: len do1 = o1 by A195, AFINSQ_1:14;
dom ((b - 1) (#) (b GeoSeq )) = NAT by FUNCT_2:def 1;
then A200: o1 c= dom ((b - 1) (#) (b GeoSeq )) by ORDINAL1:def 2;
then A201: len do1 = len g1 by A198, A196, RELAT_1:91;
A202: dom g1 = o1 by A196, A200, RELAT_1:91;
A203: 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 13;
assume A204: i in dom do1 ; :: thesis: do1 . i <= g1 . i
then i in o1 by A195, A197, AFINSQ_1:14;
then A205: g1 . I = ((b - 1) (#) (b GeoSeq )) . I by A202, FUNCT_1:70
.= (b - 1) * ((b GeoSeq ) . I) by SEQ_1:13
.= b1 * (b |^ I) by PREPOWER:def 1 ;
A206: dom do1 c= dom D by RELAT_1:89;
then d . i < b1 + 1 by A40, A41, A204;
then A207: d . i <= b1 by NAT_1:13;
do1 . i = D . i by A204, FUNCT_1:70
.= (d . i) * (b |^ i) by A42, A204, A206 ;
hence do1 . i <= g1 . i by A205, A207, XREAL_1:66; :: thesis: verum
end;
k < len d by XREAL_1:149;
then reconsider oo1 = (len d) - o1 as Element of NAT by A194, NAT_1:21, XXREAL_0:2;
A208: for u being Nat st u in oo holds
ex x being Element of NAT st S1[u,x] ;
consider d9 being XFinSequence of NAT such that
A209: ( dom d9 = oo & ( for x being Nat st x in oo holds
S1[x,d9 . x] ) ) from STIRL2_1:sch 5(A208);
A210: now
let k be Nat; :: thesis: ( k in dom <%(D . o)%> implies d9 . k = <%(D . o)%> . k )
assume k in dom <%(D . o)%> ; :: thesis: d9 . k = <%(D . o)%> . k
then k in 1 by AFINSQ_1:36;
then k < 1 by NAT_1:45;
then A211: k = 0 by NAT_1:14;
oo > 0 by A80, XREAL_1:52;
then k in dom d9 by A209, A211, NAT_1:45;
hence d9 . k = D . (k + o) by A209
.= <%(D . o)%> . k by A211, AFINSQ_1:def 5 ;
:: thesis: verum
end;
defpred S2[ Nat, set ] means $2 = D . ($1 + o1);
A212: for u being Nat st u in oo1 holds
ex x being Element of NAT st S2[u,x] ;
consider d91 being XFinSequence of NAT such that
A213: ( dom d91 = oo1 & ( for x being Nat st x in oo1 holds
S2[x,d91 . x] ) ) from STIRL2_1:sch 5(A212);
reconsider do = D | o as XFinSequence of NAT ;
A214: len d = len D by A41;
then A215: len do = o by A80, AFINSQ_1:14;
then A217: dom D = (len do) + (len d9) by A41, A209;
now
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 13;
assume A218: k in dom d9 ; :: thesis: b |^ o divides d9 . k
then k < len d9 by NAT_1:45;
then o + k < dom D by A215, A217, XREAL_1:10;
then o + k in dom D by NAT_1:45;
then D . (o + k) = (d . (o + k)) * (b |^ (o + k)) by A42;
then d9 . K = (d . (o + k)) * (b |^ (o + k)) by A209, A218
.= (d . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:13
.= ((d . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides d9 . k by NAT_D:def 3; :: thesis: verum
end;
then A219: b |^ o divides Sum d9 by Th5;
( ( for x being Nat st x in dom do holds
D . x = do . x ) & ( for x being Nat st x in dom d9 holds
D . ((len do) + x) = d9 . x ) ) by A209, A215, FUNCT_1:70;
then D = do ^ d9 by A217, AFINSQ_1:def 4;
then A220: n = (Sum do) + (Sum d9) by A43, AFINSQ_2:67;
consider ok being Nat such that
A221: ok + 1 = o by A193, NAT_1:6;
reconsider ok = ok as Element of NAT by ORDINAL1:def 13;
reconsider g = (b1 (#) (b GeoSeq )) | (ok + 1) as XFinSequence of NAT by Th3;
A222: 1 - b <> 0 by A1;
A223: Sum g = (Partial_Sums ((b - 1) (#) (b GeoSeq ))) . ok by AFINSQ_2:68
.= ((b - 1) (#) (Partial_Sums (b GeoSeq ))) . ok by SERIES_1:12
.= (b - 1) * ((Partial_Sums (b GeoSeq )) . ok) by SEQ_1:13
.= (b - 1) * ((1 - (b to_power (ok + 1))) / (1 - b)) by A1, SERIES_1:26
.= - ((1 - b) * ((1 - (b |^ o)) / (1 - b))) by A221
.= - (1 - (b |^ o)) by A222, XCMPLX_1:88
.= (b |^ o) - 1 ;
dom ((b - 1) (#) (b GeoSeq )) = NAT by FUNCT_2:def 1;
then A224: o c= dom ((b - 1) (#) (b GeoSeq )) by ORDINAL1:def 2;
then A225: dom g = o by A221, RELAT_1:91;
A226: for i being Nat st i in dom do holds
do . i <= g . i
proof
let i be Nat; :: thesis: ( i in dom do implies do . i <= g . i )
reconsider I = i as Element of NAT by ORDINAL1:def 13;
assume A227: i in dom do ; :: thesis: do . i <= g . i
then i in o by A80, A214, AFINSQ_1:14;
then A228: g . I = ((b - 1) (#) (b GeoSeq )) . I by A225, FUNCT_1:70
.= (b - 1) * ((b GeoSeq ) . I) by SEQ_1:13
.= b1 * (b |^ I) by PREPOWER:def 1 ;
A229: dom do c= dom D by RELAT_1:89;
then d . i < b1 + 1 by A40, A41, A227;
then A230: d . i <= b1 by NAT_1:13;
do . i = D . i by A227, FUNCT_1:70
.= (d . i) * (b |^ i) by A42, A227, A229 ;
hence do . i <= g . i by A228, A230, XREAL_1:66; :: thesis: verum
end;
A231: now
let k be Nat; :: thesis: ( k in dom d91 implies d9 . ((len <%(D . o)%>) + k) = d91 . k )
assume A232: k in dom d91 ; :: thesis: d9 . ((len <%(D . o)%>) + k) = d91 . k
then k < oo1 by A213, NAT_1:45;
then k + 1 < oo1 + 1 by XREAL_1:10;
then A233: k + 1 in dom d9 by A209, NAT_1:45;
thus d9 . ((len <%(D . o)%>) + k) = d9 . (1 + k) by AFINSQ_1:36
.= D . ((len do) + (k + 1)) by A209, A215, A233
.= D . ((len do1) + k) by A215, A198
.= d91 . k by A213, A198, A232 ; :: thesis: verum
end;
dom d9 = 1 + (dom d91) by A209, A213
.= (len <%(D . o)%>) + (len d91) by AFINSQ_1:38 ;
then d9 = <%(D . o)%> ^ d91 by A210, A231, AFINSQ_1:def 4;
then A234: Sum d9 = (Sum <%(D . o)%>) + (Sum d91) by AFINSQ_2:67;
defpred S3[ Nat, set ] means $2 = E . ($1 + o);
A235: 1 - b <> 0 by A1;
consider ok being Nat such that
A236: ok + 1 = o by A193, NAT_1:6;
A237: dom D = (len do1) + (len d91) by A41, A213, A198;
now
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 13;
assume A238: k in dom d91 ; :: thesis: b |^ o1 divides d91 . k
then k < len d91 by NAT_1:45;
then o1 + k < dom D by A198, A237, XREAL_1:10;
then o1 + k in dom D by NAT_1:45;
then D . (o1 + k) = (d . (o1 + k)) * (b |^ (o1 + k)) by A42;
then d91 . K = (d . (o1 + k)) * (b |^ (o1 + k)) by A213, A238
.= (d . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:13
.= ((d . (o1 + k)) * (b |^ k)) * (b |^ o1) ;
hence b |^ o1 divides d91 . k by NAT_D:def 3; :: thesis: verum
end;
then A239: b |^ o1 divides Sum d91 by Th5;
len do = len g by A215, A221, A224, RELAT_1:91;
then Sum do < ((b |^ o) - 1) + 1 by A223, A226, AFINSQ_2:69, XREAL_1:147;
then A240: (Sum do) div (b |^ o) = 0 by NAT_D:27;
A241: 1 - b <> 0 by A1;
Sum g1 = (Partial_Sums ((b - 1) (#) (b GeoSeq ))) . ok1 by AFINSQ_2:68
.= ((b - 1) (#) (Partial_Sums (b GeoSeq ))) . ok1 by SERIES_1:12
.= (b - 1) * ((Partial_Sums (b GeoSeq )) . ok1) by SEQ_1:13
.= (b - 1) * ((1 - (b to_power (ok1 + 1))) / (1 - b)) by A1, SERIES_1:26
.= - ((1 - b) * ((1 - (b |^ o1)) / (1 - b))) by A196
.= - (1 - (b |^ o1)) by A241, XCMPLX_1:88
.= (b |^ o1) - 1 ;
then Sum do1 < ((b |^ o1) - 1) + 1 by A201, A203, AFINSQ_2:69, XREAL_1:147;
then A242: (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 A213, A198, FUNCT_1:70;
then D = do1 ^ d91 by A237, AFINSQ_1:def 4;
then A243: n = (Sum do1) + (Sum d91) by A43, AFINSQ_2:67;
bo1 <> 0 by A1, PREPOWER:12;
then (Sum d91) mod (b |^ o1) = 0 by A239, PEPIN:6;
then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by A243, NAT_D:19;
then A244: (n div (b |^ o1)) * (b |^ o1) = Sum d91 by A242, A239, NAT_D:3;
A245: bo <> 0 by A1, PREPOWER:12;
then (Sum d9) mod (b |^ o) = 0 by A219, PEPIN:6;
then n div (b |^ o) = ((Sum d9) div (b |^ o)) + ((Sum do) div (b |^ o)) by A220, NAT_D:19;
then ( (n div (b |^ o)) * (b |^ o) = Sum d9 & Sum <%(D . o)%> = D . o ) by A240, A219, NAT_D:3, AFINSQ_2:65;
then (d . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A41, A42, A78, A244, A234;
then (d . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * ((b |^ o) * (b |^ 1))) by NEWTON:13;
then (d . o) * (b |^ o) = (b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * (b |^ 1))) ;
then ((b |^ o) * (d . o)) / (b |^ o) = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o) by NEWTON:10;
then A246: d . o = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o) by A245, XCMPLX_1:90;
reconsider o1 = o + 1 as Element of NAT ;
A247: o1 <= k by A193, NAT_1:13;
then A248: o1 < len d by XREAL_1:149;
reconsider ok = ok as Element of NAT by ORDINAL1:def 13;
reconsider g = (b1 (#) (b GeoSeq )) | (ok + 1) as XFinSequence of NAT by Th3;
A249: 1 - b <> 0 by A1;
reconsider bo1 = b |^ o1 as Element of NAT by ORDINAL1:def 13;
reconsider do1 = E | o1 as XFinSequence of NAT ;
reconsider bo = b |^ o as Element of NAT by ORDINAL1:def 13;
consider ok1 being Nat such that
A250: ok1 + 1 = o1 ;
reconsider ok1 = ok1 as Element of NAT by ORDINAL1:def 13;
reconsider g1 = (b1 (#) (b GeoSeq )) | (ok1 + 1) as XFinSequence of NAT by Th3;
A251: len e = len E by A60;
then A252: len do1 = o1 by A77, A248, AFINSQ_1:14;
dom ((b - 1) (#) (b GeoSeq )) = NAT by FUNCT_2:def 1;
then A254: o1 c= dom ((b - 1) (#) (b GeoSeq )) by ORDINAL1:def 2;
then A255: len do1 = len g1 by A252, A250, RELAT_1:91;
A256: dom g1 = o1 by A250, A254, RELAT_1:91;
A257: 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 13;
assume A258: i in dom do1 ; :: thesis: do1 . i <= g1 . i
then i in o1 by A77, A248, A251, AFINSQ_1:14;
then A259: g1 . I = ((b - 1) (#) (b GeoSeq )) . I by A256, FUNCT_1:70
.= (b - 1) * ((b GeoSeq ) . I) by SEQ_1:13
.= b1 * (b |^ I) by PREPOWER:def 1 ;
A260: dom do1 c= dom E by RELAT_1:89;
then e . i < b1 + 1 by A59, A60, A258;
then A261: e . i <= b1 by NAT_1:13;
do1 . i = E . i by A258, FUNCT_1:70
.= (e . i) * (b |^ i) by A61, A258, A260 ;
hence do1 . i <= g1 . i by A259, A261, XREAL_1:66; :: thesis: verum
end;
Sum g1 = (Partial_Sums ((b - 1) (#) (b GeoSeq ))) . ok1 by AFINSQ_2:68
.= ((b - 1) (#) (Partial_Sums (b GeoSeq ))) . ok1 by SERIES_1:12
.= (b - 1) * ((Partial_Sums (b GeoSeq )) . ok1) by SEQ_1:13
.= (b - 1) * ((1 - (b to_power (ok1 + 1))) / (1 - b)) by A1, SERIES_1:26
.= - ((1 - b) * ((1 - (b |^ o1)) / (1 - b))) by A250
.= - (1 - (b |^ o1)) by A249, XCMPLX_1:88
.= (b |^ o1) - 1 ;
then Sum do1 < ((b |^ o1) - 1) + 1 by A255, A257, AFINSQ_2:69, XREAL_1:147;
then A262: (Sum do1) div (b |^ o1) = 0 by NAT_D:27;
k < len d by XREAL_1:149;
then reconsider oo1 = (len d) - o1 as Element of NAT by A247, NAT_1:21, XXREAL_0:2;
A263: for u being Nat st u in oo holds
ex x being Element of NAT st S3[u,x] ;
consider d9 being XFinSequence of NAT such that
A264: ( dom d9 = oo & ( for x being Nat st x in oo holds
S3[x,d9 . x] ) ) from STIRL2_1:sch 5(A263);
A265: now
let k be Nat; :: thesis: ( k in dom <%(E . o)%> implies d9 . k = <%(E . o)%> . k )
assume k in dom <%(E . o)%> ; :: thesis: d9 . k = <%(E . o)%> . k
then k in 1 by AFINSQ_1:36;
then k < 1 by NAT_1:45;
then A266: k = 0 by NAT_1:14;
oo > 0 by A80, XREAL_1:52;
then k in dom d9 by A264, A266, NAT_1:45;
hence d9 . k = E . (k + o) by A264
.= <%(E . o)%> . k by A266, AFINSQ_1:def 5 ;
:: thesis: verum
end;
defpred S4[ Nat, set ] means $2 = E . ($1 + o1);
A267: for u being Nat st u in oo1 holds
ex x being Element of NAT st S4[u,x] ;
consider d91 being XFinSequence of NAT such that
A268: ( dom d91 = oo1 & ( for x being Nat st x in oo1 holds
S4[x,d91 . x] ) ) from STIRL2_1:sch 5(A267);
A269: dom E = (len do1) + (len d91) by A60, A77, A268, A252;
now
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 13;
assume A270: k in dom d91 ; :: thesis: b |^ o1 divides d91 . k
then k < len d91 by NAT_1:45;
then o1 + k < dom E by A252, A269, XREAL_1:10;
then o1 + k in dom E by NAT_1:45;
then E . (o1 + k) = (e . (o1 + k)) * (b |^ (o1 + k)) by A61;
then d91 . K = (e . (o1 + k)) * (b |^ (o1 + k)) by A268, A270
.= (e . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:13
.= ((e . (o1 + k)) * (b |^ k)) * (b |^ o1) ;
hence b |^ o1 divides d91 . k by NAT_D:def 3; :: thesis: verum
end;
then A271: b |^ o1 divides Sum d91 by Th5;
( ( 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 A268, A252, FUNCT_1:70;
then E = do1 ^ d91 by A269, AFINSQ_1:def 4;
then A272: n = (Sum do1) + (Sum d91) by A62, AFINSQ_2:67;
bo1 <> 0 by A1, PREPOWER:12;
then (Sum d91) mod (b |^ o1) = 0 by A271, PEPIN:6;
then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by A272, NAT_D:19;
then A273: (n div (b |^ o1)) * (b |^ o1) = Sum d91 by A262, A271, NAT_D:3;
reconsider do = E | o as XFinSequence of NAT ;
A274: len e = len E by A60;
then A275: len do = o by A77, A80, AFINSQ_1:14;
then A277: dom E = (len do) + (len d9) by A60, A77, A264;
now
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 13;
assume A278: k in dom d9 ; :: thesis: b |^ o divides d9 . k
then k < len d9 by NAT_1:45;
then o + k < dom E by A275, A277, XREAL_1:10;
then o + k in dom E by NAT_1:45;
then E . (o + k) = (e . (o + k)) * (b |^ (o + k)) by A61;
then d9 . K = (e . (o + k)) * (b |^ (o + k)) by A264, A278
.= (e . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:13
.= ((e . (o + k)) * (b |^ k)) * (b |^ o) ;
hence b |^ o divides d9 . k by NAT_D:def 3; :: thesis: verum
end;
then A279: b |^ o divides Sum d9 by Th5;
dom ((b - 1) (#) (b GeoSeq )) = NAT by FUNCT_2:def 1;
then A280: o c= dom ((b - 1) (#) (b GeoSeq )) by ORDINAL1:def 2;
then A281: len do = len g by A275, A236, RELAT_1:91;
A282: dom g = o by A236, A280, RELAT_1:91;
A283: for i being Nat st i in dom do holds
do . i <= g . i
proof
let i be Nat; :: thesis: ( i in dom do implies do . i <= g . i )
reconsider I = i as Element of NAT by ORDINAL1:def 13;
assume A284: i in dom do ; :: thesis: do . i <= g . i
then i in o by A77, A80, A274, AFINSQ_1:14;
then A285: g . I = ((b - 1) (#) (b GeoSeq )) . I by A282, FUNCT_1:70
.= (b - 1) * ((b GeoSeq ) . I) by SEQ_1:13
.= b1 * (b |^ I) by PREPOWER:def 1 ;
A286: dom do c= dom E by RELAT_1:89;
then e . i < b1 + 1 by A59, A60, A284;
then A287: e . i <= b1 by NAT_1:13;
do . i = E . i by A284, FUNCT_1:70
.= (e . i) * (b |^ i) by A61, A284, A286 ;
hence do . i <= g . i by A285, A287, XREAL_1:66; :: thesis: verum
end;
Sum g = (Partial_Sums ((b - 1) (#) (b GeoSeq ))) . ok by AFINSQ_2:68
.= ((b - 1) (#) (Partial_Sums (b GeoSeq ))) . ok by SERIES_1:12
.= (b - 1) * ((Partial_Sums (b GeoSeq )) . ok) by SEQ_1:13
.= (b - 1) * ((1 - (b to_power (ok + 1))) / (1 - b)) by A1, SERIES_1:26
.= - ((1 - b) * ((1 - (b |^ o)) / (1 - b))) by A236
.= - (1 - (b |^ o)) by A235, XCMPLX_1:88
.= (b |^ o) - 1 ;
then Sum do < ((b |^ o) - 1) + 1 by A281, A283, AFINSQ_2:69, XREAL_1:147;
then A288: (Sum do) div (b |^ o) = 0 by NAT_D:27;
A289: now
let k be Nat; :: thesis: ( k in dom d91 implies d9 . ((len <%(E . o)%>) + k) = d91 . k )
assume A290: k in dom d91 ; :: thesis: d9 . ((len <%(E . o)%>) + k) = d91 . k
then k < oo1 by A268, NAT_1:45;
then k + 1 < oo1 + 1 by XREAL_1:10;
then A291: k + 1 in oo by NAT_1:45;
thus d9 . ((len <%(E . o)%>) + k) = d9 . (1 + k) by AFINSQ_1:36
.= E . ((len do) + (k + 1)) by A264, A275, A291
.= E . ((len do1) + k) by A275, A252
.= d91 . k by A268, A252, A290 ; :: thesis: verum
end;
dom d9 = 1 + (dom d91) by A264, A268
.= (len <%(E . o)%>) + (len d91) by AFINSQ_1:38 ;
then d9 = <%(E . o)%> ^ d91 by A265, A289, AFINSQ_1:def 4;
then A292: Sum d9 = (Sum <%(E . o)%>) + (Sum d91) by AFINSQ_2:67;
( ( for x being Nat st x in dom do holds
E . x = do . x ) & ( for x being Nat st x in dom d9 holds
E . ((len do) + x) = d9 . x ) ) by A264, A275, FUNCT_1:70;
then E = do ^ d9 by A277, AFINSQ_1:def 4;
then A293: n = (Sum do) + (Sum d9) by A62, AFINSQ_2:67;
A294: bo <> 0 by A1, PREPOWER:12;
then (Sum d9) mod (b |^ o) = 0 by A279, PEPIN:6;
then n div (b |^ o) = ((Sum d9) div (b |^ o)) + ((Sum do) div (b |^ o)) by A293, NAT_D:19;
then (n div (b |^ o)) * (b |^ o) = Sum d9 by A288, A279, NAT_D:3;
then E . o = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A273, A292, AFINSQ_2:65;
then (e . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A60, A61, A77, A78;
then (e . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * ((b |^ o) * (b |^ 1))) by NEWTON:13;
then (e . o) * (b |^ o) = (b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * (b |^ 1))) ;
then ((b |^ o) * (e . o)) / (b |^ o) = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o) by NEWTON:10;
hence d . a = e . a by A246, A294, XCMPLX_1:90; :: thesis: verum
end;
end;
end;
hence d = e by A77, FUNCT_1:9; :: thesis: verum
end;
assume that
n = 0 and
A295: ( d = <%0 %> & e = <%0 %> ) ; :: thesis: d = e
thus d = e by A295; :: thesis: verum