theorem Th26: :: NUMBER03:26
for a, b, i being Nat st a <> 0 & b <> 0 & i <> 0 holds
((i |^ a) - 1) gcd ((i |^ b) - 1) = (i |^ (a gcd b)) - 1