let a, m be Element of NAT ; :: thesis: ( a <> 0 & m > 1 & a,m are_relative_prime implies for b, x being Integer st ((a * x) - b) mod m = 0 holds
[x,(b * (a |^ ((Euler m) -' 1)))] in Cong m )
assume that
A1: a <> 0 and
A2: m > 1 and
A3: a,m are_relative_prime ; :: thesis: for b, x being Integer st ((a * x) - b) mod m = 0 holds
[x,(b * (a |^ ((Euler m) -' 1)))] in Cong m
let b, x be Integer; :: thesis: ( ((a * x) - b) mod m = 0 implies [x,(b * (a |^ ((Euler m) -' 1)))] in Cong m )
(a |^ (Euler m)) mod m = 1 by A1, A2, A3, EULER_2:33;
then a |^ (Euler m) = (m * ((a |^ (Euler m)) div m)) + 1 by A2, NAT_D:2;
then m divides (a |^ (Euler m)) - 1 by INT_1:def 9;
then a |^ (Euler m),1 are_congruent_mod m by INT_2:19;
then A4: (a |^ (Euler m)) * x,1 * x are_congruent_mod m by Th11;
Euler m <> 0

proof

set X = { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ;
1 gcd m = 1 by NEWTON:64;
then m,1 are_relative_prime by INT_2:def 4;
then A5: 1 in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } by A2;
assume Euler m = 0 ; :: thesis: contradiction
hence contradiction by A5; :: thesis: verum

end;

then A6: ((Euler m) -' 1) + 1 = ((Euler m) - 1) + 1 by NAT_1:14, XREAL_1:235
.= Euler m ;
assume ((a * x) - b) mod m = 0 ; :: thesis: [x,(b * (a |^ ((Euler m) -' 1)))] in Cong m
then m divides ((a * x) - b) - 0 by A2, INT_1:89;
then (a * x) - b, 0 are_congruent_mod m by INT_2:19;
then 0 ,(a * x) - b are_congruent_mod m by INT_1:35;
then (a |^ ((Euler m) -' 1)) * 0 ,(a |^ ((Euler m) -' 1)) * ((a * x) - b) are_congruent_mod m by Th11;
then 0 ,(((a |^ ((Euler m) -' 1)) * a) * x) - ((a |^ ((Euler m) -' 1)) * b) are_congruent_mod m ;
then 0 ,((a |^ (((Euler m) -' 1) + 1)) * x) - ((a |^ ((Euler m) -' 1)) * b) are_congruent_mod m by NEWTON:11;
then 0 + ((a |^ ((Euler m) -' 1)) * b),(a |^ (Euler m)) * x are_congruent_mod m by A6, INT_1:40;
then (a |^ ((Euler m) -' 1)) * b,x are_congruent_mod m by A4, INT_1:36;
then x,b * (a |^ ((Euler m) -' 1)) are_congruent_mod m by INT_1:35;
hence [x,(b * (a |^ ((Euler m) -' 1)))] in Cong m by Def1; :: thesis: verum