let k be Integer; :: thesis: ( ex a, b being Integer st (a |^ 2) - (b |^ 2) = k iff k mod 4 <> 2 )
L1: ( ex a, b being Integer st (a |^ 2) - (b |^ 2) = k implies k mod 4 <> 2 )

proof

assume ex a, b being Integer st (a |^ 2) - (b |^ 2) = k ; :: thesis: k mod 4 <> 2
then consider a, b being Integer such that
A1: (a |^ 2) - (b |^ 2) = k ;
A2: (a - b) * (a + b) = k by A1, NEWTON01:1;
parity (a - b) = parity (a + b) by NEWTON05:53;
then ( ( a - b is odd & a + b is odd ) or ( a - b is even & a + b is even ) ) ;
then ( k is odd or 2 * 2 divides k ) by A2, NEWTON02:2;
then ( k mod (2 * 2) is odd or k mod (2 * 2) = 0 ) by INT_1:62;
hence k mod 4 <> 2 ; :: thesis: verum

end;

( k mod 4 <> 2 implies ex a, b being Integer st (a |^ 2) - (b |^ 2) = k )

proof

assume A1: k mod 4 <> 2 ; :: thesis: ex a, b being Integer st (a |^ 2) - (b |^ 2) = k
not not k mod (3 + 1) = 0 & ... & not k mod (3 + 1) = 3 by NUMBER03:11;

per cases then ( k mod 4 = 0 or k mod 4 = 1 or k mod 4 = 3 ) by A1;

suppose k mod 4 = 0 ; :: thesis: ex a, b being Integer st (a |^ 2) - (b |^ 2) = k

then 4 divides k by INT_1:62;
then reconsider m = k / 4 as Integer ;
((m + 1) |^ 2) - ((m - 1) |^ 2) = ((m + 1) + (m - 1)) * ((m + 1) - (m - 1)) by NEWTON01:1
.= 4 * m ;
hence ex a, b being Integer st (a |^ 2) - (b |^ 2) = k ; :: thesis: verum

end;

suppose ( k mod 4 = 1 or k mod 4 = 3 ) ; :: thesis: ex a, b being Integer st (a |^ 2) - (b |^ 2) = k

then ( k mod (2 * 2) = (2 * 0) + 1 or k mod (2 * 2) = (2 * 1) + 1 ) ;
then k is odd ;
then reconsider m = (k - 1) / 2 as Integer ;
((m + 1) |^ 2) - (m |^ 2) = ((m + 1) + m) * ((m + 1) - m) by NEWTON01:1
.= (2 * m) + 1 ;
hence ex a, b being Integer st (a |^ 2) - (b |^ 2) = k ; :: thesis: verum

end;

end;

end;

hence ( ex a, b being Integer st (a |^ 2) - (b |^ 2) = k iff k mod 4 <> 2 ) by L1; :: thesis: verum