let p be Prime; :: thesis: for b being Nat st p > 2 & b gcd p = 1 & not b is_quadratic_residue_mod p holds
(b |^ ((p -' 1) div 2)) mod p = p - 1
let b be Nat; :: thesis: ( p > 2 & b gcd p = 1 & not b is_quadratic_residue_mod p implies (b |^ ((p -' 1) div 2)) mod p = p - 1 )
assume A1:
( p > 2 & b gcd p = 1 & not b is_quadratic_residue_mod p )
; :: thesis: (b |^ ((p -' 1) div 2)) mod p = p - 1
reconsider b = b as Element of NAT by ORDINAL1:def 13;
b,p are_relative_prime
by A1, INT_2:def 4;
then A2:
(b |^ (p -' 1)) mod p = 1
by PEPIN:38;
A3:
p > 1
by INT_2:def 5;
then A4:
1 mod p = 1
by NAT_D:14;
then A5:
((b |^ (p -' 1)) - 1) mod p = 0
by A2, INT_4:22;
not p is even
by A1, PEPIN:17;
then
p - 1 is even
by HILBERT3:2;
then
p -' 1 is even
by A3, XREAL_1:235;
then
2 divides p -' 1
by PEPIN:22;
then
p -' 1 = 2 * ((p -' 1) div 2)
by NAT_D:3;
then (b |^ (p -' 1)) - 1 =
((b |^ ((p -' 1) div 2)) |^ 2) - 1
by NEWTON:14
.=
((b |^ ((p -' 1) div 2)) ^2 ) - 1
by NEWTON:100
.=
((b |^ ((p -' 1) div 2)) + 1) * ((b |^ ((p -' 1) div 2)) - 1)
;
then A6:
p divides ((b |^ ((p -' 1) div 2)) + 1) * ((b |^ ((p -' 1) div 2)) - 1)
by A5, Lm1;
p - 1 > 2 - 1
by A1, XREAL_1:11;
then
p - 1 >= 1 + 1
by INT_1:20;
then
p -' 1 >= 2
by A3, XREAL_1:235;
then
(p -' 1) div 2 >= 2 div 2
by NAT_2:26;
then A7:
(p -' 1) div 2 >= 1
by PEPIN:48;
per cases
( (p -' 1) div 2 = 1 or (p -' 1) div 2 > 1 )
by A7, XXREAL_0:1;
suppose A11:
(p -' 1) div 2
> 1
;
:: thesis: (b |^ ((p -' 1) div 2)) mod p = p - 1set l =
(p -' 1) div 2;
set fs =
(<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0 )) ^ <*1*>;
A12:
(
- 1 is
Element of
INT & 1 is
Element of
INT &
0 is
Element of
INT )
by INT_1:def 2;
then A13:
(
<*(- 1)*> is
FinSequence of
INT &
<*1*> is
FinSequence of
INT )
by FINSEQ_1:95;
(((p -' 1) div 2) -' 1) |-> 0 is
FinSequence of
INT
by A12, FINSEQ_2:77;
then
<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0 ) is
FinSequence of
INT
by A13, FINSEQ_1:96;
then reconsider fs =
(<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0 )) ^ <*1*> as
FinSequence of
INT by A13, FINSEQ_1:96;
A14:
len fs =
len (<*(- 1)*> ^ (((((p -' 1) div 2) -' 1) |-> 0 ) ^ <*1*>))
by FINSEQ_1:45
.=
1
+ (len (((((p -' 1) div 2) -' 1) |-> 0 ) ^ <*1*>))
by FINSEQ_5:8
.=
(1 + (len ((((p -' 1) div 2) -' 1) |-> 0 ))) + 1
by FINSEQ_2:19
.=
1
+ ((((p -' 1) div 2) -' 1) + 1)
by FINSEQ_1:def 18
.=
1
+ ((p -' 1) div 2)
by A11, XREAL_1:237
;
A15:
len ((((p -' 1) div 2) -' 1) |-> 0 ) = ((p -' 1) div 2) -' 1
by FINSEQ_1:def 18;
set K1 =
<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0 );
A16:
len (<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0 )) =
1
+ (((p -' 1) div 2) -' 1)
by A15, FINSEQ_5:8
.=
(p -' 1) div 2
by A11, XREAL_1:237
;
then A17:
fs . (((p -' 1) div 2) + 1) = 1
by FINSEQ_1:59;
A18:
fs . 1 =
(<*(- 1)*> ^ (((((p -' 1) div 2) -' 1) |-> 0 ) ^ <*1*>)) . 1
by FINSEQ_1:45
.=
- 1
by FINSEQ_1:58
;
A19:
for
x being
Element of
INT holds
(Poly-INT fs) . x = (x |^ ((p -' 1) div 2)) - 1
proof
let x be
Element of
INT ;
:: thesis: (Poly-INT fs) . x = (x |^ ((p -' 1) div 2)) - 1
consider fr being
FinSequence of
INT such that A20:
(
len fr = len fs & ( for
d being
Nat st
d in dom fr holds
fr . d = (fs . d) * (x |^ (d -' 1)) ) &
(Poly-INT fs) . x = Sum fr )
by Def1;
fr = (<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0 )) ^ <*(x |^ ((p -' 1) div 2))*>
proof
set K =
(<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0 )) ^ <*(x |^ ((p -' 1) div 2))*>;
len ((<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0 )) ^ <*(x |^ ((p -' 1) div 2))*>) =
len (<*(- 1)*> ^ (((((p -' 1) div 2) -' 1) |-> 0 ) ^ <*(x |^ ((p -' 1) div 2))*>))
by FINSEQ_1:45
.=
1
+ (len (((((p -' 1) div 2) -' 1) |-> 0 ) ^ <*(x |^ ((p -' 1) div 2))*>))
by FINSEQ_5:8
.=
(1 + (len ((((p -' 1) div 2) -' 1) |-> 0 ))) + 1
by FINSEQ_2:19
.=
1
+ ((((p -' 1) div 2) -' 1) + 1)
by FINSEQ_1:def 18
.=
len fr
by A11, A14, A20, XREAL_1:237
;
then A21:
dom fr = dom ((<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0 )) ^ <*(x |^ ((p -' 1) div 2))*>)
by FINSEQ_3:31;
for
d being
Nat st
d in dom fr holds
fr . d = ((<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0 )) ^ <*(x |^ ((p -' 1) div 2))*>) . d
proof
let d be
Nat;
:: thesis: ( d in dom fr implies fr . d = ((<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0 )) ^ <*(x |^ ((p -' 1) div 2))*>) . d )
assume A22:
d in dom fr
;
:: thesis: fr . d = ((<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0 )) ^ <*(x |^ ((p -' 1) div 2))*>) . d
then
d in Seg (((p -' 1) div 2) + 1)
by A14, A20, FINSEQ_1:def 3;
then A23:
(
d >= 1 &
d <= ((p -' 1) div 2) + 1 )
by FINSEQ_1:3;
per cases
( d = 1 or ( d > 1 & d < ((p -' 1) div 2) + 1 ) or d = ((p -' 1) div 2) + 1 )
by A23, XXREAL_0:1;
suppose
(
d > 1 &
d < ((p -' 1) div 2) + 1 )
;
:: thesis: fr . d = ((<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0 )) ^ <*(x |^ ((p -' 1) div 2))*>) . dthen A26:
(
d - 1
> 0 &
d - 1
< (((p -' 1) div 2) + 1) - 1 )
by XREAL_1:11, XREAL_1:52;
then reconsider w =
d - 1 as
Element of
NAT by INT_1:16;
A27:
(
w <= ((p -' 1) div 2) -' 1 &
w >= 0 + 1 &
w < (p -' 1) div 2 )
by A26, INT_1:20, NAT_D:49;
then A28:
((((p -' 1) div 2) -' 1) |-> 0 ) . w = 0
by GOBRD10:def 3;
w in Seg (((p -' 1) div 2) -' 1)
by A27, FINSEQ_1:3;
then A29:
w in dom ((((p -' 1) div 2) -' 1) |-> 0 )
by A15, FINSEQ_1:def 3;
then A30:
(
w in dom (((((p -' 1) div 2) -' 1) |-> 0 ) ^ <*1*>) &
w in dom (((((p -' 1) div 2) -' 1) |-> 0 ) ^ <*(x |^ ((p -' 1) div 2))*>) )
by FINSEQ_2:18;
A31:
fs . d =
(<*(- 1)*> ^ (((((p -' 1) div 2) -' 1) |-> 0 ) ^ <*1*>)) . (w + 1)
by FINSEQ_1:45
.=
(((((p -' 1) div 2) -' 1) |-> 0 ) ^ <*1*>) . w
by A30, FINSEQ_3:112
.=
0
by A28, A29, FINSEQ_1:def 7
;
thus ((<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0 )) ^ <*(x |^ ((p -' 1) div 2))*>) . d =
(<*(- 1)*> ^ (((((p -' 1) div 2) -' 1) |-> 0 ) ^ <*(x |^ ((p -' 1) div 2))*>)) . (w + 1)
by FINSEQ_1:45
.=
(((((p -' 1) div 2) -' 1) |-> 0 ) ^ <*(x |^ ((p -' 1) div 2))*>) . w
by A30, FINSEQ_3:112
.=
(fs . d) * (x |^ (d -' 1))
by A28, A29, A31, FINSEQ_1:def 7
.=
fr . d
by A20, A22
;
:: thesis: verum end;
end;
hence
fr = (<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0 )) ^ <*(x |^ ((p -' 1) div 2))*>
by A21, FINSEQ_1:17;
:: thesis: verum
end;
then Sum fr =
Sum (<*(- 1)*> ^ (((((p -' 1) div 2) -' 1) |-> 0 ) ^ <*(x |^ ((p -' 1) div 2))*>))
by FINSEQ_1:45
.=
(- 1) + (Sum (((((p -' 1) div 2) -' 1) |-> 0 ) ^ <*(x |^ ((p -' 1) div 2))*>))
by RVSUM_1:106
.=
(- 1) + ((Sum ((((p -' 1) div 2) -' 1) |-> 0 )) + (x |^ ((p -' 1) div 2)))
by RVSUM_1:104
.=
(- 1) + (((((p -' 1) div 2) -' 1) * 0 ) + (x |^ ((p -' 1) div 2)))
by RVSUM_1:110
;
hence
(Poly-INT fs) . x = (x |^ ((p -' 1) div 2)) - 1
by A20;
:: thesis: verum
end; consider fp being
FinSequence of
NAT such that A34:
(
len fp = (p -' 1) div 2 & ( for
d being
Nat st
d in dom fp holds
(fp . d) gcd p = 1 ) & ( for
d being
Nat st
d in dom fp holds
fp . d is_quadratic_residue_mod p ) & ( for
d,
e being
Nat st
d in dom fp &
e in dom fp &
d <> e holds
not
fp . d,
fp . e are_congruent_mod p ) )
by A1, Th16;
now assume
p divides (b |^ ((p -' 1) div 2)) - 1
;
:: thesis: contradictionthen A35:
((b |^ ((p -' 1) div 2)) - 1) mod p = 0
by Lm1;
reconsider b =
b as
Element of
INT by INT_1:def 2;
A36:
((Poly-INT fs) . b) mod p = 0
by A19, A35;
set f =
fp ^ <*b*>;
<*b*> is
FinSequence of
NAT
by FINSEQ_1:95;
then reconsider f =
fp ^ <*b*> as
FinSequence of
NAT by FINSEQ_1:96;
A37:
len f = ((p -' 1) div 2) + 1
by A34, FINSEQ_2:19;
A38:
for
d being
Nat st
d in dom f holds
((Poly-INT fs) . (f . d)) mod p = 0
A42:
for
d,
e being
Nat st
d in dom f &
e in dom f &
d <> e holds
not
f . d,
f . e are_congruent_mod p
A55:
(
len fs = ((p -' 1) div 2) + 1 & not
p divides fs . (((p -' 1) div 2) + 1) &
p > 2 )
by A1, A3, A14, A17, NAT_D:7;
reconsider f =
f as
FinSequence of
INT by FINSEQ_2:27, NUMBERS:17;
len f <= (p -' 1) div 2
by A38, A42, A55, Th8;
hence
contradiction
by A37, XREAL_1:31;
:: thesis: verum end; then
p divides (b |^ ((p -' 1) div 2)) + 1
by A6, Th7;
then consider k being
Nat such that A56:
(b |^ ((p -' 1) div 2)) + 1
= p * k
by NAT_D:def 3;
- p < - 1
by A3, XREAL_1:26;
then A57:
(- 1) mod p = (- 1) + p
by INT_3:10;
(b |^ ((p -' 1) div 2)) mod p =
((p * k) + (- 1)) mod p
by A56
.=
p - 1
by A57, INT_3:8
;
hence
(b |^ ((p -' 1) div 2)) mod p = p - 1
;
:: thesis: verum end;