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 A1, PEPIN:17;
then p - 1 is even by HILBERT3:2;
then p -' 1 is even by A4, XREAL_1:233;
then 2 divides p -' 1 by PEPIN:22;
then p -' 1 = 2 * ((p -' 1) div 2) ;
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 A2, INT_2:def 3;
then (b |^ (p -' 1)) mod p = 1 by PEPIN:37;
then ((b |^ (p -' 1)) - 1) mod p = 0 by A5, INT_4:22;
then A7: p divides ((b |^ ((p -' 1) div 2)) + 1) * ((b |^ ((p -' 1) div 2)) - 1) by A6, Lm1;
p - 1 > 2 - 1 by A1, XREAL_1:9;
then p - 1 >= 1 + 1 by INT_1:7;
then p -' 1 >= 2 by A4, XREAL_1:233;
then (p -' 1) div 2 >= 2 div 2 by NAT_2:24;
then A8: (p -' 1) div 2 >= 1 ;

per cases ( (p -' 1) div 2 = 1 or (p -' 1) div 2 > 1 ) by A8, XXREAL_0:1;

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 A10, Th7;
then b, - 1 are_congruent_mod p ;
then A11: b mod p = (- 1) mod p by NAT_D:64;
- p < - 2 by A1, XREAL_1:24;
then - p < (- 2) + 1 by XREAL_1:39;
then b mod p = p - 1 by A11, NAT_D:63;
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;
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 A12, XREAL_1:235 ;
set fs = (<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0)) ^ <*1*>;
reconsider fs = (<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0)) ^ <*1*> as FinSequence of INT by FINSEQ_1:75;
A17: len fs = 1 + ((((p -' 1) div 2) -' 1) + 1) by CARD_1:def 7
.= 1 + ((p -' 1) div 2) by A12, XREAL_1:235 ;
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 A17, A20, FINSEQ_1:def 3;
then A26: d >= 1 by FINSEQ_1:1;
A27: d <= ((p -' 1) div 2) + 1 by A25, FINSEQ_1:1;

per cases ( d = 1 or ( d > 1 & d < ((p -' 1) div 2) + 1 ) or d = ((p -' 1) div 2) + 1 ) by A26, A27, XXREAL_0:1;

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 A21, A24
.= (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 A29, FINSEQ_1:41 ;
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 A30, XREAL_1:9;
then A31: w <= ((p -' 1) div 2) -' 1 by NAT_D:49;
A32: w >= 0 + 1 by A30, INT_1:7, XREAL_1:50;
A33: ((((p -' 1) div 2) -' 1) |-> 0) . w = 0 ;
w in Seg (((p -' 1) div 2) -' 1) by A31, A32, FINSEQ_1:1;
then A34: w in dom ((((p -' 1) div 2) -' 1) |-> 0) by A14, FINSEQ_1:def 3;
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 A34, FINSEQ_2:15;
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 A35, FINSEQ_3:103
.= 0 by A33, A34, 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:32
.= (((((p -' 1) div 2) -' 1) |-> 0) ^ <*(x |^ ((p -' 1) div 2))*>) . w by A36, FINSEQ_3:103
.= (fs . d) * (x |^ (d -' 1)) by A33, A34, A37, FINSEQ_1:def 7
.= fr . d by A21, A24 ; :: 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 A17, FINSEQ_5:6;
then A39: d in dom fr by A20, FINSEQ_3:29;
fs . d = 1 by A15, A38, FINSEQ_1:42;
hence fr . d = 1 * (x |^ ((((p -' 1) div 2) + 1) -' 1)) by A21, A38, A39
.= x |^ ((p -' 1) div 2) by NAT_D:34
.= ((<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0)) ^ <*(x |^ ((p -' 1) div 2))*>) . d by A15, A38, FINSEQ_1:42 ;
:: 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 A12, A17, A20, XREAL_1:235 ;
hence fr = (<*(- 1)*> ^ ((((p -' 1) div 2) -' 1) |-> 0)) ^ <*(x |^ ((p -' 1) div 2))*> by A23, FINSEQ_3:29; :: 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 A1, Th16;
A44: fs . (((p -' 1) div 2) + 1) = 1 by A15, FINSEQ_1:42;

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*>;
reconsider f = fp ^ <*b*> as FinSequence of NAT by FINSEQ_1:75;
A46: len f = ((p -' 1) div 2) + 1 by A40, FINSEQ_2:16;
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 A49, FINSEQ_3:25;
A52: d <= ((p -' 1) div 2) + 1 by A46, A48, FINSEQ_3:25;
A53: e <= ((p -' 1) div 2) + 1 by A46, A49, FINSEQ_3:25;

per cases ( ( d >= 1 & d < ((p -' 1) div 2) + 1 ) or d = ((p -' 1) div 2) + 1 ) by A48, A52, FINSEQ_3:25, XXREAL_0:1;

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 A40, A54, FINSEQ_3:25;
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 A49, A53, FINSEQ_3:25, XXREAL_0:1;

suppose A57: ( e >= 1 & e < ((p -' 1) div 2) + 1 ) ; :: thesis: not f . d,f . e are_congruent_mod p

then e <= (p -' 1) div 2 by NAT_1:13;
then A58: e in dom fp by A40, A57, FINSEQ_3:25;
then not fp . d,fp . e are_congruent_mod p by A43, A50, A55;
hence not f . d,f . e are_congruent_mod p by A56, A58, FINSEQ_1:def 7; :: thesis: verum

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 A42, A55, A56;
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 A60, INT_1:62;
then p divides ((j ^2) - (f . d)) + ((f . d) - b) by a61, WSIERP_1:4;
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 A40, A59, FINSEQ_1:42; :: 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 A50, A53, NAT_1:8;
then A63: e in dom fp by A40, A51, FINSEQ_3:25;
then f . e = fp . e by FINSEQ_1:def 7;
then f . e is_quadratic_residue_mod p by A42, A63;
then consider j being Integer such that
A64: ((j ^2) - (f . e)) mod p = 0 ;
A65: p divides (j ^2) - (f . e) by A64, INT_1:62;
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 A65, Th1;
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 A40, A62, FINSEQ_1:42; :: thesis: verum

end;

end;

end;

A66: ((Poly-INT fs) . b) mod p = 0 by A19, A45;
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 A46, FINSEQ_1:def 3;
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 A68, A69, FINSEQ_1:1, XXREAL_0:1;

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 A70, NAT_1:13;
then A71: d in dom fp by A40, A70, FINSEQ_3:25;
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 A71, FINSEQ_1:def 7; :: 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 A40, A66, FINSEQ_1:42; :: thesis: verum

end;

end;

end;

reconsider f = f as FinSequence of INT by FINSEQ_2:24, NUMBERS:17;
not p divides fs . (((p -' 1) div 2) + 1) by A4, A44, NAT_D:7;
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 A7, Th7;
then consider k being Nat such that
A72: (b |^ ((p -' 1) div 2)) + 1 = p * k by NAT_D:def 3;
- p < - 1 by A4, XREAL_1:24;
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 A73, NAT_D:61 ;
hence (b |^ ((p -' 1) div 2)) mod p = p - 1 ; :: thesis: verum

end;

end;