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 that
A1: p > 2 and
A2: b gcd p = 1 and
A3: 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 12;
A4: p > 1 by INT_2:def 4;
then A5: 1 mod p = 1 by NAT_D:14;
p is odd by ;
then p - 1 is even by HILBERT3:2;
then p -' 1 is even by ;
then 2 divides p -' 1 by PEPIN:22;
then p -' 1 = 2 * ((p -' 1) div 2) by NAT_D:3;
then A6: (b |^ (p -' 1)) - 1 = ((b |^ ((p -' 1) div 2)) |^ 2) - 1 by NEWTON:9
.= ((b |^ ((p -' 1) div 2)) ^2) - 1 by NEWTON:81
.= ((b |^ ((p -' 1) div 2)) + 1) * ((b |^ ((p -' 1) div 2)) - 1) ;
b,p are_coprime by ;
then (b |^ (p -' 1)) mod p = 1 by PEPIN:37;
then ((b |^ (p -' 1)) - 1) mod p = 0 by ;
then A7: p divides ((b |^ ((p -' 1) div 2)) + 1) * ((b |^ ((p -' 1) div 2)) - 1) by ;
p - 1 > 2 - 1 by ;
then p - 1 >= 1 + 1 by INT_1:7;
then p -' 1 >= 2 by ;
then (p -' 1) div 2 >= 2 div 2 by NAT_2:24;
then A8: (p -' 1) div 2 >= 1 by PEPIN:44;
per cases ) div 2 = 1 or (p -' 1) div 2 > 1 ) by ;
suppose A9: (p -' 1) div 2 = 1 ; :: thesis: (b |^ ((p -' 1) div 2)) mod p = p - 1
A10: now :: thesis: not p divides b - 1
assume p divides b - 1 ; :: thesis: contradiction
then p divides - (b - 1) by INT_2:10;
then ((1 ^2) - b) mod p = 0 by Lm1;
hence contradiction by A3; :: thesis: verum
end;
p divides (b + 1) * ((b |^ 1) - 1) by A7, A9;
then p divides b - (- 1) by ;
then b, - 1 are_congruent_mod p ;
then A11: b mod p = (- 1) mod p by NAT_D:64;
- p < - 2 by ;
then - p < (- 2) + 1 by XREAL_1:39;
then b mod p = p - 1 by ;
hence (b |^ ((p -' 1) div 2)) mod p = p - 1 by A9; :: thesis: verum
end;
suppose A12: (p -' 1) div 2 > 1 ; :: thesis: (b |^ ((p -' 1) div 2)) mod p = p - 1
set l = (p -' 1) div 2;
0 is Element of INT by INT_1:def 2;
then A13: (((p -' 1) div 2) -' 1) |-> 0 is FinSequence of INT by FINSEQ_2:63;
set K1 = <*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0);
A14: len ((((p -' 1) div 2) -' 1) |-> 0) = ((p -' 1) div 2) -' 1 by CARD_1:def 7;
A15: len (<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0)) = 1 + (((p -' 1) div 2) -' 1) by CARD_1:def 7
.= (p -' 1) div 2 by ;
set fs = (<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0)) ^ <*1*>;
1 is Element of INT by INT_1:def 2;
then A16: <*1*> is FinSequence of INT by FINSEQ_1:74;
- 1 is Element of INT by INT_1:def 2;
then <*(- 1)*> is FinSequence of INT by FINSEQ_1:74;
then <*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0) is FinSequence of INT by ;
then reconsider fs = (<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0)) ^ <*1*> as FinSequence of INT by ;
A17: len fs = 1 + ((((p -' 1) div 2) -' 1) + 1) by CARD_1:def 7
.= 1 + ((p -' 1) div 2) by ;
A18: fs . 1 = (<*(- 1)*> ^ (((((p -' 1) div 2) -' 1) |-> 0) ^ <*1*>)) . 1 by FINSEQ_1:32
.= - 1 by FINSEQ_1:41 ;
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 and
A21: for d being Nat st d in dom fr holds
fr . d = (fs . d) * (x |^ (d -' 1)) and
A22: (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))*>;
A23: 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 A24: d in dom fr ; :: thesis: fr . d = ((<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0)) ^ <*(x |^ ((p -' 1) div 2))*>) . d
then A25: d in Seg (((p -' 1) div 2) + 1) by ;
then A26: d >= 1 by FINSEQ_1:1;
A27: d <= ((p -' 1) div 2) + 1 by ;
per cases ( d = 1 or ( d > 1 & d < ((p -' 1) div 2) + 1 ) or d = ((p -' 1) div 2) + 1 ) by ;
suppose A28: d = 1 ; :: thesis: fr . d = ((<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0)) ^ <*(x |^ ((p -' 1) div 2))*>) . d
then A29: fr . 1 = (fs . 1) * (x |^ (1 -' 1)) by
.= (fs . 1) * (x |^ 0) by XREAL_1:232
.= (fs . 1) * 1 by NEWTON:4
.= - 1 by A18 ;
((<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0)) ^ <*(x |^ ((p -' 1) div 2))*>) . 1 = (<*(- 1)*> ^ (((((p -' 1) div 2) -' 1) |-> 0) ^ <*(x |^ ((p -' 1) div 2))*>)) . 1 by FINSEQ_1:32
.= fr . 1 by ;
hence fr . d = ((<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0)) ^ <*(x |^ ((p -' 1) div 2))*>) . d by A28; :: thesis: verum
end;
suppose A30: ( d > 1 & d < ((p -' 1) div 2) + 1 ) ; :: thesis: fr . d = ((<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0)) ^ <*(x |^ ((p -' 1) div 2))*>) . d
then reconsider w = d - 1 as Element of NAT by INT_1:3;
d - 1 < (((p -' 1) div 2) + 1) - 1 by ;
then A31: w <= ((p -' 1) div 2) -' 1 by NAT_D:49;
A32: w >= 0 + 1 by ;
A33: ((((p -' 1) div 2) -' 1) |-> 0) . w = 0 ;
w in Seg (((p -' 1) div 2) -' 1) by ;
then A34: w in dom ((((p -' 1) div 2) -' 1) |-> 0) by ;
then A35: w in dom (((((p -' 1) div 2) -' 1) |-> 0) ^ <*1*>) by FINSEQ_2:15;
A36: w in dom (((((p -' 1) div 2) -' 1) |-> 0) ^ <*(x |^ ((p -' 1) div 2))*>) by ;
A37: fs . d = (<*(- 1)*> ^ (((((p -' 1) div 2) -' 1) |-> 0) ^ <*1*>)) . (w + 1) by FINSEQ_1:32
.= (((((p -' 1) div 2) -' 1) |-> 0) ^ <*1*>) . w by
.= 0 by ;
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:32
.= (((((p -' 1) div 2) -' 1) |-> 0) ^ <*(x |^ ((p -' 1) div 2))*>) . w by
.= (fs . d) * (x |^ (d -' 1)) by
.= fr . d by ; :: thesis: verum
end;
suppose A38: d = ((p -' 1) div 2) + 1 ; :: thesis: fr . d = ((<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0)) ^ <*(x |^ ((p -' 1) div 2))*>) . d
then d in dom fs by ;
then A39: d in dom fr by ;
fs . d = 1 by ;
hence fr . d = 1 * (x |^ ((((p -' 1) div 2) + 1) -' 1)) by
.= x |^ ((p -' 1) div 2) by NAT_D:34
.= ((<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0)) ^ <*(x |^ ((p -' 1) div 2))*>) . d by ;
:: thesis: verum
end;
end;
end;
len ((<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0)) ^ <*(x |^ ((p -' 1) div 2))*>) = 1 + ((((p -' 1) div 2) -' 1) + 1) by CARD_1:def 7
.= len fr by ;
hence fr = (<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0)) ^ <*(x |^ ((p -' 1) div 2))*> by ; :: thesis: verum
end;
then Sum fr = Sum (<*(- 1)*> ^ (((((p -' 1) div 2) -' 1) |-> 0) ^ <*(x |^ ((p -' 1) div 2))*>)) by FINSEQ_1:32
.= (- 1) + (Sum (((((p -' 1) div 2) -' 1) |-> 0) ^ <*(x |^ ((p -' 1) div 2))*>)) by RVSUM_1:76
.= (- 1) + ((Sum ((((p -' 1) div 2) -' 1) |-> 0)) + (x |^ ((p -' 1) div 2))) by RVSUM_1:74
.= (- 1) + (((((p -' 1) div 2) -' 1) * 0) + (x |^ ((p -' 1) div 2))) by RVSUM_1:80 ;
hence (Poly-INT fs) . x = (x |^ ((p -' 1) div 2)) - 1 by A22; :: thesis: verum
end;
consider fp being FinSequence of NAT such that
A40: len fp = (p -' 1) div 2 and
A41: for d being Nat st d in dom fp holds
(fp . d) gcd p = 1 and
A42: for d being Nat st d in dom fp holds
fp . d is_quadratic_residue_mod p and
A43: 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 ;
A44: fs . (((p -' 1) div 2) + 1) = 1 by ;
now :: thesis: not p divides (b |^ ((p -' 1) div 2)) - 1
assume p divides (b |^ ((p -' 1) div 2)) - 1 ; :: thesis: contradiction
then A45: ((b |^ ((p -' 1) div 2)) - 1) mod p = 0 by Lm1;
reconsider b = b as Element of INT by INT_1:def 2;
set f = fp ^ <*b*>;
<*b*> is FinSequence of NAT by FINSEQ_1:74;
then reconsider f = fp ^ <*b*> as FinSequence of NAT by FINSEQ_1:75;
A46: len f = ((p -' 1) div 2) + 1 by ;
A47: 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
proof
let d, e be Nat; :: thesis: ( d in dom f & e in dom f & d <> e implies not f . d,f . e are_congruent_mod p )
assume that
A48: d in dom f and
A49: e in dom f and
A50: d <> e ; :: thesis: not f . d,f . e are_congruent_mod p
A51: e >= 1 by ;
A52: d <= ((p -' 1) div 2) + 1 by ;
A53: e <= ((p -' 1) div 2) + 1 by ;
per cases ( ( d >= 1 & d < ((p -' 1) div 2) + 1 ) or d = ((p -' 1) div 2) + 1 ) by ;
suppose A54: ( d >= 1 & d < ((p -' 1) div 2) + 1 ) ; :: thesis: not f . d,f . e are_congruent_mod p
then d <= (p -' 1) div 2 by NAT_1:13;
then A55: d in dom fp by ;
then A56: f . d = fp . d by FINSEQ_1:def 7;
per cases ( ( e >= 1 & e < ((p -' 1) div 2) + 1 ) or e = ((p -' 1) div 2) + 1 ) by ;
suppose A57: ( e >= 1 & e < ((p -' 1) div 2) + 1 ) ; :: thesis: not f . d,f . e are_congruent_mod p
end;
suppose A59: e = ((p -' 1) div 2) + 1 ; :: thesis: not f . d,f . e are_congruent_mod p
not f . d,b are_congruent_mod p
proof
f . d is_quadratic_residue_mod p by ;
then consider j being Integer such that
A60: ((j ^2) - (f . d)) mod p = 0 ;
assume a61: f . d,b are_congruent_mod p ; :: thesis: contradiction
p divides (j ^2) - (f . d) by ;
then p divides ((j ^2) - (f . d)) + ((f . d) - b) by ;
then ((j ^2) - b) mod p = 0 by INT_1:62;
hence contradiction by A3; :: thesis: verum
end;
hence not f . d,f . e are_congruent_mod p by ; :: thesis: verum
end;
end;
end;
suppose A62: d = ((p -' 1) div 2) + 1 ; :: thesis: not f . d,f . e are_congruent_mod p
then e <= (p -' 1) div 2 by ;
then A63: e in dom fp by ;
then f . e = fp . e by FINSEQ_1:def 7;
then f . e is_quadratic_residue_mod p by ;
then consider j being Integer such that
A64: ((j ^2) - (f . e)) mod p = 0 ;
A65: p divides (j ^2) - (f . e) by ;
not b,f . e are_congruent_mod p
proof
assume b,f . e are_congruent_mod p ; :: thesis: contradiction
then p divides ((j ^2) - (f . e)) - (b - (f . e)) by ;
then ((j ^2) - b) mod p = 0 by INT_1:62;
hence contradiction by A3; :: thesis: verum
end;
hence not f . d,f . e are_congruent_mod p by ; :: thesis: verum
end;
end;
end;
A66: ((Poly-INT fs) . b) mod p = 0 by ;
A67: for d being Nat st d in dom f holds
((Poly-INT fs) . (f . d)) mod p = 0
proof
let d be Nat; :: thesis: ( d in dom f implies ((Poly-INT fs) . (f . d)) mod p = 0 )
assume d in dom f ; :: thesis: ((Poly-INT fs) . (f . d)) mod p = 0
then A68: d in Seg (((p -' 1) div 2) + 1) by ;
then A69: d <= ((p -' 1) div 2) + 1 by FINSEQ_1:1;
per cases ( ( d >= 1 & d < ((p -' 1) div 2) + 1 ) or d = ((p -' 1) div 2) + 1 ) by ;
suppose A70: ( d >= 1 & d < ((p -' 1) div 2) + 1 ) ; :: thesis: ((Poly-INT fs) . (f . d)) mod p = 0
reconsider k = fp . d as Element of INT by INT_1:def 2;
d <= (p -' 1) div 2 by ;
then A71: d in dom fp by ;
then (fp . d) gcd p = 1 by A41;
then ((fp . d) |^ ((p -' 1) div 2)) mod p = 1 mod p by A1, A5, A42, A71, Th17;
then ((k |^ ((p -' 1) div 2)) - 1) mod p = 0 by INT_4:22;
then ((Poly-INT fs) . k) mod p = 0 by A19;
hence ((Poly-INT fs) . (f . d)) mod p = 0 by ; :: thesis: verum
end;
suppose d = ((p -' 1) div 2) + 1 ; :: thesis: ((Poly-INT fs) . (f . d)) mod p = 0
hence ((Poly-INT fs) . (f . d)) mod p = 0 by ; :: thesis: verum
end;
end;
end;
reconsider f = f as FinSequence of INT by ;
not p divides fs . (((p -' 1) div 2) + 1) by ;
then len f <= (p -' 1) div 2 by A1, A17, A67, A47, Th8;
hence contradiction by A46, XREAL_1:29; :: thesis: verum
end;
then p divides (b |^ ((p -' 1) div 2)) + 1 by ;
then consider k being Nat such that
A72: (b |^ ((p -' 1) div 2)) + 1 = p * k by NAT_D:def 3;
- p < - 1 by ;
then A73: (- 1) mod p = (- 1) + p by NAT_D:63;
(b |^ ((p -' 1) div 2)) mod p = ((p * k) + (- 1)) mod p by A72
.= p - 1 by ;
hence (b |^ ((p -' 1) div 2)) mod p = p - 1 ; :: thesis: verum
end;
end;