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 that
A1: a,b are_congruent_mod n and
A2: n <> 0 ; :: thesis: a |^ x,b |^ x are_congruent_mod n
consider an being Nat such that
A3: an,a are_congruent_mod n by A2, Lm8;
b mod n >= 0 by A2, NAT_D:62;
then b mod n is Element of NAT by INT_1:3;
then consider nb being Nat such that
A4: nb = b mod n ;
reconsider ai = an as Integer ;
A5: ai,b are_congruent_mod n by A1, A3, INT_1:15;
reconsider bi = nb as Integer ;
b mod n = (b mod n) mod n by NAT_D:65;
then b,bi are_congruent_mod n by A2, A4, NAT_D:64;
then an,nb are_congruent_mod n by A5, INT_1:15;
then an |^ x,nb |^ x are_congruent_mod n by A2, Lm9;
then A6: (an |^ x) mod n = (nb |^ x) mod n by NAT_D:64;
A7: (b |^ x) mod n = ((b mod n) |^ x) mod n by Th30;
A8: (a |^ x) mod n = ((a mod n) |^ x) mod n by Th30;
an mod n = a mod n by A3, NAT_D:64;
then ((a mod n) |^ x) mod n = ((b mod n) |^ x) mod n by A4, A6, PEPIN:12;
hence a |^ x,b |^ x are_congruent_mod n by A2, A8, A7, NAT_D:64; :: thesis: verum