let x be Integer; :: thesis: ( not x - 3 divides (x |^ 3) - 3 or x = - 21 or x = - 9 or x = - 5 or x = - 3 or x = - 1 or x = 0 or x = 1 or x = 2 or x = 4 or x = 5 or x = 6 or x = 7 or x = 9 or x = 11 or x = 15 or x = 27 )
assume x: x - 3 divides (x |^ 3) - 3 ; :: thesis: ( x = - 21 or x = - 9 or x = - 5 or x = - 3 or x = - 1 or x = 0 or x = 1 or x = 2 or x = 4 or x = 5 or x = 6 or x = 7 or x = 9 or x = 11 or x = 15 or x = 27 )
set t = x - 3;
e: (((x - 3) + 3) |^ (2 + 1)) - 3 = ((((x - 3) + 3) |^ (1 + 1)) * ((x - 3) + 3)) - 3 by NEWTON:6
.= (((((x - 3) + 3) |^ 1) * ((x - 3) + 3)) * ((x - 3) + 3)) - 3 by NEWTON:6
.= ((((x - 3) + 3) * ((x - 3) + 3)) * ((x - 3) + 3)) - 3 by NEWTON:5
.= (((((x - 3) * (x - 3)) * (x - 3)) + (27 * (x - 3))) + ((9 * (x - 3)) * (x - 3))) + 24 ;
t: ( x - 3 divides ((x - 3) * (x - 3)) * (x - 3) & x - 3 divides 27 * (x - 3) & x - 3 divides (9 * (x - 3)) * (x - 3) ) by INT_1:def 3;
then x - 3 divides (((x - 3) * (x - 3)) * (x - 3)) + (27 * (x - 3)) by WSIERP_1:4;
then x - 3 divides ((((x - 3) * (x - 3)) * (x - 3)) + (27 * (x - 3))) + ((9 * (x - 3)) * (x - 3)) by t, WSIERP_1:4;
then x - 3 divides 24 by x, e, INT_2:1;
then ( x - 3 = - 1 or x - 3 = 1 or x - 3 = - 2 or x - 3 = 2 or x - 3 = - 3 or x - 3 = 3 or x - 3 = - 4 or x - 3 = 4 or x - 3 = - 6 or x - 3 = 6 or x - 3 = - 8 or x - 3 = 8 or x - 3 = - 12 or x - 3 = 12 or x - 3 = - 24 or x - 3 = 24 ) by lem24;
hence ( x = - 21 or x = - 9 or x = - 5 or x = - 3 or x = - 1 or x = 0 or x = 1 or x = 2 or x = 4 or x = 5 or x = 6 or x = 7 or x = 9 or x = 11 or x = 15 or x = 27 ) ; :: thesis: verum