let n be Nat; :: thesis: for p being Prime
for a being Element of (GF p) st a <> 0 holds
(a ") |^ n = (a |^ n) "
let p be Prime; :: thesis: for a being Element of (GF p) st a <> 0 holds
(a ") |^ n = (a |^ n) "
let a be Element of (GF p); :: thesis: ( a <> 0 implies (a ") |^ n = (a |^ n) " )
assume A1: a <> 0 ; :: thesis: (a ") |^ n = (a |^ n) "
A2: p > 1 by INT_2:def 4;
consider n1 being Nat such that
A3: a = n1 mod p by Th13;
consider n2 being Nat such that
A4: a " = n2 mod p by Th13;
A5: a |^ n = (n1 |^ n) mod p by A3, Th23;
A6: (a ") |^ n = (n2 |^ n) mod p by A4, Th23;
A7: ((n1 * n2) |^ n) mod p = ((n1 |^ n) * (n2 |^ n)) mod p by NEWTON:7
.= (a |^ n) * ((a ") |^ n) by A5, A6, Th18 ;
a <> 0. (GF p) by A1, Th11;
then (a ") * a = 1. (GF p) by VECTSP_1:def 10
.= 1 by Th12 ;
then (n1 * n2) mod p = 1 by A3, A4, Th18;
then ((n1 * n2) |^ n) mod p = 1 by A2, PEPIN:35;
then A8: ((a ") |^ n) * (a |^ n) = 1. (GF p) by A7;
then a |^ n <> 0. (GF p) ;
hence (a ") |^ n = (a |^ n) " by A8, VECTSP_1:def 10; :: thesis: verum