let i be Integer; :: thesis: ( not i is even implies (i ^2 ) mod 4 = 1 )
assume not i is even ; :: thesis: (i ^2 ) mod 4 = 1
then consider i9 being Integer such that
A1: i = (2 * i9) + 1 by ABIAN:1;
i ^2 = (4 * ((i9 ^2 ) + i9)) + 1 by A1;
hence (i ^2 ) mod 4 = 1 mod 4 by EULER_1:13
.= 1 by NAT_D:24 ;
:: thesis: verum