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
proof
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;
then reconsider X = { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } as finite set ;
assume A1: n is prime ; :: thesis: Euler n = n - 1
n <> 0
proof
assume n = 0 ; :: thesis: contradiction
then n in SetPrimenumber 2 by ;
hence contradiction ; :: thesis: verum
end;
then 0 in { l where l is Nat : l < n } ;
then A2: 0 in n by AXIOMS:4;
(Segm n) \ c= X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Segm n) \ or x in X )
assume A3: x in (Segm n) \ ; :: thesis: x in X
then A4: x in Segm n by XBOOLE_0:def 5;
not x in by ;
hence x in X by A1, Th3, A4; :: thesis: verum
end;
then A5: card (n \ ) <= card X by NAT_1:43;
A6: Euler n <= n - 1 by ;
( card n = n & card = 1 ) by CARD_1:30;
then n - 1 <= Euler n by A5, A2, Th4;
hence Euler n = n - 1 by ; :: thesis: verum