let p, q be Prime; :: thesis: ( p > 2 & q > 2 & p <> q & ( p mod 4 = 1 or q mod 4 = 1 ) 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 = 1 or q mod 4 = 1 ) ; :: thesis: Lege (p,q) = Lege (q,p)
p > 1 by INT_2:def 4;
then A5: p -' 1 = p - 1 by XREAL_1:233;
q > 1 by INT_2:def 4;
then A6: q -' 1 = q - 1 by XREAL_1:233;

per cases ( p mod 4 = 1 or q mod 4 = 1 ) by A4;

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

then p = (4 * (p div 4)) + 1 by NAT_D:2;
then p -' 1 = 2 * (2 * (p div 4)) by A5;
then (p -' 1) div 2 = 2 * (p div 4) ;
then A7: (Lege (p,q)) * (Lege (q,p)) = (- 1) |^ ((2 * (p div 4)) * ((q -' 1) div 2)) by A1, A2, A3, Th49
.= ((- 1) |^ (2 * (p div 4))) |^ ((q -' 1) div 2) by NEWTON:9
.= (((- 1) |^ 2) |^ (p div 4)) |^ ((q -' 1) div 2) by NEWTON:9
.= ((1 |^ 2) |^ (p div 4)) |^ ((q -' 1) div 2) by WSIERP_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 A7; :: thesis: verum

end;

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

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

end;

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

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

end;

end;

end;

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

then q = (4 * (q div 4)) + 1 by NAT_D:2;
then q -' 1 = 2 * (2 * (q div 4)) by A6;
then (q -' 1) div 2 = 2 * (q div 4) ;
then A8: (Lege (p,q)) * (Lege (q,p)) = (- 1) |^ ((2 * (q div 4)) * ((p -' 1) div 2)) by A1, A2, A3, Th49
.= ((- 1) |^ (2 * (q div 4))) |^ ((p -' 1) div 2) by NEWTON:9
.= (((- 1) |^ 2) |^ (q div 4)) |^ ((p -' 1) div 2) by NEWTON:9
.= ((1 |^ 2) |^ (q div 4)) |^ ((p -' 1) div 2) by WSIERP_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 A8; :: thesis: verum

end;

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

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

end;

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

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

end;

end;

end;

end;