let a be Integer; :: thesis: ( 3 divides a or (a |^ 3) mod 9 = 1 or (a |^ 3) mod 9 = 8 )
assume not 3 divides a ; :: thesis: ( (a |^ 3) mod 9 = 1 or (a |^ 3) mod 9 = 8 )
then a mod 3 <> 0 by INT_1:62;
then ( a mod 3 > 0 & a mod 3 < 3 ) by INT_1:57, INT_1:58;
then A1: ( a mod 3 > 0 & a mod 3 in Segm 3 ) by NAT_1:44;
set d = a div 3;

A2: now :: thesis: ( a mod 3 = 1 implies (a |^ 3) mod 9 = 1 )

assume a mod 3 = 1 ; :: thesis: (a |^ 3) mod 9 = 1
then a = ((a div 3) * 3) + 1 by INT_1:59;
then a |^ 3 = ((((3 * (a div 3)) |^ 3) + (3 * ((3 * (a div 3)) |^ 2))) + (3 * (3 * (a div 3)))) + 1 by SERIES_2:2
.= ((((3 |^ 3) * ((a div 3) |^ 3)) + (3 * ((3 * (a div 3)) |^ 2))) + (3 * (3 * (a div 3)))) + 1 by NEWTON:7
.= (((((3 * 3) * 3) * ((a div 3) |^ 3)) + (3 * ((3 * (a div 3)) |^ 2))) + (3 * (3 * (a div 3)))) + 1 by POLYEQ_3:27
.= (((((3 * 3) * 3) * ((a div 3) |^ 3)) + (3 * ((3 |^ 2) * ((a div 3) |^ 2)))) + (3 * (3 * (a div 3)))) + 1 by NEWTON:7
.= (((((3 * 3) * 3) * ((a div 3) |^ 3)) + (3 * ((3 * 3) * ((a div 3) |^ 2)))) + (3 * (3 * (a div 3)))) + 1 by WSIERP_1:1
.= (9 * (((3 * ((a div 3) |^ 3)) + (3 * ((a div 3) |^ 2))) + (a div 3))) + 1 ;
hence (a |^ 3) mod 9 = (((9 * (((3 * ((a div 3) |^ 3)) + (3 * ((a div 3) |^ 2))) + (a div 3))) mod 9) + (1 mod 9)) mod 9 by NAT_D:66
.= (0 + (1 mod 9)) mod 9 by NAT_D:71
.= 1 by NAT_D:63 ;
:: thesis: verum

end;

A3: now :: thesis: ( a mod 3 = 2 implies (a |^ 3) mod 9 = 8 )

assume a mod 3 = 2 ; :: thesis: (a |^ 3) mod 9 = 8
then a = ((a div 3) * 3) + 2 by INT_1:59;
then a |^ 3 = ((((3 * (a div 3)) |^ 3) + ((3 * ((3 * (a div 3)) |^ 2)) * 2)) + ((3 * (2 |^ 2)) * (3 * (a div 3)))) + (2 |^ 3) by SERIES_4:2
.= ((((3 |^ 3) * ((a div 3) |^ 3)) + ((3 * ((3 * (a div 3)) |^ 2)) * 2)) + ((3 * (2 |^ 2)) * (3 * (a div 3)))) + (2 |^ 3) by NEWTON:7
.= (((((3 * 3) * 3) * ((a div 3) |^ 3)) + ((3 * ((3 * (a div 3)) |^ 2)) * 2)) + ((3 * (2 |^ 2)) * (3 * (a div 3)))) + (2 |^ 3) by POLYEQ_3:27
.= (((((3 * 3) * 3) * ((a div 3) |^ 3)) + ((3 * ((3 |^ 2) * ((a div 3) |^ 2))) * 2)) + ((3 * (2 |^ 2)) * (3 * (a div 3)))) + (2 |^ 3) by NEWTON:7
.= (((((3 * 3) * 3) * ((a div 3) |^ 3)) + ((3 * ((3 * 3) * ((a div 3) |^ 2))) * 2)) + ((3 * (2 |^ 2)) * (3 * (a div 3)))) + (2 |^ 3) by WSIERP_1:1
.= (9 * (((3 * ((a div 3) |^ 3)) + ((3 * ((a div 3) |^ 2)) * 2)) + ((2 |^ 2) * (a div 3)))) + ((2 * 2) * 2) by POLYEQ_3:27 ;
hence (a |^ 3) mod 9 = (((9 * (((3 * ((a div 3) |^ 3)) + ((3 * ((a div 3) |^ 2)) * 2)) + ((2 |^ 2) * (a div 3)))) mod 9) + (((2 * 2) * 2) mod 9)) mod 9 by NAT_D:66
.= (0 + (8 mod 9)) mod 9 by NAT_D:71
.= 8 by NAT_D:63 ;
:: thesis: verum

end;

thus ( (a |^ 3) mod 9 = 1 or (a |^ 3) mod 9 = 8 ) by A2, A3, A1, ENUMSET1:def 1, CARD_1:51; :: thesis: verum