let n be Nat; :: thesis: for p being Prime st p mod 4 = 3 holds
( (p |^ (2 * n)) mod 4 = 1 & (p |^ ((2 * n) + 1)) mod 4 = 3 )
let p be Prime; :: thesis: ( p mod 4 = 3 implies ( (p |^ (2 * n)) mod 4 = 1 & (p |^ ((2 * n) + 1)) mod 4 = 3 ) )
assume A1: p mod 4 = 3 ; :: thesis: ( (p |^ (2 * n)) mod 4 = 1 & (p |^ ((2 * n) + 1)) mod 4 = 3 )
defpred S₁[ Nat] means ( (p |^ (2 * $1)) mod 4 = 1 & (p |^ ((2 * $1) + 1)) mod 4 = 3 );
( p |^ (2 * 0) = 1 & p |^ ((2 * 0) + 1) = p ) by NEWTON:4;
then A2: S₁[ 0 ] by A1, PEPIN:5;
A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

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

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
hence ( (p |^ (2 * n)) mod 4 = 1 & (p |^ ((2 * n) + 1)) mod 4 = 3 ) ; :: thesis: verum