let k, n be Nat; :: thesis: for p being Prime st p is prime & p mod 4 = 1 & n divides p |^ k holds
n mod 4 = 1
let p be Prime; :: thesis: ( p is prime & p mod 4 = 1 & n divides p |^ k implies n mod 4 = 1 )
assume A1: ( p is prime & p mod 4 = 1 & n divides p |^ k ) ; :: thesis: n mod 4 = 1
then consider t being Element of NAT such that
A2: ( n = p |^ t & t <= k ) by PEPIN:34;
defpred S₁[ Nat] means (p |^ $1) mod 4 = 1;
p |^ 0 = 1 by NEWTON:4;
then A3: S₁[ 0 ] by PEPIN:5;
A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume S₁[i] ; :: thesis: S₁[i + 1]
then (p * (p |^ i)) mod 4 = 1 by A1, Th8;
hence S₁[i + 1] by NEWTON:6; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A4);
hence n mod 4 = 1 by A2; :: thesis: verum