let a, b, c be Nat; :: thesis: ( b,c are_coprime & (b |^ 2) + (c |^ 2) = a |^ 2 implies not 3 divides a )
( b,c are_coprime & (b |^ 2) + (c |^ 2) = a |^ 2 implies not 3 divides a |^ (1 + 1) ) by Th95;
hence ( b,c are_coprime & (b |^ 2) + (c |^ 2) = a |^ 2 implies not 3 divides a ) by Th96, PEPIN:41; :: thesis: verum