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

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 \ {0}) = (card n) - (card {0}) by Th4;

A3: X c= n \ {0}

hence Euler n <= n - 1 by A3, A2, NAT_1:43; :: 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 > 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 \ {0}) = (card n) - (card {0}) by Th4;

A3: X c= n \ {0}

proof

( card n = n & card {0} = 1 )
by CARD_1:30;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in n \ {0} )

assume x in X ; :: thesis: x in n \ {0}

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 A1, Th1;

then k < n by A5, A7, XXREAL_0:1;

then k in { l where l is Nat : l < n } ;

then A8: k in n by AXIOMS:4;

not k in {0} by A6, TARSKI:def 1;

hence x in n \ {0} by A4, A8, XBOOLE_0:def 5; :: thesis: verum

end;assume x in X ; :: thesis: x in n \ {0}

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 A1, Th1;

then k < n by A5, A7, XXREAL_0:1;

then k in { l where l is Nat : l < n } ;

then A8: k in n by AXIOMS:4;

not k in {0} by A6, TARSKI:def 1;

hence x in n \ {0} by A4, A8, XBOOLE_0:def 5; :: thesis: verum

hence Euler n <= n - 1 by A3, A2, NAT_1:43; :: thesis: verum