let a, n, x, y be Nat; :: thesis: ( a,n are_coprime & a <> 0 & n <> 0 & x,y are_congruent_mod Euler n implies a |^ x,a |^ y are_congruent_mod n )
set e = Euler n;
assume that
A1: a,n are_coprime and
A2: a <> 0 and
A3: n <> 0 and
A4: x,y are_congruent_mod Euler n ; :: thesis: a |^ x,a |^ y are_congruent_mod n
A5: y,x are_congruent_mod Euler n by A4, INT_1:14;
n >= 1 + 0 by A3, NAT_1:13;

per cases then ( n = 1 or n > 1 ) by XXREAL_0:1;

suppose n = 1 ; :: thesis: a |^ x,a |^ y are_congruent_mod n

hence a |^ x,a |^ y are_congruent_mod n by INT_1:13; :: thesis: verum

end;

suppose A6: n > 1 ; :: thesis: a |^ x,a |^ y are_congruent_mod n

then A7: 1 mod n = 1 by NAT_D:24;
A8: (a |^ (Euler n)) mod n = 1 by A1, A2, A6, EULER_2:18;

per cases ( x >= y or x < y ) ;

suppose x >= y ; :: thesis: a |^ x,a |^ y are_congruent_mod n

then consider k being Nat such that
A9: x = (k * (Euler n)) + y by A3, A4, Th28;
A10: a |^ (k * (Euler n)) = (a |^ (Euler n)) |^ k by NEWTON:9;
A11: a |^ y,a |^ y are_congruent_mod n by INT_1:11;
(a |^ (Euler n)) |^ k,1 |^ k are_congruent_mod n by A3, A7, A8, GR_CY_3:34, NAT_D:64;
then (a |^ (k * (Euler n))) * (a |^ y),1 * (a |^ y) are_congruent_mod n by A10, A11, INT_1:18;
hence a |^ x,a |^ y are_congruent_mod n by A9, NEWTON:8; :: thesis: verum

end;

suppose x < y ; :: thesis: a |^ x,a |^ y are_congruent_mod n

then consider k being Nat such that
A12: y = (k * (Euler n)) + x by A3, A5, Th28;
A13: a |^ ((k * (Euler n)) + x) = (a |^ (k * (Euler n))) * (a |^ x) by NEWTON:8;
A14: a |^ (k * (Euler n)) = (a |^ (Euler n)) |^ k by NEWTON:9;
A15: a |^ x,a |^ x are_congruent_mod n by INT_1:11;
(a |^ (Euler n)) |^ k,1 |^ k are_congruent_mod n by A3, A7, A8, GR_CY_3:34, NAT_D:64;
then (a |^ (k * (Euler n))) * (a |^ x),1 * (a |^ x) are_congruent_mod n by A14, A15, INT_1:18;
hence a |^ x,a |^ y are_congruent_mod n by A12, A13, INT_1:14; :: thesis: verum

end;

end;

end;

end;