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 ;
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 ;
p is odd by ;
then A9: p -' 1 is even by ;
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 ;
then A12: (p -' 1) div 2 < p by ;
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 ;
hence (q * (idseq ((p -' 1) div 2))) . d = q * d by A15; :: thesis: verum
end;
A16: for d being Nat st d in dom (q * (idseq ((p -' 1) div 2))) holds
(q * (idseq ((p -' 1) div 2))) . d in NAT ;
dom (q * (idseq ((p -' 1) div 2))) = dom (idseq ((p -' 1) div 2)) by VALUED_1:def 5;
then A17: len (q * (idseq ((p -' 1) div 2))) = len (idseq ((p -' 1) div 2)) by FINSEQ_3:29;
then A18: len (q * (idseq ((p -' 1) div 2))) = (p -' 1) div 2 by CARD_1:def 7;
set q9 = (q -' 1) div 2;
set g1 = p * (idseq ((q -' 1) div 2));
A19: for d being Nat st d in dom (p * (idseq ((q -' 1) div 2))) holds
(p * (idseq ((q -' 1) div 2))) . d = p * d
proof
let d be Nat; :: thesis: ( d in dom (p * (idseq ((q -' 1) div 2))) implies (p * (idseq ((q -' 1) div 2))) . d = p * d )
assume A20: d in dom (p * (idseq ((q -' 1) div 2))) ; :: thesis: (p * (idseq ((q -' 1) div 2))) . d = p * d
then d in dom (idseq ((q -' 1) div 2)) by VALUED_1:def 5;
then d in Seg (len (idseq ((q -' 1) div 2))) by FINSEQ_1:def 3;
then A21: d is Element of Seg ((q -' 1) div 2) by CARD_1:def 7;
(p * (idseq ((q -' 1) div 2))) . d = p * ((idseq ((q -' 1) div 2)) . d) by ;
hence (p * (idseq ((q -' 1) div 2))) . d = p * d by A21; :: thesis: verum
end;
A22: for d being Nat st d in dom (p * (idseq ((q -' 1) div 2))) holds
(p * (idseq ((q -' 1) div 2))) . d in NAT ;
dom (p * (idseq ((q -' 1) div 2))) = dom (idseq ((q -' 1) div 2)) by VALUED_1:def 5;
then len (p * (idseq ((q -' 1) div 2))) = len (idseq ((q -' 1) div 2)) by FINSEQ_3:29;
then A23: len (p * (idseq ((q -' 1) div 2))) = (q -' 1) div 2 by CARD_1:def 7;
reconsider g1 = p * (idseq ((q -' 1) div 2)) as FinSequence of NAT by ;
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
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;
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))) ;
reconsider f1 = q * (idseq ((p -' 1) div 2)) as FinSequence of NAT by ;
deffunc H1( 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 = H1(d) ) ) from A28: q > 1 by INT_2:def 4;
then A29: q -' 1 = q - 1 by XREAL_1:233;
then A30: q -' 1 > 0 by ;
q >= 2 + 1 by ;
then q - 1 >= 3 - 1 by XREAL_1:9;
then A31: (q -' 1) div 2 >= 1 by ;
then len (g1 mod q) >= 1 by ;
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) \/ by HEYTING3:1;
deffunc H2( 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 = H2(d) ) ) from 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 ;
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 ;
hence g1 . d = ((g2 . d) * q) + ((g1 mod q) . d) by ; :: thesis: verum
end;
q is odd by ;
then A38: q -' 1 is even by ;
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 ;
then A41: (q -' 1) div 2 < q by ;
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 ;
then A44: g1 . a = ((g2 . a) * q) + 0 by ;
a in dom g1 by ;
then p * a = (g2 . a) * q by ;
then A45: q divides p * a ;
a >= 1 by ;
then A46: q <= a by ;
a <= (q -' 1) div 2 by ;
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 ;
A49: for d, e being Nat st d in dom g1 & e in dom g1 & q divides (g1 . d) - (g1 . e) holds
d = e
proof
A50: q,p are_coprime by ;
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 ;
g1 . d = p * d by ;
then A55: q divides (d - e) * p by ;
now :: thesis: not d <> e
assume d <> e ; :: thesis: contradiction
then d - e <> 0 ;
then |.q.| <= |.(d - e).| by ;
then A56: q <= |.(d - e).| by ABSVALUE:def 1;
A57: e >= 1 by ;
A58: d >= 1 by ;
e <= (q -' 1) div 2 by ;
then A59: d - e >= 1 - ((q -' 1) div 2) by ;
A60: ((q -' 1) div 2) - 1 < q by ;
d <= (q -' 1) div 2 by ;
then d - e <= ((q -' 1) div 2) - 1 by ;
then A61: d - e < q by ;
- (((q -' 1) div 2) - 1) > - q by ;
then d - e > - q by ;
hence contradiction by A56, A61, SEQ_2:1; :: thesis: verum
end;
hence d = e ; :: thesis: verum
end;
for x, y being object st x in dom (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 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 ;
A65: g1 . y = ((g2 . y) * q) + ((g1 mod q) . y) by ;
g1 . x = ((g2 . x) * q) + ((g1 mod q) . x) by ;
then (g1 . x) - (g1 . y) = ((g2 . x) - (g2 . y)) * q by ;
then q divides (g1 . x) - (g1 . y) ;
hence x = y by A49, A25, A62, A63; :: thesis: verum
end;
then A66: g1 mod q is one-to-one ;
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 ;
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 ;
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 ;
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 ;
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 ;
dom (q * g2) = dom g2 by VALUED_1:def 5;
then A71: len (q * g2) = (q -' 1) div 2 by ;
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 ;
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 ;
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 ;
((q * g2) + (g1 mod q)) . d = ((q * g2) . d) + ((g1 mod q) . d) by ;
hence ((q * g2) + (g1 mod q)) . d = (q * (g2 . d)) + ((g1 mod q) . d) by
.= g1 . d by ;
:: thesis: verum
end;
then g1 = (q * g2) + (g1 mod q) by A73;
then A76: Sum g1 = (Sum (q * g2)) + (Sum (g1 mod q)) by
.= (q * (Sum g2)) + (Sum (g1 mod q)) by RVSUM_1:87 ;
A77: rng (g1 mod q) c= Seg n2 by ;
then A78: rng (Sgm (rng (g1 mod q))) = rng (g1 mod q) by FINSEQ_1:def 13;
then A79: XX c= Seg n2 by ;
A80: len (g1 mod q) = card (rng (Sgm (rng (g1 mod q)))) by ;
card XX <= card (rng (Sgm (rng (g1 mod q)))) by ;
then card XX <= (q -' 1) div 2 by ;
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 ;
A83: (q -' 1) div 2 = ((q -' 1) + 1) div 2 by
.= q div 2 by ;
A84: g1 mod q is FinSequence of REAL by ;
Sgm (rng (g1 mod q)) is FinSequence of REAL by ;
then A85: Sum (Sgm (rng (g1 mod q))) = Sum (g1 mod q) by ;
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 ;
for k, l being Nat st k in YY & l in XX holds
k < l
proof
let k, l be Nat; :: thesis: ( k in YY & l in XX implies k < l )
assume that
A88: k in YY and
A89: l in XX ; :: thesis: k < l
A90: not k in XX by ;
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 ;
then k <= q / 2 by A90;
hence k < l by ; :: thesis: verum
end;
then Sgm (YY \/ XX) = (Sgm YY) ^ (Sgm XX) by ;
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 ;
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 ;
A94: len (Sgm YY) = card YY by
.= ((q -' 1) div 2) - (card XX) by ;
then A95: (Sgm (rng (g1 mod q))) /^ nn = Sgm XX by ;
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;
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 ;
then A98: p - 1 >= 3 - 1 by XREAL_1:9;
then f1 mod p <> {} by ;
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) \/ by HEYTING3:1;
A100: dom f1 = dom f2 by ;
A101: 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 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 ;
hence f1 . d = ((f2 . d) * p) + ((f1 mod p) . d) by ; :: 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
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 ;
then q * a = (f2 . a) * p by ;
then A106: p divides q * a ;
a >= 1 by ;
then A107: p <= a by ;
a <= (p -' 1) div 2 by ;
hence contradiction by A12, A107, XXREAL_0:2; :: thesis: verum
end;
then A108: {0} misses rng (f1 mod p) by ZFMISC_1:50;
then A109: Sgm (rng (f1 mod p)) is one-to-one by ;
A110: for d, e being Nat st d in dom f1 & e in dom f1 & p divides (f1 . d) - (f1 . e) holds
d = e
proof
A111: q,p are_coprime by ;
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 ;
f1 . d = q * d by ;
then A116: p divides (d - e) * q by ;
now :: thesis: not d <> e
assume d <> e ; :: thesis: contradiction
then d - e <> 0 ;
then |.p.| <= |.(d - e).| by ;
then A117: p <= |.(d - e).| by ABSVALUE:def 1;
A118: e >= 1 by ;
A119: d >= 1 by ;
e <= (p -' 1) div 2 by ;
then A120: d - e >= 1 - ((p -' 1) div 2) by ;
A121: ((p -' 1) div 2) - 1 < p by ;
d <= (p -' 1) div 2 by ;
then d - e <= ((p -' 1) div 2) - 1 by ;
then A122: d - e < p by ;
- (((p -' 1) div 2) - 1) > - p by ;
then d - e > - p by ;
hence contradiction by A117, A122, SEQ_2:1; :: thesis: verum
end;
hence d = e ; :: thesis: verum
end;
for x, y being object st x in dom (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 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 ;
A126: f1 . y = ((f2 . y) * p) + ((f1 mod p) . y) by ;
f1 . x = ((f2 . x) * p) + ((f1 mod p) . x) by ;
then (f1 . x) - (f1 . y) = ((f2 . x) - (f2 . y)) * p by ;
then p divides (f1 . x) - (f1 . y) ;
hence x = y by ; :: thesis: verum
end;
then A127: f1 mod p is one-to-one ;
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 ;
A129: (Sgm (rng (g1 mod q))) | nn = Sgm YY by ;
A130: (Sgm (rng (g1 mod q))) | nn is one-to-one by ;
A131: 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));
A132: (Sgm (rng (g1 mod q))) /^ nn is FinSequence of REAL by ;
A133: len ((Sgm (rng (g1 mod q))) | nn) = nn by ;
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
.= 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
.= 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 ;
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 ; :: 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 ;
then (Sgm XX) . d in XX by ;
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 ;
((Sgm (rng (g1 mod q))) /^ nn) . d = (g1 . e) mod q by ;
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 ;
then w < q - (q / 2) by ;
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 ; :: thesis: verum
end;
A146: rng (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) c= INT by RELAT_1:def 19;
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 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 ;
hence (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d in NAT by ; :: 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;
A148: g6 is FinSequence of REAL by ;
A149: nn <= len (Sgm (rng (g1 mod q))) by ;
A150: 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 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 ;
x = q - (((Sgm (rng (g1 mod q))) /^ nn) . e) by ;
then A155: x = q - ((Sgm (rng (g1 mod q))) . (e + nn)) by ;
e + nn in dom (Sgm (rng (g1 mod q))) by ;
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 ;
A158: e1 <= (q -' 1) div 2 by ;
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 ;
d1 <= (q -' 1) div 2 by ;
then d1 + e1 <= ((q -' 1) div 2) + ((q -' 1) div 2) by ;
then A161: d1 + e1 < q by ;
A162: e1 in dom g1 by ;
then A163: (Sgm (rng (g1 mod q))) . (e + nn) = (g1 . e1) mod q by ;
A164: d1 in dom g1 by ;
then x = (g1 . d1) mod q by ;
then (((g1 . d1) mod q) + ((g1 . e1) mod q)) mod q = 0 by ;
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 ;
then q divides (d1 * p) + (e1 * p) by ;
then A165: q divides (d1 + e1) * p ;
d1 >= 1 by ;
hence contradiction by A4, A165, A161, NAT_D:7, PEPIN:3; :: thesis: verum
end;
for d, e being Nat st 1 <= d & d < e & e <= len g5 holds
g5 . d <> g5 . e
proof
let d, e be Nat; :: thesis: ( 1 <= d & d < e & e <= len g5 implies g5 . d <> g5 . e )
assume that
A166: 1 <= d and
A167: d < e and
A168: e <= len g5 ; :: thesis: g5 . d <> g5 . e
1 <= e by ;
then A169: e in dom g5 by ;
then A170: g5 . e = q - (((Sgm (rng (g1 mod q))) /^ nn) . e) by A137;
d < len g5 by ;
then A171: d in dom g5 by ;
then g5 . d = q - (((Sgm (rng (g1 mod q))) /^ nn) . d) by A137;
hence g5 . d <> g5 . e by ; :: thesis: verum
end;
then len g5 = card (rng g5) by GRAPH_5:7;
then g5 is one-to-one by FINSEQ_4:62;
then A172: g6 is one-to-one by ;
A173: for d being Nat st d in dom g6 holds
( g6 . d > 0 & g6 . d <= (q -' 1) div 2 )
proof
let d be Nat; :: thesis: ( d in dom g6 implies ( g6 . d > 0 & g6 . d <= (q -' 1) div 2 ) )
assume A174: d in dom g6 ; :: thesis: ( g6 . d > 0 & g6 . d <= (q -' 1) div 2 )
per cases ( d in dom ((Sgm (rng (g1 mod q))) | nn) or ex l being Nat st
( l in dom g5 & d = (len ((Sgm (rng (g1 mod q))) | nn)) + l ) )
by ;
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 ;
then A176: ((Sgm (rng (g1 mod q))) | nn) . d in YY by ;
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 ;
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 ;
not ((Sgm (rng (g1 mod q))) | nn) . d in by ;
then ((Sgm (rng (g1 mod q))) | nn) . d <> 0 by TARSKI:def 1;
hence ( g6 . d > 0 & g6 . d <= (q -' 1) div 2 ) by ; :: 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
A179: l in dom g5 and
A180: d = (len ((Sgm (rng (g1 mod q))) | nn)) + l ;
g6 . d = g5 . l by ;
hence ( g6 . d > 0 & g6 . d <= (q -' 1) div 2 ) by ; :: thesis: verum
end;
end;
end;
A181: idseq ((q -' 1) div 2) is FinSequence of REAL by RVSUM_1:145;
len g6 = (len ((Sgm (rng (g1 mod q))) | nn)) + (len g5) by FINSEQ_1:22
.= (q -' 1) div 2 by ;
then rng g6 = rng (idseq ((q -' 1) div 2)) by ;
then N = Sum g6 by
.= (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
.= ((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 ;
then A182: ((p -' 1) * N) mod 2 = (((q * (Sum g2)) - ((card XX) * q)) + (2 * (Sum (Sgm XX)))) mod 2 by
.= ((q * (Sum g2)) - ((card XX) * q)) mod 2 by EULER_1:12 ;
2 divides (p -' 1) * N by ;
then (q * ((Sum g2) - (card XX))) mod 2 = 0 by ;
then 2 divides q * ((Sum g2) - (card XX)) by Lm1;
then 2 divides (Sum g2) - (card XX) by ;
then Sum g2, card XX are_congruent_mod 2 ;
then (Sum g2) mod 2 = (card XX) mod 2 by NAT_D:64;
then (- 1) |^ (Sum g2) = (- 1) |^ (card XX) by Th45;
hence Lege (p,q) = (- 1) |^ (Sum g2) by A2, A5, A78, Th41; :: thesis: verum
end;
for d being Nat st d in dom (idseq ((p -' 1) div 2)) holds
(idseq ((p -' 1) div 2)) . d in NAT ;
then idseq ((p -' 1) div 2) is FinSequence of NAT by FINSEQ_2:12;
then reconsider M = Sum (idseq ((p -' 1) div 2)) as Element of NAT by Lm4;
A183: 2,p are_coprime by ;
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
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;
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))) ;
A185: (p -' 1) div 2 >= 1 by ;
A186: (Sum f2) + (Sum g2) = ((p -' 1) div 2) * ((q -' 1) div 2)
proof
reconsider A = Seg ((p -' 1) div 2), B = Seg ((q -' 1) div 2) as non empty finite Subset of NAT by ;
deffunc H3( 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 H3(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) = H3(x,y) from 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 } );
A189: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not l in x1 or l in dom z )
assume l in x1 ; :: thesis: l in dom z
then ex yy being Element of B st
( [d,yy] = l & z . (d,yy) > 0 ) ;
then l in [:A,B:] ;
hence l in dom z by FUNCT_2:def 1; :: thesis: verum
end;
hence ( x1 is Element of bool (dom z) & S1[d,x1] ) ; :: thesis: verum
end;
consider Pr being FinSequence of bool (dom z) such that
A190: ( dom Pr = Seg ((p -' 1) div 2) & ( for d being Nat st d in Seg ((p -' 1) div 2) holds
S1[d,Pr . d] ) ) from A191: dom (Card Pr) = dom Pr by CARD_3:def 2
.= dom f2 by ;
for d being Nat st d in dom (Card Pr) holds
(Card Pr) . d = f2 . d
proof
let d be Nat; :: thesis: ( d in dom (Card Pr) implies (Card Pr) . d = f2 . d )
assume A192: d in dom (Card Pr) ; :: thesis: (Card Pr) . d = f2 . d
then d in Seg ((p -' 1) div 2) by ;
then consider m being Element of A such that
A193: m = d and
A194: Pr . d = { [m,y] where y is Element of B : z . (m,y) > 0 } by A190;
Pr . d = [:{m},(Seg (f2 . m)):]
proof
set L = [:{m},(Seg (f2 . m)):];
A195: [:{m},(Seg (f2 . m)):] c= Pr . d
proof
then A197: - (q div p) = ((- q) div p) + 1 by WSIERP_1:41;
2 divides (p -' 1) * q by ;
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
.= (((p * q) - q) div p) div 2 by PRE_FF:5
.= (q + ((- (q div p)) - 1)) div 2 by
.= ((2 * ((q -' 1) div 2)) + (- (q div p))) div 2 by
.= ((q -' 1) div 2) + ((- (q div p)) div 2) by NAT_D:61 ;
A199: (((p -' 1) div 2) * q) div p <= (q -' 1) div 2
proof
per cases ) mod 2 = 0 or (q div p) mod 2 <> 0 ) ;
suppose (q div p) mod 2 = 0 ; :: thesis: (((p -' 1) div 2) * q) div p <= (q -' 1) div 2
then (- (q div p)) div 2 = - ((q div p) div 2) by WSIERP_1:42
.= - (q div (2 * p)) by NAT_2:27 ;
then (((p -' 1) div 2) * q) div p = ((q -' 1) div 2) - (q div (2 * p)) by A198;
hence (((p -' 1) div 2) * q) div p <= (q -' 1) div 2 by XREAL_1:43; :: thesis: verum
end;
suppose (q div p) mod 2 <> 0 ; :: thesis: (((p -' 1) div 2) * q) div p <= (q -' 1) div 2
then - ((q div p) div 2) = ((- (q div p)) div 2) + 1 by WSIERP_1:41;
then (- (q div p)) div 2 = (- ((q div p) div 2)) - 1
.= (- (q div (2 * p))) - 1 by NAT_2:27 ;
then (((p -' 1) div 2) * q) div p = ((q -' 1) div 2) - ((q div (2 * p)) + 1) by A198;
hence (((p -' 1) div 2) * q) div p <= (q -' 1) div 2 by XREAL_1:43; :: thesis: verum
end;
end;
end;
m <= (p -' 1) div 2 by FINSEQ_1:1;
then m * q <= ((p -' 1) div 2) * q by XREAL_1:64;
then (m * q) div p <= (((p -' 1) div 2) * q) div p by NAT_2:24;
then A200: (m * q) div p <= (q -' 1) div 2 by ;
m in Seg ((p -' 1) div 2) ;
then A201: m in dom f1 by ;
then A202: f2 . m = (f1 . m) div p by
.= (m * q) div p by ;
then A205: [\((m * q) / p)/] < (m * q) / p by INT_1:26;
let l be object ; :: according to TARSKI:def 3 :: thesis: ( not l in [:{m},(Seg (f2 . m)):] or l in Pr . d )
assume l in [:{m},(Seg (f2 . m)):] ; :: thesis: l in Pr . d
then consider x, y being object such that
A206: x in {m} and
A207: y in Seg (f2 . m) and
A208: l = [x,y] by ZFMISC_1:def 2;
reconsider y = y as Element of NAT by A207;
A209: 1 <= y by ;
y <= f2 . m by ;
then y <= (q -' 1) div 2 by ;
then reconsider y = y as Element of B by ;
y <= [\((m * q) / p)/] by ;
then y < (m * q) / p by ;
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 ; :: thesis: verum
end;
Pr . d c= [:{m},(Seg (f2 . m)):]
proof
let l be object ; :: according to TARSKI:def 3 :: thesis: ( not l in Pr . d or l in [:{m},(Seg (f2 . m)):] )
A210: m in {m} by TARSKI:def 1;
m in Seg ((p -' 1) div 2) ;
then A211: m in dom f1 by ;
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 ;
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 ;
then A214: y1 <= f2 . m by ;
y1 >= 1 by FINSEQ_1:1;
then y1 in Seg (f2 . m) by ;
hence l in [:{m},(Seg (f2 . m)):] by ; :: thesis: verum
end;
hence Pr . d = [:{m},(Seg (f2 . m)):] by ; :: thesis: verum
end;
then card (Pr . d) = card [:(Seg (f2 . m)),{m}:] by CARD_2:4
.= card (Seg (f2 . m)) by CARD_1:69 ;
then A215: card (Pr . d) = card (f2 . d) by
.= f2 . d ;
d in dom Pr by ;
hence (Card Pr) . d = f2 . d by ; :: thesis: verum
end;
then A216: Card Pr = f2 by A191;
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 } );
A217: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not l in x1 or l in dom z )
assume l in x1 ; :: thesis: l in dom z
then ex xx being Element of A st
( [xx,d] = l & z . (xx,d) < 0 ) ;
then l in [:A,B:] ;
hence l in dom z by FUNCT_2:def 1; :: thesis: verum
end;
hence ( x1 is Element of bool (dom z) & S2[d,x1] ) ; :: thesis: verum
end;
consider Pk being FinSequence of bool (dom z) such that
A218: ( dom Pk = Seg ((q -' 1) div 2) & ( for d being Nat st d in Seg ((q -' 1) div 2) holds
S2[d,Pk . d] ) ) from A219: dom (Card Pk) = Seg (len g2) by
.= dom g2 by FINSEQ_1:def 3 ;
A220: for d being Nat st d in dom (Card Pk) holds
(Card Pk) . d = g2 . d
proof
let d be Nat; :: thesis: ( d in dom (Card Pk) implies (Card Pk) . d = g2 . d )
assume A221: d in dom (Card Pk) ; :: thesis: (Card Pk) . d = g2 . d
then d in Seg ((q -' 1) div 2) by ;
then consider n being Element of B such that
A222: n = d and
A223: Pk . d = { [x,n] where x is Element of A : z . (x,n) < 0 } by A218;
Pk . d = [:(Seg (g2 . n)),{n}:]
proof
set L = [:(Seg (g2 . n)),{n}:];
A224: [:(Seg (g2 . n)),{n}:] c= Pk . d
proof
then A226: - (p div q) = ((- p) div q) + 1 by WSIERP_1:41;
2 divides (q -' 1) * p by ;
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
.= (((q * p) - p) div q) div 2 by PRE_FF:5
.= (p + ((- (p div q)) - 1)) div 2 by
.= ((2 * ((p -' 1) div 2)) - (p div q)) div 2 by
.= ((p -' 1) div 2) + ((- (p div q)) div 2) by NAT_D:61 ;
A228: (((q -' 1) div 2) * p) div q <= (p -' 1) div 2
proof
per cases ) mod 2 = 0 or (p div q) mod 2 <> 0 ) ;
suppose (p div q) mod 2 = 0 ; :: thesis: (((q -' 1) div 2) * p) div q <= (p -' 1) div 2
then (- (p div q)) div 2 = - ((p div q) div 2) by WSIERP_1:42
.= - (p div (2 * q)) by NAT_2:27 ;
then (((q -' 1) div 2) * p) div q = ((p -' 1) div 2) - (p div (2 * q)) by A227;
hence (((q -' 1) div 2) * p) div q <= (p -' 1) div 2 by XREAL_1:43; :: thesis: verum
end;
suppose (p div q) mod 2 <> 0 ; :: thesis: (((q -' 1) div 2) * p) div q <= (p -' 1) div 2
then - ((p div q) div 2) = ((- (p div q)) div 2) + 1 by WSIERP_1:41;
then (- (p div q)) div 2 = (- ((p div q) div 2)) - 1
.= (- (p div (2 * q))) - 1 by NAT_2:27 ;
then (((q -' 1) div 2) * p) div q = ((p -' 1) div 2) - ((p div (2 * q)) + 1) by A227;
hence (((q -' 1) div 2) * p) div q <= (p -' 1) div 2 by XREAL_1:43; :: thesis: verum
end;
end;
end;
n in Seg ((q -' 1) div 2) ;
then A229: n in dom g1 by ;
then A230: g2 . n = (g1 . n) div q by
.= (n * p) div q by ;
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 ;
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 ;
then A235: x <= (p -' 1) div 2 by ;
1 <= x by ;
then reconsider x = x as Element of A by ;
then [\((n * p) / q)/] < (n * p) / q by INT_1:26;
then x < (n * p) / q by ;
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 ;
then z . (x,n) < 0 by A188;
then [x,n] in Pk . d by A223;
hence l in Pk . d by ; :: thesis: verum
end;
Pk . d c= [:(Seg (g2 . n)),{n}:]
proof
let l be object ; :: according to TARSKI:def 3 :: thesis: ( not l in Pk . d or l in [:(Seg (g2 . n)),{n}:] )
A238: n in {n} by TARSKI:def 1;
n in Seg ((q -' 1) div 2) ;
then A239: n in dom g1 by ;
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 ;
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 ;
then A242: x <= g2 . n by ;
x >= 1 by FINSEQ_1:1;
then x in Seg (g2 . n) by ;
hence l in [:(Seg (g2 . n)),{n}:] by ; :: thesis: verum
end;
hence Pk . d = [:(Seg (g2 . n)),{n}:] by ; :: thesis: verum
end;
then card (Pk . d) = card (Seg (g2 . n)) by CARD_1:69;
then A243: card (Pk . d) = card (g2 . d) by
.= g2 . d ;
d in dom Pk by ;
hence (Card Pk) . d = g2 . d by ; :: thesis: verum
end;
reconsider U1 = union (rng Pr), U2 = union (rng Pk) as finite Subset of (dom z) by PROB_3:48;
dom z c= U1 \/ U2
proof
let l be object ; :: according to TARSKI:def 3 :: thesis: ( not l in dom z or l in U1 \/ U2 )
assume l in dom z ; :: thesis: l in U1 \/ U2
then consider x, y being object such that
A244: x in A and
A245: y in B and
A246: l = [x,y] by ZFMISC_1:def 2;
reconsider y = y as Element of B by A245;
reconsider x = x as Element of A by A244;
A247: z . (x,y) <> 0
proof
assume z . (x,y) = 0 ; :: thesis: contradiction
then (x / p) - (y / q) = 0 by A188;
then x * q = y * p by XCMPLX_1:95;
then A248: p divides x * q ;
A249: x <= (p -' 1) div 2 by FINSEQ_1:1;
x >= 0 + 1 by FINSEQ_1:1;
then p <= x by ;
hence contradiction by A12, A249, XXREAL_0:2; :: thesis: verum
end;
per cases ( z . (x,y) > 0 or z . (x,y) < 0 ) by A247;
suppose A250: z . (x,y) > 0 ; :: thesis: l in U1 \/ U2
S1[x,Pr . x] by A190;
then l in Pr . x by ;
then l in Union Pr by ;
hence l in U1 \/ U2 by XBOOLE_0:def 3; :: thesis: verum
end;
suppose A251: z . (x,y) < 0 ; :: thesis: l in U1 \/ U2
S2[y,Pk . y] by A218;
then l in Pk . y by ;
then l in Union Pk by ;
hence l in U1 \/ U2 by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
then A252: U1 \/ U2 = dom z by XBOOLE_0:def 10;
A253: U1 misses U2
proof
assume U1 meets U2 ; :: thesis: contradiction
then consider l being object such that
A254: l in U1 and
A255: l in U2 by XBOOLE_0:3;
l in Union Pk by A255;
then consider k2 being Nat such that
A256: k2 in dom Pk and
A257: l in Pk . k2 by PROB_3:49;
l in Union Pr by A254;
then consider k1 being Nat such that
A258: k1 in dom Pr and
A259: l in Pr . k1 by PROB_3:49;
reconsider k1 = k1, k2 = k2 as Element of NAT by ORDINAL1:def 12;
consider n1 being Element of B such that
n1 = k2 and
A260: Pk . k2 = { [x,n1] where x is Element of A : z . (x,n1) < 0 } by ;
consider n2 being Element of A such that
A261: l = [n2,n1] and
A262: z . (n2,n1) < 0 by ;
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 ;
A264: ex m2 being Element of B st
( l = [m1,m2] & z . (m1,m2) > 0 ) by ;
then m1 = n2 by ;
hence contradiction by A264, A261, A262, XTUPLE_0:1; :: thesis: verum
end;
A265: for d, e being Nat st d in dom Pk & e in dom Pk & d <> e holds
Pk . d misses Pk . e
proof
let d, e be Nat; :: thesis: ( d in dom Pk & e in dom Pk & d <> e implies Pk . d misses Pk . e )
assume that
A266: d in dom Pk and
A267: e in dom Pk and
A268: d <> e ; :: thesis: Pk . d misses Pk . e
consider y2 being Element of B such that
A269: y2 = e and
A270: Pk . e = { [x,y2] where x is Element of A : z . (x,y2) < 0 } by ;
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 ;
now :: thesis: Pk . d misses Pk . e
assume not Pk . d misses Pk . e ; :: thesis: contradiction
then consider l being object such that
A273: l in Pk . d and
A274: l in Pk . e by XBOOLE_0:3;
A275: ex x2 being Element of A st
( l = [x2,y2] & z . (x2,y2) < 0 ) by ;
ex x1 being Element of A st
( l = [x1,y1] & z . (x1,y1) < 0 ) by ;
hence contradiction by A268, A271, A269, A275, XTUPLE_0:1; :: thesis: verum
end;
hence Pk . d misses Pk . e ; :: thesis: verum
end;
A276: card (union (rng Pk)) = Sum (Card Pk) by ;
A277: for d, e being Nat st d in dom Pr & e in dom Pr & d <> e holds
Pr . d misses Pr . e
proof
let d, e be Nat; :: thesis: ( d in dom Pr & e in dom Pr & d <> e implies Pr . d misses Pr . e )
assume that
A278: d in dom Pr and
A279: e in dom Pr and
A280: d <> e ; :: thesis: Pr . d misses Pr . e
consider x2 being Element of A such that
A281: x2 = e and
A282: Pr . e = { [x2,y] where y is Element of B : z . (x2,y) > 0 } by ;
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 ;
now :: thesis: Pr . d misses Pr . e
assume not Pr . d misses Pr . e ; :: thesis: contradiction
then consider l being object such that
A285: l in Pr . d and
A286: l in Pr . e by XBOOLE_0:3;
A287: ex y2 being Element of B st
( l = [x2,y2] & z . (x2,y2) > 0 ) by ;
ex y1 being Element of B st
( l = [x1,y1] & z . (x1,y1) > 0 ) by ;
hence contradiction by A280, A283, A281, A287, XTUPLE_0:1; :: thesis: verum
end;
hence Pr . d misses Pr . e ; :: thesis: verum
end;
card (union (rng Pr)) = Sum (Card Pr) by ;
then card (U1 \/ U2) = (Sum (Card Pr)) + (Sum (Card Pk)) by ;
then (Sum (Card Pr)) + (Sum (Card Pk)) = card [:A,B:] by
.= (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 ; :: thesis: verum
end;
dom (p * f2) = dom f2 by VALUED_1:def 5;
then A288: len (p * f2) = (p -' 1) div 2 by ;
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 ;
A290: (p -' 1) div 2 = ((p -' 1) + 1) div 2 by
.= p div 2 by ;
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 ;
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 ;
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 ;
A293: rng (f1 mod p) c= Seg n1 by ;
then A294: rng (Sgm (rng (f1 mod p))) = rng (f1 mod p) by FINSEQ_1:def 13;
then A295: X c= Seg n1 by ;
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 ;
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 A297: d in dom f1 ; :: thesis: f1 . d = ((p * f2) + (f1 mod p)) . d
then A298: d in dom (p * f2) by ;
((p * f2) + (f1 mod p)) . d = ((p * f2) . d) + ((f1 mod p) . d) by ;
hence ((p * f2) + (f1 mod p)) . d = (p * (f2 . d)) + ((f1 mod p) . d) by
.= f1 . d by ;
:: thesis: verum
end;
then f1 = (p * f2) + (f1 mod p) by A296;
then A299: Sum f1 = (Sum (p * f2)) + (Sum (f1 mod p)) by
.= (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 ;
A302: len (f1 mod p) = card (rng (Sgm (rng (f1 mod p)))) by ;
then reconsider n = ((p -' 1) div 2) - (card X) as Element of NAT by ;
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 ;
A305: f1 mod p is FinSequence of REAL by ;
Sgm (rng (f1 mod p)) is FinSequence of REAL by ;
then A306: Sum (Sgm (rng (f1 mod p))) = Sum (f1 mod p) by ;
for k, l being Nat st k in Y & l in X holds
k < l
proof
let k, l be Nat; :: thesis: ( k in Y & l in X implies k < l )
assume that
A307: k in Y and
A308: l in X ; :: thesis: k < l
A309: not k in X by ;
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 ;
then k <= p / 2 by A309;
hence k < l by ; :: thesis: verum
end;
then Sgm (Y \/ X) = (Sgm Y) ^ (Sgm X) by ;
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 ;
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 ;
A313: len (Sgm Y) = card Y by
.= ((p -' 1) div 2) - (card X) by ;
then A314: (Sgm (rng (f1 mod p))) /^ n = Sgm X by ;
A315: (Sgm (rng (f1 mod p))) | n = Sgm Y by ;
A316: (Sgm (rng (f1 mod p))) | n is one-to-one by ;
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));
A317: (Sgm (rng (f1 mod p))) /^ n is FinSequence of REAL by ;
A318: len ((Sgm (rng (f1 mod p))) | n) = n by ;
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
.= 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
.= 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
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 ;
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 ; :: thesis: verum
end;
A324: 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 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 ;
then (Sgm X) . d in X by ;
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 ;
((Sgm (rng (f1 mod p))) /^ n) . d = (f1 . e) mod p by ;
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 ;
then w < p - (p / 2) by ;
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 ; :: thesis: verum
end;
A331: rng (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) c= INT by RELAT_1:def 19;
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 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 ;
hence (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d in NAT by ; :: 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;
A333: f6 is FinSequence of REAL by ;
A334: n <= len (Sgm (rng (f1 mod p))) by ;
A335: 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 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 ;
x = p - (((Sgm (rng (f1 mod p))) /^ n) . e) by ;
then A340: x = p - ((Sgm (rng (f1 mod p))) . (e + n)) by ;
e + n in dom (Sgm (rng (f1 mod p))) by ;
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 ;
A343: e1 <= (p -' 1) div 2 by ;
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 ;
d1 <= (p -' 1) div 2 by ;
then d1 + e1 <= ((p -' 1) div 2) + ((p -' 1) div 2) by ;
then A346: d1 + e1 < p by ;
x = (f1 . d1) mod p by ;
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 ;
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 ;
then p divides (d1 * q) + (e1 * q) by ;
then A347: p divides (d1 + e1) * q ;
d1 >= 1 by ;
hence contradiction by A4, A347, A346, NAT_D:7, PEPIN:3; :: thesis: verum
end;
for d, e being Nat st 1 <= d & d < e & e <= len f5 holds
f5 . d <> f5 . e
proof
let d, e be Nat; :: thesis: ( 1 <= d & d < e & e <= len f5 implies f5 . d <> f5 . e )
assume that
A348: 1 <= d and
A349: d < e and
A350: e <= len f5 ; :: thesis: f5 . d <> f5 . e
1 <= e by ;
then A351: e in dom f5 by ;
then A352: f5 . e = p - (((Sgm (rng (f1 mod p))) /^ n) . e) by A322;
d < len f5 by ;
then A353: d in dom f5 by ;
then f5 . d = p - (((Sgm (rng (f1 mod p))) /^ n) . d) by A322;
hence f5 . d <> f5 . e by ; :: thesis: verum
end;
then len f5 = card (rng f5) by GRAPH_5:7;
then f5 is one-to-one by FINSEQ_4:62;
then A354: f6 is one-to-one by ;
A355: for d being Nat st d in dom f6 holds
( f6 . d > 0 & f6 . d <= (p -' 1) div 2 )
proof
let d be Nat; :: thesis: ( d in dom f6 implies ( f6 . d > 0 & f6 . d <= (p -' 1) div 2 ) )
assume A356: d in dom f6 ; :: thesis: ( f6 . d > 0 & f6 . d <= (p -' 1) div 2 )
per cases ( d in dom ((Sgm (rng (f1 mod p))) | n) or ex l being Nat st
( l in dom f5 & d = (len ((Sgm (rng (f1 mod p))) | n)) + l ) )
by ;
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 ;
then A358: ((Sgm (rng (f1 mod p))) | n) . d in Y by ;
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 ;
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 ;
not ((Sgm (rng (f1 mod p))) | n) . d in by ;
then ((Sgm (rng (f1 mod p))) | n) . d <> 0 by TARSKI:def 1;
hence ( f6 . d > 0 & f6 . d <= (p -' 1) div 2 ) by ; :: 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
A361: l in dom f5 and
A362: d = (len ((Sgm (rng (f1 mod p))) | n)) + l ;
f6 . d = f5 . l by ;
hence ( f6 . d > 0 & f6 . d <= (p -' 1) div 2 ) by ; :: thesis: verum
end;
end;
end;
A363: idseq ((p -' 1) div 2) is FinSequence of REAL by RVSUM_1:145;
len f6 = (len ((Sgm (rng (f1 mod p))) | n)) + (len f5) by FINSEQ_1:22
.= (p -' 1) div 2 by ;
then rng f6 = rng (idseq ((p -' 1) div 2)) by ;
then M = Sum f6 by
.= (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
.= ((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 ;
then A364: ((q -' 1) * M) mod 2 = (((p * (Sum f2)) - ((card X) * p)) + (2 * (Sum (Sgm X)))) mod 2 by
.= ((p * (Sum f2)) - ((card X) * p)) mod 2 by EULER_1:12 ;
2 divides (q -' 1) * M by ;
then ((q -' 1) * M) mod 2 = 0 by PEPIN:6;
then 2 divides p * ((Sum f2) - (card X)) by ;
then Sum f2, card X are_congruent_mod 2 by ;
then (Sum f2) mod 2 = (card X) mod 2 by NAT_D:64;
then (- 1) |^ (Sum f2) = (- 1) |^ (card X) by Th45;
hence Lege (q,p) = (- 1) |^ (Sum f2) by A1, A5, A294, Th41; :: thesis: verum
end;
hence (Lege (p,q)) * (Lege (q,p)) = (- 1) |^ (((p -' 1) div 2) * ((q -' 1) div 2)) by ; :: thesis: verum