let p be Prime; :: thesis: for a, m being Nat

for f being FinSequence of NAT st p > 2 & a gcd p = 1 & f = a * (idseq ((p -' 1) div 2)) & m = card { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } holds

Lege (a,p) = (- 1) |^ m

let a, m be Nat; :: thesis: for f being FinSequence of NAT st p > 2 & a gcd p = 1 & f = a * (idseq ((p -' 1) div 2)) & m = card { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } holds

Lege (a,p) = (- 1) |^ m

let f be FinSequence of NAT ; :: thesis: ( p > 2 & a gcd p = 1 & f = a * (idseq ((p -' 1) div 2)) & m = card { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } implies Lege (a,p) = (- 1) |^ m )

assume that

A1: p > 2 and

A2: a gcd p = 1 and

A3: f = a * (idseq ((p -' 1) div 2)) and

A4: m = card { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } ; :: thesis: Lege (a,p) = (- 1) |^ m

set f1 = f mod p;

A5: len (f mod p) = len f by EULER_2:def 1;

set X = { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } ;

for x being object st x in { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } holds

x in rng (f mod p)

then reconsider X = { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } as finite set ;

reconsider X = X as finite Subset of NAT by A6, XBOOLE_1:1;

card X is Element of NAT ;

then reconsider m = m as Element of NAT by A4;

A7: (rng (f mod p)) \ X c= rng (f mod p) by XBOOLE_1:36;

reconsider Y = (rng (f mod p)) \ X as finite Subset of NAT ;

A8: a |^ ((p -' 1) div 2), Lege (a,p) are_congruent_mod p by A1, A2, Th28, INT_1:14;

set f2 = Sgm (rng (f mod p));

(Product (f mod p)) mod p = (Product f) mod p by EULER_2:11;

then A9: Product (f mod p), Product f are_congruent_mod p by NAT_D:64;

A10: p > 1 by INT_2:def 4;

then A11: p -' 1 = p - 1 by XREAL_1:233;

then A12: p -' 1 > 0 by A10, XREAL_1:50;

set p9 = (p -' 1) div 2;

rng (idseq ((p -' 1) div 2)) = Seg ((p -' 1) div 2) ;

then reconsider I = idseq ((p -' 1) div 2) as FinSequence of NAT by FINSEQ_1:def 4;

dom f = dom I by A3, VALUED_1:def 5;

then A13: len f = len I by FINSEQ_3:29

.= (p -' 1) div 2 by CARD_1:def 7 ;

p >= 2 + 1 by A1, NAT_1:13;

then p - 1 >= 3 - 1 by XREAL_1:9;

then f mod p <> {} by A13, A11, A5, NAT_2:13;

then rng (f mod p) is non empty Subset of NAT ;

then consider n1 being Element of NAT such that

A14: rng (f mod p) c= (Seg n1) \/ {0} by HEYTING3:1;

I is Element of ((p -' 1) div 2) -tuples_on REAL by FINSEQ_2:109, NUMBERS:19;

then A15: Product f = (Product (((p -' 1) div 2) |-> a)) * (Product I) by A3, RVSUM_1:108

.= (a |^ ((p -' 1) div 2)) * (Product I) by NEWTON:def 1 ;

p is odd by A1, PEPIN:17;

then A16: p -' 1 is even by A11, HILBERT3:2;

then A17: (p -' 1) div 2 = ((p -' 1) + 1) div 2 by NAT_2:26

.= p div 2 by A10, XREAL_1:235 ;

2 divides p -' 1 by A16, PEPIN:22;

then A18: p -' 1 = 2 * ((p -' 1) div 2) by NAT_D:3;

then (p -' 1) div 2 divides p -' 1 ;

then (p -' 1) div 2 <= p -' 1 by A12, NAT_D:7;

then A19: (p -' 1) div 2 < p by A11, XREAL_1:146, XXREAL_0:2;

for d being Nat st d in dom I holds

(I . d) gcd p = 1

A25: for d being Nat st d in dom f holds

f . d = a * d

(f mod p) . d <> (f mod p) . e

then A43: f mod p is one-to-one by FINSEQ_4:62;

A44: dom (f mod p) = dom f by A5, FINSEQ_3:29;

not 0 in rng (f mod p)

then A50: Sgm (rng (f mod p)) is one-to-one by A14, FINSEQ_3:92, XBOOLE_1:73;

A51: rng (f mod p) c= Seg n1 by A14, A49, XBOOLE_1:73;

then A52: X c= Seg n1 by A6;

len f = card (rng (f mod p)) by A5, A28, GRAPH_5:7;

then reconsider n = ((p -' 1) div 2) - m as Element of NAT by A4, A13, A6, NAT_1:21, NAT_1:43;

A53: Y c= Seg n1 by A51, A7;

A54: rng (f mod p) = rng (Sgm (rng (f mod p))) by A51, FINSEQ_1:def 13;

then A55: Product (f mod p) = Product (Sgm (rng (f mod p))) by A43, A50, EULER_2:10, RFINSEQ:26;

set f3 = ((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n);

set f4 = ((Sgm (rng (f mod p))) | n) ^ (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n));

A56: (Sgm (rng (f mod p))) /^ n is FinSequence of INT by FINSEQ_2:24, NUMBERS:17;

A57: dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) = (dom ((len ((Sgm (rng (f mod p))) /^ n)) |-> p)) /\ (dom ((Sgm (rng (f mod p))) /^ n)) by VALUED_1:12

.= (Seg (len ((len ((Sgm (rng (f mod p))) /^ n)) |-> p))) /\ (dom ((Sgm (rng (f mod p))) /^ n)) by FINSEQ_1:def 3

.= (dom ((Sgm (rng (f mod p))) /^ n)) /\ (dom ((Sgm (rng (f mod p))) /^ n)) by FINSEQ_1:def 3, CARD_1:def 7

.= dom ((Sgm (rng (f mod p))) /^ n) ;

then A58: len (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) = len ((Sgm (rng (f mod p))) /^ n) by FINSEQ_3:29;

for k, l being Nat st k in Y & l in X holds

k < l

then Sgm ((rng (f mod p)) \/ X) = (Sgm Y) ^ (Sgm X) by XBOOLE_1:39;

then A63: Sgm (rng (f mod p)) = (Sgm Y) ^ (Sgm X) by A6, XBOOLE_1:12;

A64: for d being Nat st d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) holds

(((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d = p - (((Sgm (rng (f mod p))) /^ n) . d)

.= ((p -' 1) div 2) - m by A4, A13, A5, A6, A42, CARD_2:44 ;

then A67: (Sgm (rng (f mod p))) /^ n = Sgm X by A63, FINSEQ_5:37;

A68: for d being Nat st d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) holds

( (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d > 0 & (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d <= (p -' 1) div 2 )

for d being Nat st d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) holds

(((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d in NAT

|.((- 1) |^ m).| = 1 by SERIES_2:1;

then A77: ( (- 1) |^ m = 1 or - ((- 1) |^ m) = 1 ) by ABSVALUE:1;

f3 is FinSequence of NAT ;

then reconsider f4 = ((Sgm (rng (f mod p))) | n) ^ (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) as FinSequence of NAT by FINSEQ_1:75;

A78: (Sgm (rng (f mod p))) | n = Sgm Y by A63, A66, FINSEQ_3:113, FINSEQ_6:10;

A79: for d being Nat st d in dom f4 holds

( f4 . d > 0 & f4 . d <= (p -' 1) div 2 )

then A88: (Sgm (rng (f mod p))) /^ n is one-to-one by A50, FINSEQ_3:91;

for d, e being Nat st 1 <= d & d < e & e <= len f3 holds

f3 . d <> f3 . e

then A95: f3 is one-to-one by FINSEQ_4:62;

A96: len (Sgm (rng (f mod p))) = (p -' 1) div 2 by A13, A5, A14, A49, A42, FINSEQ_3:39, XBOOLE_1:73;

then A97: n <= len (Sgm (rng (f mod p))) by XREAL_1:43;

A98: rng ((Sgm (rng (f mod p))) | n) misses rng f3

then A112: f4 is one-to-one by A95, A98, FINSEQ_3:91;

A113: for d being Nat st d in dom f3 holds

f3 . d, - (((Sgm (rng (f mod p))) /^ n) . d) are_congruent_mod p

.= (len (Sgm (rng (f mod p)))) - n by A96, XREAL_1:43, XREAL_1:233

.= m by A96 ;

len ((Sgm (rng (f mod p))) | n) = n by A96, FINSEQ_1:59, XREAL_1:43;

then len f4 = n + m by A58, A114, FINSEQ_1:22

.= len f by A13 ;

then rng f4 = rng I by A13, A112, A79, Th40;

then Product f4 = Product I by A112, EULER_2:10, RFINSEQ:26;

then A115: (Product ((Sgm (rng (f mod p))) | n)) * (Product f3) = Product I by RVSUM_1:97;

f3 is FinSequence of INT by FINSEQ_2:24, NUMBERS:17;

then (Product f3) * (Product ((Sgm (rng (f mod p))) | n)),(((- 1) |^ m) * (Product ((Sgm (rng (f mod p))) /^ n))) * (Product ((Sgm (rng (f mod p))) | n)) are_congruent_mod p by A58, A114, A56, A113, Th33, INT_4:11;

then (Product f3) * (Product ((Sgm (rng (f mod p))) | n)),((- 1) |^ m) * ((Product ((Sgm (rng (f mod p))) | n)) * (Product ((Sgm (rng (f mod p))) /^ n))) are_congruent_mod p ;

then Product I,((- 1) |^ m) * (Product (((Sgm (rng (f mod p))) | n) ^ ((Sgm (rng (f mod p))) /^ n))) are_congruent_mod p by A115, RVSUM_1:97;

then A116: Product I,((- 1) |^ m) * (Product (f mod p)) are_congruent_mod p by A55, RFINSEQ:8;

((- 1) |^ m) * (Product (f mod p)),((- 1) |^ m) * (Product f) are_congruent_mod p by A9, INT_4:11;

then Product I,(((- 1) |^ m) * (a |^ ((p -' 1) div 2))) * (Product I) are_congruent_mod p by A15, A116, INT_1:15;

then p divides (1 - (((- 1) |^ m) * (a |^ ((p -' 1) div 2)))) * (Product I) ;

then p divides 1 - (((- 1) |^ m) * (a |^ ((p -' 1) div 2))) by A24, WSIERP_1:29;

then p divides ((- 1) |^ m) * (1 - (((- 1) |^ m) * (a |^ ((p -' 1) div 2)))) by INT_2:2;

then A117: p divides ((- 1) |^ m) - ((((- 1) |^ m) * ((- 1) |^ m)) * (a |^ ((p -' 1) div 2))) ;

((- 1) |^ m) * ((- 1) |^ m) = (- 1) |^ (m + m) by NEWTON:8

.= (- 1) |^ (2 * m)

.= ((- 1) |^ 2) |^ m by NEWTON:9

.= (1 |^ 2) |^ m by WSIERP_1:1

.= 1 ;

then (- 1) |^ m,a |^ ((p -' 1) div 2) are_congruent_mod p by A117;

then A118: (- 1) |^ m, Lege (a,p) are_congruent_mod p by A8, INT_1:15;

for f being FinSequence of NAT st p > 2 & a gcd p = 1 & f = a * (idseq ((p -' 1) div 2)) & m = card { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } holds

Lege (a,p) = (- 1) |^ m

let a, m be Nat; :: thesis: for f being FinSequence of NAT st p > 2 & a gcd p = 1 & f = a * (idseq ((p -' 1) div 2)) & m = card { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } holds

Lege (a,p) = (- 1) |^ m

let f be FinSequence of NAT ; :: thesis: ( p > 2 & a gcd p = 1 & f = a * (idseq ((p -' 1) div 2)) & m = card { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } implies Lege (a,p) = (- 1) |^ m )

assume that

A1: p > 2 and

A2: a gcd p = 1 and

A3: f = a * (idseq ((p -' 1) div 2)) and

A4: m = card { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } ; :: thesis: Lege (a,p) = (- 1) |^ m

set f1 = f mod p;

A5: len (f mod p) = len f by EULER_2:def 1;

set X = { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } ;

for x being object st x in { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } holds

x in rng (f mod p)

proof

then A6:
{ k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } c= rng (f mod p)
;
let x be object ; :: thesis: ( x in { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } implies x in rng (f mod p) )

assume x in { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } ; :: thesis: x in rng (f mod p)

then ex k being Element of NAT st

( x = k & k in rng (f mod p) & k > p / 2 ) ;

hence x in rng (f mod p) ; :: thesis: verum

end;assume x in { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } ; :: thesis: x in rng (f mod p)

then ex k being Element of NAT st

( x = k & k in rng (f mod p) & k > p / 2 ) ;

hence x in rng (f mod p) ; :: thesis: verum

then reconsider X = { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } as finite set ;

reconsider X = X as finite Subset of NAT by A6, XBOOLE_1:1;

card X is Element of NAT ;

then reconsider m = m as Element of NAT by A4;

A7: (rng (f mod p)) \ X c= rng (f mod p) by XBOOLE_1:36;

reconsider Y = (rng (f mod p)) \ X as finite Subset of NAT ;

A8: a |^ ((p -' 1) div 2), Lege (a,p) are_congruent_mod p by A1, A2, Th28, INT_1:14;

set f2 = Sgm (rng (f mod p));

(Product (f mod p)) mod p = (Product f) mod p by EULER_2:11;

then A9: Product (f mod p), Product f are_congruent_mod p by NAT_D:64;

A10: p > 1 by INT_2:def 4;

then A11: p -' 1 = p - 1 by XREAL_1:233;

then A12: p -' 1 > 0 by A10, XREAL_1:50;

set p9 = (p -' 1) div 2;

rng (idseq ((p -' 1) div 2)) = Seg ((p -' 1) div 2) ;

then reconsider I = idseq ((p -' 1) div 2) as FinSequence of NAT by FINSEQ_1:def 4;

dom f = dom I by A3, VALUED_1:def 5;

then A13: len f = len I by FINSEQ_3:29

.= (p -' 1) div 2 by CARD_1:def 7 ;

p >= 2 + 1 by A1, NAT_1:13;

then p - 1 >= 3 - 1 by XREAL_1:9;

then f mod p <> {} by A13, A11, A5, NAT_2:13;

then rng (f mod p) is non empty Subset of NAT ;

then consider n1 being Element of NAT such that

A14: rng (f mod p) c= (Seg n1) \/ {0} by HEYTING3:1;

I is Element of ((p -' 1) div 2) -tuples_on REAL by FINSEQ_2:109, NUMBERS:19;

then A15: Product f = (Product (((p -' 1) div 2) |-> a)) * (Product I) by A3, RVSUM_1:108

.= (a |^ ((p -' 1) div 2)) * (Product I) by NEWTON:def 1 ;

p is odd by A1, PEPIN:17;

then A16: p -' 1 is even by A11, HILBERT3:2;

then A17: (p -' 1) div 2 = ((p -' 1) + 1) div 2 by NAT_2:26

.= p div 2 by A10, XREAL_1:235 ;

2 divides p -' 1 by A16, PEPIN:22;

then A18: p -' 1 = 2 * ((p -' 1) div 2) by NAT_D:3;

then (p -' 1) div 2 divides p -' 1 ;

then (p -' 1) div 2 <= p -' 1 by A12, NAT_D:7;

then A19: (p -' 1) div 2 < p by A11, XREAL_1:146, XXREAL_0:2;

for d being Nat st d in dom I holds

(I . d) gcd p = 1

proof

then A24:
(Product I) gcd p = 1
by WSIERP_1:36;
let d be Nat; :: thesis: ( d in dom I implies (I . d) gcd p = 1 )

assume d in dom I ; :: thesis: (I . d) gcd p = 1

then A20: d in Seg (len I) by FINSEQ_1:def 3;

then A21: d in Seg ((p -' 1) div 2) by CARD_1:def 7;

then A22: I . d = d by FINSEQ_2:49;

d <= (p -' 1) div 2 by A21, FINSEQ_1:1;

then A23: d < p by A19, XXREAL_0:2;

d >= 1 by A20, FINSEQ_1:1;

then d,p are_coprime by A23, EULER_1:2;

hence (I . d) gcd p = 1 by A22, INT_2:def 3; :: thesis: verum

end;assume d in dom I ; :: thesis: (I . d) gcd p = 1

then A20: d in Seg (len I) by FINSEQ_1:def 3;

then A21: d in Seg ((p -' 1) div 2) by CARD_1:def 7;

then A22: I . d = d by FINSEQ_2:49;

d <= (p -' 1) div 2 by A21, FINSEQ_1:1;

then A23: d < p by A19, XXREAL_0:2;

d >= 1 by A20, FINSEQ_1:1;

then d,p are_coprime by A23, EULER_1:2;

hence (I . d) gcd p = 1 by A22, INT_2:def 3; :: thesis: verum

A25: for d being Nat st d in dom f holds

f . d = a * d

proof

A28:
for d, e being Nat st 1 <= d & d < e & e <= len (f mod p) holds
let d be Nat; :: thesis: ( d in dom f implies f . d = a * d )

assume A26: d in dom f ; :: thesis: f . d = a * d

then d in dom I by A3, VALUED_1:def 5;

then d in Seg (len I) by FINSEQ_1:def 3;

then A27: d is Element of Seg ((p -' 1) div 2) by CARD_1:def 7;

thus f . d = a * (I . d) by A3, A26, VALUED_1:def 5

.= a * d by A27 ; :: thesis: verum

end;assume A26: d in dom f ; :: thesis: f . d = a * d

then d in dom I by A3, VALUED_1:def 5;

then d in Seg (len I) by FINSEQ_1:def 3;

then A27: d is Element of Seg ((p -' 1) div 2) by CARD_1:def 7;

thus f . d = a * (I . d) by A3, A26, VALUED_1:def 5

.= a * d by A27 ; :: thesis: verum

(f mod p) . d <> (f mod p) . e

proof

then A42:
len (f mod p) = card (rng (f mod p))
by GRAPH_5:7;
let d, e be Nat; :: thesis: ( 1 <= d & d < e & e <= len (f mod p) implies (f mod p) . d <> (f mod p) . e )

assume that

A29: 1 <= d and

A30: d < e and

A31: e <= len (f mod p) ; :: thesis: (f mod p) . d <> (f mod p) . e

A32: e <= len f by A31, EULER_2:def 1;

1 <= e by A29, A30, XXREAL_0:2;

then A33: e in dom f by A32, FINSEQ_3:25;

then A34: (f mod p) . e = (f . e) mod p by EULER_2:def 1;

d < len f by A30, A32, XXREAL_0:2;

then A35: d in dom f by A29, FINSEQ_3:25;

then A36: (f mod p) . d = (f . d) mod p by EULER_2:def 1;

end;assume that

A29: 1 <= d and

A30: d < e and

A31: e <= len (f mod p) ; :: thesis: (f mod p) . d <> (f mod p) . e

A32: e <= len f by A31, EULER_2:def 1;

1 <= e by A29, A30, XXREAL_0:2;

then A33: e in dom f by A32, FINSEQ_3:25;

then A34: (f mod p) . e = (f . e) mod p by EULER_2:def 1;

d < len f by A30, A32, XXREAL_0:2;

then A35: d in dom f by A29, FINSEQ_3:25;

then A36: (f mod p) . d = (f . d) mod p by EULER_2:def 1;

now :: thesis: not (f mod p) . d = (f mod p) . e

hence
(f mod p) . d <> (f mod p) . e
; :: thesis: verumassume
(f mod p) . d = (f mod p) . e
; :: thesis: contradiction

then f . e,f . d are_congruent_mod p by A36, A34, NAT_D:64;

then p divides (a * e) - (f . d) by A25, A33;

then p divides (a * e) - (a * d) by A25, A35;

then A37: p divides a * (e - d) ;

A38: ((p -' 1) div 2) - 1 < p by A19, XREAL_1:147;

reconsider dd = e - d as Element of NAT by A30, NAT_1:21;

A39: |.p.| = p by ABSVALUE:def 1;

A40: |.dd.| = dd by ABSVALUE:def 1;

A41: dd <= ((p -' 1) div 2) - 1 by A13, A5, A29, A31, XREAL_1:13;

dd <> 0 by A30;

then p <= dd by A2, A37, A39, A40, INT_4:6, WSIERP_1:29;

hence contradiction by A41, A38, XXREAL_0:2; :: thesis: verum

end;then f . e,f . d are_congruent_mod p by A36, A34, NAT_D:64;

then p divides (a * e) - (f . d) by A25, A33;

then p divides (a * e) - (a * d) by A25, A35;

then A37: p divides a * (e - d) ;

A38: ((p -' 1) div 2) - 1 < p by A19, XREAL_1:147;

reconsider dd = e - d as Element of NAT by A30, NAT_1:21;

A39: |.p.| = p by ABSVALUE:def 1;

A40: |.dd.| = dd by ABSVALUE:def 1;

A41: dd <= ((p -' 1) div 2) - 1 by A13, A5, A29, A31, XREAL_1:13;

dd <> 0 by A30;

then p <= dd by A2, A37, A39, A40, INT_4:6, WSIERP_1:29;

hence contradiction by A41, A38, XXREAL_0:2; :: thesis: verum

then A43: f mod p is one-to-one by FINSEQ_4:62;

A44: dom (f mod p) = dom f by A5, FINSEQ_3:29;

not 0 in rng (f mod p)

proof

then A49:
{0} misses rng (f mod p)
by ZFMISC_1:50;
reconsider a = a as Element of NAT by ORDINAL1:def 12;

assume 0 in rng (f mod p) ; :: thesis: contradiction

then consider n being Nat such that

A45: n in dom (f mod p) and

A46: (f mod p) . n = 0 by FINSEQ_2:10;

0 = (f . n) mod p by A44, A45, A46, EULER_2:def 1

.= (a * n) mod p by A25, A44, A45 ;

then A47: p divides a * n by PEPIN:6;

n >= 1 by A45, FINSEQ_3:25;

then A48: p <= n by A2, A47, NAT_D:7, WSIERP_1:30;

n <= (p -' 1) div 2 by A13, A5, A45, FINSEQ_3:25;

hence contradiction by A19, A48, XXREAL_0:2; :: thesis: verum

end;assume 0 in rng (f mod p) ; :: thesis: contradiction

then consider n being Nat such that

A45: n in dom (f mod p) and

A46: (f mod p) . n = 0 by FINSEQ_2:10;

0 = (f . n) mod p by A44, A45, A46, EULER_2:def 1

.= (a * n) mod p by A25, A44, A45 ;

then A47: p divides a * n by PEPIN:6;

n >= 1 by A45, FINSEQ_3:25;

then A48: p <= n by A2, A47, NAT_D:7, WSIERP_1:30;

n <= (p -' 1) div 2 by A13, A5, A45, FINSEQ_3:25;

hence contradiction by A19, A48, XXREAL_0:2; :: thesis: verum

then A50: Sgm (rng (f mod p)) is one-to-one by A14, FINSEQ_3:92, XBOOLE_1:73;

A51: rng (f mod p) c= Seg n1 by A14, A49, XBOOLE_1:73;

then A52: X c= Seg n1 by A6;

len f = card (rng (f mod p)) by A5, A28, GRAPH_5:7;

then reconsider n = ((p -' 1) div 2) - m as Element of NAT by A4, A13, A6, NAT_1:21, NAT_1:43;

A53: Y c= Seg n1 by A51, A7;

A54: rng (f mod p) = rng (Sgm (rng (f mod p))) by A51, FINSEQ_1:def 13;

then A55: Product (f mod p) = Product (Sgm (rng (f mod p))) by A43, A50, EULER_2:10, RFINSEQ:26;

set f3 = ((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n);

set f4 = ((Sgm (rng (f mod p))) | n) ^ (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n));

A56: (Sgm (rng (f mod p))) /^ n is FinSequence of INT by FINSEQ_2:24, NUMBERS:17;

A57: dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) = (dom ((len ((Sgm (rng (f mod p))) /^ n)) |-> p)) /\ (dom ((Sgm (rng (f mod p))) /^ n)) by VALUED_1:12

.= (Seg (len ((len ((Sgm (rng (f mod p))) /^ n)) |-> p))) /\ (dom ((Sgm (rng (f mod p))) /^ n)) by FINSEQ_1:def 3

.= (dom ((Sgm (rng (f mod p))) /^ n)) /\ (dom ((Sgm (rng (f mod p))) /^ n)) by FINSEQ_1:def 3, CARD_1:def 7

.= dom ((Sgm (rng (f mod p))) /^ n) ;

then A58: len (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) = len ((Sgm (rng (f mod p))) /^ n) by FINSEQ_3:29;

for k, l being Nat st k in Y & l in X holds

k < l

proof

then
Sgm (Y \/ X) = (Sgm Y) ^ (Sgm X)
by A52, A53, FINSEQ_3:42;
let k, l be Nat; :: thesis: ( k in Y & l in X implies k < l )

assume that

A59: k in Y and

A60: l in X ; :: thesis: k < l

A61: not k in X by A59, XBOOLE_0:def 5;

A62: ex l1 being Element of NAT st

( l1 = l & l1 in rng (f mod p) & l1 > p / 2 ) by A60;

k in rng (f mod p) by A59, XBOOLE_0:def 5;

then k <= p / 2 by A61;

hence k < l by A62, XXREAL_0:2; :: thesis: verum

end;assume that

A59: k in Y and

A60: l in X ; :: thesis: k < l

A61: not k in X by A59, XBOOLE_0:def 5;

A62: ex l1 being Element of NAT st

( l1 = l & l1 in rng (f mod p) & l1 > p / 2 ) by A60;

k in rng (f mod p) by A59, XBOOLE_0:def 5;

then k <= p / 2 by A61;

hence k < l by A62, XXREAL_0:2; :: thesis: verum

then Sgm ((rng (f mod p)) \/ X) = (Sgm Y) ^ (Sgm X) by XBOOLE_1:39;

then A63: Sgm (rng (f mod p)) = (Sgm Y) ^ (Sgm X) by A6, XBOOLE_1:12;

A64: for d being Nat st d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) holds

(((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d = p - (((Sgm (rng (f mod p))) /^ n) . d)

proof

A66: len (Sgm Y) =
card Y
by A51, A7, FINSEQ_3:39, XBOOLE_1:1
let d be Nat; :: thesis: ( d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) implies (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d = p - (((Sgm (rng (f mod p))) /^ n) . d) )

assume A65: d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) ; :: thesis: (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d = p - (((Sgm (rng (f mod p))) /^ n) . d)

then d in Seg (len ((Sgm (rng (f mod p))) /^ n)) by A57, FINSEQ_1:def 3;

then ((len ((Sgm (rng (f mod p))) /^ n)) |-> p) . d = p by FINSEQ_2:57;

hence (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d = p - (((Sgm (rng (f mod p))) /^ n) . d) by A65, VALUED_1:13; :: thesis: verum

end;assume A65: d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) ; :: thesis: (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d = p - (((Sgm (rng (f mod p))) /^ n) . d)

then d in Seg (len ((Sgm (rng (f mod p))) /^ n)) by A57, FINSEQ_1:def 3;

then ((len ((Sgm (rng (f mod p))) /^ n)) |-> p) . d = p by FINSEQ_2:57;

hence (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d = p - (((Sgm (rng (f mod p))) /^ n) . d) by A65, VALUED_1:13; :: thesis: verum

.= ((p -' 1) div 2) - m by A4, A13, A5, A6, A42, CARD_2:44 ;

then A67: (Sgm (rng (f mod p))) /^ n = Sgm X by A63, FINSEQ_5:37;

A68: for d being Nat st d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) holds

( (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d > 0 & (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d <= (p -' 1) div 2 )

proof

A75:
rng (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) c= INT
by RELAT_1:def 19;
let d be Nat; :: thesis: ( d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) implies ( (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d > 0 & (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d <= (p -' 1) div 2 ) )

reconsider w = (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d as Element of INT by INT_1:def 2;

assume A69: d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) ; :: thesis: ( (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d > 0 & (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d <= (p -' 1) div 2 )

then (Sgm X) . d in rng (Sgm X) by A67, A57, FUNCT_1:3;

then (Sgm X) . d in X by A52, FINSEQ_1:def 13;

then A70: ex ll being Element of NAT st

( ll = (Sgm X) . d & ll in rng (f mod p) & ll > p / 2 ) ;

then consider e being Nat such that

A71: e in dom (f mod p) and

A72: (f mod p) . e = ((Sgm (rng (f mod p))) /^ n) . d by A67, FINSEQ_2:10;

((Sgm (rng (f mod p))) /^ n) . d = (f . e) mod p by A44, A71, A72, EULER_2:def 1;

then A73: ((Sgm (rng (f mod p))) /^ n) . d < p by NAT_D:1;

A74: (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d = p - (((Sgm (rng (f mod p))) /^ n) . d) by A64, A69;

then w < p - (p / 2) by A67, A70, XREAL_1:10;

hence ( (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d > 0 & (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d <= (p -' 1) div 2 ) by A17, A74, A73, INT_1:54, XREAL_1:50; :: thesis: verum

end;reconsider w = (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d as Element of INT by INT_1:def 2;

assume A69: d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) ; :: thesis: ( (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d > 0 & (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d <= (p -' 1) div 2 )

then (Sgm X) . d in rng (Sgm X) by A67, A57, FUNCT_1:3;

then (Sgm X) . d in X by A52, FINSEQ_1:def 13;

then A70: ex ll being Element of NAT st

( ll = (Sgm X) . d & ll in rng (f mod p) & ll > p / 2 ) ;

then consider e being Nat such that

A71: e in dom (f mod p) and

A72: (f mod p) . e = ((Sgm (rng (f mod p))) /^ n) . d by A67, FINSEQ_2:10;

((Sgm (rng (f mod p))) /^ n) . d = (f . e) mod p by A44, A71, A72, EULER_2:def 1;

then A73: ((Sgm (rng (f mod p))) /^ n) . d < p by NAT_D:1;

A74: (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d = p - (((Sgm (rng (f mod p))) /^ n) . d) by A64, A69;

then w < p - (p / 2) by A67, A70, XREAL_1:10;

hence ( (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d > 0 & (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d <= (p -' 1) div 2 ) by A17, A74, A73, INT_1:54, XREAL_1:50; :: thesis: verum

for d being Nat st d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) holds

(((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d in NAT

proof

then reconsider f3 = ((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n) as FinSequence of NAT by FINSEQ_2:12;
let d be Nat; :: thesis: ( d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) implies (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d in NAT )

assume A76: d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) ; :: thesis: (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d in NAT

(((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d > 0 by A68, A76;

hence (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d in NAT by A75, INT_1:3; :: thesis: verum

end;assume A76: d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) ; :: thesis: (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d in NAT

(((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d > 0 by A68, A76;

hence (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d in NAT by A75, INT_1:3; :: thesis: verum

|.((- 1) |^ m).| = 1 by SERIES_2:1;

then A77: ( (- 1) |^ m = 1 or - ((- 1) |^ m) = 1 ) by ABSVALUE:1;

f3 is FinSequence of NAT ;

then reconsider f4 = ((Sgm (rng (f mod p))) | n) ^ (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) as FinSequence of NAT by FINSEQ_1:75;

A78: (Sgm (rng (f mod p))) | n = Sgm Y by A63, A66, FINSEQ_3:113, FINSEQ_6:10;

A79: for d being Nat st d in dom f4 holds

( f4 . d > 0 & f4 . d <= (p -' 1) div 2 )

proof

A87:
Sgm (rng (f mod p)) = ((Sgm (rng (f mod p))) | n) ^ ((Sgm (rng (f mod p))) /^ n)
by RFINSEQ:8;
let d be Nat; :: thesis: ( d in dom f4 implies ( f4 . d > 0 & f4 . d <= (p -' 1) div 2 ) )

assume A80: d in dom f4 ; :: thesis: ( f4 . d > 0 & f4 . d <= (p -' 1) div 2 )

end;assume A80: d in dom f4 ; :: thesis: ( f4 . d > 0 & f4 . d <= (p -' 1) div 2 )

per cases
( d in dom ((Sgm (rng (f mod p))) | n) or ex l being Nat st

( l in dom f3 & d = (len ((Sgm (rng (f mod p))) | n)) + l ) ) by A80, FINSEQ_1:25;

end;

( l in dom f3 & d = (len ((Sgm (rng (f mod p))) | n)) + l ) ) by A80, FINSEQ_1:25;

suppose A81:
d in dom ((Sgm (rng (f mod p))) | n)
; :: thesis: ( f4 . d > 0 & f4 . d <= (p -' 1) div 2 )

reconsider d = d as Element of NAT by ORDINAL1:def 12;

((Sgm (rng (f mod p))) | n) . d in rng (Sgm Y) by A78, A81, FUNCT_1:3;

then A82: ((Sgm (rng (f mod p))) | n) . d in Y by A53, FINSEQ_1:def 13;

then A83: ((Sgm (rng (f mod p))) | n) . d in rng (f mod p) by XBOOLE_0:def 5;

not ((Sgm (rng (f mod p))) | n) . d in X by A82, XBOOLE_0:def 5;

then ((Sgm (rng (f mod p))) | n) . d <= p / 2 by A83;

then A84: ((Sgm (rng (f mod p))) | n) . d <= (p -' 1) div 2 by A17, INT_1:54;

not ((Sgm (rng (f mod p))) | n) . d in {0} by A49, A83, XBOOLE_0:3;

then ((Sgm (rng (f mod p))) | n) . d <> 0 by TARSKI:def 1;

hence ( f4 . d > 0 & f4 . d <= (p -' 1) div 2 ) by A81, A84, FINSEQ_1:def 7; :: thesis: verum

end;((Sgm (rng (f mod p))) | n) . d in rng (Sgm Y) by A78, A81, FUNCT_1:3;

then A82: ((Sgm (rng (f mod p))) | n) . d in Y by A53, FINSEQ_1:def 13;

then A83: ((Sgm (rng (f mod p))) | n) . d in rng (f mod p) by XBOOLE_0:def 5;

not ((Sgm (rng (f mod p))) | n) . d in X by A82, XBOOLE_0:def 5;

then ((Sgm (rng (f mod p))) | n) . d <= p / 2 by A83;

then A84: ((Sgm (rng (f mod p))) | n) . d <= (p -' 1) div 2 by A17, INT_1:54;

not ((Sgm (rng (f mod p))) | n) . d in {0} by A49, A83, XBOOLE_0:3;

then ((Sgm (rng (f mod p))) | n) . d <> 0 by TARSKI:def 1;

hence ( f4 . d > 0 & f4 . d <= (p -' 1) div 2 ) by A81, A84, FINSEQ_1:def 7; :: thesis: verum

suppose
ex l being Nat st

( l in dom f3 & d = (len ((Sgm (rng (f mod p))) | n)) + l ) ; :: thesis: ( f4 . d > 0 & f4 . d <= (p -' 1) div 2 )

( l in dom f3 & d = (len ((Sgm (rng (f mod p))) | n)) + l ) ; :: thesis: ( f4 . d > 0 & f4 . d <= (p -' 1) div 2 )

then consider l being Element of NAT such that

A85: l in dom f3 and

A86: d = (len ((Sgm (rng (f mod p))) | n)) + l ;

f4 . d = f3 . l by A85, A86, FINSEQ_1:def 7;

hence ( f4 . d > 0 & f4 . d <= (p -' 1) div 2 ) by A68, A85; :: thesis: verum

end;A85: l in dom f3 and

A86: d = (len ((Sgm (rng (f mod p))) | n)) + l ;

f4 . d = f3 . l by A85, A86, FINSEQ_1:def 7;

hence ( f4 . d > 0 & f4 . d <= (p -' 1) div 2 ) by A68, A85; :: thesis: verum

then A88: (Sgm (rng (f mod p))) /^ n is one-to-one by A50, FINSEQ_3:91;

for d, e being Nat st 1 <= d & d < e & e <= len f3 holds

f3 . d <> f3 . e

proof

then
len f3 = card (rng f3)
by GRAPH_5:7;
let d, e be Nat; :: thesis: ( 1 <= d & d < e & e <= len f3 implies f3 . d <> f3 . e )

assume that

A89: 1 <= d and

A90: d < e and

A91: e <= len f3 ; :: thesis: f3 . d <> f3 . e

1 <= e by A89, A90, XXREAL_0:2;

then A92: e in dom f3 by A91, FINSEQ_3:25;

then A93: f3 . e = p - (((Sgm (rng (f mod p))) /^ n) . e) by A64;

d < len f3 by A90, A91, XXREAL_0:2;

then A94: d in dom f3 by A89, FINSEQ_3:25;

then f3 . d = p - (((Sgm (rng (f mod p))) /^ n) . d) by A64;

hence f3 . d <> f3 . e by A88, A57, A90, A94, A92, A93; :: thesis: verum

end;assume that

A89: 1 <= d and

A90: d < e and

A91: e <= len f3 ; :: thesis: f3 . d <> f3 . e

1 <= e by A89, A90, XXREAL_0:2;

then A92: e in dom f3 by A91, FINSEQ_3:25;

then A93: f3 . e = p - (((Sgm (rng (f mod p))) /^ n) . e) by A64;

d < len f3 by A90, A91, XXREAL_0:2;

then A94: d in dom f3 by A89, FINSEQ_3:25;

then f3 . d = p - (((Sgm (rng (f mod p))) /^ n) . d) by A64;

hence f3 . d <> f3 . e by A88, A57, A90, A94, A92, A93; :: thesis: verum

then A95: f3 is one-to-one by FINSEQ_4:62;

A96: len (Sgm (rng (f mod p))) = (p -' 1) div 2 by A13, A5, A14, A49, A42, FINSEQ_3:39, XBOOLE_1:73;

then A97: n <= len (Sgm (rng (f mod p))) by XREAL_1:43;

A98: rng ((Sgm (rng (f mod p))) | n) misses rng f3

proof

(Sgm (rng (f mod p))) | n is one-to-one
by A50, A87, FINSEQ_3:91;
assume
rng ((Sgm (rng (f mod p))) | n) meets rng f3
; :: thesis: contradiction

then consider x being object such that

A99: x in rng ((Sgm (rng (f mod p))) | n) and

A100: x in rng f3 by XBOOLE_0:3;

consider e being Nat such that

A101: e in dom f3 and

A102: f3 . e = x by A100, FINSEQ_2:10;

x = p - (((Sgm (rng (f mod p))) /^ n) . e) by A64, A101, A102;

then A103: x = p - ((Sgm (rng (f mod p))) . (e + n)) by A97, A57, A101, RFINSEQ:def 1;

e + n in dom (Sgm (rng (f mod p))) by A57, A101, FINSEQ_5:26;

then consider e1 being Nat such that

A104: e1 in dom (f mod p) and

A105: (f mod p) . e1 = (Sgm (rng (f mod p))) . (e + n) by A54, FINSEQ_2:10, FUNCT_1:3;

A106: e1 in dom f by A5, A104, FINSEQ_3:29;

A107: e1 <= (p -' 1) div 2 by A13, A5, A104, FINSEQ_3:25;

rng ((Sgm (rng (f mod p))) | n) c= rng (Sgm (rng (f mod p))) by FINSEQ_5:19;

then consider d1 being Nat such that

A108: d1 in dom (f mod p) and

A109: (f mod p) . d1 = x by A54, A99, FINSEQ_2:10;

d1 <= (p -' 1) div 2 by A13, A5, A108, FINSEQ_3:25;

then d1 + e1 <= ((p -' 1) div 2) + ((p -' 1) div 2) by A107, XREAL_1:7;

then A110: d1 + e1 < p by A11, A18, XREAL_1:146, XXREAL_0:2;

x = (f . d1) mod p by A44, A108, A109, EULER_2:def 1;

then ((f . d1) mod p) + ((Sgm (rng (f mod p))) . (e + n)) = p by A103;

then ((f . d1) mod p) + ((f . e1) mod p) = p by A105, A106, EULER_2:def 1;

then (((f . d1) mod p) + ((f . e1) mod p)) mod p = 0 by NAT_D:25;

then ((f . d1) + (f . e1)) mod p = 0 by EULER_2:6;

then p divides (f . d1) + (f . e1) by PEPIN:6;

then p divides (d1 * a) + (f . e1) by A25, A44, A108;

then p divides (d1 * a) + (e1 * a) by A25, A106;

then A111: p divides (d1 + e1) * a ;

d1 >= 1 by A108, FINSEQ_3:25;

hence contradiction by A2, A111, A110, NAT_D:7, WSIERP_1:30; :: thesis: verum

end;then consider x being object such that

A99: x in rng ((Sgm (rng (f mod p))) | n) and

A100: x in rng f3 by XBOOLE_0:3;

consider e being Nat such that

A101: e in dom f3 and

A102: f3 . e = x by A100, FINSEQ_2:10;

x = p - (((Sgm (rng (f mod p))) /^ n) . e) by A64, A101, A102;

then A103: x = p - ((Sgm (rng (f mod p))) . (e + n)) by A97, A57, A101, RFINSEQ:def 1;

e + n in dom (Sgm (rng (f mod p))) by A57, A101, FINSEQ_5:26;

then consider e1 being Nat such that

A104: e1 in dom (f mod p) and

A105: (f mod p) . e1 = (Sgm (rng (f mod p))) . (e + n) by A54, FINSEQ_2:10, FUNCT_1:3;

A106: e1 in dom f by A5, A104, FINSEQ_3:29;

A107: e1 <= (p -' 1) div 2 by A13, A5, A104, FINSEQ_3:25;

rng ((Sgm (rng (f mod p))) | n) c= rng (Sgm (rng (f mod p))) by FINSEQ_5:19;

then consider d1 being Nat such that

A108: d1 in dom (f mod p) and

A109: (f mod p) . d1 = x by A54, A99, FINSEQ_2:10;

d1 <= (p -' 1) div 2 by A13, A5, A108, FINSEQ_3:25;

then d1 + e1 <= ((p -' 1) div 2) + ((p -' 1) div 2) by A107, XREAL_1:7;

then A110: d1 + e1 < p by A11, A18, XREAL_1:146, XXREAL_0:2;

x = (f . d1) mod p by A44, A108, A109, EULER_2:def 1;

then ((f . d1) mod p) + ((Sgm (rng (f mod p))) . (e + n)) = p by A103;

then ((f . d1) mod p) + ((f . e1) mod p) = p by A105, A106, EULER_2:def 1;

then (((f . d1) mod p) + ((f . e1) mod p)) mod p = 0 by NAT_D:25;

then ((f . d1) + (f . e1)) mod p = 0 by EULER_2:6;

then p divides (f . d1) + (f . e1) by PEPIN:6;

then p divides (d1 * a) + (f . e1) by A25, A44, A108;

then p divides (d1 * a) + (e1 * a) by A25, A106;

then A111: p divides (d1 + e1) * a ;

d1 >= 1 by A108, FINSEQ_3:25;

hence contradiction by A2, A111, A110, NAT_D:7, WSIERP_1:30; :: thesis: verum

then A112: f4 is one-to-one by A95, A98, FINSEQ_3:91;

A113: for d being Nat st d in dom f3 holds

f3 . d, - (((Sgm (rng (f mod p))) /^ n) . d) are_congruent_mod p

proof

A114: len ((Sgm (rng (f mod p))) /^ n) =
(len (Sgm (rng (f mod p)))) -' n
by RFINSEQ:29
let d be Nat; :: thesis: ( d in dom f3 implies f3 . d, - (((Sgm (rng (f mod p))) /^ n) . d) are_congruent_mod p )

assume d in dom f3 ; :: thesis: f3 . d, - (((Sgm (rng (f mod p))) /^ n) . d) are_congruent_mod p

then (f3 . d) mod p = (p - (((Sgm (rng (f mod p))) /^ n) . d)) mod p by A64

.= ((1 * p) + (- (((Sgm (rng (f mod p))) /^ n) . d))) mod p

.= (- (((Sgm (rng (f mod p))) /^ n) . d)) mod p by EULER_1:12 ;

hence f3 . d, - (((Sgm (rng (f mod p))) /^ n) . d) are_congruent_mod p by NAT_D:64; :: thesis: verum

end;assume d in dom f3 ; :: thesis: f3 . d, - (((Sgm (rng (f mod p))) /^ n) . d) are_congruent_mod p

then (f3 . d) mod p = (p - (((Sgm (rng (f mod p))) /^ n) . d)) mod p by A64

.= ((1 * p) + (- (((Sgm (rng (f mod p))) /^ n) . d))) mod p

.= (- (((Sgm (rng (f mod p))) /^ n) . d)) mod p by EULER_1:12 ;

hence f3 . d, - (((Sgm (rng (f mod p))) /^ n) . d) are_congruent_mod p by NAT_D:64; :: thesis: verum

.= (len (Sgm (rng (f mod p)))) - n by A96, XREAL_1:43, XREAL_1:233

.= m by A96 ;

len ((Sgm (rng (f mod p))) | n) = n by A96, FINSEQ_1:59, XREAL_1:43;

then len f4 = n + m by A58, A114, FINSEQ_1:22

.= len f by A13 ;

then rng f4 = rng I by A13, A112, A79, Th40;

then Product f4 = Product I by A112, EULER_2:10, RFINSEQ:26;

then A115: (Product ((Sgm (rng (f mod p))) | n)) * (Product f3) = Product I by RVSUM_1:97;

f3 is FinSequence of INT by FINSEQ_2:24, NUMBERS:17;

then (Product f3) * (Product ((Sgm (rng (f mod p))) | n)),(((- 1) |^ m) * (Product ((Sgm (rng (f mod p))) /^ n))) * (Product ((Sgm (rng (f mod p))) | n)) are_congruent_mod p by A58, A114, A56, A113, Th33, INT_4:11;

then (Product f3) * (Product ((Sgm (rng (f mod p))) | n)),((- 1) |^ m) * ((Product ((Sgm (rng (f mod p))) | n)) * (Product ((Sgm (rng (f mod p))) /^ n))) are_congruent_mod p ;

then Product I,((- 1) |^ m) * (Product (((Sgm (rng (f mod p))) | n) ^ ((Sgm (rng (f mod p))) /^ n))) are_congruent_mod p by A115, RVSUM_1:97;

then A116: Product I,((- 1) |^ m) * (Product (f mod p)) are_congruent_mod p by A55, RFINSEQ:8;

((- 1) |^ m) * (Product (f mod p)),((- 1) |^ m) * (Product f) are_congruent_mod p by A9, INT_4:11;

then Product I,(((- 1) |^ m) * (a |^ ((p -' 1) div 2))) * (Product I) are_congruent_mod p by A15, A116, INT_1:15;

then p divides (1 - (((- 1) |^ m) * (a |^ ((p -' 1) div 2)))) * (Product I) ;

then p divides 1 - (((- 1) |^ m) * (a |^ ((p -' 1) div 2))) by A24, WSIERP_1:29;

then p divides ((- 1) |^ m) * (1 - (((- 1) |^ m) * (a |^ ((p -' 1) div 2)))) by INT_2:2;

then A117: p divides ((- 1) |^ m) - ((((- 1) |^ m) * ((- 1) |^ m)) * (a |^ ((p -' 1) div 2))) ;

((- 1) |^ m) * ((- 1) |^ m) = (- 1) |^ (m + m) by NEWTON:8

.= (- 1) |^ (2 * m)

.= ((- 1) |^ 2) |^ m by NEWTON:9

.= (1 |^ 2) |^ m by WSIERP_1:1

.= 1 ;

then (- 1) |^ m,a |^ ((p -' 1) div 2) are_congruent_mod p by A117;

then A118: (- 1) |^ m, Lege (a,p) are_congruent_mod p by A8, INT_1:15;

per cases
( (- 1) |^ m = 1 or (- 1) |^ m = - 1 )
by A77;

end;

suppose A119:
(- 1) |^ m = 1
; :: thesis: Lege (a,p) = (- 1) |^ m

then A120:
Lege (a,p) <> - 1
by A118, A1, NAT_D:7;

end;now :: thesis: not Lege (a,p) = 0

hence
Lege (a,p) = (- 1) |^ m
by A119, Th25, A120; :: thesis: verumassume
Lege (a,p) = 0
; :: thesis: contradiction

then p divides 1 - 0 by A118, A119;

then p = 1 by WSIERP_1:15;

hence contradiction by A1; :: thesis: verum

end;then p divides 1 - 0 by A118, A119;

then p = 1 by WSIERP_1:15;

hence contradiction by A1; :: thesis: verum

suppose A121:
(- 1) |^ m = - 1
; :: thesis: Lege (a,p) = (- 1) |^ m

end;

A122: now :: thesis: not Lege (a,p) = 1

assume
Lege (a,p) = 1
; :: thesis: contradiction

then p divides - 2 by A118, A121;

then p divides 2 by INT_2:10;

hence contradiction by A1, NAT_D:7; :: thesis: verum

end;then p divides - 2 by A118, A121;

then p divides 2 by INT_2:10;

hence contradiction by A1, NAT_D:7; :: thesis: verum

now :: thesis: not Lege (a,p) = 0

hence
Lege (a,p) = (- 1) |^ m
by A121, Th25, A122; :: thesis: verumassume
Lege (a,p) = 0
; :: thesis: contradiction

then p divides (- 1) - 0 by A118, A121;

then p = 1 by WSIERP_1:15, INT_2:10;

hence contradiction by A1; :: thesis: verum

end;then p divides (- 1) - 0 by A118, A121;

then p = 1 by WSIERP_1:15, INT_2:10;

hence contradiction by A1; :: thesis: verum