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)
proof
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;
then A6: { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } c= 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 ;
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 ;
set f2 = Sgm (rng (f mod p));
(Product (f mod p)) mod p = () 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 ;
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 ;
then A13: len f = len I by FINSEQ_3:29
.= (p -' 1) div 2 by CARD_1:def 7 ;
p >= 2 + 1 by ;
then p - 1 >= 3 - 1 by XREAL_1:9;
then f mod p <> {} by ;
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) \/ by HEYTING3:1;
I is Element of ((p -' 1) div 2) -tuples_on REAL by ;
then A15: Product f = (Product (((p -' 1) div 2) |-> a)) * () by
.= (a |^ ((p -' 1) div 2)) * () by NEWTON:def 1 ;
p is odd by ;
then A16: p -' 1 is even by ;
then A17: (p -' 1) div 2 = ((p -' 1) + 1) div 2 by NAT_2:26
.= p div 2 by ;
2 divides p -' 1 by ;
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 ;
then A19: (p -' 1) div 2 < p by ;
for d being Nat st d in dom I holds
(I . d) gcd p = 1
proof
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 ;
then A23: d < p by ;
d >= 1 by ;
then d,p are_coprime by ;
hence (I . d) gcd p = 1 by ; :: thesis: verum
end;
then A24: (Product I) gcd p = 1 by WSIERP_1:36;
A25: for d being Nat st d in dom f holds
f . d = a * d
proof
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 ;
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
.= a * d by A27 ; :: thesis: verum
end;
A28: for d, e being Nat st 1 <= d & d < e & e <= len (f mod p) holds
(f mod p) . d <> (f mod p) . e
proof
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 ;
1 <= e by ;
then A33: e in dom f by ;
then A34: (f mod p) . e = (f . e) mod p by EULER_2:def 1;
d < len f by ;
then A35: d in dom f by ;
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
assume (f mod p) . d = (f mod p) . e ; :: thesis: contradiction
then f . e,f . d are_congruent_mod p by ;
then p divides (a * e) - (f . d) by ;
then p divides (a * e) - (a * d) by ;
then A37: p divides a * (e - d) ;
A38: ((p -' 1) div 2) - 1 < p by ;
reconsider dd = e - d as Element of NAT by ;
A39: |.p.| = p by ABSVALUE:def 1;
A40: |.dd.| = dd by ABSVALUE:def 1;
A41: dd <= ((p -' 1) div 2) - 1 by ;
dd <> 0 by A30;
then p <= dd by ;
hence contradiction by A41, A38, XXREAL_0:2; :: thesis: verum
end;
hence (f mod p) . d <> (f mod p) . e ; :: thesis: verum
end;
then A42: len (f mod p) = card (rng (f mod p)) by GRAPH_5:7;
then A43: f mod p is one-to-one by FINSEQ_4:62;
A44: dom (f mod p) = dom f by ;
not 0 in rng (f mod p)
proof
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
.= (a * n) mod p by ;
then A47: p divides a * n by PEPIN:6;
n >= 1 by ;
then A48: p <= n by ;
n <= (p -' 1) div 2 by ;
hence contradiction by A19, A48, XXREAL_0:2; :: thesis: verum
end;
then A49: {0} misses rng (f mod p) by ZFMISC_1:50;
then A50: Sgm (rng (f mod p)) is one-to-one by ;
A51: rng (f mod p) c= Seg n1 by ;
then A52: X c= Seg n1 by A6;
len f = card (rng (f mod p)) by ;
then reconsider n = ((p -' 1) div 2) - m as Element of NAT by ;
A53: Y c= Seg n1 by ;
A54: rng (f mod p) = rng (Sgm (rng (f mod p))) by ;
then A55: Product (f mod p) = Product (Sgm (rng (f mod p))) by ;
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 ;
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
.= 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
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 ;
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 ;
then k <= p / 2 by A61;
hence k < l by ; :: thesis: verum
end;
then Sgm (Y \/ X) = (Sgm Y) ^ (Sgm X) by ;
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 ;
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
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 ;
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 ; :: thesis: verum
end;
A66: len (Sgm Y) = card Y by
.= ((p -' 1) div 2) - m by ;
then A67: (Sgm (rng (f mod p))) /^ n = Sgm X by ;
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
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 ;
then (Sgm X) . d in X by ;
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 ;
((Sgm (rng (f mod p))) /^ n) . d = (f . e) mod p by ;
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 ;
then w < p - (p / 2) by ;
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 ; :: thesis: verum
end;
A75: rng (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) c= INT by RELAT_1:def 19;
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
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 ;
hence (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d in NAT by ; :: thesis: verum
end;
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;
|.((- 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 ;
A79: for d being Nat st d in dom f4 holds
( f4 . d > 0 & f4 . d <= (p -' 1) div 2 )
proof
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 )
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 ;
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 ;
then A82: ((Sgm (rng (f mod p))) | n) . d in Y by ;
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 ;
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 ;
not ((Sgm (rng (f mod p))) | n) . d in by ;
then ((Sgm (rng (f mod p))) | n) . d <> 0 by TARSKI:def 1;
hence ( f4 . d > 0 & f4 . d <= (p -' 1) div 2 ) by ; :: thesis: verum
end;
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 )
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 ;
hence ( f4 . d > 0 & f4 . d <= (p -' 1) div 2 ) by ; :: thesis: verum
end;
end;
end;
A87: Sgm (rng (f mod p)) = ((Sgm (rng (f mod p))) | n) ^ ((Sgm (rng (f mod p))) /^ n) by RFINSEQ:8;
then A88: (Sgm (rng (f mod p))) /^ n is one-to-one by ;
for d, e being Nat st 1 <= d & d < e & e <= len f3 holds
f3 . d <> f3 . e
proof
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 ;
then A92: e in dom f3 by ;
then A93: f3 . e = p - (((Sgm (rng (f mod p))) /^ n) . e) by A64;
d < len f3 by ;
then A94: d in dom f3 by ;
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;
then len f3 = card (rng f3) by GRAPH_5:7;
then A95: f3 is one-to-one by FINSEQ_4:62;
A96: len (Sgm (rng (f mod p))) = (p -' 1) div 2 by ;
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
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 ;
x = p - (((Sgm (rng (f mod p))) /^ n) . e) by ;
then A103: x = p - ((Sgm (rng (f mod p))) . (e + n)) by ;
e + n in dom (Sgm (rng (f mod p))) by ;
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 ;
A106: e1 in dom f by ;
A107: e1 <= (p -' 1) div 2 by ;
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 ;
d1 <= (p -' 1) div 2 by ;
then d1 + e1 <= ((p -' 1) div 2) + ((p -' 1) div 2) by ;
then A110: d1 + e1 < p by ;
x = (f . d1) mod p by ;
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 ;
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 ;
then p divides (d1 * a) + (e1 * a) by ;
then A111: p divides (d1 + e1) * a ;
d1 >= 1 by ;
hence contradiction by A2, A111, A110, NAT_D:7, WSIERP_1:30; :: thesis: verum
end;
(Sgm (rng (f mod p))) | n is one-to-one by ;
then A112: f4 is one-to-one by ;
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
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;
A114: len ((Sgm (rng (f mod p))) /^ n) = (len (Sgm (rng (f mod p)))) -' n by RFINSEQ:29
.= (len (Sgm (rng (f mod p)))) - n by
.= m by A96 ;
len ((Sgm (rng (f mod p))) | n) = n by ;
then len f4 = n + m by
.= len f by A13 ;
then rng f4 = rng I by ;
then Product f4 = Product I by ;
then A115: (Product ((Sgm (rng (f mod p))) | n)) * (Product f3) = Product I by RVSUM_1:97;
f3 is FinSequence of INT by ;
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 ;
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 ;
then A116: Product I,((- 1) |^ m) * (Product (f mod p)) are_congruent_mod p by ;
((- 1) |^ m) * (Product (f mod p)),((- 1) |^ m) * () are_congruent_mod p by ;
then Product I,(((- 1) |^ m) * (a |^ ((p -' 1) div 2))) * () are_congruent_mod p by ;
then p divides (1 - (((- 1) |^ m) * (a |^ ((p -' 1) div 2)))) * () ;
then p divides 1 - (((- 1) |^ m) * (a |^ ((p -' 1) div 2))) by ;
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 ;
per cases ( (- 1) |^ m = 1 or (- 1) |^ m = - 1 ) by A77;
suppose A119: (- 1) |^ m = 1 ; :: thesis: Lege (a,p) = (- 1) |^ m
then A120: Lege (a,p) <> - 1 by ;
now :: thesis: not Lege (a,p) = 0
assume Lege (a,p) = 0 ; :: thesis: contradiction
then p divides 1 - 0 by ;
then p = 1 by WSIERP_1:15;
hence contradiction by A1; :: thesis: verum
end;
hence Lege (a,p) = (- 1) |^ m by ; :: thesis: verum
end;
suppose A121: (- 1) |^ m = - 1 ; :: thesis: Lege (a,p) = (- 1) |^ m
A122: now :: thesis: not Lege (a,p) = 1end;
now :: thesis: not Lege (a,p) = 0
assume Lege (a,p) = 0 ; :: thesis: contradiction
then p divides (- 1) - 0 by ;
then p = 1 by ;
hence contradiction by A1; :: thesis: verum
end;
hence Lege (a,p) = (- 1) |^ m by ; :: thesis: verum
end;
end;