let b, c be Nat; :: thesis: ( not 3 divides b implies not 3 divides (b |^ 2) + (c |^ 2) )
L1: ( not 3 divides b & not 3 divides c implies not 3 divides (b |^ 2) + (c |^ 2) )
proof
assume A0: ( not 3 divides b & not 3 divides c ) ; :: thesis: not 3 divides (b |^ 2) + (c |^ 2)
2 + 1 = 3 ;
then ( 3 divides (b |^ 2) - 1 & 3 divides (c |^ 2) - 1 ) by A0, Th59, PEPIN:41;
then A1: 3 divides ((b |^ 2) - 1) + ((c |^ 2) - 1) by WSIERP_1:4;
(b |^ 2) + (c |^ 2) = (((b |^ 2) + (c |^ 2)) - 2) + 2 ;
hence not 3 divides (b |^ 2) + (c |^ 2) by A1, INT_2:1, INT_2:27; :: thesis: verum
end;
( not 3 divides b & 3 divides c implies not 3 divides (b |^ 2) + (c |^ 2) )
proof
assume A1: ( not 3 divides b & 3 divides c ) ; :: thesis: not 3 divides (b |^ 2) + (c |^ 2)
c divides c |^ 2 by NAT_3:3;
then ( not 3 divides b |^ 2 & 3 divides c |^ 2 ) by INT_2:9, A1, NAT_3:5, PEPIN:41;
hence not 3 divides (b |^ 2) + (c |^ 2) by INT_2:1; :: thesis: verum
end;
hence ( not 3 divides b implies not 3 divides (b |^ 2) + (c |^ 2) ) by L1; :: thesis: verum