let n be Nat; :: thesis: for p being Prime
for a being Element of (GF p) st a <> 0 holds
a |^ n <> 0
let p be Prime; :: thesis: for a being Element of (GF p) st a <> 0 holds
a |^ n <> 0
let a be Element of (GF p); :: thesis: ( a <> 0 implies a |^ n <> 0 )
assume A1: a <> 0 ; :: thesis: a |^ n <> 0
consider n1 being Nat such that
A2: a = n1 mod p by Th13;
not p divides n1 by A1, A2, INT_1:62;
then not p divides n1 |^ n by NAT_3:5;
then (n1 |^ n) mod p <> 0 by INT_1:62;
hence a |^ n <> 0 by A2, Th23; :: thesis: verum