per cases ( a >= 0 or a < 0 ) ;

suppose a >= 0 ; :: thesis: not 2 * a is square

then a in NAT by INT_1:3;
then reconsider a = a as odd Nat ;
A1: a,2 are_coprime by NEWTON03:def 5;
not (2 -root 2) |^ 2 is square by INT_2:28;
then A2: not 2 -root 2 in NAT ;
for c being Nat holds not 2 * a = c ^2

proof

assume ex c being Nat st 2 * a = c ^2 ; :: thesis: contradiction
then consider c being Nat such that
B1: 2 * a = c ^2 ;
2 * a = c |^ 2 by B1, NEWTON:81;
hence contradiction by A1, A2, NEWTON03:14; :: thesis: verum

end;

hence not 2 * a is square by PYTHTRIP:def 3; :: thesis: verum

end;

suppose a < 0 ; :: thesis: not 2 * a is square

hence not 2 * a is square ; :: thesis: verum

end;

end;