let a be Nat; :: thesis: ( not 7 divides (a |^ 3) - 2 & not 7 divides (a |^ 3) + 2 & not 7 divides (a |^ 3) - 3 & not 7 divides (a |^ 3) + 3 & not 7 divides (a |^ 3) - 4 & not 7 divides (a |^ 3) + 4 & not 7 divides (a |^ 3) - 5 & not 7 divides (a |^ 3) + 5 )
7 = (2 * 3) + 1 ;
hence ( not 7 divides (a |^ 3) - 2 & not 7 divides (a |^ 3) + 2 & not 7 divides (a |^ 3) - 3 & not 7 divides (a |^ 3) + 3 & not 7 divides (a |^ 3) - 4 & not 7 divides (a |^ 3) + 4 & not 7 divides (a |^ 3) - 5 & not 7 divides (a |^ 3) + 5 ) by Th84, NAT_4:26; :: thesis: verum