let n be Nat; :: thesis: for p being Prime
for a being Element of (GF p) st a <> 0 & n mod 2 = 0 holds
Lege_p (a |^ n) = 1
let p be Prime; :: thesis: for a being Element of (GF p) st a <> 0 & n mod 2 = 0 holds
Lege_p (a |^ n) = 1
let a be Element of (GF p); :: thesis: ( a <> 0 & n mod 2 = 0 implies Lege_p (a |^ n) = 1 )
assume A1: ( a <> 0 & n mod 2 = 0 ) ; :: thesis: Lege_p (a |^ n) = 1
A2: n = ((n div 2) * 2) + (n mod 2) by INT_1:59
.= (n div 2) * 2 by A1 ;
reconsider n1 = n div 2 as Nat ;
(a |^ n1) |^ 2 is quadratic_residue by A1, Th31, Th25;
then a |^ n is quadratic_residue by A2, Lm4;
hence Lege_p (a |^ n) = 1 by Def5; :: thesis: verum