let p be Prime; :: thesis: for n being Nat st p mod 4 = 1 holds
( card (divisors ((p |^ n),4,1)) = n + 1 & card (divisors ((p |^ n),4,3)) = 0 )
let n be Nat; :: thesis: ( p mod 4 = 1 implies ( card (divisors ((p |^ n),4,1)) = n + 1 & card (divisors ((p |^ n),4,3)) = 0 ) )
assume A1: p mod 4 = 1 ; :: thesis: ( card (divisors ((p |^ n),4,1)) = n + 1 & card (divisors ((p |^ n),4,3)) = 0 )
set X = { k where k is Nat : ( k mod 4 = 1 & k divides p |^ n ) } ;
set Y = { k where k is Nat : k divides p |^ n } ;
A2: divisors ((p |^ n),4,1) c= { k where k is Nat : k divides p |^ n }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in divisors ((p |^ n),4,1) or x in { k where k is Nat : k divides p |^ n } )
assume x in divisors ((p |^ n),4,1) ; :: thesis: x in { k where k is Nat : k divides p |^ n }
then ex k being Nat st
( x = k & k mod 4 = 1 & k divides p |^ n ) ;
hence x in { k where k is Nat : k divides p |^ n } ; :: thesis: verum

end;

{ k where k is Nat : k divides p |^ n } c= divisors ((p |^ n),4,1)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Nat : k divides p |^ n } or x in divisors ((p |^ n),4,1) )
assume x in { k where k is Nat : k divides p |^ n } ; :: thesis: x in divisors ((p |^ n),4,1)
then consider k being Nat such that
A3: ( x = k & k divides p |^ n ) ;
k mod 4 = 1 by Th10, A1, A3;
hence x in divisors ((p |^ n),4,1) by A3; :: thesis: verum

end;

then { k where k is Nat : k divides p |^ n } = divisors ((p |^ n),4,1) by A2, XBOOLE_0:def 10;
hence card (divisors ((p |^ n),4,1)) = n + 1 by Th16; :: thesis: card (divisors ((p |^ n),4,3)) = 0
assume card (divisors ((p |^ n),4,3)) <> 0 ; :: thesis: contradiction
then divisors ((p |^ n),4,3) <> {} ;
then consider x being object such that
A4: x in divisors ((p |^ n),4,3) by XBOOLE_0:def 1;
ex k being Nat st
( x = k & k mod 4 = 3 & k divides p |^ n ) by A4;
hence contradiction by Th10, A1; :: thesis: verum