let p be Prime; ( p > 2 implies Lege (2,p) = (- 1) |^ (((p ^2) -' 1) div 8) )
set p9 = (p -' 1) div 2;
set I = idseq ((p -' 1) div 2);
set fp = 2 * (idseq ((p -' 1) div 2));
set nn = p div 8;
A1:
p > 1
by INT_2:def 4;
then A2:
p - 1 = p -' 1
by XREAL_1:233;
A3:
for d being Nat st d in dom (2 * (idseq ((p -' 1) div 2))) holds
(2 * (idseq ((p -' 1) div 2))) . d = 2 * d
for d being Nat st d in dom (2 * (idseq ((p -' 1) div 2))) holds
(2 * (idseq ((p -' 1) div 2))) . d in NAT
;
then reconsider fp = 2 * (idseq ((p -' 1) div 2)) as FinSequence of NAT by FINSEQ_2:12;
set f = fp mod p;
reconsider f = fp mod p as FinSequence of NAT by FINSEQ_1:102;
set X = { k where k is Element of NAT : ( k in rng f & k > p / 2 ) } ;
set m = card { k where k is Element of NAT : ( k in rng f & k > p / 2 ) } ;
dom fp = dom (idseq ((p -' 1) div 2))
by VALUED_1:def 5;
then A6: len fp =
len (idseq ((p -' 1) div 2))
by FINSEQ_3:29
.=
(p -' 1) div 2
by CARD_1:def 7
;
set Y = { d where d is Element of NAT : ( d in dom f & f . d > p / 2 ) } ;
for x being object st x in { d where d is Element of NAT : ( d in dom f & f . d > p / 2 ) } holds
x in dom f
then
{ d where d is Element of NAT : ( d in dom f & f . d > p / 2 ) } c= dom f
;
then reconsider Y = { d where d is Element of NAT : ( d in dom f & f . d > p / 2 ) } as finite Subset of NAT by XBOOLE_1:1;
set Z = seq ((p div 4),(((p -' 1) div 2) -' (p div 4)));
A7:
p mod 8 <= 8 - 1
by INT_1:52, NAT_D:1;
8 = 2 * 4
;
then A8:
2 divides 8
;
for x being object st x in { k where k is Element of NAT : ( k in rng f & k > p / 2 ) } holds
x in rng f
then A10:
{ k where k is Element of NAT : ( k in rng f & k > p / 2 ) } c= rng f
;
then reconsider X = { k where k is Element of NAT : ( k in rng f & k > p / 2 ) } as finite set ;
card X is Element of NAT
;
then reconsider m = card { k where k is Element of NAT : ( k in rng f & k > p / 2 ) } as Element of NAT ;
A11:
len f = len fp
by EULER_2:def 2;
then A12:
dom f = dom fp
by FINSEQ_3:29;
assume A13:
p > 2
; Lege (2,p) = (- 1) |^ (((p ^2) -' 1) div 8)
then
2,p are_coprime
by EULER_1:2;
then A14:
2 gcd p = 1
by INT_2:def 3;
then A15:
Lege (2,p) = (- 1) |^ m
by A13, Th41;
p is odd
by A13, PEPIN:17;
then A16:
p - 1 is even
by HILBERT3:2;
then A17: (p -' 1) div 2 =
((p -' 1) + 1) div 2
by A2, NAT_2:26
.=
p div 2
by A1, XREAL_1:235
;
then A18:
f <> {}
by A13, A6, A11, NAT_2:13;
then reconsider U = dom f as non empty finite Subset of NAT ;
2 divides p -' 1
by A16, A2, PEPIN:22;
then A19:
p -' 1 = 2 * ((p -' 1) div 2)
;
A20:
for d being Nat st d in dom f holds
f . d = 2 * d
A22:
for d1, d2 being Nat st 1 <= d1 & d1 < d2 & d2 <= len f holds
f . d1 < f . d2
rng f is non empty Subset of NAT
by A18;
then consider n1 being Element of NAT such that
A29:
rng f c= (Seg n1) \/ {0}
by HEYTING3:1;
reconsider X = X as finite Subset of NAT by A10, XBOOLE_1:1;
seq ((p div 4),(((p -' 1) div 2) -' (p div 4))),((p -' 1) div 2) -' (p div 4) are_equipotent
by CALCUL_2:6;
then A30:
card (seq ((p div 4),(((p -' 1) div 2) -' (p div 4)))) = ((p -' 1) div 2) -' (p div 4)
by CARD_1:def 2;
not 0 in rng f
then
{0} misses rng f
by ZFMISC_1:50;
then
rng f c= Seg n1
by A29, XBOOLE_1:73;
then ddd:
rng f is included_in_Seg
by FINSEQ_1:def 13;
then A34:
Sgm (rng f) = f
by A22, FINSEQ_1:def 14;
A35:
X,Y are_equipotent
p div 2 < p
by INT_1:56;
then
(p div 2) div 2 <= p div 2
by NAT_2:24;
then A48:
p div (2 * 2) <= p div 2
by NAT_2:27;
A49:
seq ((p div 4),(((p -' 1) div 2) -' (p div 4))) c= Y
proof
let x be
object ;
TARSKI:def 3 ( not x in seq ((p div 4),(((p -' 1) div 2) -' (p div 4))) or x in Y )
assume A50:
x in seq (
(p div 4),
(((p -' 1) div 2) -' (p div 4)))
;
x in Y
then reconsider x =
x as
Element of
NAT ;
A51:
x >= (p div 4) + 1
by A50, CALCUL_2:1;
then
(p div 4) + x >= (p div 4) + 1
by NAT_1:12;
then A52:
x >= 1
by XREAL_1:6;
x <= (((p -' 1) div 2) -' (p div 4)) + (p div 4)
by A50, CALCUL_2:1;
then
x <= (p -' 1) div 2
by A17, A48, XREAL_1:235;
then A53:
x in dom f
by A6, A11, A52, FINSEQ_3:25;
x > p / 4
by A51, INT_1:29, XXREAL_0:2;
then
2
* x > 2
* (p / 4)
by XREAL_1:68;
then
f . x > p / 2
by A20, A53;
hence
x in Y
by A53;
verum
end;
now for x being object st x in Y holds
x in seq ((p div 4),(((p -' 1) div 2) -' (p div 4)))let x be
object ;
( x in Y implies x in seq ((p div 4),(((p -' 1) div 2) -' (p div 4))) )A54:
p / 4
>= [\(p / 4)/]
by INT_1:def 6;
assume
x in Y
;
x in seq ((p div 4),(((p -' 1) div 2) -' (p div 4)))then consider x1 being
Element of
NAT such that A55:
x1 = x
and A56:
x1 in dom f
and A57:
f . x1 > p / 2
;
2
* x1 > p / 2
by A20, A56, A57;
then
x1 > (p / 2) / 2
by XREAL_1:83;
then
x1 > [\(p / 4)/]
by A54, XXREAL_0:2;
then A58:
x1 >= (p div 4) + 1
by NAT_1:13;
x1 <= (p -' 1) div 2
by A6, A11, A56, FINSEQ_3:25;
then
x1 <= (((p -' 1) div 2) -' (p div 4)) + (p div 4)
by A17, A48, XREAL_1:235;
hence
x in seq (
(p div 4),
(((p -' 1) div 2) -' (p div 4)))
by A55, A58;
verum end;
then
Y c= seq ((p div 4),(((p -' 1) div 2) -' (p div 4)))
;
then
Y = seq ((p div 4),(((p -' 1) div 2) -' (p div 4)))
by A49, XBOOLE_0:def 10;
then A59:
m = ((p -' 1) div 2) -' (p div 4)
by A30, A35, CARD_1:5;
not not p mod 8 = 0 & ... & not p mod 8 = 7
by A7;
per cases then
( p mod 8 = 1 or p mod 8 = 3 or p mod 8 = 5 or p mod 8 = 7 )
by A9, A60, A61, A63;
suppose
p mod 8
= 7
;
Lege (2,p) = (- 1) |^ (((p ^2) -' 1) div 8)then A76:
p = (8 * (p div 8)) + 7
by NAT_D:2;
then
p -' 1
= 2
* ((4 * (p div 8)) + 3)
by A2;
then A77:
(p -' 1) div 2
= (4 * (p div 8)) + 3
;
A78:
4
* (p div 8) >= 2
* (p div 8)
by XREAL_1:64;
p div 4 =
((4 * ((2 * (p div 8)) + 1)) + 3) div 4
by A76
.=
((2 * (p div 8)) + 1) + (3 div 4)
by NAT_D:61
.=
((2 * (p div 8)) + 1) + 0
by NAT_D:27
;
then m =
((4 * (p div 8)) + 3) - ((2 * (p div 8)) + 1)
by A59, A77, A78, XREAL_1:7, XREAL_1:233
.=
(2 * (p div 8)) + 2
;
then A79:
Lege (2,
p) =
(- 1) |^ (2 * ((p div 8) + 1))
by A13, A14, Th41
.=
((- 1) |^ 2) |^ ((p div 8) + 1)
by NEWTON:9
.=
(1 |^ 2) |^ ((p div 8) + 1)
by WSIERP_1:1
.=
1
;
((p ^2) -' 1) div 8 =
((((8 * (8 * ((p div 8) ^2))) + (8 * (14 * (p div 8)))) + 49) - 1) div 8
by A76, NAT_1:12, XREAL_1:233
.=
(8 * (((8 * ((p div 8) ^2)) + (14 * (p div 8))) + 6)) div 8
.=
((8 * ((p div 8) ^2)) + (14 * (p div 8))) + 6
;
hence (- 1) |^ (((p ^2) -' 1) div 8) =
(- 1) |^ (2 * (((4 * ((p div 8) ^2)) + (7 * (p div 8))) + 3))
.=
((- 1) |^ 2) |^ (((4 * ((p div 8) ^2)) + (7 * (p div 8))) + 3)
by NEWTON:9
.=
(1 |^ 2) |^ (((4 * ((p div 8) ^2)) + (7 * (p div 8))) + 3)
by WSIERP_1:1
.=
Lege (2,
p)
by A79
;
verum end;