let n be Nat; :: thesis: ( n is prime implies Euler n = n - 1 )
assume A1: n is prime ; :: thesis: Euler n = n - 1
set X = { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } ;
{ kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } c= Seg n

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } or x in Seg n )
assume x in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } ; :: thesis: x in Seg n
then consider k being Element of NAT such that
A2: ( k = x & n,k are_relative_prime & k >= 1 & k <= n ) ;
thus x in Seg n by A2, FINSEQ_1:3; :: thesis: verum

end;

then reconsider X = { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } as finite set ;
A3: ( n < 1 or n = 1 or n > 1 ) by XXREAL_0:1;
A4: n <> 0

proof

assume n = 0 ; :: thesis: contradiction
then n in SetPrimenumber 2 by A1, NEWTON:def 7;
hence contradiction ; :: thesis: verum

end;

A5: Euler n <= n - 1 by A1, A3, Th20, INT_2:def 5;
n - 1 <= Euler n

proof

n \ {0 } c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in n \ {0 } or x in X )
assume x in n \ {0 } ; :: thesis: x in X
then A6: ( x in n & not x in {0 } ) by XBOOLE_0:def 5;
then x in { k where k is Element of NAT : k < n } by AXIOMS:30;
then ex k being Element of NAT st
( k = x & k < n ) ;
hence x in X by A1, A6, Th4; :: thesis: verum

end;

then A7: card (n \ {0 }) <= card X by NAT_1:44;
0 < n by A4;
then 0 in { l where l is Element of NAT : l < n } ;
then A8: 0 in n by AXIOMS:30;
( card n = n & card {0 } = 1 ) by CARD_1:50, CARD_1:def 5;
hence n - 1 <= Euler n by A7, A8, Th5; :: thesis: verum

end;

hence Euler n = n - 1 by A5, XXREAL_0:1; :: thesis: verum