let a be Nat; ( 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
; 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 )
; verum