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) by NAT_D:3;

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

(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

(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;

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:29;

set XX = { k where k is Element of NAT : ( k in rng (Sgm (rng (g1 mod q))) & k > q / 2 ) } ;

for x being object 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)))

reconsider f1 = q * (idseq ((p -' 1) div 2)) as FinSequence of NAT by A16, FINSEQ_2:12;

deffunc H_{1}( 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_{1}(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 (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 ;

then consider n2 being Element of NAT such that

A32: rng (g1 mod q) c= (Seg n2) \/ {0} by HEYTING3:1;

deffunc H_{2}( 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_{2}(d) ) )
from FINSEQ_1:sch 2();

for d being Nat st d in dom g2 holds

g2 . d in NAT

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) + ((g1 mod q) . d)

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 ;

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 (g1 mod q)

then A48: Sgm (rng (g1 mod q)) is one-to-one by A32, FINSEQ_3:92, 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

x = y

then len (g1 mod q) = card (rng (g1 mod q)) by FINSEQ_4:62;

then A67: len (Sgm (rng (g1 mod q))) = (q -' 1) div 2 by A23, A24, A32, A47, FINSEQ_3:39, 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: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) + (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

then A76: Sum g1 = (Sum (q * g2)) + (Sum (g1 mod q)) by A72, A69, RVSUM_1:89

.= (q * (Sum g2)) + (Sum (g1 mod q)) by RVSUM_1:87 ;

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;

A80: len (g1 mod q) = card (rng (Sgm (rng (g1 mod q)))) by A66, A78, FINSEQ_4:62;

card XX <= card (rng (Sgm (rng (g1 mod q)))) by A26, NAT_1:43;

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:8;

then A82: (Sgm (rng (g1 mod q))) /^ 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 ;

A84: g1 mod q is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

Sgm (rng (g1 mod q)) is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

then A85: Sum (Sgm (rng (g1 mod q))) = Sum (g1 mod q) by A66, A78, A48, RFINSEQ:9, RFINSEQ:26, A84;

A86: (rng (Sgm (rng (g1 mod q)))) \ XX c= rng (Sgm (rng (g1 mod q))) by XBOOLE_1:36;

then A87: YY c= Seg n2 by A77, A78;

for k, l being Nat st k in YY & l in XX holds

k < l

then Sgm ((rng (Sgm (rng (g1 mod q)))) \/ XX) = (Sgm YY) ^ (Sgm XX) by XBOOLE_1:39;

then A92: 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: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 A77, A78, A86, FINSEQ_3:39, XBOOLE_1:1

.= ((q -' 1) div 2) - (card XX) by A23, A24, A26, A80, CARD_2:44 ;

then A95: (Sgm (rng (g1 mod q))) /^ nn = Sgm XX by A92, FINSEQ_5:37;

for d being Nat st d in dom f2 holds

f2 . d in NAT

set f3 = f1 mod p;

A96: len (f1 mod p) = len f1 by EULER_2:def 1;

then A97: dom f1 = dom (f1 mod p) by FINSEQ_3:29;

set f4 = Sgm (rng (f1 mod p));

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

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

then f1 mod p <> {} by A18, A7, A96, NAT_2:13;

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

then consider n1 being Element of NAT such that

A99: rng (f1 mod p) 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) + ((f1 mod p) . d)

then A109: Sgm (rng (f1 mod p)) is one-to-one by A99, FINSEQ_3:92, XBOOLE_1:73;

A110: for d, e being Nat st d in dom f1 & e in dom f1 & p divides (f1 . d) - (f1 . e) holds

d = e

x = y

then len (f1 mod p) = card (rng (f1 mod p)) by FINSEQ_4:62;

then A128: len (Sgm (rng (f1 mod p))) = (p -' 1) div 2 by A18, A96, A99, A108, FINSEQ_3:39, XBOOLE_1:73;

A129: (Sgm (rng (g1 mod q))) | nn = Sgm YY by A92, A94, FINSEQ_3:113, FINSEQ_6:10;

A130: (Sgm (rng (g1 mod q))) | nn is one-to-one by A48, A81, FINSEQ_3:91;

A131: Lege (p,q) = (- 1) |^ (Sum g2)

(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 (f1 mod p))) & k > p / 2 ) } ;

for x being object 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)))

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)

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 (f1 mod p))) & k > p / 2 ) } as finite Subset of NAT by A184, XBOOLE_1:1;

set m = card X;

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

A291: f1 mod p is Element of NAT * by FINSEQ_1:def 11;

