let n be Nat; :: thesis: for p being Prime
for a being Element of (GF p) st n mod 2 = 1 holds
Lege_p (a |^ n) = Lege_p a
let p be Prime; :: thesis: for a being Element of (GF p) st n mod 2 = 1 holds
Lege_p (a |^ n) = Lege_p a
let a be Element of (GF p); :: thesis: ( n mod 2 = 1 implies Lege_p (a |^ n) = Lege_p a )
assume A1: n mod 2 = 1 ; :: thesis: Lege_p (a |^ n) = Lege_p a
A2: n = ((n div 2) * 2) + 1 by A1, INT_1:59;
reconsider n1 = n - 1 as Nat by A2;
a |^ (n1 + 1) = (a |^ n1) * a by Th24;
then A3: Lege_p (a |^ n) = (Lege_p (a |^ n1)) * (Lege_p a) by Th36;

per cases ( a = 0 or a <> 0 ) ;

suppose a = 0 ; :: thesis: Lege_p (a |^ n) = Lege_p a

then Lege_p a = 0 by Def5;
hence Lege_p (a |^ n) = Lege_p a by A3; :: thesis: verum

end;

suppose A4: a <> 0 ; :: thesis: Lege_p (a |^ n) = Lege_p a

(n - 1) mod 2 = (0 + ((n div 2) * 2)) mod 2 by A2
.= 0 mod 2 by NAT_D:61
.= 0 by NAT_D:26 ;
then Lege_p (a |^ n1) = 1 by A4, Th37;
hence Lege_p (a |^ n) = Lege_p a by A3; :: thesis: verum

end;

end;