let n, k be Nat; :: thesis: ( k > 1 implies not k divides (k + 1) |^ n )
assume k > 1 ; :: thesis: not k divides (k + 1) |^ n
then not k divides 1 |^ n by NAT_D:7;
hence not k divides (k + 1) |^ n by Th11; :: thesis: verum