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 5;
then A6:
q -' 1 = q - 1
by XREAL_1:235;
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 5;
then A8:
p -' 1 = p - 1
by XREAL_1:235;
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: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
;