let p be Prime; :: thesis: ( p > 2 implies Lege 2,p = (- 1) |^ (((p ^2 ) -' 1) div 8) )
assume A1:
p > 2
; :: thesis: Lege 2,p = (- 1) |^ (((p ^2 ) -' 1) div 8)
then
2,p are_relative_prime
by EULER_1:3;
then A2:
2 gcd p = 1
by INT_2:def 4;
set p' = (p -' 1) div 2;
set I = idseq ((p -' 1) div 2);
set fp = 2 * (idseq ((p -' 1) div 2));
not p is even
by A1, PEPIN:17;
then A3:
p - 1 is even
by HILBERT3:2;
A4:
p > 1
by INT_2:def 5;
then A5:
p - 1 = p -' 1
by XREAL_1:235;
then
2 divides p -' 1
by A3, PEPIN:22;
then A6:
p -' 1 = 2 * ((p -' 1) div 2)
by NAT_D:3;
A7: (p -' 1) div 2 =
((p -' 1) + 1) div 2
by A3, A5, NAT_2:28
.=
p div 2
by A4, XREAL_1:237
;
A8:
p div 2 >= 1
by A1, NAT_2:15;
p div 2 < p
by INT_1:83;
then
(p div 2) div 2 <= p div 2
by NAT_2:26;
then A9:
p div (2 * 2) <= p div 2
by NAT_2:29;
A10:
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:14;
dom fp = dom (idseq ((p -' 1) div 2))
by VALUED_1:def 5;
then A13: len fp =
len (idseq ((p -' 1) div 2))
by FINSEQ_3:31
.=
(p -' 1) div 2
by FINSEQ_1:def 18
;
set f = fp mod p;
set X = { k where k is Element of NAT : ( k in rng (fp mod p) & k > p / 2 ) } ;
set m = card { k where k is Element of NAT : ( k in rng (fp mod p) & k > p / 2 ) } ;
set Y = { d where d is Element of NAT : ( d in dom (fp mod p) & (fp mod p) . d > p / 2 ) } ;
set Z = seq (p div 4),(((p -' 1) div 2) -' (p div 4));
for x being set st x in { d where d is Element of NAT : ( d in dom (fp mod p) & (fp mod p) . d > p / 2 ) } holds
x in dom (fp mod p)
then
{ d where d is Element of NAT : ( d in dom (fp mod p) & (fp mod p) . d > p / 2 ) } c= dom (fp mod p)
by TARSKI:def 3;
then reconsider Y = { d where d is Element of NAT : ( d in dom (fp mod p) & (fp mod p) . d > p / 2 ) } as finite Subset of NAT by XBOOLE_1:1;
for x being set st x in { k where k is Element of NAT : ( k in rng (fp mod p) & k > p / 2 ) } holds
x in rng (fp mod p)
then A16:
{ k where k is Element of NAT : ( k in rng (fp mod p) & k > p / 2 ) } c= rng (fp mod p)
by TARSKI:def 3;
then reconsider X = { k where k is Element of NAT : ( k in rng (fp mod p) & 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 (fp mod p) & k > p / 2 ) } as Element of NAT ;
A17:
Lege 2,p = (- 1) |^ m
by A1, A2, Th41;
rng (fp mod p) c= NAT
by FINSEQ_1:def 4;
then reconsider X = X as finite Subset of NAT by A16, XBOOLE_1:1;
A18:
len (fp mod p) = len fp
by EULER_2:def 1;
then A19:
dom (fp mod p) = dom fp
by FINSEQ_3:31;
A20:
for d being Nat st d in dom (fp mod p) holds
(fp mod p) . d = 2 * d
A22:
fp mod p <> {}
by A7, A8, A13, A18;
then
rng (fp mod p) is non empty Subset of NAT
by FINSEQ_1:def 4;
then consider n1 being Element of NAT such that
A23:
rng (fp mod p) c= (Seg n1) \/ {0 }
by HEYTING3:3;
not 0 in rng (fp mod p)
then A25:
{0 } misses rng (fp mod p)
by ZFMISC_1:56;
then A26:
rng (fp mod p) c= Seg n1
by A23, XBOOLE_1:73;
for d1, d2, k1, k2 being Nat st 1 <= d1 & d1 < d2 & d2 <= len (fp mod p) & k1 = (fp mod p) . d1 & k2 = (fp mod p) . d2 holds
k1 < k2
then A28:
Sgm (rng (fp mod p)) = fp mod p
by A26, FINSEQ_1:def 13;
A29:
Y = seq (p div 4),(((p -' 1) div 2) -' (p div 4))
proof
now let x be
set ;
:: thesis: ( x in Y implies x in seq (p div 4),(((p -' 1) div 2) -' (p div 4)) )assume
x in Y
;
:: thesis: x in seq (p div 4),(((p -' 1) div 2) -' (p div 4))then consider x1 being
Element of
NAT such that A30:
(
x1 = x &
x1 in dom (fp mod p) &
(fp mod p) . x1 > p / 2 )
;
2
* x1 > p / 2
by A20, A30;
then A31:
x1 > (p / 2) / 2
by XREAL_1:85;
p / 4
>= [\(p / 4)/]
by INT_1:def 4;
then
(
x1 > [\(p / 4)/] &
[\(p / 4)/] is
Element of
NAT )
by A31, INT_1:80, XXREAL_0:2;
then A32:
x1 >= (p div 4) + 1
by NAT_1:13;
x1 <= (p -' 1) div 2
by A13, A18, A30, FINSEQ_3:27;
then
x1 <= (((p -' 1) div 2) -' (p div 4)) + (p div 4)
by A7, A9, XREAL_1:237;
hence
x in seq (p div 4),
(((p -' 1) div 2) -' (p div 4))
by A30, A32;
:: thesis: verum end;
then A33:
Y c= seq (p div 4),
(((p -' 1) div 2) -' (p div 4))
by TARSKI:def 3;
seq (p div 4),
(((p -' 1) div 2) -' (p div 4)) c= Y
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in seq (p div 4),(((p -' 1) div 2) -' (p div 4)) or x in Y )
assume A34:
x in seq (p div 4),
(((p -' 1) div 2) -' (p div 4))
;
:: thesis: x in Y
then reconsider x =
x as
Element of
NAT ;
A35:
(
x >= (p div 4) + 1 &
x <= (((p -' 1) div 2) -' (p div 4)) + (p div 4) )
by A34, CALCUL_2:1;
then
(p div 4) + x >= (p div 4) + 1
by NAT_1:12;
then A36:
x >= 1
by XREAL_1:8;
(
x >= (p div 4) + 1 &
x <= (p -' 1) div 2 )
by A7, A9, A35, XREAL_1:237;
then A37:
x in dom (fp mod p)
by A13, A18, A36, FINSEQ_3:27;
x > p / 4
by A35, INT_1:52, XXREAL_0:2;
then
2
* x > 2
* (p / 4)
by XREAL_1:70;
then
(fp mod p) . x > p / 2
by A20, A37;
hence
x in Y
by A37;
:: thesis: verum
end;
hence
Y = seq (p div 4),
(((p -' 1) div 2) -' (p div 4))
by A33, XBOOLE_0:def 10;
:: thesis: verum
end;
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 A38: card (seq (p div 4),(((p -' 1) div 2) -' (p div 4))) =
card (((p -' 1) div 2) -' (p div 4))
by CARD_1:21
.=
((p -' 1) div 2) -' (p div 4)
by CARD_1:def 5
;
reconsider U = dom (fp mod p) as non empty finite Subset of NAT by A22;
X,Y are_equipotent
then A49:
m = ((p -' 1) div 2) -' (p div 4)
by A29, A38, CARD_1:21;
A50:
( 2 divides 8 & 4 divides 8 )
A51:
( p mod 8 = 1 or p mod 8 = 3 or p mod 8 = 5 or p mod 8 = 7 )
set nn = p div 8;
per cases
( p mod 8 = 1 or p mod 8 = 3 or p mod 8 = 5 or p mod 8 = 7 )
by A51;
suppose
p mod 8
= 7
;
:: thesis: Lege 2,p = (- 1) |^ (((p ^2 ) -' 1) div 8)then A69:
p = (8 * (p div 8)) + 7
by NAT_D:2;
then
p -' 1
= 2
* ((4 * (p div 8)) + 3)
by A5;
then A70:
(p -' 1) div 2
= (4 * (p div 8)) + 3
by NAT_D:18;
A71:
p div 4 =
((4 * ((2 * (p div 8)) + 1)) + 3) div 4
by A69
.=
((2 * (p div 8)) + 1) + (3 div 4)
by INT_3:8
.=
((2 * (p div 8)) + 1) + 0
by NAT_D:27
;
4
* (p div 8) >= 2
* (p div 8)
by XREAL_1:66;
then m =
((4 * (p div 8)) + 3) - ((2 * (p div 8)) + 1)
by A49, A70, A71, XREAL_1:9, XREAL_1:235
.=
(2 * (p div 8)) + 2
;
then A72:
Lege 2,
p =
(- 1) |^ (2 * ((p div 8) + 1))
by A1, A2, Th41
.=
((- 1) |^ 2) |^ ((p div 8) + 1)
by NEWTON:14
.=
(1 |^ 2) |^ ((p div 8) + 1)
by WSIERP_1:2
.=
1
|^ ((p div 8) + 1)
by NEWTON:15
.=
1
by NEWTON:15
;
((p ^2 ) -' 1) div 8 =
((((8 * (8 * ((p div 8) ^2 ))) + (8 * (14 * (p div 8)))) + 49) - 1) div 8
by A69, NAT_1:12, XREAL_1:235
.=
(8 * (((8 * ((p div 8) ^2 )) + (14 * (p div 8))) + 6)) div 8
.=
((8 * ((p div 8) ^2 )) + (14 * (p div 8))) + 6
by NAT_D:18
;
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:14
.=
(1 |^ 2) |^ (((4 * ((p div 8) ^2 )) + (7 * (p div 8))) + 3)
by WSIERP_1:2
.=
1
|^ (((4 * ((p div 8) ^2 )) + (7 * (p div 8))) + 3)
by NEWTON:15
.=
Lege 2,
p
by A72, NEWTON:15
;
:: thesis: verum end;