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 A1: ( p > 2 & q > 2 & p <> q & ( p mod 4 = 1 or q mod 4 = 1 ) ) ; :: thesis: Lege p,q = Lege q,p
( p > 1 & q > 1 ) by INT_2:def 5;
then A2: ( p -' 1 = p - 1 & q -' 1 = q - 1 ) by XREAL_1:235;

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

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 A2;
then (p -' 1) div 2 = 2 * (p div 4) by NAT_D:18;
then A3: (Lege p,q) * (Lege q,p) = (- 1) |^ ((2 * (p div 4)) * ((q -' 1) div 2)) by A1, Th49
.= ((- 1) |^ (2 * (p div 4))) |^ ((q -' 1) div 2) by NEWTON:14
.= (((- 1) |^ 2) |^ (p div 4)) |^ ((q -' 1) div 2) by NEWTON:14
.= ((1 |^ 2) |^ (p div 4)) |^ ((q -' 1) div 2) by WSIERP_1:2
.= ((1 ^2 ) |^ (p div 4)) |^ ((q -' 1) div 2) by NEWTON:100
.= 1 |^ ((q -' 1) div 2) by NEWTON:15
.= 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;

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 A2;
then (q -' 1) div 2 = 2 * (q div 4) by NAT_D:18;
then A4: (Lege p,q) * (Lege q,p) = (- 1) |^ ((2 * (q div 4)) * ((p -' 1) div 2)) by A1, Th49
.= ((- 1) |^ (2 * (q div 4))) |^ ((p -' 1) div 2) by NEWTON:14
.= (((- 1) |^ 2) |^ (q div 4)) |^ ((p -' 1) div 2) by NEWTON:14
.= ((1 |^ 2) |^ (q div 4)) |^ ((p -' 1) div 2) by WSIERP_1:2
.= ((1 ^2 ) |^ (q div 4)) |^ ((p -' 1) div 2) by NEWTON:100
.= 1 |^ ((p -' 1) div 2) by NEWTON:15
.= 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 A4; :: thesis: verum

end;

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

hence Lege p,q = Lege q,p by A4; :: thesis: verum

end;

end;

end;

end;