let n be Nat; :: thesis: ( n is prime implies Euler n = n - 1 )

set X = { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } ;

{ kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } c= Seg n

assume A1: n is prime ; :: thesis: Euler n = n - 1

n <> 0

then A2: 0 in n by AXIOMS:4;

(Segm n) \ {0} c= X

A6: Euler n <= n - 1 by A1, Th19, INT_2:def 4;

( card n = n & card {0} = 1 ) by CARD_1:30;

then n - 1 <= Euler n by A5, A2, Th4;

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

set X = { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } ;

{ kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } c= Seg n

proof

then reconsider X = { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } as finite set ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } or x in Seg n )

assume x in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } ; :: thesis: x in Seg n

then ex k being Element of NAT st

( k = x & n,k are_coprime & k >= 1 & k <= n ) ;

hence x in Seg n by FINSEQ_1:1; :: thesis: verum

end;assume x in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } ; :: thesis: x in Seg n

then ex k being Element of NAT st

( k = x & n,k are_coprime & k >= 1 & k <= n ) ;

hence x in Seg n by FINSEQ_1:1; :: thesis: verum

assume A1: n is prime ; :: thesis: Euler n = n - 1

n <> 0

proof

then
0 in { l where l is Nat : l < n }
;
assume
n = 0
; :: thesis: contradiction

then n in SetPrimenumber 2 by A1, NEWTON:def 7;

hence contradiction ; :: thesis: verum

end;then n in SetPrimenumber 2 by A1, NEWTON:def 7;

hence contradiction ; :: thesis: verum

then A2: 0 in n by AXIOMS:4;

(Segm n) \ {0} c= X

proof

then A5:
card (n \ {0}) <= card X
by NAT_1:43;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Segm n) \ {0} or x in X )

assume A3: x in (Segm n) \ {0} ; :: thesis: x in X

then A4: x in Segm n by XBOOLE_0:def 5;

not x in {0} by A3, XBOOLE_0:def 5;

hence x in X by A1, Th3, A4; :: thesis: verum

end;assume A3: x in (Segm n) \ {0} ; :: thesis: x in X

then A4: x in Segm n by XBOOLE_0:def 5;

not x in {0} by A3, XBOOLE_0:def 5;

hence x in X by A1, Th3, A4; :: thesis: verum

A6: Euler n <= n - 1 by A1, Th19, INT_2:def 4;

( card n = n & card {0} = 1 ) by CARD_1:30;

then n - 1 <= Euler n by A5, A2, Th4;

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