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)
(- 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 A2: Lege (- 1),p,(- 1) |^ ((p -' 1) div 2) are_congruent_mod p by A1, Th28;
abs ((- 1) |^ ((p -' 1) div 2)) = 1 by SERIES_2:1;
then A3: ( (- 1) |^ ((p -' 1) div 2) = 1 or - ((- 1) |^ ((p -' 1) div 2)) = 1 ) by ABSVALUE:1;

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

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 A2, 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 A2, 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;