let p, q be Prime; :: thesis: ( p > 2 & q > 2 & p <> q implies (Lege (p,q)) * (Lege (q,p)) = (- 1) |^ (((p -' 1) div 2) * ((q -' 1) div 2)) )
assume that
A1: p > 2 and
A2: q > 2 and
A3: p <> q ; :: thesis: (Lege (p,q)) * (Lege (q,p)) = (- 1) |^ (((p -' 1) div 2) * ((q -' 1) div 2))
A4: q,p are_relative_prime by A3, INT_2: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;
not p is even by A1, PEPIN:17;
then A9: p -' 1 is even by A7, HILBERT3:2;
then A10: 2 divides p -' 1 by PEPIN:22;
then A11: p -' 1 = 2 * ((p -' 1) div 2) by NAT_D:3;
then (p -' 1) div 2 divides p -' 1 by NAT_D:def 3;
then (p -' 1) div 2 <= p -' 1 by A8, NAT_D:7;
then A12: (p -' 1) div 2 < p by A7, XREAL_1:146, XXREAL_0:2;
set f1 = q * (idseq ((p -' 1) div 2));
A13: for d being Nat st d in dom (q * (idseq ((p -' 1) div 2))) holds
(q * (idseq ((p -' 1) div 2))) . d = q * d
proof
let d be Nat; :: thesis: ( d in dom (q * (idseq ((p -' 1) div 2))) implies (q * (idseq ((p -' 1) div 2))) . d = q * d )
assume A14: d in dom (q * (idseq ((p -' 1) div 2))) ; :: thesis: (q * (idseq ((p -' 1) div 2))) . d = q * d
then d in dom (idseq ((p -' 1) div 2)) by VALUED_1:def 5;
then d in Seg (len (idseq ((p -' 1) div 2))) by FINSEQ_1:def 3;
then A15: d is Element of Seg ((p -' 1) div 2) by CARD_1:def 7;
(q * (idseq ((p -' 1) div 2))) . d = q * ((idseq ((p -' 1) div 2)) . d) by A14, VALUED_1:def 5;
hence (q * (idseq ((p -' 1) div 2))) . d = q * d by A15, FINSEQ_2:49; :: thesis: verum
end;
A16: for d being Nat st d in dom (q * (idseq ((p -' 1) div 2))) holds
(q * (idseq ((p -' 1) div 2))) . d in NAT
proof
let d be Nat; :: thesis: ( d in dom (q * (idseq ((p -' 1) div 2))) implies (q * (idseq ((p -' 1) div 2))) . d in NAT )
assume d in dom (q * (idseq ((p -' 1) div 2))) ; :: thesis: (q * (idseq ((p -' 1) div 2))) . d in NAT
then (q * (idseq ((p -' 1) div 2))) . d = q * d by A13;
hence (q * (idseq ((p -' 1) div 2))) . d in NAT ; :: thesis: verum
end;
dom (q * (idseq ((p -' 1) div 2))) = dom (idseq ((p -' 1) div 2)) by VALUED_1:def 5;
then A17: len (q * (idseq ((p -' 1) div 2))) = len (idseq ((p -' 1) div 2)) by FINSEQ_3:29;
then A18: len (q * (idseq ((p -' 1) div 2))) = (p -' 1) div 2 by CARD_1:def 7;
set q9 = (q -' 1) div 2;
set g1 = p * (idseq ((q -' 1) div 2));
A19: for d being Nat st d in dom (p * (idseq ((q -' 1) div 2))) holds
(p * (idseq ((q -' 1) div 2))) . d = p * d
proof
let d be Nat; :: thesis: ( d in dom (p * (idseq ((q -' 1) div 2))) implies (p * (idseq ((q -' 1) div 2))) . d = p * d )
assume A20: d in dom (p * (idseq ((q -' 1) div 2))) ; :: thesis: (p * (idseq ((q -' 1) div 2))) . d = p * d
then d in dom (idseq ((q -' 1) div 2)) by VALUED_1:def 5;
then d in Seg (len (idseq ((q -' 1) div 2))) by FINSEQ_1:def 3;
then A21: d is Element of Seg ((q -' 1) div 2) by CARD_1:def 7;
(p * (idseq ((q -' 1) div 2))) . d = p * ((idseq ((q -' 1) div 2)) . d) by A20, VALUED_1:def 5;
hence (p * (idseq ((q -' 1) div 2))) . d = p * d by A21, FINSEQ_2:49; :: thesis: verum
end;
A22: for d being Nat st d in dom (p * (idseq ((q -' 1) div 2))) holds
(p * (idseq ((q -' 1) div 2))) . d in NAT
proof
let d be Nat; :: thesis: ( d in dom (p * (idseq ((q -' 1) div 2))) implies (p * (idseq ((q -' 1) div 2))) . d in NAT )
assume d in dom (p * (idseq ((q -' 1) div 2))) ; :: thesis: (p * (idseq ((q -' 1) div 2))) . d in NAT
then (p * (idseq ((q -' 1) div 2))) . d = p * d by A19;
hence (p * (idseq ((q -' 1) div 2))) . d in NAT ; :: thesis: verum
end;
dom (p * (idseq ((q -' 1) div 2))) = dom (idseq ((q -' 1) div 2)) by VALUED_1:def 5;
then len (p * (idseq ((q -' 1) div 2))) = len (idseq ((q -' 1) div 2)) by FINSEQ_3: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 set st x in { k where k is Element of NAT : ( k in rng (Sgm (rng (g1 mod q))) & k > q / 2 ) } holds
x in rng (Sgm (rng (g1 mod q)))
proof
let x be set ; :: thesis: ( x in { k where k is Element of NAT : ( k in rng (Sgm (rng (g1 mod q))) & k > q / 2 ) } implies x in rng (Sgm (rng (g1 mod q))) )
assume x in { k where k is Element of NAT : ( k in rng (Sgm (rng (g1 mod q))) & k > q / 2 ) } ; :: thesis: x in rng (Sgm (rng (g1 mod q)))
then ex k being Element of NAT st
( x = k & k in rng (Sgm (rng (g1 mod q))) & k > q / 2 ) ;
hence x in rng (Sgm (rng (g1 mod q))) ; :: thesis: verum
end;
then A26: { k where k is Element of NAT : ( k in rng (Sgm (rng (g1 mod q))) & k > q / 2 ) } c= rng (Sgm (rng (g1 mod q))) by TARSKI:def 3;
reconsider f1 = q * (idseq ((p -' 1) div 2)) as FinSequence of NAT by A16, FINSEQ_2:12;
deffunc H1( Nat) -> Element of NAT = (f1 . $1) div p;
consider f2 being FinSequence such that
A27: ( len f2 = (p -' 1) div 2 & ( for d being Nat st d in dom f2 holds
f2 . d = H1(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 by FINSEQ_1:def 4;
then consider n2 being Element of NAT such that
A32: rng (g1 mod q) c= (Seg n2) \/ {0} by HEYTING3:1;
deffunc H2( Nat) -> Element of NAT = (g1 . $1) div q;
consider g2 being FinSequence such that
A33: ( len g2 = (q -' 1) div 2 & ( for d being Nat st d in dom g2 holds
g2 . d = H2(d) ) ) from FINSEQ_1:sch 2();
 for d being Nat st d in dom g2 holds
g2 . d in NAT
proof
let d be Nat; :: thesis: ( d in dom g2 implies g2 . d in NAT )
assume d in dom g2 ; :: thesis: g2 . d in NAT
then g2 . d = (g1 . d) div q by A33;
hence g2 . d in NAT ; :: thesis: verum
end;
then reconsider g2 = g2 as FinSequence of NAT by FINSEQ_2:12;
A34: dom g1 = dom g2 by A23, A33, FINSEQ_3:29;
A35: for d being Nat st d in dom g1 holds
g1 . d = ((g2 . d) * q) + ((g1 mod q) . d)
proof
let d be Nat; :: thesis: ( d in dom g1 implies g1 . d = ((g2 . d) * q) + ((g1 mod q) . d) )
assume A36: d in dom g1 ; :: thesis: g1 . d = ((g2 . d) * q) + ((g1 mod q) . d)
then A37: (g1 mod q) . d = (g1 . d) mod q by EULER_2:def 1;
g2 . d = (g1 . d) div q by A33, A34, A36;
hence g1 . d = ((g2 . d) * q) + ((g1 mod q) . d) by A37, NAT_D:2; :: thesis: verum
end;
not q is even by A2, PEPIN:17;
then A38: q -' 1 is even by A29, HILBERT3:2;
then A39: 2 divides q -' 1 by PEPIN:22;
then A40: q -' 1 = 2 * ((q -' 1) div 2) by NAT_D:3;
then (q -' 1) div 2 divides q -' 1 by NAT_D:def 3;
then (q -' 1) div 2 <= q -' 1 by A30, NAT_D:7;
then A41: (q -' 1) div 2 < q by A29, XREAL_1:146, XXREAL_0:2;
not 0 in rng (g1 mod q)
proof
assume 0 in rng (g1 mod q) ; :: thesis: contradiction
then consider a being Nat such that
A42: a in dom (g1 mod q) and
A43: (g1 mod q) . a = 0 by FINSEQ_2: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 by NAT_D:def 3;
a >= 1 by A42, FINSEQ_3:25;
then A46: q <= a by A4, A45, NAT_D:7, PEPIN:3;
a <= (q -' 1) div 2 by A23, A24, A42, FINSEQ_3:25;
hence contradiction by A41, A46, XXREAL_0:2; :: thesis: verum
end;
then A47: {0} misses rng (g1 mod q) by ZFMISC_1:50;
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
A50: q,p are_relative_prime by A3, INT_2:30;
let d, e be Nat; :: thesis: ( d in dom g1 & e in dom g1 & q divides (g1 . d) - (g1 . e) implies d = e )
assume that
A51: d in dom g1 and
A52: e in dom g1 and
A53: q divides (g1 . d) - (g1 . e) ; :: thesis: d = e
A54: g1 . e = p * e by A19, A52;
g1 . d = p * d by A19, A51;
then A55: q divides (d - e) * p by A53, A54;
now
assume d <> e ; :: thesis: contradiction
then d - e <> 0 ;
then abs q <= abs (d - e) by A55, A50, INT_2:25, INT_4:6;
then A56: q <= abs (d - e) by ABSVALUE:def 1;
A57: e >= 1 by A52, FINSEQ_3:25;
A58: d >= 1 by A51, FINSEQ_3:25;
e <= (q -' 1) div 2 by A23, A52, FINSEQ_3:25;
then A59: d - e >= 1 - ((q -' 1) div 2) by A58, XREAL_1:13;
A60: ((q -' 1) div 2) - 1 < q by A41, XREAL_1:147;
d <= (q -' 1) div 2 by A23, A51, FINSEQ_3:25;
then d - e <= ((q -' 1) div 2) - 1 by A57, XREAL_1:13;
then A61: d - e < q by A60, XXREAL_0:2;
- (((q -' 1) div 2) - 1) > - q by A60, XREAL_1:24;
then d - e > - q by A59, XXREAL_0:2;
hence contradiction by A56, A61, SEQ_2:1; :: thesis: verum
end;
hence d = e ; :: thesis: verum
end;
for x, y being set st x in dom (g1 mod q) & y in dom (g1 mod q) & (g1 mod q) . x = (g1 mod q) . y holds
x = y
proof
let x, y be set ; :: thesis: ( x in dom (g1 mod q) & y in dom (g1 mod q) & (g1 mod q) . x = (g1 mod q) . y implies x = y )
assume that
A62: x in dom (g1 mod q) and
A63: y in dom (g1 mod q) and
A64: (g1 mod q) . x = (g1 mod q) . y ; :: thesis: x = y
reconsider x = x, y = y as Element of NAT by A62, A63;
A65: g1 . y = ((g2 . y) * q) + ((g1 mod q) . y) by A25, A35, A63;
g1 . x = ((g2 . x) * q) + ((g1 mod q) . x) by A25, A35, A62;
then (g1 . x) - (g1 . y) = ((g2 . x) - (g2 . y)) * q by A64, A65;
then q divides (g1 . x) - (g1 . y) by INT_1:def 3;
hence x = y by A49, A25, A62, A63; :: thesis: verum
end;
then A66: g1 mod q is one-to-one by FUNCT_1:def 4;
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;
for d being Nat st d in dom (idseq ((q -' 1) div 2)) holds
(idseq ((q -' 1) div 2)) . d in NAT by ORDINAL1:def 12;
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_relative_prime 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;
A73: dom ((q * g2) + (g1 mod q)) = (dom (q * g2)) /\ (dom (g1 mod q)) by VALUED_1:def 1
.= (dom g2) /\ (dom (g1 mod q)) by VALUED_1:def 5
.= dom g1 by A25, A34 ;
for d being Nat st d in dom g1 holds
g1 . d = ((q * g2) + (g1 mod q)) . d
proof
let d be Nat; :: thesis: ( d in dom g1 implies g1 . d = ((q * g2) + (g1 mod q)) . d )
assume A74: d in dom g1 ; :: thesis: g1 . d = ((q * g2) + (g1 mod q)) . d
then A75: d in dom (q * g2) by A34, VALUED_1:def 5;
((q * g2) + (g1 mod q)) . d = ((q * g2) . d) + ((g1 mod q) . d) by A73, A74, VALUED_1:def 1;
hence ((q * g2) + (g1 mod q)) . d = (q * (g2 . d)) + ((g1 mod q) . d) by A75, VALUED_1:def 5
.= g1 . d by A35, A74 ;
:: thesis: verum
end;
then g1 = (q * g2) + (g1 mod q) by A73, FINSEQ_1:13;
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, XBOOLE_1:1;
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 ;
Sgm (rng (g1 mod q)) is FinSequence of REAL by FINSEQ_2:24;
then A84: Sum (Sgm (rng (g1 mod q))) = Sum (g1 mod q) by A66, A78, A48, RFINSEQ:9, RFINSEQ:26;
A85: (rng (Sgm (rng (g1 mod q)))) \ XX c= rng (Sgm (rng (g1 mod q))) by XBOOLE_1:36;
then A86: YY c= Seg n2 by A77, A78, XBOOLE_1:1;
for k, l being Element of NAT st k in YY & l in XX holds
k < l
proof
let k, l be Element of NAT ; :: thesis: ( k in YY & l in XX implies k < l )
assume that
A87: k in YY and
A88: l in XX ; :: thesis: k < l
A89: not k in XX by A87, XBOOLE_0:def 5;
A90: ex l1 being Element of NAT st
( l1 = l & l1 in rng (Sgm (rng (g1 mod q))) & l1 > q / 2 ) by A88;
k in rng (Sgm (rng (g1 mod q))) by A87, XBOOLE_0:def 5;
then k <= q / 2 by A89;
hence k < l by A90, XXREAL_0:2; :: thesis: verum
end;
then Sgm (YY \/ XX) = (Sgm YY) ^ (Sgm XX) by A86, A79, FINSEQ_3:42;
then Sgm ((rng (Sgm (rng (g1 mod q)))) \/ XX) = (Sgm YY) ^ (Sgm XX) by XBOOLE_1:39;
then A91: Sgm (rng (g1 mod q)) = (Sgm YY) ^ (Sgm XX) by A78, A26, XBOOLE_1:12;
then Sum (Sgm (rng (g1 mod q))) = (Sum (Sgm YY)) + (Sum (Sgm XX)) by RVSUM_1:75;
then A92: p * (Sum (idseq ((q -' 1) div 2))) = ((q * (Sum g2)) + (Sum (Sgm YY))) + (Sum (Sgm XX)) by A76, A84, RVSUM_1:87;
A93: len (Sgm YY) = card YY by A77, A78, A85, FINSEQ_3:39, XBOOLE_1:1
.= ((q -' 1) div 2) - (card XX) by A23, A24, A26, A80, CARD_2:44 ;
then A94: (Sgm (rng (g1 mod q))) /^ nn = Sgm XX by A91, FINSEQ_5:37;
for d being Nat st d in dom f2 holds
f2 . d in NAT
proof
let d be Nat; :: thesis: ( d in dom f2 implies f2 . d in NAT )
assume d in dom f2 ; :: thesis: f2 . d in NAT
then f2 . d = (f1 . d) div p by A27;
hence f2 . d in NAT ; :: thesis: verum
end;
then reconsider f2 = f2 as FinSequence of NAT by FINSEQ_2:12;
set f3 = f1 mod p;
A95: len (f1 mod p) = len f1 by EULER_2:def 1;
then A96: 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 A97: p - 1 >= 3 - 1 by XREAL_1:9;
then f1 mod p <> {} by A18, A7, A95, NAT_2:13;
then rng (f1 mod p) is non empty finite Subset of NAT by FINSEQ_1:def 4;
then consider n1 being Element of NAT such that
A98: rng (f1 mod p) c= (Seg n1) \/ {0} by HEYTING3:1;
A99: dom f1 = dom f2 by A18, A27, FINSEQ_3:29;
A100: for d being Nat st d in dom f1 holds
f1 . d = ((f2 . d) * p) + ((f1 mod p) . d)
proof
let d be Nat; :: thesis: ( d in dom f1 implies f1 . d = ((f2 . d) * p) + ((f1 mod p) . d) )
assume A101: d in dom f1 ; :: thesis: f1 . d = ((f2 . d) * p) + ((f1 mod p) . d)
then A102: (f1 mod p) . d = (f1 . d) mod p by EULER_2:def 1;
f2 . d = (f1 . d) div p by A27, A99, A101;
hence f1 . d = ((f2 . d) * p) + ((f1 mod p) . d) by A102, NAT_D:2; :: thesis: verum
end;
not 0 in rng (f1 mod p)
proof
assume 0 in rng (f1 mod p) ; :: thesis: contradiction
then consider a being Nat such that
A103: a in dom (f1 mod p) and
A104: (f1 mod p) . a = 0 by FINSEQ_2:10;
f1 . a = ((f2 . a) * p) + 0 by A96, A100, A103, A104;
then q * a = (f2 . a) * p by A13, A96, A103;
then A105: p divides q * a by NAT_D:def 3;
a >= 1 by A103, FINSEQ_3:25;
then A106: p <= a by A4, A105, NAT_D:7, PEPIN:3;
a <= (p -' 1) div 2 by A18, A95, A103, FINSEQ_3:25;
hence contradiction by A12, A106, XXREAL_0:2; :: thesis: verum
end;
then A107: {0} misses rng (f1 mod p) by ZFMISC_1:50;
then A108: Sgm (rng (f1 mod p)) is one-to-one by A98, FINSEQ_3:92, XBOOLE_1:73;
A109: for d, e being Nat st d in dom f1 & e in dom f1 & p divides (f1 . d) - (f1 . e) holds
d = e
proof
A110: q,p are_relative_prime by A3, INT_2: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
A111: d in dom f1 and
A112: e in dom f1 and
A113: p divides (f1 . d) - (f1 . e) ; :: thesis: d = e
A114: f1 . e = q * e by A13, A112;
f1 . d = q * d by A13, A111;
then A115: p divides (d - e) * q by A113, A114;
now
assume d <> e ; :: thesis: contradiction
then d - e <> 0 ;
then abs p <= abs (d - e) by A115, A110, INT_2:25, INT_4:6;
then A116: p <= abs (d - e) by ABSVALUE:def 1;
A117: e >= 1 by A112, FINSEQ_3:25;
A118: d >= 1 by A111, FINSEQ_3:25;
e <= (p -' 1) div 2 by A18, A112, FINSEQ_3:25;
then A119: d - e >= 1 - ((p -' 1) div 2) by A118, XREAL_1:13;
A120: ((p -' 1) div 2) - 1 < p by A12, XREAL_1:147;
d <= (p -' 1) div 2 by A18, A111, FINSEQ_3:25;
then d - e <= ((p -' 1) div 2) - 1 by A117, XREAL_1:13;
then A121: d - e < p by A120, XXREAL_0:2;
- (((p -' 1) div 2) - 1) > - p by A120, XREAL_1:24;
then d - e > - p by A119, XXREAL_0:2;
hence contradiction by A116, A121, SEQ_2:1; :: thesis: verum
end;
hence d = e ; :: thesis: verum
end;
for x, y being set st x in dom (f1 mod p) & y in dom (f1 mod p) & (f1 mod p) . x = (f1 mod p) . y holds
x = y
proof
let x, y be set ; :: thesis: ( x in dom (f1 mod p) & y in dom (f1 mod p) & (f1 mod p) . x = (f1 mod p) . y implies x = y )
assume that
A122: x in dom (f1 mod p) and
A123: y in dom (f1 mod p) and
A124: (f1 mod p) . x = (f1 mod p) . y ; :: thesis: x = y
reconsider x = x, y = y as Element of NAT by A122, A123;
A125: f1 . y = ((f2 . y) * p) + ((f1 mod p) . y) by A96, A100, A123;
f1 . x = ((f2 . x) * p) + ((f1 mod p) . x) by A96, A100, A122;
then (f1 . x) - (f1 . y) = ((f2 . x) - (f2 . y)) * p by A124, A125;
then p divides (f1 . x) - (f1 . y) by INT_1:def 3;
hence x = y by A109, A96, A122, A123; :: thesis: verum
end;
then A126: f1 mod p is one-to-one by FUNCT_1:def 4;
then len (f1 mod p) = card (rng (f1 mod p)) by FINSEQ_4:62;
then A127: len (Sgm (rng (f1 mod p))) = (p -' 1) div 2 by A18, A95, A98, A107, FINSEQ_3:39, XBOOLE_1:73;
A128: (Sgm (rng (g1 mod q))) | nn = Sgm YY by A91, A93, FINSEQ_3:113, FINSEQ_6:10;
A129: (Sgm (rng (g1 mod q))) | nn is one-to-one by A48, A81, FINSEQ_3:91;
A130: Lege (p,q) = (- 1) |^ (Sum g2)
proof
set g5 = ((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn);
set g6 = ((Sgm (rng (g1 mod q))) | nn) ^ (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn));
A131: rng (idseq ((q -' 1) div 2)) = Seg ((q -' 1) div 2) by RELAT_1:45;
A132: (Sgm (rng (g1 mod q))) /^ nn is FinSequence of REAL by FINSEQ_2:24;
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
.= (Seg (len ((Sgm (rng (g1 mod q))) /^ nn))) /\ (dom ((Sgm (rng (g1 mod q))) /^ nn)) by A134, CARD_1:def 7
.= (dom ((Sgm (rng (g1 mod q))) /^ nn)) /\ (dom ((Sgm (rng (g1 mod q))) /^ nn)) by FINSEQ_1:def 3
.= dom ((Sgm (rng (g1 mod q))) /^ nn) ;
then 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
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;
A139: for d being Nat st d in dom (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) holds
( (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d > 0 & (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d <= (q -' 1) div 2 )
proof
let d be Nat; :: thesis: ( d in dom (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) implies ( (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d > 0 & (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d <= (q -' 1) div 2 ) )
reconsider w = (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d as Element of INT by INT_1:def 2;
assume 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 A94, 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 A94, 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 A94, 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;
for d being Nat st d in dom (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) holds
(((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d in NAT
proof
let d be Nat; :: thesis: ( d in dom (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) implies (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d in NAT )
assume d in dom (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) ; :: thesis: (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d in NAT
then (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d > 0 by A139;
hence (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d in NAT by INT_1:3; :: thesis: verum
end;
then reconsider g5 = ((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn) as FinSequence of NAT by FINSEQ_2:12;
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;
A146: g6 is FinSequence of REAL by FINSEQ_2:24;
A147: nn <= len (Sgm (rng (g1 mod q))) by A67, XREAL_1:43;
A148: rng ((Sgm (rng (g1 mod q))) | nn) misses rng g5
proof
assume not rng ((Sgm (rng (g1 mod q))) | nn) misses rng g5 ; :: thesis: contradiction
then consider x being set such that
A149: x in rng ((Sgm (rng (g1 mod q))) | nn) and
A150: x in rng g5 by XBOOLE_0:3;
consider e being Nat such that
A151: e in dom g5 and
A152: g5 . e = x by A150, FINSEQ_2:10;
x = q - (((Sgm (rng (g1 mod q))) /^ nn) . e) by A137, A151, A152;
then A153: x = q - ((Sgm (rng (g1 mod q))) . (e + nn)) by A147, A135, A151, RFINSEQ:def 1;
e + nn in dom (Sgm (rng (g1 mod q))) by A135, A151, FINSEQ_5:26;
then consider e1 being Nat such that
A154: e1 in dom (g1 mod q) and
A155: (g1 mod q) . e1 = (Sgm (rng (g1 mod q))) . (e + nn) by A78, FINSEQ_2:10, FUNCT_1:3;
A156: e1 <= (q -' 1) div 2 by A23, A24, A154, 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
A157: d1 in dom (g1 mod q) and
A158: (g1 mod q) . d1 = x by A78, A149, FINSEQ_2:10;
d1 <= (q -' 1) div 2 by A23, A24, A157, FINSEQ_3:25;
then d1 + e1 <= ((q -' 1) div 2) + ((q -' 1) div 2) by A156, XREAL_1:7;
then A159: d1 + e1 < q by A29, A40, XREAL_1:146, XXREAL_0:2;
A160: e1 in dom g1 by A24, A154, FINSEQ_3:29;
then A161: (Sgm (rng (g1 mod q))) . (e + nn) = (g1 . e1) mod q by A155, EULER_2:def 1;
A162: d1 in dom g1 by A24, A157, FINSEQ_3:29;
then x = (g1 . d1) mod q by A158, EULER_2:def 1;
then (((g1 . d1) mod q) + ((g1 . e1) mod q)) mod q = 0 by A153, A161, 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, A162;
then q divides (d1 * p) + (e1 * p) by A19, A160;
then A163: q divides (d1 + e1) * p ;
d1 >= 1 by A157, FINSEQ_3:25;
hence contradiction by A4, A163, A159, NAT_D:7, PEPIN:3; :: thesis: verum
end;
for d, e being Element of NAT st 1 <= d & d < e & e <= len g5 holds
g5 . d <> g5 . e
proof
let d, e be Element of NAT ; :: thesis: ( 1 <= d & d < e & e <= len g5 implies g5 . d <> g5 . e )
assume that
A164: 1 <= d and
A165: d < e and
A166: e <= len g5 ; :: thesis: g5 . d <> g5 . e
1 <= e by A164, A165, XXREAL_0:2;
then A167: e in dom g5 by A166, FINSEQ_3:25;
then A168: g5 . e = q - (((Sgm (rng (g1 mod q))) /^ nn) . e) by A137;
d < len g5 by A165, A166, XXREAL_0:2;
then A169: d in dom g5 by A164, FINSEQ_3:25;
then g5 . d = q - (((Sgm (rng (g1 mod q))) /^ nn) . d) by A137;
hence g5 . d <> g5 . e by A82, A135, A165, A169, A167, A168, FUNCT_1:def 4; :: thesis: verum
end;
then len g5 = card (rng g5) by GRAPH_5:7;
then g5 is one-to-one by FINSEQ_4:62;
then A170: g6 is one-to-one by A129, A148, FINSEQ_3:91;
A171: for d being Nat st d in dom g6 holds
( g6 . d > 0 & g6 . d <= (q -' 1) div 2 )
proof
let d be Nat; :: thesis: ( d in dom g6 implies ( g6 . d > 0 & g6 . d <= (q -' 1) div 2 ) )
assume A172: 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 A172, FINSEQ_1:25;
suppose A173: d in dom ((Sgm (rng (g1 mod q))) | nn) ; :: thesis: ( g6 . d > 0 & g6 . d <= (q -' 1) div 2 )
then ((Sgm (rng (g1 mod q))) | nn) . d in rng (Sgm YY) by A128, FUNCT_1:3;
then A174: ((Sgm (rng (g1 mod q))) | nn) . d in YY by A86, FINSEQ_1:def 13;
then A175: ((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 A174, XBOOLE_0:def 5;
then ((Sgm (rng (g1 mod q))) | nn) . d <= q / 2 by A175;
then A176: ((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, A175, 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 A173, A176, FINSEQ_1:def 7; :: thesis: verum
end;
suppose ex l being Nat st
( l in dom g5 & d = (len ((Sgm (rng (g1 mod q))) | nn)) + l ) ; :: thesis: ( g6 . d > 0 & g6 . d <= (q -' 1) div 2 )
then consider l being Element of NAT such that
A177: l in dom g5 and
A178: d = (len ((Sgm (rng (g1 mod q))) | nn)) + l ;
g6 . d = g5 . l by A177, A178, FINSEQ_1:def 7;
hence ( g6 . d > 0 & g6 . d <= (q -' 1) div 2 ) by A139, A177; :: thesis: verum
end;
end;
end;
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 A131, A170, A171, Th40;
then N = Sum g6 by A170, A146, 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 A92, A94, A128;
then A179: ((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 A179, 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 by INT_2:15;
then (Sum g2) mod 2 = (card XX) mod 2 by NAT_D:64;
then (- 1) |^ (Sum g2) = (- 1) |^ (card XX) by Th45;
hence Lege (p,q) = (- 1) |^ (Sum g2) by A2, A5, A78, Th41; :: thesis: verum
end;
for d being Nat st d in dom (idseq ((p -' 1) div 2)) holds
(idseq ((p -' 1) div 2)) . d in NAT
proof
let d be Nat; :: thesis: ( d in dom (idseq ((p -' 1) div 2)) implies (idseq ((p -' 1) div 2)) . d in NAT )
assume A180: d in dom (idseq ((p -' 1) div 2)) ; :: thesis: (idseq ((p -' 1) div 2)) . d in NAT
then d in Seg (len (idseq ((p -' 1) div 2))) by FINSEQ_1:def 3;
then d is Element of Seg ((p -' 1) div 2) by CARD_1:def 7;
then (idseq ((p -' 1) div 2)) . d = d by FINSEQ_2:49;
hence (idseq ((p -' 1) div 2)) . d in NAT by A180; :: thesis: verum
end;
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;
A181: 2,p are_relative_prime 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 set st x in { k where k is Element of NAT : ( k in rng (Sgm (rng (f1 mod p))) & k > p / 2 ) } holds
x in rng (Sgm (rng (f1 mod p)))
proof
let x be set ; :: thesis: ( x in { k where k is Element of NAT : ( k in rng (Sgm (rng (f1 mod p))) & k > p / 2 ) } implies x in rng (Sgm (rng (f1 mod p))) )
assume x in { k where k is Element of NAT : ( k in rng (Sgm (rng (f1 mod p))) & k > p / 2 ) } ; :: thesis: x in rng (Sgm (rng (f1 mod p)))
then ex k being Element of NAT st
( x = k & k in rng (Sgm (rng (f1 mod p))) & k > p / 2 ) ;
hence x in rng (Sgm (rng (f1 mod p))) ; :: thesis: verum
end;
then A182: { k where k is Element of NAT : ( k in rng (Sgm (rng (f1 mod p))) & k > p / 2 ) } c= rng (Sgm (rng (f1 mod p))) by TARSKI:def 3;
A183: (p -' 1) div 2 >= 1 by A7, A97, NAT_2:13;
A184: (Sum f2) + (Sum g2) = ((p -' 1) div 2) * ((q -' 1) div 2)
proof
reconsider A = Seg ((p -' 1) div 2), B = Seg ((q -' 1) div 2) as non empty finite Subset of NAT by A183, A31;
deffunc H3( Element of A, Element of B) -> set = ($1 / p) - ($2 / q);
A185: for x being Element of A
for y being Element of B holds H3(x,y) in REAL by XREAL_0:def 1;
consider z being Function of [:A,B:],REAL such that
A186: for x being Element of A
for y being Element of B holds z . (x,y) = H3(x,y) from FUNCT_7:sch 1(A185);
 defpred S1[ 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 } );
A187: for d being Nat st d in Seg ((p -' 1) div 2) holds
ex x1 being Element of bool (dom z) st S1[d,x1]
proof
let d be Nat; :: thesis: ( d in Seg ((p -' 1) div 2) implies ex x1 being Element of bool (dom z) st S1[d,x1] )
assume d in Seg ((p -' 1) div 2) ; :: thesis: ex x1 being Element of bool (dom z) st S1[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) & S1[d,x1] )
x1 c= dom z
proof
let l be set ; :: according to TARSKI:def 3 :: thesis: ( not l in x1 or l in dom z )
assume l in x1 ; :: thesis: l in dom z
then ex yy being Element of B st
( [d,yy] = l & z . (d,yy) > 0 ) ;
then l in [:A,B:] ;
hence l in dom z by FUNCT_2:def 1; :: thesis: verum
end;
hence ( x1 is Element of bool (dom z) & S1[d,x1] ) ; :: thesis: verum
end;
consider Pr being FinSequence of bool (dom z) such that
A188: ( dom Pr = Seg ((p -' 1) div 2) & ( for d being Nat st d in Seg ((p -' 1) div 2) holds
S1[d,Pr . d] ) ) from FINSEQ_1:sch 5(A187);
 A189: dom (Card Pr) = dom Pr by CARD_3:def 2
.= dom f2 by A27, A188, FINSEQ_1:def 3 ;
for d being Nat st d in dom (Card Pr) holds
(Card Pr) . d = f2 . d
proof
let d be Nat; :: thesis: ( d in dom (Card Pr) implies (Card Pr) . d = f2 . d )
assume A190: d in dom (Card Pr) ; :: thesis: (Card Pr) . d = f2 . d
then d in Seg ((p -' 1) div 2) by A27, A189, FINSEQ_1:def 3;
then consider m being Element of A such that
A191: m = d and
A192: Pr . d = { [m,y] where y is Element of B : z . (m,y) > 0 } by A188;
Pr . d = [:{m},(Seg (f2 . m)):]
proof
set L = [:{m},(Seg (f2 . m)):];
A193: [:{m},(Seg (f2 . m)):] c= Pr . d
proof
then A195: - (q div p) = ((- q) div p) + 1 by WSIERP_1:41;
2 divides (p -' 1) * q by A10, NAT_D:9;
then ((p -' 1) * q) mod 2 = 0 by PEPIN:6;
then ((p -' 1) * q) div 2 = ((p -' 1) * q) / 2 by REAL_3:4;
then A196: (((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 A195, 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 ;
A197: (((p -' 1) div 2) * q) div p <= (q -' 1) div 2
proof
per cases ( (q div p) mod 2 = 0 or (q div p) mod 2 <> 0 ) ;
suppose (q div p) mod 2 = 0 ; :: thesis: (((p -' 1) div 2) * q) div p <= (q -' 1) div 2
then (- (q div p)) div 2 = - ((q div p) div 2) by WSIERP_1:42
.= - (q div (2 * p)) by NAT_2:27 ;
then (((p -' 1) div 2) * q) div p = ((q -' 1) div 2) - (q div (2 * p)) by A196;
hence (((p -' 1) div 2) * q) div p <= (q -' 1) div 2 by XREAL_1:43; :: thesis: verum
end;
suppose (q div p) mod 2 <> 0 ; :: thesis: (((p -' 1) div 2) * q) div p <= (q -' 1) div 2
then - ((q div p) div 2) = ((- (q div p)) div 2) + 1 by WSIERP_1:41;
then (- (q div p)) div 2 = (- ((q div p) div 2)) - 1
.= (- (q div (2 * p))) - 1 by NAT_2:27 ;
then (((p -' 1) div 2) * q) div p = ((q -' 1) div 2) - ((q div (2 * p)) + 1) by A196;
hence (((p -' 1) div 2) * q) div p <= (q -' 1) div 2 by XREAL_1:43; :: thesis: verum
end;
end;
end;
m <= (p -' 1) div 2 by FINSEQ_1:1;
then m * q <= ((p -' 1) div 2) * q by XREAL_1:64;
then (m * q) div p <= (((p -' 1) div 2) * q) div p by NAT_2:24;
then A198: (m * q) div p <= (q -' 1) div 2 by A197, XXREAL_0:2;
m in Seg ((p -' 1) div 2) ;
then A199: m in dom f1 by A18, FINSEQ_1:def 3;
then A200: f2 . m = (f1 . m) div p by A27, A99
.= (m * q) div p by A13, A199 ;
then A203: [\((m * q) / p)/] < (m * q) / p by INT_1:26;
let l be set ; :: according to TARSKI:def 3 :: thesis: ( not l in [:{m},(Seg (f2 . m)):] or l in Pr . d )
assume l in [:{m},(Seg (f2 . m)):] ; :: thesis: l in Pr . d
then consider x, y being set such that
A204: x in {m} and
A205: y in Seg (f2 . m) and
A206: l = [x,y] by ZFMISC_1:def 2;
reconsider y = y as Element of NAT by A205;
A207: 1 <= y by A205, FINSEQ_1:1;
y <= f2 . m by A205, FINSEQ_1:1;
then y <= (q -' 1) div 2 by A198, A200, XXREAL_0:2;
then reconsider y = y as Element of B by A207, FINSEQ_1:1;
y <= [\((m * q) / p)/] by A205, A200, FINSEQ_1:1;
then y < (m * q) / p by A203, 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 A186;
then [m,y] in Pr . d by A192;
hence l in Pr . d by A204, A206, TARSKI:def 1; :: thesis: verum
end;
Pr . d c= [:{m},(Seg (f2 . m)):]
proof
let l be set ; :: according to TARSKI:def 3 :: thesis: ( not l in Pr . d or l in [:{m},(Seg (f2 . m)):] )
A208: m in {m} by TARSKI:def 1;
m in Seg ((p -' 1) div 2) ;
then A209: 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
A210: l = [m,y1] and
A211: z . (m,y1) > 0 by A192;
(m / p) - (y1 / q) > 0 by A186, A211;
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, A209;
then A212: y1 <= f2 . m by A27, A99, A209;
y1 >= 1 by FINSEQ_1:1;
then y1 in Seg (f2 . m) by A212, FINSEQ_1:1;
hence l in [:{m},(Seg (f2 . m)):] by A210, A208, ZFMISC_1:def 2; :: thesis: verum
end;
hence Pr . d = [:{m},(Seg (f2 . m)):] by A193, XBOOLE_0:def 10; :: thesis: verum
end;
then card (Pr . d) = card [:(Seg (f2 . m)),{m}:] by CARD_2:4
.= card (Seg (f2 . m)) by CARD_1:69 ;
then A213: card (Pr . d) = card (f2 . d) by A191, FINSEQ_1:55
.= f2 . d by CARD_1:def 2 ;
d in dom Pr by A190, CARD_3:def 2;
hence (Card Pr) . d = f2 . d by A213, CARD_3:def 2; :: thesis: verum
end;
then A214: Card Pr = f2 by A189, FINSEQ_1:13;
defpred S2[ 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 } );
A215: for d being Nat st d in Seg ((q -' 1) div 2) holds
ex x1 being Element of bool (dom z) st S2[d,x1]
proof
let d be Nat; :: thesis: ( d in Seg ((q -' 1) div 2) implies ex x1 being Element of bool (dom z) st S2[d,x1] )
assume d in Seg ((q -' 1) div 2) ; :: thesis: ex x1 being Element of bool (dom z) st S2[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) & S2[d,x1] )
x1 c= dom z
proof
let l be set ; :: according to TARSKI:def 3 :: thesis: ( not l in x1 or l in dom z )
assume l in x1 ; :: thesis: l in dom z
then ex xx being Element of A st
( [xx,d] = l & z . (xx,d) < 0 ) ;
then l in [:A,B:] ;
hence l in dom z by FUNCT_2:def 1; :: thesis: verum
end;
hence ( x1 is Element of bool (dom z) & S2[d,x1] ) ; :: thesis: verum
end;
consider Pk being FinSequence of bool (dom z) such that
A216: ( dom Pk = Seg ((q -' 1) div 2) & ( for d being Nat st d in Seg ((q -' 1) div 2) holds
S2[d,Pk . d] ) ) from FINSEQ_1:sch 5(A215);
 A217: dom (Card Pk) = Seg (len g2) by A33, A216, CARD_3:def 2
.= dom g2 by FINSEQ_1:def 3 ;
A218: for d being Nat st d in dom (Card Pk) holds
(Card Pk) . d = g2 . d
proof
let d be Nat; :: thesis: ( d in dom (Card Pk) implies (Card Pk) . d = g2 . d )
assume A219: d in dom (Card Pk) ; :: thesis: (Card Pk) . d = g2 . d
then d in Seg ((q -' 1) div 2) by A33, A217, FINSEQ_1:def 3;
then consider n being Element of B such that
A220: n = d and
A221: Pk . d = { [x,n] where x is Element of A : z . (x,n) < 0 } by A216;
Pk . d = [:(Seg (g2 . n)),{n}:]
proof
set L = [:(Seg (g2 . n)),{n}:];
A222: [:(Seg (g2 . n)),{n}:] c= Pk . d
proof
then A224: - (p div q) = ((- p) div q) + 1 by WSIERP_1:41;
2 divides (q -' 1) * p by A39, NAT_D:9;
then ((q -' 1) * p) mod 2 = 0 by PEPIN:6;
then ((q -' 1) * p) div 2 = ((q -' 1) * p) / 2 by REAL_3:4;
then A225: (((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 A224, 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 ;
A226: (((q -' 1) div 2) * p) div q <= (p -' 1) div 2
proof
per cases ( (p div q) mod 2 = 0 or (p div q) mod 2 <> 0 ) ;
suppose (p div q) mod 2 = 0 ; :: thesis: (((q -' 1) div 2) * p) div q <= (p -' 1) div 2
then (- (p div q)) div 2 = - ((p div q) div 2) by WSIERP_1:42
.= - (p div (2 * q)) by NAT_2:27 ;
then (((q -' 1) div 2) * p) div q = ((p -' 1) div 2) - (p div (2 * q)) by A225;
hence (((q -' 1) div 2) * p) div q <= (p -' 1) div 2 by XREAL_1:43; :: thesis: verum
end;
suppose (p div q) mod 2 <> 0 ; :: thesis: (((q -' 1) div 2) * p) div q <= (p -' 1) div 2
then - ((p div q) div 2) = ((- (p div q)) div 2) + 1 by WSIERP_1:41;
then (- (p div q)) div 2 = (- ((p div q) div 2)) - 1
.= (- (p div (2 * q))) - 1 by NAT_2:27 ;
then (((q -' 1) div 2) * p) div q = ((p -' 1) div 2) - ((p div (2 * q)) + 1) by A225;
hence (((q -' 1) div 2) * p) div q <= (p -' 1) div 2 by XREAL_1:43; :: thesis: verum
end;
end;
end;
n in Seg ((q -' 1) div 2) ;
then A227: n in dom g1 by A23, FINSEQ_1:def 3;
then A228: g2 . n = (g1 . n) div q by A33, A34
.= (n * p) div q by A19, A227 ;
let l be set ; :: according to TARSKI:def 3 :: thesis: ( not l in [:(Seg (g2 . n)),{n}:] or l in Pk . d )
assume l in [:(Seg (g2 . n)),{n}:] ; :: thesis: l in Pk . d
then consider x, y being set such that
A229: x in Seg (g2 . n) and
A230: y in {n} and
A231: l = [x,y] by ZFMISC_1:def 2;
reconsider x = x as Element of NAT by A229;
A232: x <= g2 . n by A229, 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 A226, XXREAL_0:2;
then A233: x <= (p -' 1) div 2 by A228, A232, XXREAL_0:2;
1 <= x by A229, FINSEQ_1:1;
then reconsider x = x as Element of A by A233, FINSEQ_1:1;
then [\((n * p) / q)/] < (n * p) / q by INT_1:26;
then x < (n * p) / q by A228, A232, 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 A186;
then [x,n] in Pk . d by A221;
hence l in Pk . d by A230, A231, TARSKI:def 1; :: thesis: verum
end;
Pk . d c= [:(Seg (g2 . n)),{n}:]
proof
let l be set ; :: according to TARSKI:def 3 :: thesis: ( not l in Pk . d or l in [:(Seg (g2 . n)),{n}:] )
A236: n in {n} by TARSKI:def 1;
n in Seg ((q -' 1) div 2) ;
then A237: 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
A238: l = [x,n] and
A239: z . (x,n) < 0 by A221;
(x / p) - (n / q) < 0 by A186, A239;
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, A237;
then A240: x <= g2 . n by A33, A34, A237;
x >= 1 by FINSEQ_1:1;
then x in Seg (g2 . n) by A240, FINSEQ_1:1;
hence l in [:(Seg (g2 . n)),{n}:] by A238, A236, ZFMISC_1:def 2; :: thesis: verum
end;
hence Pk . d = [:(Seg (g2 . n)),{n}:] by A222, XBOOLE_0:def 10; :: thesis: verum
end;
then card (Pk . d) = card (Seg (g2 . n)) by CARD_1:69;
then A241: card (Pk . d) = card (g2 . d) by A220, FINSEQ_1:55
.= g2 . d by CARD_1:def 2 ;
d in dom Pk by A219, CARD_3:def 2;
hence (Card Pk) . d = g2 . d by A241, CARD_3:def 2; :: thesis: verum
end;
reconsider U1 = union (rng Pr), U2 = union (rng Pk) as finite Subset of (dom z) by PROB_3:48;
dom z c= U1 \/ U2
proof
let l be set ; :: according to TARSKI:def 3 :: thesis: ( not l in dom z or l in U1 \/ U2 )
assume l in dom z ; :: thesis: l in U1 \/ U2
then consider x, y being set such that
A242: x in A and
A243: y in B and
A244: l = [x,y] by ZFMISC_1:def 2;
reconsider y = y as Element of B by A243;
reconsider x = x as Element of A by A242;
A245: z . (x,y) <> 0
per cases ( z . (x,y) > 0 or z . (x,y) < 0 ) by A245;
end;
end;
then A250: U1 \/ U2 = dom z by XBOOLE_0:def 10;
A251: U1 misses U2
proof
assume U1 meets U2 ; :: thesis: contradiction
then consider l being set such that
A252: l in U1 and
A253: l in U2 by XBOOLE_0:3;
l in Union Pk by A253;
then consider k2 being Nat such that
A254: k2 in dom Pk and
A255: l in Pk . k2 by PROB_3:49;
l in Union Pr by A252;
then consider k1 being Nat such that
A256: k1 in dom Pr and
A257: 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
A258: Pk . k2 = { [x,n1] where x is Element of A : z . (x,n1) < 0 } by A216, A254;
consider n2 being Element of A such that
A259: l = [n2,n1] and
A260: z . (n2,n1) < 0 by A255, A258;
consider m1 being Element of A such that
m1 = k1 and
A261: Pr . k1 = { [m1,y] where y is Element of B : z . (m1,y) > 0 } by A188, A256;
A262: ex m2 being Element of B st
( l = [m1,m2] & z . (m1,m2) > 0 ) by A257, A261;
then m1 = n2 by A259, ZFMISC_1:27;
hence contradiction by A262, A259, A260, ZFMISC_1:27; :: thesis: verum
end;
A263: for d, e being Nat st d in dom Pk & e in dom Pk & d <> e holds
Pk . d misses Pk . e
proof
let d, e be Nat; :: thesis: ( d in dom Pk & e in dom Pk & d <> e implies Pk . d misses Pk . e )
assume that
A264: d in dom Pk and
A265: e in dom Pk and
A266: d <> e ; :: thesis: Pk . d misses Pk . e
consider y2 being Element of B such that
A267: y2 = e and
A268: Pk . e = { [x,y2] where x is Element of A : z . (x,y2) < 0 } by A216, A265;
consider y1 being Element of B such that
A269: y1 = d and
A270: Pk . d = { [x,y1] where x is Element of A : z . (x,y1) < 0 } by A216, A264;
now
assume not Pk . d misses Pk . e ; :: thesis: contradiction
then consider l being set such that
A271: l in Pk . d and
A272: l in Pk . e by XBOOLE_0:3;
A273: ex x2 being Element of A st
( l = [x2,y2] & z . (x2,y2) < 0 ) by A268, A272;
ex x1 being Element of A st
( l = [x1,y1] & z . (x1,y1) < 0 ) by A270, A271;
hence contradiction by A266, A269, A267, A273, ZFMISC_1:27; :: thesis: verum
end;
hence Pk . d misses Pk . e ; :: thesis: verum
end;
len Pk = (q -' 1) div 2 by A216, FINSEQ_1:def 3;
then A274: card (union (rng Pk)) = Sum (Card Pk) by A263, Th48;
A275: for d, e being Nat st d in dom Pr & e in dom Pr & d <> e holds
Pr . d misses Pr . e
proof
let d, e be Nat; :: thesis: ( d in dom Pr & e in dom Pr & d <> e implies Pr . d misses Pr . e )
assume that
A276: d in dom Pr and
A277: e in dom Pr and
A278: d <> e ; :: thesis: Pr . d misses Pr . e
consider x2 being Element of A such that
A279: x2 = e and
A280: Pr . e = { [x2,y] where y is Element of B : z . (x2,y) > 0 } by A188, A277;
consider x1 being Element of A such that
A281: x1 = d and
A282: Pr . d = { [x1,y] where y is Element of B : z . (x1,y) > 0 } by A188, A276;
now
assume not Pr . d misses Pr . e ; :: thesis: contradiction
then consider l being set such that
A283: l in Pr . d and
A284: l in Pr . e by XBOOLE_0:3;
A285: ex y2 being Element of B st
( l = [x2,y2] & z . (x2,y2) > 0 ) by A280, A284;
ex y1 being Element of B st
( l = [x1,y1] & z . (x1,y1) > 0 ) by A282, A283;
hence contradiction by A278, A281, A279, A285, ZFMISC_1:27; :: thesis: verum
end;
hence Pr . d misses Pr . e ; :: thesis: verum
end;
len Pr = (p -' 1) div 2 by A188, FINSEQ_1:def 3;
then card (union (rng Pr)) = Sum (Card Pr) by A275, Th48;
then card (U1 \/ U2) = (Sum (Card Pr)) + (Sum (Card Pk)) by A274, A251, CARD_2:40;
then (Sum (Card Pr)) + (Sum (Card Pk)) = card [:A,B:] by A250, 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 A214, A217, A218, FINSEQ_1:13; :: thesis: verum
end;
dom (p * f2) = dom f2 by VALUED_1:def 5;
then A286: 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 A286;
then A287: p * f2 is Element of ((p -' 1) div 2) -tuples_on REAL by FINSEQ_2:109;
A288: (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 A182, XBOOLE_1:1;
set m = card X;
reconsider Y = (rng (Sgm (rng (f1 mod p)))) \ X as finite Subset of NAT ;
A289: f1 mod p is Element of NAT * by FINSEQ_1:def 11;
len (f1 mod p) = (p -' 1) div 2 by A17, A95, CARD_1:def 7;
then f1 mod p in ((p -' 1) div 2) -tuples_on NAT by A289;
then A290: f1 mod p is Element of ((p -' 1) div 2) -tuples_on REAL by FINSEQ_2:109;
A291: rng (f1 mod p) c= Seg n1 by A98, A107, XBOOLE_1:73;
then A292: rng (Sgm (rng (f1 mod p))) = rng (f1 mod p) by FINSEQ_1:def 13;
then A293: X c= Seg n1 by A291, A182, XBOOLE_1:1;
A294: dom ((p * f2) + (f1 mod p)) = (dom (p * f2)) /\ (dom (f1 mod p)) by VALUED_1:def 1
.= (dom f2) /\ (dom (f1 mod p)) by VALUED_1:def 5
.= dom f1 by A96, A99 ;
for d being Nat st d in dom f1 holds
f1 . d = ((p * f2) + (f1 mod p)) . d
proof
let d be Nat; :: thesis: ( d in dom f1 implies f1 . d = ((p * f2) + (f1 mod p)) . d )
assume A295: d in dom f1 ; :: thesis: f1 . d = ((p * f2) + (f1 mod p)) . d
then A296: d in dom (p * f2) by A99, VALUED_1:def 5;
((p * f2) + (f1 mod p)) . d = ((p * f2) . d) + ((f1 mod p) . d) by A294, A295, VALUED_1:def 1;
hence ((p * f2) + (f1 mod p)) . d = (p * (f2 . d)) + ((f1 mod p) . d) by A296, VALUED_1:def 5
.= f1 . d by A100, A295 ;
:: thesis: verum
end;
then f1 = (p * f2) + (f1 mod p) by A294, FINSEQ_1:13;
then A297: Sum f1 = (Sum (p * f2)) + (Sum (f1 mod p)) by A287, A290, RVSUM_1:89
.= (p * (Sum f2)) + (Sum (f1 mod p)) by RVSUM_1:87 ;
A298: (rng (Sgm (rng (f1 mod p)))) \ X c= rng (Sgm (rng (f1 mod p))) by XBOOLE_1:36;
then A299: Y c= Seg n1 by A291, A292, XBOOLE_1:1;
A300: len (f1 mod p) = card (rng (Sgm (rng (f1 mod p)))) by A126, A292, FINSEQ_4:62;
then reconsider n = ((p -' 1) div 2) - (card X) as Element of NAT by A18, A95, A182, NAT_1:21, NAT_1:43;
A301: Sgm (rng (f1 mod p)) = ((Sgm (rng (f1 mod p))) | n) ^ ((Sgm (rng (f1 mod p))) /^ n) by RFINSEQ:8;
then A302: (Sgm (rng (f1 mod p))) /^ n is one-to-one by A108, FINSEQ_3:91;
Sgm (rng (f1 mod p)) is FinSequence of REAL by FINSEQ_2:24;
then A303: Sum (Sgm (rng (f1 mod p))) = Sum (f1 mod p) by A126, A292, A108, RFINSEQ:9, RFINSEQ:26;
for k, l being Element of NAT st k in Y & l in X holds
k < l
proof
let k, l be Element of NAT ; :: thesis: ( k in Y & l in X implies k < l )
assume that
A304: k in Y and
A305: l in X ; :: thesis: k < l
A306: not k in X by A304, XBOOLE_0:def 5;
A307: ex l1 being Element of NAT st
( l1 = l & l1 in rng (Sgm (rng (f1 mod p))) & l1 > p / 2 ) by A305;
k in rng (Sgm (rng (f1 mod p))) by A304, XBOOLE_0:def 5;
then k <= p / 2 by A306;
hence k < l by A307, XXREAL_0:2; :: thesis: verum
end;
then Sgm (Y \/ X) = (Sgm Y) ^ (Sgm X) by A293, A299, FINSEQ_3:42;
then Sgm ((rng (Sgm (rng (f1 mod p)))) \/ X) = (Sgm Y) ^ (Sgm X) by XBOOLE_1:39;
then A308: Sgm (rng (f1 mod p)) = (Sgm Y) ^ (Sgm X) by A292, A182, XBOOLE_1:12;
then Sum (Sgm (rng (f1 mod p))) = (Sum (Sgm Y)) + (Sum (Sgm X)) by RVSUM_1:75;
then A309: q * (Sum (idseq ((p -' 1) div 2))) = ((p * (Sum f2)) + (Sum (Sgm Y))) + (Sum (Sgm X)) by A297, A303, RVSUM_1:87;
A310: len (Sgm Y) = card Y by A291, A292, A298, FINSEQ_3:39, XBOOLE_1:1
.= ((p -' 1) div 2) - (card X) by A18, A95, A182, A300, CARD_2:44 ;
then A311: (Sgm (rng (f1 mod p))) /^ n = Sgm X by A308, FINSEQ_5:37;
A312: (Sgm (rng (f1 mod p))) | n = Sgm Y by A308, A310, FINSEQ_3:113, FINSEQ_6:10;
A313: (Sgm (rng (f1 mod p))) | n is one-to-one by A108, A301, FINSEQ_3:91;
Lege (q,p) = (- 1) |^ (Sum f2)
proof
set f5 = ((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n);
set f6 = ((Sgm (rng (f1 mod p))) | n) ^ (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n));
A314: rng (idseq ((p -' 1) div 2)) = Seg ((p -' 1) div 2) by RELAT_1:45;
A315: (Sgm (rng (f1 mod p))) /^ n is FinSequence of REAL by FINSEQ_2:24;
A316: len ((Sgm (rng (f1 mod p))) | n) = n by A127, FINSEQ_1:59, XREAL_1:43;
A317: 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 A127, XREAL_1:43, XREAL_1:233
.= card X by A127 ;
A318: dom (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) = (dom ((card X) |-> p)) /\ (dom ((Sgm (rng (f1 mod p))) /^ n)) by VALUED_1:12
.= (Seg (len ((card X) |-> p))) /\ (dom ((Sgm (rng (f1 mod p))) /^ n)) by FINSEQ_1:def 3
.= (Seg (len ((Sgm (rng (f1 mod p))) /^ n))) /\ (dom ((Sgm (rng (f1 mod p))) /^ n)) by A317, CARD_1:def 7
.= (dom ((Sgm (rng (f1 mod p))) /^ n)) /\ (dom ((Sgm (rng (f1 mod p))) /^ n)) by FINSEQ_1:def 3
.= dom ((Sgm (rng (f1 mod p))) /^ n) ;
then A319: len (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) = len ((Sgm (rng (f1 mod p))) /^ n) by FINSEQ_3:29;
A320: for d being Nat st d in dom (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) holds
(((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d = p - (((Sgm (rng (f1 mod p))) /^ n) . d)
proof
let d be Nat; :: thesis: ( d in dom (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) implies (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d = p - (((Sgm (rng (f1 mod p))) /^ n) . d) )
assume A321: 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 A317, A318, 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 A321, VALUED_1:13; :: thesis: verum
end;
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 > 0 & (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d <= (p -' 1) div 2 )
proof
let d be Nat; :: thesis: ( d in dom (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) implies ( (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d > 0 & (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d <= (p -' 1) div 2 ) )
reconsider w = (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d as Element of INT by INT_1:def 2;
assume A323: 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 A311, A318, FUNCT_1:3;
then (Sgm X) . d in X by A293, FINSEQ_1:def 13;
then A324: ex ll being Element of NAT st
( ll = (Sgm X) . d & ll in rng (f1 mod p) & ll > p / 2 ) by A292;
then consider e being Nat such that
A325: e in dom (f1 mod p) and
A326: (f1 mod p) . e = ((Sgm (rng (f1 mod p))) /^ n) . d by A311, FINSEQ_2:10;
((Sgm (rng (f1 mod p))) /^ n) . d = (f1 . e) mod p by A96, A325, A326, EULER_2:def 1;
then A327: ((Sgm (rng (f1 mod p))) /^ n) . d < p by NAT_D:1;
A328: (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d = p - (((Sgm (rng (f1 mod p))) /^ n) . d) by A320, A323;
then w < p - (p / 2) by A311, A324, 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 A288, A328, A327, INT_1:54, XREAL_1:50; :: thesis: verum
end;
for d being Nat st d in dom (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) holds
(((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d in NAT
proof
let d be Nat; :: thesis: ( d in dom (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) implies (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d in NAT )
assume d in dom (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) ; :: thesis: (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d in NAT
then (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d > 0 by A322;
hence (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d in NAT by INT_1:3; :: thesis: verum
end;
then reconsider f5 = ((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n) as FinSequence of NAT by FINSEQ_2:12;
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;
A329: f6 is FinSequence of REAL by FINSEQ_2:24;
A330: n <= len (Sgm (rng (f1 mod p))) by A127, XREAL_1:43;
A331: rng ((Sgm (rng (f1 mod p))) | n) misses rng f5
proof
assume not rng ((Sgm (rng (f1 mod p))) | n) misses rng f5 ; :: thesis: contradiction
then consider x being set such that
A332: x in rng ((Sgm (rng (f1 mod p))) | n) and
A333: x in rng f5 by XBOOLE_0:3;
consider e being Nat such that
A334: e in dom f5 and
A335: f5 . e = x by A333, FINSEQ_2:10;
x = p - (((Sgm (rng (f1 mod p))) /^ n) . e) by A320, A334, A335;
then A336: x = p - ((Sgm (rng (f1 mod p))) . (e + n)) by A330, A318, A334, RFINSEQ:def 1;
e + n in dom (Sgm (rng (f1 mod p))) by A318, A334, FINSEQ_5:26;
then consider e1 being Nat such that
A337: e1 in dom (f1 mod p) and
A338: (f1 mod p) . e1 = (Sgm (rng (f1 mod p))) . (e + n) by A292, FINSEQ_2:10, FUNCT_1:3;
A339: e1 <= (p -' 1) div 2 by A18, A95, A337, 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
A340: d1 in dom (f1 mod p) and
A341: (f1 mod p) . d1 = x by A292, A332, FINSEQ_2:10;
d1 <= (p -' 1) div 2 by A18, A95, A340, FINSEQ_3:25;
then d1 + e1 <= ((p -' 1) div 2) + ((p -' 1) div 2) by A339, XREAL_1:7;
then A342: d1 + e1 < p by A7, A11, XREAL_1:146, XXREAL_0:2;
x = (f1 . d1) mod p by A96, A340, A341, EULER_2:def 1;
then ((f1 . d1) mod p) + ((Sgm (rng (f1 mod p))) . (e + n)) = p by A336;
then ((f1 . d1) mod p) + ((f1 . e1) mod p) = p by A96, A337, A338, 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, A96, A340;
then p divides (d1 * q) + (e1 * q) by A13, A96, A337;
then A343: p divides (d1 + e1) * q ;
d1 >= 1 by A340, FINSEQ_3:25;
hence contradiction by A4, A343, A342, NAT_D:7, PEPIN:3; :: thesis: verum
end;
for d, e being Element of NAT st 1 <= d & d < e & e <= len f5 holds
f5 . d <> f5 . e
proof
let d, e be Element of NAT ; :: thesis: ( 1 <= d & d < e & e <= len f5 implies f5 . d <> f5 . e )
assume that
A344: 1 <= d and
A345: d < e and
A346: e <= len f5 ; :: thesis: f5 . d <> f5 . e
1 <= e by A344, A345, XXREAL_0:2;
then A347: e in dom f5 by A346, FINSEQ_3:25;
then A348: f5 . e = p - (((Sgm (rng (f1 mod p))) /^ n) . e) by A320;
d < len f5 by A345, A346, XXREAL_0:2;
then A349: d in dom f5 by A344, FINSEQ_3:25;
then f5 . d = p - (((Sgm (rng (f1 mod p))) /^ n) . d) by A320;
hence f5 . d <> f5 . e by A302, A318, A345, A349, A347, A348, FUNCT_1:def 4; :: thesis: verum
end;
then len f5 = card (rng f5) by GRAPH_5:7;
then f5 is one-to-one by FINSEQ_4:62;
then A350: f6 is one-to-one by A313, A331, FINSEQ_3:91;
A351: for d being Nat st d in dom f6 holds
( f6 . d > 0 & f6 . d <= (p -' 1) div 2 )
proof
let d be Nat; :: thesis: ( d in dom f6 implies ( f6 . d > 0 & f6 . d <= (p -' 1) div 2 ) )
assume A352: 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 A352, FINSEQ_1:25;
suppose A353: 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 A312, FUNCT_1:3;
then A354: ((Sgm (rng (f1 mod p))) | n) . d in Y by A299, FINSEQ_1:def 13;
then A355: ((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 A354, XBOOLE_0:def 5;
then ((Sgm (rng (f1 mod p))) | n) . d <= p / 2 by A355;
then A356: ((Sgm (rng (f1 mod p))) | n) . d <= (p -' 1) div 2 by A288, INT_1:54;
not ((Sgm (rng (f1 mod p))) | n) . d in {0} by A107, A292, A355, 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 A353, A356, FINSEQ_1:def 7; :: thesis: verum
end;
suppose ex l being Nat st
( l in dom f5 & d = (len ((Sgm (rng (f1 mod p))) | n)) + l ) ; :: thesis: ( f6 . d > 0 & f6 . d <= (p -' 1) div 2 )
then consider l being Element of NAT such that
A357: l in dom f5 and
A358: d = (len ((Sgm (rng (f1 mod p))) | n)) + l ;
f6 . d = f5 . l by A357, A358, FINSEQ_1:def 7;
hence ( f6 . d > 0 & f6 . d <= (p -' 1) div 2 ) by A322, A357; :: thesis: verum
end;
end;
end;
len f6 = (len ((Sgm (rng (f1 mod p))) | n)) + (len f5) by FINSEQ_1:22
.= (p -' 1) div 2 by A316, A317, A319 ;
then rng f6 = rng (idseq ((p -' 1) div 2)) by A314, A350, A351, Th40;
then M = Sum f6 by A350, A329, 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 A317, A315, 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 A309, A311, A312;
then A359: ((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 A359, Lm1;
then 2 divides (Sum f2) - (card X) by A181, INT_2:25;
then Sum f2, card X are_congruent_mod 2 by INT_2:15;
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, A292, Th41; :: thesis: verum
end;
hence (Lege (p,q)) * (Lege (q,p)) = (- 1) |^ (((p -' 1) div 2) * ((q -' 1) div 2)) by A130, A184, NEWTON:8; :: thesis: verum