now :: thesis: for x being Integer holds not x |^ 2,2 are_congruent_mod 3

assume ex x being Integer st x |^ 2,2 are_congruent_mod 3 ; :: thesis: contradiction
then consider x being Integer such that
A1: x |^ 2,2 are_congruent_mod 3 ;

now :: thesis: ( ( x |^ 2, 0 are_congruent_mod 3 & contradiction ) or ( x |^ 2,1 are_congruent_mod 3 & contradiction ) )

per cases ( x |^ 2, 0 are_congruent_mod 3 or x |^ 2,1 are_congruent_mod 3 ) by Th15;

case x |^ 2, 0 are_congruent_mod 3 ; :: thesis: contradiction

hence contradiction by A1, Th14; :: thesis: verum

end;

case x |^ 2,1 are_congruent_mod 3 ; :: thesis: contradiction

hence contradiction by A1, Th14; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence 2 is_quadratic_non_residue_mod 3 by Th22; :: thesis: verum