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 AS: ( a <> 0 & n mod 2 = 0 ) ; :: thesis: Lege_p (a |^ n) = 1
P0: n = ((n div 2) * 2) + (n mod 2) by INT_1:59
.= (n div 2) * 2 by AS ;
reconsider n1 = n div 2 as Nat ;
(a |^ n1) |^ 2 is quadratic_residue by AS, QR1, EX6;
then a |^ n is quadratic_residue by P0, EX12;
hence Lege_p (a |^ n) = 1 by QRDef3; :: thesis: verum