let a, m be Nat; :: thesis: ( m > 0 implies 2 * a divides (a |^ m) + (a |^ m) )
assume m > 0 ; :: thesis: 2 * a divides (a |^ m) + (a |^ m)
then a divides a |^ m by NAT_3:3;
then 2 * a divides 2 * (a |^ m) by NAT_3:1;
hence 2 * a divides (a |^ m) + (a |^ m) ; :: thesis: verum