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 A1: ( p > 2 & q > 2 & p <> q & p mod 4 = 3 & q mod 4 = 3 ) ; :: thesis: Lege p,q = - (Lege q,p)
then A2: ( p = (4 * (p div 4)) + 3 & q = (4 * (q div 4)) + 3 ) by NAT_D:2;
( p > 1 & q > 1 ) by INT_2:def 5;
then ( p -' 1 = p - 1 & q -' 1 = q - 1 ) by XREAL_1:235;
then ( p -' 1 = 2 * ((2 * (p div 4)) + 1) & q -' 1 = 2 * ((2 * (q div 4)) + 1) ) by A2;
then ( (p -' 1) div 2 = (2 * (p div 4)) + 1 & (q -' 1) div 2 = (2 * (q div 4)) + 1 ) by NAT_D:18;
then A3: (Lege p,q) * (Lege q,p) = (- 1) |^ (((2 * (p div 4)) + 1) * ((2 * (q div 4)) + 1)) by A1, Th49
.= ((- 1) |^ ((2 * (p div 4)) + 1)) |^ ((2 * (q div 4)) + 1) by NEWTON:14
.= (((- 1) |^ (2 * (p div 4))) * (- 1)) |^ ((2 * (q div 4)) + 1) by NEWTON:11
.= ((((- 1) |^ 2) |^ (p div 4)) * (- 1)) |^ ((2 * (q div 4)) + 1) by NEWTON:14
.= (((1 |^ 2) |^ (p div 4)) * (- 1)) |^ ((2 * (q div 4)) + 1) by WSIERP_1:2
.= (((1 ^2 ) |^ (p div 4)) * (- 1)) |^ ((2 * (q div 4)) + 1) by NEWTON:100
.= (1 * (- 1)) |^ ((2 * (q div 4)) + 1) by NEWTON:15
.= ((- 1) |^ (2 * (q div 4))) * (- 1) by NEWTON:11
.= (((- 1) |^ 2) |^ (q div 4)) * (- 1) by NEWTON:14
.= ((1 |^ 2) |^ (q div 4)) * (- 1) by WSIERP_1:2
.= ((1 ^2 ) |^ (q div 4)) * (- 1) by NEWTON:100
.= 1 * (- 1) by NEWTON:15 ;

per cases ( Lege p,q = 1 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 A3; :: thesis: verum

end;

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

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

end;

end;