let a be Nat; :: thesis: for m being positive Integer
for f being XFinSequence of INT st a > 1 & len f = m - 1 & ( for i being Nat st i in dom f holds
f . i = (a |^ (i + 1)) - 1 ) holds
((a |^ m) - 1) div (a - 1) = (Sum f) + m
let m be positive Integer; :: thesis: for f being XFinSequence of INT st a > 1 & len f = m - 1 & ( for i being Nat st i in dom f holds
f . i = (a |^ (i + 1)) - 1 ) holds
((a |^ m) - 1) div (a - 1) = (Sum f) + m
let f be XFinSequence of INT ; :: thesis: ( a > 1 & len f = m - 1 & ( for i being Nat st i in dom f holds
f . i = (a |^ (i + 1)) - 1 ) implies ((a |^ m) - 1) div (a - 1) = (Sum f) + m )
assume f: ( a > 1 & len f = m - 1 & ( for i being Nat st i in dom f holds
f . i = (a |^ (i + 1)) - 1 ) ) ; :: thesis: ((a |^ m) - 1) div (a - 1) = (Sum f) + m
a: a - 1 <> 0 by f;
reconsider a1 = a - 1 as Nat by f, INT_1:74;
m >= 0 + 1 by INT_1:7;
then reconsider m0 = m as Nat by POLYFORM:3;
reconsider m1 = m0 - 1 as Nat by INT_1:74;
defpred S₁[ Nat] means for f being XFinSequence of INT st len f = $1 & ( for i being Nat st i in dom f holds
f . i = (a |^ (i + 1)) - 1 ) holds
((a |^ ($1 + 1)) - 1) div (a - 1) = (Sum f) + ($1 + 1);
z: S₁[ 0 ]

proof

let f0 be XFinSequence of INT ; :: thesis: ( len f0 = 0 & ( for i being Nat st i in dom f0 holds
f0 . i = (a |^ (i + 1)) - 1 ) implies ((a |^ (0 + 1)) - 1) div (a - 1) = (Sum f0) + (0 + 1) )
assume f0: ( len f0 = 0 & ( for i being Nat st i in dom f0 holds
f0 . i = (a |^ (i + 1)) - 1 ) ) ; :: thesis: ((a |^ (0 + 1)) - 1) div (a - 1) = (Sum f0) + (0 + 1)
f0 = {} by f0;
then sz: Sum f0 = 0 ;
thus ((a |^ (0 + 1)) - 1) div (a - 1) = (a - 1) div (a - 1) by NEWTON:5
.= (Sum f0) + (0 + 1) by sz, a, INT_1:49 ; :: thesis: verum

end;

k: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume pk: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

let f1 be XFinSequence of INT ; :: thesis: ( len f1 = k + 1 & ( for i being Nat st i in dom f1 holds
f1 . i = (a |^ (i + 1)) - 1 ) implies ((a |^ ((k + 1) + 1)) - 1) div (a - 1) = (Sum f1) + ((k + 1) + 1) )
assume f1: ( len f1 = k + 1 & ( for i being Nat st i in dom f1 holds
f1 . i = (a |^ (i + 1)) - 1 ) ) ; :: thesis: ((a |^ ((k + 1) + 1)) - 1) div (a - 1) = (Sum f1) + ((k + 1) + 1)
set fk = f1 | k;
km: k < k + 1 by NAT_1:13;
then df: dom (f1 | k) = k by f1, AFINSQ_1:11;
( k in Segm (k + 1) & dom f1 = k + 1 ) by f1, km, NAT_1:44;
then kd: k in dom f1 ;
lek: len (f1 | k) = k by km, f1, AFINSQ_1:54;

now :: thesis: for i being Nat st i in dom (f1 | k) holds
(f1 | k) . i = (a |^ (i + 1)) - 1

let i be Nat; :: thesis: ( i in dom (f1 | k) implies (f1 | k) . i = (a |^ (i + 1)) - 1 )
assume idk: i in dom (f1 | k) ; :: thesis: (f1 | k) . i = (a |^ (i + 1)) - 1
dom (f1 | k) c= dom f1 by RELAT_1:60;
then idf: i in dom f1 by idk;
thus (f1 | k) . i = f1 . i by df, km, idk, f1, AFINSQ_1:53
.= (a |^ (i + 1)) - 1 by f1, idf ; :: thesis: verum

end;

then pek: ((a |^ (k + 1)) - 1) div (a - 1) = (Sum (f1 | k)) + (k + 1) by pk, lek;
sf: Sum <%(f1 . k)%> = f1 . k by AFINSQ_2:53;
f1 = (f1 | k) ^ <%(f1 . k)%> by f1, AFINSQ_1:56;
then ss: Sum f1 = (Sum (f1 | k)) + (f1 . k) by sf, AFINSQ_2:55;
ld: ( a - 1 divides (a |^ ((k + 1) + 1)) - 1 & a - 1 divides (a |^ (k + 1)) - 1 ) by lemdiv;
hence ((a |^ ((k + 1) + 1)) - 1) div (a - 1) = ((a |^ ((k + 1) + 1)) - 1) / a1 by RING_3:6
.= (((((a |^ (k + 1)) * a) + (a |^ (k + 1))) - (a |^ (k + 1))) - 1) / a1 by NEWTON:6
.= (((a |^ (k + 1)) * (a - 1)) + ((a |^ (k + 1)) - 1)) / a1
.= (((a |^ (k + 1)) * (a - 1)) / a1) + (((a |^ (k + 1)) - 1) / a1) by XCMPLX_1:62
.= (a |^ (k + 1)) + (((a |^ (k + 1)) - 1) / a1) by a, XCMPLX_1:89
.= (a |^ (k + 1)) + (((a |^ (k + 1)) - 1) div a1) by ld, RING_3:6
.= (((a |^ (k + 1)) - 1) + (Sum (f1 | k))) + ((k + 1) + 1) by pek
.= ((f1 . k) + (Sum (f1 | k))) + ((k + 1) + 1) by f1, kd
.= (Sum f1) + ((k + 1) + 1) by ss ;
:: thesis: verum

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(z, k);
then ((a |^ (m1 + 1)) - 1) div (a - 1) = (Sum f) + (m1 + 1) by f;
hence ((a |^ m) - 1) div (a - 1) = (Sum f) + m ; :: thesis: verum