let p be Prime; :: thesis: ( p > 2 implies Lege ((- 1),p) = (- 1) |^ ((p -' 1) div 2) )
assume A1: p > 2 ; :: thesis: Lege ((- 1),p) = (- 1) |^ ((p -' 1) div 2)
abs ((- 1) |^ ((p -' 1) div 2)) = 1 by SERIES_2:1;
then A2: ( (- 1) |^ ((p -' 1) div 2) = 1 or - ((- 1) |^ ((p -' 1) div 2)) = 1 ) by ABSVALUE:1;
(- 1) gcd p = ((- 1) |^ 1) gcd p by NEWTON:10
.= (abs ((- 1) |^ 1)) gcd (abs p) by INT_2:51
.= 1 gcd (abs p) by SERIES_2:1
.= 1 by NEWTON:64 ;
then A3: Lege ((- 1),p),(- 1) |^ ((p -' 1) div 2) are_congruent_mod p by A1, Th28;

per cases ( (- 1) |^ ((p -' 1) div 2) = 1 or (- 1) |^ ((p -' 1) div 2) = - 1 ) by A2;

suppose A4: (- 1) |^ ((p -' 1) div 2) = 1 ; :: thesis: Lege ((- 1),p) = (- 1) |^ ((p -' 1) div 2)

then A5: p divides (Lege ((- 1),p)) - 1 by A3, INT_2:19;

now

assume Lege ((- 1),p) = - 1 ; :: thesis: contradiction
then p divides - 2 by A5;
then p divides 2 by INT_2:14;
hence contradiction by A1, NAT_D:7; :: thesis: verum

end;

hence Lege ((- 1),p) = (- 1) |^ ((p -' 1) div 2) by A4, Th25; :: thesis: verum

end;

suppose A6: (- 1) |^ ((p -' 1) div 2) = - 1 ; :: thesis: Lege ((- 1),p) = (- 1) |^ ((p -' 1) div 2)

then p divides (Lege ((- 1),p)) - (- 1) by A3, INT_2:19;
then Lege ((- 1),p) <> 1 by A1, NAT_D:7;
hence Lege ((- 1),p) = (- 1) |^ ((p -' 1) div 2) by A6, Th25; :: thesis: verum

end;

end;