let k, n be Nat; :: thesis: ( n <> 1 & n divides 2 |^ k & not n mod 4 = 0 implies n mod 4 = 2 )
assume ( n <> 1 & n divides 2 |^ k ) ; :: thesis: ( n mod 4 = 0 or n mod 4 = 2 )
then consider k being Element of NAT such that
A1: n = 2 * k by INT_2:28, PEPIN:32;
k = (2 * (k div 2)) + (k mod 2) by NAT_D:2;
then ( k = (2 * (k div 2)) + 0 or k = (2 * (k div 2)) + 1 ) by NAT_D:12;
then ( 2 * k = (4 * (k div 2)) + 0 or 2 * k = (4 * (k div 2)) + (2 * 1) ) ;
hence ( n mod 4 = 0 or n mod 4 = 2 ) by A1, NUMBER02:16; :: thesis: verum