A1: ( 2 divides u iff |.2.| divides |.u.| ) by INT_2:16;
A2: ( |.u.| is odd implies |.u.| |^ k is odd ) by PEPIN:20;
|.(u |^ k).| = |.u.| |^ k by TAYLOR_2:1;
hence not u |^ k is even by A1, A2, INT_2:16; :: thesis: verum