theorem :: EC_PF_2:29

for p being Prime
for n being Nat
for g2, g3 being Element of (GF p) st p > 3 & g3 = 3 mod p holds
( g3 <> 0. (GF p) & g3 |^ n <> 0. (GF p) )