let n be Nat; :: thesis: ( n > 1 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 > 1 ; :: thesis: Euler n <= n - 1
then 0 in { l where l is Nat : l < n } ;
then 0 in n by AXIOMS:4;
then A2: card (n \ ) = (card n) - () by Th4;
A3: X c= n \
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in n \ )
assume x in X ; :: thesis: x in n \
then consider k being Element of NAT such that
A4: k = x and
A5: n,k are_coprime and
A6: k >= 1 and
A7: k <= n ;
not n,n are_coprime by ;
then k < n by ;
then k in { l where l is Nat : l < n } ;
then A8: k in n by AXIOMS:4;
not k in by ;
hence x in n \ by ; :: thesis: verum
end;
( card n = n & card = 1 ) by CARD_1:30;
hence Euler n <= n - 1 by ; :: thesis: verum