len (f1 mod p) = (p -' 1) div 2 by A17, A96, CARD_1:def 7;

then f1 mod p in ((p -' 1) div 2) -tuples_on NAT by A291;

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

A293: rng (f1 mod p) c= Seg n1 by A99, A108, XBOOLE_1:73;

then A294: rng (Sgm (rng (f1 mod p))) = rng (f1 mod p) by FINSEQ_1:def 13;

then A295: X c= Seg n1 by A293, A184;

A296: 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 A97, A100 ;

for d being Nat st d in dom f1 holds

f1 . d = ((p * f2) + (f1 mod p)) . d

then A299: Sum f1 = (Sum (p * f2)) + (Sum (f1 mod p)) by A289, A292, RVSUM_1:89

.= (p * (Sum f2)) + (Sum (f1 mod p)) by RVSUM_1:87 ;

A300: (rng (Sgm (rng (f1 mod p)))) \ X c= rng (Sgm (rng (f1 mod p))) by XBOOLE_1:36;

then A301: Y c= Seg n1 by A293, A294;

A302: len (f1 mod p) = card (rng (Sgm (rng (f1 mod p)))) 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 (f1 mod p)) = ((Sgm (rng (f1 mod p))) | n) ^ ((Sgm (rng (f1 mod p))) /^ n) by RFINSEQ:8;

then A304: (Sgm (rng (f1 mod p))) /^ n is one-to-one by A109, FINSEQ_3:91;

A305: f1 mod p is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

Sgm (rng (f1 mod p)) is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

then A306: Sum (Sgm (rng (f1 mod p))) = Sum (f1 mod p) by A127, A294, A109, RFINSEQ:9, RFINSEQ:26, A305;

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

k < l

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

then A311: Sgm (rng (f1 mod p)) = (Sgm Y) ^ (Sgm X) by A294, A184, XBOOLE_1:12;

then Sum (Sgm (rng (f1 mod p))) = (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 A293, A294, A300, FINSEQ_3:39, XBOOLE_1:1

.= ((p -' 1) div 2) - (card X) by A18, A96, A184, A302, CARD_2:44 ;

then A314: (Sgm (rng (f1 mod p))) /^ n = Sgm X by A311, FINSEQ_5:37;

A315: (Sgm (rng (f1 mod p))) | n = Sgm Y by A311, A313, FINSEQ_3:113, FINSEQ_6:10;

A316: (Sgm (rng (f1 mod p))) | n is one-to-one by A109, A303, FINSEQ_3:91;

Lege (q,p) = (- 1) |^ (Sum f2)

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) by NAT_D:3;

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

A16:
for d being Nat st d in dom (q * (idseq ((p -' 1) div 2))) holds
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;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

(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

A22:
for d being Nat st d in dom (p * (idseq ((q -' 1) div 2))) holds
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;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

(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;

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:29;

set XX = { k where k is Element of NAT : ( k in rng (Sgm (rng (g1 mod q))) & k > q / 2 ) } ;

for x being object 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

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)))
;
let x be object ; :: 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;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

reconsider f1 = q * (idseq ((p -' 1) div 2)) as FinSequence of NAT by A16, FINSEQ_2:12;

deffunc H

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

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 (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 ;

then consider n2 being Element of NAT such that

A32: rng (g1 mod q) c= (Seg n2) \/ {0} by HEYTING3:1;

deffunc H

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

for d being Nat st d in dom g2 holds

g2 . d in NAT

proof

then reconsider g2 = g2 as FinSequence of NAT by FINSEQ_2:12;
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;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

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) + ((g1 mod q) . d)

proof

q is odd
by A2, PEPIN:17;
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;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

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 ;

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 (g1 mod q)

proof

then A47:
{0} misses rng (g1 mod q)
by ZFMISC_1:50;
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: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 consider a being Nat such that

A42: a in dom (g1 mod q) and

A43: (g1 mod q) . 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

then A48: Sgm (rng (g1 mod q)) is one-to-one by A32, FINSEQ_3:92, 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

for x, y being object st x in dom (g1 mod q) & y in dom (g1 mod q) & (g1 mod q) . x = (g1 mod q) . y holds
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;

end;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

hence
d = e
; :: thesis: verumassume
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;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

x = y

proof

then A66:
g1 mod q is one-to-one
;
let x, y be object ; :: 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) ;

hence x = y by A49, A25, A62, A63; :: thesis: verum

end;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) ;

hence x = y by A49, A25, A62, A63; :: thesis: verum

then len (g1 mod q) = card (rng (g1 mod q)) by FINSEQ_4:62;

then A67: len (Sgm (rng (g1 mod q))) = (q -' 1) div 2 by A23, A24, A32, A47, FINSEQ_3:39, 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: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) + (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

then
g1 = (q * g2) + (g1 mod q)
by A73;
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;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

then A76: Sum g1 = (Sum (q * g2)) + (Sum (g1 mod q)) by A72, A69, RVSUM_1:89

.= (q * (Sum g2)) + (Sum (g1 mod q)) by RVSUM_1:87 ;

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;

A80: len (g1 mod q) = card (rng (Sgm (rng (g1 mod q)))) by A66, A78, FINSEQ_4:62;

card XX <= card (rng (Sgm (rng (g1 mod q)))) by A26, NAT_1:43;

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:8;

then A82: (Sgm (rng (g1 mod q))) /^ 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 ;

A84: g1 mod q is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

Sgm (rng (g1 mod q)) is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

then A85: Sum (Sgm (rng (g1 mod q))) = Sum (g1 mod q) by A66, A78, A48, RFINSEQ:9, RFINSEQ:26, A84;

A86: (rng (Sgm (rng (g1 mod q)))) \ XX c= rng (Sgm (rng (g1 mod q))) by XBOOLE_1:36;

then A87: YY c= Seg n2 by A77, A78;

for k, l being Nat st k in YY & l in XX holds

k < l

proof

then
Sgm (YY \/ XX) = (Sgm YY) ^ (Sgm XX)
by A87, A79, FINSEQ_3:42;
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 (g1 mod q))) & l1 > q / 2 ) by A89;

k in rng (Sgm (rng (g1 mod q))) by A88, XBOOLE_0:def 5;

then k <= q / 2 by A90;

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

end;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 (g1 mod q))) & l1 > q / 2 ) by A89;

k in rng (Sgm (rng (g1 mod q))) by A88, XBOOLE_0:def 5;

then k <= q / 2 by A90;

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

then Sgm ((rng (Sgm (rng (g1 mod q)))) \/ XX) = (Sgm YY) ^ (Sgm XX) by XBOOLE_1:39;

then A92: 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: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 A77, A78, A86, FINSEQ_3:39, XBOOLE_1:1

.= ((q -' 1) div 2) - (card XX) by A23, A24, A26, A80, CARD_2:44 ;

then A95: (Sgm (rng (g1 mod q))) /^ nn = Sgm XX by A92, FINSEQ_5:37;

for d being Nat st d in dom f2 holds

f2 . d in NAT

proof

then reconsider f2 = f2 as FinSequence of NAT by FINSEQ_2:12;
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;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

set f3 = f1 mod p;

A96: len (f1 mod p) = len f1 by EULER_2:def 1;

then A97: dom f1 = dom (f1 mod p) by FINSEQ_3:29;

set f4 = Sgm (rng (f1 mod p));

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

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

then f1 mod p <> {} by A18, A7, A96, NAT_2:13;

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

then consider n1 being Element of NAT such that

A99: rng (f1 mod p) 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) + ((f1 mod p) . d)

proof

not 0 in rng (f1 mod p)
let d be Nat; :: thesis: ( d in dom f1 implies f1 . d = ((f2 . d) * p) + ((f1 mod p) . d) )

assume A102: d in dom f1 ; :: thesis: f1 . d = ((f2 . d) * p) + ((f1 mod p) . d)

then A103: (f1 mod p) . d = (f1 . d) mod p by EULER_2:def 1;

f2 . d = (f1 . d) div p by A27, A100, A102;

hence f1 . d = ((f2 . d) * p) + ((f1 mod p) . d) by A103, NAT_D:2; :: thesis: verum

end;assume A102: d in dom f1 ; :: thesis: f1 . d = ((f2 . d) * p) + ((f1 mod p) . d)

then A103: (f1 mod p) . d = (f1 . d) mod p by EULER_2:def 1;

f2 . d = (f1 . d) div p by A27, A100, A102;

hence f1 . d = ((f2 . d) * p) + ((f1 mod p) . d) by A103, NAT_D:2; :: thesis: verum

proof

then A108:
{0} misses rng (f1 mod p)
by ZFMISC_1:50;
assume
0 in rng (f1 mod p)
; :: thesis: contradiction

then consider a being Nat such that

A104: a in dom (f1 mod p) and

A105: (f1 mod p) . 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 consider a being Nat such that

A104: a in dom (f1 mod p) and

A105: (f1 mod p) . 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

then A109: Sgm (rng (f1 mod p)) is one-to-one by A99, FINSEQ_3:92, XBOOLE_1:73;

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

for x, y being object st x in dom (f1 mod p) & y in dom (f1 mod p) & (f1 mod p) . x = (f1 mod p) . y holds
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;

end;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

hence
d = e
; :: thesis: verumassume
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;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

x = y

proof

then A127:
f1 mod p is one-to-one
;
let x, y be object ; :: 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

A123: x in dom (f1 mod p) and

A124: y in dom (f1 mod p) and

A125: (f1 mod p) . x = (f1 mod p) . y ; :: thesis: x = y

reconsider x = x, y = y as Element of NAT by A123, A124;

A126: f1 . y = ((f2 . y) * p) + ((f1 mod p) . y) by A97, A101, A124;

f1 . x = ((f2 . x) * p) + ((f1 mod p) . 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;assume that

A123: x in dom (f1 mod p) and

A124: y in dom (f1 mod p) and

A125: (f1 mod p) . x = (f1 mod p) . y ; :: thesis: x = y

reconsider x = x, y = y as Element of NAT by A123, A124;

A126: f1 . y = ((f2 . y) * p) + ((f1 mod p) . y) by A97, A101, A124;

f1 . x = ((f2 . x) * p) + ((f1 mod p) . 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

then len (f1 mod p) = card (rng (f1 mod p)) by FINSEQ_4:62;

then A128: len (Sgm (rng (f1 mod p))) = (p -' 1) div 2 by A18, A96, A99, A108, FINSEQ_3:39, XBOOLE_1:73;

A129: (Sgm (rng (g1 mod q))) | nn = Sgm YY by A92, A94, FINSEQ_3:113, FINSEQ_6:10;

A130: (Sgm (rng (g1 mod q))) | nn is one-to-one by A48, A81, FINSEQ_3:91;

A131: Lege (p,q) = (- 1) |^ (Sum g2)

proof

for d being Nat st d in dom (idseq ((p -' 1) div 2)) holds
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));

A132: (Sgm (rng (g1 mod q))) /^ nn is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

A133: len ((Sgm (rng (g1 mod q))) | nn) = nn by A67, FINSEQ_1:59, XREAL_1:43;

A134: len ((Sgm (rng (g1 mod q))) /^ nn) = (len (Sgm (rng (g1 mod q)))) -' nn by RFINSEQ:29

.= (len (Sgm (rng (g1 mod q)))) - nn by A67, XREAL_1:43, XREAL_1:233

.= card XX by A67 ;

A135: 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

.= (dom ((Sgm (rng (g1 mod q))) /^ nn)) /\ (dom ((Sgm (rng (g1 mod q))) /^ nn)) by FINSEQ_1:def 3, A134, CARD_1:def 7

.= dom ((Sgm (rng (g1 mod q))) /^ nn) ;

then A136: len (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) = len ((Sgm (rng (g1 mod q))) /^ nn) by FINSEQ_3:29;

A137: 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)

( (((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 )

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

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:75;

A148: g6 is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

A149: nn <= len (Sgm (rng (g1 mod q))) by A67, XREAL_1:43;

A150: rng ((Sgm (rng (g1 mod q))) | nn) misses rng g5

g5 . d <> g5 . e

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 )

len g6 = (len ((Sgm (rng (g1 mod q))) | 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, A148, A181, RFINSEQ:9, RFINSEQ:26

.= (Sum ((Sgm (rng (g1 mod q))) | nn)) + (Sum g5) by RVSUM_1:75

.= (Sum ((Sgm (rng (g1 mod q))) | nn)) + (((card XX) * q) - (Sum ((Sgm (rng (g1 mod q))) /^ nn))) by A134, A132, 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 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 EULER_1:12 ;

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;set g6 = ((Sgm (rng (g1 mod q))) | nn) ^ (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn));

A132: (Sgm (rng (g1 mod q))) /^ nn is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

A133: len ((Sgm (rng (g1 mod q))) | nn) = nn by A67, FINSEQ_1:59, XREAL_1:43;

A134: len ((Sgm (rng (g1 mod q))) /^ nn) = (len (Sgm (rng (g1 mod q)))) -' nn by RFINSEQ:29

.= (len (Sgm (rng (g1 mod q)))) - nn by A67, XREAL_1:43, XREAL_1:233

.= card XX by A67 ;

A135: 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

.= (dom ((Sgm (rng (g1 mod q))) /^ nn)) /\ (dom ((Sgm (rng (g1 mod q))) /^ nn)) by FINSEQ_1:def 3, A134, CARD_1:def 7

.= dom ((Sgm (rng (g1 mod q))) /^ nn) ;

then A136: len (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) = len ((Sgm (rng (g1 mod q))) /^ nn) by FINSEQ_3:29;

A137: 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

A139:
for d being Nat st d in dom (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) holds
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 A138: 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 A134, A135, FINSEQ_1:def 3;

then ((card XX) |-> q) . d = q by FINSEQ_2:57;

hence (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d = q - (((Sgm (rng (g1 mod q))) /^ nn) . d) by A138, VALUED_1:13; :: thesis: verum

end;assume A138: 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 A134, A135, FINSEQ_1:def 3;

then ((card XX) |-> q) . d = q by FINSEQ_2:57;

hence (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d = q - (((Sgm (rng (g1 mod q))) /^ nn) . d) by A138, VALUED_1:13; :: thesis: verum

( (((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

A146:
rng (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) c= INT
by RELAT_1:def 19;
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 A140: 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 A95, A135, FUNCT_1:3;

then (Sgm XX) . d in XX by A79, FINSEQ_1:def 13;

then A141: 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

A142: e in dom (g1 mod q) and

A143: (g1 mod q) . e = ((Sgm (rng (g1 mod q))) /^ nn) . d by A95, FINSEQ_2:10;

((Sgm (rng (g1 mod q))) /^ nn) . d = (g1 . e) mod q by A25, A142, A143, EULER_2:def 1;

then A144: ((Sgm (rng (g1 mod q))) /^ nn) . d < q by NAT_D:1;

A145: (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d = q - (((Sgm (rng (g1 mod q))) /^ nn) . d) by A137, A140;

then w < q - (q / 2) by A95, A141, XREAL_1:10;

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, A145, A144, INT_1:54, XREAL_1:50; :: thesis: verum

end;reconsider w = (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d as Element of INT by INT_1:def 2;

assume A140: 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 A95, A135, FUNCT_1:3;

then (Sgm XX) . d in XX by A79, FINSEQ_1:def 13;

then A141: 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

A142: e in dom (g1 mod q) and

A143: (g1 mod q) . e = ((Sgm (rng (g1 mod q))) /^ nn) . d by A95, FINSEQ_2:10;

((Sgm (rng (g1 mod q))) /^ nn) . d = (g1 . e) mod q by A25, A142, A143, EULER_2:def 1;

then A144: ((Sgm (rng (g1 mod q))) /^ nn) . d < q by NAT_D:1;

A145: (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d = q - (((Sgm (rng (g1 mod q))) /^ nn) . d) by A137, A140;

then w < q - (q / 2) by A95, A141, XREAL_1:10;

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, A145, A144, INT_1:54, XREAL_1:50; :: thesis: verum

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

then reconsider g5 = ((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn) as FinSequence of NAT by FINSEQ_2:12;
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 A147: 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

(((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d > 0 by A139, A147;

hence (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d in NAT by A146, INT_1:3; :: thesis: verum

end;assume A147: 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

(((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d > 0 by A139, A147;

hence (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d in NAT by A146, INT_1:3; :: thesis: verum

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:75;

A148: g6 is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

A149: nn <= len (Sgm (rng (g1 mod q))) by A67, XREAL_1:43;

A150: rng ((Sgm (rng (g1 mod q))) | nn) misses rng g5

proof

for d, e being Nat st 1 <= d & d < e & e <= len g5 holds
assume
not rng ((Sgm (rng (g1 mod q))) | nn) misses rng g5
; :: thesis: contradiction

then consider x being object such that

A151: x in rng ((Sgm (rng (g1 mod q))) | 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 (g1 mod q))) /^ nn) . e) by A137, A153, A154;

then A155: x = q - ((Sgm (rng (g1 mod q))) . (e + nn)) by A149, A135, A153, RFINSEQ:def 1;

e + nn in dom (Sgm (rng (g1 mod q))) by A135, A153, FINSEQ_5:26;

then consider e1 being Nat such that

A156: e1 in dom (g1 mod q) and

A157: (g1 mod q) . e1 = (Sgm (rng (g1 mod q))) . (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 (g1 mod q))) | nn) c= rng (Sgm (rng (g1 mod q))) by FINSEQ_5:19;

then consider d1 being Nat such that

A159: d1 in dom (g1 mod q) and

A160: (g1 mod q) . 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 (g1 mod q))) . (e + nn) = (g1 . e1) mod q by A157, EULER_2:def 1;

A164: d1 in dom g1 by A24, A159, FINSEQ_3:29;

then x = (g1 . d1) mod q by A160, EULER_2:def 1;

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 EULER_2:6;

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;then consider x being object such that

A151: x in rng ((Sgm (rng (g1 mod q))) | 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 (g1 mod q))) /^ nn) . e) by A137, A153, A154;

then A155: x = q - ((Sgm (rng (g1 mod q))) . (e + nn)) by A149, A135, A153, RFINSEQ:def 1;

e + nn in dom (Sgm (rng (g1 mod q))) by A135, A153, FINSEQ_5:26;

then consider e1 being Nat such that

A156: e1 in dom (g1 mod q) and

A157: (g1 mod q) . e1 = (Sgm (rng (g1 mod q))) . (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 (g1 mod q))) | nn) c= rng (Sgm (rng (g1 mod q))) by FINSEQ_5:19;

then consider d1 being Nat such that

A159: d1 in dom (g1 mod q) and

A160: (g1 mod q) . 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 (g1 mod q))) . (e + nn) = (g1 . e1) mod q by A157, EULER_2:def 1;

A164: d1 in dom g1 by A24, A159, FINSEQ_3:29;

then x = (g1 . d1) mod q by A160, EULER_2:def 1;

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 EULER_2:6;

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

g5 . d <> g5 . e

proof

then
len g5 = card (rng g5)
by GRAPH_5:7;
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 (g1 mod q))) /^ 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 (g1 mod q))) /^ nn) . d) by A137;

hence g5 . d <> g5 . e by A82, A135, A167, A171, A169, A170; :: thesis: verum

end;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 (g1 mod q))) /^ 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 (g1 mod q))) /^ nn) . d) by A137;

hence g5 . d <> g5 . e by A82, A135, A167, A171, A169, A170; :: thesis: verum

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

A181:
idseq ((q -' 1) div 2) is FinSequence of REAL
by RVSUM_1:145;
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 )

end;assume A174: 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 A174, FINSEQ_1:25;

end;

( l in dom g5 & d = (len ((Sgm (rng (g1 mod q))) | nn)) + l ) ) by A174, FINSEQ_1:25;

suppose A175:
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 A129, FUNCT_1:3;

then A176: ((Sgm (rng (g1 mod q))) | nn) . d in YY by A87, FINSEQ_1:def 13;

then A177: ((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 A176, XBOOLE_0:def 5;

then ((Sgm (rng (g1 mod q))) | nn) . d <= q / 2 by A177;

then A178: ((Sgm (rng (g1 mod q))) | nn) . d <= (q -' 1) div 2 by A83, INT_1:54;

not ((Sgm (rng (g1 mod q))) | nn) . d in {0} by A47, A78, A177, 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 A175, A178, FINSEQ_1:def 7; :: thesis: verum

end;then A176: ((Sgm (rng (g1 mod q))) | nn) . d in YY by A87, FINSEQ_1:def 13;

then A177: ((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 A176, XBOOLE_0:def 5;

then ((Sgm (rng (g1 mod q))) | nn) . d <= q / 2 by A177;

then A178: ((Sgm (rng (g1 mod q))) | nn) . d <= (q -' 1) div 2 by A83, INT_1:54;

not ((Sgm (rng (g1 mod q))) | nn) . d in {0} by A47, A78, A177, 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 A175, A178, FINSEQ_1:def 7; :: thesis: verum

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 )

( 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

A179: l in dom g5 and

A180: d = (len ((Sgm (rng (g1 mod q))) | 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;A179: l in dom g5 and

A180: d = (len ((Sgm (rng (g1 mod q))) | 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

len g6 = (len ((Sgm (rng (g1 mod q))) | 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, A148, A181, RFINSEQ:9, RFINSEQ:26

.= (Sum ((Sgm (rng (g1 mod q))) | nn)) + (Sum g5) by RVSUM_1:75

.= (Sum ((Sgm (rng (g1 mod q))) | nn)) + (((card XX) * q) - (Sum ((Sgm (rng (g1 mod q))) /^ nn))) by A134, A132, 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 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 EULER_1:12 ;

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

(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 (f1 mod p))) & k > p / 2 ) } ;

for x being object 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

then A184:
{ 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)))
;
let x be object ; :: 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;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

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

dom (p * f2) = dom f2
by VALUED_1:def 5;
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_{3}( 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_{3}(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_{3}(x,y)
from FUNCT_7:sch 1(A187);

defpred S_{1}[ 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_{1}[d,x1]

A190: ( dom Pr = Seg ((p -' 1) div 2) & ( for d being Nat st d in Seg ((p -' 1) div 2) holds

S_{1}[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

defpred S_{2}[ 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_{2}[d,x1]

A218: ( dom Pk = Seg ((q -' 1) div 2) & ( for d being Nat st d in Seg ((q -' 1) div 2) holds

S_{2}[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

dom z c= U1 \/ U2

A253: U1 misses U2

Pk . d misses Pk . e

A277: for d, e being Nat st d in dom Pr & e in dom Pr & d <> e holds

Pr . d misses Pr . e

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;deffunc H

A187: for x being Element of A

for y being Element of B holds H

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

defpred S

( $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

proof

consider Pr being FinSequence of bool (dom z) such that
let d be Nat; :: thesis: ( d in Seg ((p -' 1) div 2) implies ex x1 being Element of bool (dom z) st S_{1}[d,x1] )

assume d in Seg ((p -' 1) div 2) ; :: thesis: ex x1 being Element of bool (dom z) st S_{1}[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_{1}[d,x1] )

x1 c= dom z_{1}[d,x1] )
; :: thesis: verum

end;assume d in Seg ((p -' 1) div 2) ; :: thesis: ex x1 being Element of bool (dom z) st S

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

x1 c= dom z

proof

hence
( x1 is Element of bool (dom z) & S
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;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

A190: ( dom Pr = Seg ((p -' 1) div 2) & ( for d being Nat st d in Seg ((p -' 1) div 2) holds

S

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

then A216:
Card Pr = f2
by A191;
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)):]

.= 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;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

then card (Pr . d) =
card [:(Seg (f2 . m)),{m}:]
by CARD_2:4
set L = [:{m},(Seg (f2 . m)):];

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

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

proof

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

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 ;

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)):]
now :: thesis: not q mod p = 0

then A197:
- (q div p) = ((- q) div p) + 1
by WSIERP_1:41;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 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

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
end;

m <= (p -' 1) div 2
by FINSEQ_1:1;per cases
( (q div p) mod 2 = 0 or (q div p) mod 2 <> 0 )
;

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)
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;.= - (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

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;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

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

then A205:
[\((m * q) / p)/] < (m * q) / p
by INT_1:26;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 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

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

proof

hence
Pr . d = [:{m},(Seg (f2 . m)):]
by A195, XBOOLE_0:def 10; :: thesis: verum
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;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

.= 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

defpred S

( $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

proof

consider Pk being FinSequence of bool (dom z) such that
let d be Nat; :: thesis: ( d in Seg ((q -' 1) div 2) implies ex x1 being Element of bool (dom z) st S_{2}[d,x1] )

assume d in Seg ((q -' 1) div 2) ; :: thesis: ex x1 being Element of bool (dom z) st S_{2}[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_{2}[d,x1] )

x1 c= dom z_{2}[d,x1] )
; :: thesis: verum

end;assume d in Seg ((q -' 1) div 2) ; :: thesis: ex x1 being Element of bool (dom z) st S

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

x1 c= dom z

proof

hence
( x1 is Element of bool (dom z) & S
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;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

A218: ( dom Pk = Seg ((q -' 1) div 2) & ( for d being Nat st d in Seg ((q -' 1) div 2) holds

S

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

reconsider U1 = union (rng Pr), U2 = union (rng Pk) as finite Subset of (dom z) by PROB_3:48;
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}:]

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;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

then
card (Pk . d) = card (Seg (g2 . n))
by CARD_1:69;
set L = [:(Seg (g2 . n)),{n}:];

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

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

proof

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

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;

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}:]
now :: thesis: not p mod q = 0

then A226:
- (p div q) = ((- p) div q) + 1
by WSIERP_1:41;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 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

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
end;

n in Seg ((q -' 1) div 2)
;per cases
( (p div q) mod 2 = 0 or (p div q) mod 2 <> 0 )
;

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)
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;.= - (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

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;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

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

then
[\((n * p) / q)/] < (n * p) / q
by INT_1:26;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 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

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

proof

hence
Pk . d = [:(Seg (g2 . n)),{n}:]
by A224, XBOOLE_0:def 10; :: thesis: verum
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;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

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

dom z c= U1 \/ U2

proof

then A252:
U1 \/ U2 = dom z
by XBOOLE_0:def 10;
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

end;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;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

A253: U1 misses U2

proof

A265:
for d, e being Nat st d in dom Pk & e in dom Pk & d <> e holds
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;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

Pk . d misses Pk . e

proof

A276:
card (union (rng Pk)) = Sum (Card Pk)
by A265, Th48;
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;

end;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

hence
Pk . d misses Pk . e
; :: thesis: verumassume
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;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

A277: for d, e being Nat st d in dom Pr & e in dom Pr & d <> e holds

Pr . d misses Pr . e

proof

card (union (rng Pr)) = Sum (Card Pr)
by A277, Th48;
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;

end;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

hence
Pr . d misses Pr . e
; :: thesis: verumassume
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;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

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

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 (f1 mod p))) & k > p / 2 ) } as finite Subset of NAT by A184, XBOOLE_1:1;

set m = card X;

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

A291: f1 mod p is Element of NAT * by FINSEQ_1:def 11;

len (f1 mod p) = (p -' 1) div 2 by A17, A96, CARD_1:def 7;

then f1 mod p in ((p -' 1) div 2) -tuples_on NAT by A291;

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

A293: rng (f1 mod p) c= Seg n1 by A99, A108, XBOOLE_1:73;

then A294: rng (Sgm (rng (f1 mod p))) = rng (f1 mod p) by FINSEQ_1:def 13;

then A295: X c= Seg n1 by A293, A184;

A296: 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 A97, A100 ;

for d being Nat st d in dom f1 holds

f1 . d = ((p * f2) + (f1 mod p)) . d

proof

then
f1 = (p * f2) + (f1 mod p)
by A296;
let d be Nat; :: thesis: ( d in dom f1 implies f1 . d = ((p * f2) + (f1 mod p)) . d )

assume A297: d in dom f1 ; :: thesis: f1 . d = ((p * f2) + (f1 mod p)) . d

then A298: d in dom (p * f2) by A100, VALUED_1:def 5;

((p * f2) + (f1 mod p)) . d = ((p * f2) . d) + ((f1 mod p) . d) by A296, A297, VALUED_1:def 1;

hence ((p * f2) + (f1 mod p)) . d = (p * (f2 . d)) + ((f1 mod p) . d) by A298, VALUED_1:def 5

.= f1 . d by A101, A297 ;

:: thesis: verum

end;assume A297: d in dom f1 ; :: thesis: f1 . d = ((p * f2) + (f1 mod p)) . d

then A298: d in dom (p * f2) by A100, VALUED_1:def 5;

((p * f2) + (f1 mod p)) . d = ((p * f2) . d) + ((f1 mod p) . d) by A296, A297, VALUED_1:def 1;

hence ((p * f2) + (f1 mod p)) . d = (p * (f2 . d)) + ((f1 mod p) . d) by A298, VALUED_1:def 5

.= f1 . d by A101, A297 ;

:: thesis: verum

then A299: Sum f1 = (Sum (p * f2)) + (Sum (f1 mod p)) by A289, A292, RVSUM_1:89

.= (p * (Sum f2)) + (Sum (f1 mod p)) by RVSUM_1:87 ;

A300: (rng (Sgm (rng (f1 mod p)))) \ X c= rng (Sgm (rng (f1 mod p))) by XBOOLE_1:36;

then A301: Y c= Seg n1 by A293, A294;

A302: len (f1 mod p) = card (rng (Sgm (rng (f1 mod p)))) 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 (f1 mod p)) = ((Sgm (rng (f1 mod p))) | n) ^ ((Sgm (rng (f1 mod p))) /^ n) by RFINSEQ:8;

then A304: (Sgm (rng (f1 mod p))) /^ n is one-to-one by A109, FINSEQ_3:91;

A305: f1 mod p is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

Sgm (rng (f1 mod p)) is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

then A306: Sum (Sgm (rng (f1 mod p))) = Sum (f1 mod p) by A127, A294, A109, RFINSEQ:9, RFINSEQ:26, A305;

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

k < l

proof

then
Sgm (Y \/ X) = (Sgm Y) ^ (Sgm X)
by A295, A301, FINSEQ_3:42;
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 (f1 mod p))) & l1 > p / 2 ) by A308;

k in rng (Sgm (rng (f1 mod p))) by A307, XBOOLE_0:def 5;

then k <= p / 2 by A309;

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

end;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 (f1 mod p))) & l1 > p / 2 ) by A308;

k in rng (Sgm (rng (f1 mod p))) by A307, XBOOLE_0:def 5;

then k <= p / 2 by A309;

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

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

then A311: Sgm (rng (f1 mod p)) = (Sgm Y) ^ (Sgm X) by A294, A184, XBOOLE_1:12;

then Sum (Sgm (rng (f1 mod p))) = (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 A293, A294, A300, FINSEQ_3:39, XBOOLE_1:1

.= ((p -' 1) div 2) - (card X) by A18, A96, A184, A302, CARD_2:44 ;

then A314: (Sgm (rng (f1 mod p))) /^ n = Sgm X by A311, FINSEQ_5:37;

A315: (Sgm (rng (f1 mod p))) | n = Sgm Y by A311, A313, FINSEQ_3:113, FINSEQ_6:10;

A316: (Sgm (rng (f1 mod p))) | n is one-to-one by A109, A303, FINSEQ_3:91;

Lege (q,p) = (- 1) |^ (Sum f2)

proof

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

A317: (Sgm (rng (f1 mod p))) /^ n is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

A318: len ((Sgm (rng (f1 mod p))) | n) = n by A128, FINSEQ_1:59, XREAL_1:43;

A319: len ((Sgm (rng (f1 mod p))) /^ n) = (len (Sgm (rng (f1 mod p)))) -' n by RFINSEQ:29

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

.= card X by A128 ;

A320: 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

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

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

then A321: len (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) = len ((Sgm (rng (f1 mod p))) /^ n) by FINSEQ_3:29;

A322: 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)

( (((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 )

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

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:75;

A333: f6 is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

A334: n <= len (Sgm (rng (f1 mod p))) by A128, XREAL_1:43;

A335: rng ((Sgm (rng (f1 mod p))) | n) misses rng f5

f5 . d <> f5 . e

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 )

len f6 = (len ((Sgm (rng (f1 mod p))) | 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 A363, A354, A333, RFINSEQ:9, RFINSEQ:26

.= (Sum ((Sgm (rng (f1 mod p))) | n)) + (Sum f5) by RVSUM_1:75

.= (Sum ((Sgm (rng (f1 mod p))) | n)) + (((card X) * p) - (Sum ((Sgm (rng (f1 mod p))) /^ n))) by A319, A317, 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 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 EULER_1:12 ;

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;set f6 = ((Sgm (rng (f1 mod p))) | n) ^ (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n));

A317: (Sgm (rng (f1 mod p))) /^ n is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

A318: len ((Sgm (rng (f1 mod p))) | n) = n by A128, FINSEQ_1:59, XREAL_1:43;

A319: len ((Sgm (rng (f1 mod p))) /^ n) = (len (Sgm (rng (f1 mod p)))) -' n by RFINSEQ:29

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

.= card X by A128 ;

A320: 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

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

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

then A321: len (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) = len ((Sgm (rng (f1 mod p))) /^ n) by FINSEQ_3:29;

A322: 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

A324:
for d being Nat st d in dom (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) holds
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 A323: 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 A319, A320, FINSEQ_1:def 3;

then ((card X) |-> p) . d = p by FINSEQ_2:57;

hence (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d = p - (((Sgm (rng (f1 mod p))) /^ n) . d) by A323, VALUED_1:13; :: thesis: verum

end;assume A323: 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 A319, A320, FINSEQ_1:def 3;

then ((card X) |-> p) . d = p by FINSEQ_2:57;

hence (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d = p - (((Sgm (rng (f1 mod p))) /^ n) . d) by A323, VALUED_1:13; :: thesis: verum

( (((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

A331:
rng (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) c= INT
by RELAT_1:def 19;
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 A325: 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 A314, A320, FUNCT_1:3;

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

then A326: ex ll being Element of NAT st

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

then consider e being Nat such that

A327: e in dom (f1 mod p) and

A328: (f1 mod p) . e = ((Sgm (rng (f1 mod p))) /^ n) . d by A314, FINSEQ_2:10;

((Sgm (rng (f1 mod p))) /^ n) . d = (f1 . e) mod p by A97, A327, A328, EULER_2:def 1;

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

A330: (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d = p - (((Sgm (rng (f1 mod p))) /^ n) . d) by A322, A325;

then w < p - (p / 2) by A314, A326, XREAL_1:10;

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 A290, A330, A329, INT_1:54, XREAL_1:50; :: thesis: verum

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

assume A325: 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 A314, A320, FUNCT_1:3;

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

then A326: ex ll being Element of NAT st

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

then consider e being Nat such that

A327: e in dom (f1 mod p) and

A328: (f1 mod p) . e = ((Sgm (rng (f1 mod p))) /^ n) . d by A314, FINSEQ_2:10;

((Sgm (rng (f1 mod p))) /^ n) . d = (f1 . e) mod p by A97, A327, A328, EULER_2:def 1;

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

A330: (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d = p - (((Sgm (rng (f1 mod p))) /^ n) . d) by A322, A325;

then w < p - (p / 2) by A314, A326, XREAL_1:10;

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 A290, A330, A329, INT_1:54, XREAL_1:50; :: thesis: verum

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

then reconsider f5 = ((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n) as FinSequence of NAT by FINSEQ_2:12;
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 A332: 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

(((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d > 0 by A332, A324;

hence (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d in NAT by A331, INT_1:3; :: thesis: verum

end;assume A332: 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

(((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d > 0 by A332, A324;

hence (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d in NAT by A331, INT_1:3; :: thesis: verum

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:75;

A333: f6 is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

A334: n <= len (Sgm (rng (f1 mod p))) by A128, XREAL_1:43;

A335: rng ((Sgm (rng (f1 mod p))) | n) misses rng f5

proof

for d, e being Nat st 1 <= d & d < e & e <= len f5 holds
assume
not rng ((Sgm (rng (f1 mod p))) | n) misses rng f5
; :: thesis: contradiction

then consider x being object such that

A336: x in rng ((Sgm (rng (f1 mod p))) | 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 (f1 mod p))) /^ n) . e) by A322, A338, A339;

then A340: x = p - ((Sgm (rng (f1 mod p))) . (e + n)) by A334, A320, A338, RFINSEQ:def 1;

e + n in dom (Sgm (rng (f1 mod p))) by A320, A338, FINSEQ_5:26;

then consider e1 being Nat such that

A341: e1 in dom (f1 mod p) and

A342: (f1 mod p) . e1 = (Sgm (rng (f1 mod p))) . (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 (f1 mod p))) | n) c= rng (Sgm (rng (f1 mod p))) by FINSEQ_5:19;

then consider d1 being Nat such that

A344: d1 in dom (f1 mod p) and

A345: (f1 mod p) . 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 1;

then ((f1 . d1) mod p) + ((Sgm (rng (f1 mod p))) . (e + n)) = p by A340;

then ((f1 . d1) mod p) + ((f1 . e1) mod p) = p by A97, A341, A342, 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:6;

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;then consider x being object such that

A336: x in rng ((Sgm (rng (f1 mod p))) | 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 (f1 mod p))) /^ n) . e) by A322, A338, A339;

then A340: x = p - ((Sgm (rng (f1 mod p))) . (e + n)) by A334, A320, A338, RFINSEQ:def 1;

e + n in dom (Sgm (rng (f1 mod p))) by A320, A338, FINSEQ_5:26;

then consider e1 being Nat such that

A341: e1 in dom (f1 mod p) and

A342: (f1 mod p) . e1 = (Sgm (rng (f1 mod p))) . (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 (f1 mod p))) | n) c= rng (Sgm (rng (f1 mod p))) by FINSEQ_5:19;

then consider d1 being Nat such that

A344: d1 in dom (f1 mod p) and

A345: (f1 mod p) . 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 1;

then ((f1 . d1) mod p) + ((Sgm (rng (f1 mod p))) . (e + n)) = p by A340;

then ((f1 . d1) mod p) + ((f1 . e1) mod p) = p by A97, A341, A342, 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:6;

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

f5 . d <> f5 . e

proof

then
len f5 = card (rng f5)
by GRAPH_5:7;
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 (f1 mod p))) /^ 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 (f1 mod p))) /^ n) . d) by A322;

hence f5 . d <> f5 . e by A304, A320, A349, A353, A351, A352; :: thesis: verum

end;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 (f1 mod p))) /^ 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 (f1 mod p))) /^ n) . d) by A322;

hence f5 . d <> f5 . e by A304, A320, A349, A353, A351, A352; :: thesis: verum

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

A363:
idseq ((p -' 1) div 2) is FinSequence of REAL
by RVSUM_1:145;
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 )

end;assume A356: 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 A356, FINSEQ_1:25;

end;

( l in dom f5 & d = (len ((Sgm (rng (f1 mod p))) | n)) + l ) ) by A356, FINSEQ_1:25;

suppose A357:
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 A315, FUNCT_1:3;

then A358: ((Sgm (rng (f1 mod p))) | n) . d in Y by A301, FINSEQ_1:def 13;

then A359: ((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 A358, XBOOLE_0:def 5;

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

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

not ((Sgm (rng (f1 mod p))) | n) . d in {0} by A108, A294, A359, 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 A357, A360, FINSEQ_1:def 7; :: thesis: verum

end;then A358: ((Sgm (rng (f1 mod p))) | n) . d in Y by A301, FINSEQ_1:def 13;

then A359: ((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 A358, XBOOLE_0:def 5;

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

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

not ((Sgm (rng (f1 mod p))) | n) . d in {0} by A108, A294, A359, 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 A357, A360, FINSEQ_1:def 7; :: thesis: verum

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 )

( 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

A361: l in dom f5 and

A362: d = (len ((Sgm (rng (f1 mod p))) | 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;A361: l in dom f5 and

A362: d = (len ((Sgm (rng (f1 mod p))) | 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

len f6 = (len ((Sgm (rng (f1 mod p))) | 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 A363, A354, A333, RFINSEQ:9, RFINSEQ:26

.= (Sum ((Sgm (rng (f1 mod p))) | n)) + (Sum f5) by RVSUM_1:75

.= (Sum ((Sgm (rng (f1 mod p))) | n)) + (((card X) * p) - (Sum ((Sgm (rng (f1 mod p))) /^ n))) by A319, A317, 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 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 EULER_1:12 ;

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