let b be Nat; :: thesis: not 3 divides (((b |^ 3) + (b |^ 2)) - b) + 1
A0: ((b |^ 2) + 1) + ((b |^ 3) - b) = (((b |^ 3) + (b |^ 2)) - b) + 1 ;
not 3 divides (b |^ 2) + 1 by Th92;
hence not 3 divides (((b |^ 3) + (b |^ 2)) - b) + 1 by A0, PEPIN:41, Th58, INT_2:1; :: thesis: verum