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