let p be Prime; :: thesis: 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) )
let n be Nat; :: thesis: 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) )
let g2, g3 be Element of (GF p); :: thesis: ( p > 3 & g3 = 3 mod p implies ( g3 <> 0. (GF p) & g3 |^ n <> 0. (GF p) ) )
assume A1: p > 3 ; :: thesis: ( not g3 = 3 mod p or ( g3 <> 0. (GF p) & g3 |^ n <> 0. (GF p) ) )
assume A2: g3 = 3 mod p ; :: thesis: ( g3 <> 0. (GF p) & g3 |^ n <> 0. (GF p) )
A3: g3 <> 0 by A1, A2, NAT_D:63;
hence g3 <> 0. (GF p) by EC_PF_1:11; :: thesis: g3 |^ n <> 0. (GF p)
g3 |^ n <> 0 by A3, EC_PF_1:25;
hence g3 |^ n <> 0. (GF p) by EC_PF_1:11; :: thesis: verum