let i be Integer; :: thesis: ( i is odd implies (i ^2) mod 4 = 1 )
assume i is odd ; :: 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:12
.= 1 by NAT_D:24 ;
:: thesis: verum