let a, b, i be Nat; :: thesis: ( a <> 0 & b <> 0 & i <> 0 implies ((i |^ a) - 1) gcd ((i |^ b) - 1) = (i |^ (a gcd b)) - 1 )
set d = a gcd b;
assume that
A1: ( a <> 0 & b <> 0 ) and
A2: i <> 0 ; :: thesis: ((i |^ a) - 1) gcd ((i |^ b) - 1) = (i |^ (a gcd b)) - 1
1 <= i by A2, NAT_1:14;

per cases then ( i = 1 or 1 < i ) by XXREAL_0:1;

suppose A3: i = 1 ; :: thesis: ((i |^ a) - 1) gcd ((i |^ b) - 1) = (i |^ (a gcd b)) - 1

then ((i |^ a) - 1) gcd ((i |^ b) - 1) = 0 gcd ((1 |^ b) - 1)
.= (i |^ (a gcd b)) - 1 by A3 ;
hence ((i |^ a) - 1) gcd ((i |^ b) - 1) = (i |^ (a gcd b)) - 1 ; :: thesis: verum

end;

suppose A4: 1 < i ; :: thesis: ((i |^ a) - 1) gcd ((i |^ b) - 1) = (i |^ (a gcd b)) - 1

consider A, B being Nat such that
A5: a = (a gcd b) * A and
A6: b = (a gcd b) * B and
A7: A,B are_coprime by A1, Th18;
( A <> 0 & B <> 0 ) by A1, A5, A6;
then reconsider a1 = A - 1, b1 = B - 1 as Nat ;
set x = i |^ (a gcd b);
set P = Partial_Sums ((i |^ (a gcd b)) GeoSeq);
( A = a1 + 1 & B = b1 + 1 ) ;
then (Partial_Sums ((i |^ (a gcd b)) GeoSeq)) . a1,(Partial_Sums ((i |^ (a gcd b)) GeoSeq)) . b1 are_coprime by A7, Th25;
then A8: ((i |^ (a gcd b)) - 1) * (((Partial_Sums ((i |^ (a gcd b)) GeoSeq)) . a1) gcd ((Partial_Sums ((i |^ (a gcd b)) GeoSeq)) . b1)) = (i |^ (a gcd b)) - 1 ;
A9: 1 <= a gcd b by A1, NAT_1:14;
1 + 1 <= i by A4, NAT_1:13;
then A10: i |^ (a gcd b) > a gcd b by NEWTON:86;
then A11: (i |^ (a gcd b)) - 1 <> 1 - 1 by A9;
A12: |.((i |^ (a gcd b)) - 1).| = (i |^ (a gcd b)) - 1 by A4, ABSVALUE:def 1;
(Partial_Sums ((i |^ (a gcd b)) GeoSeq)) . a1 = (1 - ((i |^ (a gcd b)) to_power (a1 + 1))) / (1 - (i |^ (a gcd b))) by A9, A10, SERIES_1:22
.= (- (1 - ((i |^ (a gcd b)) to_power (a1 + 1)))) / (- (1 - (i |^ (a gcd b)))) by XCMPLX_1:191
.= (((i |^ (a gcd b)) to_power A) - 1) / ((i |^ (a gcd b)) - 1) ;
then A13: ((Partial_Sums ((i |^ (a gcd b)) GeoSeq)) . a1) * ((i |^ (a gcd b)) - 1) = ((i |^ (a gcd b)) |^ A) - 1 by A11, XCMPLX_1:87;
(Partial_Sums ((i |^ (a gcd b)) GeoSeq)) . b1 = (1 - ((i |^ (a gcd b)) to_power (b1 + 1))) / (1 - (i |^ (a gcd b))) by A9, A10, SERIES_1:22
.= (- (1 - ((i |^ (a gcd b)) to_power (b1 + 1)))) / (- (1 - (i |^ (a gcd b)))) by XCMPLX_1:191
.= (((i |^ (a gcd b)) to_power B) - 1) / ((i |^ (a gcd b)) - 1) ;
then A14: ((Partial_Sums ((i |^ (a gcd b)) GeoSeq)) . b1) * ((i |^ (a gcd b)) - 1) = ((i |^ (a gcd b)) |^ B) - 1 by A11, XCMPLX_1:87;
( i |^ a = (i |^ (a gcd b)) |^ A & i |^ b = (i |^ (a gcd b)) |^ B ) by A5, A6, NEWTON:9;
hence ((i |^ a) - 1) gcd ((i |^ b) - 1) = (i |^ (a gcd b)) - 1 by A8, A13, A14, A12, INT_6:16; :: thesis: verum

end;

end;