let a be Nat; :: thesis: ( (a ^2) mod 7 = 0 or (a ^2) mod 7 = 1 or (a ^2) mod 7 = 2 or (a ^2) mod 7 = 4 )

per cases ( not 7 divides a or 7 divides a ) ;

suppose not 7 divides a ; :: thesis: ( (a ^2) mod 7 = 0 or (a ^2) mod 7 = 1 or (a ^2) mod 7 = 2 or (a ^2) mod 7 = 4 )

then ex k being Nat st
( a ^2 = (7 * k) + 1 or a ^2 = (7 * k) + 2 or a ^2 = (7 * k) + 4 ) by Th46;
hence ( (a ^2) mod 7 = 0 or (a ^2) mod 7 = 1 or (a ^2) mod 7 = 2 or (a ^2) mod 7 = 4 ) by Th16; :: thesis: verum

end;

suppose 7 divides a ; :: thesis: ( (a ^2) mod 7 = 0 or (a ^2) mod 7 = 1 or (a ^2) mod 7 = 2 or (a ^2) mod 7 = 4 )

then 7 divides a ^2 by INT_2:2;
hence ( (a ^2) mod 7 = 0 or (a ^2) mod 7 = 1 or (a ^2) mod 7 = 2 or (a ^2) mod 7 = 4 ) by PEPIN:6; :: thesis: verum

end;

end;