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 that
A1: p>2 and
A2: a gcd p = 1 and
A3: b gcd p = 1 and
A4: a is_quadratic_residue_mod p and
A5: not b is_quadratic_residue_mod p;
A6: a*b gcd p = 1 by A2,A3,WSIERP_1:6;
set l = (p-'1) div 2;
(b|^l + 1) mod p = 0 by A1,A3,A5,Th21; then
A7: p divides (b|^l + 1) by INT_1:62;
A8: (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:7
.= ((a*b)|^l -1) +(a|^l - 1) -(b|^l - 1);
(a|^l -1) mod p = 0 by A1,A2,A4,Th20; then
A9: p divides (a|^l -1) by INT_1:62; then
A10: p divides (a|^l -1)*(b|^l +1) by INT_2:2;
assume a*b is_quadratic_residue_mod p;
then ((a*b)|^l -1) mod p = 0 by A1,A6,Th20;
then p divides ((a*b)|^l -1) by INT_1:62;
then p divides ((a*b)|^l -1) +(a|^l - 1) by A9,WSIERP_1:4;
then p divides (b|^l - 1) by A10,A8,Th2;
then p divides ((b|^l +1) - (b|^l -1)) by A7,Th1;
hence contradiction by A1,NAT_D:7;
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 that
A1: p>2 and
A2: a gcd p = 1 and
A3: b gcd p = 1 and
A4: not a is_quadratic_residue_mod p and
A5: not b is_quadratic_residue_mod p;
A6: a*b gcd p = 1 by A2,A3,WSIERP_1:6;
set l = (p-'1) div 2;
(b|^l + 1) mod p = 0 by A1,A3,A5,Th21;
then
A7: p divides (b|^l + 1) by INT_1:62;
A8: (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:7
.= ((a*b)|^l +1) +(a|^l + 1) - (1- b|^l);
(a|^l +1) mod p = 0 by A1,A2,A4,Th21; then
A9: p divides (a|^l +1) by INT_1:62; then
A10: p divides (a|^l +1)*(b|^l +1) by INT_2:2;
now
assume not a*b is_quadratic_residue_mod p;
then ((a*b)|^l +1) mod p = 0 by A1,A6,Th21;
then p divides ((a*b)|^l +1) by INT_1:62;
then p divides ((a*b)|^l +1) +(a|^l + 1) by A9,WSIERP_1:4;
then p divides (1- b|^l) by A10,A8,Th2;
then p divides ((b|^l +1) + (1- b|^l)) by A7,WSIERP_1:4;
hence contradiction by A1,NAT_D:7;
end;
hence thesis;
end;
definition
::$N Legendre symbol
let a be Integer, p be Prime;
func Lege (a,p) -> Integer equals :Def3:
1 if (a is_quadratic_residue_mod p & a mod p <> 0),
0 if (a is_quadratic_residue_mod p & a mod p = 0)
otherwise -1;
coherence;
consistency;
end;
theorem Th25:
Lege (a,p) = 1 or Lege (a,p) = 0 or Lege (a,p) = -1
proof
per cases;
suppose a is_quadratic_residue_mod p & a mod p <> 0;
hence thesis by Def3;
end;
suppose a is_quadratic_residue_mod p & a mod p = 0;
hence thesis by Def3;
end;
suppose not a is_quadratic_residue_mod p;
hence thesis by Def3;
end;
end;
theorem Th26:
a mod p <> 0 implies Lege (a^2,p) = 1
proof
assume a mod p <> 0; then
not p divides a by INT_1:62; then
not p divides a^2 by Th7; then
A1: a^2 mod p <> 0 by INT_1:62;
a^2 is_quadratic_residue_mod p by Th9;
hence thesis by Def3,A1;
end;
theorem
Lege (1,p) = 1
proof
1 < p by INT_2:def 4; then
1 mod p <> 0 by NAT_D:14; then
Lege (1^2,p) = 1 by Th26;
hence thesis;
end;
Lm3: a gcd p = 1 implies not p divides a
proof
assume
A1: a gcd p = 1;
assume p divides a; then
p divides (p gcd a) by INT_2:def 2; then
p = 1 by A1,WSIERP_1:15;
hence thesis by INT_2:def 4;
end;
theorem Th28:
p>2 & a gcd p = 1 implies Lege (a,p),a|^((p-'1) div 2) are_congruent_mod p
proof
assume that
A1: p>2 and
A2: a gcd p = 1;
not p divides a by Lm3,A2; then
A3: a mod p <> 0 by INT_1:62;
A4: p>1 by INT_2:def 4;
then -p < -1 by XREAL_1:24; then
A5: (-1) mod p = p+(-1) by NAT_D:63;
per cases;
suppose
A6: a is_quadratic_residue_mod p;
then a|^((p-'1) div 2) mod p = 1 by A1,A2,Th17;
then a|^((p-'1) div 2) mod p = 1 mod p by A4,NAT_D:14;
then a|^((p-'1) div 2) mod p = Lege (a,p) mod p by A6,Def3,A3;
hence thesis by NAT_D:64;
end;
suppose
A7: not a is_quadratic_residue_mod p;
then a|^((p-'1) div 2) mod p = p-1 by A1,A2,Th19
.= Lege (a,p) mod p by A5,A7,Def3;
hence thesis by NAT_D:64;
end;
end;
theorem
p>2 & a gcd p =1 & a,b are_congruent_mod p implies Lege (a,p) = Lege (b,p)
proof
assume that
A1: p>2 and
A2: a gcd p = 1 and
A3: a,b are_congruent_mod p;
Lege (a,p),a|^((p-'1) div 2) are_congruent_mod p by A1,A2,Th28; then
A4: Lege (a,p) mod p = a|^((p-'1) div 2) mod p by NAT_D:64;
b gcd p = 1 by A2,A3,INT_4:14;
then Lege (b,p),b|^((p-'1) div 2) are_congruent_mod p by A1,Th28;
then
A5: Lege (b,p) mod p = b|^((p-'1) div 2) mod p by NAT_D:64;
a mod p = b mod p by A3,NAT_D:64;
then Lege (a,p) mod p = Lege (b,p) mod p by A4,A5,Th13;
then Lege (a,p),Lege (b,p) are_congruent_mod p by NAT_D:64;
then
A6: p divides (Lege (a,p) - Lege (b,p));
per cases by Th25;
suppose
A7: Lege (a,p) = 1;
A8: now assume Lege (b,p) = 0; then
p = 1 by A6,A7,WSIERP_1:15;
hence contradiction by A1;
end;
Lege (b,p) <> -1 by A7,A1,A6,NAT_D:7;
hence thesis by A7,A8,Th25;
end;
suppose
A9: Lege (a,p) = 0;
A10: now assume Lege (b,p) = 1; then
p divides 1 by A6,A9,INT_2:10; then
p = 1 by WSIERP_1:15;
hence contradiction by A1;
end;
now assume Lege (b,p) = -1; then
p = 1 by A6,A9,WSIERP_1:15;
hence contradiction by A1;
end;
hence thesis by A9,Th25,A10;
end;
suppose
A11: Lege (a,p) = -1;
A12: now
assume Lege (b,p) = 1;
then p divides -2 by A6,A11;
then p divides 2 by INT_2:10;
hence contradiction by A1,NAT_D:7;
end;
now assume Lege (b,p) = 0; then
p divides 1 by A6,A11,INT_2:10; then
p = 1 by WSIERP_1:15;
hence contradiction by A1;
end;
hence thesis by A11,Th25,A12;
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 that
A1: p>2 and
A2: a gcd p=1 and
A3: b gcd p=1;
A4: Lege(b,p),b|^((p-'1) div 2) are_congruent_mod p by A1,A3,Th28;
Lege(a,p),a|^((p-'1) div 2) are_congruent_mod p by A1,A2,Th28;
then Lege(a,p)*Lege(b,p),(a|^((p-'1) div 2))*(b|^((p-'1) div 2))
are_congruent_mod p by A4,INT_1:18;
then Lege(a,p)*Lege(b,p),(a*b)|^((p-'1) div 2) are_congruent_mod p by
NEWTON:7;
then
A5: (a*b)|^((p-'1) div 2),Lege(a,p)*Lege(b,p) are_congruent_mod p by INT_1:14;
a*b gcd p = 1 by A2,A3,WSIERP_1:6;
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 A5,INT_1:15;
then
A6: p divides (Lege(a*b,p)-Lege(a,p)*Lege(b,p));
A7: Lege(b,p) = 1 or Lege(b,p) = -1 or Lege(b,p) = 0 by Th25;
A8: Lege(a,p) = 1 or Lege(a,p) = -1 or Lege(a,p) = 0 by Th25;
per cases by Th25;
suppose
A9: Lege(a*b,p) = 1;
now
assume Lege(a,p) = 0 or Lege(b,p) = 0; then
p = 1 by A6,A9,WSIERP_1:15;
hence contradiction by A1;
end;
hence thesis by A8,A7,A1,A6,A9,NAT_D:7;
end;
suppose
A10: Lege(a*b,p) = 0;
A11: now
assume Lege(a,p) * Lege(b,p) = -1; then
p <= 1 by A6,A10,NAT_D:7; then
p < 1+1 by NAT_1:13;
hence contradiction by A1;
end;
now
assume Lege(a,p) * Lege(b,p) = 1; then
p divides 1 by A6,A10,INT_2:10; then
p <= 1 by NAT_D:7; then
p < 1+1 by NAT_1:13;
hence contradiction by A1;
end;
hence thesis by A8,A7,A11,A10;
end;
suppose
A12: Lege(a*b,p) = -1;
A13: now
assume Lege(a,p) = 0 or Lege(b,p) = 0; then
p = 1 or p = -1 by A6,A12,INT_2:13;
hence contradiction by INT_2:def 4;
end;
now
assume Lege(a,p) * Lege(b,p) = 1; then
p divides (-2) by A6,A12; then
p divides 2 by INT_2:10;
hence contradiction by A1,NAT_D:7;
end;
hence thesis by A12,A13,A7,A8;
end;
end;
theorem Th31:
(for d st d in dom fr holds fr.d = 1 or fr.d = 0 or fr.d = -1) implies
Product fr = 1 or Product fr = 0 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 = 0 or $1.d = -1) implies Product $1 = 1 or Product $1 = 0 or
Product $1 = -1;
A1: 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;
set p1 = p^<*i*>;
assume
A2: P[p];
P[p1]
proof
assume
A3: for d st d in dom p1 holds p1.d = 1 or p1.d = 0 or p1.d = -1;
A4: for d st d in dom p holds p.d = 1 or p.d = 0 or p.d = -1
proof
let d;
assume
A5: d in dom p;
then p1.d = 1 or p1.d = 0 or p1.d = -1 by A3,FINSEQ_2:15;
hence thesis by A5,FINSEQ_1:def 7;
end;
A6: len p1 in dom p1 by FINSEQ_5:6;
A7: Product p1 = (Product p)*i by RVSUM_1:96;
len p1 =len p +1 by FINSEQ_2:16;
then
A8: p1.(len p + 1) = 1 or p1.(len p + 1) = 0 or
p1.(len p + 1) = -1 by A3,A6;
per cases by A2,A4,A8,FINSEQ_1:42;
suppose
Product p = 1 & i =1;
hence thesis by A7;
end;
suppose
Product p = 1 & i =0;
hence thesis by A7;
end;
suppose
Product p = 1 & i = -1;
hence thesis by A7;
end;
suppose
Product p = -1 & i = 1;
hence thesis by A7;
end;
suppose
Product p = -1 & i = 0;
hence thesis by A7;
end;
suppose
Product p = -1 & i = -1;
hence thesis by A7;
end;
suppose
Product p = 0 & i = 1;
hence thesis by A7;
end;
suppose
Product p = 0 & i = 0;
hence thesis by A7;
end;
suppose
Product p = 0 & i = -1;
hence thesis by A7;
end;
end;
hence thesis;
end;
A9: P[<*>INT] by RVSUM_1:94;
for p being FinSequence of INT holds P[p] from FINSEQ_2:sch 2(A9,A1 );
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: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
P[n+1]
proof
let f,fr;
assume that
A3: len f = n+1 and
A4: len f = len fr and
A5: for d st d in dom f holds f.d,fr.d are_congruent_mod m;
consider fr1 being FinSequence of INT,b being Element of INT such that
A6: fr = fr1^<*b*> by A3,A4,FINSEQ_2:19;
f <> {} by A3; then
A7: (n+1) in dom f by A3,FINSEQ_5:6;
consider f1 being FinSequence of INT,a being Element of INT such that
A8: f = f1^<*a*> by A3,FINSEQ_2:19;
A9: n+1 = len fr1 +1 by A3,A4,A6,FINSEQ_2:16; then
A10: fr.(n+1) = b by A6,FINSEQ_1:42;
A11: n+1 = len f1 +1 by A3,A8,FINSEQ_2:16; then
A12: dom f1 = dom fr1 by A9,FINSEQ_3:29;
for d st d in dom f1 holds f1.d,fr1.d are_congruent_mod m
proof
let d;
assume
A13: d in dom f1; then
A14: f.d = f1.d by A8,FINSEQ_1:def 7;
fr.d = fr1.d by A6,A12,A13,FINSEQ_1:def 7;
hence thesis by A5,A8,A13,A14,FINSEQ_2:15;
end;
then
A15: Product f1,Product fr1 are_congruent_mod m by A2,A11,A9;
f.(n+1) = a by A8,A11,FINSEQ_1:42;
then a,b are_congruent_mod m by A5,A7,A10;
then (Product f1)*a,(Product fr1)*b are_congruent_mod m by A15,INT_1:18;
then Product f,(Product fr1)*b are_congruent_mod m by A8,RVSUM_1:96;
hence thesis by A6,RVSUM_1:96;
end;
hence thesis;
end;
A16: P[0]
proof
let f,fr;
assume that
A17: len f = 0 and
A18: len f = len fr;
A19: f = <*>INT by A17;
fr = <*>INT by A17,A18;
hence thesis by A19,INT_1:11;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A16,A1);
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: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
P[n+1]
proof
let f,fr;
assume that
A3: len f = n+1 and
A4: len f = len fr and
A5: for d st d in dom f holds f.d,-fr.d are_congruent_mod m;
consider fr1 be FinSequence of INT,b be Element of INT such that
A6: fr = fr1^<*b*> by A3,A4,FINSEQ_2:19;
f <> {} by A3; then
A7: (n+1) in dom f by A3,FINSEQ_5:6;
consider f1 be FinSequence of INT,a be Element of INT such that
A8: f = f1^<*a*> by A3,FINSEQ_2:19;
A9: n+1 = len fr1 +1 by A3,A4,A6,FINSEQ_2:16; then
A10: fr.(n+1) = b by A6,FINSEQ_1:42;
A11: n+1 = len f1 +1 by A3,A8,FINSEQ_2:16;
then
A12: dom f1 = dom fr1 by A9,FINSEQ_3:29;
for d st d in dom f1 holds f1.d,-fr1.d are_congruent_mod m
proof
let d;
assume
A13: d in dom f1;
then
A14: f.d = f1.d by A8,FINSEQ_1:def 7;
fr.d = fr1.d by A6,A12,A13,FINSEQ_1:def 7;
hence thesis by A5,A8,A13,A14,FINSEQ_2:15;
end;
then
A15: Product f1,((-1)|^(len f1))*Product fr1 are_congruent_mod m by A2,A11,A9;
f.(n+1) = a by A8,A11,FINSEQ_1:42;
then a,-b are_congruent_mod m by A5,A7,A10;
then (Product f1)*a,((-1)|^(len f1))*(Product fr1)*(-b)
are_congruent_mod m by A15,INT_1:18; then
Product f,((-1)|^(len f1))*(-1)*((Product fr1)*b) are_congruent_mod
m by A8,RVSUM_1:96;
then Product f,((-1)|^(len f1 + 1))*((Product fr1)*b) are_congruent_mod
m by NEWTON:6;
hence thesis by A3,A6,A11,RVSUM_1:96;
end;
hence thesis;
end;
A16: P[0]
proof
let f,fr;
assume that
A17: len f = 0 and
A18: len f = len fr;
A19: f = <*>INT by A17;
A20: (-1)|^(len f) = 1 by A17,NEWTON:4;
fr = <*>INT by A17,A18;
hence thesis by A19,A20,INT_1:11;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A16,A1);
hence thesis;
end;
reserve fp for FinSequence of NAT;
theorem Th34:
p>2 & (for d st d in dom fp holds fp.d gcd 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;
deffunc F(Nat) = Lege (fp.$1,p);
set k = (p-'1) div 2;
assume
A2: for d st d in dom fp holds fp.d gcd p = 1;
set f = fp|^k;
reconsider f as FinSequence of INT by FINSEQ_2:24,NUMBERS:17;
consider fr being FinSequence such that
A3: len fr = len fp & for d being Nat st d in dom fr holds fr.d = F(d)
from FINSEQ_1:sch 2;
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 A3;
hence thesis by INT_1:def 2;
end;
then reconsider fr as FinSequence of INT by FINSEQ_2:12;
A4: fp is FinSequence of REAL by FINSEQ_2:24,NUMBERS:19;
A5: 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
A6: d in dom fr;
then d in dom fp by A3,FINSEQ_3:29;
then fp.d gcd p = 1 by A2;
then Lege (fp.d,p),(fp.d)|^k are_congruent_mod p by A1,Th28; then
A7: fr.d,(fp.d)|^k are_congruent_mod p by A3,A6;
d in dom f by A3,A5,A6,FINSEQ_3:29;
hence thesis by A7,NAT_3:def 1;
end; then
A8: Product f,Product fr are_congruent_mod p by A3,A5,Th32,INT_1:14;
Product(fp) gcd p = 1 by A2,WSIERP_1:36;
then
Lege (Product fp,p),(Product fp)|^((p-'1) div 2) are_congruent_mod p by A1
,Th28;
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 A8,INT_1:15;
then
A9: p divides (Lege (Product fp,p) - Product fr);
take fr;
A10: for d st d in dom fr holds fr.d = 1 or fr.d = 0 or fr.d = -1
proof
let d;
assume d in dom fr;
then fr.d = Lege (fp.d,p) by A3;
hence thesis by Th25;
end;
per cases by Th25;
suppose
A11: Lege (Product fp,p) = 1;
then A12: Product fr <> -1 by A1,A9,NAT_D:7;
now
assume Product fr = 0;
then p = 1 by A9,A11,WSIERP_1:15;
hence contradiction by A1;
end;
hence thesis by A3,A10,A11,Th31,A12;
end;
suppose
A13: Lege (Product fp,p) = 0;
A14: now
assume Product fr = -1;
then p = 1 by A9,A13,WSIERP_1:15;
hence contradiction by A1;
end;
now
assume Product fr = 1;
then p divides 1 by A9,A13,INT_2:10;
then p = 1 by WSIERP_1:15;
hence contradiction by A1;
end;
hence thesis by A3,A10,A13,Th31,A14;
end;
suppose
A15: Lege (Product fp,p) = -1;
A16: now
assume Product fr = 1;
then p divides -2 by A9,A15;
then p divides 2 by INT_2:10;
hence contradiction by A1,NAT_D:7;
end;
now
assume Product fr = 0;
then p divides 1 by A9,A15,INT_2:10;
then p = 1 by WSIERP_1:15;
hence contradiction by A1;
end;
hence thesis by A3,A10,A15,Th31,A16;
end;
end;
theorem
p > 2 & d gcd p = 1 & e gcd p = 1 implies Lege((d^2)*e,p) = Lege(e,p)
proof
assume that
A1: p > 2 and
A2: d gcd p = 1 and
A3: e gcd p = 1;
reconsider d2=d^2, e as Element of NAT by ORDINAL1:def 12;
set fp = <*d2,e*>;
reconsider fp as FinSequence of NAT by FINSEQ_2:13;
not p divides d by A2,Lm3; then
d mod p <> 0 by INT_1:62; then
A4: Lege(d^2,p) = 1 by Th26;
reconsider p as prime Element of NAT by ORDINAL1:def 12;
for k st k in dom fp holds fp.k gcd p = 1
proof
let k;
assume k in dom fp;
then k in Seg(len fp) by FINSEQ_1:def 3;
then
A5: k in Seg 2 by FINSEQ_1:44;
per cases by A5,FINSEQ_1:2,TARSKI:def 2;
suppose
k = 1;
then fp.k = d^2 by FINSEQ_1:44;
hence thesis by A2,WSIERP_1:7;
end;
suppose
k = 2;
hence thesis by A3,FINSEQ_1:44;
end;
end;
then consider fr be FinSequence of INT such that
A6: len fr = len fp and
A7: for k be Nat st k in dom fr holds fr.k = Lege (fp.k,p) and
A8: Lege (Product fp,p) = Product fr by A1,Th34;
A9: len fr = 2 by A6,FINSEQ_1:44;
then 2 in dom fr by FINSEQ_3:25;
then fr.2 = Lege(fp.2,p) by A7;
then
A10: fr.2 = Lege(e,p) by FINSEQ_1:44;
1 in dom fr by A9,FINSEQ_3:25;
then fr.1 = Lege(fp.1,p) by A7;
then fr.1 = Lege(d^2,p) by FINSEQ_1:44;
then fr = <*1,Lege(e,p)*> by A4,A9,A10,FINSEQ_1:44;
then Product fr = 1 * Lege(e,p) by RVSUM_1:99;
hence thesis by A8,RVSUM_1:99;
end;
theorem Th36:
p>2 implies Lege (-1,p) = (-1)|^((p-'1) div 2)
proof
assume
A1: p>2;
|.(-1)|^((p-'1) div 2).| = 1 by SERIES_2:1;
then
A2: (-1)|^((p-'1) div 2) =1 or -(-1)|^((p-'1) div 2) =1 by ABSVALUE:1;
(-1) gcd p = (-1)|^1 gcd p
.= |.(-1)|^1.| gcd |.p.| by INT_2:34
.= 1 gcd |.p.| by SERIES_2:1
.= 1 by NEWTON:51;
then
A3: Lege (-1,p),(-1)|^((p-'1) div 2) are_congruent_mod p by A1,Th28;
per cases by A2;
suppose
A4: (-1)|^((p-'1) div 2) = 1;
then
A5: p divides (Lege (-1,p) - 1) by A3;
A6: now
assume Lege(-1,p) = -1;
then p divides -2 by A5;
then p divides 2 by INT_2:10;
hence contradiction by A1,NAT_D:7;
end;
now
assume Lege(-1,p) = 0;
then p divides 1 by A5,INT_2:10; then
p <= 1 by NAT_D:7; then
p < 1+1 by NAT_1:13;
hence contradiction by A1;
end;
hence thesis by A4,Th25,A6;
end;
suppose
A7: (-1)|^((p-'1) div 2) = -1;
then A8: p divides (Lege (-1,p) - (-1)) by A3;
then A9: Lege(-1,p) <> 1 by A1,NAT_D:7;
now
assume Lege(-1,p) = 0; then
p <= 1 by A8,NAT_D:7; then
p < 1+1 by NAT_1:13;
hence contradiction by A1;
end;
hence thesis by A7,Th25,A9;
end;
end;
theorem
p>2 & p mod 4 = 1 implies (-1) is_quadratic_residue_mod p
proof
assume that
A1: p>2 and
A2: p mod 4 = 1;
p>1 by INT_2:def 4;
then
A3: p-'1 = p-1 by XREAL_1:233;
p = (p div 4)*4 + 1 by A2,NAT_D:2;
then p-'1 = 2*(2*(p div 4)) by A3;
then (-1)|^((p-'1) div 2) = (-1)|^(2*(p div 4)) by NAT_D:18
.= ((-1)|^2)|^(p div 4) by NEWTON:9
.= (1|^2)|^(p div 4) by WSIERP_1:1
.= 1^2|^(p div 4)
.= 1;
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 that
A1: p>2 and
A2: p mod 4 = 3;
p>1 by INT_2:def 4; then
A3: p-'1 = p-1 by XREAL_1:233;
p = (p div 4)*4 + 3 by A2,NAT_D:2;
then p-'1 = 2*(2*(p div 4) + 1) by A3;
then (-1)|^((p-'1) div 2) = (-1)|^(2*(p div 4) + 1) by NAT_D:18
.= (-1)|^(2*(p div 4)) * (-1) by NEWTON:6
.= ((-1)|^2)|^(p div 4) *(-1) by NEWTON:9
.= (1|^2)|^(p div 4) *(-1) by WSIERP_1:1
.= 1^2|^(p div 4) *(-1)
.= 1 *(-1);
then Lege(-1,p) = -1 by A1,Th36; then
not (-1 is_quadratic_residue_mod p & -1 mod p <> 0) &
not (-1 is_quadratic_residue_mod p & -1 mod p = 0) by Def3;
hence thesis;
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
set ff = Swap(f,i,j);
A1: rng ff = rng f by FINSEQ_7:22;
assume f is one-to-one;
then
A2: card(rng f) = len f by FINSEQ_4:62;
len ff = len f by FINSEQ_7:18;
hence thesis by A2,A1,FINSEQ_4:62;
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:62;
then card(rng f) = len Swap(f,i,j) by FINSEQ_7:22;
then card(rng f) = len f by FINSEQ_7:18;
hence thesis by FINSEQ_4:62;
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: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
P[n+1]
proof
let f be FinSequence of NAT;
assume that
A3: len f = n+1 and
A4: for d st d in dom f holds f.d>0 & f.d<=n+1 and
A5: f is one-to-one;
A6: f <> {} by A3;
then
A7: n+1 in dom f by A3,FINSEQ_5:6;
then
A8: f.(n+1) > 0 by A4;
consider f1 being FinSequence of NAT,a being Element of NAT such that
A9: f = f1^<*a*> by A6,HILBERT2:4;
A10: f1 is one-to-one by A5,A9,FINSEQ_3:91;
A11: len f = len f1 + 1 by A9,FINSEQ_2:16;
f.(n+1) <= n+1 by A4,A7;
then
A12: a<=n+1 by A3,A9,A11,FINSEQ_1:42;
per cases by A3,A9,A11,A8,A12,FINSEQ_1:42,XXREAL_0:1;
suppose
A13: a = n+1;
for d st d in dom f1 holds f1.d>0 & f1.d<=n
proof
let d;
assume
A14: d in dom f1;
then
A15: d in dom f by A9,FINSEQ_2:15;
A16: now
d <= n by A3,A11,A14,FINSEQ_3:25;
then d < n+1 by XREAL_1:145;
then f.d <> f.(n+1) by A5,A7,A15;
then
A17: f1.d <> f.(n+1) by A9,A14,FINSEQ_1:def 7;
assume f1.d = n+1;
hence contradiction by A3,A9,A11,A13,A17,FINSEQ_1:42;
end;
f.d<=n+1 by A4,A15;
then f1.d<=n+1 by A9,A14,FINSEQ_1:def 7;
then
A18: f1.d < n+1 by A16,XXREAL_0:1;
f.d>0 by A4,A15;
hence thesis by A9,A14,A18,FINSEQ_1:def 7,NAT_1:13;
end;
then rng f1 = Seg n by A2,A3,A11,A10;
then rng f1 \/ {a} = Seg (n+1) by A13,FINSEQ_1:9;
then rng f1 \/ rng <*a*> = Seg (n+1) by FINSEQ_1:38;
hence thesis by A9,FINSEQ_1:31;
end;
suppose
A19: a > 0 & a < n+1;
ex d st d in dom f1 & f1.d = n+1
proof
assume
A20: 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
A21: d in dom f;
then
A22: d in Seg(n+1) by A3,FINSEQ_1:def 3;
then
A23: d<=n+1 by FINSEQ_1:1;
per cases by A22,A23,FINSEQ_1:1,XXREAL_0:1;
suppose
d=n+1;
then
A24: f.d = a by A3,A9,A11,FINSEQ_1:42;
then
A25: f.d<=n by A19,NAT_1:13;
f.d>=0+1 by A19,A24,NAT_1:13;
hence thesis by A25,FINSEQ_1:1;
end;
suppose
A26: d>=1 & d

p/2;
consider d being Nat such that
A39: d in U and
A40: f.d = y by A38,FINSEQ_2:10;
reconsider d as Element of U by A39;
take d;
thus x=F(d) by A37,A40;
end;
A41: Y c= YY
proof
let x be object;
assume x in Y;
then
A42: ex d be Element of NAT st d = x & d in dom f & f.d > p/ 2;
then reconsider x as Element of U;
reconsider f as FinSequence of NAT qua set;
f.x in rng f by FUNCT_1:3;
then F(x) in X by A42;
hence thesis;
end;
now
let x be object;
assume x in YY;
then consider d be Element of U such that
A43: d = x and
A44: f.d in X;
ex k be Element of NAT st k = f.d & k in rng f & k > p/ 2 by A44;
hence x in Y by A43;
end;
then
A45: YY c= Y;
A46: for d1,d2 being Element of U st F(d1) = F(d2) holds d1 = d2
proof
let d1,d2 be Element of U;
assume
A47: F(d1)=F(d2);
f is one-to-one by A29,A33,A34,FINSEQ_3:92,XBOOLE_1:73;
hence thesis by A47;
end;
X,YY are_equipotent from FUNCT_7:sch 3(A36,A46);
hence thesis by A41,A45,XBOOLE_0:def 10;
end;
p div 2 < p by INT_1:56;
then (p div 2) div 2 <= p div 2 by NAT_2:24;
then
A48: p div (2*2) <= p div 2 by NAT_2:27;
A49: Z c= Y
proof
let x be object;
assume
A50: x in Z;
then reconsider x as Element of NAT;
A51: x>=(p div 4)+1 by A50,CALCUL_2:1;
then (p div 4)+x >= (p div 4)+1 by NAT_1:12;
then
A52: x >= 1 by XREAL_1:6;
x<=((p-'1) div 2)-'(p div 4)+(p div 4) by A50,CALCUL_2:1;
then x<=((p-'1) div 2) by A17,A48,XREAL_1:235;
then
A53: x in dom f by A6,A11,A52,FINSEQ_3:25;
x > p/4 by A51,INT_1:29,XXREAL_0:2;
then 2*x > 2*(p/4) by XREAL_1:68;
then f.x > p/2 by A20,A53;
hence thesis by A53;
end;
now
let x be object;
A54: p/4 >= [\p/4/] by INT_1:def 6;
assume x in Y;
then consider x1 be Element of NAT such that
A55: x1=x and
A56: x1 in dom f and
A57: f.x1 >p/2;
2*x1>p/2 by A20,A56,A57;
then x1 > (p/2)/2 by XREAL_1:83;
then x1 > [\p/4/] by A54,XXREAL_0:2;
then
A58: x1 >= (p div 4) + 1 by NAT_1:13;
x1 <= p9 by A6,A11,A56,FINSEQ_3:25;
then x1 <= (p9-'(p div 4) + (p div 4)) by A17,A48,XREAL_1:235;
hence x in Z by A55,A58;
end;
then Y c= Z;
then Y = Z by A49,XBOOLE_0:def 10;
then
A59: m = ((p-'1) div 2)-'(p div 4) by A30,A35,CARD_1:5;
A60: now
assume p mod 8 = 2;
then 8 divides (p - 2) by PEPIN:8;
then 2 divides (p - 2) by A8,INT_2:9;
then 2 divides -(p-2) by INT_2:10;
then 2 divides (2 - p);
then 2 divides p by Th2;
hence contradiction by A13,NAT_4:12;
end;
A61: now
assume p mod 8 = 4;
then 8 divides (p - 4) by PEPIN:8;
then 2 divides (p - 4) by A8,INT_2:9;
then 2 divides -(p - 4) by INT_2:10;
then
A62: 2 divides (4 - p);
4 = 2*2;
then 2 divides 4;
then 2 divides p by A62,Th2;
hence contradiction by A13,NAT_4:12;
end;
A63: now
assume p mod 8 = 6;
then 8 divides (p - 6) by PEPIN:8;
then 2 divides (p - 6) by A8,INT_2:9;
then 2 divides -(p - 6) by INT_2:10;
then
A64: 2 divides (6-p);
6=2*3;
then 2 divides 6;
then 2 divides p by A64,Th2;
hence contradiction by A13,NAT_4:12;
end;
p mod 8 = 0 or ... or p mod 8 = 7 by A7;
then per cases by A9,A60,A61,A63;
suppose
p mod 8 = 1;
then
A65: p=8*nn+1 by NAT_D:2;
then p-'1 = 2*(4*nn) by A2;
then
A66: (p-'1) div 2 = 4*nn by NAT_D:18;
p div 4 = (4*(2*nn)+1) div 4 by A65
.= 2*nn+(1 div 4) by NAT_D:61
.= 2*nn+0 by NAT_D:27;
then m = 4*nn - 2*nn by A59,A66,XREAL_1:64,233
.= 2*nn;
then
A67: Lege(2,p) =((-1)|^2)|^nn by A15,NEWTON:9
.= (1|^2)|^nn by WSIERP_1:1
.= 1^2|^nn
.= 1;
(p^2 -'1) div 8 = (((8*nn)^2 + 2*(8*nn)) + 1-'1) div 8 by A65
.= 8*(8*nn^2 + 2*nn) div 8 by NAT_D:34
.= 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:9
.= (1|^2)|^(4*nn^2 + nn) by WSIERP_1:1
.= 1|^(4*nn^2 + nn)
.= Lege(2,p) by A67;
end;
suppose
p mod 8 = 3;
then
A68: p=8*nn+3 by NAT_D:2;
then p-'1 = 2*(4*nn+1) by A2;
then
A69: (p-'1) div 2 = 4*nn+1 by NAT_D:18;
A70: 4*nn>=2*nn by XREAL_1:64;
p div 4 = (4*(2*nn)+3) div 4 by A68
.= 2*nn+(3 div 4) by NAT_D:61
.= 2*nn+0 by NAT_D:27;
then m = 4*nn+1-2*nn by A59,A69,A70,NAT_1:12,XREAL_1:233
.= 2*nn+1;
then
A71: Lege(2,p) = (-1)|^(2*nn)*(-1) by A15,NEWTON:6
.= ((-1)|^2)|^nn*(-1) by NEWTON:9
.= (1|^2)|^nn*(-1) by WSIERP_1:1
.= 1|^nn*(-1)
.= 1*(-1)
.= -1;
(p^2 -'1) div 8 = (8*(8*nn^2)+8*(6*nn)+3*3-1) div 8 by A68,NAT_1:12
,XREAL_1:233
.= 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:6
.= ((-1)|^2)|^(4*nn^2+3*nn)*(-1) by NEWTON:9
.= (1|^2)|^(4*nn^2+3*nn)*(-1) by WSIERP_1:1
.= 1|^(4*nn^2+3*nn)*(-1)
.= 1*(-1)
.= Lege(2,p) by A71;
end;
suppose
p mod 8 = 5;
then
A72: p=8*nn+5 by NAT_D:2;
then p-'1 = 2*(4*nn+2) by A2;
then
A73: (p-'1) div 2 = 4*nn+2 by NAT_D:18;
A74: 4*nn>=2*nn by XREAL_1:64;
p div 4 = (4*(2*nn+1)+1) div 4 by A72
.= 2*nn+1+(1 div 4) by NAT_D:61
.= 2*nn+1+0 by NAT_D:27;
then m = 4*nn+2-(2*nn+1) by A59,A73,A74,XREAL_1:7,233
.= 2*nn+1;
then
A75: Lege(2,p) = (-1)|^(2*nn)*(-1) by A15,NEWTON:6
.= ((-1)|^2)|^nn*(-1) by NEWTON:9
.= (1|^2)|^nn*(-1) by WSIERP_1:1
.= 1|^nn*(-1)
.= 1*(-1)
.= -1;
(p^2 -'1) div 8=(8*(8*nn^2)+8*(10*nn)+25-1) div 8 by A72,NAT_1:12
,XREAL_1:233
.= 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:6
.= ((-1)|^2)|^(4*nn^2+5*nn+1)*(-1) by NEWTON:9
.= (1|^2)|^(4*nn^2+5*nn+1)*(-1) by WSIERP_1:1
.= 1|^(4*nn^2+5*nn+1)*(-1)
.= 1*(-1)
.= Lege(2,p) by A75;
end;
suppose
p mod 8 = 7;
then
A76: p=8*nn+7 by NAT_D:2;
then p-'1 = 2*(4*nn+3) by A2;
then
A77: (p-'1) div 2 = 4*nn+3 by NAT_D:18;
A78: 4*nn>=2*nn by XREAL_1:64;
p div 4 = (4*(2*nn+1)+3) div 4 by A76
.= 2*nn+1+(3 div 4) by NAT_D:61
.= 2*nn+1+0 by NAT_D:27;
then m = 4*nn+3-(2*nn+1) by A59,A77,A78,XREAL_1:7,233
.= 2*nn+2;
then
A79: Lege(2,p) = (-1)|^(2*(nn+1)) by A13,A14,Th41
.= ((-1)|^2)|^(nn+1) by NEWTON:9
.= (1|^2)|^(nn+1) by WSIERP_1:1
.= 1|^(nn+1)
.= 1;
(p^2 -'1) div 8=(8*(8*nn^2)+8*(14*nn)+49-1) div 8 by A76,NAT_1:12
,XREAL_1:233
.= 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:9
.= (1|^2)|^(4*nn^2+7*nn+3) by WSIERP_1:1
.= 1|^(4*nn^2+7*nn+3)
.= Lege(2,p) by A79;
end;
end;
theorem
p>2 & (p mod 8 = 1 or p mod 8 = 7) implies 2 is_quadratic_residue_mod p
proof
assume that
A1: p>2 and
A2: p mod 8 = 1 or p mod 8 = 7;
set nn = p div 8;
per cases by A2;
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 NAT_D:34
.= 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:9
.= (1|^2)|^(4*nn^2 + nn) by WSIERP_1:1
.= 1|^(4*nn^2 + nn)
.= 1;
hence thesis by Def3;
end;
suppose
p mod 8 = 7;
then p = 8*nn+7 by NAT_D:2;
then (p^2 -'1) div 8=(8*(8*nn^2)+8*(14*nn)+49-1) div 8 by NAT_1:12
,XREAL_1:233
.= 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:9
.= (1|^2)|^(4*nn^2+7*nn+3) by WSIERP_1:1
.= 1|^(4*nn^2+7*nn+3)
.= 1;
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 that
A1: p>2 and
A2: p mod 8 = 3 or p mod 8 = 5;
set nn = p div 8;
per cases by A2;
suppose
p mod 8 = 3;
then p = 8*nn+3 by NAT_D:2;
then (p^2 -'1) div 8 = (8*(8*nn^2)+8*(6*nn)+3*3-1) div 8 by NAT_1:12
,XREAL_1:233
.= 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:6
.= ((-1)|^2)|^(4*nn^2+3*nn)*(-1) by NEWTON:9
.= (1|^2)|^(4*nn^2+3*nn)*(-1) by WSIERP_1:1
.= 1|^(4*nn^2+3*nn)*(-1)
.= 1*(-1)
.= -1; then
not (2 is_quadratic_residue_mod p & 2 mod p <> 0) &
not (2 is_quadratic_residue_mod p & 2 mod p = 0) by Def3;
hence thesis;
end;
suppose
p mod 8 = 5;
then p = 8*nn+5 by NAT_D:2;
then (p^2 -'1) div 8=(8*(8*nn^2)+8*(10*nn)+25-1) div 8 by NAT_1:12
,XREAL_1:233
.= 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:6
.= ((-1)|^2)|^(4*nn^2+5*nn+1)*(-1) by NEWTON:9
.= (1|^2)|^(4*nn^2+5*nn+1)*(-1) by WSIERP_1:1
.= 1|^(4*nn^2+5*nn+1)*(-1)
.= 1*(-1)
.= -1; then
not (2 is_quadratic_residue_mod p & 2 mod p <> 0) &
not (2 is_quadratic_residue_mod p & 2 mod p = 0) by Def3;
hence thesis;
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 NAT_D:64;
then
A1: 2 divides (a-b);
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:8
.= (-1)|^b * ((-1)|^2)|^n by NEWTON:9
.= (-1)|^b * (1|^2)|^n by WSIERP_1:1
.= (-1)|^b * 1|^n
.= (-1)|^b * 1;
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: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
P[n+1]
proof
let f be FinSequence of REAL,m be Real;
A3: len<*m*> = 1 by FINSEQ_1:39;
assume
A4: len f = n+1;
then f <> {};
then consider f1 be FinSequence of REAL,x be Element of REAL such that
A5: f = f1^<*x*> by HILBERT2:4;
reconsider mm=m as Element of REAL by XREAL_0:def 1;
A6: n + 1 = len f1 + 1 by A4,A5,FINSEQ_2:16;
then
A7: len(n|-> m)=len f1 by CARD_1:def 7;
A8: len<*x*> = 1 by FINSEQ_1:39;
((n+1)|-> m)-f = (n|-> m)^<*m*> - f1^<*x*> by A5,FINSEQ_2:60
.= ((n|-> mm)-f1) ^ (<*mm*>-<*x*>) by A7,A8,A3,Th46
.= ((n|-> m)-f1) ^ <*m-x*> by RVSUM_1:29;
hence Sum(((n+1)|-> m)-f) = Sum((n|-> m)-f1) + (m-x) by RVSUM_1:74
.= n*m - Sum f1 + (m - x) by A2,A6
.= (n+1)*m - (Sum f1 + x)
.= (n+1)*m - Sum f by A5,RVSUM_1:74;
end;
hence thesis;
end;
A9: P[0]
proof
let f be FinSequence of REAL,m be Real;
assume len f = 0;
then Sum f = 0 by PROB_3:62;
hence thesis by RVSUM_1:28,72;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A9,A1);
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 object;
assume y in rng Card F;
then consider x being object such that
A1: x in dom Card F and
A2: y = (Card F).x by FUNCT_1:def 3;
A3: x in dom F by A1,CARD_3:def 2;
then F.x in rng F by FUNCT_1:3;
then reconsider Fx = F.x as finite set;
y = card Fx by A2,A3,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: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
P[n+1]
proof
let f be FinSequence of bool X;
assume that
A3: len f = n+1 and
A4: for d,e st d in dom f & e in dom f & d<>e holds f.d misses f.e;
A5: f <> {} by A3;
then consider
f1 be FinSequence of bool X,Y be Element of bool X such that
A6: f = f1^<*Y*> by HILBERT2:4;
reconsider F1 = union(rng f1) as finite set;
A7: union(rng f) = union((rng f1) \/ (rng <*Y*>)) by A6,FINSEQ_1:31
.= union((rng f1) \/ {Y}) by FINSEQ_1:38
.= F1 \/ union {Y} by ZFMISC_1:78
.= F1 \/ Y by ZFMISC_1:25;
A8: n+1 = len f1 +1 by A3,A6,FINSEQ_2:16;
F1 misses Y
proof
A9: n+1 in dom f by A3,A5,FINSEQ_5:6;
assume F1 meets Y;
then consider x be object such that
A10: x in F1 /\ Y by XBOOLE_0:4;
x in F1 by A10,XBOOLE_0:def 4;
then consider Z be set such that
A11: x in Z and
A12: Z in rng f1 by TARSKI:def 4;
consider k be Nat such that
A13: k in dom f1 and
A14: f1.k = Z by A12,FINSEQ_2:10;
k <= n by A8,A13,FINSEQ_3:25;
then
A15: k < n + 1 by NAT_1:13;
k in dom f by A6,A13,FINSEQ_2:15;
then f.(n+1) misses f.k by A4,A15,A9;
then Y misses f.k by A6,A8,FINSEQ_1:42;
then
A16: Y misses Z by A6,A13,A14,FINSEQ_1:def 7;
x in Y \/ Z by A11,XBOOLE_0:def 3;
then not x in Y by A11,A16,XBOOLE_0:5;
hence contradiction by A10,XBOOLE_0:def 4;
end;
then
A17: card F1 + card Y = card(F1\/Y) by CARD_2:40;
reconsider gg = <*card Y*> as FinSequence of NAT;
A18: Card f = Card f1 ^ Card<*Y*> by A6,PRE_POLY:25
.= Card f1 ^ gg by PRE_POLY:24;
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 that
A19: d in dom f1 and
A20: e in dom f1 and
A21: d<>e;
A22: f.e = f1.e by A6,A20,FINSEQ_1:def 7;
A23: e in dom f by A6,A20,FINSEQ_2:15;
A24: d in dom f by A6,A19,FINSEQ_2:15;
f.d = f1.d by A6,A19,FINSEQ_1:def 7;
hence thesis by A4,A21,A22,A24,A23;
end;
then card union rng f1 = Sum Card f1 by A2,A8;
hence thesis by A17,A18,A7,RVSUM_1:74;
end;
hence thesis;
end;
A25: P[0]
proof
let f be FinSequence of bool X;
assume that
A26: len f = 0 and
for d,e st d in dom f & e in dom f & d<>e holds f.d misses f.e;
A27: Card {} = {};
f = {} by A26;
hence thesis by A27,CARD_1:27,RVSUM_1:72,ZFMISC_1:2;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A25,A1);
hence thesis;
end;
Lm4: Sum(fp) is Element of NAT;
reserve q for Prime;
::$N The law of quadratic reciprocity
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 that
A1: p>2 and
A2: q>2 and
A3: p<>q;
A4: q,p are_coprime by A3,INT_2:30;
then
A5: q gcd p = 1 by INT_2:def 3;
reconsider p,q as prime Element of NAT by ORDINAL1:def 12;
set p9 = (p-'1) div 2;
A6: p>1 by INT_2:def 4;
then
A7: p-'1 = p-1 by XREAL_1:233;
then
A8: p-'1>0 by A6,XREAL_1:50;
p is odd by A1,PEPIN:17;
then
A9: p-'1 is even by A7,HILBERT3:2;
then
A10: 2 divides (p-'1) by PEPIN:22;
then
A11: p-'1 = 2*p9 by NAT_D:3;
then p9 divides (p-'1);
then p9 <= (p-'1) by A8,NAT_D:7;
then
A12: p9 < p by A7,XREAL_1:146,XXREAL_0:2;
set f1 = q*idseq p9;
A13: for d st d in dom f1 holds f1.d = q*d
proof
let d;
assume
A14: d in dom f1;
then d in dom idseq p9 by VALUED_1:def 5;
then d in Seg len idseq p9 by FINSEQ_1:def 3;
then
A15: d is Element of Seg p9 by CARD_1:def 7;
f1.d = q * (idseq p9).d by A14,VALUED_1:def 5;
hence thesis by A15;
end;
A16: for d being Nat st d in dom f1 holds f1.d in NAT;
dom f1 = dom idseq p9 by VALUED_1:def 5;
then
A17: len f1 = len idseq p9 by FINSEQ_3:29;
then
A18: len f1 = p9 by CARD_1:def 7;
set q9 = (q-'1) div 2;
set g1 = p*idseq q9;
A19: for d st d in dom g1 holds g1.d = p*d
proof
let d;
assume
A20: d in dom g1;
then d in dom idseq q9 by VALUED_1:def 5;
then d in Seg len idseq q9 by FINSEQ_1:def 3;
then
A21: d is Element of Seg q9 by CARD_1:def 7;
g1.d = p * (idseq q9).d by A20,VALUED_1:def 5;
hence thesis by A21;
end;
A22: for d being Nat st d in dom g1 holds g1.d in NAT;
dom g1 = dom idseq q9 by VALUED_1:def 5;
then len g1 = len idseq q9 by FINSEQ_3:29;
then
A23: len g1 = q9 by CARD_1:def 7;
reconsider g1 as FinSequence of NAT by A22,FINSEQ_2:12;
set g3 = g1 mod q;
set g4 = Sgm rng g3;
A24: len g3 = len g1 by EULER_2:def 1;
then
A25: dom g1 = dom g3 by FINSEQ_3:29;
set XX = {k where k is Element of NAT:k in rng g4 & k>q/2};
for x being object st x in XX holds x in rng g4
proof
let x be object;
assume x in XX;
then ex k being Element of NAT st x = k & k in rng g4 & k > q/2;
hence thesis;
end;
then
A26: XX c= rng g4;
reconsider f1 as FinSequence of NAT by A16,FINSEQ_2:12;
deffunc F(Nat) = f1.$1 div p;
consider f2 be FinSequence such that
A27: len f2 = p9 & for d being Nat st d in dom f2 holds f2.d = F(d) from
FINSEQ_1:sch 2;
A28: q>1 by INT_2:def 4;
then
A29: q-'1 = q-1 by XREAL_1:233;
then
A30: q-'1 >0 by A28,XREAL_1:50;
q >= 2+1 by A2,NAT_1:13;
then q-1 >= 3-1 by XREAL_1:9;
then
A31: q9 >= 1 by A29,NAT_2:13;
then len g3 >=1 by A23,EULER_2:def 1;
then g3 <> {};
then rng g3 is finite non empty Subset of NAT;
then consider n2 be Element of NAT such that
A32: rng g3 c= Seg n2 \/ {0} by HEYTING3:1;
deffunc F(Nat) = g1.$1 div q;
consider g2 be FinSequence such that
A33: len g2 = q9 & for d being Nat st d in dom g2 holds g2.d = F(d)
from FINSEQ_1:sch 2;
for d being Nat st d in dom g2 holds g2.d in NAT
proof
let d be Nat;
assume d in dom g2;
then g2.d = g1.d div q by A33;
hence thesis;
end;
then reconsider g2 as FinSequence of NAT by FINSEQ_2:12;
A34: dom g1 = dom g2 by A23,A33,FINSEQ_3:29;
A35: for d st d in dom g1 holds g1.d = g2.d * q + g3.d
proof
let d;
assume
A36: d in dom g1;
then
A37: g3.d = g1.d mod q by EULER_2:def 1;
g2.d = g1.d div q by A33,A34,A36;
hence thesis by A37,NAT_D:2;
end;
q is odd by A2,PEPIN:17;
then
A38: q-'1 is even by A29,HILBERT3:2;
then
A39: 2 divides (q-'1) by PEPIN:22;
then
A40: q-'1 = 2*q9 by NAT_D:3;
then q9 divides (q-'1);
then q9 <= (q-'1) by A30,NAT_D:7;
then
A41: q9 < q by A29,XREAL_1:146,XXREAL_0:2;
not 0 in rng g3
proof
assume 0 in rng g3;
then consider a be Nat such that
A42: a in dom g3 and
A43: g3.a = 0 by FINSEQ_2:10;
a in dom g1 by A24,A42,FINSEQ_3:29;
then
A44: g1.a = g2.a * q + 0 by A35,A43;
a in dom g1 by A24,A42,FINSEQ_3:29;
then p*a = g2.a * q by A19,A44;
then
A45: q divides p*a;
a >= 1 by A42,FINSEQ_3:25;
then
A46: q <= a by A4,A45,NAT_D:7,PEPIN:3;
a <= q9 by A23,A24,A42,FINSEQ_3:25;
hence contradiction by A41,A46,XXREAL_0:2;
end;
then
A47: {0} misses rng g3 by ZFMISC_1:50;
then
A48: g4 is one-to-one by A32,FINSEQ_3:92,XBOOLE_1:73;
A49: for d,e st d in dom g1 & e in dom g1 & q divides (g1.d-g1.e) holds d=e
proof
A50: q,(p qua Integer) are_coprime by A3,INT_2:30;
let d,e;
assume that
A51: d in dom g1 and
A52: e in dom g1 and
A53: q divides (g1.d-g1.e);
A54: g1.e = p*e by A19,A52;
g1.d = p*d by A19,A51;
then
A55: q divides (d-e)*p by A53,A54;
now
assume d <> e;
then d-e <> 0;
then |.q.| <= |.d-e.| by A55,A50,INT_2:25,INT_4:6;
then
A56: q <= |.d-e.| by ABSVALUE:def 1;
A57: e>=1 by A52,FINSEQ_3:25;
A58: d>=1 by A51,FINSEQ_3:25;
e<=q9 by A23,A52,FINSEQ_3:25;
then
A59: d-e>=1-q9 by A58,XREAL_1:13;
A60: q9-1 -q by A60,XREAL_1:24;
then d-e > -q by A59,XXREAL_0:2;
hence contradiction by A56,A61,SEQ_2:1;
end;
hence thesis;
end;
for x,y be object st x in dom g3 & y in dom g3 & g3.x=g3.y holds x=y
proof
let x,y be object;
assume that
A62: x in dom g3 and
A63: y in dom g3 and
A64: g3.x=g3.y;
reconsider x,y as Element of NAT by A62,A63;
A65: g1.y = g2.y * q + g3.y by A25,A35,A63;
g1.x = g2.x * q + g3.x by A25,A35,A62;
then g1.x - g1.y = (g2.x - g2.y) * q by A64,A65;
then q divides (g1.x - g1.y);
hence thesis by A49,A25,A62,A63;
end;
then
A66: g3 is one-to-one;
then len g3 = card rng g3 by FINSEQ_4:62;
then
A67: len g4 = q9 by A23,A24,A32,A47,FINSEQ_3:39,XBOOLE_1:73;
reconsider XX as finite Subset of NAT by A26,XBOOLE_1:1;
set mm = card XX;
reconsider YY = rng g4 \ XX as finite Subset of NAT;
A68: g3 is Element of NAT* by FINSEQ_1:def 11;
len g3 = q9 by A23,EULER_2:def 1;
then g3 in q9-tuples_on NAT by A68;
then
A69: g3 is Element of q9-tuples_on REAL by FINSEQ_2:109,NUMBERS:19;
for d being Nat st d in dom idseq q9 holds (idseq q9).d in NAT;
then idseq q9 is FinSequence of NAT by FINSEQ_2:12;
then reconsider N = Sum idseq q9 as Element of NAT by Lm4;
A70: 2,q are_coprime by A2,EULER_1:2;
dom(q*g2) = dom g2 by VALUED_1:def 5;
then
A71: len(q*g2) = q9 by A33,FINSEQ_3:29;
q*g2 is Element of NAT* by FINSEQ_1:def 11;
then q*g2 in q9-tuples_on NAT by A71;
then
A72: q*g2 is Element of q9-tuples_on REAL by FINSEQ_2:109,NUMBERS:19;
A73: dom (q*g2+g3) = dom (q*g2) /\ dom g3 by VALUED_1:def 1
.= dom g2 /\ dom g3 by VALUED_1:def 5
.= dom g1 by A25,A34;
for d being Nat st d in dom g1 holds g1.d = (q*g2+g3).d
proof
let d be Nat;
assume
A74: d in dom g1;
then
A75: d in dom (q*g2) by A34,VALUED_1:def 5;
(q*g2+g3).d = (q*g2).d + g3.d by A73,A74,VALUED_1:def 1;
hence (q*g2+g3).d = q * g2.d + g3.d by A75,VALUED_1:def 5
.= g1.d by A35,A74;
end;
then g1 = q*g2 + g3 by A73;
then
A76: Sum g1 = Sum(q*g2) + Sum g3 by A72,A69,RVSUM_1:89
.= q*(Sum g2) + Sum g3 by RVSUM_1:87;
A77: rng g3 c= Seg n2 by A32,A47,XBOOLE_1:73;
then
A78: rng g4 = rng g3 by FINSEQ_1:def 13;
then
A79: XX c= Seg n2 by A77,A26;
A80: len g3 = card rng g4 by A66,A78,FINSEQ_4:62;
mm <= card rng g4 by A26,NAT_1:43;
then mm <= q9 by A23,A80,EULER_2:def 1;
then reconsider nn = q9 - mm as Element of NAT by NAT_1:21;
A81: g4 = (g4|nn)^(g4/^nn) by RFINSEQ:8;
then
A82: g4/^nn is one-to-one by A48,FINSEQ_3:91;
A83: q9 = ((q-'1)+1) div 2 by A38,NAT_2:26
.= q div 2 by A28,XREAL_1:235;
A84: g3 is FinSequence of REAL by FINSEQ_2:24,NUMBERS:19;
g4 is FinSequence of REAL by FINSEQ_2:24,NUMBERS:19;
then
A85: Sum g4 = Sum g3 by A66,A78,A48,RFINSEQ:9,26,A84;
A86: rng g4 \ XX c= rng g4 by XBOOLE_1:36;
then
A87: YY c= Seg n2 by A77,A78;
for k,l being Nat st k in YY & l in XX holds k < l
proof
let k,l be Nat;
assume that
A88: k in YY and
A89: l in XX;
A90: not k in XX by A88,XBOOLE_0:def 5;
A91: ex l1 being Element of NAT st l1 = l & l1 in rng g4 & l1>q/2 by A89;
k in rng g4 by A88,XBOOLE_0:def 5;
then k <= q/2 by A90;
hence thesis by A91,XXREAL_0:2;
end;
then Sgm (YY\/XX) = (Sgm YY)^(Sgm XX) by A87,A79,FINSEQ_3:42;
then Sgm (rng g4 \/ XX) = (Sgm YY)^(Sgm XX) by XBOOLE_1:39;
then
A92: g4 = (Sgm YY)^(Sgm XX) by A78,A26,XBOOLE_1:12;
then Sum g4 = Sum(Sgm YY) + Sum(Sgm XX) by RVSUM_1:75;
then
A93: p*(Sum idseq q9)=q*(Sum g2)+Sum(Sgm YY)+Sum(Sgm XX) by A76,A85,RVSUM_1:87;
A94: len Sgm YY = card YY by A77,A78,A86,FINSEQ_3:39,XBOOLE_1:1
.= q9 - mm by A23,A24,A26,A80,CARD_2:44;
then
A95: g4/^nn = Sgm XX by A92,FINSEQ_5:37;
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 A27;
hence thesis;
end;
then reconsider f2 as FinSequence of NAT by FINSEQ_2:12;
set f3 = f1 mod p;
A96: len f3 = len f1 by EULER_2:def 1;
then
A97: dom f1 = dom f3 by FINSEQ_3:29;
set f4 = Sgm rng f3;
p >= 2+1 by A1,NAT_1:13;
then
A98: p-1 >= 3-1 by XREAL_1:9;
then f3 <> {} by A18,A7,A96,NAT_2:13;
then rng f3 is finite non empty Subset of NAT;
then consider n1 be Element of NAT such that
A99: rng f3 c= Seg n1 \/ {0} by HEYTING3:1;
A100: dom f1 = dom f2 by A18,A27,FINSEQ_3:29;
A101: for d st d in dom f1 holds f1.d = f2.d * p + f3.d
proof
let d;
assume
A102: d in dom f1;
then
A103: f3.d = f1.d mod p by EULER_2:def 1;
f2.d = f1.d div p by A27,A100,A102;
hence thesis by A103,NAT_D:2;
end;
not 0 in rng f3
proof
assume 0 in rng f3;
then consider a be Nat such that
A104: a in dom f3 and
A105: f3.a = 0 by FINSEQ_2:10;
f1.a = f2.a * p + 0 by A97,A101,A104,A105;
then q*a = f2.a *p by A13,A97,A104;
then
A106: p divides q*a;
a >= 1 by A104,FINSEQ_3:25;
then
A107: p <= a by A4,A106,NAT_D:7,PEPIN:3;
a <= p9 by A18,A96,A104,FINSEQ_3:25;
hence contradiction by A12,A107,XXREAL_0:2;
end;
then
A108: {0} misses rng f3 by ZFMISC_1:50;
then
A109: f4 is one-to-one by A99,FINSEQ_3:92,XBOOLE_1:73;
A110: for d,e st d in dom f1 & e in dom f1 & p divides (f1.d-f1.e) holds d=e
proof
A111: q,(p qua Integer) are_coprime by A3,INT_2:30;
let d,e;
assume that
A112: d in dom f1 and
A113: e in dom f1 and
A114: p divides (f1.d-f1.e);
A115: f1.e = q*e by A13,A113;
f1.d = q*d by A13,A112;
then
A116: p divides (d-e)*q by A114,A115;
now
assume d <> e;
then d-e <> 0;
then |.p.| <= |.d-e.| by A116,A111,INT_2:25,INT_4:6;
then
A117: p <= |.d-e.| by ABSVALUE:def 1;
A118: e>=1 by A113,FINSEQ_3:25;
A119: d>=1 by A112,FINSEQ_3:25;
e<=p9 by A18,A113,FINSEQ_3:25;
then
A120: d-e>=1-p9 by A119,XREAL_1:13;
A121: p9-1**

-p by A121,XREAL_1:24;
then d-e > -p by A120,XXREAL_0:2;
hence contradiction by A117,A122,SEQ_2:1;
end;
hence thesis;
end;
for x,y be object st x in dom f3 & y in dom f3 & f3.x=f3.y holds x=y
proof
let x,y be object;
assume that
A123: x in dom f3 and
A124: y in dom f3 and
A125: f3.x=f3.y;
reconsider x,y as Element of NAT by A123,A124;
A126: f1.y = f2.y * p + f3.y by A97,A101,A124;
f1.x = f2.x * p + f3.x by A97,A101,A123;
then f1.x - f1.y = (f2.x - f2.y) * p by A125,A126;
then p divides (f1.x - f1.y);
hence thesis by A110,A97,A123,A124;
end;
then
A127: f3 is one-to-one;
then len f3 = card rng f3 by FINSEQ_4:62;
then
A128: len f4 = p9 by A18,A96,A99,A108,FINSEQ_3:39,XBOOLE_1:73;
A129: g4|nn = Sgm YY by A92,A94,FINSEQ_3:113,FINSEQ_6:10;
A130: g4|nn is one-to-one by A48,A81,FINSEQ_3:91;
A131: Lege(p,q) = (-1)|^(Sum g2)
proof
set g5 = (mm|->q)-(g4/^nn);
set g6 = (g4|nn)^g5;
A132: g4/^nn is FinSequence of REAL by FINSEQ_2:24,NUMBERS:19;
A133: len(g4|nn) = nn by A67,FINSEQ_1:59,XREAL_1:43;
A134: len(g4/^nn) = (len g4 -' nn) by RFINSEQ:29
.= len g4 - nn by A67,XREAL_1:43,233
.= mm by A67;
A135: dom g5 = dom(mm |-> q) /\ dom(g4/^nn) by VALUED_1:12
.= (Seg len (mm |-> q)) /\ dom(g4/^nn) by FINSEQ_1:def 3
.= (Seg len(g4/^nn))/\dom(g4/^nn) by A134,CARD_1:def 7
.= dom(g4/^nn) /\ dom(g4/^nn) by FINSEQ_1:def 3
.= dom(g4/^nn);
then
A136: len g5 = len(g4/^nn) by FINSEQ_3:29;
A137: for d st d in dom g5 holds g5.d = q - (g4/^nn).d
proof
let d;
assume
A138: d in dom g5;
then d in Seg mm by A134,A135,FINSEQ_1:def 3;
then (mm |-> q).d = q by FINSEQ_2:57;
hence thesis by A138,VALUED_1:13;
end;
A139: for d st d in dom g5 holds g5.d > 0 & g5.d <= q9
proof
let d;
reconsider w = g5.d as Element of INT by INT_1:def 2;
assume
A140: d in dom g5;
then (Sgm XX).d in rng Sgm XX by A95,A135,FUNCT_1:3;
then (Sgm XX).d in XX by A79,FINSEQ_1:def 13;
then
A141: ex ll be Element of NAT st ll = (Sgm XX).d & ll in rng g3 &
ll > q/2 by A78;
then consider e being Nat such that
A142: e in dom g3 and
A143: g3.e=(g4/^nn).d by A95,FINSEQ_2:10;
(g4/^nn).d = g1.e mod q by A25,A142,A143,EULER_2:def 1;
then
A144: (g4/^nn).d < q by NAT_D:1;
A145: g5.d = q - (g4/^nn).d by A137,A140;
then w < q - q/2 by A95,A141,XREAL_1:10;
hence thesis by A83,A145,A144,INT_1:54,XREAL_1:50;
end;
A146: rng g5 c= INT by RELAT_1:def 19;
for d being Nat st d in dom g5 holds g5.d in NAT
proof
let d be Nat;
assume
A147: d in dom g5;
g5.d > 0 by A139,A147;
hence thesis by A146,INT_1:3;
end;
then reconsider g5 as FinSequence of NAT by FINSEQ_2:12;
g5 is FinSequence of NAT;
then reconsider g6 as FinSequence of NAT by FINSEQ_1:75;
A148: g6 is FinSequence of REAL by FINSEQ_2:24,NUMBERS:19;
A149: nn <= len g4 by A67,XREAL_1:43;
A150: rng(g4|nn) misses rng g5
proof
assume not rng(g4|nn) misses rng g5;
then consider x be object such that
A151: x in rng(g4|nn) and
A152: x in rng g5 by XBOOLE_0:3;
consider e being Nat such that
A153: e in dom g5 and
A154: g5.e = x by A152,FINSEQ_2:10;
x = q - (g4/^nn).e by A137,A153,A154;
then
A155: x = q - g4.(e+nn) by A149,A135,A153,RFINSEQ:def 1;
e+nn in dom g4 by A135,A153,FINSEQ_5:26;
then consider e1 be Nat such that
A156: e1 in dom g3 and
A157: g3.e1 = g4.(e+nn) by A78,FINSEQ_2:10,FUNCT_1:3;
A158: e1 <= q9 by A23,A24,A156,FINSEQ_3:25;
rng(g4|nn) c= rng g4 by FINSEQ_5:19;
then consider d1 be Nat such that
A159: d1 in dom g3 and
A160: g3.d1 = x by A78,A151,FINSEQ_2:10;
d1 <= q9 by A23,A24,A159,FINSEQ_3:25;
then d1+e1 <= q9+q9 by A158,XREAL_1:7;
then
A161: d1+e1 < q by A29,A40,XREAL_1:146,XXREAL_0:2;
A162: e1 in dom g1 by A24,A156,FINSEQ_3:29;
then
A163: g4.(e+nn) = g1.e1 mod q by A157,EULER_2:def 1;
A164: d1 in dom g1 by A24,A159,FINSEQ_3:29;
then x = g1.d1 mod q by A160,EULER_2:def 1;
then ((g1.d1 mod q)+(g1.e1 mod q)) mod q = 0 by A155,A163,NAT_D:25;
then (g1.d1 + g1.e1) mod q = 0 by EULER_2:6;
then q divides (g1.d1 + g1.e1) by PEPIN:6;
then q divides (d1*p + g1.e1) by A19,A164;
then q divides (d1*p + e1*p) by A19,A162;
then
A165: q divides (d1+e1)*p;
d1 >= 1 by A159,FINSEQ_3:25;
hence contradiction by A4,A165,A161,NAT_D:7,PEPIN:3;
end;
for d,e being Nat st 1<=d & d