let p, q be 2 _greater Prime; ( p <> q implies (Leg (p,q)) * (Leg (q,p)) = (- 1) |^ (((p - 1) / 2) * ((q - 1) / 2)) )
assume A1:
p <> q
; (Leg (p,q)) * (Leg (q,p)) = (- 1) |^ (((p - 1) / 2) * ((q - 1) / 2))
A2:
( p > 2 & q > 2 )
by Def1;
p - 1 > 2 - 1
by Def1, XREAL_1:9;
then
p -' 1 = p - 1
by NAT_D:39;
then A3:
(p -' 1) div 2 = (p - 1) / 2
;
q - 1 > 2 - 1
by Def1, XREAL_1:9;
then
q -' 1 = q - 1
by NAT_D:39;
then A4:
(- 1) |^ (((p -' 1) div 2) * ((q -' 1) div 2)) = (- 1) |^ (((p - 1) / 2) * ((q - 1) / 2))
by A3;
thus (Leg (p,q)) * (Leg (q,p)) =
(Leg (p,q)) * (Lege (q,p))
by Lm4
.=
(Lege (p,q)) * (Lege (q,p))
by Lm4
.=
(- 1) |^ (((p - 1) / 2) * ((q - 1) / 2))
by A1, A2, A4, INT_5:49
; verum