let p, q be Prime; :: thesis: ( p > 2 & q > 2 & p <> q implies (Lege (p,q)) * (Lege (q,p)) = (- 1) |^ (((p -' 1) div 2) * ((q -' 1) div 2)) )
assume that
A1: p > 2 and
A2: q > 2 and
A3: p <> q ; :: thesis: (Lege (p,q)) * (Lege (q,p)) = (- 1) |^ (((p -' 1) div 2) * ((q -' 1) div 2))
A4: q,p are_coprime by A3, INT_2:30;
then A5: q gcd p = 1 by INT_2:def 3;
reconsider p = p, q = q as prime Element of NAT by ORDINAL1:def 12;
set p9 = (p -' 1) div 2;
A6: p > 1 by INT_2:def 4;
then A7: p -' 1 = p - 1 by XREAL_1:233;
then A8: p -' 1 > 0 by A6, XREAL_1:50;
p is odd by A1, PEPIN:17;
then A9: p -' 1 is even by A7, HILBERT3:2;
then A10: 2 divides p -' 1 by PEPIN:22;
then A11: p -' 1 = 2 * ((p -' 1) div 2) ;
then (p -' 1) div 2 divides p -' 1 ;
then (p -' 1) div 2 <= p -' 1 by A8, NAT_D:7;
then A12: (p -' 1) div 2 < p by A7, XREAL_1:146, XXREAL_0:2;
set f1 = q * (idseq ((p -' 1) div 2));
A13: for d being Nat st d in dom (q * (idseq ((p -' 1) div 2))) holds
(q * (idseq ((p -' 1) div 2))) . d = q * d

proof

let d be Nat; :: thesis: ( d in dom (q * (idseq ((p -' 1) div 2))) implies (q * (idseq ((p -' 1) div 2))) . d = q * d )
assume A14: d in dom (q * (idseq ((p -' 1) div 2))) ; :: thesis: (q * (idseq ((p -' 1) div 2))) . d = q * d
then d in dom (idseq ((p -' 1) div 2)) by VALUED_1:def 5;
then d in Seg (len (idseq ((p -' 1) div 2))) by FINSEQ_1:def 3;
then A15: d is Element of Seg ((p -' 1) div 2) by CARD_1:def 7;
(q * (idseq ((p -' 1) div 2))) . d = q * ((idseq ((p -' 1) div 2)) . d) by A14, VALUED_1:def 5;
hence (q * (idseq ((p -' 1) div 2))) . d = q * d by A15; :: thesis: verum

end;

A16: for d being Nat st d in dom (q * (idseq ((p -' 1) div 2))) holds
(q * (idseq ((p -' 1) div 2))) . d in NAT ;
dom (q * (idseq ((p -' 1) div 2))) = dom (idseq ((p -' 1) div 2)) by VALUED_1:def 5;
then A17: len (q * (idseq ((p -' 1) div 2))) = len (idseq ((p -' 1) div 2)) by FINSEQ_3:29;
then A18: len (q * (idseq ((p -' 1) div 2))) = (p -' 1) div 2 by CARD_1:def 7;
set q9 = (q -' 1) div 2;
set g1 = p * (idseq ((q -' 1) div 2));
A19: for d being Nat st d in dom (p * (idseq ((q -' 1) div 2))) holds
(p * (idseq ((q -' 1) div 2))) . d = p * d

proof

let d be Nat; :: thesis: ( d in dom (p * (idseq ((q -' 1) div 2))) implies (p * (idseq ((q -' 1) div 2))) . d = p * d )
assume A20: d in dom (p * (idseq ((q -' 1) div 2))) ; :: thesis: (p * (idseq ((q -' 1) div 2))) . d = p * d
then d in dom (idseq ((q -' 1) div 2)) by VALUED_1:def 5;
then d in Seg (len (idseq ((q -' 1) div 2))) by FINSEQ_1:def 3;
then A21: d is Element of Seg ((q -' 1) div 2) by CARD_1:def 7;
(p * (idseq ((q -' 1) div 2))) . d = p * ((idseq ((q -' 1) div 2)) . d) by A20, VALUED_1:def 5;
hence (p * (idseq ((q -' 1) div 2))) . d = p * d by A21; :: thesis: verum

end;

A22: for d being Nat st d in dom (p * (idseq ((q -' 1) div 2))) holds
(p * (idseq ((q -' 1) div 2))) . d in NAT ;
dom (p * (idseq ((q -' 1) div 2))) = dom (idseq ((q -' 1) div 2)) by VALUED_1:def 5;
then len (p * (idseq ((q -' 1) div 2))) = len (idseq ((q -' 1) div 2)) by FINSEQ_3:29;
then A23: len (p * (idseq ((q -' 1) div 2))) = (q -' 1) div 2 by CARD_1:def 7;
reconsider g1 = p * (idseq ((q -' 1) div 2)) as FinSequence of NAT by A22, FINSEQ_2:12;
set g3 = g1 mod q;
reconsider g3 = g1 mod q as FinSequence of NAT by FINSEQ_1:102;
set g4 = Sgm (rng g3);
A24: len g3 = len g1 by EULER_2:def 2;
then A25: dom g1 = dom g3 by FINSEQ_3:29;
set XX = { k where k is Element of NAT : ( k in rng (Sgm (rng g3)) & k > q / 2 ) } ;
for x being object st x in { k where k is Element of NAT : ( k in rng (Sgm (rng g3)) & k > q / 2 ) } holds
x in rng (Sgm (rng g3))

proof

let x be object ; :: thesis: ( x in { k where k is Element of NAT : ( k in rng (Sgm (rng g3)) & k > q / 2 ) } implies x in rng (Sgm (rng g3)) )
assume x in { k where k is Element of NAT : ( k in rng (Sgm (rng g3)) & k > q / 2 ) } ; :: thesis: x in rng (Sgm (rng g3))
then ex k being Element of NAT st
( x = k & k in rng (Sgm (rng g3)) & k > q / 2 ) ;
hence x in rng (Sgm (rng g3)) ; :: thesis: verum

end;

then A26: { k where k is Element of NAT : ( k in rng (Sgm (rng g3)) & k > q / 2 ) } c= rng (Sgm (rng g3)) ;
reconsider f1 = q * (idseq ((p -' 1) div 2)) as FinSequence of NAT by A16, FINSEQ_2:12;
deffunc H₁( Nat) -> Element of omega = (f1 . $1) div p;
consider f2 being FinSequence such that
A27: ( len f2 = (p -' 1) div 2 & ( for d being Nat st d in dom f2 holds
f2 . d = H₁(d) ) ) from FINSEQ_1:sch 2();
A28: q > 1 by INT_2:def 4;
then A29: q -' 1 = q - 1 by XREAL_1:233;
then A30: q -' 1 > 0 by A28, XREAL_1:50;
q >= 2 + 1 by A2, NAT_1:13;
then q - 1 >= 3 - 1 by XREAL_1:9;
then A31: (q -' 1) div 2 >= 1 by A29, NAT_2:13;
then len g3 >= 1 by A23, EULER_2:def 2;
then g3 <> {} ;
then rng g3 is non empty finite Subset of NAT ;
then consider n2 being Element of NAT such that
A32: rng g3 c= (Seg n2) \/ {0} by HEYTING3:1;
deffunc H₂( Nat) -> Element of omega = (g1 . $1) div q;
consider g2 being FinSequence such that
A33: ( len g2 = (q -' 1) div 2 & ( for d being Nat st d in dom g2 holds
g2 . d = H₂(d) ) ) from FINSEQ_1:sch 2();
for d being Nat st d in dom g2 holds
g2 . d in NAT

proof

let d be Nat; :: thesis: ( d in dom g2 implies g2 . d in NAT )
assume d in dom g2 ; :: thesis: g2 . d in NAT
then g2 . d = (g1 . d) div q by A33;
hence g2 . d in NAT ; :: thesis: verum

end;

then reconsider g2 = g2 as FinSequence of NAT by FINSEQ_2:12;
A34: dom g1 = dom g2 by A23, A33, FINSEQ_3:29;
A35: for d being Nat st d in dom g1 holds
g1 . d = ((g2 . d) * q) + (g3 . d)

proof

let d be Nat; :: thesis: ( d in dom g1 implies g1 . d = ((g2 . d) * q) + (g3 . d) )
assume A36: d in dom g1 ; :: thesis: g1 . d = ((g2 . d) * q) + (g3 . d)
then A37: g3 . d = (g1 . d) mod q by EULER_2:def 2;
g2 . d = (g1 . d) div q by A33, A34, A36;
hence g1 . d = ((g2 . d) * q) + (g3 . d) by A37, NAT_D:2; :: thesis: verum

end;

q is odd by A2, PEPIN:17;
then A38: q -' 1 is even by A29, HILBERT3:2;
then A39: 2 divides q -' 1 by PEPIN:22;
then A40: q -' 1 = 2 * ((q -' 1) div 2) ;
then (q -' 1) div 2 divides q -' 1 ;
then (q -' 1) div 2 <= q -' 1 by A30, NAT_D:7;
then A41: (q -' 1) div 2 < q by A29, XREAL_1:146, XXREAL_0:2;
not 0 in rng g3

proof

assume 0 in rng g3 ; :: thesis: contradiction
then consider a being Nat such that
A42: a in dom g3 and
A43: g3 . a = 0 by FINSEQ_2:10;
a in dom g1 by A24, A42, FINSEQ_3:29;
then A44: g1 . a = ((g2 . a) * q) + 0 by A35, A43;
a in dom g1 by A24, A42, FINSEQ_3:29;
then p * a = (g2 . a) * q by A19, A44;
then A45: q divides p * a ;
a >= 1 by A42, FINSEQ_3:25;
then A46: q <= a by A4, A45, NAT_D:7, PEPIN:3;
a <= (q -' 1) div 2 by A23, A24, A42, FINSEQ_3:25;
hence contradiction by A41, A46, XXREAL_0:2; :: thesis: verum

end;

then A47: {0} misses rng g3 by ZFMISC_1:50;
rng g3 c= Seg n2 by A32, A47, XBOOLE_1:73;
then kkk: rng g3 is included_in_Seg by FINSEQ_1:def 13;
then A48: Sgm (rng g3) is one-to-one by FINSEQ_3:92;
A49: for d, e being Nat st d in dom g1 & e in dom g1 & q divides (g1 . d) - (g1 . e) holds
d = e

proof

A50: q,p are_coprime by A3, INT_2:30;
let d, e be Nat; :: thesis: ( d in dom g1 & e in dom g1 & q divides (g1 . d) - (g1 . e) implies d = e )
assume that
A51: d in dom g1 and
A52: e in dom g1 and
A53: q divides (g1 . d) - (g1 . e) ; :: thesis: d = e
A54: g1 . e = p * e by A19, A52;
g1 . d = p * d by A19, A51;
then A55: q divides (d - e) * p by A53, A54;

now :: thesis: not d <> e

assume d <> e ; :: thesis: contradiction
then d - e <> 0 ;
then |.q.| <= |.(d - e).| by A55, A50, INT_2:25, INT_4:6;
then A56: q <= |.(d - e).| by ABSVALUE:def 1;
A57: e >= 1 by A52, FINSEQ_3:25;
A58: d >= 1 by A51, FINSEQ_3:25;
e <= (q -' 1) div 2 by A23, A52, FINSEQ_3:25;
then A59: d - e >= 1 - ((q -' 1) div 2) by A58, XREAL_1:13;
A60: ((q -' 1) div 2) - 1 < q by A41, XREAL_1:147;
d <= (q -' 1) div 2 by A23, A51, FINSEQ_3:25;
then d - e <= ((q -' 1) div 2) - 1 by A57, XREAL_1:13;
then A61: d - e < q by A60, XXREAL_0:2;
- (((q -' 1) div 2) - 1) > - q by A60, XREAL_1:24;
then d - e > - q by A59, XXREAL_0:2;
hence contradiction by A56, A61, SEQ_2:1; :: thesis: verum

end;

hence d = e ; :: thesis: verum

end;

for x, y being object st x in dom g3 & y in dom g3 & g3 . x = g3 . y holds
x = y

proof

let x, y be object ; :: thesis: ( x in dom g3 & y in dom g3 & g3 . x = g3 . y implies x = y )
assume that
A62: x in dom g3 and
A63: y in dom g3 and
A64: g3 . x = g3 . y ; :: thesis: x = y
reconsider x = x, y = y as Element of NAT by A62, A63;
A65: g1 . y = ((g2 . y) * q) + (g3 . y) by A25, A35, A63;
g1 . x = ((g2 . x) * q) + (g3 . x) by A25, A35, A62;
then (g1 . x) - (g1 . y) = ((g2 . x) - (g2 . y)) * q by A64, A65;
then q divides (g1 . x) - (g1 . y) ;
hence x = y by A49, A25, A62, A63; :: thesis: verum

end;

then A66: g3 is one-to-one ;
then len g3 = card (rng g3) by FINSEQ_4:62;
then A67: len (Sgm (rng g3)) = (q -' 1) div 2 by kkk, A23, A24, FINSEQ_3:39;
reconsider XX = { k where k is Element of NAT : ( k in rng (Sgm (rng g3)) & k > q / 2 ) } as finite Subset of NAT by A26, XBOOLE_1:1;
set mm = card XX;
reconsider YY = (rng (Sgm (rng g3))) \ XX as finite Subset of NAT ;
A68: g3 is Element of NAT * by FINSEQ_1:def 11;
len g3 = (q -' 1) div 2 by A23, EULER_2:def 2;
then g3 in ((q -' 1) div 2) -tuples_on NAT by A68;
then A69: g3 is Element of ((q -' 1) div 2) -tuples_on REAL by FINSEQ_2:109, NUMBERS:19;
for d being Nat st d in dom (idseq ((q -' 1) div 2)) holds
(idseq ((q -' 1) div 2)) . d in NAT ;
then idseq ((q -' 1) div 2) is FinSequence of NAT by FINSEQ_2:12;
then reconsider N = Sum (idseq ((q -' 1) div 2)) as Element of NAT by Lm4;
A70: 2,q are_coprime by A2, EULER_1:2;
dom (q * g2) = dom g2 by VALUED_1:def 5;
then A71: len (q * g2) = (q -' 1) div 2 by A33, FINSEQ_3:29;
q * g2 is Element of NAT * by FINSEQ_1:def 11;
then q * g2 in ((q -' 1) div 2) -tuples_on NAT by A71;
then A72: q * g2 is Element of ((q -' 1) div 2) -tuples_on REAL by FINSEQ_2:109, NUMBERS:19;
A73: dom ((q * g2) + g3) = (dom (q * g2)) /\ (dom g3) by VALUED_1:def 1
.= (dom g2) /\ (dom g3) by VALUED_1:def 5
.= dom g1 by A25, A34 ;
for d being Nat st d in dom g1 holds
g1 . d = ((q * g2) + g3) . d

proof

let d be Nat; :: thesis: ( d in dom g1 implies g1 . d = ((q * g2) + g3) . d )
assume A74: d in dom g1 ; :: thesis: g1 . d = ((q * g2) + g3) . d
then A75: d in dom (q * g2) by A34, VALUED_1:def 5;
((q * g2) + g3) . d = ((q * g2) . d) + (g3 . d) by A73, A74, VALUED_1:def 1;
hence ((q * g2) + g3) . d = (q * (g2 . d)) + (g3 . d) by A75, VALUED_1:def 5
.= g1 . d by A35, A74 ;
:: thesis: verum

end;

then g1 = (q * g2) + g3 by A73;
then A76: Sum g1 = (Sum (q * g2)) + (Sum g3) by A72, A69, RVSUM_1:89
.= (q * (Sum g2)) + (Sum g3) by RVSUM_1:87 ;
A77: rng g3 c= Seg n2 by A32, A47, XBOOLE_1:73;
then rng g3 is included_in_Seg by FINSEQ_1:def 13;
then A78: rng (Sgm (rng g3)) = rng g3 by FINSEQ_1:def 14;
then XX c= Seg n2 by A77, A26;
then a79: XX is included_in_Seg by FINSEQ_1:def 13;
A80: len g3 = card (rng (Sgm (rng g3))) by A66, A78, FINSEQ_4:62;
card XX <= card (rng (Sgm (rng g3))) by A26, NAT_1:43;
then card XX <= (q -' 1) div 2 by A23, A80, EULER_2:def 2;
then reconsider nn = ((q -' 1) div 2) - (card XX) as Element of NAT by NAT_1:21;
A81: Sgm (rng g3) = ((Sgm (rng g3)) | nn) ^ ((Sgm (rng g3)) /^ nn) by RFINSEQ:8;
then A82: (Sgm (rng g3)) /^ nn is one-to-one by A48, FINSEQ_3:91;
A83: (q -' 1) div 2 = ((q -' 1) + 1) div 2 by A38, NAT_2:26
.= q div 2 by A28, XREAL_1:235 ;
A85: Sum (Sgm (rng g3)) = Sum g3 by A66, A78, A48, RFINSEQ:9, RFINSEQ:26;
(rng (Sgm (rng g3))) \ XX c= rng (Sgm (rng g3)) by XBOOLE_1:36;
then YY c= Seg n2 by A77, A78;
then a87: YY is included_in_Seg by FINSEQ_1:def 13;
for k, l being Nat st k in YY & l in XX holds
k < l

proof

let k, l be Nat; :: thesis: ( k in YY & l in XX implies k < l )
assume that
A88: k in YY and
A89: l in XX ; :: thesis: k < l
A90: not k in XX by A88, XBOOLE_0:def 5;
A91: ex l1 being Element of NAT st
( l1 = l & l1 in rng (Sgm (rng g3)) & l1 > q / 2 ) by A89;
k in rng (Sgm (rng g3)) by A88, XBOOLE_0:def 5;
then k <= q / 2 by A90;
hence k < l by A91, XXREAL_0:2; :: thesis: verum

end;

then Sgm (YY \/ XX) = (Sgm YY) ^ (Sgm XX) by a87, a79, FINSEQ_3:42;
then Sgm ((rng (Sgm (rng g3))) \/ XX) = (Sgm YY) ^ (Sgm XX) by XBOOLE_1:39;
then A92: Sgm (rng g3) = (Sgm YY) ^ (Sgm XX) by A78, A26, XBOOLE_1:12;
then Sum (Sgm (rng g3)) = (Sum (Sgm YY)) + (Sum (Sgm XX)) by RVSUM_1:75;
then A93: p * (Sum (idseq ((q -' 1) div 2))) = ((q * (Sum g2)) + (Sum (Sgm YY))) + (Sum (Sgm XX)) by A76, A85, RVSUM_1:87;
A94: len (Sgm YY) = card YY by a87, FINSEQ_3:39
.= ((q -' 1) div 2) - (card XX) by A23, A24, A26, A80, CARD_2:44 ;
then A95: (Sgm (rng g3)) /^ nn = Sgm XX by A92, FINSEQ_5:37;
for d being Nat st d in dom f2 holds
f2 . d in NAT

proof

let d be Nat; :: thesis: ( d in dom f2 implies f2 . d in NAT )
assume d in dom f2 ; :: thesis: f2 . d in NAT
then f2 . d = (f1 . d) div p by A27;
hence f2 . d in NAT ; :: thesis: verum

end;

then reconsider f2 = f2 as FinSequence of NAT by FINSEQ_2:12;
set f3 = f1 mod p;
reconsider f3 = f1 mod p as FinSequence of NAT by FINSEQ_1:102;
A96: len f3 = len f1 by EULER_2:def 2;
then A97: dom f1 = dom f3 by FINSEQ_3:29;
set f4 = Sgm (rng f3);
p >= 2 + 1 by A1, NAT_1:13;
then A98: p - 1 >= 3 - 1 by XREAL_1:9;
then f3 <> {} by A18, A7, A96, NAT_2:13;
then rng f3 is non empty finite Subset of NAT ;
then consider n1 being Element of NAT such that
A99: rng f3 c= (Seg n1) \/ {0} by HEYTING3:1;
A100: dom f1 = dom f2 by A18, A27, FINSEQ_3:29;
A101: for d being Nat st d in dom f1 holds
f1 . d = ((f2 . d) * p) + (f3 . d)

proof

let d be Nat; :: thesis: ( d in dom f1 implies f1 . d = ((f2 . d) * p) + (f3 . d) )
assume A102: d in dom f1 ; :: thesis: f1 . d = ((f2 . d) * p) + (f3 . d)
then A103: f3 . d = (f1 . d) mod p by EULER_2:def 2;
f2 . d = (f1 . d) div p by A27, A100, A102;
hence f1 . d = ((f2 . d) * p) + (f3 . d) by A103, NAT_D:2; :: thesis: verum

end;

not 0 in rng f3

proof

assume 0 in rng f3 ; :: thesis: contradiction
then consider a being Nat such that
A104: a in dom f3 and
A105: f3 . a = 0 by FINSEQ_2:10;
f1 . a = ((f2 . a) * p) + 0 by A97, A101, A104, A105;
then q * a = (f2 . a) * p by A13, A97, A104;
then A106: p divides q * a ;
a >= 1 by A104, FINSEQ_3:25;
then A107: p <= a by A4, A106, NAT_D:7, PEPIN:3;
a <= (p -' 1) div 2 by A18, A96, A104, FINSEQ_3:25;
hence contradiction by A12, A107, XXREAL_0:2; :: thesis: verum

end;

then A108: {0} misses rng f3 by ZFMISC_1:50;
then rng f3 c= Seg n1 by A99, XBOOLE_1:73;
then ttt: rng f3 is included_in_Seg by FINSEQ_1:def 13;
then A109: Sgm (rng f3) is one-to-one by FINSEQ_3:92;
A110: for d, e being Nat st d in dom f1 & e in dom f1 & p divides (f1 . d) - (f1 . e) holds
d = e

proof

A111: q,p are_coprime by A3, INT_2:30;
let d, e be Nat; :: thesis: ( d in dom f1 & e in dom f1 & p divides (f1 . d) - (f1 . e) implies d = e )
assume that
A112: d in dom f1 and
A113: e in dom f1 and
A114: p divides (f1 . d) - (f1 . e) ; :: thesis: d = e
A115: f1 . e = q * e by A13, A113;
f1 . d = q * d by A13, A112;
then A116: p divides (d - e) * q by A114, A115;

now :: thesis: not d <> e

assume d <> e ; :: thesis: contradiction
then d - e <> 0 ;
then |.p.| <= |.(d - e).| by A116, A111, INT_2:25, INT_4:6;
then A117: p <= |.(d - e).| by ABSVALUE:def 1;
A118: e >= 1 by A113, FINSEQ_3:25;
A119: d >= 1 by A112, FINSEQ_3:25;
e <= (p -' 1) div 2 by A18, A113, FINSEQ_3:25;
then A120: d - e >= 1 - ((p -' 1) div 2) by A119, XREAL_1:13;
A121: ((p -' 1) div 2) - 1 < p by A12, XREAL_1:147;
d <= (p -' 1) div 2 by A18, A112, FINSEQ_3:25;
then d - e <= ((p -' 1) div 2) - 1 by A118, XREAL_1:13;
then A122: d - e < p by A121, XXREAL_0:2;
- (((p -' 1) div 2) - 1) > - p by A121, XREAL_1:24;
then d - e > - p by A120, XXREAL_0:2;
hence contradiction by A117, A122, SEQ_2:1; :: thesis: verum

end;

hence d = e ; :: thesis: verum

end;

for x, y being object st x in dom f3 & y in dom f3 & f3 . x = f3 . y holds
x = y

proof

let x, y be object ; :: thesis: ( x in dom f3 & y in dom f3 & f3 . x = f3 . y implies x = y )
assume that
A123: x in dom f3 and
A124: y in dom f3 and
A125: f3 . x = f3 . y ; :: thesis: x = y
reconsider x = x, y = y as Element of NAT by A123, A124;
A126: f1 . y = ((f2 . y) * p) + (f3 . y) by A97, A101, A124;
f1 . x = ((f2 . x) * p) + (f3 . x) by A97, A101, A123;
then (f1 . x) - (f1 . y) = ((f2 . x) - (f2 . y)) * p by A125, A126;
then p divides (f1 . x) - (f1 . y) ;
hence x = y by A110, A97, A123, A124; :: thesis: verum

end;

then A127: f3 is one-to-one ;
then len f3 = card (rng f3) by FINSEQ_4:62;
then A128: len (Sgm (rng f3)) = (p -' 1) div 2 by ttt, A18, A96, FINSEQ_3:39;
A129: (Sgm (rng g3)) | nn = Sgm YY by A92, A94, FINSEQ_3:113, FINSEQ_6:10;
A130: (Sgm (rng g3)) | nn is one-to-one by A48, A81, FINSEQ_3:91;
A131: Lege (p,q) = (- 1) |^ (Sum g2)

proof

set g5 = ((card XX) |-> q) - ((Sgm (rng g3)) /^ nn);
set g6 = ((Sgm (rng g3)) | nn) ^ (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn));
A132: (Sgm (rng g3)) /^ nn is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;
A133: len ((Sgm (rng g3)) | nn) = nn by A67, FINSEQ_1:59, XREAL_1:43;
A134: len ((Sgm (rng g3)) /^ nn) = (len (Sgm (rng g3))) -' nn by RFINSEQ:29
.= (len (Sgm (rng g3))) - nn by A67, XREAL_1:43, XREAL_1:233
.= card XX by A67 ;
A135: dom (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) = (dom ((card XX) |-> q)) /\ (dom ((Sgm (rng g3)) /^ nn)) by VALUED_1:12
.= (Seg (len ((card XX) |-> q))) /\ (dom ((Sgm (rng g3)) /^ nn)) by FINSEQ_1:def 3
.= (dom ((Sgm (rng g3)) /^ nn)) /\ (dom ((Sgm (rng g3)) /^ nn)) by FINSEQ_1:def 3, A134, CARD_1:def 7
.= dom ((Sgm (rng g3)) /^ nn) ;
then A136: len (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) = len ((Sgm (rng g3)) /^ nn) by FINSEQ_3:29;
A137: for d being Nat st d in dom (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) holds
(((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) . d = q - (((Sgm (rng g3)) /^ nn) . d)

proof

let d be Nat; :: thesis: ( d in dom (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) implies (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) . d = q - (((Sgm (rng g3)) /^ nn) . d) )
assume A138: d in dom (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) ; :: thesis: (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) . d = q - (((Sgm (rng g3)) /^ nn) . d)
then d in Seg (card XX) by A134, A135, FINSEQ_1:def 3;
then ((card XX) |-> q) . d = q by FINSEQ_2:57;
hence (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) . d = q - (((Sgm (rng g3)) /^ nn) . d) by A138, VALUED_1:13; :: thesis: verum

end;

A139: for d being Nat st d in dom (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) holds
( (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) . d > 0 & (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) . d <= (q -' 1) div 2 )

proof

let d be Nat; :: thesis: ( d in dom (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) implies ( (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) . d > 0 & (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) . d <= (q -' 1) div 2 ) )
reconsider w = (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) . d as Element of INT by INT_1:def 2;
assume A140: d in dom (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) ; :: thesis: ( (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) . d > 0 & (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) . d <= (q -' 1) div 2 )
then (Sgm XX) . d in rng (Sgm XX) by A95, A135, FUNCT_1:3;
then (Sgm XX) . d in XX by a79, FINSEQ_1:def 14;
then A141: ex ll being Element of NAT st
( ll = (Sgm XX) . d & ll in rng g3 & ll > q / 2 ) by A78;
then consider e being Nat such that
A142: e in dom g3 and
A143: g3 . e = ((Sgm (rng g3)) /^ nn) . d by A95, FINSEQ_2:10;
((Sgm (rng g3)) /^ nn) . d = (g1 . e) mod q by A25, A142, A143, EULER_2:def 2;
then A144: ((Sgm (rng g3)) /^ nn) . d < q by NAT_D:1;
A145: (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) . d = q - (((Sgm (rng g3)) /^ nn) . d) by A137, A140;
then w < q - (q / 2) by A95, A141, XREAL_1:10;
hence ( (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) . d > 0 & (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) . d <= (q -' 1) div 2 ) by A83, A145, A144, INT_1:54, XREAL_1:50; :: thesis: verum

end;

for d being Nat st d in dom (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) holds
(((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) . d in NAT

proof

let d be Nat; :: thesis: ( d in dom (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) implies (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) . d in NAT )
assume A147: d in dom (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) ; :: thesis: (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) . d in NAT
(((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) . d > 0 by A139, A147;
hence (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) . d in NAT by INT_1:3; :: thesis: verum

end;

then reconsider g5 = ((card XX) |-> q) - ((Sgm (rng g3)) /^ nn) as FinSequence of NAT by FINSEQ_2:12;
g5 is FinSequence of NAT ;
then reconsider g6 = ((Sgm (rng g3)) | nn) ^ (((card XX) |-> q) - ((Sgm (rng g3)) /^ nn)) as FinSequence of NAT by FINSEQ_1:75;
A149: nn <= len (Sgm (rng g3)) by A67, XREAL_1:43;
A150: rng ((Sgm (rng g3)) | nn) misses rng g5

proof

assume not rng ((Sgm (rng g3)) | nn) misses rng g5 ; :: thesis: contradiction
then consider x being object such that
A151: x in rng ((Sgm (rng g3)) | nn) and
A152: x in rng g5 by XBOOLE_0:3;
consider e being Nat such that
A153: e in dom g5 and
A154: g5 . e = x by A152, FINSEQ_2:10;
x = q - (((Sgm (rng g3)) /^ nn) . e) by A137, A153, A154;
then A155: x = q - ((Sgm (rng g3)) . (e + nn)) by A149, A135, A153, RFINSEQ:def 1;
e + nn in dom (Sgm (rng g3)) by A135, A153, FINSEQ_5:26;
then consider e1 being Nat such that
A156: e1 in dom g3 and
A157: g3 . e1 = (Sgm (rng g3)) . (e + nn) by A78, FINSEQ_2:10, FUNCT_1:3;
A158: e1 <= (q -' 1) div 2 by A23, A24, A156, FINSEQ_3:25;
rng ((Sgm (rng g3)) | nn) c= rng (Sgm (rng g3)) by FINSEQ_5:19;
then consider d1 being Nat such that
A159: d1 in dom g3 and
A160: g3 . d1 = x by A78, A151, FINSEQ_2:10;
d1 <= (q -' 1) div 2 by A23, A24, A159, FINSEQ_3:25;
then d1 + e1 <= ((q -' 1) div 2) + ((q -' 1) div 2) by A158, XREAL_1:7;
then A161: d1 + e1 < q by A29, A40, XREAL_1:146, XXREAL_0:2;
A162: e1 in dom g1 by A24, A156, FINSEQ_3:29;
then A163: (Sgm (rng g3)) . (e + nn) = (g1 . e1) mod q by A157, EULER_2:def 2;
A164: d1 in dom g1 by A24, A159, FINSEQ_3:29;
then x = (g1 . d1) mod q by A160, EULER_2:def 2;
then (((g1 . d1) mod q) + ((g1 . e1) mod q)) mod q = 0 by A155, A163, NAT_D:25;
then ((g1 . d1) + (g1 . e1)) mod q = 0 by NAT_D:66;
then q divides (g1 . d1) + (g1 . e1) by PEPIN:6;
then q divides (d1 * p) + (g1 . e1) by A19, A164;
then q divides (d1 * p) + (e1 * p) by A19, A162;
then A165: q divides (d1 + e1) * p ;
d1 >= 1 by A159, FINSEQ_3:25;
hence contradiction by A4, A165, A161, NAT_D:7, PEPIN:3; :: thesis: verum

end;

for d, e being Nat st 1 <= d & d < e & e <= len g5 holds
g5 . d <> g5 . e

proof

let d, e be Nat; :: thesis: ( 1 <= d & d < e & e <= len g5 implies g5 . d <> g5 . e )
assume that
A166: 1 <= d and
A167: d < e and
A168: e <= len g5 ; :: thesis: g5 . d <> g5 . e
1 <= e by A166, A167, XXREAL_0:2;
then A169: e in dom g5 by A168, FINSEQ_3:25;
then A170: g5 . e = q - (((Sgm (rng g3)) /^ nn) . e) by A137;
d < len g5 by A167, A168, XXREAL_0:2;
then A171: d in dom g5 by A166, FINSEQ_3:25;
then g5 . d = q - (((Sgm (rng g3)) /^ nn) . d) by A137;
hence g5 . d <> g5 . e by A82, A135, A167, A171, A169, A170; :: thesis: verum

end;

then len g5 = card (rng g5) by GRAPH_5:7;
then g5 is one-to-one by FINSEQ_4:62;
then A172: g6 is one-to-one by A130, A150, FINSEQ_3:91;
A173: for d being Nat st d in dom g6 holds
( g6 . d > 0 & g6 . d <= (q -' 1) div 2 )

proof

let d be Nat; :: thesis: ( d in dom g6 implies ( g6 . d > 0 & g6 . d <= (q -' 1) div 2 ) )
assume A174: d in dom g6 ; :: thesis: ( g6 . d > 0 & g6 . d <= (q -' 1) div 2 )

per cases ( d in dom ((Sgm (rng g3)) | nn) or ex l being Nat st
( l in dom g5 & d = (len ((Sgm (rng g3)) | nn)) + l ) ) by A174, FINSEQ_1:25;

suppose A175: d in dom ((Sgm (rng g3)) | nn) ; :: thesis: ( g6 . d > 0 & g6 . d <= (q -' 1) div 2 )

then ((Sgm (rng g3)) | nn) . d in rng (Sgm YY) by A129, FUNCT_1:3;
then A176: ((Sgm (rng g3)) | nn) . d in YY by a87, FINSEQ_1:def 14;
then A177: ((Sgm (rng g3)) | nn) . d in rng (Sgm (rng g3)) by XBOOLE_0:def 5;
not ((Sgm (rng g3)) | nn) . d in XX by A176, XBOOLE_0:def 5;
then ((Sgm (rng g3)) | nn) . d <= q / 2 by A177;
then A178: ((Sgm (rng g3)) | nn) . d <= (q -' 1) div 2 by A83, INT_1:54;
not ((Sgm (rng g3)) | nn) . d in {0} by A47, A78, A177, XBOOLE_0:3;
then ((Sgm (rng g3)) | nn) . d <> 0 by TARSKI:def 1;
hence ( g6 . d > 0 & g6 . d <= (q -' 1) div 2 ) by A175, A178, FINSEQ_1:def 7; :: thesis: verum

end;

suppose ex l being Nat st
( l in dom g5 & d = (len ((Sgm (rng g3)) | nn)) + l ) ; :: thesis: ( g6 . d > 0 & g6 . d <= (q -' 1) div 2 )

then consider l being Element of NAT such that
A179: l in dom g5 and
A180: d = (len ((Sgm (rng g3)) | nn)) + l ;
g6 . d = g5 . l by A179, A180, FINSEQ_1:def 7;
hence ( g6 . d > 0 & g6 . d <= (q -' 1) div 2 ) by A139, A179; :: thesis: verum

end;

end;

end;

len g6 = (len ((Sgm (rng g3)) | nn)) + (len g5) by FINSEQ_1:22
.= (q -' 1) div 2 by A133, A134, A136 ;
then rng g6 = rng (idseq ((q -' 1) div 2)) by A172, A173, Th40;
then N = Sum g6 by A172, RFINSEQ:9, RFINSEQ:26
.= (Sum ((Sgm (rng g3)) | nn)) + (Sum g5) by RVSUM_1:75
.= (Sum ((Sgm (rng g3)) | nn)) + (((card XX) * q) - (Sum ((Sgm (rng g3)) /^ nn))) by A134, A132, Th47
.= ((Sum ((Sgm (rng g3)) | nn)) + ((card XX) * q)) - (Sum ((Sgm (rng g3)) /^ nn)) ;
then (p - 1) * N = ((q * (Sum g2)) + (2 * (Sum (Sgm XX)))) - ((card XX) * q) by A93, A95, A129;
then A182: ((p -' 1) * N) mod 2 = (((q * (Sum g2)) - ((card XX) * q)) + (2 * (Sum (Sgm XX)))) mod 2 by A6, XREAL_1:233
.= ((q * (Sum g2)) - ((card XX) * q)) mod 2 by NAT_D:61 ;
2 divides (p -' 1) * N by A10, NAT_D:9;
then (q * ((Sum g2) - (card XX))) mod 2 = 0 by A182, PEPIN:6;
then 2 divides q * ((Sum g2) - (card XX)) by Lm1;
then 2 divides (Sum g2) - (card XX) by A70, INT_2:25;
then Sum g2, card XX are_congruent_mod 2 ;
then (Sum g2) mod 2 = (card XX) mod 2 by NAT_D:64;
then (- 1) |^ (Sum g2) = (- 1) |^ (card XX) by Th45;
hence Lege (p,q) = (- 1) |^ (Sum g2) by A2, A5, A78, Th41; :: thesis: verum

end;

for d being Nat st d in dom (idseq ((p -' 1) div 2)) holds
(idseq ((p -' 1) div 2)) . d in NAT ;
then idseq ((p -' 1) div 2) is FinSequence of NAT by FINSEQ_2:12;
then reconsider M = Sum (idseq ((p -' 1) div 2)) as Element of NAT by Lm4;
A183: 2,p are_coprime by A1, EULER_1:2;
set X = { k where k is Element of NAT : ( k in rng (Sgm (rng f3)) & k > p / 2 ) } ;
for x being object st x in { k where k is Element of NAT : ( k in rng (Sgm (rng f3)) & k > p / 2 ) } holds
x in rng (Sgm (rng f3))

proof

let x be object ; :: thesis: ( x in { k where k is Element of NAT : ( k in rng (Sgm (rng f3)) & k > p / 2 ) } implies x in rng (Sgm (rng f3)) )
assume x in { k where k is Element of NAT : ( k in rng (Sgm (rng f3)) & k > p / 2 ) } ; :: thesis: x in rng (Sgm (rng f3))
then ex k being Element of NAT st
( x = k & k in rng (Sgm (rng f3)) & k > p / 2 ) ;
hence x in rng (Sgm (rng f3)) ; :: thesis: verum

end;

then A184: { k where k is Element of NAT : ( k in rng (Sgm (rng f3)) & k > p / 2 ) } c= rng (Sgm (rng f3)) ;
A185: (p -' 1) div 2 >= 1 by A7, A98, NAT_2:13;
A186: (Sum f2) + (Sum g2) = ((p -' 1) div 2) * ((q -' 1) div 2)

proof

reconsider A = Seg ((p -' 1) div 2), B = Seg ((q -' 1) div 2) as non empty finite Subset of NAT by A185, A31;
deffunc H₃( Element of A, Element of B) -> set = ($1 / p) - ($2 / q);
A187: for x being Element of A
for y being Element of B holds H₃(x,y) in REAL by XREAL_0:def 1;
consider z being Function of [:A,B:],REAL such that
A188: for x being Element of A
for y being Element of B holds z . (x,y) = H₃(x,y) from FUNCT_7:sch 1(A187);
defpred S₁[ set , set ] means ex x being Element of A st
( $1 = x & $2 = { [x,y] where y is Element of B : z . (x,y) > 0 } );
A189: for d being Nat st d in Seg ((p -' 1) div 2) holds
ex x1 being Element of bool (dom z) st S₁[d,x1]

proof

let d be Nat; :: thesis: ( d in Seg ((p -' 1) div 2) implies ex x1 being Element of bool (dom z) st S₁[d,x1] )
assume d in Seg ((p -' 1) div 2) ; :: thesis: ex x1 being Element of bool (dom z) st S₁[d,x1]
then reconsider d = d as Element of A ;
take x1 = { [d,y] where y is Element of B : z . (d,y) > 0 } ; :: thesis: ( x1 is Element of bool (dom z) & S₁[d,x1] )
x1 c= dom z

proof

let l be object ; :: according to TARSKI:def 3 :: thesis: ( not l in x1 or l in dom z )
assume l in x1 ; :: thesis: l in dom z
then ex yy being Element of B st
( [d,yy] = l & z . (d,yy) > 0 ) ;
then l in [:A,B:] ;
hence l in dom z by FUNCT_2:def 1; :: thesis: verum

end;

hence ( x1 is Element of bool (dom z) & S₁[d,x1] ) ; :: thesis: verum

end;

consider Pr being FinSequence of bool (dom z) such that
A190: ( dom Pr = Seg ((p -' 1) div 2) & ( for d being Nat st d in Seg ((p -' 1) div 2) holds
S₁[d,Pr . d] ) ) from FINSEQ_1:sch 5(A189);
A191: dom (Card Pr) = dom Pr by CARD_3:def 2
.= dom f2 by A27, A190, FINSEQ_1:def 3 ;
for d being Nat st d in dom (Card Pr) holds
(Card Pr) . d = f2 . d

proof

let d be Nat; :: thesis: ( d in dom (Card Pr) implies (Card Pr) . d = f2 . d )
assume A192: d in dom (Card Pr) ; :: thesis: (Card Pr) . d = f2 . d
then d in Seg ((p -' 1) div 2) by A27, A191, FINSEQ_1:def 3;
then consider m being Element of A such that
A193: m = d and
A194: Pr . d = { [m,y] where y is Element of B : z . (m,y) > 0 } by A190;
Pr . d = [:{m},(Seg (f2 . m)):]

proof

set L = [:{m},(Seg (f2 . m)):];
A195: [:{m},(Seg (f2 . m)):] c= Pr . d

proof

now :: thesis: not q mod p = 0

assume q mod p = 0 ; :: thesis: contradiction
then A196: p divides q by PEPIN:6;
then p <= q by NAT_D:7;
then p < q by A3, XXREAL_0:1;
hence contradiction by A6, A196, NAT_4:12; :: thesis: verum

end;

then A197: - (q div p) = ((- q) div p) + 1 by WSIERP_1:41;
2 divides (p -' 1) * q by A10, NAT_D:9;
then ((p -' 1) * q) mod 2 = 0 by PEPIN:6;
then ((p -' 1) * q) div 2 = ((p -' 1) * q) / 2 by REAL_3:4;
then A198: (((p -' 1) div 2) * q) div p = ((p - 1) * q) div (2 * p) by A7, A11, NAT_2:27
.= (((p * q) - q) div p) div 2 by PRE_FF:5
.= (q + ((- (q div p)) - 1)) div 2 by A197, NAT_D:61
.= ((2 * ((q -' 1) div 2)) + (- (q div p))) div 2 by A29, A40
.= ((q -' 1) div 2) + ((- (q div p)) div 2) by NAT_D:61 ;
A199: (((p -' 1) div 2) * q) div p <= (q -' 1) div 2

proof

per cases ( (q div p) mod 2 = 0 or (q div p) mod 2 <> 0 ) ;

suppose (q div p) mod 2 = 0 ; :: thesis: (((p -' 1) div 2) * q) div p <= (q -' 1) div 2

then (- (q div p)) div 2 = - ((q div p) div 2) by WSIERP_1:42
.= - (q div (2 * p)) by NAT_2:27 ;
then (((p -' 1) div 2) * q) div p = ((q -' 1) div 2) - (q div (2 * p)) by A198;
hence (((p -' 1) div 2) * q) div p <= (q -' 1) div 2 by XREAL_1:43; :: thesis: verum

end;

suppose (q div p) mod 2 <> 0 ; :: thesis: (((p -' 1) div 2) * q) div p <= (q -' 1) div 2

then - ((q div p) div 2) = ((- (q div p)) div 2) + 1 by WSIERP_1:41;
then (- (q div p)) div 2 = (- ((q div p) div 2)) - 1
.= (- (q div (2 * p))) - 1 by NAT_2:27 ;
then (((p -' 1) div 2) * q) div p = ((q -' 1) div 2) - ((q div (2 * p)) + 1) by A198;
hence (((p -' 1) div 2) * q) div p <= (q -' 1) div 2 by XREAL_1:43; :: thesis: verum

end;

end;

end;

m <= (p -' 1) div 2 by FINSEQ_1:1;
then m * q <= ((p -' 1) div 2) * q by XREAL_1:64;
then (m * q) div p <= (((p -' 1) div 2) * q) div p by NAT_2:24;
then A200: (m * q) div p <= (q -' 1) div 2 by A199, XXREAL_0:2;
m in Seg ((p -' 1) div 2) ;
then A201: m in dom f1 by A18, FINSEQ_1:def 3;
then A202: f2 . m = (f1 . m) div p by A27, A100
.= (m * q) div p by A13, A201 ;

now :: thesis: not (m * q) / p is integer

assume (m * q) / p is integer ; :: thesis: contradiction
then A203: p divides m * q by WSIERP_1:17;
A204: m <= (p -' 1) div 2 by FINSEQ_1:1;
0 + 1 <= m by FINSEQ_1:1;
then p <= m by A5, A203, NAT_D:7, WSIERP_1:30;
hence contradiction by A12, A204, XXREAL_0:2; :: thesis: verum

end;

then A205: [\((m * q) / p)/] < (m * q) / p by INT_1:26;
let l be object ; :: according to TARSKI:def 3 :: thesis: ( not l in [:{m},(Seg (f2 . m)):] or l in Pr . d )
assume l in [:{m},(Seg (f2 . m)):] ; :: thesis: l in Pr . d
then consider x, y being object such that
A206: x in {m} and
A207: y in Seg (f2 . m) and
A208: l = [x,y] by ZFMISC_1:def 2;
reconsider y = y as Element of NAT by A207;
A209: 1 <= y by A207, FINSEQ_1:1;
y <= f2 . m by A207, FINSEQ_1:1;
then y <= (q -' 1) div 2 by A200, A202, XXREAL_0:2;
then reconsider y = y as Element of B by A209, FINSEQ_1:1;
y <= [\((m * q) / p)/] by A207, A202, FINSEQ_1:1;
then y < (m * q) / p by A205, XXREAL_0:2;
then y * p < ((m * q) / p) * p by XREAL_1:68;
then y * p < m * q by XCMPLX_1:87;
then y / q < m / p by XREAL_1:106;
then (m / p) - (y / q) > 0 by XREAL_1:50;
then z . (m,y) > 0 by A188;
then [m,y] in Pr . d by A194;
hence l in Pr . d by A206, A208, TARSKI:def 1; :: thesis: verum

end;

Pr . d c= [:{m},(Seg (f2 . m)):]

proof

let l be object ; :: according to TARSKI:def 3 :: thesis: ( not l in Pr . d or l in [:{m},(Seg (f2 . m)):] )
A210: m in {m} by TARSKI:def 1;
m in Seg ((p -' 1) div 2) ;
then A211: m in dom f1 by A18, FINSEQ_1:def 3;
assume l in Pr . d ; :: thesis: l in [:{m},(Seg (f2 . m)):]
then consider y1 being Element of B such that
A212: l = [m,y1] and
A213: z . (m,y1) > 0 by A194;
(m / p) - (y1 / q) > 0 by A188, A213;
then ((m / p) - (y1 / q)) + (y1 / q) > 0 + (y1 / q) by XREAL_1:6;
then (m / p) * q > (y1 / q) * q by XREAL_1:68;
then (m * q) / p > y1 by XCMPLX_1:87;
then (m * q) div p >= y1 by INT_1:54;
then (f1 . m) div p >= y1 by A13, A211;
then A214: y1 <= f2 . m by A27, A100, A211;
y1 >= 1 by FINSEQ_1:1;
then y1 in Seg (f2 . m) by A214, FINSEQ_1:1;
hence l in [:{m},(Seg (f2 . m)):] by A212, A210, ZFMISC_1:def 2; :: thesis: verum

end;

hence Pr . d = [:{m},(Seg (f2 . m)):] by A195, XBOOLE_0:def 10; :: thesis: verum

end;

then card (Pr . d) = card [:(Seg (f2 . m)),{m}:] by CARD_2:4
.= card (Seg (f2 . m)) by CARD_1:69 ;
then A215: card (Pr . d) = card (f2 . d) by A193, FINSEQ_1:55
.= f2 . d ;
d in dom Pr by A192, CARD_3:def 2;
hence (Card Pr) . d = f2 . d by A215, CARD_3:def 2; :: thesis: verum

end;

then A216: Card Pr = f2 by A191;
defpred S₂[ set , set ] means ex y being Element of B st
( $1 = y & $2 = { [x,y] where x is Element of A : z . (x,y) < 0 } );
A217: for d being Nat st d in Seg ((q -' 1) div 2) holds
ex x1 being Element of bool (dom z) st S₂[d,x1]

proof

let d be Nat; :: thesis: ( d in Seg ((q -' 1) div 2) implies ex x1 being Element of bool (dom z) st S₂[d,x1] )
assume d in Seg ((q -' 1) div 2) ; :: thesis: ex x1 being Element of bool (dom z) st S₂[d,x1]
then reconsider d = d as Element of B ;
take x1 = { [x,d] where x is Element of A : z . (x,d) < 0 } ; :: thesis: ( x1 is Element of bool (dom z) & S₂[d,x1] )
x1 c= dom z

proof

let l be object ; :: according to TARSKI:def 3 :: thesis: ( not l in x1 or l in dom z )
assume l in x1 ; :: thesis: l in dom z
then ex xx being Element of A st
( [xx,d] = l & z . (xx,d) < 0 ) ;
then l in [:A,B:] ;
hence l in dom z by FUNCT_2:def 1; :: thesis: verum

end;

hence ( x1 is Element of bool (dom z) & S₂[d,x1] ) ; :: thesis: verum

end;

consider Pk being FinSequence of bool (dom z) such that
A218: ( dom Pk = Seg ((q -' 1) div 2) & ( for d being Nat st d in Seg ((q -' 1) div 2) holds
S₂[d,Pk . d] ) ) from FINSEQ_1:sch 5(A217);
A219: dom (Card Pk) = Seg (len g2) by A33, A218, CARD_3:def 2
.= dom g2 by FINSEQ_1:def 3 ;
A220: for d being Nat st d in dom (Card Pk) holds
(Card Pk) . d = g2 . d

proof

let d be Nat; :: thesis: ( d in dom (Card Pk) implies (Card Pk) . d = g2 . d )
assume A221: d in dom (Card Pk) ; :: thesis: (Card Pk) . d = g2 . d
then d in Seg ((q -' 1) div 2) by A33, A219, FINSEQ_1:def 3;
then consider n being Element of B such that
A222: n = d and
A223: Pk . d = { [x,n] where x is Element of A : z . (x,n) < 0 } by A218;
Pk . d = [:(Seg (g2 . n)),{n}:]

proof

set L = [:(Seg (g2 . n)),{n}:];
A224: [:(Seg (g2 . n)),{n}:] c= Pk . d

proof

now :: thesis: not p mod q = 0

assume p mod q = 0 ; :: thesis: contradiction
then A225: q divides p by PEPIN:6;
then q <= p by NAT_D:7;
then q < p by A3, XXREAL_0:1;
hence contradiction by A28, A225, NAT_4:12; :: thesis: verum

end;

then A226: - (p div q) = ((- p) div q) + 1 by WSIERP_1:41;
2 divides (q -' 1) * p by A39, NAT_D:9;
then ((q -' 1) * p) mod 2 = 0 by PEPIN:6;
then ((q -' 1) * p) div 2 = ((q -' 1) * p) / 2 by REAL_3:4;
then A227: (((q -' 1) div 2) * p) div q = ((q - 1) * p) div (2 * q) by A29, A40, NAT_2:27
.= (((q * p) - p) div q) div 2 by PRE_FF:5
.= (p + ((- (p div q)) - 1)) div 2 by A226, NAT_D:61
.= ((2 * ((p -' 1) div 2)) - (p div q)) div 2 by A7, A11
.= ((p -' 1) div 2) + ((- (p div q)) div 2) by NAT_D:61 ;
A228: (((q -' 1) div 2) * p) div q <= (p -' 1) div 2

proof

per cases ( (p div q) mod 2 = 0 or (p div q) mod 2 <> 0 ) ;

suppose (p div q) mod 2 = 0 ; :: thesis: (((q -' 1) div 2) * p) div q <= (p -' 1) div 2

then (- (p div q)) div 2 = - ((p div q) div 2) by WSIERP_1:42
.= - (p div (2 * q)) by NAT_2:27 ;
then (((q -' 1) div 2) * p) div q = ((p -' 1) div 2) - (p div (2 * q)) by A227;
hence (((q -' 1) div 2) * p) div q <= (p -' 1) div 2 by XREAL_1:43; :: thesis: verum

end;

suppose (p div q) mod 2 <> 0 ; :: thesis: (((q -' 1) div 2) * p) div q <= (p -' 1) div 2

then - ((p div q) div 2) = ((- (p div q)) div 2) + 1 by WSIERP_1:41;
then (- (p div q)) div 2 = (- ((p div q) div 2)) - 1
.= (- (p div (2 * q))) - 1 by NAT_2:27 ;
then (((q -' 1) div 2) * p) div q = ((p -' 1) div 2) - ((p div (2 * q)) + 1) by A227;
hence (((q -' 1) div 2) * p) div q <= (p -' 1) div 2 by XREAL_1:43; :: thesis: verum

end;

end;

end;

n in Seg ((q -' 1) div 2) ;
then A229: n in dom g1 by A23, FINSEQ_1:def 3;
then A230: g2 . n = (g1 . n) div q by A33, A34
.= (n * p) div q by A19, A229 ;
let l be object ; :: according to TARSKI:def 3 :: thesis: ( not l in [:(Seg (g2 . n)),{n}:] or l in Pk . d )
assume l in [:(Seg (g2 . n)),{n}:] ; :: thesis: l in Pk . d
then consider x, y being object such that
A231: x in Seg (g2 . n) and
A232: y in {n} and
A233: l = [x,y] by ZFMISC_1:def 2;
reconsider x = x as Element of NAT by A231;
A234: x <= g2 . n by A231, FINSEQ_1:1;
n <= (q -' 1) div 2 by FINSEQ_1:1;
then n * p <= ((q -' 1) div 2) * p by XREAL_1:64;
then (n * p) div q <= (((q -' 1) div 2) * p) div q by NAT_2:24;
then (n * p) div q <= (p -' 1) div 2 by A228, XXREAL_0:2;
then A235: x <= (p -' 1) div 2 by A230, A234, XXREAL_0:2;
1 <= x by A231, FINSEQ_1:1;
then reconsider x = x as Element of A by A235, FINSEQ_1:1;

now :: thesis: not (n * p) / q is integer

assume (n * p) / q is integer ; :: thesis: contradiction
then A236: q divides n * p by WSIERP_1:17;
A237: n <= (q -' 1) div 2 by FINSEQ_1:1;
0 + 1 <= n by FINSEQ_1:1;
then q <= n by A5, A236, NAT_D:7, WSIERP_1:30;
hence contradiction by A41, A237, XXREAL_0:2; :: thesis: verum

end;

then [\((n * p) / q)/] < (n * p) / q by INT_1:26;
then x < (n * p) / q by A230, A234, XXREAL_0:2;
then x * q < ((n * p) / q) * q by XREAL_1:68;
then x * q < n * p by XCMPLX_1:87;
then (x / p) - (n / q) < 0 by XREAL_1:49, XREAL_1:106;
then z . (x,n) < 0 by A188;
then [x,n] in Pk . d by A223;
hence l in Pk . d by A232, A233, TARSKI:def 1; :: thesis: verum

end;

Pk . d c= [:(Seg (g2 . n)),{n}:]

proof

let l be object ; :: according to TARSKI:def 3 :: thesis: ( not l in Pk . d or l in [:(Seg (g2 . n)),{n}:] )
A238: n in {n} by TARSKI:def 1;
n in Seg ((q -' 1) div 2) ;
then A239: n in dom g1 by A23, FINSEQ_1:def 3;
assume l in Pk . d ; :: thesis: l in [:(Seg (g2 . n)),{n}:]
then consider x being Element of A such that
A240: l = [x,n] and
A241: z . (x,n) < 0 by A223;
(x / p) - (n / q) < 0 by A188, A241;
then ((x / p) - (n / q)) + (n / q) < 0 + (n / q) by XREAL_1:6;
then (x / p) * p < (n / q) * p by XREAL_1:68;
then x < (n * p) / q by XCMPLX_1:87;
then x <= (n * p) div q by INT_1:54;
then (g1 . n) div q >= x by A19, A239;
then A242: x <= g2 . n by A33, A34, A239;
x >= 1 by FINSEQ_1:1;
then x in Seg (g2 . n) by A242, FINSEQ_1:1;
hence l in [:(Seg (g2 . n)),{n}:] by A240, A238, ZFMISC_1:def 2; :: thesis: verum

end;

hence Pk . d = [:(Seg (g2 . n)),{n}:] by A224, XBOOLE_0:def 10; :: thesis: verum

end;

then card (Pk . d) = card (Seg (g2 . n)) by CARD_1:69;
then A243: card (Pk . d) = card (g2 . d) by A222, FINSEQ_1:55
.= g2 . d ;
d in dom Pk by A221, CARD_3:def 2;
hence (Card Pk) . d = g2 . d by A243, CARD_3:def 2; :: thesis: verum

end;

reconsider U1 = union (rng Pr), U2 = union (rng Pk) as finite Subset of (dom z) by PROB_3:48;
dom z c= U1 \/ U2

proof

let l be object ; :: according to TARSKI:def 3 :: thesis: ( not l in dom z or l in U1 \/ U2 )
assume l in dom z ; :: thesis: l in U1 \/ U2
then consider x, y being object such that
A244: x in A and
A245: y in B and
A246: l = [x,y] by ZFMISC_1:def 2;
reconsider y = y as Element of B by A245;
reconsider x = x as Element of A by A244;
A247: z . (x,y) <> 0

proof

assume z . (x,y) = 0 ; :: thesis: contradiction
then (x / p) - (y / q) = 0 by A188;
then x * q = y * p by XCMPLX_1:95;
then A248: p divides x * q ;
A249: x <= (p -' 1) div 2 by FINSEQ_1:1;
x >= 0 + 1 by FINSEQ_1:1;
then p <= x by A5, A248, NAT_D:7, WSIERP_1:30;
hence contradiction by A12, A249, XXREAL_0:2; :: thesis: verum

end;

per cases ( z . (x,y) > 0 or z . (x,y) < 0 ) by A247;

suppose A250: z . (x,y) > 0 ; :: thesis: l in U1 \/ U2

S₁[x,Pr . x] by A190;
then l in Pr . x by A246, A250;
then l in Union Pr by A190, PROB_3:49;
hence l in U1 \/ U2 by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A251: z . (x,y) < 0 ; :: thesis: l in U1 \/ U2

S₂[y,Pk . y] by A218;
then l in Pk . y by A246, A251;
then l in Union Pk by A218, PROB_3:49;
hence l in U1 \/ U2 by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

then A252: U1 \/ U2 = dom z by XBOOLE_0:def 10;
A253: U1 misses U2

proof

assume U1 meets U2 ; :: thesis: contradiction
then consider l being object such that
A254: l in U1 and
A255: l in U2 by XBOOLE_0:3;
l in Union Pk by A255;
then consider k2 being Nat such that
A256: k2 in dom Pk and
A257: l in Pk . k2 by PROB_3:49;
l in Union Pr by A254;
then consider k1 being Nat such that
A258: k1 in dom Pr and
A259: l in Pr . k1 by PROB_3:49;
reconsider k1 = k1, k2 = k2 as Element of NAT by ORDINAL1:def 12;
consider n1 being Element of B such that
n1 = k2 and
A260: Pk . k2 = { [x,n1] where x is Element of A : z . (x,n1) < 0 } by A218, A256;
consider n2 being Element of A such that
A261: l = [n2,n1] and
A262: z . (n2,n1) < 0 by A257, A260;
consider m1 being Element of A such that
m1 = k1 and
A263: Pr . k1 = { [m1,y] where y is Element of B : z . (m1,y) > 0 } by A190, A258;
A264: ex m2 being Element of B st
( l = [m1,m2] & z . (m1,m2) > 0 ) by A259, A263;
then m1 = n2 by A261, XTUPLE_0:1;
hence contradiction by A264, A261, A262, XTUPLE_0:1; :: thesis: verum

end;

A265: for d, e being Nat st d in dom Pk & e in dom Pk & d <> e holds
Pk . d misses Pk . e

proof

let d, e be Nat; :: thesis: ( d in dom Pk & e in dom Pk & d <> e implies Pk . d misses Pk . e )
assume that
A266: d in dom Pk and
A267: e in dom Pk and
A268: d <> e ; :: thesis: Pk . d misses Pk . e
consider y2 being Element of B such that
A269: y2 = e and
A270: Pk . e = { [x,y2] where x is Element of A : z . (x,y2) < 0 } by A218, A267;
consider y1 being Element of B such that
A271: y1 = d and
A272: Pk . d = { [x,y1] where x is Element of A : z . (x,y1) < 0 } by A218, A266;

now :: thesis: Pk . d misses Pk . e

assume not Pk . d misses Pk . e ; :: thesis: contradiction
then consider l being object such that
A273: l in Pk . d and
A274: l in Pk . e by XBOOLE_0:3;
A275: ex x2 being Element of A st
( l = [x2,y2] & z . (x2,y2) < 0 ) by A270, A274;
ex x1 being Element of A st
( l = [x1,y1] & z . (x1,y1) < 0 ) by A272, A273;
hence contradiction by A268, A271, A269, A275, XTUPLE_0:1; :: thesis: verum

end;

hence Pk . d misses Pk . e ; :: thesis: verum

end;

A276: card (union (rng Pk)) = Sum (Card Pk) by A265, Th48;
A277: for d, e being Nat st d in dom Pr & e in dom Pr & d <> e holds
Pr . d misses Pr . e

proof

let d, e be Nat; :: thesis: ( d in dom Pr & e in dom Pr & d <> e implies Pr . d misses Pr . e )
assume that
A278: d in dom Pr and
A279: e in dom Pr and
A280: d <> e ; :: thesis: Pr . d misses Pr . e
consider x2 being Element of A such that
A281: x2 = e and
A282: Pr . e = { [x2,y] where y is Element of B : z . (x2,y) > 0 } by A190, A279;
consider x1 being Element of A such that
A283: x1 = d and
A284: Pr . d = { [x1,y] where y is Element of B : z . (x1,y) > 0 } by A190, A278;

now :: thesis: Pr . d misses Pr . e

assume not Pr . d misses Pr . e ; :: thesis: contradiction
then consider l being object such that
A285: l in Pr . d and
A286: l in Pr . e by XBOOLE_0:3;
A287: ex y2 being Element of B st
( l = [x2,y2] & z . (x2,y2) > 0 ) by A282, A286;
ex y1 being Element of B st
( l = [x1,y1] & z . (x1,y1) > 0 ) by A284, A285;
hence contradiction by A280, A283, A281, A287, XTUPLE_0:1; :: thesis: verum

end;

hence Pr . d misses Pr . e ; :: thesis: verum

end;

card (union (rng Pr)) = Sum (Card Pr) by A277, Th48;
then card (U1 \/ U2) = (Sum (Card Pr)) + (Sum (Card Pk)) by A276, A253, CARD_2:40;
then (Sum (Card Pr)) + (Sum (Card Pk)) = card [:A,B:] by A252, FUNCT_2:def 1
.= (card A) * (card B) by CARD_2:46
.= ((p -' 1) div 2) * (card B) by FINSEQ_1:57
.= ((p -' 1) div 2) * ((q -' 1) div 2) by FINSEQ_1:57 ;
hence (Sum f2) + (Sum g2) = ((p -' 1) div 2) * ((q -' 1) div 2) by A216, A219, A220, FINSEQ_1:13; :: thesis: verum

end;

dom (p * f2) = dom f2 by VALUED_1:def 5;
then A288: len (p * f2) = (p -' 1) div 2 by A27, FINSEQ_3:29;
p * f2 is Element of NAT * by FINSEQ_1:def 11;
then p * f2 in ((p -' 1) div 2) -tuples_on NAT by A288;
then A289: p * f2 is Element of ((p -' 1) div 2) -tuples_on REAL by FINSEQ_2:109, NUMBERS:19;
A290: (p -' 1) div 2 = ((p -' 1) + 1) div 2 by A9, NAT_2:26
.= p div 2 by A6, XREAL_1:235 ;
reconsider X = { k where k is Element of NAT : ( k in rng (Sgm (rng f3)) & k > p / 2 ) } as finite Subset of NAT by A184, XBOOLE_1:1;
set m = card X;
reconsider Y = (rng (Sgm (rng f3))) \ X as finite Subset of NAT ;
A291: f3 is Element of NAT * by FINSEQ_1:def 11;
len f3 = (p -' 1) div 2 by A17, A96, CARD_1:def 7;
then f3 in ((p -' 1) div 2) -tuples_on NAT by A291;
then A292: f3 is Element of ((p -' 1) div 2) -tuples_on REAL by FINSEQ_2:109, NUMBERS:19;
A293: rng f3 c= Seg n1 by A99, A108, XBOOLE_1:73;
then rng f3 is included_in_Seg by FINSEQ_1:def 13;
then A294: rng (Sgm (rng f3)) = rng f3 by FINSEQ_1:def 14;
then X c= Seg n1 by A293, A184;
then a295: X is included_in_Seg by FINSEQ_1:def 13;
A296: dom ((p * f2) + f3) = (dom (p * f2)) /\ (dom f3) by VALUED_1:def 1
.= (dom f2) /\ (dom f3) by VALUED_1:def 5
.= dom f1 by A97, A100 ;
for d being Nat st d in dom f1 holds
f1 . d = ((p * f2) + f3) . d

proof

let d be Nat; :: thesis: ( d in dom f1 implies f1 . d = ((p * f2) + f3) . d )
assume A297: d in dom f1 ; :: thesis: f1 . d = ((p * f2) + f3) . d
then A298: d in dom (p * f2) by A100, VALUED_1:def 5;
((p * f2) + f3) . d = ((p * f2) . d) + (f3 . d) by A296, A297, VALUED_1:def 1;
hence ((p * f2) + f3) . d = (p * (f2 . d)) + (f3 . d) by A298, VALUED_1:def 5
.= f1 . d by A101, A297 ;
:: thesis: verum

end;

then f1 = (p * f2) + f3 by A296;
then A299: Sum f1 = (Sum (p * f2)) + (Sum f3) by A289, A292, RVSUM_1:89
.= (p * (Sum f2)) + (Sum f3) by RVSUM_1:87 ;
(rng (Sgm (rng f3))) \ X c= rng (Sgm (rng f3)) by XBOOLE_1:36;
then Y c= Seg n1 by A293, A294;
then a301: Y is included_in_Seg by FINSEQ_1:def 13;
A302: len f3 = card (rng (Sgm (rng f3))) by A127, A294, FINSEQ_4:62;
then reconsider n = ((p -' 1) div 2) - (card X) as Element of NAT by A18, A96, A184, NAT_1:21, NAT_1:43;
A303: Sgm (rng f3) = ((Sgm (rng f3)) | n) ^ ((Sgm (rng f3)) /^ n) by RFINSEQ:8;
then A304: (Sgm (rng f3)) /^ n is one-to-one by A109, FINSEQ_3:91;
A306: Sum (Sgm (rng f3)) = Sum f3 by A127, A294, A109, RFINSEQ:9, RFINSEQ:26;
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
A307: k in Y and
A308: l in X ; :: thesis: k < l
A309: not k in X by A307, XBOOLE_0:def 5;
A310: ex l1 being Element of NAT st
( l1 = l & l1 in rng (Sgm (rng f3)) & l1 > p / 2 ) by A308;
k in rng (Sgm (rng f3)) by A307, XBOOLE_0:def 5;
then k <= p / 2 by A309;
hence k < l by A310, XXREAL_0:2; :: thesis: verum

end;

then Sgm (Y \/ X) = (Sgm Y) ^ (Sgm X) by a295, a301, FINSEQ_3:42;
then Sgm ((rng (Sgm (rng f3))) \/ X) = (Sgm Y) ^ (Sgm X) by XBOOLE_1:39;
then A311: Sgm (rng f3) = (Sgm Y) ^ (Sgm X) by A294, A184, XBOOLE_1:12;
then Sum (Sgm (rng f3)) = (Sum (Sgm Y)) + (Sum (Sgm X)) by RVSUM_1:75;
then A312: q * (Sum (idseq ((p -' 1) div 2))) = ((p * (Sum f2)) + (Sum (Sgm Y))) + (Sum (Sgm X)) by A299, A306, RVSUM_1:87;
A313: len (Sgm Y) = card Y by a301, FINSEQ_3:39
.= ((p -' 1) div 2) - (card X) by A18, A96, A184, A302, CARD_2:44 ;
then A314: (Sgm (rng f3)) /^ n = Sgm X by A311, FINSEQ_5:37;
A315: (Sgm (rng f3)) | n = Sgm Y by A311, A313, FINSEQ_3:113, FINSEQ_6:10;
A316: (Sgm (rng f3)) | n is one-to-one by A109, A303, FINSEQ_3:91;
Lege (q,p) = (- 1) |^ (Sum f2)

proof

set f5 = ((card X) |-> p) - ((Sgm (rng f3)) /^ n);
set f6 = ((Sgm (rng f3)) | n) ^ (((card X) |-> p) - ((Sgm (rng f3)) /^ n));
A317: (Sgm (rng f3)) /^ n is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;
A318: len ((Sgm (rng f3)) | n) = n by A128, FINSEQ_1:59, XREAL_1:43;
A319: len ((Sgm (rng f3)) /^ n) = (len (Sgm (rng f3))) -' n by RFINSEQ:29
.= (len (Sgm (rng f3))) - n by A128, XREAL_1:43, XREAL_1:233
.= card X by A128 ;
A320: dom (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) = (dom ((card X) |-> p)) /\ (dom ((Sgm (rng f3)) /^ n)) by VALUED_1:12
.= (Seg (len ((card X) |-> p))) /\ (dom ((Sgm (rng f3)) /^ n)) by FINSEQ_1:def 3
.= (dom ((Sgm (rng f3)) /^ n)) /\ (dom ((Sgm (rng f3)) /^ n)) by FINSEQ_1:def 3, A319, CARD_1:def 7
.= dom ((Sgm (rng f3)) /^ n) ;
then A321: len (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) = len ((Sgm (rng f3)) /^ n) by FINSEQ_3:29;
A322: for d being Nat st d in dom (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) holds
(((card X) |-> p) - ((Sgm (rng f3)) /^ n)) . d = p - (((Sgm (rng f3)) /^ n) . d)

proof

let d be Nat; :: thesis: ( d in dom (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) implies (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) . d = p - (((Sgm (rng f3)) /^ n) . d) )
assume A323: d in dom (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) ; :: thesis: (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) . d = p - (((Sgm (rng f3)) /^ n) . d)
then d in Seg (card X) by A319, A320, FINSEQ_1:def 3;
then ((card X) |-> p) . d = p by FINSEQ_2:57;
hence (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) . d = p - (((Sgm (rng f3)) /^ n) . d) by A323, VALUED_1:13; :: thesis: verum

end;

A324: for d being Nat st d in dom (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) holds
( (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) . d > 0 & (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) . d <= (p -' 1) div 2 )

proof

let d be Nat; :: thesis: ( d in dom (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) implies ( (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) . d > 0 & (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) . d <= (p -' 1) div 2 ) )
reconsider w = (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) . d as Element of INT by INT_1:def 2;
assume A325: d in dom (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) ; :: thesis: ( (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) . d > 0 & (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) . d <= (p -' 1) div 2 )
then (Sgm X) . d in rng (Sgm X) by A314, A320, FUNCT_1:3;
then (Sgm X) . d in X by a295, FINSEQ_1:def 14;
then A326: ex ll being Element of NAT st
( ll = (Sgm X) . d & ll in rng f3 & ll > p / 2 ) by A294;
then consider e being Nat such that
A327: e in dom f3 and
A328: f3 . e = ((Sgm (rng f3)) /^ n) . d by A314, FINSEQ_2:10;
((Sgm (rng f3)) /^ n) . d = (f1 . e) mod p by A97, A327, A328, EULER_2:def 2;
then A329: ((Sgm (rng f3)) /^ n) . d < p by NAT_D:1;
A330: (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) . d = p - (((Sgm (rng f3)) /^ n) . d) by A322, A325;
then w < p - (p / 2) by A314, A326, XREAL_1:10;
hence ( (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) . d > 0 & (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) . d <= (p -' 1) div 2 ) by A290, A330, A329, INT_1:54, XREAL_1:50; :: thesis: verum

end;

for d being Nat st d in dom (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) holds
(((card X) |-> p) - ((Sgm (rng f3)) /^ n)) . d in NAT

proof

let d be Nat; :: thesis: ( d in dom (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) implies (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) . d in NAT )
assume A332: d in dom (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) ; :: thesis: (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) . d in NAT
(((card X) |-> p) - ((Sgm (rng f3)) /^ n)) . d > 0 by A332, A324;
hence (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) . d in NAT by INT_1:3; :: thesis: verum

end;

then reconsider f5 = ((card X) |-> p) - ((Sgm (rng f3)) /^ n) as FinSequence of NAT by FINSEQ_2:12;
f5 is FinSequence of NAT ;
then reconsider f6 = ((Sgm (rng f3)) | n) ^ (((card X) |-> p) - ((Sgm (rng f3)) /^ n)) as FinSequence of NAT by FINSEQ_1:75;
A334: n <= len (Sgm (rng f3)) by A128, XREAL_1:43;
A335: rng ((Sgm (rng f3)) | n) misses rng f5

proof

assume not rng ((Sgm (rng f3)) | n) misses rng f5 ; :: thesis: contradiction
then consider x being object such that
A336: x in rng ((Sgm (rng f3)) | n) and
A337: x in rng f5 by XBOOLE_0:3;
consider e being Nat such that
A338: e in dom f5 and
A339: f5 . e = x by A337, FINSEQ_2:10;
x = p - (((Sgm (rng f3)) /^ n) . e) by A322, A338, A339;
then A340: x = p - ((Sgm (rng f3)) . (e + n)) by A334, A320, A338, RFINSEQ:def 1;
e + n in dom (Sgm (rng f3)) by A320, A338, FINSEQ_5:26;
then consider e1 being Nat such that
A341: e1 in dom f3 and
A342: f3 . e1 = (Sgm (rng f3)) . (e + n) by A294, FINSEQ_2:10, FUNCT_1:3;
A343: e1 <= (p -' 1) div 2 by A18, A96, A341, FINSEQ_3:25;
rng ((Sgm (rng f3)) | n) c= rng (Sgm (rng f3)) by FINSEQ_5:19;
then consider d1 being Nat such that
A344: d1 in dom f3 and
A345: f3 . d1 = x by A294, A336, FINSEQ_2:10;
d1 <= (p -' 1) div 2 by A18, A96, A344, FINSEQ_3:25;
then d1 + e1 <= ((p -' 1) div 2) + ((p -' 1) div 2) by A343, XREAL_1:7;
then A346: d1 + e1 < p by A7, A11, XREAL_1:146, XXREAL_0:2;
x = (f1 . d1) mod p by A97, A344, A345, EULER_2:def 2;
then ((f1 . d1) mod p) + ((Sgm (rng f3)) . (e + n)) = p by A340;
then ((f1 . d1) mod p) + ((f1 . e1) mod p) = p by A97, A341, A342, EULER_2:def 2;
then (((f1 . d1) mod p) + ((f1 . e1) mod p)) mod p = 0 by NAT_D:25;
then ((f1 . d1) + (f1 . e1)) mod p = 0 by NAT_D:66;
then p divides (f1 . d1) + (f1 . e1) by PEPIN:6;
then p divides (d1 * q) + (f1 . e1) by A13, A97, A344;
then p divides (d1 * q) + (e1 * q) by A13, A97, A341;
then A347: p divides (d1 + e1) * q ;
d1 >= 1 by A344, FINSEQ_3:25;
hence contradiction by A4, A347, A346, NAT_D:7, PEPIN:3; :: thesis: verum

end;

for d, e being Nat st 1 <= d & d < e & e <= len f5 holds
f5 . d <> f5 . e

proof

let d, e be Nat; :: thesis: ( 1 <= d & d < e & e <= len f5 implies f5 . d <> f5 . e )
assume that
A348: 1 <= d and
A349: d < e and
A350: e <= len f5 ; :: thesis: f5 . d <> f5 . e
1 <= e by A348, A349, XXREAL_0:2;
then A351: e in dom f5 by A350, FINSEQ_3:25;
then A352: f5 . e = p - (((Sgm (rng f3)) /^ n) . e) by A322;
d < len f5 by A349, A350, XXREAL_0:2;
then A353: d in dom f5 by A348, FINSEQ_3:25;
then f5 . d = p - (((Sgm (rng f3)) /^ n) . d) by A322;
hence f5 . d <> f5 . e by A304, A320, A349, A353, A351, A352; :: thesis: verum

end;

then len f5 = card (rng f5) by GRAPH_5:7;
then f5 is one-to-one by FINSEQ_4:62;
then A354: f6 is one-to-one by A316, A335, FINSEQ_3:91;
A355: for d being Nat st d in dom f6 holds
( f6 . d > 0 & f6 . d <= (p -' 1) div 2 )

proof

let d be Nat; :: thesis: ( d in dom f6 implies ( f6 . d > 0 & f6 . d <= (p -' 1) div 2 ) )
assume A356: d in dom f6 ; :: thesis: ( f6 . d > 0 & f6 . d <= (p -' 1) div 2 )

per cases ( d in dom ((Sgm (rng f3)) | n) or ex l being Nat st
( l in dom f5 & d = (len ((Sgm (rng f3)) | n)) + l ) ) by A356, FINSEQ_1:25;

suppose A357: d in dom ((Sgm (rng f3)) | n) ; :: thesis: ( f6 . d > 0 & f6 . d <= (p -' 1) div 2 )

then ((Sgm (rng f3)) | n) . d in rng (Sgm Y) by A315, FUNCT_1:3;
then A358: ((Sgm (rng f3)) | n) . d in Y by a301, FINSEQ_1:def 14;
then A359: ((Sgm (rng f3)) | n) . d in rng (Sgm (rng f3)) by XBOOLE_0:def 5;
not ((Sgm (rng f3)) | n) . d in X by A358, XBOOLE_0:def 5;
then ((Sgm (rng f3)) | n) . d <= p / 2 by A359;
then A360: ((Sgm (rng f3)) | n) . d <= (p -' 1) div 2 by A290, INT_1:54;
not ((Sgm (rng f3)) | n) . d in {0} by A108, A294, A359, XBOOLE_0:3;
then ((Sgm (rng f3)) | n) . d <> 0 by TARSKI:def 1;
hence ( f6 . d > 0 & f6 . d <= (p -' 1) div 2 ) by A357, A360, FINSEQ_1:def 7; :: thesis: verum

end;

suppose ex l being Nat st
( l in dom f5 & d = (len ((Sgm (rng f3)) | n)) + l ) ; :: thesis: ( f6 . d > 0 & f6 . d <= (p -' 1) div 2 )

then consider l being Element of NAT such that
A361: l in dom f5 and
A362: d = (len ((Sgm (rng f3)) | n)) + l ;
f6 . d = f5 . l by A361, A362, FINSEQ_1:def 7;
hence ( f6 . d > 0 & f6 . d <= (p -' 1) div 2 ) by A324, A361; :: thesis: verum

end;

end;

end;

len f6 = (len ((Sgm (rng f3)) | n)) + (len f5) by FINSEQ_1:22
.= (p -' 1) div 2 by A318, A319, A321 ;
then rng f6 = rng (idseq ((p -' 1) div 2)) by A354, A355, Th40;
then M = Sum f6 by A354, RFINSEQ:9, RFINSEQ:26
.= (Sum ((Sgm (rng f3)) | n)) + (Sum f5) by RVSUM_1:75
.= (Sum ((Sgm (rng f3)) | n)) + (((card X) * p) - (Sum ((Sgm (rng f3)) /^ n))) by A319, A317, Th47
.= ((Sum ((Sgm (rng f3)) | n)) + ((card X) * p)) - (Sum ((Sgm (rng f3)) /^ n)) ;
then (q - 1) * M = ((p * (Sum f2)) + (2 * (Sum (Sgm X)))) - ((card X) * p) by A312, A314, A315;
then A364: ((q -' 1) * M) mod 2 = (((p * (Sum f2)) - ((card X) * p)) + (2 * (Sum (Sgm X)))) mod 2 by A28, XREAL_1:233
.= ((p * (Sum f2)) - ((card X) * p)) mod 2 by NAT_D:61 ;
2 divides (q -' 1) * M by A39, NAT_D:9;
then ((q -' 1) * M) mod 2 = 0 by PEPIN:6;
then 2 divides p * ((Sum f2) - (card X)) by A364, Lm1;
then Sum f2, card X are_congruent_mod 2 by A183, INT_2:25;
then (Sum f2) mod 2 = (card X) mod 2 by NAT_D:64;
then (- 1) |^ (Sum f2) = (- 1) |^ (card X) by Th45;
hence Lege (q,p) = (- 1) |^ (Sum f2) by A1, A5, A294, Th41; :: thesis: verum

end;

hence (Lege (p,q)) * (Lege (q,p)) = (- 1) |^ (((p -' 1) div 2) * ((q -' 1) div 2)) by A131, A186, NEWTON:8; :: thesis: verum