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;

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;

end;

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) by NAT_D:18;

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 ;

end;then p -' 1 = 2 * (2 * (p div 4)) by A5;

then (p -' 1) div 2 = 2 * (p div 4) by NAT_D:18;

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 ;

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) by NAT_D:18;

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 ;

end;then q -' 1 = 2 * (2 * (q div 4)) by A6;

then (q -' 1) div 2 = 2 * (q div 4) by NAT_D:18;

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 ;