let p, q be Prime; :: thesis: ( p > 2 & q > 2 & p <> q & p mod 4 = 3 & q mod 4 = 3 implies Lege (p,q) = - (Lege (q,p)) )
assume that
A1: p > 2 and
A2: q > 2 and
A3: p <> q and
A4: p mod 4 = 3 and
A5: q mod 4 = 3 ; :: thesis: Lege (p,q) = - (Lege (q,p))
q > 1 by INT_2:def 4;
then A6: q -' 1 = q - 1 by XREAL_1:233;
q = (4 * (q div 4)) + 3 by A5, NAT_D:2;
then q -' 1 = 2 * ((2 * (q div 4)) + 1) by A6;
then A7: (q -' 1) div 2 = (2 * (q div 4)) + 1 ;
p > 1 by INT_2:def 4;
then A8: p -' 1 = p - 1 by XREAL_1:233;
p = (4 * (p div 4)) + 3 by A4, NAT_D:2;
then p -' 1 = 2 * ((2 * (p div 4)) + 1) by A8;
then (p -' 1) div 2 = (2 * (p div 4)) + 1 ;
then A9: (Lege (p,q)) * (Lege (q,p)) = (- 1) |^ (((2 * (p div 4)) + 1) * ((2 * (q div 4)) + 1)) by A1, A2, A3, A7, Th49
.= ((- 1) |^ ((2 * (p div 4)) + 1)) |^ ((2 * (q div 4)) + 1) by NEWTON:9
.= (((- 1) |^ (2 * (p div 4))) * (- 1)) |^ ((2 * (q div 4)) + 1) by NEWTON:6
.= ((((- 1) |^ 2) |^ (p div 4)) * (- 1)) |^ ((2 * (q div 4)) + 1) by NEWTON:9
.= (((1 |^ 2) |^ (p div 4)) * (- 1)) |^ ((2 * (q div 4)) + 1) by WSIERP_1:1
.= ((- 1) |^ (2 * (q div 4))) * (- 1) by NEWTON:6
.= (((- 1) |^ 2) |^ (q div 4)) * (- 1) by NEWTON:9
.= ((1 |^ 2) |^ (q div 4)) * (- 1) by WSIERP_1:1
.= 1 * (- 1) ;

per cases ( Lege (p,q) = 1 or Lege (p,q) = 0 or Lege (p,q) = - 1 ) by Th25;

suppose Lege (p,q) = 1 ; :: thesis: Lege (p,q) = - (Lege (q,p))

hence Lege (p,q) = - (Lege (q,p)) by A9; :: thesis: verum

end;

suppose Lege (p,q) = 0 ; :: thesis: Lege (p,q) = - (Lege (q,p))

hence Lege (p,q) = - (Lege (q,p)) by A9; :: thesis: verum

end;

suppose Lege (p,q) = - 1 ; :: thesis: Lege (p,q) = - (Lege (q,p))

hence Lege (p,q) = - (Lege (q,p)) by A9; :: thesis: verum

end;

end;