let a be Nat; :: thesis: ex k being Nat st
( a ^2 = 7 * k or a ^2 = (7 * k) + 1 or a ^2 = (7 * k) + 2 or a ^2 = (7 * k) + 4 )

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

suppose not 7 divides a ; :: thesis: ex k being Nat st
( a ^2 = 7 * k or a ^2 = (7 * k) + 1 or a ^2 = (7 * k) + 2 or a ^2 = (7 * k) + 4 )

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

end;

suppose 7 divides a ; :: thesis: ex k being Nat st
( a ^2 = 7 * k or a ^2 = (7 * k) + 1 or a ^2 = (7 * k) + 2 or a ^2 = (7 * k) + 4 )

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

end;

end;