:: Gauss Lemma and Law of Quadratic Reciprocity
:: by Li Yan , Xiquan Liang and Junjie Zhao
::
:: Received October 9, 2007
:: Copyright (c) 2007-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, INT_1, NAT_1, FINSEQ_1, NEWTON, ARYTM_3,
ARYTM_1, RELAT_1, CARD_1, FUNCT_1, CARD_3, FUNCOP_1, ORDINAL4, XBOOLE_0,
TARSKI, XXREAL_0, FINSEQ_5, SQUARE_1, INT_2, COMPLEX1, ABIAN, FINSEQ_2,
FUNCT_7, PARTFUN1, FINSET_1, RFINSEQ, CALCUL_2, REAL_1, ZFMISC_1, INT_5,
ORDINAL1, VALUED_0, NUMBER09;
notations XREAL_0, GROUP_4, INT_1, RVSUM_1, FINSET_1, ORDINAL1, CARD_1, NAT_D,
INT_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NAT_3, ABIAN, GR_CY_1,
VALUED_0,
FINSEQ_5, FINSEQ_2, EULER_2, NEWTON, FINSEQ_7, REAL_1, PEPIN, TARSKI,
XBOOLE_0, SUBSET_1, XCMPLX_0, NUMBERS, XXREAL_0, NAT_1, DOMAIN_1,
FINSEQ_1, RFINSEQ, FUNCOP_1, CALCUL_2, ZFMISC_1, CARD_3, WSIERP_1,
BINOP_1, RECDEF_1;
constructors ABIAN, WSIERP_1, PEPIN, NAT_3, NAT_D, REALSET1, GR_CY_1,
FINSEQ_5, EULER_2, RFINSEQ, GROUP_4, FINSEQ_7, REAL_1, WELLORD2,
CALCUL_2, PROB_3, RECDEF_1, BINOP_1, BINOP_2, CLASSES1, NUMBERS;
registrations XXREAL_0, MEMBERED, RELAT_1, FINSEQ_1, ORDINAL1, WSIERP_1,
NUMBERS, XBOOLE_0, XREAL_0, NAT_1, INT_1, FINSET_1, NAT_3, RVSUM_1,
FUNCT_1, CARD_1, NEWTON, SUBSET_1, VALUED_0, VALUED_1, FINSEQ_2,
PRE_POLY, RELSET_1, EULER_2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
equalities INT_1, XCMPLX_0, SQUARE_1, FINSEQ_2, CALCUL_2, CARD_3;
expansions INT_1, FUNCT_1, TARSKI;
theorems FINSEQ_1, FINSEQ_7, RELAT_1, FINSEQ_3, FINSEQ_2, ABSVALUE, FINSEQ_5,
EULER_2, SEQ_2, FINSEQ_4, FUNCT_2, XBOOLE_0, NAT_3, NEWTON, INT_2, NAT_2,
WSIERP_1, CARD_1, PEPIN, NAT_1, XCMPLX_1, XREAL_1, HEYTING3, ORDINAL1,
EULER_1, XBOOLE_1, TARSKI, RVSUM_1, NUMBERS, INT_1, FUNCT_1, FUNCOP_1,
XXREAL_0, NAT_D, HILBERT3, SERIES_2, GRAPH_5, HILBERT2, RFINSEQ,
ZFMISC_1, CARD_2, XREAL_0, FINSEQ_6, CALCUL_2, NAT_4, PROB_3, TOPREAL7,
CARD_3, REAL_3, PRE_FF, INT_4, VALUED_1, PRE_POLY, XTUPLE_0;
schemes NAT_1, FUNCT_2, RECDEF_1, FINSEQ_2, FUNCT_7, FINSEQ_1;
begin
reserve i,i1,i2,i3,i4,i5,j,r,a,b,x,y for Integer,
d,e,k,n for Nat,
fp,fk for FinSequence of INT,
f,f1,f2 for FinSequence of REAL,
p for Prime;
theorem Th1:
i1 divides i2 & i1 divides i3 implies i1 divides i2-i3
proof
assume that
A1: i1 divides i2 and
A2: i1 divides i3;
consider i4 such that
A3: i2=i1*i4 by A1;
consider i5 such that
A4: i3=i1*i5 by A2;
i2-i3=i1*(i4-i5) by A3,A4;
hence thesis;
end;
theorem Th2:
i divides a & i divides (a-b) implies i divides b
proof
assume that
A1: i divides a and
A2: i divides (a-b);
A3: b=-(a-b)+a;
i divides -(a-b) by A2,INT_2:10;
hence thesis by A1,A3,WSIERP_1:4;
end;
Lm1: (x divides y implies y mod x = 0) &
(x<>0 & y mod x = 0 implies x divides y)
proof
thus x divides y implies y mod x = 0
proof
assume x divides y;
then consider i such that
A1: y = x * i;
y mod x = (x * i + 0) mod x by A1
.= 0 mod x by NAT_D:61
.= 0 by INT_1:73;
hence thesis;
end;
assume that
A2: x<>0 and
A3: y mod x = 0;
y = (y div x) * x + (y mod x) by A2,INT_1:59
.= (y div x) * x by A3;
hence thesis;
end;
definition
let fp;
func Poly-INT fp -> Function of INT,INT means
:Def1:
for x being Element of
INT holds ex fr being FinSequence of INT st len fr = len fp & (for d st d in
dom fr holds fr.d = (fp.d) * x|^(d-'1)) & it.x = Sum fr;
existence
proof
defpred F[Element of INT,set] means ex fr being FinSequence of INT st len
fr = len fp & (for d st d in dom fr holds fr.d = (fp.d) * $1|^(d-'1)) & $2 =
Sum fr;
A1: for x being Element of INT ex y being Element of INT st F[x,y]
proof
let x be Element of INT;
deffunc G(Nat) = (fp.$1) * x|^($1-'1);
consider fr be FinSequence such that
A2: len fr = len fp & for d being Nat st d in dom fr holds fr.d = G(
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 = (fp.d) * x|^(d-'1) by A2;
hence thesis by INT_1:def 2;
end;
then reconsider fr as FinSequence of INT by FINSEQ_2:12;
take Sum fr;
take fr;
thus thesis by A2;
end;
consider f being Function of INT,INT such that
A3: for x being Element of INT holds F[x,f.x] from FUNCT_2:sch 3(A1);
take f;
thus thesis by A3;
end;
uniqueness
proof
let f1 be Function of INT,INT;
let f2 be Function of INT,INT;
assume that
A4: for x being Element of INT holds ex fr1 being FinSequence of INT
st len fr1 = len fp & (for d st d in dom fr1 holds fr1.d = (fp.d) * x|^(d-'1))
& f1.x = Sum fr1 and
A5: for x being Element of INT holds ex fr2 being FinSequence of INT
st len fr2 = len fp & (for d st d in dom fr2 holds fr2.d = (fp.d) * x|^(d-'1))
& f2.x = Sum fr2;
for x being Element of INT holds f1.x = f2.x
proof
let x be Element of INT;
consider fr1 being FinSequence of INT such that
A6: len fr1 = len fp and
A7: for d st d in dom fr1 holds fr1.d = (fp.d) * x|^(d-'1) and
A8: f1.x = Sum fr1 by A4;
consider fr2 being FinSequence of INT such that
A9: len fr2 = len fp and
A10: for d st d in dom fr2 holds fr2.d = (fp.d) * x|^(d-'1) and
A11: f2.x = Sum fr2 by A5;
A12: dom fr1 = dom fr2 by A6,A9,FINSEQ_3:29;
for d being Nat st d in dom fr1 holds fr1.d = fr2.d
proof
let d be Nat;
assume
A13: d in dom fr1;
hence fr2.d = (fp.d) * x|^(d-'1) by A10,A12
.= fr1.d by A7,A13;
end;
hence thesis by A8,A11,A12,FINSEQ_1:13;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Th3:
len fp = 1 implies (Poly-INT fp) = INT --> fp.1
proof
assume
A1: len fp = 1;
for x being object st x in dom Poly-INT fp holds (Poly-INT fp).x = fp.1
proof
let x be object;
assume x in dom Poly-INT fp;
then reconsider x as Element of INT;
consider fr being FinSequence of INT such that
A2: len fr = len fp and
A3: for d st d in dom fr holds fr.d = (fp.d) * x|^(d-'1) and
A4: (Poly-INT fp).x = Sum fr by Def1;
1 in dom fr by A1,A2,FINSEQ_3:25;
then
A5: fr.1 = (fp.1) * x|^(1-'1) by A3
.= fp.1 * x|^0 by XREAL_1:232
.= fp.1 * 1 by NEWTON:4;
fr = <*fr.1*> by A1,A2,FINSEQ_1:40;
hence thesis by A4,A5,RVSUM_1:73;
end;
then Poly-INT fp = dom Poly-INT fp --> fp.1 by FUNCOP_1:11;
hence thesis by FUNCT_2:def 1;
end;
theorem
len fp = 1 implies for x being Element of INT holds (Poly-INT fp).x = fp.1
proof
assume
A1: len fp = 1;
let x be Element of INT;
consider fr being FinSequence of INT such that
A2: len fr = len fp and
A3: for d st d in dom fr holds fr.d = (fp.d) * x|^(d-'1) and
A4: (Poly-INT fp).x = Sum fr by Def1;
1 in dom fr by A1,A2,FINSEQ_3:25;
then
A5: fr.1 = (fp.1) * x|^(1-'1) by A3
.= fp.1 * x|^0 by XREAL_1:232
.= fp.1 * 1 by NEWTON:4;
fr = <*fr.1*> by A1,A2,FINSEQ_1:40;
hence thesis by A4,A5,RVSUM_1:73;
end;
reserve fr for FinSequence of REAL;
theorem Th5:
for f,f1,f2 st len f = n+1 & len f1 = len f & len f2 = len f & (
for d st d in dom f holds f.d = f1.d - f2.d) holds ex fr st len fr = len f - 1
& (for d st d in dom fr holds fr.d = f1.d - f2.(d + 1)) & Sum f = Sum fr + f1.(
n+1) - f2.1
proof
defpred P[Nat] means for f,f1,f2 st len f = $1 + 1 & len f1 = len f & len f2
= len f & (for d st d in dom f holds f.d = f1.d - f2.d) holds ex fr st len fr =
len f - 1 & (for d st d in dom fr holds fr.d = f1.d - f2.(d + 1)) & Sum f = Sum
fr + f1.($1+1) - f2.1;
A1: for n st P[n] holds P[n+1]
proof
let n;
assume
A2: P[n];
let f,f1,f2;
assume that
A3: len f = (n+1)+1 and
A4: len f1 = len f and
A5: len f2 = len f and
A6: for d st d in dom f holds f.d = f1.d - f2.d;
set ff1 = f1|Seg(n+1);
reconsider ff1 as FinSequence of REAL by FINSEQ_1:18;
A7: len ff1 = n+1 by A3,A4,FINSEQ_3:53;
set ff2 = f2|Seg(n+1);
reconsider ff2 as FinSequence of REAL by FINSEQ_1:18;
A8: f2 = ff2^<*f2.((n+1)+1)*> by A3,A5,FINSEQ_3:55;
A9: len ff2 = n+1 by A3,A5,FINSEQ_3:53;
then ff2 <> {};
then 1 in dom ff2 by FINSEQ_5:6;
then
A10: ff2.1 = f2.1 by A8,FINSEQ_1:def 7;
A11: f1 = ff1^<*f1.((n+1)+1)*> by A3,A4,FINSEQ_3:55;
(n+1)+1 in Seg ((n+1)+1) by FINSEQ_1:4;
then ((n+1)+1) in dom f by A3,FINSEQ_1:def 3;
then
A12: f.((n+1)+1) = f1.((n+1)+1) - f2.((n+1)+1) by A6;
set f3 = f|Seg(n+1);
reconsider f3 as FinSequence of REAL by FINSEQ_1:18;
A13: dom f3 = Seg(n+1) by A3,FINSEQ_3:54;
then
A14: len f3 = n+1 by FINSEQ_1:def 3;
A15: f = f3^<*f.(n+1+1)*> by A3,FINSEQ_3:55;
A16: for d st d in dom f3 holds f3.d = ff1.d - ff2.d
proof
let d;
A17: dom f3 c= dom f by A15,FINSEQ_1:26;
assume
A18: d in dom f3;
then
A19: d in dom ff2 by A13,A9,FINSEQ_1:def 3;
d in dom ff1 by A13,A7,A18,FINSEQ_1:def 3;
then
A20: f1.d = ff1.d by A11,FINSEQ_1:def 7;
f3.d = f.d by A15,A18,FINSEQ_1:def 7
.= f1.d - f2.d by A6,A18,A17;
hence thesis by A8,A19,A20,FINSEQ_1:def 7;
end;
ff1 <> {} by A7;
then (n+1) in dom ff1 by A7,FINSEQ_5:6;
then ff1.(n+1) = f1.(n+1) by A11,FINSEQ_1:def 7;
then consider f4 being FinSequence of REAL such that
A21: len f4 = len f3 - 1 and
A22: for d st d in dom f4 holds f4.d=ff1.d - ff2.(d + 1) and
A23: Sum f3 = Sum f4 + f1.(n+1) - f2.1 by A2,A14,A7,A9,A16,A10;
take f5 = f4^<*f1.(n+1) - f2.(n+2)*>;
reconsider f5 as FinSequence of REAL by FINSEQ_1:75;
A24: Sum f = Sum f4 + f1.(n+1) - f2.1 + f.(n+1+1) by A15,A23,RVSUM_1:74
.= Sum f4 + (f1.(n+1) - f2.(n+2)) + f1.((n+1)+1) - f2.1 by A12
.= Sum f5 + f1.((n+1)+1) - f2.1 by RVSUM_1:74;
A25: len f4 + 1 = n + 1 by A13,A21,FINSEQ_1:def 3;
A26: for d st d in dom f5 holds f5.d = f1.d - f2.(d + 1)
proof
let d;
assume d in dom f5;
then d in Seg len f5 by FINSEQ_1:def 3;
then d in Seg (len f4 + 1) by FINSEQ_2:16;
then d in Seg len f4 \/{len f4 + 1} by FINSEQ_1:9;
then
A27: d in Seg len f4 or d in {len f4 + 1} by XBOOLE_0:def 3;
per cases by A27,TARSKI:def 1;
suppose
A28: d in Seg len f4;
then d+1 in Seg(len f4 + 1) by FINSEQ_1:60;
then d+1 in Seg len ff2 by A3,A5,A14,A21,FINSEQ_3:53;
then
A29: d+1 in dom ff2 by FINSEQ_1:def 3;
A30: d in dom f4 by A28,FINSEQ_1:def 3;
len f4 <= len ff1 by A14,A7,A21,XREAL_1:147;
then dom f4 c= dom ff1 by FINSEQ_3:30;
then
A31: f1.d = ff1.d by A11,A30,FINSEQ_1:def 7;
f5.d = f4.d by A30,FINSEQ_1:def 7
.= ff1.d - ff2.(d+1) by A22,A30;
hence thesis by A8,A31,A29,FINSEQ_1:def 7;
end;
suppose
A32: d = len f4 + 1;
1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then 1 in dom <*f1.(n+1) - f2.(n+2)*> by FINSEQ_1:38;
then f5.d = <*f1.(n+1) - f2.(n+2)*>.1 by A32,FINSEQ_1:def 7
.= f1.d - f2.(d+1) by A25,A32;
hence thesis;
end;
end;
len f5 = len f4 + 1 by FINSEQ_2:16
.= len f - 1 by A3,A13,A21,FINSEQ_1:def 3;
hence thesis by A26,A24;
end;
A33: P[0]
proof
let f,f1,f2;
assume that
A34: len f = 0+1 and
len f1 = len f and
len f2 = len f and
A35: for d st d in dom f holds f.d = f1.d - f2.d;
take <*>REAL;
0+1 in Seg (0+1) by FINSEQ_1:4;
then 1 in dom f by A34,FINSEQ_1:def 3;
then f.1 = f1.1 - f2.1 by A35;
then f = <*f1.1 - f2.1*> by A34,FINSEQ_1:40;
hence thesis by A34,RVSUM_1:72,73;
end;
for n holds P[n] from NAT_1:sch 2(A33,A1);
hence thesis;
end;
theorem Th6:
len fp = n+2 implies for a being Integer holds ex fr being
FinSequence of INT, r being Integer st len fr = n+1 & (for x being Element of
INT holds (Poly-INT fp).x = (x-a)*(Poly-INT fr).x + r) & fp.(n+2) = fr.(n+1)
proof
assume
A1: len fp = n+2;
(n+1)+1 in Seg ((n+1)+1) by FINSEQ_1:4;
then n+2 in dom fp by A1,FINSEQ_1:def 3;
then reconsider A = fp.(n+2) as Element of INT by FINSEQ_2:11;
reconsider n1=n+1 as Element of NAT;
let a be Integer;
defpred P[Nat,Integer,set] means $3 = fp.(n+2-$1) +a*$2;
A2: for d being Nat st 1 <= d & d < n1 holds for x being Element
of INT ex y being Element of INT st P[d,x,y]
proof
let d be Nat;
assume that
1 <= d and
d < n1;
let x be Element of INT;
set y = fp.(n+2-d) +a*x;
reconsider y as Element of INT by INT_1:def 2;
take y;
thus thesis;
end;
consider p being FinSequence of INT such that
A3: len p = n1 & (p.1 = A or n1 = 0) & for d being Nat st 1
<= d & d < n1 holds P[d,p.d,p.(d+1)] from RECDEF_1:sch 4(A2);
take fr = Rev p;
take r = fp.1 + a*fr.1;
A4: len fr = n+1 by A3,FINSEQ_5:def 3;
for x being Element of INT holds (Poly-INT fp).x = (x-a)*(Poly-INT fr).x + r
proof
let x be Element of INT;
deffunc F(Nat) = (fr.$1)*x|^$1;
deffunc FF(Nat) = a*(fr.$1) * x|^($1-'1);
consider f1 being FinSequence of INT such that
A5: len f1 = len fp and
A6: for d st d in dom f1 holds f1.d = (fp.d) * x|^(d-'1) and
A7: (Poly-INT fp).x = Sum f1 by Def1;
A8: f1 <> {} by A1,A5;
then n+2 in dom f1 by A1,A5,FINSEQ_5:6;
then f1.(n+2)=(fp.(n+2))*x|^((n+1)+1-'1) by A6;
then
A9: f1.(n+2)=(fp.(n+2))*x|^(n+1) by NAT_D:34;
f1.1 = (fp.1)*x|^(1-'1) by A6,A8,FINSEQ_5:6;
then f1.1=(fp.1)*x|^0 by XREAL_1:232;
then
A10: f1.1 = (fp.1)*1 by NEWTON:4;
reconsider n as Element of NAT by ORDINAL1:def 12;
consider f4 being FinSequence such that
A11: len f4 = n+1 & for d being Nat st d in dom f4 holds f4.d=F(d)
from FINSEQ_1:sch 2;
A12: for d being Nat st d in dom f4 holds f4.d in INT
proof
let d be Nat;
reconsider d1 = d as Element of NAT by ORDINAL1:def 12;
assume d in dom f4;
then f4.d1 = (fr.d1)*x|^d1 by A11;
hence thesis by INT_1:def 2;
end;
f4 <> {} by A11;
then n+1 in dom f4 by A11,FINSEQ_5:6;
then f4.(n+1)=(fr.(n+1))*x|^(n+1) by A11;
then
A13: f4.(n+1) = (fp.(n+2))*x|^(n+1) by A3,FINSEQ_5:62;
reconsider f4 as FinSequence of INT by A12,FINSEQ_2:12;
consider f5 being FinSequence such that
A14: len f5 = n+1 & for d being Nat st d in dom f5 holds f5.d=FF(d)
from FINSEQ_1:sch 2;
A15: for d being Nat st d in dom f5 holds f5.d in INT
proof
let d be Nat;
assume d in dom f5;
then f5.d = a*(fr.d) * x|^(d-'1) by A14;
hence thesis by INT_1:def 2;
end;
f5 <> {} by A14;
then 1 in dom f5 by FINSEQ_5:6;
then f5.1 = a*(fr.1) * x|^(1-'1) by A14;
then f5.1 = a*(fr.1)*x|^0 by XREAL_1:232;
then
A16: f5.1 = a*(fr.1)*1 by NEWTON:4;
reconsider f5 as FinSequence of INT by A15,FINSEQ_2:12;
A17: f4 is FinSequence of REAL by FINSEQ_3:117;
consider f2 being FinSequence of INT such that
A18: len f2 = len fr and
A19: for d st d in dom f2 holds f2.d = (fr.d) * x|^(d-'1) and
A20: (Poly-INT fr).x = Sum f2 by Def1;
set f3 = (x-a)*f2;
A21: dom f3 = dom f2 by VALUED_1:def 5;
then
A22: len f3 = len f2 by FINSEQ_3:29;
A23: dom f3 = dom f4 by A4,A18,A11,A21,FINSEQ_3:29;
A24: for k being Element of NAT st k in dom f3 holds f3.k = (fr.k)*x|^k -
a*(fr.k) * x|^(k-'1)
proof
let k be Element of NAT;
assume
A25: k in dom f3;
then
A26: k >= 1 by FINSEQ_3:25;
A27: k in dom f2 by A25,VALUED_1:def 5;
thus f3.k = (x-a)*(f2.k) by A25,VALUED_1:def 5
.= (x-a)*((fr.k) * x|^(k-'1)) by A19,A27
.= (fr.k) * (x|^(k-'1)*x) - a*(fr.k) * x|^(k-'1)
.= (fr.k)*x|^(k-'1+1) - a*(fr.k) * x|^(k-'1) by NEWTON:6
.= (fr.k)*x|^k - a*(fr.k) * x|^(k-'1) by A26,XREAL_1:235;
end;
A28: dom f3 = dom f5 by A4,A18,A14,A21,FINSEQ_3:29;
A29: for d st d in dom f3 holds f3.d = f4.d - f5.d
proof
let d;
assume
A30: d in dom f3;
then
A31: f5.d = a*(fr.d) * x|^(d-'1) by A14,A28;
f4.d = (fr.d)*x|^d by A11,A23,A30;
hence thesis by A24,A30,A31;
end;
f5 is FinSequence of REAL by FINSEQ_3:117;
then consider f6 being FinSequence of REAL such that
A32: len f6 = len f3 - 1 and
A33: for d st d in dom f6 holds f6.d = f4.d - f5.(d + 1) and
A34: Sum f3 = Sum f6 + f4.(n+1) - f5.1 by A4,A18,A11,A14,A22,A29,A17,Th5;
A35: len f6 <= len f3 by A4,A18,A22,A32,XREAL_1:145;
then
A36: dom f6 c= dom f3 by FINSEQ_3:30;
A37: for d being Element of NAT st d in dom f6 holds f6.d = f1.(d+1)
proof
let d be Element of NAT;
A38: dom f6 c= dom p by A3,A4,A18,A22,A35,FINSEQ_3:30;
assume
A39: d in dom f6;
then
A40: d in Seg n by A4,A18,A22,A32,FINSEQ_1:def 3;
then
A41: d <= n by FINSEQ_1:1;
then
A42: n-d >= 0 by XREAL_1:48;
then reconsider d9=n-d+1 as Element of NAT by INT_1:3;
d >= 1 by A40,FINSEQ_1:1;
then n-d <= n-1 by XREAL_1:10;
then d9 <= (n-1)+1 by XREAL_1:6;
then
A43: d9 < n+1 by XREAL_1:145;
d9 >= 0+1 by A42,XREAL_1:6;
then
A44: p.(d9+1) = fp.(n+2-d9) +a*(p.d9) by A3,A43;
d < n+1 by A41,XREAL_1:145;
then
A45: d+1 in Seg (n+1) by FINSEQ_3:11;
then
A46: d+1 in dom f5 by A14,FINSEQ_1:def 3;
d+0 < n+2 by A41,XREAL_1:8;
then d+1 in Seg (n+2) by FINSEQ_3:11;
then
A47: d+1 in dom f1 by A1,A5,FINSEQ_1:def 3;
A48: d+1 in dom p by A3,A45,FINSEQ_1:def 3;
thus f6.d = f4.d - f5.(d + 1) by A33,A39
.= (fr.d)*x|^d - f5.(d+1) by A11,A23,A36,A39
.= (fr.d)*x|^d - a*fr.(d+1) * x|^(d+1-'1) by A14,A46
.= (fr.d)*x|^d - a*(fr.(d+1)) * x|^d by NAT_D:34
.= ((fr.d) - a*fr.(d+1))* x|^d
.= (p.((n+1)-d+1) - a*fr.(d+1))* x|^d by A3,A39,A38,FINSEQ_5:58
.= (p.((n-d+1)+1)-a*p.((n+1)-(d+1)+1))* x|^d by A3,A48,FINSEQ_5:58
.= fp.(d+1)* x|^(d+1-'1) by A44,NAT_D:34
.= f1.(d+1) by A6,A47;
end;
f1 = <*f1.1*>^f6^<*f1.(n+2)*>
proof
set K = <*f1.1*>^f6^<*f1.(n+2)*>;
A49: for d being Nat st d in dom f1 holds f1.d = K.d
proof
let d be Nat;
assume
A50: d in dom f1;
then
A51: d>=1 by FINSEQ_3:25;
A52: d<=n+2 by A1,A5,A50,FINSEQ_3:25;
per cases by A51,A52,XXREAL_0:1;
suppose
A53: d=1;
hence K.d = (<*f1.1*>^(f6^<*f1.(n+2)*>)).1 by FINSEQ_1:32
.= f1.d by A53,FINSEQ_1:41;
end;
suppose
A54: d>1 & d<n+2;
then reconsider w=d-1 as Element of NAT by INT_1:3;
d-1<n+2-1 by A54,XREAL_1:9;
then
A55: d-1<=n+1-1 by INT_1:7;
d-1>=0+1 by A54,INT_1:7,XREAL_1:50;
then w in Seg n by A55,FINSEQ_1:1;
then
A56: w in dom f6 by A4,A18,A22,A32,FINSEQ_1:def 3;
then
A57: w in dom (f6^<*f1.(n+2)*>) by FINSEQ_2:15;
thus K.d = (<*f1.1*>^(f6^<*f1.(n+2)*>)).(w+1) by FINSEQ_1:32
.= (f6^<*f1.(n+2)*>).w by A57,FINSEQ_3:103
.= f6.w by A56,FINSEQ_1:def 7
.= f1.(w+1) by A37,A56
.= f1.d;
end;
suppose
A58: d=n+2;
set K1 = <*f1.1*>^f6;
thus K.d = K.((n+1)+1) by A58
.= K.(len K1 +1) by A4,A18,A22,A32,FINSEQ_5:8
.= f1.d by A58,FINSEQ_1:42;
end;
end;
len K = len (<*f1.1*>^(f6^<*f1.(n+2)*>)) by FINSEQ_1:32
.= 1+len (f6^<*f1.(n+2)*>) by FINSEQ_5:8
.= 1+len f6 +1 by FINSEQ_2:16
.= len f1 by A1,A4,A5,A18,A22,A32;
hence thesis by A49,FINSEQ_3:29;
end;
then Sum f1 = Sum (<*f1.1*>^(f6^<*f1.(n+2)*>)) by FINSEQ_1:32
.= f1.1 + Sum (f6^<*f1.(n+2)*>) by RVSUM_1:76
.= f1.1 + (Sum f6 + f1.(n+2)) by RVSUM_1:74
.= Sum ((x-a)*f2) + r by A10,A9,A13,A16,A34
.= (x-a) * (Poly-INT fr).x + r by A20,RVSUM_1:87;
hence thesis by A7;
end;
hence thesis by A3,FINSEQ_5:62,def 3;
end;
theorem Th7:
p divides i*j implies p divides i or p divides j
proof
assume
A1: p divides i*j;
per cases;
suppose
i>=0 & j>=0;
then reconsider i,j as Element of NAT by INT_1:3;
p divides i*j by A1;
hence thesis by NEWTON:80;
end;
suppose
i>=0 & j<0;
then reconsider i,j9=-j as Element of NAT by INT_1:3;
p divides -(i*j) by A1,INT_2:10;
then p divides i*j9;
then p divides i or p divides j9 by NEWTON:80;
hence thesis by INT_2:10;
end;
suppose
i<0 & j>=0;
then reconsider i9=-i,j as Element of NAT by INT_1:3;
p divides -(i*j) by A1,INT_2:10;
then p divides i9*j;
then p divides i9 or p divides j by NEWTON:80;
hence thesis by INT_2:10;
end;
suppose
i<0 & j<0;
then reconsider i9=-i,j9=-j as Element of NAT by INT_1:3;
p divides i9*j9 by A1;
then p divides i9 or p divides j9 by NEWTON:80;
hence thesis by INT_2:10;
end;
end;
reserve fr,f for FinSequence of INT;
theorem Th8:
for fp st len fp = n+1 & p>2 & not p divides fp.(n+1) holds for
fr st (for d st d in dom fr holds (Poly-INT fp).(fr.d) mod p=0) & (for d,e st d
in dom fr & e in dom fr & d<>e holds not fr.d,fr.e are_congruent_mod p) holds
len fr <= n
proof
defpred P[Nat] means for fp st len fp = $1+1 & p>2 & not p divides fp.($1+1)
holds for fr st (for d st d in dom fr holds (Poly-INT fp).(fr.d) mod p = 0) & (
for d,e st d in dom fr & e in dom fr & d<>e holds not fr.d,fr.e
are_congruent_mod p) holds len fr <= $1;
A1: for n st P[n] holds P[n+1]
proof
let n;
assume
A2: P[n];
let fp;
assume that
A3: len fp = (n+1)+1 and
A4: p>2 and
A5: not p divides fp.(n+1+1);
per cases;
suppose
A6: for x holds (Poly-INT fp).x mod p <> 0;
assume ex fr st (for d st d in dom fr holds (Poly-INT fp).(fr.d) mod p
=0) & (for d,e st d in dom fr & e in dom fr & d<>e holds not fr.d,fr.e
are_congruent_mod p) & len fr > n+1;
then consider fr such that
A7: for d st d in dom fr holds (Poly-INT fp).(fr.d) mod p=0 and
for d,e st d in dom fr & e in dom fr & d<>e holds not fr.d,fr.e
are_congruent_mod p and
A8: len fr > n+1;
fr <> {} by A8;
then (Poly-INT fp).(fr.1) mod p=0 by A7,FINSEQ_5:6;
hence contradiction by A6;
end;
suppose
ex a being Integer st (Poly-INT fp).a mod p = 0;
then consider a being Integer such that
A9: (Poly-INT fp).a mod p=0;
assume ex f st (for d st d in dom f holds (Poly-INT fp).(f.d) mod p =
0) & (for d,e st d in dom f & e in dom f & d<>e holds not f.d,f.e
are_congruent_mod p) & len f > n+1;
then consider f such that
A10: for d st d in dom f holds (Poly-INT fp).(f.d) mod p = 0 and
A11: for d,e st d in dom f & e in dom f & d<>e holds not f.d,f.e
are_congruent_mod p and
A12: len f > n+1;
consider fk,r such that
A13: len fk = n+1 and
A14: for x being Element of INT holds (Poly-INT fp).x =(x-a)*(
Poly-INT fk).x +r and
A15: fp.(n+2)=fk.(n+1) by A3,Th6;
a is Element of INT by INT_1:def 2;
then
A16: (Poly-INT fp).a mod p =((a-a)*(Poly-INT fk).a +r) mod p by A14
.= r mod p;
A17: for d being Element of NAT st d in dom f holds p divides (f.d -a)*(
Poly-INT fk).(f.d)
proof
let d be Element of NAT;
f.d is Element of INT by INT_1:def 2;
then
A18: (Poly-INT fp).(f.d) mod p = (((f.d-a)*(Poly-INT fk).(f.d)) +r)
mod p by A14
.=(((f.d-a)*(Poly-INT fk).(f.d)) mod p + (r mod p)) mod p by NAT_D:66
.= ((f.d-a)*(Poly-INT fk).(f.d)) mod p by A9,A16,NAT_D:65;
assume d in dom f;
then ((f.d-a)*(Poly-INT fk).(f.d)) mod p = 0 by A10,A18;
hence thesis by INT_1:62;
end;
per cases;
suppose
A19: for d st d in dom f holds not p divides (f.d - a);
for d st d in dom f holds (Poly-INT fk).(f.d) mod p = 0
proof
let d;
assume
A20: d in dom f;
then p divides (f.d -a)*(Poly-INT fk).(f.d) by A17;
then p divides (f.d -a) or p divides (Poly-INT fk).(f.d) by Th7;
hence thesis by A19,A20;
end;
then len f <= n by A2,A4,A5,A13,A15,A11;
hence contradiction by A12,XREAL_1:145;
end;
suppose
ex d st d in dom f & p divides (f.d - a);
then consider d9 being Element of NAT such that
A21: d9 in dom f and
A22: p divides (f.d9 - a);
set f9 = f - {f.d9};
A23: for d st d in dom f9 holds not p divides (f9.d - a)
proof
given k being Nat such that
A24: k in dom f9 and
A25: p divides (f9.k -a);
f9.k in rng f9 by A24,FUNCT_1:3;
then
A26: f9.k in rng f \ {f.d9} by FINSEQ_3:65;
then f9.k in rng f by XBOOLE_0:def 5;
then consider w being object such that
A27: w in dom f and
A28: f.w = f9.k by FUNCT_1:def 3;
reconsider w as Element of NAT by A27;
p divides ((f.w - a)-(f.d9 - a)) by A22,A25,A28,Th1; then
A29: f.w,f.d9 are_congruent_mod p;
not f9.k in {f.d9} by A26,XBOOLE_0:def 5;
then w <> d9 by A28,TARSKI:def 1;
hence contradiction by A11,A21,A27,A29;
end;
A30: for d st d in dom f9 holds (Poly-INT fk).(f9.d) mod p = 0
proof
let d;
assume
A31: d in dom f9;
then f9.d in rng f9 by FUNCT_1:3;
then f9.d in rng f \ {f.d9} by FINSEQ_3:65;
then f9.d in rng f by XBOOLE_0:def 5;
then ex w being object st w in dom f & f.w = f9.d by FUNCT_1:def 3;
then p divides (f9.d -a)*(Poly-INT fk).(f9.d) by A17;
then p divides (f9.d -a) or p divides (Poly-INT fk).(f9.d) by Th7;
hence thesis by A23,A31;
end;
A32: f is one-to-one
by A11,INT_1:11;
then
A33: f9 is one-to-one by FINSEQ_3:87;
A34: for d,e st d in dom f9 & e in dom f9 & d<>e holds not f9.d,f9.e
are_congruent_mod p
proof
let d,e;
assume that
A35: d in dom f9 and
A36: e in dom f9 and
A37: d<>e;
f9.e in rng f9 by A36,FUNCT_1:3;
then f9.e in rng f \ {f.d9} by FINSEQ_3:65;
then f9.e in rng f by XBOOLE_0:def 5;
then consider w2 being object such that
A38: w2 in dom f and
A39: f9.e = f.w2 by FUNCT_1:def 3;
f9.d in rng f9 by A35,FUNCT_1:3;
then f9.d in rng f \ {f.d9} by FINSEQ_3:65;
then f9.d in rng f by XBOOLE_0:def 5;
then consider w1 being object such that
A40: w1 in dom f and
A41: f9.d = f.w1 by FUNCT_1:def 3;
reconsider w1,w2 as Element of NAT by A40,A38;
w1 <> w2 by A33,A35,A36,A37,A41,A39;
hence thesis by A11,A40,A41,A38,A39;
end;
f.d9 in rng f by A21,FUNCT_1:3;
then len f9 = len f - 1 by A32,FINSEQ_3:90;
then len f9 > (n+1)-1 by A12,XREAL_1:9;
hence contradiction by A2,A4,A5,A13,A15,A30,A34;
end;
end;
end;
A42: P[0]
proof
let fp;
assume that
A43: len fp = 0+1 and
p>2 and
A44: not p divides fp.(0+1);
assume ex fr st (for d st d in dom fr holds (Poly-INT fp).(fr.d) mod p=0)
& (for d,e st d in dom fr & e in dom fr & d<>e holds not fr.d,fr.e
are_congruent_mod p) & len fr > 0;
then consider fr such that
A45: for d st d in dom fr holds (Poly-INT fp).(fr.d) mod p=0 and
for d,e st d in dom fr & e in dom fr & d<>e holds not fr.d,fr.e
are_congruent_mod p and
A46: len fr > 0;
fr <> {} by A46;
then
A47: (Poly-INT fp).(fr.1) mod p=0 by A45,FINSEQ_5:6;
A48: fr.1 in INT by INT_1:def 2;
(Poly-INT fp).(fr.1) = (INT --> fp.1).(fr.1) by A43,Th3
.= fp.1 by A48,FUNCOP_1:7;
hence contradiction by A44,A47,Lm1;
end;
for n holds P[n] from NAT_1:sch 2(A42,A1);
hence thesis;
end;
definition
let a be Integer, m be natural Number;
pred a is_quadratic_residue_mod m means
ex x being Integer st (x^2 - a) mod m = 0;
end;
reserve b,m for Nat;
theorem Th9:
a^2 is_quadratic_residue_mod m
proof
(a^2 - a^2) mod m = 0 by INT_1:73;
hence thesis;
end;
theorem
1 is_quadratic_residue_mod 2
proof
1^2 is_quadratic_residue_mod 2 by Th9;
hence thesis;
end;
theorem Th11:
i is_quadratic_residue_mod m & i,j are_congruent_mod m implies
j is_quadratic_residue_mod m
proof
assume that
A1: i is_quadratic_residue_mod m and
A2: i,j are_congruent_mod m;
consider x being Integer such that
A3: (x^2 - i) mod m = 0 by A1;
A4: (i - j) mod m = 0 by A2;
(x^2 - j) mod m = ((x^2 - i) + (i - j)) mod m
.= (((x^2 - i) mod m) + ((i - j) mod m)) mod m by NAT_D:66
.= 0 by A3,A4,NAT_D:65;
hence thesis;
end;
Lm2: i,p are_coprime or p divides i
proof
per cases;
suppose
i>=0;
then reconsider i as Element of NAT by INT_1:3;
i,p are_coprime or (i gcd p) = p by PEPIN:2;
hence thesis by NAT_D:def 5;
end;
suppose
A1: i<0;
then reconsider m = -i as Element of NAT by INT_1:3;
A2: m,p are_coprime or (m gcd p) = p by PEPIN:2;
per cases by A2,NAT_D:def 5;
suppose
A3: m,p are_coprime;
m = |.i.| by A1,ABSVALUE:def 1;
then i gcd p = m gcd |.p.| by INT_2:34
.= m gcd p by ABSVALUE:def 1
.= 1 by A3,INT_2:def 3;
hence thesis by INT_2:def 3;
end;
suppose
p divides m;
then consider t being Nat such that
A4: m = p * t by NAT_D:def 3;
i = p * (-t) by A4;
hence thesis;
end;
end;
end;
theorem Th12:
i divides j implies i gcd j = |.i.|
proof
assume i divides j;
then |.i.| gcd |.j.| = |.i.| by NEWTON:49,INT_2:16;
hence thesis by INT_2:34;
end;
theorem Th13:
for i,j,m being Integer st i mod m = j mod m holds i|^n mod m = j|^n mod m
proof
let i,j,m be Integer;
defpred P[Nat] means i|^$1 mod m = j|^$1 mod m;
assume
A1: i mod m = j mod m;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A3: P[n];
thus i|^(n+1) mod m = ((i|^n)*i) mod m by NEWTON:6
.= (((j|^n) mod m)*(j mod m)) mod m by A1,A3,NAT_D:67
.= ((j|^n)*j) mod m by NAT_D:67
.= j|^(n+1) mod m by NEWTON:6;
end;
i|^0 = 1 by NEWTON:4;
then
A4: P[0] by NEWTON:4;
for n being Nat holds P[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem Th14:
a gcd p = 1 & (x^2 - a) mod p = 0 implies x,p are_coprime
proof
assume that
A1: a gcd p = 1 and
A2: (x^2 - a) mod p = 0;
assume not x,p are_coprime;
then
A3: p divides x^2 by Lm2,INT_2:2;
p divides (x^2 - a) by A2,Lm1;
then p divides (x^2 - (x^2 - a)) by A3,Th1;
then p gcd a = |.p.| by Th12
.= p by ABSVALUE:def 1;
hence contradiction by A1,INT_2:def 4;
end;
theorem
p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p implies ex x,y
being Integer st (x^2 - a) mod p = 0 & (y^2 - a) mod p = 0 & not x,y
are_congruent_mod p
proof
assume that
A1: p > 2 and
A2: a gcd p = 1 and
A3: a is_quadratic_residue_mod p;
consider x such that
A4: (x^2 - a) mod p = 0 by A3;
take x;
take -x;
not x,(-x) are_congruent_mod p
proof
assume x,(-x) are_congruent_mod p;
then
A5: p divides 2*x;
2,p are_coprime by A1,INT_2:28,30;
then 2 gcd p = 1 by INT_2:def 3;
then p divides x by A5,WSIERP_1:29;
then consider i being Integer such that
A6: x = p * i;
x gcd p = p*i gcd p*1 by A6
.= p*(i gcd 1) by EULER_1:15
.= p*1 by WSIERP_1:8;
then x gcd p <> 1 by INT_2:def 4;
then not x,p are_coprime by INT_2:def 3;
hence contradiction by A2,A4,Th14;
end;
hence thesis by A4;
end;
theorem Th16:
p>2 implies ex fp being FinSequence of NAT st len fp = (p-'1)
div 2 & (for d st d in dom fp holds fp.d gcd p = 1) & (for d st d in dom fp
holds fp.d is_quadratic_residue_mod p) & for d,e st d in dom fp & e in dom fp &
d<>e holds not fp.d,fp.e are_congruent_mod p
proof
deffunc F(Nat) = $1^2;
consider fp being FinSequence such that
A1: len fp = (p-'1) div 2 & for d being Nat st d in dom fp holds fp.d =
F(d) from FINSEQ_1:sch 2;
for d being Nat st d in dom fp holds fp.d in NAT
proof
let d be Nat;
assume d in dom fp;
then fp.d = d^2 by A1;
hence thesis;
end;
then reconsider fp as FinSequence of NAT by FINSEQ_2:12;
A2: p>1 by INT_2:def 4;
then
A3: p-'1 = p-1 by XREAL_1:233;
assume p > 2;
then p is odd by PEPIN:17;
then p-1 is even by HILBERT3:2;
then 2 divides (p-'1) by A3,PEPIN:22;
then (p-'1) mod 2 = 0;
then
A4: (p-'1) div 2 = (p-'1)/2 by PEPIN:63;
A5: for d,e st d in dom fp & e in dom fp & d<>e holds not fp.d,fp.e
are_congruent_mod p
proof
p-1>0 by A2,XREAL_1:50;
then (p-1)/2 < (p-1)/1 by XREAL_1:76;
then (p-'1) div 2 < p by A3,A4,XREAL_1:147;
then
A6: ((p-'1) div 2) - 1 < p by XREAL_1:147;
let d,e;
assume that
A7: d in dom fp and
A8: e in dom fp and
A9: d<>e;
A10: e in Seg ((p-'1) div 2) by A1,A8,FINSEQ_1:def 3;
then
A11: e <= (p-'1) div 2 by FINSEQ_1:1;
A12: d in Seg ((p-'1) div 2) by A1,A7,FINSEQ_1:def 3;
then
A13: d >= 1 by FINSEQ_1:1;
then 1-((p-'1) div 2) <= d-e by A11,XREAL_1:13;
then
A14: -(((p-'1) div 2) - 1) <= d-e;
A15: d <= (p-'1) div 2 by A12,FINSEQ_1:1;
then d+e <= (p-'1) div 2 + ((p-'1) div 2) by A11,XREAL_1:7;
then d+e < p by A3,A4,XREAL_1:147;
then (d+e),p are_coprime by A13,EULER_1:2;
then
A16: (d+e) gcd p = 1 by INT_2:def 3;
assume fp.d,fp.e are_congruent_mod p;
then p divides (d^2 - fp.e) by A1,A7;
then p divides (d^2 - e^2) by A1,A8;
then
A17: p divides (d - e)*(d+e);
d-e <> 0 by A9;
then |.p.| <= |.d-e.| by A16,A17,INT_4:6,WSIERP_1:29;
then
A18: p <= |.d-e.| by ABSVALUE:def 1;
e >= 1 by A10,FINSEQ_1:1;
then d-e <= ((p-'1) div 2) - 1 by A15,XREAL_1:13;
then |.d-e.| <= ((p-'1) div 2) - 1 by A14,ABSVALUE:5;
hence contradiction by A18,A6,XXREAL_0:2;
end;
A19: for d st d in dom fp holds d gcd p = 1
proof
let d;
A20: 1*d <= 2*d by XREAL_1:64;
assume d in dom fp;
then
A21: d in Seg ((p-'1) div 2) by A1,FINSEQ_1:def 3;
then d <= (p-'1) div 2 by FINSEQ_1:1;
then 2*d <= (p-'1)/2*2 by A4,XREAL_1:64;
then d <= p-'1 by A20,XXREAL_0:2;
then
A22: d < p by A3,XREAL_1:147;
d >= 1 by A21,FINSEQ_1:1;
then d,p are_coprime by A22,EULER_1:2;
hence thesis by INT_2:def 3;
end;
A23: for d st d in dom fp holds fp.d gcd p = 1
proof
let d;
assume
A24: d in dom fp;
then d gcd p = 1 by A19;
then d^2 gcd p = 1 by WSIERP_1:7;
hence thesis by A1,A24;
end;
take fp;
for d st d in dom fp holds fp.d is_quadratic_residue_mod p
proof
let d;
assume
A25: d in dom fp;
d^2 is_quadratic_residue_mod p by Th9;
hence thesis by A1,A25;
end;
hence thesis by A1,A23,A5;
end;
::Euler Criterion
theorem Th17:
p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p implies
a|^((p-'1) div 2) mod p = 1
proof
assume that
A1: p > 2 and
A2: a gcd p = 1 and
A3: a is_quadratic_residue_mod p;
consider s being Integer such that
A4: (s^2 - a) mod p = 0 by A3;
A5: p>1 by INT_2:def 4;
p is odd by A1,PEPIN:17;
then p-1 is even by HILBERT3:2;
then p-'1 is even by A5,XREAL_1:233;
then 2 divides (p-'1) by PEPIN:22;
then
A6: p-'1 = 2*((p-'1) div 2);
s^2,a are_congruent_mod p by A4,INT_1:62;
then a mod p = s^2 mod p by NAT_D:64;
then
A7: a|^((p-'1) div 2) mod p = (s^2)|^((p-'1) div 2) mod p by Th13
.= (s|^2)|^((p-'1) div 2) mod p by NEWTON:81
.= s|^(p-'1) mod p by A6,NEWTON:9;
A8: s,p are_coprime by A2,A4,Th14;
per cases;
suppose
s>=0;
then reconsider s as Element of NAT by INT_1:3;
s,p are_coprime by A2,A4,Th14;
hence thesis by A7,PEPIN:37;
end;
suppose
A9: s<0;
then reconsider s9 = -s as Element of NAT by INT_1:3;
A10: |.p.| = p by ABSVALUE:def 1;
s9 gcd p = |.s.| gcd p by A9,ABSVALUE:def 1
.= s gcd p by A10,INT_2:34
.= 1 by A8,INT_2:def 3;
then s9,p are_coprime by INT_2:def 3;
then
A11: s9|^(p-'1) mod p = 1 by PEPIN:37;
s|^(p-'1) mod p = (s|^2)|^((p-'1) div 2) mod p by A6,NEWTON:9
.= ((-s)|^2)|^((p-'1) div 2) mod p by WSIERP_1:1
.= 1 by A6,A11,NEWTON:9;
hence thesis by A7;
end;
end;
theorem Th18:
p>2 & b gcd p = 1 & not b is_quadratic_residue_mod p implies
b|^((p-'1) div 2) mod p = p - 1
proof
assume that
A1: p>2 and
A2: b gcd p = 1 and
A3: not b is_quadratic_residue_mod p;
reconsider b as Element of NAT by ORDINAL1:def 12;
A4: p>1 by INT_2:def 4;
then
A5: 1 mod p = 1 by NAT_D:14;
p is odd by A1,PEPIN:17;
then p-1 is even by HILBERT3:2;
then p-'1 is even by A4,XREAL_1:233;
then 2 divides (p-'1) by PEPIN:22;
then p-'1 = 2*((p-'1) div 2);
then
A6: b|^(p-'1) - 1 = (b|^((p-'1) div 2))|^2 - 1 by NEWTON:9
.= (b|^((p-'1) div 2))^2 - 1 by NEWTON:81
.= (b|^((p-'1) div 2) +1)*(b|^((p-'1) div 2)-1);
b,p are_coprime by A2,INT_2:def 3;
then (b|^(p-'1)) mod p = 1 by PEPIN:37;
then (b|^(p-'1) - 1) mod p = 0 by A5,INT_4:22;
then
A7: p divides (b|^((p-'1) div 2) +1)*(b|^((p-'1) div 2)-1) by A6,Lm1;
p-1 > 2-1 by A1,XREAL_1:9;
then p-1 >= 1 + 1 by INT_1:7;
then p-'1 >= 2 by A4,XREAL_1:233;
then (p-'1) div 2 >= 2 div 2 by NAT_2:24;then
A8: (p-'1) div 2 >= 1;
per cases by A8,XXREAL_0:1;
suppose
A9: (p-'1) div 2 = 1;
A10: now
assume p divides (b - 1);
then p divides -(b - 1) by INT_2:10;
then (1^2 - b) mod p = 0;
hence contradiction by A3;
end;
p divides (b +1)*(b|^1 -1) by A7,A9;
then p divides (b - (-1)) by A10,Th7;
then b,(-1) are_congruent_mod p;
then
A11: b mod p = (-1) mod p by NAT_D:64;
-p < -2 by A1,XREAL_1:24;
then -p < -2+1 by XREAL_1:39;
then b mod p = p - 1 by A11,NAT_D:63;
hence thesis by A9;
end;
suppose
A12: (p-'1) div 2 > 1;
set l = (p-'1) div 2;
set K1 = <*-1*>^((l-'1) |-> 0);
A14: len ((l-'1) |-> 0) = l-'1 by CARD_1:def 7;
A15: len K1 = 1 + (l-'1) by CARD_1:def 7
.= l by A12,XREAL_1:235;
set fs = <*-1*>^((l-'1) |-> 0)^<*1*>;
reconsider fs as FinSequence of INT by FINSEQ_1:75;
A17: len fs = 1 + ((l-'1) +1) by CARD_1:def 7
.= 1 + l by A12,XREAL_1:235;
A18: fs.1 = (<*-1*>^(((l-'1) |-> 0)^<*1*>)).1 by FINSEQ_1:32
.= -1 by FINSEQ_1:41;
A19: for x being Element of INT holds (Poly-INT fs).x = x|^l -1
proof
let x be Element of INT;
consider fr such that
A20: len fr = len fs and
A21: for d st d in dom fr holds fr.d = (fs.d) * x|^(d-'1) and
A22: (Poly-INT fs).x = Sum fr by Def1;
fr = <*-1*>^((l-'1) |-> 0)^<*x|^l*>
proof
set K = <*-1*>^((l-'1) |-> 0)^<*x|^l*>;
A23: for d being Nat st d in dom fr holds fr.d = K.d
proof
let d be Nat;
assume
A24: d in dom fr; then
A25: d in Seg(l + 1) by A17,A20,FINSEQ_1:def 3; then
A26: d>=1 by FINSEQ_1:1;
A27: d<=l+1 by A25,FINSEQ_1:1;
per cases by A26,A27,XXREAL_0:1;
suppose
A28: d=1; then
A29: fr.1 = (fs.1) * x|^(1-'1) by A21,A24
.= (fs.1) * x|^0 by XREAL_1:232
.= (fs.1) * 1 by NEWTON:4
.= -1 by A18;
K.1 = (<*-1*>^(((l-'1) |-> 0)^<*x|^l*>)).1 by FINSEQ_1:32
.= fr.1 by A29,FINSEQ_1:41;
hence thesis by A28;
end;
suppose
A30: d>1 & d<l+1;
then reconsider w = d-1 as Element of NAT by INT_1:3;
d-1<l+1-1 by A30,XREAL_1:9; then
A31: w <= l-'1 by NAT_D:49;
A32: w >= 0+1 by A30,INT_1:7,XREAL_1:50;
A33: ((l-'1) |-> 0).w = 0;
w in Seg(l-'1) by A31,A32,FINSEQ_1:1; then
A34: w in dom ((l-'1) |-> 0) by A14,FINSEQ_1:def 3; then
A35: w in dom (((l-'1) |-> 0)^<*1*>) by FINSEQ_2:15;
A36: w in dom (((l-'1) |-> 0)^<*x|^l*>) by A34,FINSEQ_2:15;
A37: fs.d = (<*-1*>^(((l-'1) |-> 0)^<*1*>)).(w+1) by FINSEQ_1:32
.= (((l-'1) |-> 0)^<*1*>).w by A35,FINSEQ_3:103
.= 0 by A33,A34,FINSEQ_1:def 7;
thus K.d = (<*-1*>^(((l-'1) |-> 0)^<*x|^l*>)).(w+1) by FINSEQ_1:32
.= (((l-'1) |-> 0)^<*x|^l*>).w by A36,FINSEQ_3:103
.= (fs.d)*x|^(d-'1) by A33,A34,A37,FINSEQ_1:def 7
.= fr.d by A21,A24;
end;
suppose
A38: d=l+1;
then d in dom fs by A17,FINSEQ_5:6;
then
A39: d in dom fr by A20,FINSEQ_3:29;
fs.d = 1 by A15,A38,FINSEQ_1:42;
hence fr.d = 1 * x|^(l+1-'1) by A21,A38,A39
.= x|^l by NAT_D:34
.= K.d by A15,A38,FINSEQ_1:42;
end;
end;
len K = 1 + ((l-'1) +1) by CARD_1:def 7
.= len fr by A12,A17,A20,XREAL_1:235;
hence thesis by A23,FINSEQ_3:29;
end;
then Sum fr = Sum (<*-1*>^(((l-'1) |-> 0)^<*x|^l*>)) by FINSEQ_1:32
.= -1 + Sum (((l-'1) |-> 0)^<*x|^l*>) by RVSUM_1:76
.= -1 + (Sum ((l-'1) |-> 0) + x|^l) by RVSUM_1:74
.= -1 + ((l-'1)*0 + x|^l) by RVSUM_1:80;
hence thesis by A22;
end;
consider fp being FinSequence of NAT such that
A40: len fp = l and
A41: for d st d in dom fp holds fp.d gcd p = 1 and
A42: for d st d in dom fp holds fp.d is_quadratic_residue_mod p and
A43: for d,e st d in dom fp & e in dom fp & d<>e holds not fp.d,fp.e
are_congruent_mod p by A1,Th16;
A44: fs.(l+1) = 1 by A15,FINSEQ_1:42;
now
assume p divides (b|^l - 1);
then
A45: (b|^l - 1) mod p = 0;
reconsider b as Element of INT by INT_1:def 2;
set f = fp^<*b*>;
reconsider f as FinSequence of NAT by FINSEQ_1:75;
A46: len f = l+1 by A40,FINSEQ_2:16;
A47: for d,e st d in dom f & e in dom f & d<>e holds not f.d,f.e
are_congruent_mod p
proof
let d,e;
assume that
A48: d in dom f and
A49: e in dom f and
A50: d<>e;
A51: e>=1 by A49,FINSEQ_3:25;
A52: d<= l+1 by A46,A48,FINSEQ_3:25;
A53: e<=l+1 by A46,A49,FINSEQ_3:25;
per cases by A48,A52,FINSEQ_3:25,XXREAL_0:1;
suppose
A54: d>=1 & d<l+1;
then d<=l by NAT_1:13;
then
A55: d in dom fp by A40,A54,FINSEQ_3:25;
then
A56: f.d = fp.d by FINSEQ_1:def 7;
per cases by A49,A53,FINSEQ_3:25,XXREAL_0:1;
suppose
A57: e>=1 & e<l+1;
then e<=l by NAT_1:13;
then
A58: e in dom fp by A40,A57,FINSEQ_3:25;
then not fp.d,fp.e are_congruent_mod p by A43,A50,A55;
hence thesis by A56,A58,FINSEQ_1:def 7;
end;
suppose
A59: e=l+1;
not f.d,b are_congruent_mod p
proof
f.d is_quadratic_residue_mod p by A42,A55,A56;
then consider j being Integer such that
A60: (j^2 - f.d) mod p = 0;
assume a61: f.d,b are_congruent_mod p;
p divides (j^2 - f.d) by A60,INT_1:62;
then p divides ((j^2 - f.d)+(f.d - b)) by a61,WSIERP_1:4;
then (j^2 - b) mod p = 0;
hence contradiction by A3;
end;
hence thesis by A40,A59,FINSEQ_1:42;
end;
end;
suppose
A62: d=l+1;
then e<=l by A50,A53,NAT_1:8;
then
A63: e in dom fp by A40,A51,FINSEQ_3:25;
then f.e = fp.e by FINSEQ_1:def 7;
then f.e is_quadratic_residue_mod p by A42,A63;
then consider j being Integer such that
A64: (j^2 - f.e) mod p = 0;
A65: p divides (j^2 - f.e) by A64,INT_1:62;
not b,f.e are_congruent_mod p
proof
assume b,f.e are_congruent_mod p;
then p divides ((j^2 - f.e) - (b - f.e)) by A65,Th1;
then (j^2 - b) mod p = 0;
hence contradiction by A3;
end;
hence thesis by A40,A62,FINSEQ_1:42;
end;
end;
A66: (Poly-INT fs).b mod p = 0 by A19,A45;
A67: for d st d in dom f holds (Poly-INT fs).(f.d) mod p = 0
proof
let d;
assume d in dom f;
then
A68: d in Seg (l+1) by A46,FINSEQ_1:def 3;
then
A69: d<=l+1 by FINSEQ_1:1;
per cases by A68,A69,FINSEQ_1:1,XXREAL_0:1;
suppose
A70: d>=1 & d<l+1;
reconsider k = fp.d as Element of INT by INT_1:def 2;
d<=l by A70,NAT_1:13; then
A71: d in dom fp by A40,A70,FINSEQ_3:25;
then fp.d gcd p = 1 by A41;
then (fp.d)|^l mod p = 1 mod p by A1,A5,A42,A71,Th17;
then (k|^l - 1) mod p = 0 by INT_4:22;
then (Poly-INT fs).k mod p = 0 by A19;
hence thesis by A71,FINSEQ_1:def 7;
end;
suppose
d=l+1;
hence thesis by A40,A66,FINSEQ_1:42;
end;
end;
reconsider f as FinSequence of INT by FINSEQ_2:24,NUMBERS:17;
not p divides fs.(l+1) by A4,A44,NAT_D:7;
then len f <= l by A1,A17,A67,A47,Th8;
hence contradiction by A46,XREAL_1:29;
end;
then p divides (b|^l + 1) by A7,Th7;
then consider k being Nat such that
A72: (b|^l + 1) = p*k by NAT_D:def 3;
-p < -1 by A4,XREAL_1:24;
then
A73: (-1) mod p = (-1) + p by NAT_D:63;
b|^l mod p = (p*k + (- 1)) mod p by A72
.= p - 1 by A73,NAT_D:61;
hence thesis;
end;
end;
theorem Th19:
p>2 & a gcd p = 1 & not a is_quadratic_residue_mod p implies
a|^((p-'1) div 2) mod p = p - 1
proof
assume that
A1: p>2 and
A2: a gcd p = 1 and
A3: not a is_quadratic_residue_mod p;
set l = a mod p;
reconsider l as Element of NAT by INT_1:3;
A4: l mod p = a mod p by NAT_D:65;
then
A5: l,a are_congruent_mod p by NAT_D:64;
then l gcd p = 1 by A2,WSIERP_1:43;
then l|^((p-'1) div 2) mod p = p - 1 by A1,A3,A5,Th11,Th18;
hence thesis by A4,Th13;
end;
theorem Th20:
p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p implies (a|^(
(p-'1) div 2) - 1) mod p = 0
proof
assume that
A1: p > 2 and
A2: a gcd p = 1 and
A3: a is_quadratic_residue_mod p;
A4: p>1 by INT_2:def 4;
a|^((p-'1) div 2) mod p = 1 by A1,A2,A3,Th17;
then a|^((p-'1) div 2) mod p = 1 mod p by A4,NAT_D:14;
then a|^((p-'1) div 2),1 are_congruent_mod p by NAT_D:64;
hence thesis;
end;
theorem Th21:
p > 2 & a gcd p = 1 & not a is_quadratic_residue_mod p implies
(a|^((p-'1) div 2) + 1) mod p = 0
proof
assume that
A1: p > 2 and
A2: a gcd p = 1 and
A3: not a is_quadratic_residue_mod p;
A4: p-1<p by XREAL_1:146;
a|^((p-'1) div 2) mod p = p-1 by A1,A2,A3,Th19;
then a|^((p-'1) div 2) mod p = (p-1) mod p by A4,NAT_D:63;
then a|^((p-'1) div 2),(p-1) are_congruent_mod p by NAT_D:64;
then p divides -((a|^((p-'1) div 2)+1) - p) by INT_2:10;
then p divides (p-(a|^((p-'1) div 2)+1));
then p divides (a|^((p-'1) div 2)+1) by Th2;
hence thesis;
end;
reserve b for Integer;
theorem
a is_quadratic_residue_mod p & b is_quadratic_residue_mod p implies
a*b is_quadratic_residue_mod p
proof
assume that
A1: a is_quadratic_residue_mod p and
A2: b is_quadratic_residue_mod p;
consider i being Integer such that
A3: (i^2 - a) mod p =0 by A1;
consider j being Integer such that
A4: (j^2 - b) mod p =0 by A2;
A5: j^2,b are_congruent_mod p by A4,INT_1:62;
i^2,a are_congruent_mod p by A3,INT_1:62;
then (i^2)*(j^2),a*b are_congruent_mod p by A5,INT_1:18;
then ((i*j)^2 - a*b) mod p = 0;
hence thesis;
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 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; then
not p divides a^2 by Th7; then
a^2 mod p <> 0 by INT_1:62;
hence thesis by Def3,Th9;
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,WSIERP_1:43;
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 = 1 by WSIERP_1:15,A6,A9,INT_2:10;
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 = 1 by WSIERP_1:15,A6,A11,INT_2:10;
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;
hence thesis by A2,WSIERP_1:7;
end;
suppose
k = 2;
hence thesis by A3;
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);
fr.1 = Lege(fp.1,p) by A7,A9,FINSEQ_3:25;
then fr.1 = Lege(d^2,p);
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.| 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))
.= ((-1)|^2)|^(p div 4) by NEWTON:9
.= (1|^2)|^(p div 4) by WSIERP_1:1
.= 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)
.= (-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 *(-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<n+1;
then d<=n by NAT_1:13;
then d in Seg n by A26,FINSEQ_1:1;
then
A27: d in dom f1 by A3,A11,FINSEQ_1:def 3;
then f1.d <> n+1 by A20;
then
A28: f.d <> n+1 by A9,A27,FINSEQ_1:def 7;
f.d <=n+1 by A4,A21;
then f.d <n+1 by A28,XXREAL_0:1;
then
A29: f.d<=n by NAT_1:13;
f.d>0 by A4,A21;
then f.d>=0+1 by NAT_1:13;
hence thesis by A29,FINSEQ_1:1;
end;
end;
then f is FinSequence of Seg n by FINSEQ_2:12;
then rng f c= Seg n by FINSEQ_1:def 4;
then card rng f <= card Seg n by NAT_1:43;
then n+1 <= card Seg n by A3,A5,FINSEQ_4:62;
then n+1 <= n+0 by FINSEQ_1:57;
hence contradiction by XREAL_1:6;
end;
then consider d1 being Element of NAT such that
A30: d1 in dom f1 and
A31: f1.d1 = n+1;
d1<=n by A3,A11,A30,FINSEQ_3:25;
then
A32: d1 <= len f by A3,NAT_1:13;
A33: 0+1 <= n+1 by XREAL_1:6;
set f2 = Swap(f,d1,n+1);
A34: len f2 = n+1 by A3,FINSEQ_7:18;
then
A35: f2 <> {};
then consider
f3 being FinSequence of NAT,b being Element of NAT such that
A36: f2 = f3^<*b*> by HILBERT2:4;
A37: n+1 = len f3 +1 by A34,A36,FINSEQ_2:16;
A38: 1 <= d1 by A30,FINSEQ_3:25;
then f2/.(n+1) = f/.d1 by A3,A32,A33,FINSEQ_7:31;
then f2/.(n+1) = f.d1 by A38,A32,FINSEQ_4:15;
then f2.(n+1) = f.d1 by A34,A33,FINSEQ_4:15;
then
A39: f2.(n+1) = n+1 by A9,A30,A31,FINSEQ_1:def 7;
then
A40: b = n+1 by A36,A37,FINSEQ_1:42;
A41: f2 is one-to-one by A5,Th39;
A42: for d st d in dom f3 holds f3.d>0 & f3.d<=n
proof
let d;
assume
A43: d in dom f3;
then
A44: d in dom f2 by A36,FINSEQ_2:15;
A45: now
d<=n by A37,A43,FINSEQ_3:25;
then
A46: d < n+1 by XREAL_1:145;
assume f3.d=n+1;
then
A47: f2.d = n+1 by A36,A43,FINSEQ_1:def 7;
n+1 in dom f2 by A34,A35,FINSEQ_5:6;
hence contradiction by A39,A41,A44,A47,A46;
end;
f2.d in rng f2 by A44,FUNCT_1:3;
then f2.d in rng f by FINSEQ_7:22;
then
A48: ex e being Nat st e in dom f & f2.d = f.e by FINSEQ_2:10;
then f2.d<=n+1 by A4;
then f3.d<=n+1 by A36,A43,FINSEQ_1:def 7;
then
A49: f3.d<n+1 by A45,XXREAL_0:1;
f2.d >0 by A4,A48;
hence thesis by A36,A43,A49,FINSEQ_1:def 7,NAT_1:13;
end;
f3 is one-to-one by A36,A41,FINSEQ_3:91;
then
A50: rng f3 = Seg n by A2,A37,A42;
rng f2 = rng f3 \/ rng <*b*> by A36,FINSEQ_1:31
.= Seg n \/ {n+1} by A40,A50,FINSEQ_1:38
.= Seg (n+1) by FINSEQ_1:9;
hence thesis by FINSEQ_7:22;
end;
end;
hence thesis;
end;
A51: P[0]
proof
let f be FinSequence of NAT;
assume len f = 0;
then f = {};
hence thesis;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A51,A1);
hence thesis;
end;
reserve a,m for Nat;
theorem Th41:
for f be FinSequence of NAT st p>2 & a gcd p = 1 & f = a*(idseq
((p-'1) div 2)) & m=card{k where k is Element of NAT:k in rng (f mod p) & k > p
/2} holds Lege(a,p) = (-1)|^m
proof
let f be FinSequence of NAT;
assume that
A1: p>2 and
A2: a gcd p = 1 and
A3: f = a*(idseq ((p-'1) div 2)) and
A4: m=card{k where k is Element of NAT:k in rng (f mod p) & k > p/2};
set f1 = f mod p;
A5: len f1 = len f by EULER_2:def 2;
set X = {k where k is Element of NAT:k in rng f1 & k > p/2};
for x being object st x in X holds x in rng f1
proof
let x be object;
assume x in X;
then ex k being Element of NAT st x = k & k in rng f1 & k > p/2;
hence thesis;
end;
then
A6: X c= rng f1;
then reconsider X as finite set;
reconsider X as finite Subset of NAT by A6,XBOOLE_1:1;
card X is Element of NAT;
then reconsider m as Element of NAT by A4;
A7: rng f1 \ X c= rng f1 by XBOOLE_1:36;
reconsider Y = rng f1 \ X as finite Subset of NAT;
A8: a|^((p-'1) div 2),Lege(a,p) are_congruent_mod p by A1,A2,Th28,INT_1:14;
set f2 = Sgm rng f1;
(Product f1) mod p = (Product f) mod p by EULER_2:11;
then
A9: Product f1,Product f are_congruent_mod p by NAT_D:64;
A10: p>1 by INT_2:def 4;
then
A11: p-'1 = p-1 by XREAL_1:233;
then
A12: p-'1>0 by A10,XREAL_1:50;
set p9 = (p-'1) div 2;
rng idseq p9 = Seg p9;
then reconsider I = idseq p9 as FinSequence of NAT by FINSEQ_1:def 4;
dom f = dom I by A3,VALUED_1:def 5;
then
A13: len f = len I by FINSEQ_3:29
.= p9 by CARD_1:def 7;
p >= 2+1 by A1,NAT_1:13;
then p-1 >= 3-1 by XREAL_1:9;
then f1 <> {} by A13,A11,A5,NAT_2:13;
then rng f1 is non empty Subset of NAT;
then consider n1 being Element of NAT such that
A14: rng f1 c= Seg n1 \/ {0} by HEYTING3:1;
I is Element of p9-tuples_on REAL by FINSEQ_2:109,NUMBERS:19;
then
A15: Product f = (Product (p9|->a))*(Product I) by A3,RVSUM_1:108
.= (a|^p9) * (Product I) by NEWTON:def 1;
p is odd by A1,PEPIN:17;
then
A16: p-'1 is even by A11,HILBERT3:2;
then
A17: p9 = ((p-'1)+1) div 2 by NAT_2:26
.= p div 2 by A10,XREAL_1:235;
2 divides (p-'1) by A16,PEPIN:22;
then
A18: p-'1 = 2*p9;
then p9 divides (p-'1);
then p9 <= (p-'1) by A12,NAT_D:7;
then
A19: p9 < p by A11,XREAL_1:146,XXREAL_0:2;
for d being Nat st d in dom I holds I.d gcd p = 1
proof
let d be Nat;
assume d in dom I;
then
A20: d in Seg len I by FINSEQ_1:def 3;
then
A21: d in Seg p9 by CARD_1:def 7;
then
A22: I.d = d by FINSEQ_2:49;
d <= p9 by A21,FINSEQ_1:1;
then
A23: d < p by A19,XXREAL_0:2;
d >= 1 by A20,FINSEQ_1:1;
then d,p are_coprime by A23,EULER_1:2;
hence thesis by A22,INT_2:def 3;
end;
then
A24: (Product I) gcd p = 1 by WSIERP_1:36;
A25: for d st d in dom f holds f.d = a*d
proof
let d;
assume
A26: d in dom f;
then d in dom I by A3,VALUED_1:def 5;
then d in Seg len I by FINSEQ_1:def 3;
then
A27: d is Element of Seg p9 by CARD_1:def 7;
thus f.d = a * I.d by A3,A26,VALUED_1:def 5
.= a*d by A27;
end;
A28: for d,e being Nat st 1<=d & d<e & e<=len f1 holds f1.d <> f1 .e
proof
let d,e be Nat;
assume that
A29: 1<=d and
A30: d<e and
A31: e<=len f1;
A32: e<=len f by A31,EULER_2:def 2;
1<=e by A29,A30,XXREAL_0:2;
then
A33: e in dom f by A32,FINSEQ_3:25;
then
A34: f1.e = (f.e) mod p by EULER_2:def 2;
d<len f by A30,A32,XXREAL_0:2;
then
A35: d in dom f by A29,FINSEQ_3:25;
then
A36: f1.d = (f.d) mod p by EULER_2:def 2;
now
assume f1.d = f1.e;
then f.e,f.d are_congruent_mod p by A36,A34,NAT_D:64;
then p divides (a*e - f.d) by A25,A33;
then p divides (a*e - a*d) by A25,A35;
then
A37: p divides a*(e-d);
A38: p9-1<p by A19,XREAL_1:147;
reconsider dd = e-d as Element of NAT by A30,NAT_1:21;
A39: |.p.| = p by ABSVALUE:def 1;
A40: |.dd.| = dd by ABSVALUE:def 1;
A41: dd <= p9 - 1 by A13,A5,A29,A31,XREAL_1:13;
dd <> 0 by A30;
then p <= dd by A2,A37,A39,A40,INT_4:6,WSIERP_1:29;
hence contradiction by A41,A38,XXREAL_0:2;
end;
hence thesis;
end;
then
A42: len f1 = card rng f1 by GRAPH_5:7;
then
A43: f1 is one-to-one by FINSEQ_4:62;
A44: dom f1 = dom f by A5,FINSEQ_3:29;
not 0 in rng f1
proof
reconsider a as Element of NAT by ORDINAL1:def 12;
assume 0 in rng f1;
then consider n be Nat such that
A45: n in dom f1 and
A46: f1.n = 0 by FINSEQ_2:10;
0 = (f.n) mod p by A44,A45,A46,EULER_2:def 2
.= (a*n) mod p by A25,A44,A45;
then
A47: p divides (a*n) by PEPIN:6;
n >= 1 by A45,FINSEQ_3:25;
then
A48: p <= n by A2,A47,NAT_D:7,WSIERP_1:30;
n <= p9 by A13,A5,A45,FINSEQ_3:25;
hence contradiction by A19,A48,XXREAL_0:2;
end;
then
A49: {0} misses rng f1 by ZFMISC_1:50;
then rng f1 c= Seg n1 by A14,XBOOLE_1:73;
then
ppp: rng f1 is included_in_Seg by FINSEQ_1:def 13;
then
A50: f2 is one-to-one by FINSEQ_3:92;
A51: rng f1 c= Seg n1 by A14,A49,XBOOLE_1:73;
then X c= Seg n1 by A6;
then
a52: X is included_in_Seg by FINSEQ_1:def 13;
len f = card rng f1 by A5,A28,GRAPH_5:7;
then reconsider n = p9 - m as Element of NAT by A4,A13,A6,NAT_1:21,43;
Y c= Seg n1 by A51,A7;
then
a53: Y is included_in_Seg by FINSEQ_1:def 13;
rng f1 is included_in_Seg by A51,FINSEQ_1:def 13;
then
A54: rng f1 = rng f2 by FINSEQ_1:def 14;
then
A55: Product f1 = Product f2 by A43,A50,EULER_2:10,RFINSEQ:26;
set f3 = (len (f2/^n) |-> p) - (f2/^n);
set f4 = (f2|n) ^ f3;
A56: f2/^n is FinSequence of INT by FINSEQ_2:24,NUMBERS:17;
A57: dom f3 = dom(len (f2/^n) |-> p)/\dom(f2/^n) by VALUED_1:12
.= (Seg len (len(f2/^n) |-> p))/\dom(f2/^n) by FINSEQ_1:def 3
.= dom(f2/^n) /\ dom(f2/^n) by FINSEQ_1:def 3,CARD_1:def 7
.= dom(f2/^n);
then
A58: len f3 = len(f2/^n) by FINSEQ_3:29;
for k,l being Nat st k in Y & l in X holds k < l
proof
let k,l be Nat;
assume that
A59: k in Y and
A60: l in X;
A61: not k in X by A59,XBOOLE_0:def 5;
A62: ex l1 being Element of NAT st l1 = l & l1 in rng f1 & l1>p/2 by A60;
k in rng f1 by A59,XBOOLE_0:def 5;
then k <= p/2 by A61;
hence thesis by A62,XXREAL_0:2;
end;
then Sgm (Y\/X) = (Sgm Y)^(Sgm X) by a52,a53,FINSEQ_3:42;
then Sgm (rng f1 \/ X) = (Sgm Y)^(Sgm X) by XBOOLE_1:39;
then
A63: f2 = (Sgm Y)^(Sgm X) by A6,XBOOLE_1:12;
A64: for d st d in dom f3 holds f3.d = p - (f2/^n).d
proof
let d;
assume
A65: d in dom f3;
then d in Seg len(f2/^n) by A57,FINSEQ_1:def 3;
then (len (f2/^n) |-> p).d = p by FINSEQ_2:57;
hence thesis by A65,VALUED_1:13;
end;
A66: len Sgm Y = card Y by a53,FINSEQ_3:39
.= p9 - m by A4,A13,A5,A6,A42,CARD_2:44;
then
A67: f2/^n = Sgm X by A63,FINSEQ_5:37;
A68: for d st d in dom f3 holds f3.d > 0 & f3.d <= p9
proof
let d;
reconsider w = f3.d as Element of INT by INT_1:def 2;
assume
A69: d in dom f3;
then (Sgm X).d in rng Sgm X by A67,A57,FUNCT_1:3;
then (Sgm X).d in X by a52,FINSEQ_1:def 14;
then
A70: ex ll be Element of NAT st ll = (Sgm X).d & ll in rng f1 & ll > p/2;
then consider e being Nat such that
A71: e in dom f1 and
A72: f1.e = (f2/^n).d by A67,FINSEQ_2:10;
(f2/^n).d = f.e mod p by A44,A71,A72,EULER_2:def 2;
then
A73: (f2/^n).d < p by NAT_D:1;
A74: f3.d = p - (f2/^n).d by A64,A69;
then w < p - p/2 by A67,A70,XREAL_1:10;
hence thesis by A17,A74,A73,INT_1:54,XREAL_1:50;
end;
for d being Nat st d in dom f3 holds f3.d in NAT
proof
let d be Nat;
assume
A76: d in dom f3;
f3.d > 0 by A68,A76;
hence thesis by INT_1:3;
end;
then reconsider f3 as FinSequence of NAT by FINSEQ_2:12;
|.(-1)|^m.| = 1 by SERIES_2:1;
then
A77: (-1)|^m = 1 or -((-1)|^m) = 1 by ABSVALUE:1;
f3 is FinSequence of NAT;
then reconsider f4 as FinSequence of NAT by FINSEQ_1:75;
A78: f2|n = Sgm Y by A63,A66,FINSEQ_3:113,FINSEQ_6:10;
A79: for d st d in dom f4 holds f4.d>0 & f4.d <= p9
proof
let d;
assume
A80: d in dom f4;
per cases by A80,FINSEQ_1:25;
suppose
A81: d in dom(f2|n);
reconsider d as Element of NAT by ORDINAL1:def 12;
(f2|n).d in rng Sgm Y by A78,A81,FUNCT_1:3;
then
A82: (f2|n).d in Y by a53,FINSEQ_1:def 14;
then
A83: (f2|n).d in rng f1 by XBOOLE_0:def 5;
not (f2|n).d in X by A82,XBOOLE_0:def 5;
then (f2|n).d <= p/2 by A83;
then
A84: (f2|n).d <= p9 by A17,INT_1:54;
not (f2|n).d in {0} by A49,A83,XBOOLE_0:3;
then (f2|n).d <> 0 by TARSKI:def 1;
hence thesis by A81,A84,FINSEQ_1:def 7;
end;
suppose
ex l being Nat st l in dom f3 & d=len(f2|n)+ l;
then consider l be Element of NAT such that
A85: l in dom f3 and
A86: d = len(f2|n)+ l;
f4.d = f3.l by A85,A86,FINSEQ_1:def 7;
hence thesis by A68,A85;
end;
end;
A87: f2 = (f2|n)^(f2/^n) by RFINSEQ:8;
then
A88: f2/^n is one-to-one by A50,FINSEQ_3:91;
for d,e being Nat st 1<=d & d<e & e<=len f3 holds f3.d <> f3.e
proof
let d,e be Nat;
assume that
A89: 1<=d and
A90: d<e and
A91: e<=len f3;
1<=e by A89,A90,XXREAL_0:2;
then
A92: e in dom f3 by A91,FINSEQ_3:25;
then
A93: f3.e = p - (f2/^n).e by A64;
d<len f3 by A90,A91,XXREAL_0:2;
then
A94: d in dom f3 by A89,FINSEQ_3:25;
then f3.d = p - (f2/^n).d by A64;
hence thesis by A88,A57,A90,A94,A92,A93;
end;
then len f3 = card rng f3 by GRAPH_5:7;
then
A95: f3 is one-to-one by FINSEQ_4:62;
A96: len f2 = p9 by ppp,A13,A5,A42,FINSEQ_3:39;
then
A97: n <= len f2 by XREAL_1:43;
A98: rng(f2|n) misses rng f3
proof
assume rng(f2|n) meets rng f3;
then consider x be object such that
A99: x in rng(f2|n) and
A100: x in rng f3 by XBOOLE_0:3;
consider e being Nat such that
A101: e in dom f3 and
A102: f3.e = x by A100,FINSEQ_2:10;
x = p - (f2/^n).e by A64,A101,A102;
then
A103: x = p - f2.(e+n) by A97,A57,A101,RFINSEQ:def 1;
e+n in dom f2 by A57,A101,FINSEQ_5:26;
then consider e1 be Nat such that
A104: e1 in dom f1 and
A105: f1.e1 = f2.(e+n) by A54,FINSEQ_2:10,FUNCT_1:3;
A106: e1 in dom f by A5,A104,FINSEQ_3:29;
A107: e1 <= p9 by A13,A5,A104,FINSEQ_3:25;
rng(f2|n) c= rng f2 by FINSEQ_5:19;
then consider d1 be Nat such that
A108: d1 in dom f1 and
A109: f1.d1 = x by A54,A99,FINSEQ_2:10;
d1 <= p9 by A13,A5,A108,FINSEQ_3:25;
then d1+e1 <= p9+p9 by A107,XREAL_1:7;
then
A110: d1+e1 < p by A11,A18,XREAL_1:146,XXREAL_0:2;
x = f.d1 mod p by A44,A108,A109,EULER_2:def 2;
then (f.d1 mod p) + f2.(e+n) = p by A103;
then (f.d1 mod p) + (f.e1 mod p) = p by A105,A106,EULER_2:def 2;
then ((f.d1 mod p)+(f.e1 mod p)) mod p = 0 by NAT_D:25;
then (f.d1 + f.e1) mod p = 0 by NAT_D:66;
then p divides (f.d1 + f.e1) by PEPIN:6;
then p divides (d1*a + f.e1) by A25,A44,A108;
then p divides (d1*a + e1*a) by A25,A106;
then
A111: p divides (d1+e1)*a;
d1 >= 1 by A108,FINSEQ_3:25;
hence contradiction by A2,A111,A110,NAT_D:7,WSIERP_1:30;
end;
f2|n is one-to-one by A50,A87,FINSEQ_3:91;
then
A112: f4 is one-to-one by A95,A98,FINSEQ_3:91;
A113: for d st d in dom f3 holds f3.d,-(f2/^n).d are_congruent_mod p
proof
let d;
assume d in dom f3;
then f3.d mod p = (p - (f2/^n).d) mod p by A64
.= (1*p + (-(f2/^n).d)) mod p
.= (-(f2/^n).d) mod p by NAT_D:61;
hence thesis by NAT_D:64;
end;
A114: len(f2/^n) = (len f2 -' n) by RFINSEQ:29
.= len f2 - n by A96,XREAL_1:43,233
.= m by A96;
len(f2|n) = n by A96,FINSEQ_1:59,XREAL_1:43;
then len f4 = n + m by A58,A114,FINSEQ_1:22
.= len f by A13;
then rng f4 = rng I by A13,A112,A79,Th40;
then Product f4 = Product I by A112,EULER_2:10,RFINSEQ:26;
then
A115: (Product(f2|n)) * (Product f3) = Product I by RVSUM_1:97;
f3 is FinSequence of INT by FINSEQ_2:24,NUMBERS:17;
then (Product f3)*(Product(f2|n)),(-1)|^m * Product(f2/^n)*(Product(f2|n)
) are_congruent_mod p by A58,A114,A56,A113,Th33,INT_4:11;
then (Product f3)*(Product(f2|n)),(-1)|^m * ((Product(f2|n))*Product(f2/^
n ) ) are_congruent_mod p;
then Product I,(-1)|^m * Product((f2|n)^(f2/^n)) are_congruent_mod p by
A115,RVSUM_1:97;
then
A116: Product I,(-1)|^m * Product f1 are_congruent_mod p by A55,RFINSEQ:8;
(-1)|^m * Product f1,(-1)|^m * Product f are_congruent_mod p by A9,
INT_4:11;
then Product I,(-1)|^m * (a|^p9) * (Product I) are_congruent_mod p by A15
,A116,INT_1:15;
then p divides (1-((-1)|^m * (a|^p9)))* Product I;
then p divides (1-((-1)|^m * (a|^p9))) by A24,WSIERP_1:29;
then p divides (-1)|^m * (1-((-1)|^m * (a|^p9))) by INT_2:2;
then
A117: p divides ((-1)|^m - (-1)|^m * (-1)|^m * (a|^p9));
(-1)|^m * (-1)|^m = (-1)|^(m+m) by NEWTON:8
.= (-1)|^(2*m)
.= ((-1)|^2)|^m by NEWTON:9
.= (1|^2)|^m by WSIERP_1:1
.= 1;
then (-1)|^m,a|^p9 are_congruent_mod p by A117;
then
A118: (-1)|^m,Lege(a,p) are_congruent_mod p by A8,INT_1:15;
per cases by A77;
suppose
A119: (-1)|^m = 1;
then
A120: Lege(a,p) <> -1 by A118,A1,NAT_D:7;
now
assume Lege(a,p) = 0;
then p divides (1-0) by A118,A119;
then p = 1 by WSIERP_1:15;
hence contradiction by A1;
end;
hence thesis by A119,Th25,A120;
end;
suppose
A121: (-1)|^m = -1;
A122: now
assume Lege(a,p) = 1;
then p divides (-2) by A118,A121;
then p divides 2 by INT_2:10;
hence contradiction by A1,NAT_D:7;
end;
now
assume Lege(a,p) = 0;
then p divides (-1-0) by A118,A121;
then p = 1 by WSIERP_1:15,INT_2:10;
hence contradiction by A1;
end;
hence thesis by A121,Th25,A122;
end;
end;
theorem Th42:
p>2 implies Lege(2,p) = (-1)|^((p^2 -'1) div 8)
proof
set p9 = (p-'1) div 2;
set I = idseq p9;
set fp = 2 * I;
set nn = p div 8;
A1: p>1 by INT_2:def 4;
then
A2: p-1 = p-'1 by XREAL_1:233;
A3: for d st d in dom fp holds fp.d = 2*d
proof
let d;
assume
A4: d in dom fp;
then d in dom I by VALUED_1:def 5;
then d in Seg len I by FINSEQ_1:def 3;
then
A5: d is Element of Seg p9 by CARD_1:def 7;
thus fp.d = 2 * I.d by A4,VALUED_1:def 5
.= 2 * d by A5;
end;
for d being Nat st d in dom fp holds fp.d in NAT;
then reconsider fp as FinSequence of NAT by FINSEQ_2:12;
set f = fp mod p;
reconsider f as FinSequence of NAT by FINSEQ_1:102;
set X = {k where k is Element of NAT:k in rng f & k > p/2};
set m = card X;
dom fp = dom I by VALUED_1:def 5;
then
A6: len fp = len I by FINSEQ_3:29
.= p9 by CARD_1:def 7;
set Y = {d where d is Element of NAT:d in dom f & f.d > p/2};
for x be object st x in Y holds x in dom f
proof
let x be object;
assume x in Y;
then ex k be Element of NAT st x = k & k in dom f & f.k > p/ 2;
hence thesis;
end;
then Y c= dom f;
then reconsider Y as finite Subset of NAT by XBOOLE_1:1;
set Z = seq((p div 4),p9-'(p div 4));
A7: p mod 8 <= 8-1 by INT_1:52,NAT_D:1;
8 = 2*4;
then
A8: 2 divides 8;
A9: now
assume p mod 8 = 0;
then 8 divides p by PEPIN:6;
then p = 8 by INT_2:def 4;
hence contradiction by A8,NAT_4:12;
end;
for x being object st x in X holds x in rng f
proof
let x be object;
assume x in X;
then ex k being Element of NAT st x = k & k in rng f & k > p /2;
hence thesis;
end;
then
A10: X c= rng f;
then reconsider X as finite set;
card X is Element of NAT;
then reconsider m as Element of NAT;
A11: len f = len fp by EULER_2:def 2;
then
A12: dom f = dom fp by FINSEQ_3:29;
assume
A13: p>2;
then 2,p are_coprime by EULER_1:2;
then
A14: 2 gcd p = 1 by INT_2:def 3;
then
A15: Lege(2,p) = (-1)|^m by A13,Th41;
p is odd by A13,PEPIN:17;
then
A16: p-1 is even by HILBERT3:2;
then
A17: p9 = ((p-'1)+1) div 2 by A2,NAT_2:26
.= p div 2 by A1,XREAL_1:235;
then
A18: f <> {} by A13,A6,A11,NAT_2:13;
then reconsider U=dom f as non empty finite Subset of NAT;
2 divides (p-'1) by A16,A2,PEPIN:22;
then
A19: p-'1 = 2*p9;
A20: for d st d in dom f holds f.d = 2*d
proof
let d;
assume
A21: d in dom f;
then d<= p9 by A6,A11,FINSEQ_3:25;
then 2*d<=(p-'1) by A19,XREAL_1:64;
then 2*d<p by NAT_2:9,XXREAL_0:2;
hence 2*d = 2*d mod p by NAT_D:24
.= fp.d mod p by A3,A12,A21
.= f.d by A12,A21,EULER_2:def 2;
end;
A22: for d1,d2 be Nat st 1 <= d1 & d1 < d2 & d2 <= len f holds f.d1 < f.d2
proof
let d1,d2 be Nat;
assume that
A23: 1 <= d1 and
A24: d1 < d2 and
A25: d2 <= len f;
set k1=f.d1;
set k2=f.d2;
1 <= d2 by A23,A24,XXREAL_0:2;
then d2 in dom f by A25,FINSEQ_3:25;
then
A28: k2 = 2*d2 by A20;
d1 <= len f by A24,A25,XXREAL_0:2;
then d1 in dom f by A23,FINSEQ_3:25;
then k1 = 2*d1 by A20;
hence thesis by A24,A28,XREAL_1:68;
end;
rng f is non empty Subset of NAT by A18;
then consider n1 be Element of NAT such that
A29: rng f c= Seg n1 \/ {0} by HEYTING3:1;
reconsider X as finite Subset of NAT by A10,XBOOLE_1:1;
Z, ((p-'1) div 2)-'(p div 4) are_equipotent by CALCUL_2:6; then
A30: card Z = ((p-'1) div 2)-'(p div 4) by CARD_1:def 2;
not 0 in rng f
proof
assume 0 in rng f;
then consider n be Nat such that
A31: n in dom f and
A32: f.n = 0 by FINSEQ_2:10;
2*n =0 by A20,A31,A32;
hence contradiction by A31,FINSEQ_3:25;
end;
then {0} misses rng f by ZFMISC_1:50;
then rng f c= Seg n1 by A29,XBOOLE_1:73;
then
ddd: rng f is included_in_Seg by FINSEQ_1:def 13;
then
A34: Sgm rng f = f by A22,FINSEQ_1:def 14;
A35: 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};
A36: now
let x be set;
assume x in X;
then consider y be Element of NAT such that
A37: y=x and
A38: y in rng f and
y > 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;
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;
f is one-to-one by ddd,A34,FINSEQ_3:92;
hence thesis;
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;
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;
(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;
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
.= 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;
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;
(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;
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
.= 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;
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;
(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;
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
.= 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;
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;
(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;
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
.= 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);
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;
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);
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;
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;
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; 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;
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; 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;
hence thesis;
end;
suppose a<b;
then reconsider l=b-a as Element of NAT by NAT_1:21;
2 divides -(a-b) by A1,INT_2:10;
then consider n be Nat such that
A3: l=2*n by NAT_D:def 3;
(-1)|^b = (-1)|^(a+2*n) by A3
.= (-1)|^a * (-1)|^(2*n) by NEWTON:8
.= (-1)|^a * ((-1)|^2)|^n by NEWTON:9
.= (-1)|^a * (1|^2)|^n by WSIERP_1:1
.= (-1)|^a * 1;
hence thesis;
end;
end;
reserve f,g,h,k for FinSequence of REAL;
theorem Th46:
len f = len h & len g = len k implies f^g-h^k = (f-h)^(g-k)
proof
assume that
A1: len f = len h and
A2: len g = len k;
A3: len(f-h) = len f by A1,TOPREAL7:7;
len(f^g) = len h + len k by A1,A2,FINSEQ_1:22;
then len(f^g) = len(h^k) by FINSEQ_1:22;
then
A4: len(f^g-h^k) = len(f^g) by TOPREAL7:7;
A5: len(g-k) = len g by A2,TOPREAL7:7;
then len((f-h)^(g-k)) = len f + len g by A3,FINSEQ_1:22;
then len(f^g-h^k) = len((f-h)^(g-k)) by A4,FINSEQ_1:22;
then
A6: dom(f^g-h^k) = dom((f-h)^(g-k)) by FINSEQ_3:29;
for d being Nat st d in dom((f-h)^(g-k)) holds ((f-h)^(g-k)).d = (f^g-h ^k).d
proof
let d be Nat;
assume
A7: d in dom((f-h)^(g-k));
per cases by A7,FINSEQ_1:25;
suppose
A8: d in dom(f-h);
then
A9: ((f-h)^(g-k)).d = (f-h).d by FINSEQ_1:def 7
.= f.d - h.d by A8,VALUED_1:13;
A10: dom f = dom(f-h) by A1,TOPREAL7:7;
A11: dom h = dom(f-h) by A1,A3,FINSEQ_3:29;
(f^g-h^k).d = (f^g).d - (h^k).d by A6,A8,FINSEQ_2:15,VALUED_1:13
.= f.d - (h^k).d by A8,A10,FINSEQ_1:def 7
.= f.d - h.d by A8,A11,FINSEQ_1:def 7;
hence thesis by A9;
end;
suppose
ex e being Nat st e in dom(g-k) & d = len(f-h) + e;
then consider e such that
A12: e in dom(g-k) and
A13: d = len(f-h) + e;
e in dom g by A2,A12,TOPREAL7:7;
then
A14: (f^g).d = g.e by A3,A13,FINSEQ_1:def 7;
e in dom k by A2,A5,A12,FINSEQ_3:29;
then
A15: (h^k).d = k.e by A1,A3,A13,FINSEQ_1:def 7;
((f-h)^(g-k)).d = (g-k).e by A12,A13,FINSEQ_1:def 7
.=g.e - k.e by A12,VALUED_1:13;
hence thesis by A6,A12,A13,A14,A15,FINSEQ_1:28,VALUED_1:13;
end;
end;
hence thesis by A6;
end;
theorem Th47:
for f be FinSequence of REAL,m be Real holds Sum(((len f) |-> 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; :: redefines Card (CARD_3, definition)
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 (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;
let f be FinSequence of bool X;
for n be Nat holds P[n] from NAT_1:sch 2(A25,A1); then
P[len f];
hence thesis;
end;
Lm4: Sum(fp) is Element of NAT;
reserve q for Prime;
::$N The law of quadratic reciprocity
::$L https://en.wikipedia.org/wiki/Quadratic_reciprocity 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;
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;
reconsider g3 as FinSequence of NAT by FINSEQ_1:102;
set g4 = Sgm rng g3;
A24: len g3 = len g1 by EULER_2:def 2;
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 2;
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 2;
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;
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;
rng g3 c= Seg n2 by A32,A47,XBOOLE_1:73;
then
kkk: rng g3 is included_in_Seg by FINSEQ_1:def 13;
then
A48: g4 is one-to-one by FINSEQ_3:92;
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 A41,XREAL_1:147;
d<=q9 by A23,A51,FINSEQ_3:25;
then d-e<=q9-1 by A57,XREAL_1:13;
then
A61: d-e < q by A60,XXREAL_0:2;
-(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 kkk,A23,A24,FINSEQ_3:39;
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 2;
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 rng g3 is included_in_Seg by FINSEQ_1:def 13;
then
A78: rng g4 = rng g3 by FINSEQ_1:def 14;
then XX c= Seg n2 by A77,A26;
then
a79: XX is included_in_Seg by FINSEQ_1:def 13;
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 2;
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;
A85: Sum g4 = Sum g3 by A66,A78,A48,RFINSEQ:9,26;
rng g4 \ XX c= rng g4 by XBOOLE_1:36;
then YY c= Seg n2 by A77,A78;
then
a87: YY is included_in_Seg by FINSEQ_1:def 13;
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 a87,FINSEQ_3:39
.= 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;
reconsider f3 as FinSequence of NAT by FINSEQ_1:102;
A96: len f3 = len f1 by EULER_2:def 2;
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 2;
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 rng f3 c= Seg n1 by A99,XBOOLE_1:73;
then
ttt: rng f3 is included_in_Seg by FINSEQ_1:def 13;
then
A109: f4 is one-to-one by FINSEQ_3:92;
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 A12,XREAL_1:147;
d<=p9 by A18,A112,FINSEQ_3:25;
then d-e<=p9-1 by A118,XREAL_1:13;
then
A122: d-e < p by A121,XXREAL_0:2;
-(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 ttt,A18,A96,FINSEQ_3:39;
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
.= dom(g4/^nn) /\ dom(g4/^nn) by FINSEQ_1:def 3,A134,CARD_1:def 7
.= 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 14;
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 2;
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;
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 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;
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 2;
A164: d1 in dom g1 by A24,A159,FINSEQ_3:29;
then x = g1.d1 mod q by A160,EULER_2:def 2;
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 NAT_D:66;
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<e & e<=len g5 holds g5.d
<> g5. e
proof
let d,e be Nat;
assume that
A166: 1<=d and
A167: d<e and
A168: e<=len g5;
1<=e by A166,A167,XXREAL_0:2;
then
A169: e in dom g5 by A168,FINSEQ_3:25;
then
A170: g5.e = q - (g4/^nn).e by A137;
d<len g5 by A167,A168,XXREAL_0:2;
then
A171: d in dom g5 by A166,FINSEQ_3:25;
then g5.d = q - (g4/^nn).d by A137;
hence thesis by A82,A135,A167,A171,A169,A170;
end;
then len g5 = card rng g5 by GRAPH_5:7;
then g5 is one-to-one by FINSEQ_4:62;
then
A172: g6 is one-to-one by A130,A150,FINSEQ_3:91;
A173: for d st d in dom g6 holds g6.d>0 & g6.d <= q9
proof
let d;
assume
A174: d in dom g6;
per cases by A174,FINSEQ_1:25;
suppose
A175: d in dom(g4|nn);
then (g4|nn).d in rng Sgm YY by A129,FUNCT_1:3;
then
A176: (g4|nn).d in YY by a87,FINSEQ_1:def 14;
then
A177: (g4|nn).d in rng g4 by XBOOLE_0:def 5;
not (g4|nn).d in XX by A176,XBOOLE_0:def 5;
then (g4|nn).d <= q/2 by A177;
then
A178: (g4|nn).d <= q9 by A83,INT_1:54;
not (g4|nn).d in {0} by A47,A78,A177,XBOOLE_0:3;
then (g4|nn).d <> 0 by TARSKI:def 1;
hence thesis by A175,A178,FINSEQ_1:def 7;
end;
suppose
ex l being Nat st l in dom g5 & d=len(g4|nn)+ l;
then consider l be Element of NAT such that
A179: l in dom g5 and
A180: d = len(g4|nn)+ l;
g6.d = g5.l by A179,A180,FINSEQ_1:def 7;
hence thesis by A139,A179;
end;
end;
len g6 = len(g4|nn) + len g5 by FINSEQ_1:22
.= q9 by A133,A134,A136;
then rng g6 = rng idseq q9 by A172,A173,Th40;
then N = Sum g6 by A172,RFINSEQ:9,26
.= Sum(g4|nn) + Sum g5 by RVSUM_1:75
.= Sum(g4|nn) + (mm*q - Sum(g4/^nn)) by A134,A132,Th47
.= Sum(g4|nn) + mm*q - Sum(g4/^nn);
then (p-1)*N = q*(Sum g2) + 2*Sum(Sgm XX) - mm*q by A93,A95,A129;
then
A182: (p-'1)*N mod 2 = ((q*(Sum g2)-mm*q) + 2*Sum(Sgm XX)) mod 2 by A6,
XREAL_1:233
.= (q*(Sum g2)-mm*q) mod 2 by NAT_D:61;
2 divides (p-'1)*N by A10,NAT_D:9;
then (q*((Sum g2)-mm)) mod 2 = 0 by A182;
then 2 divides (q*((Sum g2)-mm)) by Lm1;
then 2 divides ((Sum g2) - mm) by A70,INT_2:25;
then (Sum g2),mm are_congruent_mod 2;
then (Sum g2) mod 2 = mm mod 2 by NAT_D:64;
then (-1)|^(Sum g2) = (-1)|^mm by Th45;
hence thesis by A2,A5,A78,Th41;
end;
for d being Nat st d in dom idseq p9 holds (idseq p9).d in NAT;
then idseq p9 is FinSequence of NAT by FINSEQ_2:12;
then reconsider M = Sum idseq p9 as Element of NAT by Lm4;
A183: 2,p are_coprime by A1,EULER_1:2;
set X = {k where k is Element of NAT:k in rng f4 & k>p/2};
for x being object st x in X holds x in rng f4
proof
let x be object;
assume x in X;
then ex k being Element of NAT st x = k & k in rng f4 & k > p/2;
hence thesis;
end;
then
A184: X c= rng f4;
A185: p9 >= 1 by A7,A98,NAT_2:13;
A186: (Sum f2) + (Sum g2) = p9 * q9
proof
reconsider A = Seg p9,B = Seg q9 as non empty finite Subset of NAT by A185
,A31;
deffunc F(Element of A,Element of B) = $1/p - $2/q;
A187: for x be Element of A, y be Element of B holds F(x,y) in REAL by
XREAL_0:def 1;
consider z being Function of [:A,B:], REAL such that
A188: for x be Element of A, y be Element of B holds z.(x,y) = F(x,y)
from FUNCT_7:sch 1(A187);
defpred G[set,set] means ex x be Element of A st $1=x & $2 = {[x,y] where
y is Element of B:z.(x,y)>0};
A189: for d being Nat st d in Seg p9 ex x1 be Element of bool dom z st G[d ,x1]
proof
let d be Nat;
assume d in Seg p9;
then reconsider d as Element of A;
take x1 = {[d,y] where y is Element of B:z.(d,y)>0};
x1 c= dom z
proof
let l be object;
assume l in x1;
then ex yy be Element of B st [d,yy] = l & z.(d,yy) > 0;
then l in [:A,B:];
hence thesis by FUNCT_2:def 1;
end;
hence thesis;
end;
consider Pr be FinSequence of bool dom z such that
A190: dom Pr = Seg p9 & for d being Nat st d in Seg p9 holds G[d,Pr.d]
from FINSEQ_1:sch 5(A189);
A191: dom Card Pr = dom Pr by CARD_3:def 2
.= dom f2 by A27,A190,FINSEQ_1:def 3;
for d being Nat st d in dom Card Pr holds (Card Pr).d = f2.d
proof
let d be Nat;
assume
A192: d in dom Card Pr;
then d in Seg p9 by A27,A191,FINSEQ_1:def 3;
then consider m be Element of A such that
A193: m = d and
A194: Pr.d = {[m,y] where y is Element of B:z.(m,y)>0} by A190;
Pr.d = [:{m},Seg(f2.m):]
proof
set L = [:{m},Seg(f2.m):];
A195: L c= Pr.d
proof
now
assume q mod p = 0;
then
A196: p divides q by PEPIN:6;
then p <= q by NAT_D:7;
then p < q by A3,XXREAL_0:1;
hence contradiction by A6,A196,NAT_4:12;
end;
then
A197: -(q div p) = (-q) div p + 1 by WSIERP_1:41;
2 divides (p-'1)*q by A10,NAT_D:9;
then (p-'1)*q mod 2 = 0;
then ((p-'1)*q) div 2 = (p-'1)*q/2 by REAL_3:4;
then
A198: (p9*q) div p = ((p-1)*q) div (2*p) by A7,A11,NAT_2:27
.= ((p*q - q) div p) div 2 by PRE_FF:5
.= (q+(-(q div p)-1)) div 2 by A197,NAT_D:61
.= (2*q9+(-(q div p))) div 2 by A29,A40
.= q9+((-(q div p)) div 2) by NAT_D:61;
A199: (p9*q) div p <= q9
proof
per cases;
suppose
(q div p) mod 2 = 0;
then (-(q div p)) div 2 = -((q div p) div 2) by WSIERP_1:42
.= -(q div (2*p)) by NAT_2:27;
then (p9*q) div p = q9-(q div (2*p)) by A198;
hence thesis by XREAL_1:43;
end;
suppose
(q div p) mod 2 <> 0;
then -((q div p) div 2) = (-(q div p)) div 2 +1 by WSIERP_1:41;
then (-(q div p)) div 2 = -((q div p) div 2)-1
.= -(q div (2*p)) - 1 by NAT_2:27;
then (p9*q) div p = q9 -((q div (2*p)) + 1) by A198;
hence thesis by XREAL_1:43;
end;
end;
m <= p9 by FINSEQ_1:1;
then m*q <= p9*q by XREAL_1:64;
then (m*q) div p <= (p9*q) div p by NAT_2:24;
then
A200: (m*q) div p <= q9 by A199,XXREAL_0:2;
m in Seg p9;
then
A201: m in dom f1 by A18,FINSEQ_1:def 3;
then
A202: f2.m = f1.m div p by A27,A100
.= (m*q) div p by A13,A201;
now
assume m*q/p is integer;
then
A203: p divides m*q by WSIERP_1:17;
A204: m <= p9 by FINSEQ_1:1;
0+1 <= m by FINSEQ_1:1;
then p <= m by A5,A203,NAT_D:7,WSIERP_1:30;
hence contradiction by A12,A204,XXREAL_0:2;
end;
then
A205: [\m*q/p/] < m*q/p by INT_1:26;
let l be object;
assume l in L;
then consider x,y be object such that
A206: x in {m} and
A207: y in Seg(f2.m) and
A208: l = [x,y] by ZFMISC_1:def 2;
reconsider y as Element of NAT by A207;
A209: 1 <= y by A207,FINSEQ_1:1;
y <= f2.m by A207,FINSEQ_1:1;
then y <= q9 by A200,A202,XXREAL_0:2;
then reconsider y as Element of B by A209,FINSEQ_1:1;
y <= [\m*q/p/] by A207,A202,FINSEQ_1:1;
then y < m*q/p by A205,XXREAL_0:2;
then y*p < (m*q)/p*p by XREAL_1:68;
then y*p < m*q by XCMPLX_1:87;
then y/q < m/p by XREAL_1:106;
then m/p - y/q > 0 by XREAL_1:50;
then z.(m,y) > 0 by A188;
then [m,y] in Pr.d by A194;
hence thesis by A206,A208,TARSKI:def 1;
end;
Pr.d c= L
proof
let l be object;
A210: m in {m} by TARSKI:def 1;
m in Seg p9;
then
A211: m in dom f1 by A18,FINSEQ_1:def 3;
assume l in Pr.d;
then consider y1 be Element of B such that
A212: l = [m,y1] and
A213: z.(m,y1) > 0 by A194;
m/p - y1/q > 0 by A188,A213;
then m/p - y1/q + y1/q > 0 + y1/q by XREAL_1:6;
then m/p*q > y1/q*q by XREAL_1:68;
then (m*q)/p > y1 by XCMPLX_1:87;
then ((m*q) div p) >= y1 by INT_1:54;
then ((f1.m) div p) >= y1 by A13,A211;
then
A214: y1 <= f2.m by A27,A100,A211;
y1 >= 1 by FINSEQ_1:1;
then y1 in Seg(f2.m) by A214,FINSEQ_1:1;
hence thesis by A212,A210,ZFMISC_1:def 2;
end;
hence thesis by A195,XBOOLE_0:def 10;
end;
then card(Pr.d) = card [:Seg(f2.m),{m}:] by CARD_2:4
.= card Seg(f2.m) by CARD_1:69;
then
A215: card(Pr.d) = card(f2.d) by A193,FINSEQ_1:55
.= f2.d;
d in dom Pr by A192,CARD_3:def 2;
hence thesis by A215,CARD_3:def 2;
end;
then
A216: Card Pr = f2 by A191;
defpred K[set,set] means ex y be Element of B st $1=y & $2 = {[x,y] where
x is Element of A:z.(x,y)<0};
A217: for d being Nat st d in Seg q9 ex x1 be Element of bool dom z st K[d ,x1]
proof
let d be Nat;
assume d in Seg q9;
then reconsider d as Element of B;
take x1 = {[x,d] where x is Element of A:z.(x,d)<0};
x1 c= dom z
proof
let l be object;
assume l in x1;
then ex xx be Element of A st [xx,d] = l & z.(xx,d) < 0;
then l in [:A,B:];
hence thesis by FUNCT_2:def 1;
end;
hence thesis;
end;
consider Pk be FinSequence of bool dom z such that
A218: dom Pk = Seg q9 & for d being Nat st d in Seg q9 holds K[d,Pk.d]
from FINSEQ_1:sch 5(A217);
A219: dom Card Pk = Seg(len g2) by A33,A218,CARD_3:def 2
.= dom g2 by FINSEQ_1:def 3;
A220: for d being Nat st d in dom Card Pk holds (Card Pk).d = g2.d
proof
let d be Nat;
assume
A221: d in dom Card Pk;
then d in Seg q9 by A33,A219,FINSEQ_1:def 3;
then consider n be Element of B such that
A222: n = d and
A223: Pk.d = {[x,n] where x is Element of A:z.(x,n)<0} by A218;
Pk.d = [:Seg(g2.n),{n}:]
proof
set L = [:Seg(g2.n),{n}:];
A224: L c= Pk.d
proof
now
assume p mod q = 0;
then
A225: q divides p by PEPIN:6;
then q <= p by NAT_D:7;
then q < p by A3,XXREAL_0:1;
hence contradiction by A28,A225,NAT_4:12;
end;
then
A226: -(p div q) = (-p) div q + 1 by WSIERP_1:41;
2 divides (q-'1)*p by A39,NAT_D:9;
then (q-'1)*p mod 2 = 0;
then ((q-'1)*p) div 2 = (q-'1)*p/2 by REAL_3:4;
then
A227: (q9*p) div q = ((q-1)*p) div (2*q) by A29,A40,NAT_2:27
.= ((q*p - p) div q) div 2 by PRE_FF:5
.= (p+(-(p div q)-1)) div 2 by A226,NAT_D:61
.= (2*p9-(p div q)) div 2 by A7,A11
.= p9+((-(p div q)) div 2) by NAT_D:61;
A228: (q9*p) div q <= p9
proof
per cases;
suppose
(p div q) mod 2 = 0;
then (-(p div q)) div 2 = -((p div q) div 2) by WSIERP_1:42
.= -(p div (2*q)) by NAT_2:27;
then (q9*p) div q = p9-(p div (2*q)) by A227;
hence thesis by XREAL_1:43;
end;
suppose
(p div q) mod 2 <> 0;
then -((p div q) div 2) = (-(p div q)) div 2 +1 by WSIERP_1:41;
then (-(p div q)) div 2 = -((p div q) div 2)-1
.= -(p div (2*q)) - 1 by NAT_2:27;
then (q9*p) div q = p9 -((p div (2*q)) + 1) by A227;
hence thesis by XREAL_1:43;
end;
end;
n in Seg q9;
then
A229: n in dom g1 by A23,FINSEQ_1:def 3;
then
A230: g2.n = g1.n div q by A33,A34
.= (n*p) div q by A19,A229;
let l be object;
assume l in L;
then consider x,y be object such that
A231: x in Seg(g2.n) and
A232: y in {n} and
A233: l = [x,y] by ZFMISC_1:def 2;
reconsider x as Element of NAT by A231;
A234: x <= g2.n by A231,FINSEQ_1:1;
n <= q9 by FINSEQ_1:1;
then n*p <= q9*p by XREAL_1:64;
then (n*p) div q <= (q9*p) div q by NAT_2:24;
then (n*p) div q <= p9 by A228,XXREAL_0:2;
then
A235: x <= p9 by A230,A234,XXREAL_0:2;
1 <= x by A231,FINSEQ_1:1;
then reconsider x as Element of A by A235,FINSEQ_1:1;
now
assume n*p/q is integer;
then
A236: q divides n*p by WSIERP_1:17;
A237: n <= q9 by FINSEQ_1:1;
0+1 <= n by FINSEQ_1:1;
then q <= n by A5,A236,NAT_D:7,WSIERP_1:30;
hence contradiction by A41,A237,XXREAL_0:2;
end;
then [\n*p/q/] < n*p/q by INT_1:26;
then x < n*p/q by A230,A234,XXREAL_0:2;
then x*q < (n*p)/q*q by XREAL_1:68;
then x*q < n*p by XCMPLX_1:87;
then x/p - n/q < 0 by XREAL_1:49,106;
then z.(x,n) < 0 by A188;
then [x,n] in Pk.d by A223;
hence thesis by A232,A233,TARSKI:def 1;
end;
Pk.d c= L
proof
let l be object;
A238: n in {n} by TARSKI:def 1;
n in Seg q9;
then
A239: n in dom g1 by A23,FINSEQ_1:def 3;
assume l in Pk.d;
then consider x be Element of A such that
A240: l = [x,n] and
A241: z.(x,n) < 0 by A223;
x/p - n/q < 0 by A188,A241;
then x/p - n/q + n/q < 0 + n/q by XREAL_1:6;
then x/p*p < n/q*p by XREAL_1:68;
then x < (n*p)/q by XCMPLX_1:87;
then x <= (n*p) div q by INT_1:54;
then ((g1.n) div q) >= x by A19,A239;
then
A242: x <= g2.n by A33,A34,A239;
x >= 1 by FINSEQ_1:1;
then x in Seg(g2.n) by A242,FINSEQ_1:1;
hence thesis by A240,A238,ZFMISC_1:def 2;
end;
hence thesis by A224,XBOOLE_0:def 10;
end;
then card(Pk.d) = card Seg(g2.n) by CARD_1:69;
then
A243: card(Pk.d) = card(g2.d) by A222,FINSEQ_1:55
.= g2.d;
d in dom Pk by A221,CARD_3:def 2;
hence thesis by A243,CARD_3:def 2;
end;
reconsider U1 = union rng Pr, U2 = union rng Pk as finite Subset of dom z
by PROB_3:48;
dom z c= U1 \/ U2
proof
let l be object;
assume l in dom z;
then consider x,y be object such that
A244: x in A and
A245: y in B and
A246: l = [x,y] by ZFMISC_1:def 2;
reconsider y as Element of B by A245;
reconsider x as Element of A by A244;
A247: z.(x,y) <> 0
proof
assume z.(x,y) = 0;
then x/p - y/q = 0 by A188;
then x*q = y*p by XCMPLX_1:95;
then
A248: p divides x*q;
A249: x <= p9 by FINSEQ_1:1;
x >= 0 + 1 by FINSEQ_1:1;
then p <= x by A5,A248,NAT_D:7,WSIERP_1:30;
hence contradiction by A12,A249,XXREAL_0:2;
end;
per cases by A247;
suppose
A250: z.(x,y) > 0;
G[x,Pr.x] by A190;
then l in Pr.x by A246,A250;
then l in Union Pr by A190,PROB_3:49;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A251: z.(x,y) < 0;
K[y,Pk.y] by A218;
then l in Pk.y by A246,A251;
then l in Union Pk by A218,PROB_3:49;
hence thesis by XBOOLE_0:def 3;
end;
end;
then
A252: U1 \/ U2 = dom z by XBOOLE_0:def 10;
A253: U1 misses U2
proof
assume U1 meets U2;
then consider l be object such that
A254: l in U1 and
A255: l in U2 by XBOOLE_0:3;
l in Union Pk by A255;
then consider k2 be Nat such that
A256: k2 in dom Pk and
A257: l in Pk.k2 by PROB_3:49;
l in Union Pr by A254;
then consider k1 be Nat such that
A258: k1 in dom Pr and
A259: l in Pr.k1 by PROB_3:49;
reconsider k1,k2 as Element of NAT by ORDINAL1:def 12;
consider n1 be Element of B such that
n1 = k2 and
A260: Pk.k2 = {[x,n1] where x is Element of A:z.(x,n1)<0} by A218,A256;
consider n2 be Element of A such that
A261: l = [n2,n1] and
A262: z.(n2,n1) < 0 by A257,A260;
consider m1 be Element of A such that
m1 = k1 and
A263: Pr.k1 = {[m1,y] where y is Element of B:z.(m1,y)>0} by A190,A258;
A264: ex m2 be Element of B st l = [m1,m2] & z.(m1,m2) > 0 by A259,A263;
then m1 = n2 by A261,XTUPLE_0:1;
hence contradiction by A264,A261,A262,XTUPLE_0:1;
end;
A265: for d,e st d in dom Pk & e in dom Pk & d<>e holds Pk.d misses Pk.e
proof
let d,e;
assume that
A266: d in dom Pk and
A267: e in dom Pk and
A268: d<>e;
consider y2 be Element of B such that
A269: y2=e and
A270: Pk.e = {[x,y2] where x is Element of A:z.(x,y2)<0} by A218,A267;
consider y1 be Element of B such that
A271: y1=d and
A272: Pk.d = {[x,y1] where x is Element of A:z.(x,y1)<0} by A218,A266;
now
assume not Pk.d misses Pk.e;
then consider l be object such that
A273: l in Pk.d and
A274: l in Pk.e by XBOOLE_0:3;
A275: ex x2 be Element of A st l = [x2,y2] & z.(x2,y2) < 0 by A270,A274;
ex x1 be Element of A st l = [x1,y1] & z.(x1,y1) < 0 by A272,A273;
hence contradiction by A268,A271,A269,A275,XTUPLE_0:1;
end;
hence thesis;
end;
A276: card union rng Pk = Sum Card Pk by A265,Th48;
A277: for d,e st d in dom Pr & e in dom Pr & d<>e holds Pr.d misses Pr.e
proof
let d,e;
assume that
A278: d in dom Pr and
A279: e in dom Pr and
A280: d<>e;
consider x2 be Element of A such that
A281: x2=e and
A282: Pr.e = {[x2,y] where y is Element of B:z.(x2,y)>0} by A190,A279;
consider x1 be Element of A such that
A283: x1=d and
A284: Pr.d = {[x1,y] where y is Element of B:z.(x1,y)>0} by A190,A278;
now
assume not Pr.d misses Pr.e;
then consider l be object such that
A285: l in Pr.d and
A286: l in Pr.e by XBOOLE_0:3;
A287: ex y2 be Element of B st l = [x2,y2] & z.(x2,y2) > 0 by A282,A286;
ex y1 be Element of B st l = [x1,y1] & z.(x1,y1) > 0 by A284,A285;
hence contradiction by A280,A283,A281,A287,XTUPLE_0:1;
end;
hence thesis;
end;
card union rng Pr = Sum Card Pr by A277,Th48;
then card(U1 \/ U2) = (Sum Card Pr) + (Sum Card Pk) by A276,A253,CARD_2:40;
then (Sum Card Pr) + (Sum Card Pk) = card [:A,B:] by A252,FUNCT_2:def 1
.= card A * card B by CARD_2:46
.= p9* card B by FINSEQ_1:57
.= p9 * q9 by FINSEQ_1:57;
hence thesis by A216,A219,A220,FINSEQ_1:13;
end;
dom(p*f2) = dom f2 by VALUED_1:def 5;
then
A288: len(p*f2) = p9 by A27,FINSEQ_3:29;
p*f2 is Element of NAT* by FINSEQ_1:def 11;
then p*f2 in p9-tuples_on NAT by A288;
then
A289: p*f2 is Element of p9-tuples_on REAL by FINSEQ_2:109,NUMBERS:19;
A290: p9 = ((p-'1)+1) div 2 by A9,NAT_2:26
.= p div 2 by A6,XREAL_1:235;
reconsider X as finite Subset of NAT by A184,XBOOLE_1:1;
set m = card X;
reconsider Y = rng f4 \ X as finite Subset of NAT;
A291: f3 is Element of NAT* by FINSEQ_1:def 11;
len f3 = p9 by A17,A96,CARD_1:def 7;
then f3 in p9-tuples_on NAT by A291;
then
A292: f3 is Element of p9-tuples_on REAL by FINSEQ_2:109,NUMBERS:19;
A293: rng f3 c= Seg n1 by A99,A108,XBOOLE_1:73;
then rng f3 is included_in_Seg by FINSEQ_1:def 13;
then
A294: rng f4 = rng f3 by FINSEQ_1:def 14;
then X c= Seg n1 by A293,A184;
then
a295: X is included_in_Seg by FINSEQ_1:def 13;
A296: dom (p*f2+f3) = dom (p*f2) /\ dom f3 by VALUED_1:def 1
.= dom f2 /\ dom f3 by VALUED_1:def 5
.= dom f1 by A97,A100;
for d being Nat st d in dom f1 holds f1.d = (p*f2+f3).d
proof
let d be Nat;
assume
A297: d in dom f1;
then
A298: d in dom (p*f2) by A100,VALUED_1:def 5;
(p*f2+f3).d = (p*f2).d + f3.d by A296,A297,VALUED_1:def 1;
hence (p*f2+f3).d = p * f2.d + f3.d by A298,VALUED_1:def 5
.= f1.d by A101,A297;
end;
then f1 = p*f2 + f3 by A296;
then
A299: Sum f1 = Sum(p*f2) + Sum f3 by A289,A292,RVSUM_1:89
.= p*(Sum f2) + Sum f3 by RVSUM_1:87;
rng f4 \ X c= rng f4 by XBOOLE_1:36;
then Y c= Seg n1 by A293,A294;
then
a301: Y is included_in_Seg by FINSEQ_1:def 13;
A302: len f3 = card rng f4 by A127,A294,FINSEQ_4:62;
then reconsider n = p9 - m as Element of NAT by A18,A96,A184,NAT_1:21,43;
A303: f4 = (f4|n)^(f4/^n) by RFINSEQ:8;
then
A304: f4/^n is one-to-one by A109,FINSEQ_3:91;
A306: Sum f4 = Sum f3 by A127,A294,A109,RFINSEQ:9,26;
for k,l being Nat st k in Y & l in X holds k < l
proof
let k,l be Nat;
assume that
A307: k in Y and
A308: l in X;
A309: not k in X by A307,XBOOLE_0:def 5;
A310: ex l1 being Element of NAT st l1 = l & l1 in rng f4 & l1>p/2 by A308;
k in rng f4 by A307,XBOOLE_0:def 5;
then k <= p/2 by A309;
hence thesis by A310,XXREAL_0:2;
end;
then Sgm (Y\/X) = (Sgm Y)^(Sgm X) by a295,a301,FINSEQ_3:42;
then Sgm (rng f4 \/ X) = (Sgm Y)^(Sgm X) by XBOOLE_1:39;
then
A311: f4 = (Sgm Y)^(Sgm X) by A294,A184,XBOOLE_1:12;
then Sum f4 = Sum(Sgm Y) + Sum(Sgm X) by RVSUM_1:75;
then
A312: q*(Sum idseq p9)=p*(Sum f2)+Sum(Sgm Y) + Sum(Sgm X) by A299,A306,
RVSUM_1:87;
A313: len Sgm Y = card Y by a301,FINSEQ_3:39
.= p9 - m by A18,A96,A184,A302,CARD_2:44;
then
A314: f4/^n = Sgm X by A311,FINSEQ_5:37;
A315: f4|n = Sgm Y by A311,A313,FINSEQ_3:113,FINSEQ_6:10;
A316: f4|n is one-to-one by A109,A303,FINSEQ_3:91;
Lege(q,p) = (-1)|^(Sum f2)
proof
set f5 = (m|->p)-(f4/^n);
set f6 = (f4|n)^f5;
A317: f4/^n is FinSequence of REAL by FINSEQ_2:24,NUMBERS:19;
A318: len(f4|n) = n by A128,FINSEQ_1:59,XREAL_1:43;
A319: len(f4/^n) = (len f4 -' n) by RFINSEQ:29
.= len f4 - n by A128,XREAL_1:43,233
.= m by A128;
A320: dom f5 = dom(m |-> p) /\ dom(f4/^n) by VALUED_1:12
.= (Seg len (m |-> p)) /\ dom(f4/^n) by FINSEQ_1:def 3
.= dom(f4/^n) /\ dom(f4/^n) by FINSEQ_1:def 3,A319,CARD_1:def 7
.= dom(f4/^n);
then
A321: len f5 = len(f4/^n) by FINSEQ_3:29;
A322: for d st d in dom f5 holds f5.d = p - (f4/^n).d
proof
let d;
assume
A323: d in dom f5;
then d in Seg m by A319,A320,FINSEQ_1:def 3;
then (m |-> p).d = p by FINSEQ_2:57;
hence thesis by A323,VALUED_1:13;
end;
A324: for d st d in dom f5 holds f5.d > 0 & f5.d <= p9
proof
let d;
reconsider w = f5.d as Element of INT by INT_1:def 2;
assume
A325: d in dom f5;
then (Sgm X).d in rng Sgm X by A314,A320,FUNCT_1:3;
then (Sgm X).d in X by a295,FINSEQ_1:def 14;
then
A326: ex ll be Element of NAT st ll = (Sgm X).d & ll in rng f3 &
ll > p/2 by A294;
then consider e being Nat such that
A327: e in dom f3 and
A328: f3.e = (f4/^n).d by A314,FINSEQ_2:10;
(f4/^n).d = f1.e mod p by A97,A327,A328,EULER_2:def 2;
then
A329: (f4/^n).d < p by NAT_D:1;
A330: f5.d = p - (f4/^n).d by A322,A325;
then w < p - p/2 by A314,A326,XREAL_1:10;
hence thesis by A290,A330,A329,INT_1:54,XREAL_1:50;
end;
for d being Nat st d in dom f5 holds f5.d in NAT
proof
let d be Nat;
assume
A332: d in dom f5;
f5.d > 0 by A332,A324;
hence thesis by INT_1:3;
end;
then reconsider f5 as FinSequence of NAT by FINSEQ_2:12;
f5 is FinSequence of NAT;
then reconsider f6 as FinSequence of NAT by FINSEQ_1:75;
A334: n <= len f4 by A128,XREAL_1:43;
A335: rng(f4|n) misses rng f5
proof
assume not rng(f4|n) misses rng f5;
then consider x be object such that
A336: x in rng(f4|n) and
A337: x in rng f5 by XBOOLE_0:3;
consider e being Nat such that
A338: e in dom f5 and
A339: f5.e = x by A337,FINSEQ_2:10;
x = p - (f4/^n).e by A322,A338,A339;
then
A340: x = p - f4.(e+n) by A334,A320,A338,RFINSEQ:def 1;
e+n in dom f4 by A320,A338,FINSEQ_5:26;
then consider e1 be Nat such that
A341: e1 in dom f3 and
A342: f3.e1 = f4.(e+n) by A294,FINSEQ_2:10,FUNCT_1:3;
A343: e1 <= p9 by A18,A96,A341,FINSEQ_3:25;
rng(f4|n) c= rng f4 by FINSEQ_5:19;
then consider d1 be Nat such that
A344: d1 in dom f3 and
A345: f3.d1 = x by A294,A336,FINSEQ_2:10;
d1 <= p9 by A18,A96,A344,FINSEQ_3:25;
then d1+e1 <= p9+p9 by A343,XREAL_1:7;
then
A346: d1+e1 < p by A7,A11,XREAL_1:146,XXREAL_0:2;
x = f1.d1 mod p by A97,A344,A345,EULER_2:def 2;
then (f1.d1 mod p) + f4.(e+n) = p by A340;
then (f1.d1 mod p) + (f1.e1 mod p) = p by A97,A341,A342,EULER_2:def 2;
then ((f1.d1 mod p)+(f1.e1 mod p)) mod p = 0 by NAT_D:25;
then (f1.d1 + f1.e1) mod p = 0 by NAT_D:66;
then p divides (f1.d1 + f1.e1) by PEPIN:6;
then p divides (d1*q + f1.e1) by A13,A97,A344;
then p divides (d1*q + e1*q) by A13,A97,A341;
then
A347: p divides (d1+e1)*q;
d1 >= 1 by A344,FINSEQ_3:25;
hence contradiction by A4,A347,A346,NAT_D:7,PEPIN:3;
end;
for d,e being Nat st 1<=d & d<e & e<=len f5 holds f5.d <> f5.e
proof
let d,e be Nat;
assume that
A348: 1<=d and
A349: d<e and
A350: e<=len f5;
1<=e by A348,A349,XXREAL_0:2;
then
A351: e in dom f5 by A350,FINSEQ_3:25;
then
A352: f5.e = p - (f4/^n).e by A322;
d<len f5 by A349,A350,XXREAL_0:2;
then
A353: d in dom f5 by A348,FINSEQ_3:25;
then f5.d = p - (f4/^n).d by A322;
hence thesis by A304,A320,A349,A353,A351,A352;
end;
then len f5 = card rng f5 by GRAPH_5:7;
then f5 is one-to-one by FINSEQ_4:62;
then
A354: f6 is one-to-one by A316,A335,FINSEQ_3:91;
A355: for d st d in dom f6 holds f6.d>0 & f6.d <= p9
proof
let d;
assume
A356: d in dom f6;
per cases by A356,FINSEQ_1:25;
suppose
A357: d in dom(f4|n);
then (f4|n).d in rng Sgm Y by A315,FUNCT_1:3;
then
A358: (f4|n).d in Y by a301,FINSEQ_1:def 14;
then
A359: (f4|n).d in rng f4 by XBOOLE_0:def 5;
not (f4|n).d in X by A358,XBOOLE_0:def 5;
then (f4|n).d <= p/2 by A359;
then
A360: (f4|n).d <= p9 by A290,INT_1:54;
not (f4|n).d in {0} by A108,A294,A359,XBOOLE_0:3;
then (f4|n).d <> 0 by TARSKI:def 1;
hence thesis by A357,A360,FINSEQ_1:def 7;
end;
suppose
ex l being Nat st l in dom f5 & d=len(f4|n)+ l;
then consider l be Element of NAT such that
A361: l in dom f5 and
A362: d = len(f4|n)+ l;
f6.d = f5.l by A361,A362,FINSEQ_1:def 7;
hence thesis by A324,A361;
end;
end;
len f6 = len(f4|n) + len f5 by FINSEQ_1:22
.= p9 by A318,A319,A321;
then rng f6 = rng idseq p9 by A354,A355,Th40;
then M = Sum f6 by A354,RFINSEQ:9,26
.= Sum(f4|n) + Sum f5 by RVSUM_1:75
.= Sum(f4|n) + (m*p - Sum(f4/^n)) by A319,A317,Th47
.= Sum(f4|n) + m*p - Sum(f4/^n);
then (q-1)*M = p*(Sum f2) + 2*Sum(Sgm X) - m*p by A312,A314,A315;
then
A364: (q-'1)*M mod 2 = ((p*(Sum f2)-m*p) + 2*Sum(Sgm X)) mod 2 by A28,
XREAL_1:233
.= (p*(Sum f2)-m*p) mod 2 by NAT_D:61;
2 divides (q-'1)*M by A39,NAT_D:9;
then (q-'1)*M mod 2 = 0;
then 2 divides (p*((Sum f2)-m)) by A364,Lm1;
then (Sum f2),m are_congruent_mod 2 by A183,INT_2:25;
then (Sum f2) mod 2 = m mod 2 by NAT_D:64;
then (-1)|^(Sum f2) = (-1)|^m by Th45;
hence thesis by A1,A5,A294,Th41;
end;
hence thesis by A131,A186,NEWTON:8;
end;
theorem
p>2 & q>2 & p<>q & p mod 4 = 3 & q mod 4 = 3 implies Lege(p,q) = -Lege (q,p)
proof
assume that
A1: p>2 and
A2: q>2 and
A3: p<>q and
A4: p mod 4 = 3 and
A5: q mod 4 = 3;
q>1 by INT_2:def 4;
then
A6: q-'1 = q-1 by XREAL_1:233;
q = 4*(q div 4)+3 by A5,NAT_D:2;
then q-'1 = 2*(2*(q div 4)+1) by A6;
then
A7: (q-'1) div 2=2*(q div 4)+1;
p>1 by INT_2:def 4;
then
A8: p-'1 = p-1 by XREAL_1:233;
p=4*(p div 4)+3 by A4,NAT_D:2;
then p-'1 = 2*(2*(p div 4)+1) by A8;
then (p-'1) div 2=2*(p div 4)+1;
then
A9: Lege(p,q)*Lege(q,p) =(-1)|^((2*(p div 4)+1)*(2*(q div 4)+1)) by A1,A2,A3,A7
,Th49
.=((-1)|^(2*(p div 4)+1))|^(2*(q div 4)+1) by NEWTON:9
.= ((-1)|^(2*(p div 4))*(-1))|^(2*(q div 4)+1) by NEWTON:6
.= ((((-1)|^2)|^(p div 4))*(-1))|^(2*(q div 4)+1) by NEWTON:9
.= ((1|^2)|^(p div 4)*(-1))|^(2*(q div 4)+1) by WSIERP_1:1
.= (-1)|^(2*(q div 4))*(-1) by NEWTON:6
.= ((-1)|^2)|^(q div 4) * (-1) by NEWTON:9
.= (1|^2)|^(q div 4) *(-1) by WSIERP_1:1
.= 1*(-1);
per cases by Th25;
suppose
Lege(p,q) = 1;
hence thesis by A9;
end;
suppose
Lege(p,q) = 0;
hence thesis by A9;
end;
suppose
Lege(p,q) = -1;
hence thesis by A9;
end;
end;
theorem
p>2 & q>2 & p<>q & (p mod 4 = 1 or q mod 4 = 1) implies Lege(p,q) = Lege(q,p)
proof
assume that
A1: p>2 and
A2: q>2 and
A3: p<>q and
A4: p mod 4 = 1 or q mod 4 = 1;
p>1 by INT_2:def 4;
then
A5: p-'1 = p-1 by XREAL_1:233;
q>1 by INT_2:def 4;
then
A6: q-'1 = q-1 by XREAL_1:233;
per cases by A4;
suppose
p mod 4 = 1;
then p=4*(p div 4)+1 by NAT_D:2;
then p-'1 = 2*(2*(p div 4)) by A5;
then (p-'1) div 2 = 2*(p div 4);
then
A7: Lege(p,q)*Lege(q,p) = (-1)|^((2*(p div 4))*((q-'1) div 2)) by A1,A2,A3,Th49
.= ((-1)|^(2*(p div 4)))|^((q-'1) div 2) by NEWTON:9
.= (((-1)|^2)|^(p div 4))|^((q-'1) div 2) by NEWTON:9
.= ((1|^2)|^(p div 4))|^((q-'1) div 2) by WSIERP_1:1
.= 1;
per cases by Th25;
suppose
Lege(p,q)=1;
hence thesis by A7;
end;
suppose
Lege(p,q)=0;
hence thesis by A7;
end;
suppose
Lege(p,q)=-1;
hence thesis by A7;
end;
end;
suppose
q mod 4 = 1;
then q=4*(q div 4)+1 by NAT_D:2;
then q-'1 = 2*(2*(q div 4)) by A6;
then (q-'1) div 2 = 2*(q div 4);
then
A8: Lege(p,q)*Lege(q,p) = (-1)|^((2*(q div 4))*((p-'1) div 2)) by A1,A2,A3,Th49
.= ((-1)|^(2*(q div 4)))|^((p-'1) div 2) by NEWTON:9
.= (((-1)|^2)|^(q div 4))|^((p-'1) div 2) by NEWTON:9
.= ((1|^2)|^(q div 4))|^((p-'1) div 2) by WSIERP_1:1
.= 1;
per cases by Th25;
suppose
Lege(p,q)=1;
hence thesis by A8;
end;
suppose
Lege(p,q)=0;
hence thesis by A8;
end;
suppose
Lege(p,q)=-1;
hence thesis by A8;
end;
end;
end;