let m, n be Nat; :: thesis: ( m > 0 implies (n |^ m) mod n = 0 )
assume A1: m > 0 ; :: thesis: (n |^ m) mod n = 0
defpred S₁[ Nat] means ( $1 > 0 implies (n |^ $1) mod n = 0 );
A2: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume S₁[m] ; :: thesis: S₁[m + 1]
S₁[m + 1]

proof

reconsider m = m, n = n as Element of NAT by ORDINAL1:def 12;
(n * (n |^ m)) mod n = ((n mod n) * (n |^ m)) mod n by EULER_2:8
.= (0 * (n |^ m)) mod n by NAT_D:25
.= 0 by NAT_D:26 ;
hence S₁[m + 1] by NEWTON:6; :: thesis: verum

end;

hence S₁[m + 1] ; :: thesis: verum

end;

A3: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A2);
hence (n |^ m) mod n = 0 by A1; :: thesis: verum