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) |^ ((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 INT_2:34
.= 1 gcd |.p.| by SERIES_2:1
.= 1 by NEWTON:51 ;
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;
A6: now :: thesis: not Lege ((- 1),p) = - 1
assume Lege ((- 1),p) = - 1 ; :: thesis: contradiction
then p divides - 2 by A5;
then p divides 2 by INT_2:10;
hence contradiction by A1, NAT_D:7; :: thesis: verum
end;
now :: thesis: not Lege ((- 1),p) = 0
assume Lege ((- 1),p) = 0 ; :: thesis: contradiction
then p divides 1 by A5, INT_2:10;
then p <= 1 by NAT_D:7;
then p < 1 + 1 by NAT_1:13;
hence contradiction by A1; :: thesis: verum
end;
hence Lege ((- 1),p) = (- 1) |^ ((p -' 1) div 2) by A4, Th25, A6; :: thesis: verum
end;
suppose A7: (- 1) |^ ((p -' 1) div 2) = - 1 ; :: thesis: Lege ((- 1),p) = (- 1) |^ ((p -' 1) div 2)
then A8: p divides (Lege ((- 1),p)) - (- 1) by A3;
then A9: Lege ((- 1),p) <> 1 by A1, NAT_D:7;
now :: thesis: not Lege ((- 1),p) = 0
assume Lege ((- 1),p) = 0 ; :: thesis: contradiction
then p <= 1 by A8, NAT_D:7;
then p < 1 + 1 by NAT_1:13;
hence contradiction by A1; :: thesis: verum
end;
hence Lege ((- 1),p) = (- 1) |^ ((p -' 1) div 2) by A7, Th25, A9; :: thesis: verum
end;
end;