let a, m be Nat; ( a <> 0 & m > 1 & a,m are_coprime implies a |^ (Euler m),1 are_congruent_mod m )
assume that
A1:
a <> 0
and
A2:
m > 1
and
A3:
a,m are_coprime
; a |^ (Euler m),1 are_congruent_mod m
(a |^ (Euler m)) mod m =
1
by A1, A2, A3, Th18
.=
1 mod m
by A2, NAT_D:14
;
hence
a |^ (Euler m),1 are_congruent_mod m
by A2, NAT_D:64; verum