let a, e be Nat; :: thesis: for n, r, s, k being Integer st a |^ e,r are_congruent_mod n & r * r = (k * n) + s holds
a |^ (e + e),s are_congruent_mod n
let n, r, s, k be Integer; :: thesis: ( a |^ e,r are_congruent_mod n & r * r = (k * n) + s implies a |^ (e + e),s are_congruent_mod n )
assume that
A1: a |^ e,r are_congruent_mod n and
A2: r * r = (k * n) + s ; :: thesis: a |^ (e + e),s are_congruent_mod n
(a |^ e) * (a |^ e),r * r are_congruent_mod n by A1, INT_1:18;
then A3: a |^ (e + e),r * r are_congruent_mod n by NEWTON:8;
r * r,s are_congruent_mod n by A2;
hence a |^ (e + e),s are_congruent_mod n by A3, INT_1:15; :: thesis: verum