let p be Prime; :: thesis: ( 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
proof
let d be Nat; :: thesis: ( d in dom (2 * (idseq ((p -' 1) div 2))) implies (2 * (idseq ((p -' 1) div 2))) . d = 2 * d )
assume A4: d in dom (2 * (idseq ((p -' 1) div 2))) ; :: thesis: (2 * (idseq ((p -' 1) div 2))) . d = 2 * d
then d in dom (idseq ((p -' 1) div 2)) by VALUED_1:def 5;
then d in Seg (len (idseq ((p -' 1) div 2))) by FINSEQ_1:def 3;
then A5: d is Element of Seg ((p -' 1) div 2) by CARD_1:def 7;
thus (2 * (idseq ((p -' 1) div 2))) . d = 2 * ((idseq ((p -' 1) div 2)) . d) by
.= 2 * d by A5 ; :: thesis: verum
end;
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;
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 ) } ;
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 (fp mod p) & (fp mod p) . d > p / 2 ) } ;
for x being object 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)
proof
let x be object ; :: thesis: ( x in { d where d is Element of NAT : ( d in dom (fp mod p) & (fp mod p) . d > p / 2 ) } implies x in dom (fp mod p) )
assume x in { d where d is Element of NAT : ( d in dom (fp mod p) & (fp mod p) . d > p / 2 ) } ; :: thesis: x in dom (fp mod p)
then ex k being Element of NAT st
( x = k & k in dom (fp mod p) & (fp mod p) . k > p / 2 ) ;
hence x in dom (fp mod p) ; :: thesis: verum
end;
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) ;
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;
set Z = seq ((p div 4),(((p -' 1) div 2) -' (p div 4)));
A7: p mod 8 <= 8 - 1 by ;
8 = 2 * 4 ;
then A8: 2 divides 8 ;
A9: now :: thesis: not p mod 8 = 0 end;
for x being object 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)
proof
let x be object ; :: thesis: ( x in { k where k is Element of NAT : ( k in rng (fp mod p) & k > p / 2 ) } implies x in rng (fp mod p) )
assume x in { k where k is Element of NAT : ( k in rng (fp mod p) & k > p / 2 ) } ; :: thesis: x in rng (fp mod p)
then ex k being Element of NAT st
( x = k & k in rng (fp mod p) & k > p / 2 ) ;
hence x in rng (fp mod p) ; :: thesis: verum
end;
then A10: { k where k is Element of NAT : ( k in rng (fp mod p) & k > p / 2 ) } c= rng (fp mod p) ;
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 ;
A11: len (fp mod p) = len fp by EULER_2:def 1;
then A12: dom (fp mod p) = dom fp by FINSEQ_3:29;
assume A13: p > 2 ; :: thesis: 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 ;
p is odd by ;
then A16: p - 1 is even by HILBERT3:2;
then A17: (p -' 1) div 2 = ((p -' 1) + 1) div 2 by
.= p div 2 by ;
then A18: fp mod p <> {} by ;
then reconsider U = dom (fp mod p) as non empty finite Subset of NAT ;
2 divides p -' 1 by ;
then A19: p -' 1 = 2 * ((p -' 1) div 2) by NAT_D:3;
A20: for d being Nat st d in dom (fp mod p) holds
(fp mod p) . d = 2 * d
proof
let d be Nat; :: thesis: ( d in dom (fp mod p) implies (fp mod p) . d = 2 * d )
assume A21: d in dom (fp mod p) ; :: thesis: (fp mod p) . d = 2 * d
then d <= (p -' 1) div 2 by ;
then 2 * d <= p -' 1 by ;
then 2 * d < p by ;
hence 2 * d = (2 * d) mod p by NAT_D:24
.= (fp . d) mod p by A3, A12, A21
.= (fp mod p) . d by ;
:: thesis: verum
end;
A22: 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
proof
let d1, d2, k1, k2 be Nat; :: thesis: ( 1 <= d1 & d1 < d2 & d2 <= len (fp mod p) & k1 = (fp mod p) . d1 & k2 = (fp mod p) . d2 implies k1 < k2 )
assume that
A23: 1 <= d1 and
A24: d1 < d2 and
A25: d2 <= len (fp mod p) and
A26: k1 = (fp mod p) . d1 and
A27: k2 = (fp mod p) . d2 ; :: thesis: k1 < k2
1 <= d2 by ;
then d2 in dom (fp mod p) by ;
then A28: k2 = 2 * d2 by ;
d1 <= len (fp mod p) by ;
then d1 in dom (fp mod p) by ;
then k1 = 2 * d1 by ;
hence k1 < k2 by ; :: thesis: verum
end;
rng (fp mod p) is non empty Subset of NAT by A18;
then consider n1 being Element of NAT such that
A29: rng (fp mod p) c= (Seg n1) \/ by HEYTING3:1;
reconsider X = X as finite Subset of NAT by ;
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 (fp mod p)
proof
assume 0 in rng (fp mod p) ; :: thesis: contradiction
then consider n being Nat such that
A31: n in dom (fp mod p) and
A32: (fp mod p) . n = 0 by FINSEQ_2:10;
2 * n = 0 by ;
hence contradiction by A31, FINSEQ_3:25; :: thesis: verum
end;
then A33: {0} misses rng (fp mod p) by ZFMISC_1:50;
then rng (fp mod p) c= Seg n1 by ;
then A34: Sgm (rng (fp mod p)) = fp mod p by ;
A35: X,Y are_equipotent
proof
deffunc H1( Element of U) -> Element of omega = (fp mod p) . \$1;
set YY = { d where d is Element of U : H1(d) in X } ;
A36: now :: thesis: for x being set st x in X holds
ex d being Element of U st x = H1(d)
let x be set ; :: thesis: ( x in X implies ex d being Element of U st x = H1(d) )
assume x in X ; :: thesis: ex d being Element of U st x = H1(d)
then consider y being Element of NAT such that
A37: y = x and
A38: y in rng (fp mod p) and
y > p / 2 ;
consider d being Nat such that
A39: d in U and
A40: (fp mod p) . d = y by ;
reconsider d = d as Element of U by A39;
take d = d; :: thesis: x = H1(d)
thus x = H1(d) by ; :: thesis: verum
end;
A41: Y c= { d where d is Element of U : H1(d) in X }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in { d where d is Element of U : H1(d) in X } )
assume x in Y ; :: thesis: x in { d where d is Element of U : H1(d) in X }
then A42: ex d being Element of NAT st
( d = x & d in dom (fp mod p) & (fp mod p) . d > p / 2 ) ;
then reconsider x = x as Element of U ;
reconsider f = fp mod p as FinSequence of NAT ;
f . x in rng f by FUNCT_1:3;
then H1(x) in X by A42;
hence x in { d where d is Element of U : H1(d) in X } ; :: thesis: verum
end;
now :: thesis: for x being object st x in { d where d is Element of U : H1(d) in X } holds
x in Y
let x be object ; :: thesis: ( x in { d where d is Element of U : H1(d) in X } implies x in Y )
assume x in { d where d is Element of U : H1(d) in X } ; :: thesis: x in Y
then consider d being Element of U such that
A43: d = x and
A44: (fp mod p) . d in X ;
ex k being Element of NAT st
( k = (fp mod p) . d & k in rng (fp mod p) & k > p / 2 ) by A44;
hence x in Y by A43; :: thesis: verum
end;
then A45: { d where d is Element of U : H1(d) in X } c= Y ;
A46: for d1, d2 being Element of U st H1(d1) = H1(d2) holds
d1 = d2
proof
let d1, d2 be Element of U; :: thesis: ( H1(d1) = H1(d2) implies d1 = d2 )
assume A47: H1(d1) = H1(d2) ; :: thesis: d1 = d2
fp mod p is one-to-one by ;
hence d1 = d2 by A47; :: thesis: verum
end;
X, { d where d is Element of U : H1(d) in X } are_equipotent from hence X,Y are_equipotent by ; :: thesis: verum
end;
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 ; :: 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 A50: 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 ;
A51: x >= (p div 4) + 1 by ;
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 ;
then x <= (p -' 1) div 2 by ;
then A53: x in dom (fp mod p) by ;
x > p / 4 by ;
then 2 * x > 2 * (p / 4) by XREAL_1:68;
then (fp mod p) . x > p / 2 by ;
hence x in Y by A53; :: thesis: verum
end;
now :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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 (fp mod p) and
A57: (fp mod p) . x1 > p / 2 ;
2 * x1 > p / 2 by ;
then x1 > (p / 2) / 2 by XREAL_1:83;
then x1 > [\(p / 4)/] by ;
then A58: x1 >= (p div 4) + 1 by NAT_1:13;
x1 <= (p -' 1) div 2 by ;
then x1 <= (((p -' 1) div 2) -' (p div 4)) + (p div 4) by ;
hence x in seq ((p div 4),(((p -' 1) div 2) -' (p div 4))) by ; :: thesis: 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 ;
then A59: m = ((p -' 1) div 2) -' (p div 4) by ;
A60: now :: thesis: not p mod 8 = 2end;
A61: now :: thesis: not p mod 8 = 4end;
A63: now :: thesis: not p mod 8 = 6end;
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 = 1 ; :: thesis: Lege (2,p) = (- 1) |^ (((p ^2) -' 1) div 8)
then A65: p = (8 * (p div 8)) + 1 by NAT_D:2;
then p -' 1 = 2 * (4 * (p div 8)) by A2;
then A66: (p -' 1) div 2 = 4 * (p div 8) by NAT_D:18;
p div 4 = ((4 * (2 * (p div 8))) + 1) div 4 by A65
.= (2 * (p div 8)) + (1 div 4) by NAT_D:61
.= (2 * (p div 8)) + 0 by NAT_D:27 ;
then m = (4 * (p div 8)) - (2 * (p div 8)) by
.= 2 * (p div 8) ;
then A67: Lege (2,p) = ((- 1) |^ 2) |^ (p div 8) by
.= (1 |^ 2) |^ (p div 8) by WSIERP_1:1
.= 1 ;
((p ^2) -' 1) div 8 = (((((8 * (p div 8)) ^2) + (2 * (8 * (p div 8)))) + 1) -' 1) div 8 by A65
.= (8 * ((8 * ((p div 8) ^2)) + (2 * (p div 8)))) div 8 by NAT_D:34
.= (8 * ((p div 8) ^2)) + (2 * (p div 8)) by NAT_D:18 ;
hence (- 1) |^ (((p ^2) -' 1) div 8) = (- 1) |^ (2 * ((4 * ((p div 8) ^2)) + (p div 8)))
.= ((- 1) |^ 2) |^ ((4 * ((p div 8) ^2)) + (p div 8)) by NEWTON:9
.= (1 |^ 2) |^ ((4 * ((p div 8) ^2)) + (p div 8)) by WSIERP_1:1
.= Lege (2,p) by A67 ;
:: thesis: verum
end;
suppose p mod 8 = 3 ; :: thesis: Lege (2,p) = (- 1) |^ (((p ^2) -' 1) div 8)
then A68: p = (8 * (p div 8)) + 3 by NAT_D:2;
then p -' 1 = 2 * ((4 * (p div 8)) + 1) by A2;
then A69: (p -' 1) div 2 = (4 * (p div 8)) + 1 by NAT_D:18;
A70: 4 * (p div 8) >= 2 * (p div 8) by XREAL_1:64;
p div 4 = ((4 * (2 * (p div 8))) + 3) div 4 by A68
.= (2 * (p div 8)) + (3 div 4) by NAT_D:61
.= (2 * (p div 8)) + 0 by NAT_D:27 ;
then m = ((4 * (p div 8)) + 1) - (2 * (p div 8)) by
.= (2 * (p div 8)) + 1 ;
then A71: Lege (2,p) = ((- 1) |^ (2 * (p div 8))) * (- 1) by
.= (((- 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 * (6 * (p div 8)))) + (3 * 3)) - 1) div 8 by
.= (8 * (((8 * ((p div 8) ^2)) + (6 * (p div 8))) + 1)) div 8
.= ((8 * ((p div 8) ^2)) + (6 * (p div 8))) + 1 by NAT_D:18 ;
hence (- 1) |^ (((p ^2) -' 1) div 8) = ((- 1) |^ (2 * ((4 * ((p div 8) ^2)) + (3 * (p div 8))))) * (- 1) by NEWTON:6
.= (((- 1) |^ 2) |^ ((4 * ((p div 8) ^2)) + (3 * (p div 8)))) * (- 1) by NEWTON:9
.= ((1 |^ 2) |^ ((4 * ((p div 8) ^2)) + (3 * (p div 8)))) * (- 1) by WSIERP_1:1
.= Lege (2,p) by A71 ;
:: thesis: verum
end;
suppose p mod 8 = 5 ; :: thesis: Lege (2,p) = (- 1) |^ (((p ^2) -' 1) div 8)
then A72: p = (8 * (p div 8)) + 5 by NAT_D:2;
then p -' 1 = 2 * ((4 * (p div 8)) + 2) by A2;
then A73: (p -' 1) div 2 = (4 * (p div 8)) + 2 by NAT_D:18;
A74: 4 * (p div 8) >= 2 * (p div 8) by XREAL_1:64;
p div 4 = ((4 * ((2 * (p div 8)) + 1)) + 1) div 4 by A72
.= ((2 * (p div 8)) + 1) + (1 div 4) by NAT_D:61
.= ((2 * (p div 8)) + 1) + 0 by NAT_D:27 ;
then m = ((4 * (p div 8)) + 2) - ((2 * (p div 8)) + 1) by
.= (2 * (p div 8)) + 1 ;
then A75: Lege (2,p) = ((- 1) |^ (2 * (p div 8))) * (- 1) by
.= (((- 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 * (10 * (p div 8)))) + 25) - 1) div 8 by
.= (8 * (((8 * ((p div 8) ^2)) + (10 * (p div 8))) + 3)) div 8
.= ((8 * ((p div 8) ^2)) + (10 * (p div 8))) + 3 by NAT_D:18 ;
hence (- 1) |^ (((p ^2) -' 1) div 8) = (- 1) |^ ((((2 * (4 * ((p div 8) ^2))) + (2 * (5 * (p div 8)))) + (2 * 1)) + 1)
.= ((- 1) |^ (2 * (((4 * ((p div 8) ^2)) + (5 * (p div 8))) + 1))) * (- 1) by NEWTON:6
.= (((- 1) |^ 2) |^ (((4 * ((p div 8) ^2)) + (5 * (p div 8))) + 1)) * (- 1) by NEWTON:9
.= ((1 |^ 2) |^ (((4 * ((p div 8) ^2)) + (5 * (p div 8))) + 1)) * (- 1) by WSIERP_1:1
.= Lege (2,p) by A75 ;
:: thesis: verum
end;
suppose p mod 8 = 7 ; :: thesis: 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 by NAT_D:18;
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
.= (2 * (p div 8)) + 2 ;
then A79: Lege (2,p) = (- 1) |^ (2 * ((p div 8) + 1)) by
.= ((- 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
.= (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:9
.= (1 |^ 2) |^ (((4 * ((p div 8) ^2)) + (7 * (p div 8))) + 3) by WSIERP_1:1
.= Lege (2,p) by A79 ;
:: thesis: verum
end;
end;