let p, q be Prime; ( 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
; 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
by NAT_D:18;
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
by NAT_D:18;
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)
;