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 AS: a <> 0 ; :: thesis: (a ") |^ n = (a |^ n) "
P0: p > 1 by INT_2:def 4;
consider n1 being Nat such that
P1: a = n1 mod p by GF1;
consider n2 being Nat such that
P2: a " = n2 mod p by GF1;
P3: a |^ n = (n1 |^ n) mod p by P1, EX4;
P4: (a ") |^ n = (n2 |^ n) mod p by P2, EX4;
P5: ((n1 * n2) |^ n) mod p = ((n1 |^ n) * (n2 |^ n)) mod p by NEWTON:7
.= (a |^ n) * ((a ") |^ n) by P3, P4, GF6 ;
a <> 0. (GF p) by AS, XLm2;
then (a ") * a = 1. (GF p) by VECTSP_1:def 10
.= 1 by XLm3 ;
then (n1 * n2) mod p = 1 by P1, P2, GF6;
then ((n1 * n2) |^ n) mod p = 1 by P0, PEPIN:35;
then P7: ((a ") |^ n) * (a |^ n) = 1. (GF p) by P0, P5, INT_3:14;
then a |^ n <> 0. (GF p) by VECTSP_1:7;
hence (a ") |^ n = (a |^ n) " by P7, VECTSP_1:def 10; :: thesis: verum