let b, c be Nat; :: thesis: ( b,c are_coprime implies not 3 divides (b |^ 2) + (c |^ 2) )
assume A1: b,c are_coprime ; :: thesis: not 3 divides (b |^ 2) + (c |^ 2)
( 2 + 1 divides b implies not 2 + 1 divides c ) by A1, Th94;
hence not 3 divides (b |^ 2) + (c |^ 2) by Th91; :: thesis: verum