let a, k, m, n be Nat; :: thesis: for i being Integer st m <= n & i |^ m,i |^ (m + k) are_congruent_mod a holds
i |^ n,i |^ (n + k) are_congruent_mod a
let i be Integer; :: thesis: ( m <= n & i |^ m,i |^ (m + k) are_congruent_mod a implies i |^ n,i |^ (n + k) are_congruent_mod a )
assume m <= n ; :: thesis: ( not i |^ m,i |^ (m + k) are_congruent_mod a or i |^ n,i |^ (n + k) are_congruent_mod a )
then consider x being Nat such that
A1: m + x = n by NAT_1:10;
( (i |^ m) * (i |^ x) = i |^ (m + x) & (i |^ (m + k)) * (i |^ x) = i |^ ((m + k) + x) ) by NEWTON:8;
hence ( not i |^ m,i |^ (m + k) are_congruent_mod a or i |^ n,i |^ (n + k) are_congruent_mod a ) by A1, INT_4:11; :: thesis: verum