let p be natural prime number ; :: thesis: for a being integer number holds
( Leg (a,p) = 1 or Leg (a,p) = 0 or Leg (a,p) = - 1 )
let a be integer number ; :: thesis: ( Leg (a,p) = 1 or Leg (a,p) = 0 or Leg (a,p) = - 1 )
assume A1: ( Leg (a,p) <> 1 & Leg (a,p) <> 0 ) ; :: thesis: Leg (a,p) = - 1
a gcd p = 1
proof
( a gcd p = 1 or a gcd p = p ) by INT_2:def 4, INT_2:21;
hence a gcd p = 1 by A1, Def4, INT_2:21; :: thesis: verum
end;
hence Leg (a,p) = - 1 by A1, Def4; :: thesis: verum