let a be Integer; :: thesis: for p being Prime holds
( Lege (a,p) = 1 or Lege (a,p) = 0 or Lege (a,p) = - 1 )
let p be Prime; :: thesis: ( Lege (a,p) = 1 or Lege (a,p) = 0 or Lege (a,p) = - 1 )

per cases ( ( a is_quadratic_residue_mod p & a mod p <> 0 ) or ( a is_quadratic_residue_mod p & a mod p = 0 ) or not a is_quadratic_residue_mod p ) ;

suppose ( a is_quadratic_residue_mod p & a mod p <> 0 ) ; :: thesis: ( Lege (a,p) = 1 or Lege (a,p) = 0 or Lege (a,p) = - 1 )

hence ( Lege (a,p) = 1 or Lege (a,p) = 0 or Lege (a,p) = - 1 ) by Def3; :: thesis: verum

end;

suppose ( a is_quadratic_residue_mod p & a mod p = 0 ) ; :: thesis: ( Lege (a,p) = 1 or Lege (a,p) = 0 or Lege (a,p) = - 1 )

hence ( Lege (a,p) = 1 or Lege (a,p) = 0 or Lege (a,p) = - 1 ) by Def3; :: thesis: verum

end;

suppose not a is_quadratic_residue_mod p ; :: thesis: ( Lege (a,p) = 1 or Lege (a,p) = 0 or Lege (a,p) = - 1 )

hence ( Lege (a,p) = 1 or Lege (a,p) = 0 or Lege (a,p) = - 1 ) by Def3; :: thesis: verum

end;

end;