let a be Nat; :: thesis: ( not 7 divides a implies ex k being Nat st
( a ^2 = (7 * k) + 1 or a ^2 = (7 * k) + 2 or a ^2 = (7 * k) + 4 ) )
assume not 7 divides a ; :: thesis: ex k being Nat st
( a ^2 = (7 * k) + 1 or a ^2 = (7 * k) + 2 or a ^2 = (7 * k) + 4 )
then consider k being Nat such that
A1: ( a = (7 * k) + 1 or a = (7 * k) + 2 or a = (7 * k) + 3 or a = (7 * k) + 4 or a = (7 * k) + 5 or a = (7 * k) + 6 ) by Th35;
( a ^2 = (7 * (k * ((7 * k) + 2))) + 1 or a ^2 = (7 * (k * ((7 * k) + 4))) + 4 or a ^2 = (7 * ((k * ((7 * k) + 6)) + 1)) + 2 or a ^2 = (7 * ((k * ((7 * k) + 8)) + 2)) + 2 or a ^2 = (7 * ((k * ((7 * k) + 10)) + 3)) + 4 or a ^2 = (7 * ((k * ((7 * k) + 12)) + 5)) + 1 ) by A1;
hence ex k being Nat st
( a ^2 = (7 * k) + 1 or a ^2 = (7 * k) + 2 or a ^2 = (7 * k) + 4 ) ; :: thesis: verum