let p be Prime; :: thesis: for a being Element of (GF p) holds
( a = 0 iff Lege_p a = 0 )
let a be Element of (GF p); :: thesis: ( a = 0 iff Lege_p a = 0 )
thus ( a = 0 implies Lege_p a = 0 ) by QRDef3; :: thesis: ( Lege_p a = 0 implies a = 0 )
assume Lege_p a = 0 ; :: thesis: a = 0
then ( not a is quadratic_residue & Lege_p a <> - 1 ) by QRDef3;
hence a = 0 by QRDef3; :: thesis: verum