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 A1:
( p > 2 & q > 2 & p <> q )
; :: thesis: (Lege p,q) * (Lege q,p) = (- 1) |^ (((p -' 1) div 2) * ((q -' 1) div 2))
then A2:
q,p are_relative_prime
by INT_2:47;
then A3:
q gcd p = 1
by INT_2:def 4;
reconsider p = p, q = q as prime Element of NAT by ORDINAL1:def 13;
A4:
( 2,p are_relative_prime & 2,q are_relative_prime )
by A1, EULER_1:3;
set p' = (p -' 1) div 2;
set q' = (q -' 1) div 2;
set f1 = q * (idseq ((p -' 1) div 2));
dom (q * (idseq ((p -' 1) div 2))) = dom (idseq ((p -' 1) div 2))
by VALUED_1:def 5;
then A5:
len (q * (idseq ((p -' 1) div 2))) = len (idseq ((p -' 1) div 2))
by FINSEQ_3:31;
then A6:
len (q * (idseq ((p -' 1) div 2))) = (p -' 1) div 2
by FINSEQ_1:def 18;
A7:
( p > 1 & q > 1 )
by INT_2:def 5;
then A8:
( p -' 1 = p - 1 & q -' 1 = q - 1 )
by XREAL_1:235;
( p >= 2 + 1 & q >= 2 + 1 )
by A1, NAT_1:13;
then
( p - 1 >= 3 - 1 & q - 1 >= 3 - 1 )
by XREAL_1:11;
then A9:
( (p -' 1) div 2 >= 1 & (q -' 1) div 2 >= 1 )
by A8, NAT_2:15;
( not p is even & not q is even )
by A1, PEPIN:17;
then A10:
( p -' 1 is even & q -' 1 is even )
by A8, HILBERT3:2;
then A11:
( 2 divides p -' 1 & 2 divides q -' 1 )
by PEPIN:22;
then A12:
( p -' 1 = 2 * ((p -' 1) div 2) & q -' 1 = 2 * ((q -' 1) div 2) )
by NAT_D:3;
then A13:
( (p -' 1) div 2 divides p -' 1 & (q -' 1) div 2 divides q -' 1 )
by NAT_D:def 3;
( p -' 1 > 0 & q -' 1 > 0 )
by A7, A8, XREAL_1:52;
then
( (p -' 1) div 2 <= p -' 1 & (q -' 1) div 2 <= q -' 1 )
by A13, NAT_D:7;
then A14:
( (p -' 1) div 2 < p & (q -' 1) div 2 < q )
by A8, XREAL_1:148, XXREAL_0:2;
A15: (p -' 1) div 2 =
((p -' 1) + 1) div 2
by A10, NAT_2:28
.=
p div 2
by A7, XREAL_1:237
;
A16: (q -' 1) div 2 =
((q -' 1) + 1) div 2
by A10, NAT_2:28
.=
q div 2
by A7, XREAL_1:237
;
A17:
for d being Nat st d in dom (q * (idseq ((p -' 1) div 2))) holds
(q * (idseq ((p -' 1) div 2))) . d = q * d
for d being Nat st d in dom (q * (idseq ((p -' 1) div 2))) holds
(q * (idseq ((p -' 1) div 2))) . d in NAT
then reconsider f1 = q * (idseq ((p -' 1) div 2)) as FinSequence of NAT by FINSEQ_2:14;
A20:
for d, e being Nat st d in dom f1 & e in dom f1 & p divides (f1 . d) - (f1 . e) holds
d = e
proof
let d,
e be
Nat;
:: thesis: ( d in dom f1 & e in dom f1 & p divides (f1 . d) - (f1 . e) implies d = e )
assume A21:
(
d in dom f1 &
e in dom f1 &
p divides (f1 . d) - (f1 . e) )
;
:: thesis: d = e
then
(
f1 . d = q * d &
f1 . e = q * e )
by A17;
then A22:
p divides (d - e) * q
by A21;
A23:
q,
p are_relative_prime
by A1, INT_2:47;
now assume
d <> e
;
:: thesis: contradictionthen
d - e <> 0
;
then
abs p <= abs (d - e)
by A22, A23, INT_2:40, INT_4:6;
then A24:
p <= abs (d - e)
by ABSVALUE:def 1;
(
d >= 1 &
d <= (p -' 1) div 2 &
e >= 1 &
e <= (p -' 1) div 2 )
by A6, A21, FINSEQ_3:27;
then A25:
(
d - e <= ((p -' 1) div 2) - 1 &
d - e >= 1
- ((p -' 1) div 2) )
by XREAL_1:15;
A26:
((p -' 1) div 2) - 1
< p
by A14, XREAL_1:149;
then A27:
d - e < p
by A25, XXREAL_0:2;
- (((p -' 1) div 2) - 1) > - p
by A26, XREAL_1:26;
then
d - e > - p
by A25, XXREAL_0:2;
hence
contradiction
by A24, A27, SEQ_2:9;
:: thesis: verum end;
hence
d = e
;
:: thesis: verum
end;
deffunc H1( Nat) -> Element of NAT = (f1 . $1) div p;
consider f2 being FinSequence such that
A28:
( 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();
for d being Nat st d in dom f2 holds
f2 . d in NAT
then reconsider f2 = f2 as FinSequence of NAT by FINSEQ_2:14;
set f3 = f1 mod p;
A29:
len (f1 mod p) = len f1
by EULER_2:def 1;
then A30:
dom f1 = dom (f1 mod p)
by FINSEQ_3:31;
A31:
dom f1 = dom f2
by A6, A28, FINSEQ_3:31;
A32: 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 A30, A31
;
A33:
for d being Nat st d in dom f1 holds
f1 . d = ((f2 . d) * p) + ((f1 mod p) . d)
for d being Nat st d in dom f1 holds
f1 . d = ((p * f2) + (f1 mod p)) . d
then A36:
f1 = (p * f2) + (f1 mod p)
by A32, FINSEQ_1:17;
A37:
( p * f2 is Element of NAT * & f1 mod p is Element of NAT * )
by FINSEQ_1:def 11;
dom (p * f2) = dom f2
by VALUED_1:def 5;
then
( len (p * f2) = (p -' 1) div 2 & len (f1 mod p) = (p -' 1) div 2 )
by A5, A28, A29, FINSEQ_1:def 18, FINSEQ_3:31;
then
( p * f2 in ((p -' 1) div 2) -tuples_on NAT & f1 mod p in ((p -' 1) div 2) -tuples_on NAT )
by A37;
then
( p * f2 is Element of ((p -' 1) div 2) -tuples_on REAL & f1 mod p is Element of ((p -' 1) div 2) -tuples_on REAL )
by FINSEQ_2:129;
then A38: Sum f1 =
(Sum (p * f2)) + (Sum (f1 mod p))
by A36, RVSUM_1:119
.=
(p * (Sum f2)) + (Sum (f1 mod p))
by RVSUM_1:117
;
then A39:
q * (Sum (idseq ((p -' 1) div 2))) = (p * (Sum f2)) + (Sum (f1 mod p))
by RVSUM_1:117;
f1 mod p <> {}
by A6, A9, A29;
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
A40:
rng (f1 mod p) c= (Seg n1) \/ {0 }
by HEYTING3:3;
not 0 in rng (f1 mod p)
proof
assume
0 in rng (f1 mod p)
;
:: thesis: contradiction
then consider a being
Nat such that A41:
(
a in dom (f1 mod p) &
(f1 mod p) . a = 0 )
by FINSEQ_2:11;
f1 . a = ((f2 . a) * p) + 0
by A30, A33, A41;
then
q * a = (f2 . a) * p
by A17, A30, A41;
then A42:
p divides q * a
by NAT_D:def 3;
A43:
(
a >= 1 &
a <= (p -' 1) div 2 )
by A6, A29, A41, FINSEQ_3:27;
then
p <= a
by A2, A42, NAT_D:7, PEPIN:3;
hence
contradiction
by A14, A43, XXREAL_0:2;
:: thesis: verum
end;
then A44:
{0 } misses rng (f1 mod p)
by ZFMISC_1:56;
then A45:
rng (f1 mod p) c= Seg n1
by A40, XBOOLE_1:73;
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
then A47:
f1 mod p is one-to-one
by FUNCT_1:def 8;
set f4 = Sgm (rng (f1 mod p));
set X = { k where k is Element of NAT : ( k in rng (Sgm (rng (f1 mod p))) & k > p / 2 ) } ;
A48:
rng (Sgm (rng (f1 mod p))) = rng (f1 mod p)
by A45, FINSEQ_1:def 13;
A49:
Sgm (rng (f1 mod p)) is one-to-one
by A40, A44, FINSEQ_3:99, XBOOLE_1:73;
( Sgm (rng (f1 mod p)) is FinSequence of REAL & f1 mod p is FinSequence of REAL )
by FINSEQ_2:27;
then A50:
Sum (Sgm (rng (f1 mod p))) = Sum (f1 mod p)
by A47, A48, A49, RFINSEQ:22, RFINSEQ:39;
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)))
then A52:
{ 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;
then 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 XBOOLE_1:1;
A53:
X c= Seg n1
by A45, A48, A52, XBOOLE_1:1;
reconsider Y = (rng (Sgm (rng (f1 mod p)))) \ X as finite Subset of NAT ;
A54:
(rng (Sgm (rng (f1 mod p)))) \ X c= rng (Sgm (rng (f1 mod p)))
by XBOOLE_1:36;
then A55:
Y c= Seg n1
by A45, A48, XBOOLE_1:1;
set m = card X;
A56:
len (f1 mod p) = card (rng (Sgm (rng (f1 mod p))))
by A47, A48, FINSEQ_4:77;
then reconsider n = ((p -' 1) div 2) - (card X) as Element of NAT by A6, A29, A52, NAT_1:21, NAT_1:44;
len (f1 mod p) = card (rng (f1 mod p))
by A47, FINSEQ_4:77;
then A57:
len (Sgm (rng (f1 mod p))) = (p -' 1) div 2
by A6, A29, A40, A44, FINSEQ_3:44, XBOOLE_1:73;
A58:
Sgm (rng (f1 mod p)) = (Sgm Y) ^ (Sgm X)
then
Sum (Sgm (rng (f1 mod p))) = (Sum (Sgm Y)) + (Sum (Sgm X))
by RVSUM_1:105;
then A61:
q * (Sum (idseq ((p -' 1) div 2))) = ((p * (Sum f2)) + (Sum (Sgm Y))) + (Sum (Sgm X))
by A38, A50, RVSUM_1:117;
A62:
len (Sgm Y) = n
then A63:
(Sgm (rng (f1 mod p))) /^ n = Sgm X
by A58, FINSEQ_5:40;
Sgm (rng (f1 mod p)) = ((Sgm (rng (f1 mod p))) | n) ^ ((Sgm (rng (f1 mod p))) /^ n)
by RFINSEQ:21;
then A64:
( (Sgm (rng (f1 mod p))) | n is one-to-one & (Sgm (rng (f1 mod p))) /^ n is one-to-one )
by A49, FINSEQ_3:98;
A65:
(Sgm (rng (f1 mod p))) | n = Sgm Y
by A58, A62, FINSEQ_3:122, FINSEQ_6:12;
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:14;
then reconsider M = Sum (idseq ((p -' 1) div 2)) as Element of NAT by Lm3;
A67:
Lege q,p = (- 1) |^ (Sum f2)
proof
per cases
( X is empty or not X is empty )
;
suppose A68:
X is
empty
;
:: thesis: Lege q,p = (- 1) |^ (Sum f2)
for
d being
Nat st
d in dom (Sgm (rng (f1 mod p))) holds
(
(Sgm (rng (f1 mod p))) . d > 0 &
(Sgm (rng (f1 mod p))) . d <= (p -' 1) div 2 )
then
Sgm (rng (f1 mod p)) = Sgm (Seg ((p -' 1) div 2))
by A48, A49, A57, Th40;
then
q * (Sum (idseq ((p -' 1) div 2))) = (p * (Sum f2)) + (Sum (idseq ((p -' 1) div 2)))
by A39, A50, FINSEQ_3:54;
then A73:
(q * (Sum (idseq ((p -' 1) div 2)))) - (Sum (idseq ((p -' 1) div 2))) = p * (Sum f2)
;
2
divides (q -' 1) * M
by A11, NAT_D:9;
then
2
divides (Sum f2) - 0
by A4, A8, A73, PEPIN:3;
then
Sum f2,
0 are_congruent_mod 2
by INT_2:19;
then
(Sum f2) mod 2
= 0 mod 2
by INT_3:12;
then
(- 1) |^ (card X) = (- 1) |^ (Sum f2)
by A68, Th45, CARD_1:47;
hence
Lege q,
p = (- 1) |^ (Sum f2)
by A1, A3, A48, Th41;
:: thesis: verum suppose
not
X is
empty
;
:: thesis: Lege q,p = (- 1) |^ (Sum f2)A75:
n <= len (Sgm (rng (f1 mod p)))
by A57, XREAL_1:45;
A76:
len ((Sgm (rng (f1 mod p))) | n) = n
by A57, FINSEQ_1:80, XREAL_1:45;
A77:
len ((Sgm (rng (f1 mod p))) /^ n) =
(len (Sgm (rng (f1 mod p)))) -' n
by RFINSEQ:42
.=
(len (Sgm (rng (f1 mod p)))) - n
by A57, XREAL_1:45, XREAL_1:235
.=
card X
by A57
;
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));
A78:
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 A77, FINSEQ_1:def 18
.=
(dom ((Sgm (rng (f1 mod p))) /^ n)) /\ (dom ((Sgm (rng (f1 mod p))) /^ n))
by FINSEQ_1:def 3
.=
dom ((Sgm (rng (f1 mod p))) /^ n)
;
then A79:
len (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) = len ((Sgm (rng (f1 mod p))) /^ n)
by FINSEQ_3:31;
A80:
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)
A82:
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 ) )
assume A83:
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 A84:
(((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d = p - (((Sgm (rng (f1 mod p))) /^ n) . d)
by A80;
reconsider w =
(((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d as
Element of
INT by INT_1:def 2;
(Sgm X) . d in rng (Sgm X)
by A63, A78, A83, FUNCT_1:12;
then
(Sgm X) . d in X
by A53, FINSEQ_1:def 13;
then consider ll being
Element of
NAT such that A85:
(
ll = (Sgm X) . d &
ll in rng (f1 mod p) &
ll > p / 2 )
by A48;
A86:
w < p - (p / 2)
by A63, A84, A85, XREAL_1:12;
consider e being
Nat such that A87:
(
e in dom (f1 mod p) &
(f1 mod p) . e = ((Sgm (rng (f1 mod p))) /^ n) . d )
by A63, A85, FINSEQ_2:11;
((Sgm (rng (f1 mod p))) /^ n) . d = (f1 . e) mod p
by A30, A87, EULER_2:def 1;
then
((Sgm (rng (f1 mod p))) /^ n) . d < p
by NAT_D:1;
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 A15, A84, A86, INT_1:81, XREAL_1:52;
:: thesis: verum
end;
for
d being
Nat st
d in dom (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) holds
(((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) . d in NAT
then reconsider f5 =
((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n) as
FinSequence of
NAT by FINSEQ_2:14;
for
d,
e being
Element of
NAT st 1
<= d &
d < e &
e <= len f5 holds
f5 . d <> f5 . e
then
len f5 = card (rng f5)
by GRAPH_5:10;
then A90:
f5 is
one-to-one
by FINSEQ_4:77;
(
(Sgm (rng (f1 mod p))) | n is
FinSequence of
NAT &
f5 is
FinSequence of
NAT )
;
then reconsider f6 =
((Sgm (rng (f1 mod p))) | n) ^ (((card X) |-> p) - ((Sgm (rng (f1 mod p))) /^ n)) as
FinSequence of
NAT by FINSEQ_1:96;
A91:
len f6 =
(len ((Sgm (rng (f1 mod p))) | n)) + (len f5)
by FINSEQ_1:35
.=
(p -' 1) div 2
by A76, A77, A79
;
A92:
rng (idseq ((p -' 1) div 2)) = Seg ((p -' 1) div 2)
by RELAT_1:71;
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 A93:
(
x in rng ((Sgm (rng (f1 mod p))) | n) &
x in rng f5 )
by XBOOLE_0:3;
rng ((Sgm (rng (f1 mod p))) | n) c= rng (Sgm (rng (f1 mod p)))
by FINSEQ_5:21;
then consider d1 being
Nat such that A94:
(
d1 in dom (f1 mod p) &
(f1 mod p) . d1 = x )
by A48, A93, FINSEQ_2:11;
A95:
x = (f1 . d1) mod p
by A30, A94, EULER_2:def 1;
consider e being
Nat such that A96:
(
e in dom f5 &
f5 . e = x )
by A93, FINSEQ_2:11;
x = p - (((Sgm (rng (f1 mod p))) /^ n) . e)
by A80, A96;
then
x = p - ((Sgm (rng (f1 mod p))) . (e + n))
by A75, A78, A96, RFINSEQ:def 2;
then A97:
((f1 . d1) mod p) + ((Sgm (rng (f1 mod p))) . (e + n)) = p
by A95;
e + n in dom (Sgm (rng (f1 mod p)))
by A78, A96, FINSEQ_5:29;
then
(Sgm (rng (f1 mod p))) . (e + n) in rng (f1 mod p)
by A48, FUNCT_1:12;
then consider e1 being
Nat such that A98:
(
e1 in dom (f1 mod p) &
(f1 mod p) . e1 = (Sgm (rng (f1 mod p))) . (e + n) )
by FINSEQ_2:11;
((f1 . d1) mod p) + ((f1 . e1) mod p) = p
by A30, A97, A98, EULER_2:def 1;
then
(((f1 . d1) mod p) + ((f1 . e1) mod p)) mod p = 0
by NAT_D:25;
then
((f1 . d1) + (f1 . e1)) mod p = 0
by EULER_2:8;
then
p divides (f1 . d1) + (f1 . e1)
by PEPIN:6;
then
p divides (d1 * q) + (f1 . e1)
by A17, A30, A94;
then
p divides (d1 * q) + (e1 * q)
by A17, A30, A98;
then A99:
p divides (d1 + e1) * q
;
(
d1 >= 1 &
d1 <= (p -' 1) div 2 &
e1 >= 1 &
e1 <= (p -' 1) div 2 )
by A6, A29, A94, A98, FINSEQ_3:27;
then
(
d1 + e1 >= 1
+ 1 &
d1 + e1 <= ((p -' 1) div 2) + ((p -' 1) div 2) )
by XREAL_1:9;
then
(
d1 + e1 > 0 &
d1 + e1 < p )
by A8, A12, XREAL_1:148, XXREAL_0:2;
hence
contradiction
by A2, A99, NAT_D:7, PEPIN:3;
:: thesis: verum
end; then A100:
f6 is
one-to-one
by A64, A90, FINSEQ_3:98;
for
d being
Nat st
d in dom f6 holds
(
f6 . d > 0 &
f6 . d <= (p -' 1) div 2 )
then A106:
rng f6 = rng (idseq ((p -' 1) div 2))
by A91, A92, A100, Th40;
A107:
(
f6 is
FinSequence of
REAL &
(Sgm (rng (f1 mod p))) /^ n is
FinSequence of
REAL )
by FINSEQ_2:27;
then M =
Sum f6
by A100, A106, RFINSEQ:22, RFINSEQ:39
.=
(Sum ((Sgm (rng (f1 mod p))) | n)) + (Sum f5)
by RVSUM_1:105
.=
(Sum ((Sgm (rng (f1 mod p))) | n)) + (((card X) * p) - (Sum ((Sgm (rng (f1 mod p))) /^ n)))
by A77, A107, 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 A61, A63, A65;
then A108:
((q -' 1) * M) mod 2 =
(((p * (Sum f2)) - ((card X) * p)) + (2 * (Sum (Sgm X)))) mod 2
by A7, XREAL_1:235
.=
((p * (Sum f2)) - ((card X) * p)) mod 2
by EULER_1:13
;
2
divides (q -' 1) * M
by A11, NAT_D:9;
then
((q -' 1) * M) mod 2
= 0
by PEPIN:6;
then
2
divides p * ((Sum f2) - (card X))
by A108, Lm1;
then
2
divides (Sum f2) - (card X)
by A4, INT_2:40;
then
Sum f2,
card X are_congruent_mod 2
by INT_2:19;
then
(Sum f2) mod 2
= (card X) mod 2
by INT_3:12;
then
(- 1) |^ (Sum f2) = (- 1) |^ (card X)
by Th45;
hence
Lege q,
p = (- 1) |^ (Sum f2)
by A1, A3, A48, Th41;
:: thesis: verum end;
end;
set g1 = p * (idseq ((q -' 1) div 2));
dom (p * (idseq ((q -' 1) div 2))) = dom (idseq ((q -' 1) div 2))
by VALUED_1:def 5;
then
len (p * (idseq ((q -' 1) div 2))) = len (idseq ((q -' 1) div 2))
by FINSEQ_3:31;
then A109:
len (p * (idseq ((q -' 1) div 2))) = (q -' 1) div 2
by FINSEQ_1:def 18;
A110:
for d being Nat st d in dom (p * (idseq ((q -' 1) div 2))) holds
(p * (idseq ((q -' 1) div 2))) . d = p * d
for d being Nat st d in dom (p * (idseq ((q -' 1) div 2))) holds
(p * (idseq ((q -' 1) div 2))) . d in NAT
then reconsider g1 = p * (idseq ((q -' 1) div 2)) as FinSequence of NAT by FINSEQ_2:14;
A113:
for d, e being Nat st d in dom g1 & e in dom g1 & q divides (g1 . d) - (g1 . e) holds
d = e
proof
let d,
e be
Nat;
:: thesis: ( d in dom g1 & e in dom g1 & q divides (g1 . d) - (g1 . e) implies d = e )
assume A114:
(
d in dom g1 &
e in dom g1 &
q divides (g1 . d) - (g1 . e) )
;
:: thesis: d = e
then
(
g1 . d = p * d &
g1 . e = p * e )
by A110;
then A115:
q divides (d - e) * p
by A114;
A116:
q,
p are_relative_prime
by A1, INT_2:47;
now assume
d <> e
;
:: thesis: contradictionthen
d - e <> 0
;
then
abs q <= abs (d - e)
by A115, A116, INT_2:40, INT_4:6;
then A117:
q <= abs (d - e)
by ABSVALUE:def 1;
(
d >= 1 &
d <= (q -' 1) div 2 &
e >= 1 &
e <= (q -' 1) div 2 )
by A109, A114, FINSEQ_3:27;
then A118:
(
d - e <= ((q -' 1) div 2) - 1 &
d - e >= 1
- ((q -' 1) div 2) )
by XREAL_1:15;
A119:
((q -' 1) div 2) - 1
< q
by A14, XREAL_1:149;
then A120:
d - e < q
by A118, XXREAL_0:2;
- (((q -' 1) div 2) - 1) > - q
by A119, XREAL_1:26;
then
d - e > - q
by A118, XXREAL_0:2;
hence
contradiction
by A117, A120, SEQ_2:9;
:: thesis: verum end;
hence
d = e
;
:: thesis: verum
end;
deffunc H2( Nat) -> Element of NAT = (g1 . $1) div q;
consider g2 being FinSequence such that
A121:
( 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
then reconsider g2 = g2 as FinSequence of NAT by FINSEQ_2:14;
set g3 = g1 mod q;
A122:
len (g1 mod q) = len g1
by EULER_2:def 1;
then A123:
dom g1 = dom (g1 mod q)
by FINSEQ_3:31;
A124:
dom g1 = dom g2
by A109, A121, FINSEQ_3:31;
A125: 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 A123, A124
;
A126:
for d being Nat st d in dom g1 holds
g1 . d = ((g2 . d) * q) + ((g1 mod q) . d)
for d being Nat st d in dom g1 holds
g1 . d = ((q * g2) + (g1 mod q)) . d
then A129:
g1 = (q * g2) + (g1 mod q)
by A125, FINSEQ_1:17;
A130:
( q * g2 is Element of NAT * & g1 mod q is Element of NAT * )
by FINSEQ_1:def 11;
dom (q * g2) = dom g2
by VALUED_1:def 5;
then
( len (q * g2) = (q -' 1) div 2 & len (g1 mod q) = (q -' 1) div 2 )
by A109, A121, EULER_2:def 1, FINSEQ_3:31;
then
( q * g2 in ((q -' 1) div 2) -tuples_on NAT & g1 mod q in ((q -' 1) div 2) -tuples_on NAT )
by A130;
then
( q * g2 is Element of ((q -' 1) div 2) -tuples_on REAL & g1 mod q is Element of ((q -' 1) div 2) -tuples_on REAL )
by FINSEQ_2:129;
then A131: Sum g1 =
(Sum (q * g2)) + (Sum (g1 mod q))
by A129, RVSUM_1:119
.=
(q * (Sum g2)) + (Sum (g1 mod q))
by RVSUM_1:117
;
len (g1 mod q) >= 1
by A9, A109, 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
A132:
rng (g1 mod q) c= (Seg n2) \/ {0 }
by HEYTING3:3;
not 0 in rng (g1 mod q)
proof
assume
0 in rng (g1 mod q)
;
:: thesis: contradiction
then consider a being
Nat such that A133:
(
a in dom (g1 mod q) &
(g1 mod q) . a = 0 )
by FINSEQ_2:11;
a in dom g1
by A122, A133, FINSEQ_3:31;
then A134:
g1 . a = ((g2 . a) * q) + 0
by A126, A133;
a in dom g1
by A122, A133, FINSEQ_3:31;
then
p * a = (g2 . a) * q
by A110, A134;
then A135:
q divides p * a
by NAT_D:def 3;
A136:
(
a >= 1 &
a <= (q -' 1) div 2 )
by A109, A122, A133, FINSEQ_3:27;
then
q <= a
by A2, A135, NAT_D:7, PEPIN:3;
hence
contradiction
by A14, A136, XXREAL_0:2;
:: thesis: verum
end;
then A137:
{0 } misses rng (g1 mod q)
by ZFMISC_1:56;
then A138:
rng (g1 mod q) c= Seg n2
by A132, XBOOLE_1:73;
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
then A140:
g1 mod q is one-to-one
by FUNCT_1:def 8;
set g4 = Sgm (rng (g1 mod q));
set XX = { k where k is Element of NAT : ( k in rng (Sgm (rng (g1 mod q))) & k > q / 2 ) } ;
A141:
rng (Sgm (rng (g1 mod q))) = rng (g1 mod q)
by A138, FINSEQ_1:def 13;
A142:
Sgm (rng (g1 mod q)) is one-to-one
by A132, A137, FINSEQ_3:99, XBOOLE_1:73;
( Sgm (rng (g1 mod q)) is FinSequence of REAL & g1 mod q is FinSequence of REAL )
by FINSEQ_2:27;
then A143:
Sum (Sgm (rng (g1 mod q))) = Sum (g1 mod q)
by A140, A141, A142, RFINSEQ:22, RFINSEQ:39;
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)))
then A145:
{ 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;
then 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 XBOOLE_1:1;
reconsider YY = (rng (Sgm (rng (g1 mod q)))) \ XX as finite Subset of NAT ;
A146:
(rng (Sgm (rng (g1 mod q)))) \ XX c= rng (Sgm (rng (g1 mod q)))
by XBOOLE_1:36;
then A147:
YY c= Seg n2
by A138, A141, XBOOLE_1:1;
set mm = card XX;
A148:
len (g1 mod q) = card (rng (Sgm (rng (g1 mod q))))
by A140, A141, FINSEQ_4:77;
card XX <= card (rng (Sgm (rng (g1 mod q))))
by A145, NAT_1:44;
then
card XX <= (q -' 1) div 2
by A109, A148, EULER_2:def 1;
then reconsider nn = ((q -' 1) div 2) - (card XX) as Element of NAT by NAT_1:21;
len (g1 mod q) = card (rng (g1 mod q))
by A140, FINSEQ_4:77;
then A149:
len (Sgm (rng (g1 mod q))) = (q -' 1) div 2
by A109, A122, A132, A137, FINSEQ_3:44, XBOOLE_1:73;
A150:
XX c= Seg n2
by A138, A141, A145, XBOOLE_1:1;
A151:
Sgm (rng (g1 mod q)) = (Sgm YY) ^ (Sgm XX)
then
Sum (Sgm (rng (g1 mod q))) = (Sum (Sgm YY)) + (Sum (Sgm XX))
by RVSUM_1:105;
then A154:
p * (Sum (idseq ((q -' 1) div 2))) = ((q * (Sum g2)) + (Sum (Sgm YY))) + (Sum (Sgm XX))
by A131, A143, RVSUM_1:117;
A155:
len (Sgm YY) = nn
then A156:
(Sgm (rng (g1 mod q))) /^ nn = Sgm XX
by A151, FINSEQ_5:40;
Sgm (rng (g1 mod q)) = ((Sgm (rng (g1 mod q))) | nn) ^ ((Sgm (rng (g1 mod q))) /^ nn)
by RFINSEQ:21;
then A157:
( (Sgm (rng (g1 mod q))) | nn is one-to-one & (Sgm (rng (g1 mod q))) /^ nn is one-to-one )
by A142, FINSEQ_3:98;
A158:
(Sgm (rng (g1 mod q))) | nn = Sgm YY
by A151, A155, FINSEQ_3:122, FINSEQ_6:12;
for d being Nat st d in dom (idseq ((q -' 1) div 2)) holds
(idseq ((q -' 1) div 2)) . d in NAT
by ORDINAL1:def 13;
then
idseq ((q -' 1) div 2) is FinSequence of NAT
by FINSEQ_2:14;
then reconsider N = Sum (idseq ((q -' 1) div 2)) as Element of NAT by Lm3;
A159:
Lege p,q = (- 1) |^ (Sum g2)
proof
per cases
( XX is empty or not XX is empty )
;
suppose A160:
XX is
empty
;
:: thesis: Lege p,q = (- 1) |^ (Sum g2)
for
d being
Nat st
d in dom (Sgm (rng (g1 mod q))) holds
(
(Sgm (rng (g1 mod q))) . d > 0 &
(Sgm (rng (g1 mod q))) . d <= (q -' 1) div 2 )
then
rng (g1 mod q) = Seg ((q -' 1) div 2)
by A141, A142, A149, Th40;
then
Sgm (rng (g1 mod q)) = idseq ((q -' 1) div 2)
by FINSEQ_3:54;
then
p * N = (q * (Sum g2)) + N
by A131, A143, RVSUM_1:117;
then
(p * N) - N = q * (Sum g2)
;
then
(p -' 1) * N = q * (Sum g2)
by A8;
then
2
divides q * (Sum g2)
by A11, NAT_D:9;
then
2
divides (Sum g2) - 0
by A4, PEPIN:3;
then
Sum g2,
0 are_congruent_mod 2
by INT_2:19;
then
(Sum g2) mod 2
= 0 mod 2
by INT_3:12;
then
(- 1) |^ (card XX) = (- 1) |^ (Sum g2)
by A160, Th45, CARD_1:47;
hence
Lege p,
q = (- 1) |^ (Sum g2)
by A1, A3, A141, Th41;
:: thesis: verum suppose
not
XX is
empty
;
:: thesis: Lege p,q = (- 1) |^ (Sum g2)A164:
nn <= len (Sgm (rng (g1 mod q)))
by A149, XREAL_1:45;
A165:
len ((Sgm (rng (g1 mod q))) | nn) = nn
by A149, FINSEQ_1:80, XREAL_1:45;
A166:
len ((Sgm (rng (g1 mod q))) /^ nn) =
(len (Sgm (rng (g1 mod q)))) -' nn
by RFINSEQ:42
.=
(len (Sgm (rng (g1 mod q)))) - nn
by A149, XREAL_1:45, XREAL_1:235
.=
card XX
by A149
;
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));
A167:
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 A166, FINSEQ_1:def 18
.=
(dom ((Sgm (rng (g1 mod q))) /^ nn)) /\ (dom ((Sgm (rng (g1 mod q))) /^ nn))
by FINSEQ_1:def 3
.=
dom ((Sgm (rng (g1 mod q))) /^ nn)
;
then A168:
len (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) = len ((Sgm (rng (g1 mod q))) /^ nn)
by FINSEQ_3:31;
A169:
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)
A171:
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 ) )
assume A172:
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 A173:
(((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d = q - (((Sgm (rng (g1 mod q))) /^ nn) . d)
by A169;
reconsider w =
(((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d as
Element of
INT by INT_1:def 2;
(Sgm XX) . d in rng (Sgm XX)
by A156, A167, A172, FUNCT_1:12;
then
(Sgm XX) . d in XX
by A150, FINSEQ_1:def 13;
then consider ll being
Element of
NAT such that A174:
(
ll = (Sgm XX) . d &
ll in rng (g1 mod q) &
ll > q / 2 )
by A141;
A175:
w < q - (q / 2)
by A156, A173, A174, XREAL_1:12;
consider e being
Nat such that A176:
(
e in dom (g1 mod q) &
(g1 mod q) . e = ((Sgm (rng (g1 mod q))) /^ nn) . d )
by A156, A174, FINSEQ_2:11;
((Sgm (rng (g1 mod q))) /^ nn) . d = (g1 . e) mod q
by A123, A176, EULER_2:def 1;
then
((Sgm (rng (g1 mod q))) /^ nn) . d < q
by NAT_D:1;
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 A16, A173, A175, INT_1:81, XREAL_1:52;
:: thesis: verum
end;
for
d being
Nat st
d in dom (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) holds
(((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) . d in NAT
then reconsider g5 =
((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn) as
FinSequence of
NAT by FINSEQ_2:14;
for
d,
e being
Element of
NAT st 1
<= d &
d < e &
e <= len g5 holds
g5 . d <> g5 . e
then
len g5 = card (rng g5)
by GRAPH_5:10;
then A179:
g5 is
one-to-one
by FINSEQ_4:77;
(
(Sgm (rng (g1 mod q))) | nn is
FinSequence of
NAT &
g5 is
FinSequence of
NAT )
;
then reconsider g6 =
((Sgm (rng (g1 mod q))) | nn) ^ (((card XX) |-> q) - ((Sgm (rng (g1 mod q))) /^ nn)) as
FinSequence of
NAT by FINSEQ_1:96;
A180:
len g6 =
(len ((Sgm (rng (g1 mod q))) | nn)) + (len g5)
by FINSEQ_1:35
.=
(q -' 1) div 2
by A165, A166, A168
;
A181:
rng (idseq ((q -' 1) div 2)) = Seg ((q -' 1) div 2)
by RELAT_1:71;
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 A182:
(
x in rng ((Sgm (rng (g1 mod q))) | nn) &
x in rng g5 )
by XBOOLE_0:3;
rng ((Sgm (rng (g1 mod q))) | nn) c= rng (Sgm (rng (g1 mod q)))
by FINSEQ_5:21;
then consider d1 being
Nat such that A183:
(
d1 in dom (g1 mod q) &
(g1 mod q) . d1 = x )
by A141, A182, FINSEQ_2:11;
A184:
d1 in dom g1
by A122, A183, FINSEQ_3:31;
then A185:
x = (g1 . d1) mod q
by A183, EULER_2:def 1;
consider e being
Nat such that A186:
(
e in dom g5 &
g5 . e = x )
by A182, FINSEQ_2:11;
x = q - (((Sgm (rng (g1 mod q))) /^ nn) . e)
by A169, A186;
then A187:
x = q - ((Sgm (rng (g1 mod q))) . (e + nn))
by A164, A167, A186, RFINSEQ:def 2;
e + nn in dom (Sgm (rng (g1 mod q)))
by A167, A186, FINSEQ_5:29;
then
(Sgm (rng (g1 mod q))) . (e + nn) in rng (g1 mod q)
by A141, FUNCT_1:12;
then consider e1 being
Nat such that A188:
(
e1 in dom (g1 mod q) &
(g1 mod q) . e1 = (Sgm (rng (g1 mod q))) . (e + nn) )
by FINSEQ_2:11;
A189:
e1 in dom g1
by A122, A188, FINSEQ_3:31;
then
(Sgm (rng (g1 mod q))) . (e + nn) = (g1 . e1) mod q
by A188, EULER_2:def 1;
then
(((g1 . d1) mod q) + ((g1 . e1) mod q)) mod q = 0
by A185, A187, NAT_D:25;
then
((g1 . d1) + (g1 . e1)) mod q = 0
by EULER_2:8;
then
q divides (g1 . d1) + (g1 . e1)
by PEPIN:6;
then
q divides (d1 * p) + (g1 . e1)
by A110, A184;
then
q divides (d1 * p) + (e1 * p)
by A110, A189;
then A190:
q divides (d1 + e1) * p
;
(
d1 >= 1 &
d1 <= (q -' 1) div 2 &
e1 >= 1 &
e1 <= (q -' 1) div 2 )
by A109, A122, A183, A188, FINSEQ_3:27;
then
(
d1 + e1 >= 1
+ 1 &
d1 + e1 <= ((q -' 1) div 2) + ((q -' 1) div 2) )
by XREAL_1:9;
then
(
d1 + e1 > 0 &
d1 + e1 < q )
by A8, A12, XREAL_1:148, XXREAL_0:2;
hence
contradiction
by A2, A190, NAT_D:7, PEPIN:3;
:: thesis: verum
end; then A191:
g6 is
one-to-one
by A157, A179, FINSEQ_3:98;
for
d being
Nat st
d in dom g6 holds
(
g6 . d > 0 &
g6 . d <= (q -' 1) div 2 )
then A197:
rng g6 = rng (idseq ((q -' 1) div 2))
by A180, A181, A191, Th40;
A198:
(
g6 is
FinSequence of
REAL &
(Sgm (rng (g1 mod q))) /^ nn is
FinSequence of
REAL )
by FINSEQ_2:27;
then N =
Sum g6
by A191, A197, RFINSEQ:22, RFINSEQ:39
.=
(Sum ((Sgm (rng (g1 mod q))) | nn)) + (Sum g5)
by RVSUM_1:105
.=
(Sum ((Sgm (rng (g1 mod q))) | nn)) + (((card XX) * q) - (Sum ((Sgm (rng (g1 mod q))) /^ nn)))
by A166, A198, 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 A154, A156, A158;
then A199:
((p -' 1) * N) mod 2 =
(((q * (Sum g2)) - ((card XX) * q)) + (2 * (Sum (Sgm XX)))) mod 2
by A7, XREAL_1:235
.=
((q * (Sum g2)) - ((card XX) * q)) mod 2
by EULER_1:13
;
2
divides (p -' 1) * N
by A11, NAT_D:9;
then
(q * ((Sum g2) - (card XX))) mod 2
= 0
by A199, PEPIN:6;
then
2
divides q * ((Sum g2) - (card XX))
by Lm1;
then
2
divides (Sum g2) - (card XX)
by A4, INT_2:40;
then
Sum g2,
card XX are_congruent_mod 2
by INT_2:19;
then
(Sum g2) mod 2
= (card XX) mod 2
by INT_3:12;
then
(- 1) |^ (Sum g2) = (- 1) |^ (card XX)
by Th45;
hence
Lege p,
q = (- 1) |^ (Sum g2)
by A1, A3, A141, Th41;
:: thesis: verum end;
end;
(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 A9;
deffunc H3(
Element of
A,
Element of
B)
-> set =
($1 / p) - ($2 / q);
A200:
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 A201:
for
x being
Element of
A for
y being
Element of
B holds
z . x,
y = H3(
x,
y)
from FUNCT_7:sch 1(A200);
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 } );
A202:
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]
consider Pr being
FinSequence of
bool (dom z) such that A204:
(
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(A202);
A205:
len Pr = (p -' 1) div 2
by A204, FINSEQ_1:def 3;
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 A206:
(
d in dom Pr &
e in dom Pr &
d <> e )
;
:: thesis: Pr . d misses Pr . e
then consider x1 being
Element of
A such that A207:
(
x1 = d &
Pr . d = { [x1,y] where y is Element of B : z . x1,y > 0 } )
by A204;
consider x2 being
Element of
A such that A208:
(
x2 = e &
Pr . e = { [x2,y] where y is Element of B : z . x2,y > 0 } )
by A204, A206;
now assume
not
Pr . d misses Pr . e
;
:: thesis: contradictionthen consider l being
set such that A209:
(
l in Pr . d &
l in Pr . e )
by XBOOLE_0:3;
consider y1 being
Element of
B such that A210:
(
l = [x1,y1] &
z . x1,
y1 > 0 )
by A207, A209;
consider y2 being
Element of
B such that A211:
(
l = [x2,y2] &
z . x2,
y2 > 0 )
by A208, A209;
thus
contradiction
by A206, A207, A208, A210, A211, ZFMISC_1:33;
:: thesis: verum end;
hence
Pr . d misses Pr . e
;
:: thesis: verum
end;
then A212:
card (union (rng Pr)) = Sum (Card Pr)
by A205, Th48;
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 } );
A213:
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]
consider Pk being
FinSequence of
bool (dom z) such that A215:
(
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(A213);
A216:
len Pk = (q -' 1) div 2
by A215, FINSEQ_1:def 3;
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 A217:
(
d in dom Pk &
e in dom Pk &
d <> e )
;
:: thesis: Pk . d misses Pk . e
then consider y1 being
Element of
B such that A218:
(
y1 = d &
Pk . d = { [x,y1] where x is Element of A : z . x,y1 < 0 } )
by A215;
consider y2 being
Element of
B such that A219:
(
y2 = e &
Pk . e = { [x,y2] where x is Element of A : z . x,y2 < 0 } )
by A215, A217;
now assume
not
Pk . d misses Pk . e
;
:: thesis: contradictionthen consider l being
set such that A220:
(
l in Pk . d &
l in Pk . e )
by XBOOLE_0:3;
consider x1 being
Element of
A such that A221:
(
l = [x1,y1] &
z . x1,
y1 < 0 )
by A218, A220;
consider x2 being
Element of
A such that A222:
(
l = [x2,y2] &
z . x2,
y2 < 0 )
by A219, A220;
thus
contradiction
by A217, A218, A219, A221, A222, ZFMISC_1:33;
:: thesis: verum end;
hence
Pk . d misses Pk . e
;
:: thesis: verum
end;
then A223:
card (union (rng Pk)) = Sum (Card Pk)
by A216, Th48;
reconsider U1 =
union (rng Pr),
U2 =
union (rng Pk) as
finite Subset of
(dom z) by PROB_3:53;
U1 misses U2
proof
assume
U1 meets U2
;
:: thesis: contradiction
then consider l being
set such that A224:
(
l in U1 &
l in U2 )
by XBOOLE_0:3;
l in Union Pr
by A224;
then consider k1 being
Nat such that A225:
(
k1 in dom Pr &
l in Pr . k1 )
by PROB_3:54;
l in Union Pk
by A224;
then consider k2 being
Nat such that A226:
(
k2 in dom Pk &
l in Pk . k2 )
by PROB_3:54;
reconsider k1 =
k1,
k2 =
k2 as
Element of
NAT by ORDINAL1:def 13;
consider m1 being
Element of
A such that A227:
(
m1 = k1 &
Pr . k1 = { [m1,y] where y is Element of B : z . m1,y > 0 } )
by A204, A225;
consider m2 being
Element of
B such that A228:
(
l = [m1,m2] &
z . m1,
m2 > 0 )
by A225, A227;
consider n1 being
Element of
B such that A229:
(
n1 = k2 &
Pk . k2 = { [x,n1] where x is Element of A : z . x,n1 < 0 } )
by A215, A226;
consider n2 being
Element of
A such that A230:
(
l = [n2,n1] &
z . n2,
n1 < 0 )
by A226, A229;
(
m1 = n2 &
m2 = n1 )
by A228, A230, ZFMISC_1:33;
hence
contradiction
by A228, A230;
:: thesis: verum
end;
then A231:
card (U1 \/ U2) = (Sum (Card Pr)) + (Sum (Card Pk))
by A212, A223, CARD_2:53;
U1 \/ U2 = dom z
then A238:
(Sum (Card Pr)) + (Sum (Card Pk)) =
card [:A,B:]
by A231, FUNCT_2:def 1
.=
(card A) * (card B)
by CARD_2:65
.=
((p -' 1) div 2) * (card B)
by FINSEQ_1:78
.=
((p -' 1) div 2) * ((q -' 1) div 2)
by FINSEQ_1:78
;
A239:
Card Pr = f2
proof
A240:
dom (Card Pr) =
dom Pr
by CARD_3:def 2
.=
dom f2
by A28, A204, 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 A241:
d in dom (Card Pr)
;
:: thesis: (Card Pr) . d = f2 . d
then A242:
d in dom Pr
by CARD_3:def 2;
d in Seg ((p -' 1) div 2)
by A28, A240, A241, FINSEQ_1:def 3;
then consider m being
Element of
A such that A243:
(
m = d &
Pr . d = { [m,y] where y is Element of B : z . m,y > 0 } )
by A204;
Pr . d = [:{m},(Seg (f2 . m)):]
proof
set L =
[:{m},(Seg (f2 . m)):];
A244:
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)):] )
assume
l in Pr . d
;
:: thesis: l in [:{m},(Seg (f2 . m)):]
then consider y1 being
Element of
B such that A245:
(
l = [m,y1] &
z . m,
y1 > 0 )
by A243;
(m / p) - (y1 / q) > 0
by A201, A245;
then
((m / p) - (y1 / q)) + (y1 / q) > 0 + (y1 / q)
by XREAL_1:8;
then
(m / p) * q > (y1 / q) * q
by XREAL_1:70;
then
(m * q) / p > y1
by XCMPLX_1:88;
then A246:
(m * q) div p >= y1
by INT_1:81;
m in Seg ((p -' 1) div 2)
;
then A247:
m in dom f1
by A6, FINSEQ_1:def 3;
then
(f1 . m) div p >= y1
by A17, A246;
then A248:
y1 <= f2 . m
by A28, A31, A247;
y1 >= 1
by FINSEQ_1:3;
then A249:
y1 in Seg (f2 . m)
by A248, FINSEQ_1:3;
m in {m}
by TARSKI:def 1;
hence
l in [:{m},(Seg (f2 . m)):]
by A245, A249, ZFMISC_1:def 2;
:: thesis: verum
end;
[:{m},(Seg (f2 . m)):] c= Pr . d
proof
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 A250:
(
x in {m} &
y in Seg (f2 . m) &
l = [x,y] )
by ZFMISC_1:def 2;
m <= (p -' 1) div 2
by FINSEQ_1:3;
then
m * q <= ((p -' 1) div 2) * q
by XREAL_1:66;
then A251:
(m * q) div p <= (((p -' 1) div 2) * q) div p
by NAT_2:26;
then A253:
- (q div p) = ((- q) div p) + 1
by WSIERP_1:49;
2
divides (p -' 1) * q
by A11, 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 A254:
(((p -' 1) div 2) * q) div p =
((p - 1) * q) div (2 * p)
by A8, A12, NAT_2:29
.=
(((p * q) - q) div p) div 2
by PRE_FF:5
.=
(q + ((- (q div p)) - 1)) div 2
by A253, INT_3:8
.=
((2 * ((q -' 1) div 2)) + (- (q div p))) div 2
by A8, A12
.=
((q -' 1) div 2) + ((- (q div p)) div 2)
by INT_3:8
;
(((p -' 1) div 2) * q) div p <= (q -' 1) div 2
then A255:
(m * q) div p <= (q -' 1) div 2
by A251, XXREAL_0:2;
m in Seg ((p -' 1) div 2)
;
then A256:
m in dom f1
by A6, FINSEQ_1:def 3;
then A257:
f2 . m =
(f1 . m) div p
by A28, A31
.=
(m * q) div p
by A17, A256
;
reconsider y =
y as
Element of
NAT by A250;
( 1
<= y &
y <= f2 . m )
by A250, FINSEQ_1:3;
then
( 1
<= y &
y <= (q -' 1) div 2 )
by A255, A257, XXREAL_0:2;
then reconsider y =
y as
Element of
B by FINSEQ_1:3;
A258:
y <= [\((m * q) / p)/]
by A250, A257, FINSEQ_1:3;
then
[\((m * q) / p)/] < (m * q) / p
by INT_1:48;
then
y < (m * q) / p
by A258, XXREAL_0:2;
then
y * p < ((m * q) / p) * p
by XREAL_1:70;
then
y * p < m * q
by XCMPLX_1:88;
then
y / q < m / p
by XREAL_1:108;
then
(m / p) - (y / q) > 0
by XREAL_1:52;
then
z . m,
y > 0
by A201;
then
[m,y] in Pr . d
by A243;
hence
l in Pr . d
by A250, TARSKI:def 1;
:: thesis: verum
end;
hence
Pr . d = [:{m},(Seg (f2 . m)):]
by A244, XBOOLE_0:def 10;
:: thesis: verum
end;
then card (Pr . d) =
card [:(Seg (f2 . m)),{m}:]
by CARD_2:11
.=
card (Seg (f2 . m))
by CARD_2:13
;
then card (Pr . d) =
card (f2 . d)
by A243, FINSEQ_1:76
.=
f2 . d
by CARD_1:def 5
;
hence
(Card Pr) . d = f2 . d
by A242, CARD_3:def 2;
:: thesis: verum
end;
hence
Card Pr = f2
by A240, FINSEQ_1:17;
:: thesis: verum
end;
Card Pk = g2
proof
A261:
dom (Card Pk) =
Seg (len g2)
by A121, A215, CARD_3:def 2
.=
dom g2
by FINSEQ_1:def 3
;
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 A262:
d in dom (Card Pk)
;
:: thesis: (Card Pk) . d = g2 . d
then A263:
d in dom Pk
by CARD_3:def 2;
d in Seg ((q -' 1) div 2)
by A121, A261, A262, FINSEQ_1:def 3;
then consider n being
Element of
B such that A264:
(
n = d &
Pk . d = { [x,n] where x is Element of A : z . x,n < 0 } )
by A215;
Pk . d = [:(Seg (g2 . n)),{n}:]
proof
set L =
[:(Seg (g2 . n)),{n}:];
A265:
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}:] )
assume
l in Pk . d
;
:: thesis: l in [:(Seg (g2 . n)),{n}:]
then consider x being
Element of
A such that A266:
(
l = [x,n] &
z . x,
n < 0 )
by A264;
(x / p) - (n / q) < 0
by A201, A266;
then
((x / p) - (n / q)) + (n / q) < 0 + (n / q)
by XREAL_1:8;
then
(x / p) * p < (n / q) * p
by XREAL_1:70;
then
x < (n * p) / q
by XCMPLX_1:88;
then A267:
x <= (n * p) div q
by INT_1:81;
n in Seg ((q -' 1) div 2)
;
then A268:
n in dom g1
by A109, FINSEQ_1:def 3;
then
(g1 . n) div q >= x
by A110, A267;
then A269:
x <= g2 . n
by A121, A124, A268;
x >= 1
by FINSEQ_1:3;
then A270:
x in Seg (g2 . n)
by A269, FINSEQ_1:3;
n in {n}
by TARSKI:def 1;
hence
l in [:(Seg (g2 . n)),{n}:]
by A266, A270, ZFMISC_1:def 2;
:: thesis: verum
end;
[:(Seg (g2 . n)),{n}:] c= Pk . d
proof
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 A271:
(
x in Seg (g2 . n) &
y in {n} &
l = [x,y] )
by ZFMISC_1:def 2;
n <= (q -' 1) div 2
by FINSEQ_1:3;
then
n * p <= ((q -' 1) div 2) * p
by XREAL_1:66;
then A272:
(n * p) div q <= (((q -' 1) div 2) * p) div q
by NAT_2:26;
then A274:
- (p div q) = ((- p) div q) + 1
by WSIERP_1:49;
2
divides (q -' 1) * p
by A11, 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 A275:
(((q -' 1) div 2) * p) div q =
((q - 1) * p) div (2 * q)
by A8, A12, NAT_2:29
.=
(((q * p) - p) div q) div 2
by PRE_FF:5
.=
(p + ((- (p div q)) - 1)) div 2
by A274, INT_3:8
.=
((2 * ((p -' 1) div 2)) - (p div q)) div 2
by A8, A12
.=
((p -' 1) div 2) + ((- (p div q)) div 2)
by INT_3:8
;
(((q -' 1) div 2) * p) div q <= (p -' 1) div 2
then A276:
(n * p) div q <= (p -' 1) div 2
by A272, XXREAL_0:2;
n in Seg ((q -' 1) div 2)
;
then A277:
n in dom g1
by A109, FINSEQ_1:def 3;
then A278:
g2 . n =
(g1 . n) div q
by A121, A124
.=
(n * p) div q
by A110, A277
;
reconsider x =
x as
Element of
NAT by A271;
A279:
( 1
<= x &
x <= g2 . n )
by A271, FINSEQ_1:3;
then
( 1
<= x &
x <= (p -' 1) div 2 )
by A276, A278, XXREAL_0:2;
then reconsider x =
x as
Element of
A by FINSEQ_1:3;
then
[\((n * p) / q)/] < (n * p) / q
by INT_1:48;
then
x < (n * p) / q
by A278, A279, XXREAL_0:2;
then
x * q < ((n * p) / q) * q
by XREAL_1:70;
then
x * q < n * p
by XCMPLX_1:88;
then
(x / p) - (n / q) < 0
by XREAL_1:51, XREAL_1:108;
then
z . x,
n < 0
by A201;
then
[x,n] in Pk . d
by A264;
hence
l in Pk . d
by A271, TARSKI:def 1;
:: thesis: verum
end;
hence
Pk . d = [:(Seg (g2 . n)),{n}:]
by A265, XBOOLE_0:def 10;
:: thesis: verum
end;
then
card (Pk . d) = card (Seg (g2 . n))
by CARD_2:13;
then card (Pk . d) =
card (g2 . d)
by A264, FINSEQ_1:76
.=
g2 . d
by CARD_1:def 5
;
hence
(Card Pk) . d = g2 . d
by A263, CARD_3:def 2;
:: thesis: verum
end;
hence
Card Pk = g2
by A261, FINSEQ_1:17;
:: thesis: verum
end;
hence
(Sum f2) + (Sum g2) = ((p -' 1) div 2) * ((q -' 1) div 2)
by A238, A239;
:: thesis: verum
end;
hence
(Lege p,q) * (Lege q,p) = (- 1) |^ (((p -' 1) div 2) * ((q -' 1) div 2))
by A67, A159, NEWTON:13; :: thesis: verum