let p be Prime; :: thesis: 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) )
let n be Nat; :: thesis: for g2 being Element of (GF p) st p > 2 & g2 = 2 mod p holds
( g2 <> 0. (GF p) & g2 |^ n <> 0. (GF p) )
let g2 be Element of (GF p); :: thesis: ( p > 2 & g2 = 2 mod p implies ( g2 <> 0. (GF p) & g2 |^ n <> 0. (GF p) ) )
assume that
A1: p > 2 and
A2: g2 = 2 mod p ; :: thesis: ( g2 <> 0. (GF p) & g2 |^ n <> 0. (GF p) )
A3: g2 <> 0 by A1, A2, NAT_D:63;
hence g2 <> 0. (GF p) by EC_PF_1:11; :: thesis: g2 |^ n <> 0. (GF p)
g2 |^ n <> 0 by A3, EC_PF_1:25;
hence g2 |^ n <> 0. (GF p) by EC_PF_1:11; :: thesis: verum