theorem Th28: :: EC_PF_2:28

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