let a, b, c, d, e be Integer; ( 9 divides ((((a |^ 3) + (b |^ 3)) + (c |^ 3)) + (d |^ 3)) + (e |^ 3) implies 3 divides (((a * b) * c) * d) * e )
assume
9 divides ((((a |^ 3) + (b |^ 3)) + (c |^ 3)) + (d |^ 3)) + (e |^ 3)
; 3 divides (((a * b) * c) * d) * e
then A1:
(((((a |^ 3) + (b |^ 3)) + (c |^ 3)) + (d |^ 3)) + (e |^ 3)) mod 9 = 0
by INT_1:62;
assume A2:
not 3 divides (((a * b) * c) * d) * e
; contradiction
then A3:
not 3 divides a * (((b * c) * d) * e)
;
A4:
not 3 divides b * (((a * c) * d) * e)
by A2;
A5:
not 3 divides c * (((a * b) * d) * e)
by A2;
not 3 divides d * (((a * b) * c) * e)
by A2;