let n be Nat; :: thesis: ( n <> 0 implies Euler n <> 0 )
assume A1: n <> 0 ; :: thesis: Euler n <> 0
set X = { k where k is Element of NAT : ( n,k are_coprime & k >= 1 & k <= n ) } ;
A2: { k where k is Element of NAT : ( n,k are_coprime & k >= 1 & k <= n ) } c= finSeg n
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : ( n,k are_coprime & k >= 1 & k <= n ) } or x in finSeg n )
assume x in { k where k is Element of NAT : ( n,k are_coprime & k >= 1 & k <= n ) } ; :: thesis: x in finSeg n
then ex xx being Element of NAT st
( x = xx & n,xx are_coprime & xx >= 1 & xx <= n ) ;
hence x in finSeg n by FINSEQ_1:1; :: thesis: verum
end;
assume Euler n = 0 ; :: thesis: contradiction
then A3: card { k where k is Element of NAT : ( n,k are_coprime & k >= 1 & k <= n ) } = 0 by EULER_1:def 1;
reconsider X = { k where k is Element of NAT : ( n,k are_coprime & k >= 1 & k <= n ) } as finite set by A2;
ex k being Nat st k in X
proof
take 1 ; :: thesis: 1 in X
n gcd 1 = 1 by NEWTON:51;
then A4: n,1 are_coprime by INT_2:def 3;
1 <= n by A1, NAT_1:14;
hence 1 in X by A4; :: thesis: verum
end;
hence contradiction by A3; :: thesis: verum