let n be Nat; :: thesis: ( (2 |^ n) mod 4 = 2 implies n = 1 )
assume A1: (2 |^ n) mod 4 = 2 ; :: thesis: n = 1
( n = 0 or n >= 0 + 1 ) by NAT_1:13;

per cases then ( n = 0 or n = 0 + 1 or n > 0 + 1 ) by XXREAL_0:1;

suppose n = 0 ; :: thesis: n = 1

then 2 |^ n = 1 by NEWTON:4;
hence n = 1 by A1, NAT_D:24; :: thesis: verum

end;

suppose n = 0 + 1 ; :: thesis: n = 1

hence n = 1 ; :: thesis: verum

end;

suppose n > 0 + 1 ; :: thesis: n = 1

then n >= 1 + 1 by NAT_1:13;
then 2 |^ 2 divides 2 |^ n by NEWTON:89;
hence n = 1 by A1, Lm3, INT_1:62; :: thesis: verum

end;

end;