let a, b be odd Nat; :: thesis: ( a,b are_coprime & ((a |^ 2) + (b |^ 2)) / 2 is square implies not 3 divides a * b )
assume A1: a,b are_coprime ; :: thesis: ( not ((a |^ 2) + (b |^ 2)) / 2 is square or not 3 divides a * b )
assume A2: ((a |^ 2) + (b |^ 2)) / 2 is square ; :: thesis: not 3 divides a * b
then A3: (a |^ 2) mod 3 = (b |^ 2) mod 3 by ESS;
( a |^ 2,b |^ 2 are_coprime & not 3 is trivial ) by A1, WSIERP_1:11;
then A4: max (((a |^ 2) mod 3),((b |^ 2) mod 3)) > 0 by COM;
(a |^ 2) mod 3 is trivial by SM3;

per cases then ( (a |^ 2) mod 3 = 0 or (a |^ 2) mod 3 = 1 ) by NAT_2:def 1;

suppose (a |^ 2) mod 3 = 0 ; :: thesis: not 3 divides a * b

hence not 3 divides a * b by A3, A4; :: thesis: verum

end;

suppose B1: (a |^ 2) mod 3 = 1 ; :: thesis: not 3 divides a * b

then (b |^ 2) mod 3 = 1 by A2, ESS;
then B2: ( not 3 divides a |^ 2 & not 3 divides b |^ 2 ) by B1, INT_1:62;
( a divides a |^ 2 & b divides b |^ 2 ) by NAT_3:3;
then B3: ( not 3 divides a & not 3 divides b ) by B2, INT_2:9;
then ( a,3 are_coprime & b,3 are_coprime ) by PEPIN:41, GROUP_17:5;
hence not 3 divides a * b by B3, EULER_1:13; :: thesis: verum

end;

end;