let a, c, k, m, n be Nat; :: thesis: for t1, t2 being Nat st 2 |^ k = (n * t1) + a & (((a * a) * a) * a) * (2 |^ m) = (n * t2) + c holds
2 |^ ((k * 4) + m),c are_congruent_mod n
let t1, t2 be Nat; :: thesis: ( 2 |^ k = (n * t1) + a & (((a * a) * a) * a) * (2 |^ m) = (n * t2) + c implies 2 |^ ((k * 4) + m),c are_congruent_mod n )
assume that
A1: 2 |^ k = (n * t1) + a and
A2: (((a * a) * a) * a) * (2 |^ m) = (n * t2) + c ; :: thesis: 2 |^ ((k * 4) + m),c are_congruent_mod n
2 |^ k,a are_congruent_mod n by A1;
hence 2 |^ ((k * 4) + m),c are_congruent_mod n by LemS, A2; :: thesis: verum