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