2 & a gcd p = 1 & b gcd p = 1 & a is_quadratic_residue_mod p
& b is_quadratic_residue_mod p implies a*b is_quadratic_residue_mod p
proof assume A1:p>2 & a gcd p = 1 & b gcd p = 1
& a is_quadratic_residue_mod p & b is_quadratic_residue_mod p;
consider i being Integer such that A2:(i^2 - a) mod p =0 by A1,Def2;
consider j being Integer such that A3:(j^2 - b) mod p =0 by A1,Def2;
p divides (i^2 - a) & p divides (j^2 - b) by A2,A3,INT_1:89;
then i^2,a are_congruent_mod p & j^2,b are_congruent_mod p by INT_2:19;
then (i^2)*(j^2),a*b are_congruent_mod p by INT_1:39;
then p divides ((i*j)^2 - a*b) by INT_2:19;
then ((i*j)^2 - a*b) mod p = 0 by INT_1:89;
hence thesis by Def2;
end;
theorem p>2 & a gcd p = 1 & b gcd p = 1 & a is_quadratic_residue_mod p
& not b is_quadratic_residue_mod p
implies not a*b is_quadratic_residue_mod p
proof assume A1:p>2 & a gcd p = 1 & b gcd p = 1
& a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p;
then A2:a*b gcd p = 1 by WSIERP_1:11;
set l = (p-'1) div 2;
(a|^l -1) mod p = 0 & (b|^l + 1) mod p = 0 by A1,Th20,Th21;
then A3:p divides (a|^l -1) & p divides (b|^l + 1) by INT_1:89;
then A4:p divides (a|^l -1)*(b|^l +1) by INT_2:12;
A5:(a|^l -1)*(b|^l +1) = a|^l * b|^l +a|^l*1 -1*b|^l -1*1
.= (a*b)|^l +a|^l*1 -1*b|^l -1*1 by NEWTON:12
.= ((a*b)|^l -1) +(a|^l - 1) -(b|^l - 1);
now assume a*b is_quadratic_residue_mod p;
then ((a*b)|^l -1) mod p = 0 by A1,A2,Th20;
then p divides ((a*b)|^l -1) by INT_1:89;
then p divides ((a*b)|^l -1) +(a|^l - 1) by A3,WSIERP_1:9;
then p divides (b|^l - 1) by A4,A5,Th2;
then p divides ((b|^l +1) - (b|^l -1)) by A3,Th1;
hence contradiction by A1,NAT_D:7;
end;
hence thesis;
end;
theorem p>2 & a gcd p = 1 & b gcd p = 1
& not a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p
implies a*b is_quadratic_residue_mod p
proof assume A1:p>2 & a gcd p = 1 & b gcd p = 1
& not a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p;
then A2:a*b gcd p = 1 by WSIERP_1:11;
set l = (p-'1) div 2;
(a|^l +1) mod p = 0 & (b|^l + 1) mod p = 0 by A1,Th21;
then A3:p divides (a|^l +1) & p divides (b|^l + 1) by INT_1:89;
then A4:p divides (a|^l +1)*(b|^l +1) by INT_2:12;
A5:(a|^l +1)*(b|^l +1) = a|^l * b|^l +a|^l*1 +1*b|^l +1*1
.= (a*b)|^l +a|^l + b|^l +1 by NEWTON:12
.= ((a*b)|^l +1) +(a|^l + 1) - (1- b|^l);
now assume not a*b is_quadratic_residue_mod p;
then ((a*b)|^l +1) mod p = 0 by A1,A2,Th21;
then p divides ((a*b)|^l +1) by INT_1:89;
then p divides ((a*b)|^l +1) +(a|^l + 1) by A3,WSIERP_1:9;
then p divides (1- b|^l) by A4,A5,Th2;
then p divides ((b|^l +1) + (1- b|^l)) by A3,WSIERP_1:9;
hence contradiction by A1,NAT_D:7;
end;
hence thesis;
end;
definition let a be Integer, p be Prime;
func Lege (a,p) -> Integer equals :Def3:
1 if a is_quadratic_residue_mod p otherwise
-1;:: if not a is_quadratic_residue_mod p;
coherence;
consistency;
end;
theorem Th25:
Lege (a,p) = 1 or Lege (a,p) = -1
proof per cases;
suppose a is_quadratic_residue_mod p;
hence thesis by Def3;
end;
suppose not a is_quadratic_residue_mod p;
hence thesis by Def3;
end;
end;
theorem Th26:
a gcd p = 1 implies Lege (a^2,p) = 1
proof assume a gcd p = 1;
then a^2 is_quadratic_residue_mod p by Th9;
hence thesis by Def3;
end;
theorem Lege (1,p) = 1
proof 1 gcd p = 1 by WSIERP_1:13;
then Lege (1^2,p) = 1 by Th26;
hence thesis;
end;
theorem Th28: p>2 & a gcd p =1
implies Lege (a,p),a|^((p-'1) div 2) are_congruent_mod p
proof assume A1:p>2 & a gcd p = 1;
A2:p>1 by INT_2:def 5;
then -p < -1 by XREAL_1:26;
then A3:(-1) mod p = p+(-1) by INT_3:10;
per cases;
suppose A4:a is_quadratic_residue_mod p;
then a|^((p-'1) div 2) mod p = 1 by A1,Th17;
then a|^((p-'1) div 2) mod p = 1 mod p by A2,NAT_D:14;
then a|^((p-'1) div 2) mod p = Lege (a,p) mod p by A4,Def3;
hence thesis by INT_3:12;
end;
suppose A5:not a is_quadratic_residue_mod p;
then a|^((p-'1) div 2) mod p = p-1 by A1,Th19
.= Lege (a,p) mod p by A3,A5,Def3;
hence thesis by INT_3:12;
end;
end;
theorem
p>2 & a gcd p =1 & a,b are_congruent_mod p
implies Lege (a,p) = Lege (b,p)
proof assume A1:p>2 & a gcd p =1 & a,b are_congruent_mod p;
then b gcd p = 1 by INT_4:14;
then Lege (a,p),a|^((p-'1) div 2) are_congruent_mod p &
Lege (b,p),b|^((p-'1) div 2) are_congruent_mod p by A1,Th28;
then A2:Lege (a,p) mod p = a|^((p-'1) div 2) mod p
& Lege (b,p) mod p = b|^((p-'1) div 2) mod p by INT_3:12;
a mod p = b mod p by A1,INT_3:12;
then Lege (a,p) mod p = Lege (b,p) mod p by A2,Th13;
then Lege (a,p),Lege (b,p) are_congruent_mod p by INT_3:12;
then A3:p divides (Lege (a,p) - Lege (b,p)) by INT_2:19;
per cases by Th25;
suppose A4:Lege (a,p) = 1;
Lege (b,p) <> -1 by A1,A3,A4,NAT_D:7;
hence thesis by A4,Th25;
end;
suppose A5:Lege (a,p) = -1;
now assume Lege (b,p) = 1;
then p divides -2 by A3,A5;
then p divides 2 by INT_2:14;
hence contradiction by A1,NAT_D:7;
end;
hence thesis by A5,Th25;
end;
end;
theorem p>2 & a gcd p=1 & b gcd p=1 implies Lege(a*b,p)=Lege(a,p)*Lege(b,p)
proof assume A1:p>2 & a gcd p=1 & b gcd p=1;
then Lege(a,p),a|^((p-'1) div 2) are_congruent_mod p &
Lege(b,p),b|^((p-'1) div 2) are_congruent_mod p by Th28;
then Lege(a,p)*Lege(b,p),(a|^((p-'1) div 2))*(b|^((p-'1) div 2))
are_congruent_mod p by INT_1:39;
then Lege(a,p)*Lege(b,p),(a*b)|^((p-'1) div 2) are_congruent_mod p
by NEWTON:12;
then A2:(a*b)|^((p-'1) div 2),Lege(a,p)*Lege(b,p) are_congruent_mod p
by INT_1:35;
a*b gcd p = 1 by A1,WSIERP_1:11;
then Lege(a*b,p),(a*b)|^((p-'1) div 2) are_congruent_mod p by A1,Th28;
then Lege(a*b,p),Lege(a,p)*Lege(b,p) are_congruent_mod p by A2,INT_1:36;
then A3:p divides (Lege(a*b,p)-Lege(a,p)*Lege(b,p)) by INT_2:19;
A4: (Lege(a,p) = 1 or Lege(a,p) = -1) & (Lege(b,p) = 1 or Lege(b,p) = -1)
by Th25;
per cases by Th25;
suppose Lege(a*b,p) = 1;
hence thesis by A1,A3,A4,NAT_D:7;
end;
suppose A5:Lege(a*b,p) = -1;
now assume Lege(a,p)*Lege(b,p) <> -1;
then p divides (-2) by A3,A4,A5;
then p divides 2 by INT_2:14;
hence contradiction by A1,NAT_D:7;
end;
hence thesis by A5;
end;
end;
theorem Th31:
(for d st d in dom fr holds fr.d = 1 or fr.d = -1)
implies Product fr = 1 or Product fr = -1
proof defpred P[FinSequence of INT] means
(for d st d in dom $1 holds $1.d = 1 or $1.d = -1)
implies Product $1 = 1 or Product $1 = -1;
A1: P[<*>INT] by RVSUM_1:124;
A2: for p being FinSequence of INT, n being Element of INT st P[p]
holds P[p^<*n*>] proof
let p be FinSequence of INT,i be Element of INT;
assume A3:P[p];
set p1 = p^<*i*>;
P[p1]
proof assume A4:(for d st d in dom p1 holds p1.d = 1 or p1.d = -1);
A5: for d st d in dom p holds p.d = 1 or p.d = -1
proof let d;assume A6:d in dom p;
then d in dom p1 by FINSEQ_2:18;
then p1.d = 1 or p1.d = -1 by A4;
hence thesis by A6,FINSEQ_1:def 7;
end;
A7: len p1 =len p +1 by FINSEQ_2:19;
len p1 in dom p1 by FINSEQ_5:6;
then A8:p1.(len p + 1) = 1 or p1.(len p + 1) = -1 by A4,A7;
A9: Product p1 = (Product p)*i by RVSUM_1:126;
per cases by A3,A5,A8,FINSEQ_1:59;
suppose Product p = 1 & i =1;
hence thesis by A9;
end;
suppose Product p = 1 & i = -1;
hence thesis by A9;
end;
suppose Product p = -1 & i =1;
hence thesis by A9;
end;
suppose Product p = -1 & i = -1;
hence thesis by A9;
end;
end;
hence thesis;
end;
for p being FinSequence of INT holds P[p] from FINSEQ_2:sch 2(A1,A2);
hence thesis;
end;
reserve m for Integer;
theorem Th32: for f,fr st
len f = len fr & (for d st d in dom f holds f.d,fr.d are_congruent_mod m)
holds Product f,Product fr are_congruent_mod m
proof defpred P[Nat] means for f,fr st len f =$1 & len f=len fr
& (for d st d in dom f holds f.d,fr.d are_congruent_mod m)
holds Product f,Product fr are_congruent_mod m;
A1:P[0] proof let f,fr; assume len f = 0 & len f = len fr;
then f = <*>INT & fr = <*>INT by FINSEQ_1:25;
hence thesis by INT_1:32;
end;
A2:for n be Element of NAT st P[n] holds P[n+1]
proof let n be Element of NAT;
assume A3:P[n];
P[n+1] proof let f,fr;
assume A4:len f = n+1 & len f = len fr &
(for d st d in dom f holds f.d,fr.d are_congruent_mod m);
consider f1 being FinSequence of INT,a being Element of INT
such that A5:f = f1^<*a*> by A4,FINSEQ_2:22;
consider fr1 being FinSequence of INT,b being Element of INT
such that A6:fr = fr1^<*b*> by A4,FINSEQ_2:22;
A7:n+1 = len f1 +1 & n+1 = len fr1 +1 by A4,A5,A6,FINSEQ_2:19;
then A8:dom f1 = dom fr1 by FINSEQ_3:31;
for d st d in dom f1 holds f1.d,fr1.d are_congruent_mod m
proof let d;assume A9:d in dom f1;
then A10:f.d = f1.d & fr.d = fr1.d by A5,A6,A8,FINSEQ_1:def 7;
d in dom f & d in dom fr by A5,A6,A8,A9,FINSEQ_2:18;
hence thesis by A4,A10;
end;
then A11:Product f1,Product fr1 are_congruent_mod m by A3,A7;
f <> {} by A4,FINSEQ_1:25;
then A12:(n+1) in dom f by A4,FINSEQ_5:6;
f.(n+1) = a & fr.(n+1) = b by A5,A6,A7,FINSEQ_1:59;
then a,b are_congruent_mod m by A4,A12;
then (Product f1)*a,(Product fr1)*b are_congruent_mod m
by A11,INT_1:39;
then Product f,(Product fr1)*b are_congruent_mod m by A5,RVSUM_1:126;
hence thesis by A6,RVSUM_1:126;
end;
hence thesis;
end;
for n be Element of NAT holds P[n] from NAT_1:sch 1(A1,A2);
hence thesis;
end;
theorem Th33:
for f,fr st len f = len fr
& (for d st d in dom f holds f.d,-fr.d are_congruent_mod m)
holds Product f,((-1)|^(len f))*Product fr are_congruent_mod m
proof defpred P[Nat] means for f,fr st len f =$1 & len f=len fr
& (for d st d in dom f holds f.d,-fr.d are_congruent_mod m)
holds Product f,((-1)|^(len f))* Product fr are_congruent_mod m;
A1:P[0] proof let f,fr; assume A2:len f = 0 & len f = len fr;
then A3:f = <*>INT & fr = <*>INT by FINSEQ_1:25;
(-1)|^(len f) = 1 by A2,NEWTON:9;
hence thesis by A3,INT_1:32;
end;
A4:for n be Element of NAT st P[n] holds P[n+1]
proof let n be Element of NAT;
assume A5:P[n];
P[n+1] proof let f,fr;
assume A6:len f = n+1 & len f = len fr &
(for d st d in dom f holds f.d,-fr.d are_congruent_mod m);
consider f1 be FinSequence of INT,a be Element of INT such that
A7:f = f1^<*a*> by A6,FINSEQ_2:22;
consider fr1 be FinSequence of INT,b be Element of INT such that
A8: fr = fr1^<*b*> by A6,FINSEQ_2:22;
A9:n+1 = len f1 +1 & n+1 = len fr1 +1 by A6,A7,A8,FINSEQ_2:19;
then A10:dom f1 = dom fr1 by FINSEQ_3:31;
for d st d in dom f1 holds f1.d,-fr1.d are_congruent_mod m
proof let d;assume A11:d in dom f1;
then A12:f.d = f1.d & fr.d = fr1.d by A7,A8,A10,FINSEQ_1:def 7;
d in dom f & d in dom fr by A7,A8,A10,A11,FINSEQ_2:18;
hence thesis by A6,A12;
end;
then A13:Product f1,((-1)|^(len f1))*Product fr1 are_congruent_mod m
by A5,A9;
f <> {} by A6,FINSEQ_1:25;
then A14:(n+1) in dom f by A6,FINSEQ_5:6;
f.(n+1) = a & fr.(n+1) = b by A7,A8,A9,FINSEQ_1:59;
then a,-b are_congruent_mod m by A6,A14;then
(Product f1)*a,((-1)|^(len f1))*(Product fr1)*(-b) are_congruent_mod m
by A13,INT_1:39;
then Product f,((-1)|^(len f1))*(-1)*((Product fr1)*b) are_congruent_mod m
by A7,RVSUM_1:126;
then Product f,((-1)|^(len f1 + 1))*((Product fr1)*b) are_congruent_mod m
by NEWTON:11;
hence thesis by A6,A8,A9,RVSUM_1:126;
end;
hence thesis;
end;
for n be Element of NAT holds P[n] from NAT_1:sch 1(A1,A4);
hence thesis;
end;
reserve fp for FinSequence of NAT;
theorem Th34: p>2 & (for d st d in dom fp holds fp.d hcf p = 1) implies
ex fr being FinSequence of INT st len fr = len fp & (for d st d in dom fr
holds fr.d = Lege (fp.d,p)) & Lege (Product fp,p) = Product fr
proof assume A1:p>2;
assume
A2: for d st d in dom fp holds fp.d hcf p = 1;
then
A3: for d being Element of NAT st d in dom fp holds fp.d hcf p = 1;
p in NAT by ORDINAL1:def 13;
then Product(fp) hcf p = 1 by A3,WSIERP_1:43;
then Product(fp) gcd p = 1 by Lm1;then
A4:Lege (Product fp,p),(Product fp)|^((p-'1) div 2) are_congruent_mod p
by A1,Th28;
set k = (p-'1) div 2;
set f = fp|^k;
reconsider f as FinSequence of INT by FINSEQ_2:27,NUMBERS:17;
deffunc F(Nat) = Lege (fp.$1,p);
consider fr being FinSequence such that
A5:len fr = len fp &
(for d being Element of NAT st d in dom fr holds fr.d = F(d))
from FINSEQ_5:sch 1;
for d being Nat st d in dom fr holds fr.d in INT
proof let d be Nat; assume d in dom fr;
then fr.d = Lege (fp.d,p) by A5;
hence thesis by INT_1:def 2;
end;
then reconsider fr as FinSequence of INT by FINSEQ_2:14;
A6:len f = len fp by NAT_3:def 1;
for d st d in dom fr holds fr.d,f.d are_congruent_mod p
proof let d;assume A7:d in dom fr;
then d in dom fp by A5,FINSEQ_3:31;
then fp.d hcf p = 1 by A2;
then fp.d gcd p = 1 by Lm1;
then Lege (fp.d,p),(fp.d)|^k are_congruent_mod p by A1,Th28;
then A8:fr.d,(fp.d)|^k are_congruent_mod p by A5,A7;
d in dom f by A5,A6,A7,FINSEQ_3:31;
hence thesis by A8,NAT_3:def 1;
end;
then Product fr,Product f are_congruent_mod p by A5,A6,Th32;
then A9:Product f,Product fr are_congruent_mod p by INT_1:35;
fp is FinSequence of REAL by FINSEQ_2:27;
then Lege (Product fp,p),Product f are_congruent_mod p by A4,NAT_3:15;
then Lege (Product fp,p),Product fr are_congruent_mod p
by A9,INT_1:36;
then A10:p divides (Lege (Product fp,p) - Product fr) by INT_2:19;
take fr;
A11: for d st d in dom fr holds fr.d = 1 or fr.d = -1
proof let d;assume d in dom fr;
then fr.d = Lege (fp.d,p) by A5;
hence thesis by Th25;
end;
per cases by Th25;
suppose A12:Lege (Product fp,p) = 1;
Product fr <> -1 by A1,A10,A12,NAT_D:7;
hence thesis by A5,A11,A12,Th31;
end;
suppose A13:Lege (Product fp,p) = -1;
now assume Product fr = 1;
then p divides -2 by A10,A13;
then p divides 2 by INT_2:14;
hence contradiction by A1,NAT_D:7;
end;
hence thesis by A5,A11,A13,Th31;
end;
end;
theorem p > 2 & d hcf p = 1 & e hcf p = 1
implies Lege((d^2)*e,p) = Lege(e,p)
proof assume A1:p > 2 & d hcf p = 1 & e hcf p = 1;
then d gcd p = 1 by Lm1;
then A2:Lege(d^2,p) = 1 by Th26;
reconsider d2=d^2, e as Element of NAT by ORDINAL1:def 13;
set fp = <*d2,e*>;
reconsider p as prime Element of NAT by ORDINAL1:def 13;
reconsider fp as FinSequence of NAT by FINSEQ_2:15;
for k st k in dom fp holds fp.k hcf p = 1
proof let k; assume k in dom fp;
then k in Seg(len fp) by FINSEQ_1:def 3;
then A3:k in Seg 2 by FINSEQ_1:61;
A4: d in NAT by ORDINAL1:def 13;
per cases by A3,FINSEQ_1:4,TARSKI:def 2;
suppose k = 1;
then fp.k = d^2 by FINSEQ_1:61;
hence thesis by A1,A4,WSIERP_1:12;
end;
suppose k = 2;
hence thesis by A1,FINSEQ_1:61;
end;
end;
then consider fr be FinSequence of INT such that
A5: len fr = len fp & (for k be Nat st k in dom fr
holds fr.k = Lege (fp.k,p)) & Lege (Product fp,p) = Product fr by A1,Th34;
A6: len fr = 2 by A5,FINSEQ_1:61;
then 1 in dom fr & 2 in dom fr by FINSEQ_3:27;
then fr.1 = Lege(fp.1,p) & fr.2 = Lege(fp.2,p) by A5;
then fr.1 = Lege(d^2,p) & fr.2 = Lege(e,p) by FINSEQ_1:61;
then fr = <*1,Lege(e,p)*> by A2,A6,FINSEQ_1:61;
then Product fr = 1 * Lege(e,p) by RVSUM_1:129;
hence thesis by A5,RVSUM_1:129;
end;
theorem Th36: p>2 implies Lege (-1,p) = (-1)|^((p-'1) div 2)
proof assume A1:p>2;
(-1) gcd p = abs((-1)|^1) hcf abs(p) by NEWTON:10
.= 1 hcf abs(p) by SERIES_2:1
.= 1 by NEWTON:64;
then A2:Lege (-1,p),(-1)|^((p-'1) div 2) are_congruent_mod p by A1,Th28;
abs((-1)|^((p-'1) div 2)) = 1 by SERIES_2:1;
then A3:(-1)|^((p-'1) div 2) =1 or -(-1)|^((p-'1) div 2) =1 by ABSVALUE:1;
per cases by A3;
suppose A4:(-1)|^((p-'1) div 2) =1;
then A5:p divides (Lege (-1,p) - 1) by A2,INT_2:19;
now assume Lege(-1,p) = -1;
then p divides -2 by A5;
then p divides 2 by INT_2:14;
hence contradiction by A1,NAT_D:7;
end;
hence thesis by A4,Th25;
end;
suppose A6:(-1)|^((p-'1) div 2) = -1;
then A7:p divides (Lege (-1,p) - (-1)) by A2,INT_2:19;
Lege(-1,p) <> 1 by A1,A7,NAT_D:7;
hence thesis by A6,Th25;
end;
end;
theorem p>2 & p mod 4 = 1 implies (-1) is_quadratic_residue_mod p
proof assume A1:p>2 & p mod 4 = 1;
then A2:p = (p div 4)*4 + 1 by NAT_D:2;
p>1 by INT_2:def 5;
then p-'1 = p-1 by BINARITH:50;
then p-'1 = 2*(2*(p div 4)) by A2;
then (-1)|^((p-'1) div 2) = (-1)|^(2*(p div 4)) by NAT_D:18
.= ((-1)|^2)|^(p div 4) by NEWTON:14
.= (1|^2)|^(p div 4) by WSIERP_1:2
.= 1|^(p div 4) by NEWTON:100,SQUARE_1:59
.= 1 by NEWTON:15;
then Lege(-1,p) = 1 by A1,Th36;
hence thesis by Def3;
end;
theorem p>2 & p mod 4 = 3 implies not (-1) is_quadratic_residue_mod p
proof assume A1:p>2 & p mod 4 = 3;
then A2:p = (p div 4)*4 + 3 by NAT_D:2;
p>1 by INT_2:def 5;
then p-'1 = p-1 by BINARITH:50;
then p-'1 = 2*(2*(p div 4) + 1) by A2;
then (-1)|^((p-'1) div 2) = (-1)|^(2*(p div 4) + 1) by NAT_D:18
.= (-1)|^(2*(p div 4)) * (-1) by NEWTON:11
.= ((-1)|^2)|^(p div 4) *(-1) by NEWTON:14
.= (1|^2)|^(p div 4) *(-1) by WSIERP_1:2
.= 1|^(p div 4) *(-1) by NEWTON:100,SQUARE_1:59
.= 1 *(-1) by NEWTON:15;
then Lege(-1,p) = -1 by A1,Th36;
hence thesis by Def3;
end;
:: begin :: Gauss Lemma and Law of Quadratic Reciprocity
theorem Th39:for D being non empty set,f being FinSequence of D,
i,j being Nat holds f is one-to-one iff Swap(f,i,j) is one-to-one
proof let D be non empty set,f be FinSequence of D,i,j be Nat;
thus f is one-to-one implies Swap(f,i,j) is one-to-one
proof assume f is one-to-one;
then A1:card(rng f) = len f by FINSEQ_4:77;
set ff = Swap(f,i,j);
len ff = len f & rng ff = rng f by FINSEQ_7:20,24;
hence thesis by A1,FINSEQ_4:77;
end;
assume Swap(f,i,j) is one-to-one;
then card(rng Swap(f,i,j)) = len Swap(f,i,j) by FINSEQ_4:77;
then card(rng f) = len Swap(f,i,j) by FINSEQ_7:24;
then card(rng f) = len f by FINSEQ_7:20;
hence thesis by FINSEQ_4:77;
end;
theorem Th40:
for f being FinSequence of NAT st len f = n & (for d st d in dom f
holds f.d>0 & f.d<=n) & f is one-to-one holds rng f = Seg n
proof defpred P[Nat] means for f being FinSequence of NAT
st len f = $1 & (for d st d in dom f holds f.d>0 & f.d<=$1)
& f is one-to-one holds rng f = Seg $1;
A1:P[0]
proof let f be FinSequence of NAT;
assume len f = 0;
then f = {} by FINSEQ_1:25;
hence thesis by FINSEQ_1:4,27;
end;
A2:for n be Element of NAT st P[n] holds P[n+1]
proof let n be Element of NAT;
assume A3:P[n];
P[n+1] proof let f be FinSequence of NAT;
assume A4:len f = n+1 & (for d st d in dom f holds f.d>0 & f.d<=n+1)
& f is one-to-one;
then A5:f <> {} by FINSEQ_1:25;then
consider f1 being FinSequence of NAT,a being Element of NAT such that
A6: f = f1^<*a*> by HILBERT2:4;
A7: len f = len f1 + 1 by A6,FINSEQ_2:19;
A8: f1 is one-to-one & rng f1 misses rng <*a*> by A4,A6,FINSEQ_3:98;
A9: n+1 in dom f by A4,A5,FINSEQ_5:6;
then f.(n+1) > 0 & f.(n+1) <= n+1 by A4;
then A10:a>0 & a<=n+1 by A4,A6,A7,FINSEQ_1:59;
per cases by A10,REAL_1:def 5;
suppose A11:a = n+1;
for d st d in dom f1 holds f1.d>0 & f1.d<=n
proof let d; assume A12:d in dom f1;
then A13:d in dom f by A6,FINSEQ_2:18;
then A14:f.d>0 & f.d<=n+1 by A4;
then A15:f1.d>0 & f1.d<=n+1 by A6,A12,FINSEQ_1:def 7;
now assume A16:f1.d = n+1;
A17: d <= n by A4,A7,A12,FINSEQ_3:27;
d < n+1 by A17,XREAL_1:147;
then f.d <> f.(n+1) by A4,A9,A13,FUNCT_1:def 8;
then f1.d <> f.(n+1) by A6,A12,FINSEQ_1:def 7;
hence contradiction by A4,A6,A7,A11,A16,FINSEQ_1:59;
end;
then f1.d < n+1 by A15,REAL_1:def 5;
hence thesis by A6,A12,A14,FINSEQ_1:def 7,NAT_1:13;
end;
then rng f1 = Seg n by A3,A4,A7,A8;
then rng f1 \/ {a} = Seg (n+1) by A11,FINSEQ_1:11;
then rng f1 \/ rng <*a*> = Seg (n+1) by FINSEQ_1:55;
hence thesis by A6,FINSEQ_1:44;
end;
suppose A18:a > 0 & a < n+1;
ex d st d in dom f1 & f1.d = n+1
proof assume A19:for d st d in dom f1 holds f1.d <> n+1;
for d being Nat st d in dom f holds f.d in Seg n
proof let d be Nat; assume A20:d in dom f;
then d in Seg(n+1) by A4,FINSEQ_1:def 3;
then A21:d>=1 & d<=n+1 by FINSEQ_1:3;
per cases by A21,REAL_1:def 5;
suppose d=n+1;
then f.d = a by A4,A6,A7,FINSEQ_1:59;
then f.d>=0+1 & f.d<=n by A18,NAT_1:13;
hence thesis by FINSEQ_1:3;
end;
suppose d>=1 & d

= 1 & d <= p' by A20,FINSEQ_1:3;
then d >= 1 & d < p by A18,XXREAL_0:2;
then d,p are_relative_prime by A5,EULER_1:3;
hence thesis by A21,INT_2:def 6;
end;
then (Product I) hcf p = 1 by A5,WSIERP_1:43;
then A22:Product I gcd p = 1 by Lm1;
A23: for d st d in dom f holds f.d = a*d
proof let d; assume A24:d in dom f;
then d in dom I by A2,SEQ_1:def 6;
then d in Seg len I by FINSEQ_1:def 3;
then A25:d is Element of Seg p' by FINSEQ_2:55;
thus f.d = a * I.d by A2,A24,SEQ_1:def 6
.= a*d by A12,A25,FINSEQ_2:57;
end;
A26:len f1 = len f by EULER_2:def 1;
then A27:dom f1 = dom f by FINSEQ_3:31;
f1 <> {} by A7,A12,A26,FINSEQ_1:25;
then rng f1 is non empty Subset of NAT by FINSEQ_1:27,def 4;
then consider n1 being Element of NAT such that
A28:rng f1 c= Seg n1 \/ {0} by HEYTING3:3;
not 0 in rng f1
proof assume 0 in rng f1;
then consider n be Nat such that
A29: n in dom f1 & f1.n = 0 by FINSEQ_2:11;
reconsider a as Element of NAT by ORDINAL1:def 13;
0 = (f.n) mod p by A27,A29,EULER_2:def 1
.= (a*n) mod p by A23,A27,A29;
then p divides (a*n) by A5,PEPIN:6;
then A30:p divides n by A2,A5,WSIERP_1:37;
A31: n >= 1 & n <= p' by A7,A26,A29,FINSEQ_3:27;
then p <= n by A30,NAT_D:7;
hence contradiction by A18,A31,XXREAL_0:2;
end;
then A32:{0} misses rng f1 by ZFMISC_1:56;
then A33:rng f1 c= Seg n1 by A28,XBOOLE_1:73;then
A34: rng f1 = rng f2 by FINSEQ_1:def 13;
for x being set st x in X holds x in rng f1
proof let x be set; assume x in X;
then consider k being Element of NAT such that
A35: x = k & k in rng f1 & k > p/2;
thus thesis by A35;
end;
then A36:X c= rng f1 by TARSKI:def 3;
then reconsider X as finite set by FINSET_1:13;
A37:rng f1 c= NAT by FINSEQ_1:def 4;
then reconsider X as finite Subset of NAT by A36,XBOOLE_1:1;
card X is Element of NAT;
then reconsider m as Element of NAT by A2;
A38:rng f1 \ X c= rng f1 by XBOOLE_1:36;
then reconsider Y = rng f1 \ X as finite Subset of NAT by A37,XBOOLE_1:1;
A39:for d,e being Element of NAT st 1<=d & d

0 & f1.d <= p'
proof let d;assume A54:d in dom f1;
reconsider d as Element of NAT by ORDINAL1:def 13;
f1.d in rng f1 & not f1.d in X by A53,A54,FUNCT_1:12;
then A55:f1.d <= p/2;
A56: f1.d in rng f1 by A54,FUNCT_1:12;
then f1.d in {0} \/ rng f1 by XBOOLE_0:def 2;
then not f1.d in {0} by A32,A56,XBOOLE_0:5;
then f1.d <> 0 by TARSKI:def 1;
hence thesis by A19,A55,INT_1:81;
end;
then rng f1 = rng I by A6,A7,A26,A49,Th40;
then f1,I are_fiberwise_equipotent by A49,RFINSEQ:39;
then Product f1 = Product I by EULER_2:25;
then p divides (1 * Product I - a|^p' * Product I) by A8,A9,INT_2:19;
then p divides (1 - a|^p')*Product I;
then p divides (1 - a|^p') by A22,WSIERP_1:36;
then 1,a|^p' are_congruent_mod p by INT_2:19;
then A57:1,Lege(a,p) are_congruent_mod p by A4,INT_1:36;
now assume Lege(a,p) = -1;
then p divides (1-(-1)) by A57,INT_2:19;
hence contradiction by A2,NAT_D:7;
end;
then Lege(a,p) = 1 by Th25;
hence thesis by A2,A53,CARD_1:78,NEWTON:9;
end;
suppose A58:X is non empty;
A59: f2 = (Sgm Y)^(Sgm X)
proof
for k,l being Element of NAT st k in Y & l in X holds k < l
proof let k,l be Element of NAT;
assume A60:k in Y & l in X;
then k in rng f1 & not k in X by XBOOLE_0:def 4;
then A61:k <= p/2;
ex l1 being Element of NAT st l1 = l & l1 in rng f1 & l1>p/2
by A60;
hence thesis by A61,XXREAL_0:2;
end;
then Sgm (Y\/X) = (Sgm Y)^(Sgm X) by A52,FINSEQ_3:48;
then Sgm (rng f1 \/ X) = (Sgm Y)^(Sgm X) by XBOOLE_1:39;
hence thesis by A36,XBOOLE_1:12;
end;
A62: len Sgm Y = n
proof
Y c= Seg n1 by A33,A38,XBOOLE_1:1;
then len Sgm Y = card Y by FINSEQ_3:44
.= p' - m by A2,A7,A26,A36,A48,CARD_2:63;
hence thesis;
end;
then A63:f2/^n = Sgm X by A59,FINSEQ_5:40;
f2 = (f2|n)^(f2/^n) by RFINSEQ:21;
then A64:f2|n is one-to-one & f2/^n is one-to-one by A50,FINSEQ_3:98;
Sgm Y c= f2 by A59,FINSEQ_6:12;
then A65:f2|n = Sgm Y by A62,FINSEQ_3:122;
A66:m <> 0 by A2,A58,CARD_4:17;
A67:len f2 = p' by A7,A26,A33,A48,FINSEQ_3:44;
then A68:n <= len f2 by XREAL_1:45;
then A69:len(f2|n) = n by FINSEQ_1:80;
set f3 = (len (f2/^n) |-> p) - (f2/^n);
set f4 = (f2|n) ^ f3;
A70:dom f3 = dom(len (f2/^n) |-> p)/\dom(f2/^n) by SEQ_1:def 4
.= (Seg len (len(f2/^n) |-> p))/\dom(f2/^n) by FINSEQ_1:def 3
.= (Seg len(f2/^n))/\dom(f2/^n) by FINSEQ_2:69
.= dom(f2/^n) /\ dom(f2/^n) by FINSEQ_1:def 3
.= dom(f2/^n);
then A71:len f3 = len(f2/^n) by FINSEQ_3:31;
A72:len(f2/^n) = (len f2 -' n) by BINARITH:76
.= len f2 - n by A68,BINARITH:50
.= m by A67;
A73:for d st d in dom f3 holds f3.d = p - (f2/^n).d
proof let d; assume A74:d in dom f3;
then
A75: d in Seg len(f2/^n) by A70,A74,FINSEQ_1:def 3;
p in NAT by ORDINAL1:def 13;
then (len (f2/^n) |-> p).d = p by A66,A72,A75,FINSEQ_2:71;
hence thesis by A74,SEQ_1:def 4;
end;
A76:for d st d in dom f3 holds f3.d > 0 & f3.d <= p'
proof let d; assume A77:d in dom f3;
then A78:f3.d = p - (f2/^n).d by A73;
then reconsider w = f3.d as Element of INT by INT_1:def 2;
(Sgm X).d in rng Sgm X by A63,A70,A77,FUNCT_1:12;
then (Sgm X).d in X by A52,FINSEQ_1:def 13;
then consider ll be Element of NAT such that
A79: ll = (Sgm X).d & ll in rng f1 & ll > p/2;
A80: w < p - p/2 by A63,A78,A79,XREAL_1:12;
consider e being Nat such that
A81:e in dom f1 & f1.e = (f2/^n).d by A63,A79,FINSEQ_2:11;
(f2/^n).d = f.e mod p by A27,A81,EULER_2:def 1;
then (f2/^n).d < p by NAT_D:1;
hence thesis by A19,A78,A80,INT_1:81,XREAL_1:52;
end;
for d being Nat st d in dom f3 holds f3.d in NAT
proof let d be Nat; assume d in dom f3;
then f3.d = p - (f2/^n).d & f3.d > 0 by A73,A76;
hence thesis by INT_1:16;
end;
then reconsider f3 as FinSequence of NAT by FINSEQ_2:14;
for d,e being Element of NAT st 1<=d & d

{} by A8,A9,A14,A19,FINSEQ_1:25;
then rng f is non empty Subset of NAT by FINSEQ_1:27,def 4;
then consider n1 be Element of NAT such that
A24:rng f c= Seg n1 \/ {0} by HEYTING3:3;
not 0 in rng f
proof assume 0 in rng f;
then consider n be Nat such that
A25: n in dom f & f.n = 0 by FINSEQ_2:11;
2*n =0 by A21,A25;
hence contradiction by A25,FINSEQ_3:27;
end;
then {0} misses rng f by ZFMISC_1:56;
then A26:rng f c= Seg n1 by A24,XBOOLE_1:73;
for d1,d2,k1,k2 be Nat st ( 1 <= d1 & d1 < d2 &
d2 <= len f & k1=f.d1 & k2=f.d2) holds k1 < k2
proof let d1,d2,k1,k2 be Nat;
assume A27:1 <= d1 & d1 < d2 & d2 <= len f & k1=f.d1 & k2=f.d2;
then d1 <= len f & 1 <= d2 by XXREAL_0:2;
then d1 in dom f & d2 in dom f by A27,FINSEQ_3:27;
then k1 = 2*d1 & k2 = 2*d2 by A21,A27;
hence thesis by A27,XREAL_1:70;
end;
then A28:Sgm rng f = f by A26,FINSEQ_1:def 13;
A29: Y = Z
proof now let x be set;
assume x in Y;
then consider x1 be Element of NAT such that
A30: x1=x & x1 in dom f & f.x1 >p/2;
2*x1>p/2 by A21,A30;
then A31:x1 > (p/2)/2 by XREAL_1:85;
p/4 >= [\p/4/] by INT_1:def 4;
then x1 > [\p/4/] & [\p/4/] is Element of NAT
by A31,INT_1:80,XXREAL_0:2;
then A32:x1 >= (p div 4) + 1 by NAT_1:13;
x1 <= p' by A14,A19,A30,FINSEQ_3:27;then
x1 <= (p'-'(p div 4) + (p div 4)) by A8,A10,BINARITH:53;
hence x in Z by A30,A32;
end;
then A33:Y c= Z by TARSKI:def 3;
Z c= Y proof
let x be set;
assume A34:x in Z;
then reconsider x as Element of NAT;
A35: x>=(p div 4)+1 & x<=((p-'1) div 2)-'(p div 4)+(p div 4)
by A34,CALCUL_2:1;
then (p div 4)+x >= (p div 4)+1 by NAT_1:12;
then A36:x >= 1 by XREAL_1:8;
x>=(p div 4)+1 & x<=((p-'1) div 2) by A8,A10,A35,BINARITH:53;
then A37:x in dom f by A14,A19,A36,FINSEQ_3:27;
(p div 4)+1 > p/4 by INT_1:52;
then x > p/4 by A35,XXREAL_0:2;
then 2*x > 2*(p/4) by XREAL_1:70;
then f.x > p/2 by A21,A37;
hence thesis by A37;
end;
hence thesis by A33,XBOOLE_0:def 10;
end;
Z,((p-'1) div 2)-'(p div 4) are_equipotent by CALCUL_2:6;
then A38:card Z = card(((p-'1) div 2)-'(p div 4)) by CARD_1:81
.= ((p-'1) div 2)-'(p div 4) by CARD_1:66;
reconsider U=dom f as non empty finite Subset of NAT by A23,FINSEQ_1:26;
X,Y are_equipotent
proof deffunc F(Element of U) = f.$1;
set YY = {d where d is Element of U:F(d) in X};
A39: X,YY are_equipotent
proof A40:now let x be set;
assume x in X;
then consider y be Element of NAT such that
A41: y=x & y in rng f & y > p/2;
consider d being Nat such that
A42: d in U & f.d = y by A41,FINSEQ_2:11;
reconsider d as Element of U by A42;
take d;
thus x=F(d) by A41,A42;
end;
A43: for d1,d2 being Element of U st F(d1) = F(d2) holds d1 = d2
proof let d1,d2 be Element of U;
assume A44:F(d1)=F(d2);
f is one-to-one by A26,A28,FINSEQ_3:99;
hence thesis by A44,FUNCT_1:def 8;
end;
X,YY are_equipotent from FUNCT_7:sch 3(A40,A43);
hence thesis;
end;
Y = YY
proof
A45: Y c= YY proof let x be set; assume x in Y;
then consider d be Element of NAT such that
A46: d = x & d in dom f & f.d > p/2;
reconsider x as Element of U by A46;
f.x in rng f & f.x > p/2 by A46,FUNCT_1:12;
then F(x) in X;
hence thesis;
end;
now let x be set; assume x in YY;
then consider d be Element of U such that
A47: d = x & f.d in X;
consider k be Element of NAT such that
A48: k = f.d & k in rng f & k > p/2 by A47;
thus x in Y by A47,A48;
end;
then YY c= Y by TARSKI:def 3;
hence thesis by A45,XBOOLE_0:def 10;
end;
hence thesis by A39;
end;
then A49:m = ((p-'1) div 2)-'(p div 4) by A29,A38,CARD_1:81;
A50: 2 divides 8 & 4 divides 8
proof 8 = 2*4;
hence thesis by NAT_D:def 3;
end;
A51:p mod 8=1 or p mod 8=3 or p mod 8=5 or p mod 8=7
proof
A52: now assume p mod 8 = 0;
then 8 divides p by PEPIN:6;
then p = 8 by INT_2:def 5;
hence contradiction by A50,NAT_4:12;
end;
A53: now assume p mod 8 = 2;
then 8 divides (p - 2) by PEPIN:8;
then 2 divides (p - 2) by A50,INT_2:13;
then 2 divides -(p-2) by INT_2:14;
then 2 divides (2 - p);
then 2 divides p by Th2;
hence contradiction by A1,NAT_4:12;
end;
A54: now assume p mod 8 = 4;
then 8 divides (p - 4) by PEPIN:8;
then 2 divides (p - 4) by A50,INT_2:13;
then 2 divides -(p - 4) by INT_2:14;
then A55:2 divides (4 - p);
4 = 2*2;
then 2 divides 4 by NAT_D:def 3;
then 2 divides p by A55,Th2;
hence contradiction by A1,NAT_4:12;
end;
A56: now assume p mod 8 = 6;
then 8 divides (p - 6) by PEPIN:8;
then 2 divides (p - 6) by A50,INT_2:13;
then 2 divides -(p - 6) by INT_2:14;
then A57:2 divides (6-p);
6=2*3;
then 2 divides 6 by NAT_D:def 3;
then 2 divides p by A57,Th2;
hence contradiction by A1,NAT_4:12;
end;
p mod 8 < 8 by NAT_D:1;
then p mod 8 <= 8-1 by INT_1:79;
hence thesis by A52,A53,A54,A56,NAT_1:32;
end;
set nn = p div 8;
per cases by A51;
suppose p mod 8 = 1;
then A58:p=8*nn+1 by NAT_D:2;
then p-'1 = 2*(4*nn) by A5;
then A59:(p-'1) div 2 = 4*nn by NAT_D:18;
A60: p div 4 = (4*(2*nn)+1) div 4 by A58 .= 2*nn+(1 div 4) by INT_3:8
.= 2*nn+0 by NAT_D:27;
4*nn>=2*nn by XREAL_1:66;
then m = 4*nn - 2*nn by A49,A59,A60,BINARITH:50
.= 2*nn;
then A61:Lege(2,p) =((-1)|^2)|^nn by A18,NEWTON:14
.= (1|^2)|^nn by WSIERP_1:2 .= 1|^nn by NEWTON:100,SQUARE_1:59
.= 1 by NEWTON:15;
(p^2 -'1) div 8 = (((8*nn)^2 + 2*(8*nn)) + 1-'1) div 8 by A58
.= 8*(8*nn^2 + 2*nn) div 8 by BINARITH:39
.= 8*nn^2 + 2*nn by NAT_D:18;
hence (-1)|^((p^2 -'1) div 8) = (-1)|^(2*(4*nn^2 + nn))
.= ((-1)|^2)|^(4*nn^2 + nn) by NEWTON:14
.= (1|^2)|^(4*nn^2 + nn) by WSIERP_1:2
.= 1|^(4*nn^2 + nn) by NEWTON:15
.= Lege(2,p) by A61,NEWTON:15;
end;
suppose p mod 8 = 3;
then A62:p=8*nn+3 by NAT_D:2;
then p-'1 = 2*(4*nn+1) by A5;
then A63:(p-'1) div 2 = 4*nn+1 by NAT_D:18;
A64: p div 4 = (4*(2*nn)+3) div 4 by A62 .= 2*nn+(3 div 4) by INT_3:8
.= 2*nn+0 by NAT_D:27;
4*nn>=2*nn by XREAL_1:66;
then 4*nn+1>=2*nn by NAT_1:12;
then m = 4*nn+1-2*nn by A49,A63,A64,BINARITH:50 .= 2*nn+1;
then A65:Lege(2,p) = (-1)|^(2*nn)*(-1) by A18,NEWTON:11
.= ((-1)|^2)|^nn*(-1) by NEWTON:14
.= (1|^2)|^nn*(-1) by WSIERP_1:2
.= 1|^nn*(-1) by NEWTON:15
.= 1*(-1) by NEWTON:15 .= -1;
8*(8*nn^2)+8*(6*nn)+3*3 >= 1 by NAT_1:12;
then (p^2 -'1) div 8
= (8*(8*nn^2)+8*(6*nn)+3*3-1) div 8 by A62,BINARITH:50
.= 8*(8*nn^2+6*nn+1) div 8
.= 8*nn^2+6*nn+1 by NAT_D:18;
hence (-1)|^((p^2 -'1) div 8)
= (-1)|^(2*(4*nn^2+3*nn))*(-1) by NEWTON:11
.= ((-1)|^2)|^(4*nn^2+3*nn)*(-1) by NEWTON:14
.= (1|^2)|^(4*nn^2+3*nn)*(-1) by WSIERP_1:2
.= 1|^(4*nn^2+3*nn)*(-1) by NEWTON:15
.= 1*(-1) by NEWTON:15 .= Lege(2,p) by A65;
end;
suppose p mod 8 = 5;
then A66:p=8*nn+5 by NAT_D:2;
then p-'1 = 2*(4*nn+2) by A5;
then A67:(p-'1) div 2 = 4*nn+2 by NAT_D:18;
A68: p div 4 = (4*(2*nn+1)+1) div 4 by A66
.= 2*nn+1+(1 div 4) by INT_3:8
.= 2*nn+1+0 by NAT_D:27;
4*nn>=2*nn by XREAL_1:66;
then 4*nn+2>=2*nn+1 by XREAL_1:9;
then m = 4*nn+2-(2*nn+1) by A49,A67,A68,BINARITH:50
.= 2*nn+1;
then A69:Lege(2,p) = (-1)|^(2*nn)*(-1) by A18,NEWTON:11
.= ((-1)|^2)|^nn*(-1) by NEWTON:14
.= (1|^2)|^nn*(-1) by WSIERP_1:2 .= 1|^nn*(-1) by NEWTON:15
.= 1*(-1) by NEWTON:15 .= -1;
8*(8*nn^2)+8*(10*nn)+5*5 >= 1 by NAT_1:12;
then (p^2 -'1) div 8=(8*(8*nn^2)+8*(10*nn)+25-1) div 8 by A66,BINARITH:50
.= 8*(8*nn^2+10*nn+3) div 8
.= 8*nn^2+10*nn+3 by NAT_D:18;
hence (-1)|^((p^2 -'1) div 8) = (-1)|^(2*(4*nn^2)+2*(5*nn)+2*1+1)
.= (-1)|^(2*(4*nn^2+5*nn+1))*(-1) by NEWTON:11
.= ((-1)|^2)|^(4*nn^2+5*nn+1)*(-1) by NEWTON:14
.= (1|^2)|^(4*nn^2+5*nn+1)*(-1) by WSIERP_1:2
.= 1|^(4*nn^2+5*nn+1)*(-1) by NEWTON:15
.= 1*(-1) by NEWTON:15 .= Lege(2,p) by A69;
end;
suppose p mod 8 = 7;
then A70:p=8*nn+7 by NAT_D:2;
then p-'1 = 2*(4*nn+3) by A5;
then A71:(p-'1) div 2 = 4*nn+3 by NAT_D:18;
A72: p div 4 = (4*(2*nn+1)+3) div 4 by A70
.= 2*nn+1+(3 div 4) by INT_3:8
.= 2*nn+1+0 by NAT_D:27;
4*nn>=2*nn by XREAL_1:66;
then 4*nn+3>=2*nn+1 by XREAL_1:9;
then m = 4*nn+3-(2*nn+1) by A49,A71,A72,BINARITH:50 .= 2*nn+2;
then A73:Lege(2,p) = (-1)|^(2*(nn+1)) by A1,A2,Th41
.= ((-1)|^2)|^(nn+1) by NEWTON:14
.= (1|^2)|^(nn+1) by WSIERP_1:2 .= 1|^(nn+1) by NEWTON:15
.= 1 by NEWTON:15;
8*(8*nn^2)+8*(14*nn)+7*7 >= 1 by NAT_1:12;
then (p^2 -'1) div 8=(8*(8*nn^2)+8*(14*nn)+49-1) div 8 by A70,BINARITH:50
.= 8*(8*nn^2+14*nn+6) div 8
.= 8*nn^2+14*nn+6 by NAT_D:18;
hence (-1)|^((p^2 -'1) div 8) = (-1)|^(2*(4*nn^2+7*nn+3))
.= ((-1)|^2)|^(4*nn^2+7*nn+3) by NEWTON:14
.= (1|^2)|^(4*nn^2+7*nn+3) by WSIERP_1:2
.= 1|^(4*nn^2+7*nn+3) by NEWTON:15
.= Lege(2,p) by A73,NEWTON:15;
end;
end;
theorem
p>2 & (p mod 8 = 1 or p mod 8 = 7) implies 2 is_quadratic_residue_mod p
proof assume A1:p>2 & (p mod 8 = 1 or p mod 8 = 7);
set nn = p div 8;
per cases by A1;
suppose p mod 8 = 1;
then p = 8*nn+1 by NAT_D:2;
then (p^2 -'1) div 8 = (((8*nn)^2 + 2*(8*nn)) + 1-'1) div 8
.= 8*(8*nn^2 + 2*nn) div 8 by BINARITH:39
.= 2*(4*nn^2 + nn) by NAT_D:18;
then Lege(2,p) = (-1)|^(2*(4*nn^2 + nn)) by A1,Th42
.= ((-1)|^2)|^(4*nn^2 + nn) by NEWTON:14
.= (1|^2)|^(4*nn^2 + nn) by WSIERP_1:2
.= 1|^(4*nn^2 + nn) by NEWTON:15
.= 1 by NEWTON:15;
hence thesis by Def3;
end;
suppose p mod 8 = 7;
then A2:p = 8*nn+7 by NAT_D:2;
8*(8*nn^2)+8*(14*nn)+7*7 >= 1 by NAT_1:12;
then (p^2 -'1) div 8=(8*(8*nn^2)+8*(14*nn)+49-1) div 8 by A2,BINARITH:50
.= 8*(8*nn^2+14*nn+6) div 8
.= 2*(4*nn^2+7*nn+3) by NAT_D:18;
then Lege(2,p) = (-1)|^(2*(4*nn^2+7*nn+3)) by A1,Th42
.= ((-1)|^2)|^(4*nn^2+7*nn+3) by NEWTON:14
.= (1|^2)|^(4*nn^2+7*nn+3) by WSIERP_1:2
.= 1|^(4*nn^2+7*nn+3) by NEWTON:15
.= 1 by NEWTON:15;
hence thesis by Def3;
end;
end;
theorem
p>2 & (p mod 8 = 3 or p mod 8 = 5) implies not 2 is_quadratic_residue_mod p
proof assume A1:p>2 & (p mod 8 = 3 or p mod 8 = 5);
set nn = p div 8;
per cases by A1;
suppose p mod 8 = 3;
then A2:p = 8*nn+3 by NAT_D:2;
8*(8*nn^2)+8*(6*nn)+3*3 >= 1 by NAT_1:12;
then (p^2 -'1) div 8
= (8*(8*nn^2)+8*(6*nn)+3*3-1) div 8 by A2,BINARITH:50
.= 8*(8*nn^2+6*nn+1) div 8
.= 8*nn^2+6*nn+1 by NAT_D:18;
then Lege(2,p) = (-1)|^(8*nn^2+6*nn+1) by A1,Th42
.= (-1)|^(2*(4*nn^2+3*nn))*(-1) by NEWTON:11
.= ((-1)|^2)|^(4*nn^2+3*nn)*(-1) by NEWTON:14
.= (1|^2)|^(4*nn^2+3*nn)*(-1) by WSIERP_1:2
.= 1|^(4*nn^2+3*nn)*(-1) by NEWTON:15
.= 1*(-1) by NEWTON:15
.= -1;
hence thesis by Def3;
end;
suppose p mod 8 = 5;
then A3:p = 8*nn+5 by NAT_D:2;
8*(8*nn^2)+8*(10*nn)+5*5 >= 1 by NAT_1:12;
then (p^2 -'1) div 8=(8*(8*nn^2)+8*(10*nn)+25-1) div 8 by A3,BINARITH:50
.= 8*(8*nn^2+10*nn+3) div 8
.= 8*nn^2+10*nn+3 by NAT_D:18;
then Lege(2,p) = (-1)|^(2*(4*nn^2)+2*(5*nn)+2*1+1) by A1,Th42
.= (-1)|^(2*(4*nn^2+5*nn+1))*(-1) by NEWTON:11
.= ((-1)|^2)|^(4*nn^2+5*nn+1)*(-1) by NEWTON:14
.= (1|^2)|^(4*nn^2+5*nn+1)*(-1) by WSIERP_1:2
.= 1|^(4*nn^2+5*nn+1)*(-1) by NEWTON:15
.= 1*(-1) by NEWTON:15
.= -1;
hence thesis by Def3;
end;
end;
theorem Th45:
for a,b be Nat st a mod 2 = b mod 2 holds (-1)|^a = (-1)|^b
proof let a,b be Nat;
assume a mod 2 = b mod 2;
then a,b are_congruent_mod 2 by INT_3:12;
then A1:2 divides (a-b) by INT_2:19;
per cases;
suppose a>=b;
then reconsider l=a-b as Element of NAT by NAT_1:21;
consider n be Nat such that A2:l=2*n by A1,NAT_D:def 3;
(-1)|^a = (-1)|^(b + (2*n)) by A2
.= ((-1)|^b) * ((-1)|^(2*n)) by NEWTON:13
.= (-1)|^b * ((-1)|^2)|^n by NEWTON:14
.= (-1)|^b * (1|^2)|^n by WSIERP_1:2
.= (-1)|^b * 1|^n by NEWTON:15
.= (-1)|^b * 1 by NEWTON:15;
hence thesis;
end;
suppose a** m) - f) = (len f)*m - Sum f
proof defpred P[Nat] means for f be FinSequence of REAL,m be Real
st len f = $1 holds Sum(($1|-> m) - f) = $1 * m - Sum f;
A1:P[0] proof let f be FinSequence of REAL,m be Real;
assume A2:len f = 0;
then A3:(len f) |-> m = <*>REAL by FINSEQ_2:72;
Sum f = 0 by A2,PROB_3:67;
hence thesis by A2,A3,RVSUM_1:49,102;
end;
A4: for n be Element of NAT st P[n] holds P[n+1]
proof let n be Element of NAT;
assume A5:P[n];
P[n+1] proof let f be FinSequence of REAL,m be Real;
assume A6:len f = n+1;
f <> {} by A6,FINSEQ_1:25;then
consider f1 be FinSequence of REAL,x be Element of REAL such that
A7: f = f1^<*x*> by HILBERT2:4;
A8: n + 1 = len f1 + 1 by A6,A7,FINSEQ_2:19;then
A9: len(n|-> m)=len f1 & len<*x*> = 1 & len<*m*> = 1
by FINSEQ_1:56,FINSEQ_2:69;
((n+1)|-> m)-f
= (n|-> m)^<*m*> - f1^<*x*> by A7,FINSEQ_2:74
.= ((n|-> m)-f1) ^ (<*m*>-<*x*>) by A9,Th46
.= ((n|-> m)-f1) ^ <*m-x*> by RVSUM_1:50;
hence Sum(((n+1)|-> m)-f)
= Sum((n|-> m)-f1) + (m-x) by RVSUM_1:104
.= n*m - Sum f1 + (m - x) by A5,A8
.= (n+1)*m - (Sum f1 + x)
.= (n+1)*m - Sum f by A7,RVSUM_1:104;
end;
hence thesis;
end;
for n be Element of NAT holds P[n] from NAT_1:sch 1(A1,A4);
hence thesis;
end;
reserve X for finite set,
F for FinSequence of bool X;
definition let X, F;
redefine func Card F -> Cardinal-yielding FinSequence of NAT;
coherence proof
rng Card F c= NAT proof let y be set; assume y in rng Card F;
then consider x being set such that
A1: x in dom Card F & y = (Card F).x by FUNCT_1:def 5;
A2: x in dom F by A1,CARD_3:def 2;
then F.x in rng F by FUNCT_1:12;
then reconsider Fx = F.x as finite set by FINSET_1:13;
y = card Fx by A1,A2,CARD_3:def 2;
hence thesis;
end;
hence thesis by FINSEQ_1:def 4;
end;
end;
theorem Th48: for f be FinSequence of bool X st len f = n &
(for d,e st d in dom f & e in dom f & d<>e holds f.d misses f.e)
holds
Card union rng f = Sum Card f
proof defpred P[Nat] means for f be FinSequence of bool X st
len f = $1 & (for d,e st d in dom f & e in dom f & d<>e
holds f.d misses f.e) holds Card union rng f = Sum Card f;
A1: P[0] proof let f be FinSequence of bool X;
assume len f = 0 & (for d,e st d in dom f & e in dom f & d<>e
holds f.d misses f.e);
then f = {} by FINSEQ_1:25;
hence thesis by CARD_1:78,CARD_3:9,FINSEQ_1:27,RVSUM_1:102,ZFMISC_1:2;
end;
A2: for n be Element of NAT st P[n] holds P[n+1]
proof let n be Element of NAT; assume A3:P[n];
P[n+1] proof let f be FinSequence of bool X;
assume A4:len f = n+1 &
(for d,e st d in dom f & e in dom f & d<>e holds f.d misses f.e);
A5:f <> {} by A4,FINSEQ_1:25;
then consider f1 be FinSequence of bool X,Y be Element of bool X
such that A6:f = f1^<*Y*> by HILBERT2:4;
A7: n+1 = len f1 +1 by A4,A6,FINSEQ_2:19;
for d,e st d in dom f1 & e in dom f1 & d<>e holds f1.d misses f1.e
proof let d,e;
assume A8: d in dom f1 & e in dom f1 & d<>e;
then A9:f.d = f1.d & f.e = f1.e by A6,FINSEQ_1:def 7;
d in dom f & e in dom f by A6,A8,FINSEQ_2:18;
hence thesis by A4,A8,A9;
end;
then A10:Card union rng f1 = Sum Card f1 by A3,A7;
Union f1 is finite;
then reconsider F1 = union(rng f1) as finite set;
F1 misses Y
proof assume F1 meets Y;
then consider x be set such that
A11: x in F1 /\ Y by XBOOLE_0:4;
x in F1 by A11,XBOOLE_0:def 3;
then consider Z be set such that
A12: x in Z & Z in rng f1 by TARSKI:def 4;
consider k be Nat such that
A13: k in dom f1 & f1.k = Z by A12,FINSEQ_2:11;
k <= n by A7,A13,FINSEQ_3:27;then
A14: k < n + 1 by NAT_1:13;
A15: n+1 in dom f by A4,A5,FINSEQ_5:6;
k in dom f by A6,A13,FINSEQ_2:18;
then f.(n+1) misses f.k by A4,A14,A15;
then Y misses f.k by A6,A7,FINSEQ_1:59;
then A16:Y misses Z by A6,A13,FINSEQ_1:def 7;
x in Y \/ Z by A12,XBOOLE_0:def 2;
then not x in Y by A12,A16,XBOOLE_0:5;
hence contradiction by A11,XBOOLE_0:def 3;
end;
then A17:card F1 + card Y = card(F1\/Y) by CARD_2:53;
card Y = Card Y;then
reconsider gg = <*Card Y*> as FinSequence of NAT by FINSEQ_1:95;
A18:Card f = Card f1 ^ Card<*Y*> by A6,POLYNOM1:13
.= Card f1 ^ gg by POLYNOM1:12;
union(rng f) = union((rng f1) \/ (rng <*Y*>)) by A6,FINSEQ_1:44
.= union((rng f1) \/ {Y}) by FINSEQ_1:55
.= F1 \/ union {Y} by ZFMISC_1:96
.= F1 \/ Y by ZFMISC_1:31;
hence thesis by A10,A17,A18,RVSUM_1:104;
thus thesis;
end;
hence thesis;
end;
for n be Element of NAT holds P[n] from NAT_1:sch 1(A1,A2);
hence thesis;
end;
Lm4: Sum(fp) is Element of NAT;
reserve q for Prime;
theorem Th49:p>2 & q>2 & p<>q
implies Lege(p,q)*Lege(q,p)=(-1)|^(((p-'1) div 2)*((q-'1) div 2))
proof assume A1:p>2 & q>2 & p<>q;
then A2:q,p are_relative_prime by INT_2:47;
then A3:q hcf p = 1 by INT_2:def 6;
reconsider p,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';
dom f1 = dom idseq p' by SEQ_1:def 6;then
A5:len f1 = len idseq p' by FINSEQ_3:31;then
A6:len f1 = p' by FINSEQ_2:55;
A7: p>1 & q>1 by INT_2:def 5;
then A8:p-'1 = p-1 & q-'1 = q-1 by BINARITH:50;
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 & q' >= 1 by A8,NAT_2:15;
p is odd & q is odd 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' & q-'1 = 2*q' by NAT_D:3;
then A13:p' divides (p-'1) & q' divides (q-'1) by NAT_D:def 3;
p-'1>0 & q-'1 >0 by A7,A8,XREAL_1:52;
then A14:p' <= (p-'1) & q' <= (q-'1) by A13,NAT_D:7;
A15: p-'1 < p & q-'1 < q by A8,XREAL_1:148;
then A16:p' < p & q' < q by A14,XXREAL_0:2;
A17:p' = ((p-'1)+1) div 2 by A10,NAT_2:28
.= p div 2 by A7,BINARITH:53;
A18:q' = ((q-'1)+1) div 2 by A10,NAT_2:28
.= q div 2 by A7,BINARITH:53;
A19: for d st d in dom f1 holds f1.d = q*d
proof let d; assume A20:d in dom f1;
then A21:f1.d = q * (idseq p').d by SEQ_1:def 6;
d in dom idseq p' by A20,SEQ_1:def 6;
then d in Seg len idseq p' by FINSEQ_1:def 3;
then d is Element of Seg p' by FINSEQ_2:55;
hence thesis by A9,A21,FINSEQ_2:57;
end;
for d being Nat st d in dom f1 holds f1.d in NAT
proof let d be Nat; assume d in dom f1;
then f1.d = q*d by A19;
hence thesis by ORDINAL1:def 13;
end;
then reconsider f1 as FinSequence of NAT by FINSEQ_2:14;
A22: for d,e st d in dom f1 & e in dom f1 & p divides (f1.d-f1.e) holds d=e
proof let d,e;
assume A23:d in dom f1 & e in dom f1 & p divides (f1.d-f1.e);
then f1.d = q*d & f1.e = q*e by A19;
then A24:p divides (d-e)*q by A23;
q,(p qua Integer) are_relative_prime by A2,EULER_2:1;
then A25:p divides (d - e) by A24,INT_2:40;
now assume d <> e;
then d-e <> 0;
then abs(p) <= abs(d-e) by A25,INT_4:6;
then A26:p <= abs(d-e) by ABSVALUE:def 1;
d>=1 & d<=p' & e>=1 & e<=p' by A6,A23,FINSEQ_3:27;
then A27:d-e<=p'-1 & d-e>=1-p' by XREAL_1:15;
A28: p'-1**

-p by A28,XREAL_1:26;
then d-e > -p by A27,XXREAL_0:2;
hence contradiction by A26,A29,SEQ_2:9;
end;
hence thesis;
end;
deffunc F(Nat) = f1.$1 div p;
consider f2 be FinSequence such that
A30:len f2 = p' &
for d being Element of NAT st d in dom f2 holds f2.d = F(d)
from FINSEQ_5:sch 1;
for d being Nat st d in dom f2 holds f2.d in NAT
proof let d be Nat;assume d in dom f2;
then f2.d = f1.d div p by A30;
hence thesis;
end;
then reconsider f2 as FinSequence of NAT by FINSEQ_2:14;
set f3 = f1 mod p;
A31:len f3 = len f1 by EULER_2:def 1;
then A32:dom f1 = dom f3 by FINSEQ_3:31;
A33: dom f1 = dom f2 by A6,A30,FINSEQ_3:31;
A34: dom (p*f2+f3) = dom (p*f2) /\ dom f3 by SEQ_1:def 3
.= dom f2 /\ dom f3 by SEQ_1:def 6
.= dom f1 by A32,A33;
A35: for d st d in dom f1 holds f1.d = f2.d * p + f3.d
proof let d; assume d in dom f1;
then f2.d = f1.d div p & f3.d = f1.d mod p by A30,A33,EULER_2:def 1;
hence f1.d = f2.d * p + f3.d by NAT_D:2;
end;
for d being Nat st d in dom f1 holds f1.d = (p*f2+f3).d
proof let d be Nat; assume A36:d in dom f1;
then A37:(p*f2+f3).d = (p*f2).d + f3.d by A34,SEQ_1:def 3;
d in dom (p*f2) by A33,A36,SEQ_1:def 6;
hence (p*f2+f3).d = p * f2.d + f3.d by A37,SEQ_1:def 6
.= f1.d by A35,A36;
end;
then A38:f1 = p*f2 + f3 by A34,FINSEQ_1:17;
A39: p*f2 is Element of NAT* & f3 is Element of NAT* by FINSEQ_1:def 11;
dom(p*f2) = dom f2 by SEQ_1:def 6;
then len(p*f2) = p' & len f3 = p' by A5,A30,A31,FINSEQ_2:55,FINSEQ_3:31;
then p*f2 in p'-tuples_on NAT & f3 in p'-tuples_on NAT by A39;
then p*f2 is Element of p'-tuples_on REAL &
f3 is Element of p'-tuples_on REAL by FINSEQ_2:129;
then A40:Sum f1 = Sum(p*f2) + Sum f3 by A38,RVSUM_1:119
.= p*(Sum f2) + Sum f3 by RVSUM_1:117;
then A41:q*(Sum idseq p') = p*(Sum f2) + Sum f3 by RVSUM_1:117;
f3 <> {} by A6,A9,A31,FINSEQ_1:28;then
rng f3 is finite non empty Subset of NAT by FINSEQ_1:27,def 4;
then consider n1 be Element of NAT such that
A42: rng f3 c= Seg n1 \/ {0} by HEYTING3:3;
not 0 in rng f3
proof assume 0 in rng f3;
then consider a be Nat such that
A43: a in dom f3 & f3.a = 0 by FINSEQ_2:11;
f1.a = f2.a * p + 0 by A32,A35,A43;
then q*a = f2.a *p by A19,A32,A43;
then p divides q*a by NAT_D:def 3;
then A44:p divides a by A2,PEPIN:3;
A45: a >= 1 & a <= p' by A6,A31,A43,FINSEQ_3:27;
then p <= a by A44,NAT_D:7;
hence contradiction by A16,A45,XXREAL_0:2;
end;
then A46:{0} misses rng f3 by ZFMISC_1:56;
then A47:rng f3 c= Seg n1 by A42,XBOOLE_1:73;
for x,y be set st x in dom f3 & y in dom f3 & f3.x=f3.y holds x=y
proof let x,y be set;
assume A48:x in dom f3 & y in dom f3 & f3.x=f3.y;
then reconsider x,y as Element of NAT;
f1.x = f2.x * p + f3.x & f1.y = f2.y * p + f3.y by A32,A35,A48;
then f1.x - f1.y = (f2.x - f2.y) * p by A48;
then p divides (f1.x - f1.y) by INT_1:def 9;
hence thesis by A22,A32,A48;
end;
then A49:f3 is one-to-one by FUNCT_1:def 8;
set f4 = Sgm rng f3;
set X = {k where k is Element of NAT:k in rng f4 & k>p/2};
A50: rng f4 = rng f3 by A47,FINSEQ_1:def 13;
A51: f4 is one-to-one by A47,FINSEQ_3:99;
then A52:f4,f3 are_fiberwise_equipotent by A49,A50,RFINSEQ:39;
f4 is FinSequence of REAL & f3 is FinSequence of REAL by FINSEQ_2:27;
then A53:Sum f4 = Sum f3 by A52,RFINSEQ:22;
for x being set st x in X holds x in rng f4
proof let x be set; assume x in X;
then consider k being Element of NAT such that
A54: x = k & k in rng f4 & k > p/2;
thus thesis by A54;
end;
then A55:X c= rng f4 by TARSKI:def 3;
then reconsider X as finite Subset of NAT by FINSET_1:13,XBOOLE_1:1;
A56:X c= Seg n1 by A47,A50,A55,XBOOLE_1:1;
reconsider Y = rng f4 \ X as finite Subset of NAT;
rng f4 \ X c= rng f4 by XBOOLE_1:36;then
A57:Y c= Seg n1 by A47,A50,XBOOLE_1:1;
set m = card X;
A58:len f3 = card rng f4 by A49,A50,FINSEQ_4:77;
then m <= len f3 by A55,CARD_1:80;
then reconsider n = p' - m as Element of NAT by A6,A31,NAT_1:21;
len f3 = card rng f3 by A49,FINSEQ_4:77;then
A59:len f4 = p' by A6,A31,A47,FINSEQ_3:44;
A60:f4 = (Sgm Y)^(Sgm X)
proof
for k,l being Element of NAT st k in Y & l in X holds k < l
proof let k,l be Element of NAT;
assume A61:k in Y & l in X;
then k in rng f4 & not k in X by XBOOLE_0:def 4;
then A62:k <= p/2;
ex l1 being Element of NAT st l1 = l & l1 in rng f4 & l1>p/2
by A61;
hence thesis by A62,XXREAL_0:2;
end;
then Sgm (Y\/X) = (Sgm Y)^(Sgm X) by A56,A57,FINSEQ_3:48;
then Sgm (rng f4 \/ X) = (Sgm Y)^(Sgm X) by XBOOLE_1:39;
hence thesis by A50,A55,XBOOLE_1:12;
end;
Sum f4 = Sum(Sgm Y) + Sum(Sgm X) by A60,RVSUM_1:105;
then A63:q*(Sum idseq p')=p*(Sum f2)+Sum(Sgm Y) + Sum(Sgm X)
by A40,A53,RVSUM_1:117;
A64: len Sgm Y = n
proof
len Sgm Y = card Y by A57,FINSEQ_3:44
.= p' - m by A6,A31,A55,A58,CARD_2:63;
hence thesis;
end;
then A65:f4/^n = Sgm X by A60,FINSEQ_5:40;
f4 = (f4|n)^(f4/^n) by RFINSEQ:21;then
A66:f4|n is one-to-one & f4/^n is one-to-one by A51,FINSEQ_3:98;
Sgm Y c= f4 by A60,FINSEQ_6:12;
then A67:f4|n = Sgm Y by A64,FINSEQ_3:122;
for d being Nat st d in dom idseq p' holds (idseq p').d in NAT
proof let d be Nat; assume d in dom idseq p';
then
A68: d in Seg len idseq p' by FINSEQ_1:def 3;
then d is Element of Seg p' by FINSEQ_2:55;
then (idseq p').d = d by A9,FINSEQ_2:57;
hence thesis by A68;
end;
then idseq p' is FinSequence of NAT by FINSEQ_2:14;
then reconsider M = Sum idseq p' as Element of NAT by Lm4;
A69: Lege(q,p) = (-1)|^(Sum f2)
proof per cases;
suppose A70:X is empty;
for d st d in dom f4 holds f4.d > 0 & f4.d <= p'
proof let d; assume A71:d in dom f4;
A72: not f4.d in X by A70;
f4.d in rng f4 by A71,FUNCT_1:12;then
A73: f4.d <= p/2 by A72;
A74: f4.d in rng f3 by A50,A71,FUNCT_1:12;
then f4.d in (rng f3)\/{0} by XBOOLE_0:def 2;
then not f4.d in {0} by A46,A74,XBOOLE_0:5;
then f4.d <> 0 by TARSKI:def 1;
hence thesis by A17,A73,INT_1:81;
end;
then Sgm rng f3 = Sgm(Seg p') by A50,A51,A59,Th40;
then q*(Sum idseq p') = p*(Sum f2) + Sum idseq p'
by A41,A53,FINSEQ_3:54;
then A75:q*(Sum idseq p') - Sum idseq p' = p*(Sum f2);
2 divides (q-'1)*M by A11,NAT_D:9;
then 2 divides ((Sum f2)-0) by A4,A8,A75,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)|^m = (-1)|^(Sum f2) by A70,Th45,CARD_1:78;
hence thesis by A1,A3,A50,Th41;
end;
suppose X is non empty;
then A76:m <> 0 by CARD_4:17;
A77: n <= len f4 by A59,XREAL_1:45;then
A78: len(f4|n) = n by FINSEQ_1:80;
A79: len(f4/^n) = (len f4 -' n) by BINARITH:76
.= len f4 - n by A77,BINARITH:50
.= m by A59;
set f5 = (m|->p)-(f4/^n);
set f6 = (f4|n)^f5;
A80:dom f5 = dom(m |-> p) /\ dom(f4/^n) by SEQ_1:def 4
.= (Seg len (m |-> p)) /\ dom(f4/^n) by FINSEQ_1:def 3
.= (Seg len(f4/^n))/\dom(f4/^n) by A79,FINSEQ_2:69
.= dom(f4/^n) /\ dom(f4/^n) by FINSEQ_1:def 3
.= dom(f4/^n);
then A81:len f5 = len(f4/^n) by FINSEQ_3:31;
A82:for d st d in dom f5 holds f5.d = p - (f4/^n).d
proof let d; assume A83:d in dom f5;
then d in Seg m by A79,A80,FINSEQ_1:def 3;
then (m |-> p).d = p by A76,FINSEQ_2:71;
hence thesis by A83,SEQ_1:def 4;
end;
A84:for d st d in dom f5 holds f5.d > 0 & f5.d <= p'
proof let d; assume A85:d in dom f5;
then A86:f5.d = p - (f4/^n).d by A82;
then reconsider w = f5.d as Element of INT by INT_1:def 2;
(Sgm X).d in rng Sgm X by A65,A80,A85,FUNCT_1:12;
then (Sgm X).d in X by A56,FINSEQ_1:def 13;
then consider ll be Element of NAT such that
A87: ll = (Sgm X).d & ll in rng f3 & ll > p/2 by A50;
A88: w < p - p/2 by A65,A86,A87,XREAL_1:12;
consider e being Nat such that
A89:e in dom f3 & f3.e = (f4/^n).d by A65,A87,FINSEQ_2:11;
(f4/^n).d = f1.e mod p by A32,A89,EULER_2:def 1;
then (f4/^n).d < p by NAT_D:1;
hence thesis by A17,A86,A88,INT_1:81,XREAL_1:52;
end;
for d being Nat st d in dom f5 holds f5.d in NAT
proof let d be Nat; assume d in dom f5;
then f5.d = p - (f4/^n).d & f5.d > 0 by A82,A84;
hence thesis by INT_1:16;
end;
then reconsider f5 as FinSequence of NAT by FINSEQ_2:14;
for d,e being Element of NAT st 1<=d & d -q by A122,XREAL_1:26;
then d-e > -q by A121,XXREAL_0:2;
hence contradiction by A120,A123,SEQ_2:9;
end;
hence thesis;
end;
deffunc F(Nat) = g1.$1 div q;
consider g2 be FinSequence such that
A124:len g2 = q' & for d being Element of NAT st d in dom g2 holds g2.d = F(d)
from FINSEQ_5:sch 1;
for d being Nat st d in dom g2 holds g2.d in NAT
proof let d be Nat;assume d in dom g2;
then g2.d = g1.d div q by A124;
hence thesis;
end;
then reconsider g2 as FinSequence of NAT by FINSEQ_2:14;
set g3 = g1 mod q;
A125: len g3 = len g1 by EULER_2:def 1;then
A126: dom g1 = dom g3 by FINSEQ_3:31;
A127: dom g1 = dom g2 by A112,A124,FINSEQ_3:31;
A128: dom (q*g2+g3) = dom (q*g2) /\ dom g3 by SEQ_1:def 3
.= dom g2 /\ dom g3 by SEQ_1:def 6
.= dom g1 by A126,A127;
A129: for d st d in dom g1 holds g1.d = g2.d * q + g3.d
proof let d; assume d in dom g1;
then g2.d = g1.d div q & g3.d = g1.d mod q by A124,A127,EULER_2:def 1;
hence g1.d = g2.d * q + g3.d by NAT_D:2;
end;
for d being Nat st d in dom g1 holds g1.d = (q*g2+g3).d
proof let d be Nat; assume A130:d in dom g1;
then A131:(q*g2+g3).d = (q*g2).d + g3.d by A128,SEQ_1:def 3;
d in dom (q*g2) by A127,A130,SEQ_1:def 6;
hence (q*g2+g3).d = q * g2.d + g3.d by A131,SEQ_1:def 6
.= g1.d by A129,A130;
end;
then A132:g1 = q*g2 + g3 by A128,FINSEQ_1:17;
A133: q*g2 is Element of NAT* & g3 is Element of NAT* by FINSEQ_1:def 11;
dom(q*g2) = dom g2 by SEQ_1:def 6;
then len(q*g2) = q' & len g3 = q' by A112,A124,EULER_2:def 1,FINSEQ_3:31;
then A134:q*g2 in q'-tuples_on NAT & g3 in q'-tuples_on NAT by A133;
q*g2 is Element of q'-tuples_on REAL & g3 is Element of q'-tuples_on REAL
by A134,FINSEQ_2:129;
then A135:Sum g1 = Sum(q*g2) + Sum g3 by A132,RVSUM_1:119
.= q*(Sum g2) + Sum g3 by RVSUM_1:117;
len g3 >=1 by A9,A112,EULER_2:def 1;
then g3 <> {} by FINSEQ_1:28;
then rng g3 is finite non empty Subset of NAT
by FINSEQ_1:27,def 4;
then consider n2 be Element of NAT such that
A136: rng g3 c= Seg n2 \/ {0} by HEYTING3:3;
not 0 in rng g3
proof assume 0 in rng g3;
then consider a be Nat such that
A137: a in dom g3 & g3.a = 0 by FINSEQ_2:11;
a in dom g1 by A125,A137,FINSEQ_3:31;then
A138: g1.a = g2.a * q + 0 by A129,A137;
a in dom g1 by A125,A137,FINSEQ_3:31;
then p*a = g2.a * q by A113,A138;
then q divides p*a by NAT_D:def 3;
then A139:q divides a by A2,PEPIN:3;
A140: a >= 1 & a <= q' by A112,A125,A137,FINSEQ_3:27;
then q <= a by A139,NAT_D:7;
hence contradiction by A16,A140,XXREAL_0:2;
end;
then A141:{0} misses rng g3 by ZFMISC_1:56;
then A142:rng g3 c= Seg n2 by A136,XBOOLE_1:73;
for x,y be set st x in dom g3 & y in dom g3 & g3.x=g3.y holds x=y
proof let x,y be set;
assume A143:x in dom g3 & y in dom g3 & g3.x=g3.y;
then reconsider x,y as Element of NAT;
g1.x = g2.x * q + g3.x & g1.y = g2.y * q + g3.y by A126,A129,A143;
then g1.x - g1.y = (g2.x - g2.y) * q by A143;
then q divides (g1.x - g1.y) by INT_1:def 9;
hence thesis by A116,A126,A143;
end;
then A144:g3 is one-to-one by FUNCT_1:def 8;
set g4 = Sgm rng g3;
set XX = {k where k is Element of NAT:k in rng g4 & k>q/2};
A145: rng g4 = rng g3 by A142,FINSEQ_1:def 13;
A146: g4 is one-to-one by A142,FINSEQ_3:99;
then A147:g4,g3 are_fiberwise_equipotent by A144,A145,RFINSEQ:39;
g4 is FinSequence of REAL & g3 is FinSequence of REAL by FINSEQ_2:27;
then A148:Sum g4 = Sum g3 by A147,RFINSEQ:22;
for x being set st x in XX holds x in rng g4
proof let x be set; assume x in XX;
then consider k being Element of NAT such that
A149: x = k & k in rng g4 & k > q/2;
thus thesis by A149;
end;
then A150:XX c= rng g4 by TARSKI:def 3;
then reconsider XX as finite Subset of NAT by FINSET_1:13,XBOOLE_1:1;
reconsider YY = rng g4 \ XX as finite Subset of NAT;
rng g4 \ XX c= rng g4 by XBOOLE_1:36;then
A151:YY c= Seg n2 by A142,A145,XBOOLE_1:1;
set mm = card XX;
A152:len g3 = card rng g4 by A144,A145,FINSEQ_4:77;
mm <= card rng g4 by A150,CARD_1:80;
then mm <= q' by A112,A152,EULER_2:def 1;
then reconsider nn = q' - mm as Element of NAT by NAT_1:21;
len g3 = card rng g3 by A144,FINSEQ_4:77;then
A153:len g4 = q' by A112,A125,A142,FINSEQ_3:44;
A154:XX c= Seg n2 by A142,A145,A150,XBOOLE_1:1;
A155:g4 = (Sgm YY)^(Sgm XX)
proof
per cases;
suppose A156:YY is empty;
then rng g4 c= XX by XBOOLE_1:37;
then XX = rng g4 by A150,XBOOLE_0:def 10;
hence g4 = (Sgm YY)^(Sgm XX) by A145,A156,FINSEQ_1:47,FINSEQ_3:49;
end;
suppose YY is non empty;
for k,l being Element of NAT st k in YY & l in XX holds k < l
proof let k,l be Element of NAT;
assume A157:k in YY & l in XX;
then k in rng g4 & not k in XX by XBOOLE_0:def 4;
then A158:k <= q/2;
ex l1 being Element of NAT st l1 = l & l1 in rng g4 & l1>q/2
by A157;
hence thesis by A158,XXREAL_0:2;
end;
then Sgm (YY\/XX) = (Sgm YY)^(Sgm XX) by A151,A154,FINSEQ_3:48;
then Sgm (rng g4 \/ XX) = (Sgm YY)^(Sgm XX) by XBOOLE_1:39;
hence thesis by A145,A150,XBOOLE_1:12;
end;
end;
Sum g4 = Sum(Sgm YY) + Sum(Sgm XX) by A155,RVSUM_1:105;
then A159:p*(Sum idseq q')=q*(Sum g2)+Sum(Sgm YY)+Sum(Sgm XX)
by A135,A148,RVSUM_1:117;
A160: len Sgm YY = nn
proof
len Sgm YY = card YY by A151,FINSEQ_3:44
.= q' - mm by A112,A125,A150,A152,CARD_2:63;
hence thesis;
end;
then A161:g4/^nn = Sgm XX by A155,FINSEQ_5:40;
g4 = (g4|nn)^(g4/^nn) by RFINSEQ:21;then
A162:g4|nn is one-to-one & g4/^nn is one-to-one by A146,FINSEQ_3:98;
Sgm YY c= g4 by A155,FINSEQ_6:12;
then A163:g4|nn = Sgm YY by A160,FINSEQ_3:122;
for d being Nat st d in dom idseq q' holds (idseq q').d in NAT
proof let d be Nat; assume d in dom idseq q';
then d in Seg len idseq q' by FINSEQ_1:def 3;
then d is Element of Seg q' by FINSEQ_2:55;
then (idseq q').d = d by A9,FINSEQ_2:57;
hence thesis by ORDINAL1:def 13;
end;
then idseq q' is FinSequence of NAT by FINSEQ_2:14;
then reconsider N = Sum idseq q' as Element of NAT by Lm4;
A164: Lege(p,q) = (-1)|^(Sum g2)
proof per cases;
suppose A165:XX is empty;
for d st d in dom g4 holds g4.d > 0 & g4.d <= q'
proof let d; assume d in dom g4;
then A166:g4.d in rng g4 by FUNCT_1:12;
not g4.d in XX by A165;
then A167:g4.d <= q/2 by A166;
g4.d in (rng g3)\/{0} by A145,A166,XBOOLE_0:def 2;
then not g4.d in {0} by A141,A145,A166,XBOOLE_0:5;
then g4.d <> 0 by TARSKI:def 1;
hence thesis by A18,A167,INT_1:81;
end;
then rng g3 = Seg q' by A145,A146,A153,Th40;
then g4 = idseq q' by FINSEQ_3:54;
then p*N = q*(Sum g2) + N by A135,A148,RVSUM_1:117;
then p*N - N = q*(Sum g2);
then A168:(p-'1)*N = q*(Sum g2) by A8;
2 divides q*(Sum g2) by A11,A168,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)|^mm = (-1)|^(Sum g2) by A165,Th45,CARD_1:78;
hence thesis by A1,A3,A145,Th41;
end;
suppose XX is non empty;
then A169:mm <> 0 by CARD_4:17;
A170: nn <= len g4 by A153,XREAL_1:45;then
A171: len(g4|nn) = nn by FINSEQ_1:80;
A172: len(g4/^nn) = (len g4 -' nn) by BINARITH:76
.= len g4 - nn by A170,BINARITH:50
.= mm by A153;
set g5 = (mm|->q)-(g4/^nn);
set g6 = (g4|nn)^g5;
A173:dom g5 = dom(mm |-> q) /\ dom(g4/^nn) by SEQ_1:def 4
.= (Seg len (mm |-> q)) /\ dom(g4/^nn) by FINSEQ_1:def 3
.= (Seg len(g4/^nn))/\dom(g4/^nn) by A172,FINSEQ_2:69
.= dom(g4/^nn) /\ dom(g4/^nn) by FINSEQ_1:def 3
.= dom(g4/^nn);
then A174:len g5 = len(g4/^nn) by FINSEQ_3:31;
A175:for d st d in dom g5 holds g5.d = q - (g4/^nn).d
proof let d; assume A176:d in dom g5;
then d in Seg mm by A172,A173,FINSEQ_1:def 3;
then (mm |-> q).d = q by A169,FINSEQ_2:71;
hence thesis by A176,SEQ_1:def 4;
end;
A177:for d st d in dom g5 holds g5.d > 0 & g5.d <= q'
proof let d; assume A178:d in dom g5;
then A179:g5.d = q - (g4/^nn).d by A175;
then reconsider w = g5.d as Element of INT by INT_1:def 2;
(Sgm XX).d in rng Sgm XX by A161,A173,A178,FUNCT_1:12;
then (Sgm XX).d in XX by A154,FINSEQ_1:def 13;
then consider ll be Element of NAT such that
A180: ll = (Sgm XX).d & ll in rng g3 & ll > q/2 by A145;
A181: w < q - q/2 by A161,A179,A180,XREAL_1:12;
consider e being Nat such that
A182:e in dom g3 & g3.e=(g4/^nn).d by A161,A180,FINSEQ_2:11;
(g4/^nn).d = g1.e mod q by A126,A182,EULER_2:def 1;
then (g4/^nn).d < q by NAT_D:1;
hence thesis by A18,A179,A181,INT_1:81,XREAL_1:52;
end;
for d being Nat st d in dom g5 holds g5.d in NAT
proof let d be Nat; assume d in dom g5;
then g5.d = q - (g4/^nn).d & g5.d > 0 by A175,A177;
hence thesis by INT_1:16;
end;
then reconsider g5 as FinSequence of NAT by FINSEQ_2:14;
for d,e being Element of NAT st 1<=d & d