let i be Integer; :: thesis: (((2 * i) + 1) ^2) mod 8 = 1

per cases ( (2 * i) + 1 >= 0 or (2 * i) + 1 < 0 ) ;

suppose (2 * i) + 1 >= 0 ; :: thesis: (((2 * i) + 1) ^2) mod 8 = 1

then (2 * i) + 1 in NAT by INT_1:3;
hence (((2 * i) + 1) ^2) mod 8 = 1 by NUMBER05:41; :: thesis: verum

end;

suppose (2 * i) + 1 < 0 ; :: thesis: (((2 * i) + 1) ^2) mod 8 = 1

then A1: - ((2 * i) + 1) in NAT by INT_1:3;
((2 * i) + 1) ^2 = (- ((2 * i) + 1)) ^2 ;
hence (((2 * i) + 1) ^2) mod 8 = 1 by A1, NUMBER05:41; :: thesis: verum

end;

end;