let a, b be Integer; :: thesis: for n, x being Nat st a,b are_congruent_mod n & n <> 0 holds
a |^ x,b |^ x are_congruent_mod n
let n, x be Nat; :: thesis: ( a,b are_congruent_mod n & n <> 0 implies a |^ x,b |^ x are_congruent_mod n )
assume A1: ( a,b are_congruent_mod n & n <> 0 ) ; :: thesis: a |^ x,b |^ x are_congruent_mod n
consider an being Nat such that
A2: an,a are_congruent_mod n by A1, Lmmod2;
reconsider ai = an as Integer ;
A4: an mod n = a mod n by A2, INT_3:12;
A5: ( (a |^ x) mod n = ((a mod n) |^ x) mod n & (b |^ x) mod n = ((b mod n) |^ x) mod n ) by INTPOW;
( b mod n is Integer & b mod n >= 0 ) by A1, INT_3:9;
then A6: b mod n is Element of NAT by INT_1:16;
A7: b mod n = (b mod n) mod n by INT_3:13;
consider nb being Nat such that
A8: nb = b mod n by A6;
reconsider bi = nb as Integer ;
A10: b,bi are_congruent_mod n by A1, A7, A8, INT_3:12;
ai,b are_congruent_mod n by A1, A2, INT_1:36;
then an,nb are_congruent_mod n by A10, INT_1:36;
then an |^ x,nb |^ x are_congruent_mod n by A1, Lmsm1;
then A11: (an |^ x) mod n = (nb |^ x) mod n by INT_3:12;
((a mod n) |^ x) mod n = ((b mod n) |^ x) mod n by A4, A8, A11, PEPIN:12;
hence a |^ x,b |^ x are_congruent_mod n by A1, INT_3:12, A5; :: thesis: verum