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_relative_prime by A3, INT_2:47;
then A5: q gcd p = 1 by INT_2:def 4;
reconsider p = p, q = q as prime Element of NAT by ORDINAL1:def 13;
set p9 = (p -' 1) div 2;
A6: p > 1 by INT_2:def 5;
then A7: p -' 1 = p - 1 by XREAL_1:235;
then A8: p -' 1 > 0 by A6, XREAL_1:52;
not p is even 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) by NAT_D:3;
then (p -' 1) div 2 divides p -' 1 by NAT_D:def 3;
then (p -' 1) div 2 <= p -' 1 by A8, NAT_D:7;
then A12: (p -' 1) div 2 < p by A7, XREAL_1:148, 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 FINSEQ_1:def 18;
(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, FINSEQ_2:57; :: 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

proof

let d be Nat; :: thesis: ( d in dom (q * (idseq ((p -' 1) div 2))) implies (q * (idseq ((p -' 1) div 2))) . d in NAT )
assume d in dom (q * (idseq ((p -' 1) div 2))) ; :: thesis: (q * (idseq ((p -' 1) div 2))) . d in NAT
then (q * (idseq ((p -' 1) div 2))) . d = q * d by A13;
hence (q * (idseq ((p -' 1) div 2))) . d in NAT ; :: thesis: verum

end;

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:31;
then A18: len (q * (idseq ((p -' 1) div 2))) = (p -' 1) div 2 by FINSEQ_1:def 18;
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 FINSEQ_1:def 18;
(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, FINSEQ_2:57; :: 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

proof

let d be Nat; :: thesis: ( d in dom (p * (idseq ((q -' 1) div 2))) implies (p * (idseq ((q -' 1) div 2))) . d in NAT )
assume d in dom (p * (idseq ((q -' 1) div 2))) ; :: thesis: (p * (idseq ((q -' 1) div 2))) . d in NAT
then (p * (idseq ((q -' 1) div 2))) . d = p * d by A19;
hence (p * (idseq ((q -' 1) div 2))) . d in NAT ; :: thesis: verum

end;

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:31;
then A23: len (p * (idseq ((q -' 1) div 2))) = (q -' 1) div 2 by FINSEQ_1:def 18;
reconsider g1 = p * (idseq ((q -' 1) div 2)) as FinSequence of NAT by A22, FINSEQ_2:14;
set g3 = g1 mod q;
set g4 = Sgm (rng (g1 mod q));
A24: len (g1 mod q) = len g1 by EULER_2:def 1;
then A25: dom g1 = dom (g1 mod q) by FINSEQ_3:31;
set XX = { k where k is Element of NAT : ( k in rng (Sgm (rng (g1 mod q))) & k > q / 2 ) } ;
for x being set st x in { k where k is Element of NAT : ( k in rng (Sgm (rng (g1 mod q))) & k > q / 2 ) } holds
x in rng (Sgm (rng (g1 mod q)))

proof

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

end;

then A26: { k where k is Element of NAT : ( k in rng (Sgm (rng (g1 mod q))) & k > q / 2 ) } c= rng (Sgm (rng (g1 mod q))) by TARSKI:def 3;
reconsider f1 = q * (idseq ((p -' 1) div 2)) as FinSequence of NAT by A16, FINSEQ_2:14;
deffunc H₁( Nat) -> Element of NAT = (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 5;
then A29: q -' 1 = q - 1 by XREAL_1:235;
then A30: q -' 1 > 0 by A28, XREAL_1:52;
q >= 2 + 1 by A2, NAT_1:13;
then q - 1 >= 3 - 1 by XREAL_1:11;
then A31: (q -' 1) div 2 >= 1 by A29, NAT_2:15;
then len (g1 mod q) >= 1 by A23, EULER_2:def 1;
then g1 mod q <> {} ;
then rng (g1 mod q) is non empty finite Subset of NAT by FINSEQ_1:def 4;
then consider n2 being Element of NAT such that
A32: rng (g1 mod q) c= (Seg n2) \/ {0 } by HEYTING3:3;
deffunc H₂( Nat) -> Element of NAT = (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:14;
A34: dom g1 = dom g2 by A23, A33, FINSEQ_3:31;
A35: for d being Nat st d in dom g1 holds
g1 . d = ((g2 . d) * q) + ((g1 mod q) . d)

proof

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

end;

not q is even 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) by NAT_D:3;
then (q -' 1) div 2 divides q -' 1 by NAT_D:def 3;
then (q -' 1) div 2 <= q -' 1 by A30, NAT_D:7;
then A41: (q -' 1) div 2 < q by A29, XREAL_1:148, XXREAL_0:2;
not 0 in rng (g1 mod q)

proof

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

end;

then A47: {0 } misses rng (g1 mod q) by ZFMISC_1:56;
then A48: Sgm (rng (g1 mod q)) is one-to-one by A32, FINSEQ_3:99, XBOOLE_1:73;
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_relative_prime by A3, INT_2:47;
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

assume d <> e ; :: thesis: contradiction
then d - e <> 0 ;
then abs q <= abs (d - e) by A55, A50, INT_2:40, INT_4:6;
then A56: q <= abs (d - e) by ABSVALUE:def 1;
A57: e >= 1 by A52, FINSEQ_3:27;
A58: d >= 1 by A51, FINSEQ_3:27;
e <= (q -' 1) div 2 by A23, A52, FINSEQ_3:27;
then A59: d - e >= 1 - ((q -' 1) div 2) by A58, XREAL_1:15;
A60: ((q -' 1) div 2) - 1 < q by A41, XREAL_1:149;
d <= (q -' 1) div 2 by A23, A51, FINSEQ_3:27;
then d - e <= ((q -' 1) div 2) - 1 by A57, XREAL_1:15;
then A61: d - e < q by A60, XXREAL_0:2;
- (((q -' 1) div 2) - 1) > - q by A60, XREAL_1:26;
then d - e > - q by A59, XXREAL_0:2;
hence contradiction by A56, A61, SEQ_2:9; :: thesis: verum

end;

hence d = e ; :: thesis: verum

end;

for x, y being set st x in dom (g1 mod q) & y in dom (g1 mod q) & (g1 mod q) . x = (g1 mod q) . y holds
x = y

proof

let x, y be set ; :: thesis: ( x in dom (g1 mod q) & y in dom (g1 mod q) & (g1 mod q) . x = (g1 mod q) . y implies x = y )
assume that
A62: x in dom (g1 mod q) and
A63: y in dom (g1 mod q) and
A64: (g1 mod q) . x = (g1 mod q) . y ; :: thesis: x = y
reconsider x = x, y = y as Element of NAT by A62, A63;
A65: g1 . y = ((g2 . y) * q) + ((g1 mod q) . y) by A25, A35, A63;
g1 . x = ((g2 . x) * q) + ((g1 mod q) . 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) by INT_1:def 9;
hence x = y by A49, A25, A62, A63; :: thesis: verum

end;

then A66: g1 mod q is one-to-one by FUNCT_1:def 8;
then len (g1 mod q) = card (rng (g1 mod q)) by FINSEQ_4:77;
then A67: len (Sgm (rng (g1 mod q))) = (q -' 1) div 2 by A23, A24, A32, A47, FINSEQ_3:44, XBOOLE_1:73;
reconsider XX = { k where k is Element of NAT : ( k in rng (Sgm (rng (g1 mod q))) & k > q / 2 ) } as finite Subset of NAT by A26, XBOOLE_1:1;
set mm = card XX;
reconsider YY = (rng (Sgm (rng (g1 mod q)))) \ XX as finite Subset of NAT ;
A68: g1 mod q is Element of NAT * by FINSEQ_1:def 11;
len (g1 mod q) = (q -' 1) div 2 by A23, EULER_2:def 1;
then g1 mod q in ((q -' 1) div 2) -tuples_on NAT by A68;
then A69: g1 mod q is Element of ((q -' 1) div 2) -tuples_on REAL by FINSEQ_2:129;
for d being Nat st d in dom (idseq ((q -' 1) div 2)) holds
(idseq ((q -' 1) div 2)) . d in NAT by ORDINAL1:def 13;
then idseq ((q -' 1) div 2) is FinSequence of NAT by FINSEQ_2:14;
then reconsider N = Sum (idseq ((q -' 1) div 2)) as Element of NAT by Lm3;
A70: 2,q are_relative_prime by A2, EULER_1:3;
dom (q * g2) = dom g2 by VALUED_1:def 5;
then A71: len (q * g2) = (q -' 1) div 2 by A33, FINSEQ_3:31;
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:129;
A73: dom ((q * g2) + (g1 mod q)) = (dom (q * g2)) /\ (dom (g1 mod q)) by VALUED_1:def 1
.= (dom g2) /\ (dom (g1 mod q)) by VALUED_1:def 5
.= dom g1 by A25, A34 ;
for d being Nat st d in dom g1 holds
g1 . d = ((q * g2) + (g1 mod q)) . d

proof

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

end;

then g1 = (q * g2) + (g1 mod q) by A73, FINSEQ_1:17;
then A76: Sum g1 = (Sum (q * g2)) + (Sum (g1 mod q)) by A72, A69, RVSUM_1:119
.= (q * (Sum g2)) + (Sum (g1 mod q)) by RVSUM_1:117 ;
A77: rng (g1 mod q) c= Seg n2 by A32, A47, XBOOLE_1:73;
then A78: rng (Sgm (rng (g1 mod q))) = rng (g1 mod q) by FINSEQ_1:def 13;
then A79: XX c= Seg n2 by A77, A26, XBOOLE_1:1;
A80: len (g1 mod q) = card (rng (Sgm (rng (g1 mod q)))) by A66, A78, FINSEQ_4:77;
card XX <= card (rng (Sgm (rng (g1 mod q)))) by A26, NAT_1:44;
then card XX <= (q -' 1) div 2 by A23, A80, EULER_2:def 1;
then reconsider nn = ((q -' 1) div 2) - (card XX) as Element of NAT by NAT_1:21;
A81: Sgm (rng (g1 mod q)) = ((Sgm (rng (g1 mod q))) | nn) ^ ((Sgm (rng (g1 mod q))) /^ nn) by RFINSEQ:21;
then A82: (Sgm (rng (g1 mod q))) /^ nn is one-to-one by A48, FINSEQ_3:98;
A83: (q -' 1) div 2 = ((q -' 1) + 1) div 2 by A38, NAT_2:28
.= q div 2 by A28, XREAL_1:237 ;
Sgm (rng (g1 mod q)) is FinSequence of REAL by FINSEQ_2:27;
then A84: Sum (Sgm (rng (g1 mod q))) = Sum (g1 mod q) by A66, A78, A48, RFINSEQ:22, RFINSEQ:39;
A85: (rng (Sgm (rng (g1 mod q)))) \ XX c= rng (Sgm (rng (g1 mod q))) by XBOOLE_1:36;
then A86: YY c= Seg n2 by A77, A78, XBOOLE_1:1;
for k, l being Element of NAT st k in YY & l in XX holds
k < l

proof

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

end;

then Sgm (YY \/ XX) = (Sgm YY) ^ (Sgm XX) by A86, A79, FINSEQ_3:48;
then Sgm ((rng (Sgm (rng (g1 mod q)))) \/ XX) = (Sgm YY) ^ (Sgm XX) by XBOOLE_1:39;
then A91: Sgm (rng (g1 mod q)) = (Sgm YY) ^ (Sgm XX) by A78, A26, XBOOLE_1:12;
then Sum (Sgm (rng (g1 mod q))) = (Sum (Sgm YY)) + (Sum (Sgm XX)) by RVSUM_1:105;
then A92: p * (Sum (idseq ((q -' 1) div 2))) = ((q * (Sum g2)) + (Sum (Sgm YY))) + (Sum (Sgm XX)) by A76, A84, RVSUM_1:117;
A93: len (Sgm YY) = card YY by A77, A78, A85, FINSEQ_3:44, XBOOLE_1:1
.= ((q -' 1) div 2) - (card XX) by A23, A24, A26, A80, CARD_2:63 ;
then A94: (Sgm (rng (g1 mod q))) /^ nn = Sgm XX by A91, FINSEQ_5:40;
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:14;
set f3 = f1 mod p;
A95: len (f1 mod p) = len f1 by EULER_2:def 1;
then A96: dom f1 = dom (f1 mod p) by FINSEQ_3:31;
set f4 = Sgm (rng (f1 mod p));
p >= 2 + 1 by A1, NAT_1:13;
then A97: p - 1 >= 3 - 1 by XREAL_1:11;
then f1 mod p <> {} by A18, A7, A95, NAT_2:15;
then rng (f1 mod p) is non empty finite Subset of NAT by FINSEQ_1:def 4;
then consider n1 being Element of NAT such that
A98: rng (f1 mod p) c= (Seg n1) \/ {0 } by HEYTING3:3;
A99: dom f1 = dom f2 by A18, A27, FINSEQ_3:31;
A100: for d being Nat st d in dom f1 holds
f1 . d = ((f2 . d) * p) + ((f1 mod p) . d)

proof

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

end;

not 0 in rng (f1 mod p)

proof

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

end;

then A107: {0 } misses rng (f1 mod p) by ZFMISC_1:56;
then A108: Sgm (rng (f1 mod p)) is one-to-one by A98, FINSEQ_3:99, XBOOLE_1:73;
A109: for d, e being Nat st d in dom f1 & e in dom f1 & p divides (f1 . d) - (f1 . e) holds
d = e

proof

A110: q,p are_relative_prime by A3, INT_2:47;
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
A111: d in dom f1 and
A112: e in dom f1 and
A113: p divides (f1 . d) - (f1 . e) ; :: thesis: d = e
A114: f1 . e = q * e by A13, A112;
f1 . d = q * d by A13, A111;
then A115: p divides (d - e) * q by A113, A114;

now

assume d <> e ; :: thesis: contradiction
then d - e <> 0 ;
then abs p <= abs (d - e) by A115, A110, INT_2:40, INT_4:6;
then A116: p <= abs (d - e) by ABSVALUE:def 1;
A117: e >= 1 by A112, FINSEQ_3:27;
A118: d >= 1 by A111, FINSEQ_3:27;
e <= (p -' 1) div 2 by A18, A112, FINSEQ_3:27;
then A119: d - e >= 1 - ((p -' 1) div 2) by A118, XREAL_1:15;
A120: ((p -' 1) div 2) - 1 < p by A12, XREAL_1:149;
d <= (p -' 1) div 2 by A18, A111, FINSEQ_3:27;
then d - e <= ((p -' 1) div 2) - 1 by A117, XREAL_1:15;
then A121: d - e < p by A120, XXREAL_0:2;
- (((p -' 1) div 2) - 1) > - p by A120, XREAL_1:26;
then d - e > - p by A119, XXREAL_0:2;
hence contradiction by A116, A121, SEQ_2:9; :: thesis: verum

end;

hence d = e ; :: thesis: verum

end;

for x, y being set st x in dom (f1 mod p) & y in dom (f1 mod p) & (f1 mod p) . x = (f1 mod p) . y holds
x = y

proof

let x, y be set ; :: thesis: ( x in dom (f1 mod p) & y in dom (f1 mod p) & (f1 mod p) . x = (f1 mod p) . y implies x = y )
assume that
A122: x in dom (f1 mod p) and
A123: y in dom (f1 mod p) and
A124: (f1 mod p) . x = (f1 mod p) . y ; :: thesis: x = y
reconsider x = x, y = y as Element of NAT by A122, A123;
A125: f1 . y = ((f2 . y) * p) + ((f1 mod p) . y) by A96, A100, A123;
f1 . x = ((f2 . x) * p) + ((f1 mod p) . x) by A96, A100, A122;
then (f1 . x) - (f1 . y) = ((f2 . x) - (f2 . y)) * p by A124, A125;
then p divides (f1 . x) - (f1 . y) by INT_1:def 9;
hence x = y by A109, A96, A122, A123; :: thesis: verum

end;

then A126: f1 mod p is one-to-one by FUNCT_1:def 8;
then len (f1 mod p) = card (rng (f1 mod p)) by FINSEQ_4:77;
then A127: len (Sgm (rng (f1 mod p))) = (p -' 1) div 2 by A18, A95, A98, A107, FINSEQ_3:44, XBOOLE_1:73;
A128: (Sgm (rng (g1 mod q))) | nn = Sgm YY by A91, A93, FINSEQ_3:122, FINSEQ_6:12;
A129: (Sgm (rng (g1 mod q))) | nn is one-to-one by A48, A81, FINSEQ_3:98;
A130: Lege p,q = (- 1) |^ (Sum g2)

proof

set g5 = ((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn);
set g6 = ((Sgm (rng (g1 mod q))) | nn) ^ (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn));
A134: rng (idseq ((q -' 1) div 2)) = Seg ((q -' 1) div 2) by RELAT_1:71;
A135: (Sgm (rng (g1 mod q))) /^ nn is FinSequence of REAL by FINSEQ_2:27;
A136: len ((Sgm (rng (g1 mod q))) | nn) = nn by A67, FINSEQ_1:80, XREAL_1:45;
A137: len ((Sgm (rng (g1 mod q))) /^ nn) = (len (Sgm (rng (g1 mod q)))) -' nn by RFINSEQ:42
.= (len (Sgm (rng (g1 mod q)))) - nn by A67, XREAL_1:45, XREAL_1:235
.= card XX by A67 ;
A138: dom (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) = (dom ((card XX) |-> q)) /\ (dom ((Sgm (rng (g1 mod q))) /^ nn)) by VALUED_1:12
.= (Seg (len ((card XX) |-> q))) /\ (dom ((Sgm (rng (g1 mod q))) /^ nn)) by FINSEQ_1:def 3
.= (Seg (len ((Sgm (rng (g1 mod q))) /^ nn))) /\ (dom ((Sgm (rng (g1 mod q))) /^ nn)) by A137, FINSEQ_1:def 18
.= (dom ((Sgm (rng (g1 mod q))) /^ nn)) /\ (dom ((Sgm (rng (g1 mod q))) /^ nn)) by FINSEQ_1:def 3
.= dom ((Sgm (rng (g1 mod q))) /^ nn) ;
then A139: len (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) = len ((Sgm (rng (g1 mod q))) /^ nn) by FINSEQ_3:31;
A140: for d being Nat st d in dom (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) holds
(((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d = q - (((Sgm (rng (g1 mod q))) /^ nn) . d)

proof

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

end;

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

proof

let d be Nat; :: thesis: ( d in dom (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) implies ( (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d > 0 & (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d <= (q -' 1) div 2 ) )
reconsider w = (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d as Element of INT by INT_1:def 2;
assume A143: d in dom (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) ; :: thesis: ( (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d > 0 & (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d <= (q -' 1) div 2 )
then (Sgm XX) . d in rng (Sgm XX) by A94, A138, FUNCT_1:12;
then (Sgm XX) . d in XX by A79, FINSEQ_1:def 13;
then A144: ex ll being Element of NAT st
( ll = (Sgm XX) . d & ll in rng (g1 mod q) & ll > q / 2 ) by A78;
then consider e being Nat such that
A145: e in dom (g1 mod q) and
A146: (g1 mod q) . e = ((Sgm (rng (g1 mod q))) /^ nn) . d by A94, FINSEQ_2:11;
((Sgm (rng (g1 mod q))) /^ nn) . d = (g1 . e) mod q by A25, A145, A146, EULER_2:def 1;
then A147: ((Sgm (rng (g1 mod q))) /^ nn) . d < q by NAT_D:1;
A148: (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d = q - (((Sgm (rng (g1 mod q))) /^ nn) . d) by A140, A143;
then w < q - (q / 2) by A94, A144, XREAL_1:12;
hence ( (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d > 0 & (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d <= (q -' 1) div 2 ) by A83, A148, A147, INT_1:81, XREAL_1:52; :: thesis: verum

end;

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

proof

let d be Nat; :: thesis: ( d in dom (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) implies (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d in NAT )
assume d in dom (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) ; :: thesis: (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d in NAT
then (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d > 0 by A142;
hence (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d in NAT by INT_1:16; :: thesis: verum

end;

then reconsider g5 = ((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn) as FinSequence of NAT by FINSEQ_2:14;
g5 is FinSequence of NAT ;
then reconsider g6 = ((Sgm (rng (g1 mod q))) | nn) ^ (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) as FinSequence of NAT by FINSEQ_1:96;
A149: g6 is FinSequence of REAL by FINSEQ_2:27;
A150: nn <= len (Sgm (rng (g1 mod q))) by A67, XREAL_1:45;
A151: rng ((Sgm (rng (g1 mod q))) | nn) misses rng g5

proof

assume not rng ((Sgm (rng (g1 mod q))) | nn) misses rng g5 ; :: thesis: contradiction
then consider x being set such that
A152: x in rng ((Sgm (rng (g1 mod q))) | nn) and
A153: x in rng g5 by XBOOLE_0:3;
consider e being Nat such that
A154: e in dom g5 and
A155: g5 . e = x by A153, FINSEQ_2:11;
x = q - (((Sgm (rng (g1 mod q))) /^ nn) . e) by A140, A154, A155;
then A156: x = q - ((Sgm (rng (g1 mod q))) . (e + nn)) by A150, A138, A154, RFINSEQ:def 2;
e + nn in dom (Sgm (rng (g1 mod q))) by A138, A154, FINSEQ_5:29;
then consider e1 being Nat such that
A157: e1 in dom (g1 mod q) and
A158: (g1 mod q) . e1 = (Sgm (rng (g1 mod q))) . (e + nn) by A78, FINSEQ_2:11, FUNCT_1:12;
A159: e1 <= (q -' 1) div 2 by A23, A24, A157, FINSEQ_3:27;
rng ((Sgm (rng (g1 mod q))) | nn) c= rng (Sgm (rng (g1 mod q))) by FINSEQ_5:21;
then consider d1 being Nat such that
A160: d1 in dom (g1 mod q) and
A161: (g1 mod q) . d1 = x by A78, A152, FINSEQ_2:11;
d1 <= (q -' 1) div 2 by A23, A24, A160, FINSEQ_3:27;
then d1 + e1 <= ((q -' 1) div 2) + ((q -' 1) div 2) by A159, XREAL_1:9;
then A162: d1 + e1 < q by A29, A40, XREAL_1:148, XXREAL_0:2;
A163: e1 in dom g1 by A24, A157, FINSEQ_3:31;
then A164: (Sgm (rng (g1 mod q))) . (e + nn) = (g1 . e1) mod q by A158, EULER_2:def 1;
A165: d1 in dom g1 by A24, A160, FINSEQ_3:31;
then x = (g1 . d1) mod q by A161, EULER_2:def 1;
then (((g1 . d1) mod q) + ((g1 . e1) mod q)) mod q = 0 by A156, A164, NAT_D:25;
then ((g1 . d1) + (g1 . e1)) mod q = 0 by EULER_2:8;
then q divides (g1 . d1) + (g1 . e1) by PEPIN:6;
then q divides (d1 * p) + (g1 . e1) by A19, A165;
then q divides (d1 * p) + (e1 * p) by A19, A163;
then A166: q divides (d1 + e1) * p ;
d1 >= 1 by A160, FINSEQ_3:27;
hence contradiction by A4, A166, A162, NAT_D:7, PEPIN:3; :: thesis: verum

end;

for d, e being Element of NAT st 1 <= d & d < e & e <= len g5 holds
g5 . d <> g5 . e

proof

let d, e be Element of NAT ; :: thesis: ( 1 <= d & d < e & e <= len g5 implies g5 . d <> g5 . e )
assume that
A167: 1 <= d and
A168: d < e and
A169: e <= len g5 ; :: thesis: g5 . d <> g5 . e
1 <= e by A167, A168, XXREAL_0:2;
then A170: e in dom g5 by A169, FINSEQ_3:27;
then A171: g5 . e = q - (((Sgm (rng (g1 mod q))) /^ nn) . e) by A140;
d < len g5 by A168, A169, XXREAL_0:2;
then A172: d in dom g5 by A167, FINSEQ_3:27;
then g5 . d = q - (((Sgm (rng (g1 mod q))) /^ nn) . d) by A140;
hence g5 . d <> g5 . e by A82, A138, A168, A172, A170, A171, FUNCT_1:def 8; :: thesis: verum

end;

then len g5 = card (rng g5) by GRAPH_5:10;
then g5 is one-to-one by FINSEQ_4:77;
then A173: g6 is one-to-one by A129, A151, FINSEQ_3:98;
A174: 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 A175: d in dom g6 ; :: thesis: ( g6 . d > 0 & g6 . d <= (q -' 1) div 2 )

per cases ( d in dom ((Sgm (rng (g1 mod q))) | nn) or ex l being Nat st
( l in dom g5 & d = (len ((Sgm (rng (g1 mod q))) | nn)) + l ) ) by A175, FINSEQ_1:38;

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

then ((Sgm (rng (g1 mod q))) | nn) . d in rng (Sgm YY) by A128, FUNCT_1:12;
then A177: ((Sgm (rng (g1 mod q))) | nn) . d in YY by A86, FINSEQ_1:def 13;
then A178: ((Sgm (rng (g1 mod q))) | nn) . d in rng (Sgm (rng (g1 mod q))) by XBOOLE_0:def 5;
not ((Sgm (rng (g1 mod q))) | nn) . d in XX by A177, XBOOLE_0:def 5;
then ((Sgm (rng (g1 mod q))) | nn) . d <= q / 2 by A178;
then A179: ((Sgm (rng (g1 mod q))) | nn) . d <= (q -' 1) div 2 by A83, INT_1:81;
not ((Sgm (rng (g1 mod q))) | nn) . d in {0 } by A47, A78, A178, XBOOLE_0:3;
then ((Sgm (rng (g1 mod q))) | nn) . d <> 0 by TARSKI:def 1;
hence ( g6 . d > 0 & g6 . d <= (q -' 1) div 2 ) by A176, A179, FINSEQ_1:def 7; :: thesis: verum

end;

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

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

end;

end;

end;

len g6 = (len ((Sgm (rng (g1 mod q))) | nn)) + (len g5) by FINSEQ_1:35
.= (q -' 1) div 2 by A136, A137, A139 ;
then rng g6 = rng (idseq ((q -' 1) div 2)) by A134, A173, A174, Th40;
then N = Sum g6 by A173, A149, RFINSEQ:22, RFINSEQ:39
.= (Sum ((Sgm (rng (g1 mod q))) | nn)) + (Sum g5) by RVSUM_1:105
.= (Sum ((Sgm (rng (g1 mod q))) | nn)) + (((card XX) * q) - (Sum ((Sgm (rng (g1 mod q))) /^ nn))) by A137, A135, Th47
.= ((Sum ((Sgm (rng (g1 mod q))) | nn)) + ((card XX) * q)) - (Sum ((Sgm (rng (g1 mod q))) /^ nn)) ;
then (p - 1) * N = ((q * (Sum g2)) + (2 * (Sum (Sgm XX)))) - ((card XX) * q) by A92, A94, A128;
then A182: ((p -' 1) * N) mod 2 = (((q * (Sum g2)) - ((card XX) * q)) + (2 * (Sum (Sgm XX)))) mod 2 by A6, XREAL_1:235
.= ((q * (Sum g2)) - ((card XX) * q)) mod 2 by EULER_1:13 ;
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:40;
then Sum g2, card XX are_congruent_mod 2 by INT_2:19;
then (Sum g2) mod 2 = (card XX) mod 2 by INT_3:12;
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

proof

let d be Nat; :: thesis: ( d in dom (idseq ((p -' 1) div 2)) implies (idseq ((p -' 1) div 2)) . d in NAT )
assume A183: d in dom (idseq ((p -' 1) div 2)) ; :: thesis: (idseq ((p -' 1) div 2)) . d in NAT
then d in Seg (len (idseq ((p -' 1) div 2))) by FINSEQ_1:def 3;
then d is Element of Seg ((p -' 1) div 2) by FINSEQ_1:def 18;
then (idseq ((p -' 1) div 2)) . d = d by FINSEQ_2:57;
hence (idseq ((p -' 1) div 2)) . d in NAT by A183; :: thesis: verum

end;

then idseq ((p -' 1) div 2) is FinSequence of NAT by FINSEQ_2:14;
then reconsider M = Sum (idseq ((p -' 1) div 2)) as Element of NAT by Lm3;
A184: 2,p are_relative_prime by A1, EULER_1:3;
set X = { k where k is Element of NAT : ( k in rng (Sgm (rng (f1 mod p))) & k > p / 2 ) } ;
for x being set st x in { k where k is Element of NAT : ( k in rng (Sgm (rng (f1 mod p))) & k > p / 2 ) } holds
x in rng (Sgm (rng (f1 mod p)))

proof

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

end;

then A185: { k where k is Element of NAT : ( k in rng (Sgm (rng (f1 mod p))) & k > p / 2 ) } c= rng (Sgm (rng (f1 mod p))) by TARSKI:def 3;
A186: (p -' 1) div 2 >= 1 by A7, A97, NAT_2:15;
A187: (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 A186, A31;
deffunc H₃( Element of A, Element of B) -> set = ($1 / p) - ($2 / q);
A188: 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
A189: for x being Element of A
for y being Element of B holds z . x,y = H₃(x,y) from FUNCT_7:sch 1(A188);
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 } );
A190: 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 set ; :: 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
A191: ( 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(A190);
A192: dom (Card Pr) = dom Pr by CARD_3:def 2
.= dom f2 by A27, A191, 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 A193: d in dom (Card Pr) ; :: thesis: (Card Pr) . d = f2 . d
then d in Seg ((p -' 1) div 2) by A27, A192, FINSEQ_1:def 3;
then consider m being Element of A such that
A194: m = d and
A195: Pr . d = { [m,y] where y is Element of B : z . m,y > 0 } by A191;
Pr . d = [:{m},(Seg (f2 . m)):]

proof

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

proof

now

assume q mod p = 0 ; :: thesis: contradiction
then A197: 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, A197, NAT_4:12; :: thesis: verum

end;

then A198: - (q div p) = ((- q) div p) + 1 by WSIERP_1:49;
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 A199: (((p -' 1) div 2) * q) div p = ((p - 1) * q) div (2 * p) by A7, A11, NAT_2:29
.= (((p * q) - q) div p) div 2 by PRE_FF:5
.= (q + ((- (q div p)) - 1)) div 2 by A198, INT_3:8
.= ((2 * ((q -' 1) div 2)) + (- (q div p))) div 2 by A29, A40
.= ((q -' 1) div 2) + ((- (q div p)) div 2) by INT_3:8 ;
A200: (((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:50
.= - (q div (2 * p)) by NAT_2:29 ;
then (((p -' 1) div 2) * q) div p = ((q -' 1) div 2) - (q div (2 * p)) by A199;
hence (((p -' 1) div 2) * q) div p <= (q -' 1) div 2 by XREAL_1:45; :: 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:49;
then (- (q div p)) div 2 = (- ((q div p) div 2)) - 1
.= (- (q div (2 * p))) - 1 by NAT_2:29 ;
then (((p -' 1) div 2) * q) div p = ((q -' 1) div 2) - ((q div (2 * p)) + 1) by A199;
hence (((p -' 1) div 2) * q) div p <= (q -' 1) div 2 by XREAL_1:45; :: thesis: verum

end;

end;

end;

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

now

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

end;

then A206: [\((m * q) / p)/] < (m * q) / p by INT_1:48;
let l be set ; :: 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 set such that
A207: x in {m} and
A208: y in Seg (f2 . m) and
A209: l = [x,y] by ZFMISC_1:def 2;
reconsider y = y as Element of NAT by A208;
A210: 1 <= y by A208, FINSEQ_1:3;
y <= f2 . m by A208, FINSEQ_1:3;
then y <= (q -' 1) div 2 by A201, A203, XXREAL_0:2;
then reconsider y = y as Element of B by A210, FINSEQ_1:3;
y <= [\((m * q) / p)/] by A208, A203, FINSEQ_1:3;
then y < (m * q) / p by A206, XXREAL_0:2;
then y * p < ((m * q) / p) * p by XREAL_1:70;
then y * p < m * q by XCMPLX_1:88;
then y / q < m / p by XREAL_1:108;
then (m / p) - (y / q) > 0 by XREAL_1:52;
then z . m,y > 0 by A189;
then [m,y] in Pr . d by A195;
hence l in Pr . d by A207, A209, TARSKI:def 1; :: thesis: verum

end;

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

proof

let l be set ; :: according to TARSKI:def 3 :: thesis: ( not l in Pr . d or l in [:{m},(Seg (f2 . m)):] )
A211: m in {m} by TARSKI:def 1;
m in Seg ((p -' 1) div 2) ;
then A212: 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
A213: l = [m,y1] and
A214: z . m,y1 > 0 by A195;
(m / p) - (y1 / q) > 0 by A189, A214;
then ((m / p) - (y1 / q)) + (y1 / q) > 0 + (y1 / q) by XREAL_1:8;
then (m / p) * q > (y1 / q) * q by XREAL_1:70;
then (m * q) / p > y1 by XCMPLX_1:88;
then (m * q) div p >= y1 by INT_1:81;
then (f1 . m) div p >= y1 by A13, A212;
then A215: y1 <= f2 . m by A27, A99, A212;
y1 >= 1 by FINSEQ_1:3;
then y1 in Seg (f2 . m) by A215, FINSEQ_1:3;
hence l in [:{m},(Seg (f2 . m)):] by A213, A211, ZFMISC_1:def 2; :: thesis: verum

end;

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

end;

then card (Pr . d) = card [:(Seg (f2 . m)),{m}:] by CARD_2:11
.= card (Seg (f2 . m)) by CARD_2:13 ;
then A216: card (Pr . d) = card (f2 . d) by A194, FINSEQ_1:76
.= f2 . d by CARD_1:def 5 ;
d in dom Pr by A193, CARD_3:def 2;
hence (Card Pr) . d = f2 . d by A216, CARD_3:def 2; :: thesis: verum

end;

then A217: Card Pr = f2 by A192, FINSEQ_1:17;
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 } );
A218: 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 set ; :: 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
A219: ( 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(A218);
A220: dom (Card Pk) = Seg (len g2) by A33, A219, CARD_3:def 2
.= dom g2 by FINSEQ_1:def 3 ;
A221: 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 A222: d in dom (Card Pk) ; :: thesis: (Card Pk) . d = g2 . d
then d in Seg ((q -' 1) div 2) by A33, A220, FINSEQ_1:def 3;
then consider n being Element of B such that
A223: n = d and
A224: Pk . d = { [x,n] where x is Element of A : z . x,n < 0 } by A219;
Pk . d = [:(Seg (g2 . n)),{n}:]

proof

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

proof

now

assume p mod q = 0 ; :: thesis: contradiction
then A226: 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, A226, NAT_4:12; :: thesis: verum

end;

then A227: - (p div q) = ((- p) div q) + 1 by WSIERP_1:49;
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 A228: (((q -' 1) div 2) * p) div q = ((q - 1) * p) div (2 * q) by A29, A40, NAT_2:29
.= (((q * p) - p) div q) div 2 by PRE_FF:5
.= (p + ((- (p div q)) - 1)) div 2 by A227, INT_3:8
.= ((2 * ((p -' 1) div 2)) - (p div q)) div 2 by A7, A11
.= ((p -' 1) div 2) + ((- (p div q)) div 2) by INT_3:8 ;
A229: (((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:50
.= - (p div (2 * q)) by NAT_2:29 ;
then (((q -' 1) div 2) * p) div q = ((p -' 1) div 2) - (p div (2 * q)) by A228;
hence (((q -' 1) div 2) * p) div q <= (p -' 1) div 2 by XREAL_1:45; :: 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:49;
then (- (p div q)) div 2 = (- ((p div q) div 2)) - 1
.= (- (p div (2 * q))) - 1 by NAT_2:29 ;
then (((q -' 1) div 2) * p) div q = ((p -' 1) div 2) - ((p div (2 * q)) + 1) by A228;
hence (((q -' 1) div 2) * p) div q <= (p -' 1) div 2 by XREAL_1:45; :: thesis: verum

end;

end;

end;

n in Seg ((q -' 1) div 2) ;
then A230: n in dom g1 by A23, FINSEQ_1:def 3;
then A231: g2 . n = (g1 . n) div q by A33, A34
.= (n * p) div q by A19, A230 ;
let l be set ; :: 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 set such that
A232: x in Seg (g2 . n) and
A233: y in {n} and
A234: l = [x,y] by ZFMISC_1:def 2;
reconsider x = x as Element of NAT by A232;
A235: x <= g2 . n by A232, FINSEQ_1:3;
n <= (q -' 1) div 2 by FINSEQ_1:3;
then n * p <= ((q -' 1) div 2) * p by XREAL_1:66;
then (n * p) div q <= (((q -' 1) div 2) * p) div q by NAT_2:26;
then (n * p) div q <= (p -' 1) div 2 by A229, XXREAL_0:2;
then A236: x <= (p -' 1) div 2 by A231, A235, XXREAL_0:2;
1 <= x by A232, FINSEQ_1:3;
then reconsider x = x as Element of A by A236, FINSEQ_1:3;

now

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

end;

then [\((n * p) / q)/] < (n * p) / q by INT_1:48;
then x < (n * p) / q by A231, A235, XXREAL_0:2;
then x * q < ((n * p) / q) * q by XREAL_1:70;
then x * q < n * p by XCMPLX_1:88;
then (x / p) - (n / q) < 0 by XREAL_1:51, XREAL_1:108;
then z . x,n < 0 by A189;
then [x,n] in Pk . d by A224;
hence l in Pk . d by A233, A234, TARSKI:def 1; :: thesis: verum

end;

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

proof

let l be set ; :: according to TARSKI:def 3 :: thesis: ( not l in Pk . d or l in [:(Seg (g2 . n)),{n}:] )
A239: n in {n} by TARSKI:def 1;
n in Seg ((q -' 1) div 2) ;
then A240: 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
A241: l = [x,n] and
A242: z . x,n < 0 by A224;
(x / p) - (n / q) < 0 by A189, A242;
then ((x / p) - (n / q)) + (n / q) < 0 + (n / q) by XREAL_1:8;
then (x / p) * p < (n / q) * p by XREAL_1:70;
then x < (n * p) / q by XCMPLX_1:88;
then x <= (n * p) div q by INT_1:81;
then (g1 . n) div q >= x by A19, A240;
then A243: x <= g2 . n by A33, A34, A240;
x >= 1 by FINSEQ_1:3;
then x in Seg (g2 . n) by A243, FINSEQ_1:3;
hence l in [:(Seg (g2 . n)),{n}:] by A241, A239, ZFMISC_1:def 2; :: thesis: verum

end;

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

end;

then card (Pk . d) = card (Seg (g2 . n)) by CARD_2:13;
then A244: card (Pk . d) = card (g2 . d) by A223, FINSEQ_1:76
.= g2 . d by CARD_1:def 5 ;
d in dom Pk by A222, CARD_3:def 2;
hence (Card Pk) . d = g2 . d by A244, 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:53;
dom z c= U1 \/ U2

proof

let l be set ; :: 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 set such that
A245: x in A and
A246: y in B and
A247: l = [x,y] by ZFMISC_1:def 2;
reconsider y = y as Element of B by A246;
reconsider x = x as Element of A by A245;
A248: z . x,y <> 0

proof

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

end;

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

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

S₁[x,Pr . x] by A191;
then l in Pr . x by A247, A251;
then l in Union Pr by A191, PROB_3:54;
hence l in U1 \/ U2 by XBOOLE_0:def 3; :: thesis: verum

end;

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

S₂[y,Pk . y] by A219;
then l in Pk . y by A247, A252;
then l in Union Pk by A219, PROB_3:54;
hence l in U1 \/ U2 by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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

proof

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

end;

A266: 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
A267: d in dom Pk and
A268: e in dom Pk and
A269: d <> e ; :: thesis: Pk . d misses Pk . e
consider y2 being Element of B such that
A270: y2 = e and
A271: Pk . e = { [x,y2] where x is Element of A : z . x,y2 < 0 } by A219, A268;
consider y1 being Element of B such that
A272: y1 = d and
A273: Pk . d = { [x,y1] where x is Element of A : z . x,y1 < 0 } by A219, A267;

now

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

end;

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

end;

len Pk = (q -' 1) div 2 by A219, FINSEQ_1:def 3;
then A277: card (union (rng Pk)) = Sum (Card Pk) by A266, Th48;
A278: 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
A279: d in dom Pr and
A280: e in dom Pr and
A281: d <> e ; :: thesis: Pr . d misses Pr . e
consider x2 being Element of A such that
A282: x2 = e and
A283: Pr . e = { [x2,y] where y is Element of B : z . x2,y > 0 } by A191, A280;
consider x1 being Element of A such that
A284: x1 = d and
A285: Pr . d = { [x1,y] where y is Element of B : z . x1,y > 0 } by A191, A279;

now

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

end;

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

end;

len Pr = (p -' 1) div 2 by A191, FINSEQ_1:def 3;
then card (union (rng Pr)) = Sum (Card Pr) by A278, Th48;
then card (U1 \/ U2) = (Sum (Card Pr)) + (Sum (Card Pk)) by A277, A254, CARD_2:53;
then (Sum (Card Pr)) + (Sum (Card Pk)) = card [:A,B:] by A253, FUNCT_2:def 1
.= (card A) * (card B) by CARD_2:65
.= ((p -' 1) div 2) * (card B) by FINSEQ_1:78
.= ((p -' 1) div 2) * ((q -' 1) div 2) by FINSEQ_1:78 ;
hence (Sum f2) + (Sum g2) = ((p -' 1) div 2) * ((q -' 1) div 2) by A217, A220, A221, FINSEQ_1:17; :: thesis: verum

end;

dom (p * f2) = dom f2 by VALUED_1:def 5;
then A289: len (p * f2) = (p -' 1) div 2 by A27, FINSEQ_3:31;
p * f2 is Element of NAT * by FINSEQ_1:def 11;
then p * f2 in ((p -' 1) div 2) -tuples_on NAT by A289;
then A290: p * f2 is Element of ((p -' 1) div 2) -tuples_on REAL by FINSEQ_2:129;
A291: (p -' 1) div 2 = ((p -' 1) + 1) div 2 by A9, NAT_2:28
.= p div 2 by A6, XREAL_1:237 ;
reconsider X = { k where k is Element of NAT : ( k in rng (Sgm (rng (f1 mod p))) & k > p / 2 ) } as finite Subset of NAT by A185, XBOOLE_1:1;
set m = card X;
reconsider Y = (rng (Sgm (rng (f1 mod p)))) \ X as finite Subset of NAT ;
A292: f1 mod p is Element of NAT * by FINSEQ_1:def 11;
len (f1 mod p) = (p -' 1) div 2 by A17, A95, FINSEQ_1:def 18;
then f1 mod p in ((p -' 1) div 2) -tuples_on NAT by A292;
then A293: f1 mod p is Element of ((p -' 1) div 2) -tuples_on REAL by FINSEQ_2:129;
A294: rng (f1 mod p) c= Seg n1 by A98, A107, XBOOLE_1:73;
then A295: rng (Sgm (rng (f1 mod p))) = rng (f1 mod p) by FINSEQ_1:def 13;
then A296: X c= Seg n1 by A294, A185, XBOOLE_1:1;
A297: dom ((p * f2) + (f1 mod p)) = (dom (p * f2)) /\ (dom (f1 mod p)) by VALUED_1:def 1
.= (dom f2) /\ (dom (f1 mod p)) by VALUED_1:def 5
.= dom f1 by A96, A99 ;
for d being Nat st d in dom f1 holds
f1 . d = ((p * f2) + (f1 mod p)) . d

proof

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

end;

then f1 = (p * f2) + (f1 mod p) by A297, FINSEQ_1:17;
then A300: Sum f1 = (Sum (p * f2)) + (Sum (f1 mod p)) by A290, A293, RVSUM_1:119
.= (p * (Sum f2)) + (Sum (f1 mod p)) by RVSUM_1:117 ;
A302: (rng (Sgm (rng (f1 mod p)))) \ X c= rng (Sgm (rng (f1 mod p))) by XBOOLE_1:36;
then A303: Y c= Seg n1 by A294, A295, XBOOLE_1:1;
A304: len (f1 mod p) = card (rng (Sgm (rng (f1 mod p)))) by A126, A295, FINSEQ_4:77;
then reconsider n = ((p -' 1) div 2) - (card X) as Element of NAT by A18, A95, A185, NAT_1:21, NAT_1:44;
A305: Sgm (rng (f1 mod p)) = ((Sgm (rng (f1 mod p))) | n) ^ ((Sgm (rng (f1 mod p))) /^ n) by RFINSEQ:21;
then A306: (Sgm (rng (f1 mod p))) /^ n is one-to-one by A108, FINSEQ_3:98;
Sgm (rng (f1 mod p)) is FinSequence of REAL by FINSEQ_2:27;
then A307: Sum (Sgm (rng (f1 mod p))) = Sum (f1 mod p) by A126, A295, A108, RFINSEQ:22, RFINSEQ:39;
for k, l being Element of NAT st k in Y & l in X holds
k < l

proof

let k, l be Element of NAT ; :: thesis: ( k in Y & l in X implies k < l )
assume that
A308: k in Y and
A309: l in X ; :: thesis: k < l
A310: not k in X by A308, XBOOLE_0:def 5;
A311: ex l1 being Element of NAT st
( l1 = l & l1 in rng (Sgm (rng (f1 mod p))) & l1 > p / 2 ) by A309;
k in rng (Sgm (rng (f1 mod p))) by A308, XBOOLE_0:def 5;
then k <= p / 2 by A310;
hence k < l by A311, XXREAL_0:2; :: thesis: verum

end;

then Sgm (Y \/ X) = (Sgm Y) ^ (Sgm X) by A296, A303, FINSEQ_3:48;
then Sgm ((rng (Sgm (rng (f1 mod p)))) \/ X) = (Sgm Y) ^ (Sgm X) by XBOOLE_1:39;
then A312: Sgm (rng (f1 mod p)) = (Sgm Y) ^ (Sgm X) by A295, A185, XBOOLE_1:12;
then Sum (Sgm (rng (f1 mod p))) = (Sum (Sgm Y)) + (Sum (Sgm X)) by RVSUM_1:105;
then A313: q * (Sum (idseq ((p -' 1) div 2))) = ((p * (Sum f2)) + (Sum (Sgm Y))) + (Sum (Sgm X)) by A300, A307, RVSUM_1:117;
A314: len (Sgm Y) = card Y by A294, A295, A302, FINSEQ_3:44, XBOOLE_1:1
.= ((p -' 1) div 2) - (card X) by A18, A95, A185, A304, CARD_2:63 ;
then A315: (Sgm (rng (f1 mod p))) /^ n = Sgm X by A312, FINSEQ_5:40;
A316: (Sgm (rng (f1 mod p))) | n = Sgm Y by A312, A314, FINSEQ_3:122, FINSEQ_6:12;
A317: (Sgm (rng (f1 mod p))) | n is one-to-one by A108, A305, FINSEQ_3:98;
Lege q,p = (- 1) |^ (Sum f2)

proof

set f5 = ((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n);
set f6 = ((Sgm (rng (f1 mod p))) | n) ^ (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n));
A324: rng (idseq ((p -' 1) div 2)) = Seg ((p -' 1) div 2) by RELAT_1:71;
A325: (Sgm (rng (f1 mod p))) /^ n is FinSequence of REAL by FINSEQ_2:27;
A326: len ((Sgm (rng (f1 mod p))) | n) = n by A127, FINSEQ_1:80, XREAL_1:45;
A327: len ((Sgm (rng (f1 mod p))) /^ n) = (len (Sgm (rng (f1 mod p)))) -' n by RFINSEQ:42
.= (len (Sgm (rng (f1 mod p)))) - n by A127, XREAL_1:45, XREAL_1:235
.= card X by A127 ;
A328: dom (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) = (dom ((card X) |-> p)) /\ (dom ((Sgm (rng (f1 mod p))) /^ n)) by VALUED_1:12
.= (Seg (len ((card X) |-> p))) /\ (dom ((Sgm (rng (f1 mod p))) /^ n)) by FINSEQ_1:def 3
.= (Seg (len ((Sgm (rng (f1 mod p))) /^ n))) /\ (dom ((Sgm (rng (f1 mod p))) /^ n)) by A327, FINSEQ_1:def 18
.= (dom ((Sgm (rng (f1 mod p))) /^ n)) /\ (dom ((Sgm (rng (f1 mod p))) /^ n)) by FINSEQ_1:def 3
.= dom ((Sgm (rng (f1 mod p))) /^ n) ;
then A329: len (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) = len ((Sgm (rng (f1 mod p))) /^ n) by FINSEQ_3:31;
A330: for d being Nat st d in dom (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) holds
(((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d = p - (((Sgm (rng (f1 mod p))) /^ n) . d)

proof

let d be Nat; :: thesis: ( d in dom (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) implies (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d = p - (((Sgm (rng (f1 mod p))) /^ n) . d) )
assume A331: d in dom (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) ; :: thesis: (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d = p - (((Sgm (rng (f1 mod p))) /^ n) . d)
then d in Seg (card X) by A327, A328, FINSEQ_1:def 3;
then ((card X) |-> p) . d = p by FINSEQ_2:71;
hence (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d = p - (((Sgm (rng (f1 mod p))) /^ n) . d) by A331, VALUED_1:13; :: thesis: verum

end;

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

proof

let d be Nat; :: thesis: ( d in dom (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) implies ( (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d > 0 & (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d <= (p -' 1) div 2 ) )
reconsider w = (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d as Element of INT by INT_1:def 2;
assume A333: d in dom (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) ; :: thesis: ( (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d > 0 & (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d <= (p -' 1) div 2 )
then (Sgm X) . d in rng (Sgm X) by A315, A328, FUNCT_1:12;
then (Sgm X) . d in X by A296, FINSEQ_1:def 13;
then A334: ex ll being Element of NAT st
( ll = (Sgm X) . d & ll in rng (f1 mod p) & ll > p / 2 ) by A295;
then consider e being Nat such that
A335: e in dom (f1 mod p) and
A336: (f1 mod p) . e = ((Sgm (rng (f1 mod p))) /^ n) . d by A315, FINSEQ_2:11;
((Sgm (rng (f1 mod p))) /^ n) . d = (f1 . e) mod p by A96, A335, A336, EULER_2:def 1;
then A337: ((Sgm (rng (f1 mod p))) /^ n) . d < p by NAT_D:1;
A338: (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d = p - (((Sgm (rng (f1 mod p))) /^ n) . d) by A330, A333;
then w < p - (p / 2) by A315, A334, XREAL_1:12;
hence ( (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d > 0 & (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d <= (p -' 1) div 2 ) by A291, A338, A337, INT_1:81, XREAL_1:52; :: thesis: verum

end;

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

proof

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

end;

then reconsider f5 = ((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n) as FinSequence of NAT by FINSEQ_2:14;
f5 is FinSequence of NAT ;
then reconsider f6 = ((Sgm (rng (f1 mod p))) | n) ^ (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) as FinSequence of NAT by FINSEQ_1:96;
A339: f6 is FinSequence of REAL by FINSEQ_2:27;
A340: n <= len (Sgm (rng (f1 mod p))) by A127, XREAL_1:45;
A341: rng ((Sgm (rng (f1 mod p))) | n) misses rng f5

proof

assume not rng ((Sgm (rng (f1 mod p))) | n) misses rng f5 ; :: thesis: contradiction
then consider x being set such that
A342: x in rng ((Sgm (rng (f1 mod p))) | n) and
A343: x in rng f5 by XBOOLE_0:3;
consider e being Nat such that
A344: e in dom f5 and
A345: f5 . e = x by A343, FINSEQ_2:11;
x = p - (((Sgm (rng (f1 mod p))) /^ n) . e) by A330, A344, A345;
then A346: x = p - ((Sgm (rng (f1 mod p))) . (e + n)) by A340, A328, A344, RFINSEQ:def 2;
e + n in dom (Sgm (rng (f1 mod p))) by A328, A344, FINSEQ_5:29;
then consider e1 being Nat such that
A347: e1 in dom (f1 mod p) and
A348: (f1 mod p) . e1 = (Sgm (rng (f1 mod p))) . (e + n) by A295, FINSEQ_2:11, FUNCT_1:12;
A349: e1 <= (p -' 1) div 2 by A18, A95, A347, FINSEQ_3:27;
rng ((Sgm (rng (f1 mod p))) | n) c= rng (Sgm (rng (f1 mod p))) by FINSEQ_5:21;
then consider d1 being Nat such that
A350: d1 in dom (f1 mod p) and
A351: (f1 mod p) . d1 = x by A295, A342, FINSEQ_2:11;
d1 <= (p -' 1) div 2 by A18, A95, A350, FINSEQ_3:27;
then d1 + e1 <= ((p -' 1) div 2) + ((p -' 1) div 2) by A349, XREAL_1:9;
then A352: d1 + e1 < p by A7, A11, XREAL_1:148, XXREAL_0:2;
x = (f1 . d1) mod p by A96, A350, A351, EULER_2:def 1;
then ((f1 . d1) mod p) + ((Sgm (rng (f1 mod p))) . (e + n)) = p by A346;
then ((f1 . d1) mod p) + ((f1 . e1) mod p) = p by A96, A347, A348, EULER_2:def 1;
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 EULER_2:8;
then p divides (f1 . d1) + (f1 . e1) by PEPIN:6;
then p divides (d1 * q) + (f1 . e1) by A13, A96, A350;
then p divides (d1 * q) + (e1 * q) by A13, A96, A347;
then A353: p divides (d1 + e1) * q ;
d1 >= 1 by A350, FINSEQ_3:27;
hence contradiction by A4, A353, A352, NAT_D:7, PEPIN:3; :: thesis: verum

end;

for d, e being Element of NAT st 1 <= d & d < e & e <= len f5 holds
f5 . d <> f5 . e

proof

let d, e be Element of NAT ; :: thesis: ( 1 <= d & d < e & e <= len f5 implies f5 . d <> f5 . e )
assume that
A354: 1 <= d and
A355: d < e and
A356: e <= len f5 ; :: thesis: f5 . d <> f5 . e
1 <= e by A354, A355, XXREAL_0:2;
then A357: e in dom f5 by A356, FINSEQ_3:27;
then A358: f5 . e = p - (((Sgm (rng (f1 mod p))) /^ n) . e) by A330;
d < len f5 by A355, A356, XXREAL_0:2;
then A359: d in dom f5 by A354, FINSEQ_3:27;
then f5 . d = p - (((Sgm (rng (f1 mod p))) /^ n) . d) by A330;
hence f5 . d <> f5 . e by A306, A328, A355, A359, A357, A358, FUNCT_1:def 8; :: thesis: verum

end;

then len f5 = card (rng f5) by GRAPH_5:10;
then f5 is one-to-one by FINSEQ_4:77;
then A360: f6 is one-to-one by A317, A341, FINSEQ_3:98;
A361: 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 A362: d in dom f6 ; :: thesis: ( f6 . d > 0 & f6 . d <= (p -' 1) div 2 )

per cases ( d in dom ((Sgm (rng (f1 mod p))) | n) or ex l being Nat st
( l in dom f5 & d = (len ((Sgm (rng (f1 mod p))) | n)) + l ) ) by A362, FINSEQ_1:38;

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

then ((Sgm (rng (f1 mod p))) | n) . d in rng (Sgm Y) by A316, FUNCT_1:12;
then A364: ((Sgm (rng (f1 mod p))) | n) . d in Y by A303, FINSEQ_1:def 13;
then A365: ((Sgm (rng (f1 mod p))) | n) . d in rng (Sgm (rng (f1 mod p))) by XBOOLE_0:def 5;
not ((Sgm (rng (f1 mod p))) | n) . d in X by A364, XBOOLE_0:def 5;
then ((Sgm (rng (f1 mod p))) | n) . d <= p / 2 by A365;
then A366: ((Sgm (rng (f1 mod p))) | n) . d <= (p -' 1) div 2 by A291, INT_1:81;
not ((Sgm (rng (f1 mod p))) | n) . d in {0 } by A107, A295, A365, XBOOLE_0:3;
then ((Sgm (rng (f1 mod p))) | n) . d <> 0 by TARSKI:def 1;
hence ( f6 . d > 0 & f6 . d <= (p -' 1) div 2 ) by A363, A366, FINSEQ_1:def 7; :: thesis: verum

end;

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

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

end;

end;

end;

len f6 = (len ((Sgm (rng (f1 mod p))) | n)) + (len f5) by FINSEQ_1:35
.= (p -' 1) div 2 by A326, A327, A329 ;
then rng f6 = rng (idseq ((p -' 1) div 2)) by A324, A360, A361, Th40;
then M = Sum f6 by A360, A339, RFINSEQ:22, RFINSEQ:39
.= (Sum ((Sgm (rng (f1 mod p))) | n)) + (Sum f5) by RVSUM_1:105
.= (Sum ((Sgm (rng (f1 mod p))) | n)) + (((card X) * p) - (Sum ((Sgm (rng (f1 mod p))) /^ n))) by A327, A325, Th47
.= ((Sum ((Sgm (rng (f1 mod p))) | n)) + ((card X) * p)) - (Sum ((Sgm (rng (f1 mod p))) /^ n)) ;
then (q - 1) * M = ((p * (Sum f2)) + (2 * (Sum (Sgm X)))) - ((card X) * p) by A313, A315, A316;
then A369: ((q -' 1) * M) mod 2 = (((p * (Sum f2)) - ((card X) * p)) + (2 * (Sum (Sgm X)))) mod 2 by A28, XREAL_1:235
.= ((p * (Sum f2)) - ((card X) * p)) mod 2 by EULER_1:13 ;
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 A369, Lm1;
then 2 divides (Sum f2) - (card X) by A184, INT_2:40;
then Sum f2, card X are_congruent_mod 2 by INT_2:19;
then (Sum f2) mod 2 = (card X) mod 2 by INT_3:12;
then (- 1) |^ (Sum f2) = (- 1) |^ (card X) by Th45;
hence Lege q,p = (- 1) |^ (Sum f2) by A1, A5, A295, Th41; :: thesis: verum

end;

hence (Lege p,q) * (Lege q,p) = (- 1) |^ (((p -' 1) div 2) * ((q -' 1) div 2)) by A130, A187, NEWTON:13; :: thesis: verum