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;