let n be Nat; :: thesis: for p being Prime holds card (divisors ((p |^ n),4,1)) >= card (divisors ((p |^ n),4,3))
let p be Prime; :: thesis: card (divisors ((p |^ n),4,1)) >= card (divisors ((p |^ n),4,3))

per cases ( p = 2 or p mod 4 = 1 or p mod 4 = 3 ) by Th19;

suppose p = 2 ; :: thesis: card (divisors ((p |^ n),4,1)) >= card (divisors ((p |^ n),4,3))

then ( divisors ((p |^ n),4,1) = {1} & divisors ((p |^ n),4,3) = {} ) by Th15;
hence card (divisors ((p |^ n),4,1)) >= card (divisors ((p |^ n),4,3)) ; :: thesis: verum

end;

suppose p mod 4 = 1 ; :: thesis: card (divisors ((p |^ n),4,1)) >= card (divisors ((p |^ n),4,3))

hence card (divisors ((p |^ n),4,1)) >= card (divisors ((p |^ n),4,3)) by Th17; :: thesis: verum

end;

suppose A1: p mod 4 = 3 ; :: thesis: card (divisors ((p |^ n),4,1)) >= card (divisors ((p |^ n),4,3))

per cases ( n is odd or n is even ) ;

suppose n is odd ; :: thesis: card (divisors ((p |^ n),4,1)) >= card (divisors ((p |^ n),4,3))

then consider k1 being Nat such that
A2: n = (2 * k1) + 1 by ABIAN:9;
( card (divisors ((p |^ n),4,1)) = k1 + 1 & card (divisors ((p |^ n),4,3)) = k1 + 1 ) by A2, A1, Th18;
hence card (divisors ((p |^ n),4,1)) >= card (divisors ((p |^ n),4,3)) ; :: thesis: verum

end;

suppose n is even ; :: thesis: card (divisors ((p |^ n),4,1)) >= card (divisors ((p |^ n),4,3))

then consider k1 being Nat such that
A3: n = 2 * k1 ;
( card (divisors ((p |^ n),4,1)) = k1 + 1 & card (divisors ((p |^ n),4,3)) = k1 ) by A3, A1, Th18;
hence card (divisors ((p |^ n),4,1)) >= card (divisors ((p |^ n),4,3)) by NAT_1:13; :: thesis: verum

end;

end;

end;

end;