let a be Nat; ( not 7 divides a implies 7 divides (a |^ 6) - 1 )
assume
not 7 divides a
; 7 divides (a |^ 6) - 1
then A1:
not a gcd 7 = 7
by INT_2:def 2;
7 divides (a |^ (6 + 1)) - a
by NAT_4:26, Th58;
then
7 divides ((a |^ 6) * a) - a
by NEWTON:6;
then
7 divides a * ((a |^ 6) - 1)
;
hence
7 divides (a |^ 6) - 1
by A1, NAT_4:26, PEPIN:2, INT_2:25; verum