let k, n be Nat; :: thesis: ( k divides 5 |^ n implies k mod 4 = 1 )
assume k divides 5 |^ n ; :: thesis: k mod 4 = 1
then consider t being Element of NAT such that
A1: k = 5 |^ t and
t <= n by PEPIN:34, PEPIN:59;
A2: ((4 * 1) + 1) mod 4 = 1 mod 4 by NAT_D:21;
(5 |^ t) mod 4 = ((5 mod 4) |^ t) mod 4 by PEPIN:12;
hence k mod 4 = 1 by A1, A2, Lm3; :: thesis: verum