:: Gauss Lemma and Law of Quadratic Reciprocity :: by Li Yan , Xiquan Liang and Junjie Zhao :: :: Received October 9, 2007 :: Copyright (c) 2007 Association of Mizar Users environ vocabularies RELAT_1, FINSEQ_1, INT_1, INT_2, ABSVALUE, FUNCT_1, GROUP_1, ARYTM_3, ORDINAL2, CARD_3, FINSET_1, ARYTM_1, BOOLE, NAT_1, NAT_LAT, FUNCOP_1, CARD_1, SQUARE_1, MATRIX_2, RLVECT_1, FINSEQ_5, FINSEQ_2, RFINSEQ, FINSEQ_4, FINSEQ_7, TARSKI, SUBLEMMA, PROB_1, INT_5, FILTER_0, ARYTM; notations 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, FINSEQ_5, FINSEQ_2, EULER_2, NEWTON, GOBRD10, FINSEQ_7, REAL_1, PEPIN, TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, NUMBERS, XXREAL_0, NAT_1, DOMAIN_1, FINSEQ_1, BINARITH, RFINSEQ, FUNCOP_1, CALCUL_2, ZFMISC_1, CARD_3, WSIERP_1, BINOP_1, PROB_3, RECDEF_1; constructors BINARITH, ABIAN, WSIERP_1, PEPIN, UPROOTS, NAT_3, NAT_D, REALSET1, GR_CY_1, FINSEQ_5, GOBRD10, EULER_2, RFINSEQ, GROUP_4, FINSEQ_7, REAL_1, WELLORD2, CALCUL_2, SETFAM_1, PROB_3, SEQ_1, RECDEF_1, BINOP_2; 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, CALCUL_2, FUNCT_1, CARD_1, NEWTON, SUBSET_1, POLYNOM1, VALUED_0, VALUED_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions INT_1, FUNCT_1, XCMPLX_0, SQUARE_1, FINSEQ_2, TARSKI, CALCUL_2, CARD_3; theorems FINSEQ_1, FINSEQ_7, RELAT_1, FINSEQ_3, FINSEQ_2, ABSVALUE, FINSEQ_5, BINARITH, EULER_2, INT_3, SEQ_2, FINSEQ_4, FUNCT_2, XBOOLE_0, NAT_3, NEWTON, INT_2, NAT_2, WSIERP_1, SQUARE_1, CARD_1, PEPIN, NAT_1, XCMPLX_1, XREAL_1, HEYTING3, ORDINAL1, EULER_1, XBOOLE_1, TARSKI, RVSUM_1, FINSET_1, NUMBERS, INT_1, FUNCT_1, CARD_4, FUNCOP_1, REAL_1, XXREAL_0, NAT_D, HILBERT3, GOBRD10, SERIES_2, GRAPH_5, HILBERT2, RFINSEQ, ZFMISC_1, CARD_2, XREAL_0, FINSEQ_6, CALCUL_2, NAT_4, PROB_3, TOPREAL7, POLYNOM1, CARD_3, REAL_3, PRE_FF, INT_4, VALUED_1; schemes NAT_1, FUNCT_2, RECDEF_1, FINSEQ_2, FUNCT_7, FINSEQ_1; begin reserve X for Subset of INT, i,i1,i2,i3,i4,i5,j,m,m1,m2,m3,r,s,a,b,c,c1,c2,x,y for Integer, q,n1,n2,n3,d,e,k,n for Nat, fp,fk,fr for FinSequence of INT, fp1,fp2 for FinSequence of NAT, 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 A1: i1 divides i2 & i1 divides i3; then consider i4 such that A2: i2=i1*i4 by INT_1:def 9; consider i5 such that A3: i3=i1*i5 by A1,INT_1:def 9; i2-i3=i1*(i4-i5) by A2,A3; hence thesis by INT_1:def 9; end; theorem Th2: i divides a & i divides (a-b) implies i divides b proof assume A1: i divides a & i divides (a-b); then A2: i divides -(a-b) by INT_2:14; b=-(a-b)+a; hence thesis by A1,A2,WSIERP_1:9; end; Lm1: (x divides y implies y mod x = 0) & (x<>0 & y mod x = 0 implies x divides y) proof A1: x divides y implies y mod x = 0 proof assume x divides y; then consider i such that A2: y = x * i by INT_1:def 9; y mod x = (x * i + 0) mod x by A2 .= 0 mod x by EULER_1:13 .= 0 by INT_4:12; hence thesis; end; x<>0 & y mod x = 0 implies x divides y proof assume A3: x<>0 & y mod x = 0; then y = (y div x) * x + (y mod x) by INT_1:86 .= (y div x) * x by A3; hence thesis by INT_1:def 9; end; hence thesis by A1; 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:14; take y = 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 & (for d st d in dom fr1 holds fr1.d = (fp.d) * x|^(d-'1)) & f1.x = Sum fr1 by A4; consider fr2 being FinSequence of INT such that A7: len fr2 = len fp & (for d st d in dom fr2 holds fr2.d = (fp.d) * x|^(d-'1)) & f2.x = Sum fr2 by A5; A8: dom fr1 = dom fr2 by A6,A7,FINSEQ_3:31; for d being Nat st d in dom fr1 holds fr1.d = fr2.d proof let d be Nat; assume A9: d in dom fr1; hence fr2.d = (fp.d) * x|^(d-'1) by A7,A8 .= fr1.d by A6,A9; end; hence f1.x = f2.x by A6,A7,A8,FINSEQ_1:17; end; hence f1 = f2 by FUNCT_2:113; end; end; registration let fp be FinSequence of INT,x be Integer; cluster (Poly-INT fp).x -> integer; coherence; end; theorem Th3: len fp = 1 implies (Poly-INT fp) = INT --> fp.1 proof assume A1: len fp = 1; for x being set st x in dom Poly-INT fp holds (Poly-INT fp).x = fp.1 proof let x be set; 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 & (for d st d in dom fr holds fr.d = (fp.d) * x|^(d-'1)) & (Poly-INT fp).x = Sum fr by Def1; A3: fr = <*fr.1*> by A1,A2,FINSEQ_1:57; 1 in dom fr by A1,A2,FINSEQ_3:27; then fr.1 = (fp.1) * x|^(1-'1) by A2 .= fp.1 * x|^0 by BINARITH:51 .= fp.1 * 1 by NEWTON:9; hence thesis by A2,A3,RVSUM_1:103; end; then Poly-INT fp = dom Poly-INT fp --> fp.1 by FUNCOP_1:17; 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 & (for d st d in dom fr holds fr.d = (fp.d) * x|^(d-'1)) & (Poly-INT fp).x = Sum fr by Def1; A3: fr = <*fr.1*> by A1,A2,FINSEQ_1:57; 1 in dom fr by A1,A2,FINSEQ_3:27; then fr.1 = (fp.1) * x|^(1-'1) by A2 .= fp.1 * x|^0 by BINARITH:51 .= fp.1 * 1 by NEWTON:9; hence thesis by A2,A3,RVSUM_1:103; 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: P[0] proof let f,f1,f2; assume A2: len f = 0+1 & len f1 = len f & len f2 = len f & (for d st d in dom f holds f.d = f1.d - f2.d); 0+1 in Seg (0+1) by FINSEQ_1:6; then 1 in dom f by A2,FINSEQ_1:def 3; then f.1 = f1.1 - f2.1 by A2; then A3: f = <*f1.1 - f2.1*> by A2,FINSEQ_1:57; take fr = <*>REAL; thus thesis by A2,A3,RVSUM_1:102,103; end; A4: for n st P[n] holds P[n+1] proof let n; assume A5: P[n]; let f,f1,f2; assume A6: len f = (n+1)+1 & len f1 = len f & len f2 = len f & (for d st d in dom f holds f.d = f1.d - f2.d); set f3 = f|Seg(n+1); reconsider f3 as FinSequence of REAL by FINSEQ_1:23; A7: dom f3 = Seg(n+1) & f = f3^<*f.(n+1+1)*> by A6,FINSEQ_3:60,61; then A8: len f3 = n+1 by FINSEQ_1:def 3; set ff1 = f1|Seg(n+1); reconsider ff1 as FinSequence of REAL by FINSEQ_1:23; A9: len ff1 = n+1 & f1 = ff1^<*f1.((n+1)+1)*> by A6,FINSEQ_3:59,61; set ff2 = f2|Seg(n+1); reconsider ff2 as FinSequence of REAL by FINSEQ_1:23; A10: len ff2 = n+1 & f2 = ff2^<*f2.((n+1)+1)*> by A6,FINSEQ_3:59,61; for d st d in dom f3 holds f3.d = ff1.d - ff2.d proof let d; assume A11: d in dom f3; A12: dom f3 c= dom f by A7,FINSEQ_1:39; A13: f3.d = f.d by A7,A11,FINSEQ_1:def 7 .= f1.d - f2.d by A6,A11,A12; d in dom ff1 & d in dom ff2 by A7,A9,A10,A11,FINSEQ_1:def 3; then f1.d = ff1.d & f2.d = ff2.d by A9,A10,FINSEQ_1:def 7; hence thesis by A13; end; then consider f4 being FinSequence of REAL such that A14: len f4 = len f3 - 1 & (for d st d in dom f4 holds f4.d = ff1.d - ff2.(d+1)) & Sum f3 = Sum f4 + ff1.(n+1) - ff2.1 by A5,A8,A9,A10; ff1 <> {} & ff2 <> {} by A9,A10; then 1 in dom ff2 & (n+1) in dom ff1 by A9,FINSEQ_5:6; then ff2.1 = f2.1 & ff1.(n+1) = f1.(n+1) by A9,A10,FINSEQ_1:def 7; then consider f4 being FinSequence of REAL such that A15: len f4 = len f3 - 1 & (for d st d in dom f4 holds f4.d=ff1.d - ff2.(d + 1)) & Sum f3 = Sum f4 + f1.(n+1) - f2.1 by A14; take f5 = f4^<*f1.(n+1) - f2.(n+2)*>; f1.(n+1) - f2.(n+2) is Element of REAL by XREAL_0:def 1; then f4 is FinSequence of REAL & <*f1.(n+1) - f2.(n+2)*> is FinSequence of REAL by FINSEQ_1:95; then reconsider f5 as FinSequence of REAL by FINSEQ_1:96; A16: len f5 = len f4 + 1 by FINSEQ_2:19 .= len f - 1 by A6,A7,A15,FINSEQ_1:def 3; A17: len f4 + 1 = n + 1 by A7,A15,FINSEQ_1:def 3; A18: 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:19; then d in Seg len f4 \/{len f4 + 1} by FINSEQ_1:11; then A19: d in Seg len f4 or d in {len f4 + 1} by XBOOLE_0:def 2; per cases by A19,TARSKI:def 1; suppose A20: d in Seg len f4; then A21: d in dom f4 by FINSEQ_1:def 3; then A22: f5.d = f4.d by FINSEQ_1:def 7 .= ff1.d - ff2.(d+1) by A15,A21; len f4 <= len ff1 & len f4 + 1 <= len ff2 by A6,A8,A9,A15,FINSEQ_3:59,XREAL_1:149; then dom f4 c= dom ff1 by FINSEQ_3:32; then A23: f1.d = ff1.d by A9,A21,FINSEQ_1:def 7; d+1 in Seg(len f4 + 1) by A20,FINSEQ_1:81; then d+1 in Seg len ff2 by A6,A8,A15,FINSEQ_3:59; then d+1 in dom ff2 by FINSEQ_1:def 3; hence thesis by A10,A22,A23,FINSEQ_1:def 7; end; suppose A24: d = len f4 + 1; 1 in Seg 1 by FINSEQ_1:4,TARSKI:def 1; then 1 in dom <*f1.(n+1) - f2.(n+2)*> by FINSEQ_1:55; then f5.d = <*f1.(n+1) - f2.(n+2)*>.1 by A24,FINSEQ_1:def 7 .= f1.d - f2.(d+1) by A17,A24,FINSEQ_1:57; hence thesis; end; end; (n+1)+1 in Seg ((n+1)+1) by FINSEQ_1:6; then ((n+1)+1) in dom f by A6,FINSEQ_1:def 3; then A25: f.((n+1)+1) = f1.((n+1)+1) - f2.((n+1)+1) by A6; Sum f = Sum f4 + f1.(n+1) - f2.1 + f.(n+1+1) by A7,A15,RVSUM_1:104 .= Sum f4 + (f1.(n+1) - f2.(n+2)) + f1.((n+1)+1) - f2.1 by A25 .= Sum f5 + f1.((n+1)+1) - f2.1 by RVSUM_1:104; hence thesis by A16,A18; end; for n holds P[n] from NAT_1:sch 2(A1,A4); 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:6; 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:13; let a be Integer; defpred P[Nat,set,set] means ex i st i = $2 & $3 = fp.(n+2-$1) +a*i; reconsider n1=n+1 as Element of NAT; A2: for d being Element of 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 Element of NAT; assume 1 <= d & 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 Element of 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; consider f1 being FinSequence of INT such that A5: len f1 = len fp & (for d st d in dom f1 holds f1.d = (fp.d) * x|^(d-'1)) & (Poly-INT fp).x = Sum f1 by Def1; f1 <> {} by A1,A5; then 1 in dom f1 & n+2 in dom f1 by A1,A5,FINSEQ_5:6; then f1.1 = (fp.1)*x|^(1-'1) & f1.(n+2) = (fp.(n+2)) * x|^((n+2)-'1) by A5; then f1.1=(fp.1)*x|^0 & f1.(n+2)=(fp.(n+2))*x|^((n+1)+1-'1) by BINARITH: 51; then A6: f1.1 = (fp.1)*1 & f1.(n+2)=(fp.(n+2))*x|^(n+1) by BINARITH:39, NEWTON :9; consider f2 being FinSequence of INT such that A7: len f2 = len fr & (for d st d in dom f2 holds f2.d = (fr.d) * x|^(d-'1)) & (Poly-INT fr).x = Sum f2 by Def1; set f3 = (x-a)*f2; A8: 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 A9: k in dom f3; then A10: k >= 1 by FINSEQ_3:27; A11: k in dom f2 by A9,VALUED_1:def 5; thus f3.k = (x-a)*(f2.k) by A9,VALUED_1:def 5 .= (x-a)*((fr.k) * x|^(k-'1)) by A7,A11 .= (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:11 .= (fr.k)*x|^k - a*(fr.k) * x|^(k-'1) by A10,BINARITH:53; end; deffunc F(Nat) = (fr.$1)*x|^$1; deffunc FF(Nat) = a*(fr.$1) * x|^($1-'1); reconsider n as Element of NAT by ORDINAL1:def 13; consider f4 being FinSequence such that A12: len f4 = n+1 & for d being Nat st d in dom f4 holds f4.d=F(d) from FINSEQ_1:sch 2; consider f5 being FinSequence such that A13: len f5 = n+1 & for d being Nat st d in dom f5 holds f5.d=FF(d) from FINSEQ_1:sch 2; f4 <> {} & f5 <> {} by A12,A13; then 1 in dom f5 & n+1 in dom f4 by A12,FINSEQ_5:6; then f4.(n+1)=(fr.(n+1))*x|^(n+1) & f5.1 = a*(fr.1) * x|^(1-'1) by A12, A13; then f4.(n+1)=(fp.(n+2))*x|^(n+1) & f5.1 = a*(fr.1)*x|^0 by A3,BINARITH:51,FINSEQ_5:65; then A14: f4.(n+1) = (fp.(n+2))*x|^(n+1) & f5.1 = a*(fr.1)*1 by NEWTON:9; 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 13; assume d in dom f4; then f4.d1 = (fr.d1)*x|^d1 by A12; hence thesis by INT_1:def 2; end; then reconsider f4 as FinSequence of INT by FINSEQ_2:14; 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 A13; hence thesis by INT_1:def 2; end; then reconsider f5 as FinSequence of INT by FINSEQ_2:14; A15: dom f3 = dom f2 by VALUED_1:def 5; then A16: dom f3 = dom f4 & dom f3 = dom f5 by A4,A7,A12,A13,FINSEQ_3:31; A17: len f3 = len f2 by A15,FINSEQ_3:31; A18: for d st d in dom f3 holds f3.d = f4.d - f5.d proof let d; assume A19: d in dom f3; then f4.d = (fr.d)*x|^d & f5.d = a*(fr.d) * x|^(d-'1) by A12,A13,A16; hence thesis by A8,A19; end; f4 is FinSequence of REAL & f5 is FinSequence of REAL by FINSEQ_3:126; then consider f6 being FinSequence of REAL such that A20: len f6 = len f3 - 1 & (for d st d in dom f6 holds f6.d = f4.d - f5.(d + 1)) & Sum f3 = Sum f6 + f4.(n+1) - f5.1 by A4,A7,A12,A13,A17,A18,Th5; A21: len f6 <= len f3 by A4,A7,A17,A20,XREAL_1:147; then A22: dom f6 c= dom f3 by FINSEQ_3:32; A23: for d being Element of NAT st d in dom f6 holds f6.d = f1.(d+1) proof let d be Element of NAT; assume A24: d in dom f6; then d in Seg n by A4,A7,A17,A20,FINSEQ_1:def 3; then A25: d <= n & d >= 1 by FINSEQ_1:3; then d < n+1 by XREAL_1:147; then d+1 in Seg (n+1) by FINSEQ_3:12; then A26: d+1 in dom f5 & d+1 in dom p by A3,A13,FINSEQ_1:def 3; A27: dom f6 c= dom p by A3,A4,A7,A17,A21,FINSEQ_3:32; A28: n-d >= 0 & n-d <= n-1 by A25,XREAL_1:12,50; then n-d+1 >= 0+1 by XREAL_1:8; then reconsider d'=n-d+1 as Element of NAT by INT_1:16; d' >= 0+1 & d' <= (n-1)+1 by A28,XREAL_1:8; then d' >= 1 & d' < n+1 by XREAL_1:147; then consider i such that A29: i = p.d' & p.(d'+1) = fp.(n+2-d') +a*i by A3; d+0 < n+2 by A25,XREAL_1:10; then d+1 in Seg (n+2) by FINSEQ_3:12; then A30: d+1 in dom f1 by A1,A5,FINSEQ_1:def 3; thus f6.d = f4.d - f5.(d + 1) by A20,A24 .= (fr.d)*x|^d - f5.(d+1) by A12,A16,A22,A24 .= (fr.d)*x|^d - a*fr.(d+1) * x|^(d+1-'1) by A13,A26 .= (fr.d)*x|^d - a*(fr.(d+1)) * x|^d by BINARITH:39 .= ((fr.d) - a*fr.(d+1))* x|^d .= (p.((n+1)-d+1) - a*fr.(d+1))* x|^d by A3,A24,A27,FINSEQ_5:61 .= (p.((n-d+1)+1)-a*p.((n+1)-(d+1)+1))* x|^d by A3,A26,FINSEQ_5:61 .= fp.(d+1)* x|^(d+1-'1) by A29,BINARITH:39 .= f1.(d+1) by A5,A30; end; f1 = <*f1.1*>^f6^<*f1.(n+2)*> proof set K = <*f1.1*>^f6^<*f1.(n+2)*>; len K = len (<*f1.1*>^(f6^<*f1.(n+2)*>)) by FINSEQ_1:45 .= 1+len (f6^<*f1.(n+2)*>) by FINSEQ_5:8 .= 1+len f6 +1 by FINSEQ_2:19 .= len f1 by A1,A4,A5,A7,A17,A20; then A31: dom f1 = dom K by FINSEQ_3:31; for d being Nat st d in dom f1 holds f1.d = K.d proof let d be Nat; assume d in dom f1; then A32: d>=1 & d<=n+2 by A1,A5,FINSEQ_3:27; per cases by A32,REAL_1:def 5; suppose A33: d=1; hence K.d = (<*f1.1*>^(f6^<*f1.(n+2)*>)).1 by FINSEQ_1:45 .= f1.d by A33,FINSEQ_1:58; end; suppose d>1 & d0 & d-1=0+1 & d-1<=n+1-1 by A34,INT_1:20; then w in Seg n by FINSEQ_1:3; then A35: w in dom f6 by A4,A7,A17,A20,FINSEQ_1:def 3; then A36: w in dom (f6^<*f1.(n+2)*>) by FINSEQ_2:18; thus K.d = (<*f1.1*>^(f6^<*f1.(n+2)*>)).(w+1) by FINSEQ_1:45 .= (f6^<*f1.(n+2)*>).w by A36,FINSEQ_3:112 .= f6.w by A35,FINSEQ_1:def 7 .= f1.(w+1) by A23,A35 .= f1.d; end; suppose A37: d=n+2; set K1 = <*f1.1*>^f6; thus K.d = K.((n+1)+1) by A37 .= K.(len K1 +1) by A4,A7,A17,A20,FINSEQ_5:8 .= f1.d by A37,FINSEQ_1:59; end; end; hence thesis by A31,FINSEQ_1:17; end; then Sum f1 = Sum (<*f1.1*>^(f6^<*f1.(n+2)*>)) by FINSEQ_1:45 .= f1.1 + Sum (f6^<*f1.(n+2)*>) by RVSUM_1:106 .= f1.1 + (Sum f6 + f1.(n+2)) by RVSUM_1:104 .= Sum ((x-a)*f2) + r by A6,A14,A20 .= (x-a) * (Poly-INT fr).x + r by A7,RVSUM_1:117; hence thesis by A5; end; hence thesis by A3,FINSEQ_5:65,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:16; p divides i*j by A1; hence thesis by NEWTON:98; end; suppose i>=0 & j<0; then i>=0 & -j>0 by XREAL_1:60; then reconsider i,j'=-j as Element of NAT by INT_1:16; p divides -(i*j) by A1,INT_2:14; then p divides i*j'; then p divides i or p divides j' by NEWTON:98; hence thesis by INT_2:14; end; suppose i<0 & j>=0; then -i>0 & j>=0 by XREAL_1:60; then reconsider i'=-i,j as Element of NAT by INT_1:16; p divides -(i*j) by A1,INT_2:14; then p divides i'*j; then p divides i' or p divides j by NEWTON:98; hence thesis by INT_2:14; end; suppose i<0 & j<0; then -i>0 & -j>0 by XREAL_1:60; then reconsider i'=-i,j'=-j as Element of NAT by INT_1:16; p divides i'*j' by A1; then p divides i' or p divides j' by NEWTON:98; hence thesis by INT_2:14; 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: P[0] proof let fp; assume A2: len fp = 0+1 & p>2 & 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 A3: (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; fr <> {} by A3; then 1 in dom fr by FINSEQ_5:6; then A4: (Poly-INT fp).(fr.1) mod p=0 by A3; A5: fr.1 in INT by INT_1:def 2; (Poly-INT fp).(fr.1) = (INT --> fp.1).(fr.1) by A2,Th3 .= fp.1 by A5,FUNCOP_1:13; hence contradiction by A2,A4,Lm1; end; A6: for n st P[n] holds P[n+1] proof let n; assume A7: P[n]; let fp; assume A8: len fp = (n+1)+1 & p>2 & not p divides fp.(n+1+1); per cases; suppose A9: 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 A10: (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; fr <> {} by A10; then 1 in dom fr by FINSEQ_5:6; then (Poly-INT fp).(fr.1) mod p=0 by A10; hence contradiction by A9; end; suppose ex a being Integer st (Poly-INT fp).a mod p = 0; then consider a being Integer such that A11: (Poly-INT fp).a mod p=0; consider fk,r such that A12: len fk = n+1 & (for x being Element of INT holds (Poly-INT fp).x =(x-a)*(Poly-INT fk).x +r) & fp.(n+2)=fk.(n+1) by A8,Th6; a is Element of INT by INT_1:def 2; then A13: (Poly-INT fp).a mod p =((a-a)*(Poly-INT fk).a +r) mod p by A12 .= r mod p; 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 A14: (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; A15: 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; assume A16: d in dom f; f.d is Element of INT by INT_1:def 2; then (Poly-INT fp).(f.d) mod p = (((f.d-a)*(Poly-INT fk).(f.d)) +r) mod p by A12 .=(((f.d-a)*(Poly-INT fk).(f.d)) mod p + (r mod p)) mod p by INT_3:14 .= ((f.d-a)*(Poly-INT fk).(f.d)) mod p by A11,A13,INT_3:13; then ((f.d-a)*(Poly-INT fk).(f.d)) mod p = 0 by A14,A16; hence thesis by INT_1:89; end; per cases; suppose A17: 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 A18: d in dom f; then p divides (f.d -a)*(Poly-INT fk).(f.d) by A15; then p divides (f.d -a) or p divides (Poly-INT fk).(f.d) by Th7; hence thesis by A17,A18,INT_1:89; end; then len f <= n by A7,A8,A12,A14; hence contradiction by A14,XREAL_1:147; end; suppose ex d st d in dom f & p divides (f.d - a); then consider d' being Element of NAT such that A19: d' in dom f & p divides (f.d' - a); set f' = f - {f.d'}; A20: f is one-to-one proof let x1,x2 be set; assume A21: x1 in dom f & x2 in dom f & f.x1 = f.x2 & x1 <> x2; then reconsider x1,x2 as Element of NAT; not f.x1,f.x2 are_congruent_mod p by A14,A21; hence contradiction by A21,INT_1:32; end; then A22: f' is one-to-one by FINSEQ_3:94; A23: for d st d in dom f' holds not p divides (f'.d - a) proof given k being Nat such that A24: k in dom f' & p divides (f'.k -a); f'.k in rng f' by A24,FUNCT_1:12; then f'.k in rng f \ {f.d'} by FINSEQ_3:72; then A25: f'.k in rng f & not f'.k in {f.d'} by XBOOLE_0:def 4; then consider w being set such that A26: w in dom f & f.w = f'.k by FUNCT_1:def 5; reconsider w as Element of NAT by A26; p divides ((f.w - a)-(f.d' - a)) by A19,A24,A26,Th1; then p divides (f.w - f.d'); then A27: f.w,f.d' are_congruent_mod p by INT_2:19; w <> d' by A25,A26,TARSKI:def 1; hence contradiction by A14,A19,A26,A27; end; A28: for d st d in dom f' holds (Poly-INT fk).(f'.d) mod p = 0 proof let d; assume A29: d in dom f'; then f'.d in rng f' by FUNCT_1:12; then f'.d in rng f \ {f.d'} by FINSEQ_3:72; then f'.d in rng f & not f'.d in {f.d'} by XBOOLE_0:def 4; then consider w being set such that A30: w in dom f & f.w = f'.d by FUNCT_1:def 5; p divides (f'.d -a)*(Poly-INT fk).(f'.d) by A15,A30; then p divides (f'.d -a) or p divides (Poly-INT fk).(f'.d) by Th7; hence thesis by A23,A29,INT_1:89; end; A31: 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 A32: d in dom f' & e in dom f' & d<>e; then f'.d in rng f' & f'.e in rng f' by FUNCT_1:12; then f'.d in rng f \ {f.d'} & f'.e in rng f \ {f.d'} by FINSEQ_3:72; then A33: f'.d in rng f & f'.e in rng f by XBOOLE_0:def 4; then consider w1 being set such that A34: w1 in dom f & f'.d = f.w1 by FUNCT_1:def 5; consider w2 being set such that A35: w2 in dom f & f'.e = f.w2 by A33,FUNCT_1:def 5; reconsider w1,w2 as Element of NAT by A34,A35; w1 <> w2 by A22,A32,A34,A35,FUNCT_1:def 8; hence thesis by A14,A34,A35; end; f.d' in rng f by A19,FUNCT_1:12; then len f' = len f - 1 by A20,FINSEQ_3:97; then len f' > (n+1)-1 by A14,XREAL_1:11; hence contradiction by A7,A8,A12,A28,A31; end; end; end; for n holds P[n] from NAT_1:sch 2(A1,A6); hence thesis; end; definition let a be Integer, m be Nat; pred a is_quadratic_residue_mod m means :Def2: ex x being Integer st (x^2 - a) mod m = 0; end; reserve b,m for Nat; theorem Th9: a gcd m = 1 implies a^2 is_quadratic_residue_mod m proof assume a gcd m = 1; (a^2 - a^2) mod m = 0 by INT_4:12; hence thesis by Def2; end; theorem 1 is_quadratic_residue_mod 2 proof 1 gcd 2 = 1 by WSIERP_1:13; then 1^2 is_quadratic_residue_mod 2 by Th9; hence thesis; end; theorem Th11: i gcd m = 1 & i is_quadratic_residue_mod m & i,j are_congruent_mod m implies j is_quadratic_residue_mod m proof assume A1: i gcd m = 1 & i is_quadratic_residue_mod m & i,j are_congruent_mod m; then consider x being Integer such that A2: (x^2 - i) mod m = 0 by Def2; m divides (i - j) by A1,INT_2:19; then A3: (i - j) mod m = 0 by Lm1; (x^2 - j) mod m = ((x^2 - i) + (i - j)) mod m .= (((x^2 - i) mod m) + ((i - j) mod m)) mod m by INT_3:14 .= 0 by A2,A3,INT_3:13; hence thesis by Def2; end; Lm2: i,p are_relative_prime or p divides i proof per cases; suppose i>=0; then reconsider i as Element of NAT by INT_1:16; i,p are_relative_prime or (i hcf p) = p by PEPIN:2; hence thesis by NAT_D:def 5; end; suppose A1: i<0; then -i>0 by XREAL_1:60; then reconsider m = -i as Element of NAT by INT_1:16; A2: m,p are_relative_prime or (m hcf p) = p by PEPIN:2; per cases by A2,NAT_D:def 5; suppose A3: m,p are_relative_prime; m = abs i by A1,ABSVALUE:def 1; then i gcd p = m hcf abs(p) by INT_2:51 .= m hcf p by ABSVALUE:def 1 .= 1 by A3,INT_2:def 4; hence thesis by INT_2:def 4; 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 by INT_1:def 9; end; end; end; theorem Th12: i divides j implies i gcd j = abs(i) proof assume i divides j; then abs(i) divides abs(j) by INT_2:21; then abs i gcd abs j = abs(i) by NEWTON:62; hence thesis by INT_2:51; 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; assume A1: i mod m = j mod m; defpred P[Nat] means i|^$1 mod m = j|^$1 mod m; A2: P[0] proof i|^0 = 1 & j|^0 = 1 by NEWTON:9; hence thesis; end; A3: for n being Element of NAT st P[n] holds P[n+1] proof let n be Element of NAT; assume A4: P[n]; thus i|^(n+1) mod m = ((i|^n)*i) mod m by NEWTON:11 .= (((j|^n) mod m)*(j mod m)) mod m by A1,A4,INT_3:15 .= ((j|^n)*j) mod m by INT_3:15 .= j|^(n+1) mod m by NEWTON:11; end; A5: for n being Element of NAT holds P[n] from NAT_1:sch 1(A2,A3); for n holds P[n] proof let n; n in NAT by ORDINAL1:def 13; hence thesis by A5; end; hence thesis; end; theorem Th14: a gcd p = 1 & (x^2 - a) mod p = 0 implies x,p are_relative_prime proof assume A1: a gcd p = 1 & (x^2 - a) mod p = 0; then A2: p divides (x^2 - a) by Lm1; assume not x,p are_relative_prime; then p divides x^2 by Lm2,INT_2:12; then p divides (x^2 - (x^2 - a)) by A2,Th1; then p gcd a = abs(p) by Th12 .= p by ABSVALUE:def 1; hence contradiction by A1,INT_2:def 5; 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 A1: p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p; then consider x such that A2: (x^2 - a) mod p = 0 by Def2; A3: not x,(-x) are_congruent_mod p proof assume x,(-x) are_congruent_mod p; then p divides (x - (-x)) by INT_2:19; then A4: p divides 2*x; 2,p are_relative_prime by A1,INT_2:44,47; then 2 hcf p = 1 by INT_2:def 4; then p divides x by A4,WSIERP_1:36; then consider i being Integer such that A5: x = p * i by INT_1:def 9; x <> 0 proof assume x = 0; then p divides (-a) by A2,INT_1:89; then p divides a*1 by INT_2:14; then p <= 1 by A1,NAT_D:7,WSIERP_1:36; hence contradiction by INT_2:def 5; end; then A6: i <> 0 by A5; x gcd p = p*i gcd p*1 by A5 .= p*(i gcd 1) by A6,EULER_1:16 .= p*1 by WSIERP_1:13; then x gcd p <> 1 by INT_2:def 5; then not x,p are_relative_prime by INT_2:def 4; hence contradiction by A1,A2,Th14; end; take x; take y = -x; thus thesis by A2,A3; end; registration let fp be FinSequence of NAT, d; cluster fp.d -> natural; coherence; 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 hcf 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 assume p > 2; then p is odd by PEPIN:17; then A1: p-1 is even by HILBERT3:2; A3: p>1 by INT_2:def 5; then A4: p-'1 = p-1 by BINARITH:50; then 2 divides (p-'1) by A1,PEPIN:22; then (p-'1) mod 2 = 0 by PEPIN:6; then A5: (p-'1) div 2 = (p-'1)/2 by PEPIN:68; deffunc F(Nat) = $1^2; consider fp being FinSequence such that A6: 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 A6; hence thesis; end; then reconsider fp as FinSequence of NAT by FINSEQ_2:14; A7: for d st d in dom fp holds d hcf p = 1 proof let d; assume d in dom fp; then d in Seg ((p-'1) div 2) by A6,FINSEQ_1:def 3; then A8: d >= 1 & d <= (p-'1) div 2 by FINSEQ_1:3; then A9: 2*d <= (p-'1)/2*2 by A5,XREAL_1:66; 1*d <= 2*d by XREAL_1:66; then d <= p-'1 by A9,XXREAL_0:2; then d < p by A4,XREAL_1:149; then d,p are_relative_prime by A8,EULER_1:3; hence thesis by INT_2:def 4; end; A10: for d st d in dom fp holds fp.d hcf p = 1 proof let d; assume A11: d in dom fp; d hcf p = 1 by A7,A11; then d^2 hcf p = 1 by WSIERP_1:12; hence thesis by A6,A11; end; A13: for d st d in dom fp holds fp.d is_quadratic_residue_mod p proof let d; assume A14: d in dom fp; then d hcf p = 1 by A7; then d^2 is_quadratic_residue_mod p by Th9; hence thesis by A6,A14; end; A15: 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 let d,e; assume A16: d in dom fp & e in dom fp & d<>e; then d in Seg ((p-'1) div 2) & e in Seg ((p-'1) div 2) by A6,FINSEQ_1:def 3; then A17: d >= 1 & d <= (p-'1) div 2 & e >= 1 & e <= (p-'1) div 2 by FINSEQ_1:3; then d+e >= 1+1 & d+e <= (p-'1) div 2 + ((p-'1) div 2) by XREAL_1:9; then d+e <> 0 & d+e < p by A4,A5,XREAL_1:149; then (d+e),p are_relative_prime by EULER_1:3; then A18: (d+e) gcd p = 1 by INT_2:def 4; assume fp.d,fp.e are_congruent_mod p; then p divides (fp.d - fp.e) by INT_2:19; then p divides (d^2 - fp.e) by A6,A16; then p divides (d^2 - e^2) by A6,A16; then A19: p divides (d - e)*(d+e); d-e <> 0 by A16; then abs(p) <= abs(d-e) by A18,A19,INT_4:6,WSIERP_1:36; then A20: p <= abs(d-e) by ABSVALUE:def 1; 1-((p-'1) div 2) <= d-e & d-e <= ((p-'1) div 2) - 1 by A17,XREAL_1:15; then -(((p-'1) div 2) - 1) <= d-e & d-e <= ((p-'1) div 2) - 1; then A21: abs(d-e) <= ((p-'1) div 2) - 1 by ABSVALUE:12; p-1>0 by A3,XREAL_1:52; then (p-1)/2 < (p-1)/1 by XREAL_1:78; then (p-'1) div 2 < p by A4,A5,XREAL_1:149; then ((p-'1) div 2) - 1 < p by XREAL_1:149; hence contradiction by A20,A21,XXREAL_0:2; end; take fp; thus thesis by A6,A10,A13,A15; 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 A1: p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p; then consider s being Integer such that A2: (s^2 - a) mod p = 0 by Def2; p is odd by A1,PEPIN:17; then A3: p-1 is even by HILBERT3:2; p>1 by INT_2:def 5; then p-'1 is even by A3,BINARITH:50; then 2 divides (p-'1) by PEPIN:22; then A4: p-'1 = 2*((p-'1) div 2) by NAT_D:3; A5: s,p are_relative_prime by A1,A2,Th14; p divides (s^2 - a) by A2,INT_1:89; then s^2,a are_congruent_mod p by INT_2:19; then a mod p = s^2 mod p by INT_3:12; then A6: 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:100 .= s|^(p-'1) mod p by A4,NEWTON:14; per cases; suppose s>=0; then reconsider s as Element of NAT by INT_1:16; s,p are_relative_prime by A1,A2,Th14; hence thesis by A6,PEPIN:38; end; suppose A7: s<0; then -s > 0 by XREAL_1:60; then reconsider s' = -s as Element of NAT by INT_1:16; A8: abs p = p by ABSVALUE:def 1; s' hcf p = abs(s) gcd p by A7,ABSVALUE:def 1 .= s gcd p by A8,INT_2:51 .= 1 by A5,INT_2:def 4; then s',p are_relative_prime by INT_2:def 4; then A9: s'|^(p-'1) mod p = 1 by PEPIN:38; s|^(p-'1) mod p = (s|^2)|^((p-'1) div 2) mod p by A4,NEWTON:14 .= ((-s)|^2)|^((p-'1) div 2) mod p by WSIERP_1:2 .= 1 by A4,A9,NEWTON:14; hence thesis by A6; 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 A1: p>2 & b gcd p = 1 & not b is_quadratic_residue_mod p; reconsider b as Element of NAT by ORDINAL1:def 13; b,p are_relative_prime by A1,INT_2:def 4; then A2: (b|^(p-'1)) mod p = 1 by PEPIN:38; A3: p>1 by INT_2:def 5; then A4: 1 mod p = 1 by NAT_D:14; then A5: (b|^(p-'1) - 1) mod p = 0 by A2,INT_4:22; p is odd by A1,PEPIN:17; then p-1 is even by HILBERT3:2; then p-'1 is even by A3,BINARITH:50; then 2 divides (p-'1) by PEPIN:22; then p-'1 = 2*((p-'1) div 2) by NAT_D:3; then b|^(p-'1) - 1 = (b|^((p-'1) div 2))|^2 - 1 by NEWTON:14 .= (b|^((p-'1) div 2))^2 - 1 by NEWTON:100 .= (b|^((p-'1) div 2) +1)*(b|^((p-'1) div 2)-1); then A6: p divides (b|^((p-'1) div 2) +1)*(b|^((p-'1) div 2)-1) by A5,Lm1; p-1 > 2-1 by A1,XREAL_1:11; then p-1 >= 1 + 1 by INT_1:20; then p-'1 >= 2 by A3,BINARITH:50; then (p-'1) div 2 >= 2 div 2 by NAT_2:26; then A7: (p-'1) div 2 >= 1 by PEPIN:48; per cases by A7,REAL_1:def 5; suppose A8: (p-'1) div 2 = 1; then p divides (b +1)*(b|^1 -1) by A6,NEWTON:10; then A9: p divides (b +1)*(b -1) by NEWTON:10; now assume p divides (b - 1); then p divides -(b - 1) by INT_2:14; then (1^2 - b) mod p = 0 by Lm1; hence contradiction by A1,Def2; end; then p divides (b - (-1)) by A9,Th7; then b,(-1) are_congruent_mod p by INT_2:19; then A10: b mod p = (-1) mod p by INT_3:12; -p < -2 by A1,XREAL_1:26; then -p < -2+1 by XREAL_1:41; then b mod p = p - 1 by A10,INT_3:10; hence thesis by A8,NEWTON:10; end; suppose A11: (p-'1) div 2 > 1; set l = (p-'1) div 2; set fs = <*-1*>^((l-'1) |-> 0)^<*1*>; A12: -1 is Element of INT & 1 is Element of INT & 0 is Element of INT by INT_1:def 2; then A13: <*-1*> is FinSequence of INT & <*1*> is FinSequence of INT by FINSEQ_1:95; (l-'1) |-> 0 is FinSequence of INT by A12,FINSEQ_2:77; then <*-1*>^((l-'1) |-> 0) is FinSequence of INT by A13,FINSEQ_1:96; then reconsider fs as FinSequence of INT by A13,FINSEQ_1:96; A14: len fs = len (<*-1*>^(((l-'1) |-> 0)^<*1*>)) by FINSEQ_1:45 .= 1 + len (((l-'1) |-> 0)^<*1*>) by FINSEQ_5:8 .= 1 + len ((l-'1) |-> 0) + 1 by FINSEQ_2:19 .= 1 + ((l-'1) +1) by FINSEQ_2:69 .= 1 + l by A11,BINARITH:53; A15: len ((l-'1) |-> 0) = l-'1 by FINSEQ_2:69; set K1 = <*-1*>^((l-'1) |-> 0); A16: len K1 = 1 + (l-'1) by A15,FINSEQ_5:8 .= l by A11,BINARITH:53; then A17: fs.(l+1) = 1 by FINSEQ_1:59; A18: fs.1 = (<*-1*>^(((l-'1) |-> 0)^<*1*>)).1 by FINSEQ_1:45 .= -1 by FINSEQ_1:58; 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 & (for d st d in dom fr holds fr.d = (fs.d) * x|^(d-'1)) & (Poly-INT fs).x = Sum fr by Def1; fr = <*-1*>^((l-'1) |-> 0)^<*x|^l*> proof set K = <*-1*>^((l-'1) |-> 0)^<*x|^l*>; len K = len (<*-1*>^(((l-'1) |-> 0)^<*x|^l*>)) by FINSEQ_1:45 .= 1 + len (((l-'1) |-> 0)^<*x|^l*>) by FINSEQ_5:8 .= 1 + len ((l-'1) |-> 0) + 1 by FINSEQ_2:19 .= 1 + ((l-'1) +1) by FINSEQ_2:69 .= len fr by A11,A14,A20,BINARITH:53; then A21: dom fr = dom K by FINSEQ_3:31; for d being Nat st d in dom fr holds fr.d = K.d proof let d be Nat; assume A22: d in dom fr; then d in Seg(l + 1) by A14,A20,FINSEQ_1:def 3; then A23: d>=1 & d<=l+1 by FINSEQ_1:3; per cases by A23,REAL_1:def 5; suppose A24: d=1; then A25: fr.1 = (fs.1) * x|^(1-'1) by A20,A22 .= (fs.1) * x|^0 by BINARITH:51 .= (fs.1) * 1 by NEWTON:9 .= -1 by A18; K.1 = (<*-1*>^(((l-'1) |-> 0)^<*x|^l*>)).1 by FINSEQ_1:45 .= fr.1 by A25,FINSEQ_1:58; hence thesis by A24; end; suppose d>1 & d0 & d-1= 0+1 & w < l by A26,BINARITH:67,INT_1:20; then A28: ((l-'1) |-> 0).w = 0 by GOBRD10:def 3; w in Seg(l-'1) by A27,FINSEQ_1:3; then A29: w in dom ((l-'1) |-> 0) by A15,FINSEQ_1:def 3; then A30: w in dom (((l-'1) |-> 0)^<*1*>) & w in dom (((l-'1) |-> 0)^<*x|^l*>)by FINSEQ_2:18; A31: fs.d = (<*-1*>^(((l-'1) |-> 0)^<*1*>)).(w+1) by FINSEQ_1:45 .= (((l-'1) |-> 0)^<*1*>).w by A30,FINSEQ_3:112 .= 0 by A28,A29,FINSEQ_1:def 7; thus K.d = (<*-1*>^(((l-'1) |-> 0)^<*x|^l*>)).(w+1) by FINSEQ_1:45 .= (((l-'1) |-> 0)^<*x|^l*>).w by A30,FINSEQ_3:112 .= (fs.d)*x|^(d-'1) by A28,A29,A31,FINSEQ_1:def 7 .= fr.d by A20,A22; end; suppose A32: d=l+1; then A33: fs.d = 1 by A16,FINSEQ_1:59; d in dom fs by A14,A32,FINSEQ_5:6; then d in dom fr by A20,FINSEQ_3:31; hence fr.d = 1 * x|^(l+1-'1) by A20,A32,A33 .= x|^l by BINARITH:39 .= K.d by A16,A32,FINSEQ_1:59; end; end; hence thesis by A21,FINSEQ_1:17; end; then Sum fr = Sum (<*-1*>^(((l-'1) |-> 0)^<*x|^l*>)) by FINSEQ_1:45 .= -1 + Sum (((l-'1) |-> 0)^<*x|^l*>) by RVSUM_1:106 .= -1 + (Sum ((l-'1) |-> 0) + x|^l) by RVSUM_1:104 .= -1 + ((l-'1)*0 + x|^l) by RVSUM_1:110; hence thesis by A20; end; consider fp being FinSequence of NAT such that A34: len fp = l & (for d st d in dom fp holds fp.d hcf 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) by A1,Th16; now assume p divides (b|^l - 1); then A35: (b|^l - 1) mod p = 0 by Lm1; reconsider b as Element of INT by INT_1:def 2; A36: (Poly-INT fs).b mod p = 0 by A19,A35; set f = fp^<*b*>; <*b*> is FinSequence of NAT by FINSEQ_1:95; then reconsider f as FinSequence of NAT by FINSEQ_1:96; A37: len f = l+1 by A34,FINSEQ_2:19; A38: 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 d in Seg (l+1) by A37,FINSEQ_1:def 3; then A39: d>=1 & d<=l+1 by FINSEQ_1:3; per cases by A39,REAL_1:def 5; suppose d>=1 & d=1 & d<=l by NAT_1:13; then A40: d in dom fp by A34,FINSEQ_3:27; then fp.d hcf p = 1 & fp.d is_quadratic_residue_mod p by A34; then A41: (fp.d)|^l mod p = 1 mod p by A1,A4,Th17; reconsider k = fp.d as Element of INT by INT_1:def 2; (k|^l - 1) mod p = 0 by A41,INT_4:22; then (Poly-INT fs).k mod p = 0 by A19; hence thesis by A40,FINSEQ_1:def 7; end; suppose d=l+1; hence thesis by A34,A36,FINSEQ_1:59; end; end; A42: 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 A43: d in dom f & e in dom f & d<>e; then A44: d>=1 & d<= l+1 & e>=1 & e<=l+1 by A37,FINSEQ_3:27; per cases by A44,REAL_1:def 5; suppose d>=1 & d=1 & d<=l by NAT_1:13; then A45: d in dom fp by A34,FINSEQ_3:27; then A46: f.d = fp.d by FINSEQ_1:def 7; per cases by A44,REAL_1:def 5; suppose e>=1 & e=1 & e<=l by NAT_1:13; then A47: e in dom fp by A34,FINSEQ_3:27; then not fp.d,fp.e are_congruent_mod p by A34,A43,A45; hence thesis by A46,A47,FINSEQ_1:def 7; end; suppose A48: e=l+1; not f.d,b are_congruent_mod p proof assume f.d,b are_congruent_mod p; then A49: p divides (f.d - b) by INT_2:19; f.d is_quadratic_residue_mod p & f.d hcf p = 1 by A34,A45,A46; then consider j being Integer such that A50: (j^2 - f.d) mod p = 0 by Def2; p divides (j^2 - f.d) by A50,INT_1:89; then p divides ((j^2 - f.d)+(f.d - b)) by A49,WSIERP_1:9; then (j^2 - b) mod p = 0 by INT_1:89; hence contradiction by A1,Def2; end; hence thesis by A34,A48,FINSEQ_1:59; end; end; suppose A51: d=l+1; then e>=1 & e<=l by A43,A44,NAT_1:8; then A52: e in dom fp by A34,FINSEQ_3:27; then f.e = fp.e by FINSEQ_1:def 7; then f.e is_quadratic_residue_mod p & f.e hcf p = 1 by A34,A52; then consider j being Integer such that A53: (j^2 - f.e) mod p = 0 by Def2; A54: p divides (j^2 - f.e) by A53,INT_1:89; not b,f.e are_congruent_mod p proof assume b,f.e are_congruent_mod p; then p divides (b - f.e) by INT_2:19; then p divides ((j^2 - f.e) - (b - f.e)) by A54,Th1; then (j^2 - b) mod p = 0 by INT_1:89; hence contradiction by A1,Def2; end; hence thesis by A34,A51,FINSEQ_1:59; end; end; A55: len fs = l+1 & not p divides fs.(l+1) & p>2 by A1,A3,A14,A17,NAT_D:7; reconsider f as FinSequence of INT by FINSEQ_2:27,NUMBERS:17; len f <= l by A38,A42,A55,Th8; hence contradiction by A37,XREAL_1:31; end; then p divides (b|^l + 1) by A6,Th7; then consider k being Nat such that A56: (b|^l + 1) = p*k by NAT_D:def 3; -p < -1 by A3,XREAL_1:26; then A57: (-1) mod p = (-1) + p by INT_3:10; b|^l mod p = (p*k + (- 1)) mod p by A56 .= p - 1 by A57,INT_3:8; 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 A1: p>2 & a gcd p = 1 & not a is_quadratic_residue_mod p; set l = a mod p; reconsider l as Element of NAT by INT_1:16,84; A2: l mod p = a mod p by INT_3:13; then A3: l,a are_congruent_mod p by INT_3:12; then l gcd p = 1 by A1,INT_4:14; then l|^((p-'1) div 2) mod p = p - 1 by A1,A3,Th11,Th18; hence thesis by A2,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 p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p; then A1: a|^((p-'1) div 2) mod p = 1 by Th17; p>1 by INT_2:def 5; then a|^((p-'1) div 2) mod p = 1 mod p by A1,NAT_D:14; then a|^((p-'1) div 2),1 are_congruent_mod p by INT_3:12; then p divides (a|^((p-'1) div 2) - 1) by INT_2:19; hence thesis by INT_1:89; 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 A1: p > 2 & a gcd p = 1 & not a is_quadratic_residue_mod p; then A2: a|^((p-'1) div 2) mod p = p-1 by Th19; p-1 > 2-1 & p-1

2 & a gcd p = 1 & b gcd p = 1 & a is_quadratic_residue_mod p & b is_quadratic_residue_mod p implies a*b is_quadratic_residue_mod p proof assume A1: p>2 & a gcd p = 1 & b gcd p = 1 & a is_quadratic_residue_mod p & b is_quadratic_residue_mod p; then consider i being Integer such that A2: (i^2 - a) mod p =0 by Def2; consider j being Integer such that A3: (j^2 - b) mod p =0 by A1,Def2; p divides (i^2 - a) & p divides (j^2 - b) by A2,A3,INT_1:89; then i^2,a are_congruent_mod p & j^2,b are_congruent_mod p by INT_2:19; then (i^2)*(j^2),a*b are_congruent_mod p by INT_1:39; then p divides ((i*j)^2 - a*b) by INT_2:19; then ((i*j)^2 - a*b) mod p = 0 by INT_1:89; hence thesis by Def2; end; theorem p>2 & a gcd p = 1 & b gcd p = 1 & a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p implies not a*b is_quadratic_residue_mod p proof assume A1: p>2 & a gcd p = 1 & b gcd p = 1 & a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p; then A2: a*b gcd p = 1 by WSIERP_1:11; set l = (p-'1) div 2; (a|^l -1) mod p = 0 & (b|^l + 1) mod p = 0 by A1,Th20,Th21; then A3: p divides (a|^l -1) & p divides (b|^l + 1) by INT_1:89; then A4: p divides (a|^l -1)*(b|^l +1) by INT_2:12; A5: (a|^l -1)*(b|^l +1) = a|^l * b|^l +a|^l*1 -1*b|^l -1*1 .= (a*b)|^l +a|^l*1 -1*b|^l -1*1 by NEWTON:12 .= ((a*b)|^l -1) +(a|^l - 1) -(b|^l - 1); now assume a*b is_quadratic_residue_mod p; then ((a*b)|^l -1) mod p = 0 by A1,A2,Th20; then p divides ((a*b)|^l -1) by INT_1:89; then p divides ((a*b)|^l -1) +(a|^l - 1) by A3,WSIERP_1:9; then p divides (b|^l - 1) by A4,A5,Th2; then p divides ((b|^l +1) - (b|^l -1)) by A3,Th1; hence contradiction by A1,NAT_D:7; end; hence thesis; end; theorem p>2 & a gcd p = 1 & b gcd p = 1 & not a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p implies a*b is_quadratic_residue_mod p proof assume A1: p>2 & a gcd p = 1 & b gcd p = 1 & not a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p; then A2: a*b gcd p = 1 by WSIERP_1:11; set l = (p-'1) div 2; (a|^l +1) mod p = 0 & (b|^l + 1) mod p = 0 by A1,Th21; then A3: p divides (a|^l +1) & p divides (b|^l + 1) by INT_1:89; then A4: p divides (a|^l +1)*(b|^l +1) by INT_2:12; A5: (a|^l +1)*(b|^l +1) = a|^l * b|^l +a|^l*1 +1*b|^l +1*1 .= (a*b)|^l +a|^l + b|^l +1 by NEWTON:12 .= ((a*b)|^l +1) +(a|^l + 1) - (1- b|^l); now assume not a*b is_quadratic_residue_mod p; then ((a*b)|^l +1) mod p = 0 by A1,A2,Th21; then p divides ((a*b)|^l +1) by INT_1:89; then p divides ((a*b)|^l +1) +(a|^l + 1) by A3,WSIERP_1:9; then p divides (1- b|^l) by A4,A5,Th2; then p divides ((b|^l +1) + (1- b|^l)) by A3,WSIERP_1:9; hence contradiction by A1,NAT_D:7; end; hence thesis; end; definition let a be Integer, p be Prime; func Lege (a,p) -> Integer equals :Def3: 1 if a is_quadratic_residue_mod p, -1 if not a is_quadratic_residue_mod p; coherence; consistency; end; theorem Th25: Lege (a,p) = 1 or Lege (a,p) = -1 proof per cases; suppose a is_quadratic_residue_mod p; thus thesis by Def3; end; suppose not a is_quadratic_residue_mod p; thus thesis by Def3; end; end; theorem Th26: a gcd p = 1 implies Lege (a^2,p) = 1 proof assume a gcd p = 1; then a^2 is_quadratic_residue_mod p by Th9; hence thesis by Def3; end; theorem Lege (1,p) = 1 proof 1 gcd p = 1 by WSIERP_1:13; then Lege (1^2,p) = 1 by Th26; hence thesis; end; theorem Th28: p>2 & a gcd p =1 implies Lege (a,p),a|^((p-'1) div 2) are_congruent_mod p proof assume A1: p>2 & a gcd p = 1; A2: p>1 by INT_2:def 5; then -p < -1 by XREAL_1:26; then A3: (-1) mod p = p+(-1) by INT_3:10; per cases; suppose A4: a is_quadratic_residue_mod p; then a|^((p-'1) div 2) mod p = 1 by A1,Th17; then a|^((p-'1) div 2) mod p = 1 mod p by A2,NAT_D:14; then a|^((p-'1) div 2) mod p = Lege (a,p) mod p by A4,Def3; hence thesis by INT_3:12; end; suppose A5: not a is_quadratic_residue_mod p; then a|^((p-'1) div 2) mod p = p-1 by A1,Th19 .= Lege (a,p) mod p by A3,A5,Def3; hence thesis by INT_3:12; end; end; theorem p>2 & a gcd p =1 & a,b are_congruent_mod p implies Lege (a,p) = Lege (b,p) proof assume A1: p>2 & a gcd p =1 & a,b are_congruent_mod p; then b gcd p = 1 by INT_4:14; then Lege (a,p),a|^((p-'1) div 2) are_congruent_mod p & Lege (b,p),b|^((p-'1) div 2) are_congruent_mod p by A1,Th28; then A2: Lege (a,p) mod p = a|^((p-'1) div 2) mod p & Lege (b,p) mod p = b|^((p-'1) div 2) mod p by INT_3:12; a mod p = b mod p by A1,INT_3:12; then Lege (a,p) mod p = Lege (b,p) mod p by A2,Th13; then Lege (a,p),Lege (b,p) are_congruent_mod p by INT_3:12; then A3: p divides (Lege (a,p) - Lege (b,p)) by INT_2:19; per cases by Th25; suppose A4: Lege (a,p) = 1; then Lege (b,p) <> -1 by A1,A3,NAT_D:7; hence thesis by A4,Th25; end; suppose A5: Lege (a,p) = -1; now assume Lege (b,p) = 1; then p divides -2 by A3,A5; then p divides 2 by INT_2:14; hence contradiction by A1,NAT_D:7; end; hence thesis by A5,Th25; end; end; theorem p>2 & a gcd p=1 & b gcd p=1 implies Lege(a*b,p)=Lege(a,p)*Lege(b,p) proof assume A1: p>2 & a gcd p=1 & b gcd p=1; then Lege(a,p),a|^((p-'1) div 2) are_congruent_mod p & Lege(b,p),b|^((p-'1) div 2) are_congruent_mod p by Th28; then Lege(a,p)*Lege(b,p),(a|^((p-'1) div 2))*(b|^((p-'1) div 2)) are_congruent_mod p by INT_1:39; then Lege(a,p)*Lege(b,p),(a*b)|^((p-'1) div 2) are_congruent_mod p by NEWTON:12; then A2: (a*b)|^((p-'1) div 2),Lege(a,p)*Lege(b,p) are_congruent_mod p by INT_1:35; a*b gcd p = 1 by A1,WSIERP_1:11; then Lege(a*b,p),(a*b)|^((p-'1) div 2) are_congruent_mod p by A1,Th28; then Lege(a*b,p),Lege(a,p)*Lege(b,p) are_congruent_mod p by A2,INT_1:36; then A3: p divides (Lege(a*b,p)-Lege(a,p)*Lege(b,p)) by INT_2:19; A4: (Lege(a,p) = 1 or Lege(a,p) = -1) & (Lege(b,p) = 1 or Lege(b,p) = -1) by Th25; per cases by Th25; suppose Lege(a*b,p) = 1; hence thesis by A1,A3,A4,NAT_D:7; end; suppose A5: Lege(a*b,p) = -1; now assume Lege(a,p)*Lege(b,p) <> -1; then p divides (-2) by A3,A4,A5; then p divides 2 by INT_2:14; hence contradiction by A1,NAT_D:7; end; hence thesis by A5; end; end; theorem Th31: (for d st d in dom fr holds fr.d = 1 or fr.d = -1) implies Product fr = 1 or Product fr = -1 proof defpred P[FinSequence of INT] means (for d st d in dom $1 holds $1.d = 1 or $1.d = -1) implies Product $1 = 1 or Product $1 = -1; A1: P[<*>INT] by RVSUM_1:124; A2: for p being FinSequence of INT, n being Element of INT st P[p] holds P[p^<*n*>] proof let p be FinSequence of INT,i be Element of INT; assume A3: P[p]; set p1 = p^<*i*>; P[p1] proof assume A4: (for d st d in dom p1 holds p1.d = 1 or p1.d = -1); A5: for d st d in dom p holds p.d = 1 or p.d = -1 proof let d; assume A6: d in dom p; then p1.d = 1 or p1.d = -1 by A4,FINSEQ_2:18; hence thesis by A6,FINSEQ_1:def 7; end; A7: len p1 =len p +1 by FINSEQ_2:19; len p1 in dom p1 by FINSEQ_5:6; then A8: p1.(len p + 1) = 1 or p1.(len p + 1) = -1 by A4,A7; A9: Product p1 = (Product p)*i by RVSUM_1:126; per cases by A3,A5,A8,FINSEQ_1:59; suppose Product p = 1 & i =1; hence thesis by A9; end; suppose Product p = 1 & i = -1; hence thesis by A9; end; suppose Product p = -1 & i =1; hence thesis by A9; end; suppose Product p = -1 & i = -1; hence thesis by A9; end; end; hence thesis; end; for p being FinSequence of INT holds P[p] from FINSEQ_2:sch 2(A1,A2); hence thesis; end; reserve m for Integer; theorem Th32: for f,fr st len f = len fr & (for d st d in dom f holds f.d,fr.d are_congruent_mod m) holds Product f,Product fr are_congruent_mod m proof defpred P[Nat] means for f,fr st len f =$1 & len f=len fr & (for d st d in dom f holds f.d,fr.d are_congruent_mod m) holds Product f,Product fr are_congruent_mod m; A1: P[0] proof let f,fr; assume len f = 0 & len f = len fr; then f = <*>INT & fr = <*>INT; hence thesis by INT_1:32; end; A2: for n be Element of NAT st P[n] holds P[n+1] proof let n be Element of NAT; assume A3: P[n]; P[n+1] proof let f,fr; assume A4: len f = n+1 & len f = len fr & (for d st d in dom f holds f.d,fr.d are_congruent_mod m); then consider f1 being FinSequence of INT,a being Element of INT such that A5: f = f1^<*a*> by FINSEQ_2:22; consider fr1 being FinSequence of INT,b being Element of INT such that A6: fr = fr1^<*b*> by A4,FINSEQ_2:22; A7: n+1 = len f1 +1 & n+1 = len fr1 +1 by A4,A5,A6,FINSEQ_2:19; then A8: dom f1 = dom fr1 by FINSEQ_3:31; for d st d in dom f1 holds f1.d,fr1.d are_congruent_mod m proof let d; assume A9: d in dom f1; then f.d = f1.d & fr.d = fr1.d by A5,A6,A8,FINSEQ_1:def 7; hence thesis by A4,A5,A9,FINSEQ_2:18; end; then A10: Product f1,Product fr1 are_congruent_mod m by A3,A7; f <> {} by A4; then A11: (n+1) in dom f by A4,FINSEQ_5:6; f.(n+1) = a & fr.(n+1) = b by A5,A6,A7,FINSEQ_1:59; then a,b are_congruent_mod m by A4,A11; then (Product f1)*a,(Product fr1)*b are_congruent_mod m by A10,INT_1:39; then Product f,(Product fr1)*b are_congruent_mod m by A5,RVSUM_1:126; hence thesis by A6,RVSUM_1:126; end; hence thesis; end; for n be Element of NAT holds P[n] from NAT_1:sch 1(A1,A2); hence thesis; end; theorem Th33: for f,fr st len f = len fr & (for d st d in dom f holds f.d,-fr.d are_congruent_mod m) holds Product f,((-1)|^(len f))*Product fr are_congruent_mod m proof defpred P[Nat] means for f,fr st len f =$1 & len f=len fr & (for d st d in dom f holds f.d,-fr.d are_congruent_mod m) holds Product f,((-1)|^(len f))* Product fr are_congruent_mod m; A1: P[0] proof let f,fr; assume A2: len f = 0 & len f = len fr; then A3: f = <*>INT & fr = <*>INT; (-1)|^(len f) = 1 by A2,NEWTON:9; hence thesis by A3,INT_1:32; end; A4: for n be Element of NAT st P[n] holds P[n+1] proof let n be Element of NAT; assume A5: P[n]; P[n+1] proof let f,fr; assume A6: len f = n+1 & len f = len fr & (for d st d in dom f holds f.d,-fr.d are_congruent_mod m); then consider f1 be FinSequence of INT,a be Element of INT such that A7: f = f1^<*a*> by FINSEQ_2:22; consider fr1 be FinSequence of INT,b be Element of INT such that A8: fr = fr1^<*b*> by A6,FINSEQ_2:22; A9: n+1 = len f1 +1 & n+1 = len fr1 +1 by A6,A7,A8,FINSEQ_2:19; then A10: dom f1 = dom fr1 by FINSEQ_3:31; for d st d in dom f1 holds f1.d,-fr1.d are_congruent_mod m proof let d; assume A11: d in dom f1; then f.d = f1.d & fr.d = fr1.d by A7,A8,A10,FINSEQ_1:def 7; hence thesis by A6,A7,A11,FINSEQ_2:18; end; then A12: Product f1,((-1)|^(len f1))*Product fr1 are_congruent_mod m by A5,A9; f <> {} by A6; then A13: (n+1) in dom f by A6,FINSEQ_5:6; f.(n+1) = a & fr.(n+1) = b by A7,A8,A9,FINSEQ_1:59; then a,-b are_congruent_mod m by A6,A13; then (Product f1)*a,((-1)|^(len f1))*(Product fr1)*(-b) are_congruent_mod m by A12,INT_1:39; then Product f,((-1)|^(len f1))*(-1)*((Product fr1)*b) are_congruent_mod m by A7,RVSUM_1:126; then Product f,((-1)|^(len f1 + 1))*((Product fr1)*b) are_congruent_mod m by NEWTON:11; hence thesis by A6,A8,A9,RVSUM_1:126; end; hence thesis; end; for n be Element of NAT holds P[n] from NAT_1:sch 1(A1,A4); hence thesis; end; reserve fp for FinSequence of NAT; theorem Th34: p>2 & (for d st d in dom fp holds fp.d hcf p = 1) implies ex fr being FinSequence of INT st len fr = len fp & (for d st d in dom fr holds fr.d = Lege (fp.d,p)) & Lege (Product fp,p) = Product fr proof assume A1: p>2; assume A2: for d st d in dom fp holds fp.d hcf p = 1; Product(fp) hcf p = 1 by A2,WSIERP_1:43; then A4: Lege (Product fp,p),(Product fp)|^((p-'1) div 2) are_congruent_mod p by A1,Th28; set k = (p-'1) div 2; set f = fp|^k; reconsider f as FinSequence of INT by FINSEQ_2:27,NUMBERS:17; deffunc F(Nat) = Lege (fp.$1,p); consider fr being FinSequence such that A5: len fr = len fp & (for d being 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 A5; hence thesis by INT_1:def 2; end; then reconsider fr as FinSequence of INT by FINSEQ_2:14; A6: len f = len fp by NAT_3:def 1; for d st d in dom fr holds fr.d,f.d are_congruent_mod p proof let d; assume A7: d in dom fr; then d in dom fp by A5,FINSEQ_3:31; then fp.d hcf p = 1 by A2; then Lege (fp.d,p),(fp.d)|^k are_congruent_mod p by A1,Th28; then A8: fr.d,(fp.d)|^k are_congruent_mod p by A5,A7; d in dom f by A5,A6,A7,FINSEQ_3:31; hence thesis by A8,NAT_3:def 1; end; then Product fr,Product f are_congruent_mod p by A5,A6,Th32; then A9: Product f,Product fr are_congruent_mod p by INT_1:35; fp is FinSequence of REAL by FINSEQ_2:27; then Lege (Product fp,p),Product f are_congruent_mod p by A4,NAT_3:15; then Lege (Product fp,p),Product fr are_congruent_mod p by A9,INT_1:36; then A10: p divides (Lege (Product fp,p) - Product fr) by INT_2:19; take fr; A11: for d st d in dom fr holds fr.d = 1 or fr.d = -1 proof let d; assume d in dom fr; then fr.d = Lege (fp.d,p) by A5; hence thesis by Th25; end; per cases by Th25; suppose A12: Lege (Product fp,p) = 1; then Product fr <> -1 by A1,A10,NAT_D:7; hence thesis by A5,A11,A12,Th31; end; suppose A13: Lege (Product fp,p) = -1; now assume Product fr = 1; then p divides -2 by A10,A13; then p divides 2 by INT_2:14; hence contradiction by A1,NAT_D:7; end; hence thesis by A5,A11,A13,Th31; end; end; theorem p > 2 & d hcf p = 1 & e hcf p = 1 implies Lege((d^2)*e,p) = Lege(e,p) proof assume A1: p > 2 & d hcf p = 1 & e hcf p = 1; then A2: Lege(d^2,p) = 1 by Th26; reconsider d2=d^2, e as Element of NAT by ORDINAL1:def 13; set fp = <*d2,e*>; reconsider p as prime Element of NAT by ORDINAL1:def 13; reconsider fp as FinSequence of NAT by FINSEQ_2:15; for k st k in dom fp holds fp.k hcf p = 1 proof let k; assume k in dom fp; then k in Seg(len fp) by FINSEQ_1:def 3; then A3: k in Seg 2 by FINSEQ_1:61; per cases by A3,FINSEQ_1:4,TARSKI:def 2; suppose k = 1; then fp.k = d^2 by FINSEQ_1:61; hence thesis by A1,WSIERP_1:12; end; suppose k = 2; hence thesis by A1,FINSEQ_1:61; end; end; then consider fr be FinSequence of INT such that A5: len fr = len fp & (for k be Nat st k in dom fr holds fr.k = Lege (fp.k,p)) & Lege (Product fp,p) = Product fr by A1,Th34; A6: len fr = 2 by A5,FINSEQ_1:61; then 1 in dom fr & 2 in dom fr by FINSEQ_3:27; then fr.1 = Lege(fp.1,p) & fr.2 = Lege(fp.2,p) by A5; then fr.1 = Lege(d^2,p) & fr.2 = Lege(e,p) by FINSEQ_1:61; then fr = <*1,Lege(e,p)*> by A2,A6,FINSEQ_1:61; then Product fr = 1 * Lege(e,p) by RVSUM_1:129; hence thesis by A5,RVSUM_1:129; end; theorem Th36: p>2 implies Lege (-1,p) = (-1)|^((p-'1) div 2) proof assume A1: p>2; (-1) gcd p = (-1)|^1 gcd p by NEWTON:10 .= abs((-1)|^1) hcf abs(p) by INT_2:51 .= 1 hcf abs(p) by SERIES_2:1 .= 1 by NEWTON:64; then A2: Lege (-1,p),(-1)|^((p-'1) div 2) are_congruent_mod p by A1,Th28; abs((-1)|^((p-'1) div 2)) = 1 by SERIES_2:1; then A3: (-1)|^((p-'1) div 2) =1 or -(-1)|^((p-'1) div 2) =1 by ABSVALUE:1; per cases by A3; suppose A4: (-1)|^((p-'1) div 2) =1; then A5: p divides (Lege (-1,p) - 1) by A2,INT_2:19; now assume Lege(-1,p) = -1; then p divides -2 by A5; then p divides 2 by INT_2:14; hence contradiction by A1,NAT_D:7; end; hence thesis by A4,Th25; end; suppose A6: (-1)|^((p-'1) div 2) = -1; then p divides (Lege (-1,p) - (-1)) by A2,INT_2:19; then Lege(-1,p) <> 1 by A1,NAT_D:7; hence thesis by A6,Th25; end; end; theorem p>2 & p mod 4 = 1 implies (-1) is_quadratic_residue_mod p proof assume A1: p>2 & p mod 4 = 1; then A2: p = (p div 4)*4 + 1 by NAT_D:2; p>1 by INT_2:def 5; then p-'1 = p-1 by BINARITH:50; then p-'1 = 2*(2*(p div 4)) by A2; then (-1)|^((p-'1) div 2) = (-1)|^(2*(p div 4)) by NAT_D:18 .= ((-1)|^2)|^(p div 4) by NEWTON:14 .= (1|^2)|^(p div 4) by WSIERP_1:2 .= 1|^(p div 4) by NEWTON:100,SQUARE_1:59 .= 1 by NEWTON:15; then Lege(-1,p) = 1 by A1,Th36; hence thesis by Def3; end; theorem p>2 & p mod 4 = 3 implies not (-1) is_quadratic_residue_mod p proof assume A1: p>2 & p mod 4 = 3; then A2: p = (p div 4)*4 + 3 by NAT_D:2; p>1 by INT_2:def 5; then p-'1 = p-1 by BINARITH:50; then p-'1 = 2*(2*(p div 4) + 1) by A2; then (-1)|^((p-'1) div 2) = (-1)|^(2*(p div 4) + 1) by NAT_D:18 .= (-1)|^(2*(p div 4)) * (-1) by NEWTON:11 .= ((-1)|^2)|^(p div 4) *(-1) by NEWTON:14 .= (1|^2)|^(p div 4) *(-1) by WSIERP_1:2 .= 1|^(p div 4) *(-1) by NEWTON:100,SQUARE_1:59 .= 1 *(-1) by NEWTON:15; then Lege(-1,p) = -1 by A1,Th36; hence thesis by Def3; end; begin :: Gauss Lemma and Law of Quadratic Reciprocity theorem Th39: for D being non empty set,f being FinSequence of D, i,j being Nat holds f is one-to-one iff Swap(f,i,j) is one-to-one proof let D be non empty set,f be FinSequence of D,i,j be Nat; thus f is one-to-one implies Swap(f,i,j) is one-to-one proof assume f is one-to-one; then A1: card(rng f) = len f by FINSEQ_4:77; set ff = Swap(f,i,j); len ff = len f & rng ff = rng f by FINSEQ_7:20,24; hence thesis by A1,FINSEQ_4:77; end; assume Swap(f,i,j) is one-to-one; then card(rng Swap(f,i,j)) = len Swap(f,i,j) by FINSEQ_4:77; then card(rng f) = len Swap(f,i,j) by FINSEQ_7:24; then card(rng f) = len f by FINSEQ_7:20; hence thesis by FINSEQ_4:77; end; theorem Th40: for f being FinSequence of NAT st len f = n & (for d st d in dom f holds f.d>0 & f.d<=n) & f is one-to-one holds rng f = Seg n proof defpred P[Nat] means for f being FinSequence of NAT st len f = $1 & (for d st d in dom f holds f.d>0 & f.d<=$1) & f is one-to-one holds rng f = Seg $1; A1: P[0] by FINSEQ_1:4,RELAT_1:60,CARD_2:59; A2: for n be Element of NAT st P[n] holds P[n+1] proof let n be Element of NAT; assume A3: P[n]; P[n+1] proof let f be FinSequence of NAT; assume A4: len f = n+1 & (for d st d in dom f holds f.d>0 & f.d<=n+1) & f is one-to-one; then A5: f <> {}; then consider f1 being FinSequence of NAT,a being Element of NAT such that A6: f = f1^<*a*> by HILBERT2:4; A7: len f = len f1 + 1 by A6,FINSEQ_2:19; A8: f1 is one-to-one & rng f1 misses rng <*a*> by A4,A6,FINSEQ_3:98; A9: n+1 in dom f by A4,A5,FINSEQ_5:6; then f.(n+1) > 0 & f.(n+1) <= n+1 by A4; then A10: a>0 & a<=n+1 by A4,A6,A7,FINSEQ_1:59; per cases by A10,REAL_1:def 5; suppose A11: a = n+1; for d st d in dom f1 holds f1.d>0 & f1.d<=n proof let d; assume A12: d in dom f1; then A13: d in dom f by A6,FINSEQ_2:18; then A14: f.d>0 & f.d<=n+1 by A4; then A15: f1.d>0 & f1.d<=n+1 by A6,A12,FINSEQ_1:def 7; now assume A16: f1.d = n+1; d <= n by A4,A7,A12,FINSEQ_3:27; then d < n+1 by XREAL_1:147; then f.d <> f.(n+1) by A4,A9,A13,FUNCT_1:def 8; then f1.d <> f.(n+1) by A6,A12,FINSEQ_1:def 7; hence contradiction by A4,A6,A7,A11,A16,FINSEQ_1:59; end; then f1.d < n+1 by A15,REAL_1:def 5; hence thesis by A6,A12,A14,FINSEQ_1:def 7,NAT_1:13; end; then rng f1 = Seg n by A3,A4,A7,A8; then rng f1 \/ {a} = Seg (n+1) by A11,FINSEQ_1:11; then rng f1 \/ rng <*a*> = Seg (n+1) by FINSEQ_1:55; hence thesis by A6,FINSEQ_1:44; end; suppose A17: a > 0 & a < n+1; ex d st d in dom f1 & f1.d = n+1 proof assume A18: 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 A19: d in dom f; then d in Seg(n+1) by A4,FINSEQ_1:def 3; then A20: d>=1 & d<=n+1 by FINSEQ_1:3; per cases by A20,REAL_1:def 5; suppose d=n+1; then f.d = a by A4,A6,A7,FINSEQ_1:59; then f.d>=0+1 & f.d<=n by A17,NAT_1:13; hence thesis by FINSEQ_1:3; end; suppose d>=1 & d=1 & d<=n by NAT_1:13; then d in Seg n by FINSEQ_1:3; then A21: d in dom f1 by A4,A7,FINSEQ_1:def 3; then f1.d <> n+1 by A18; then A22: f.d <> n+1 by A6,A21,FINSEQ_1:def 7; f.d>0 & f.d <=n+1 by A4,A19; then f.d>0 & f.d =0+1 & f.d<=n by NAT_1:13; hence thesis by FINSEQ_1:3; end; end; then f is FinSequence of Seg n by FINSEQ_2:14; then rng f c= Seg n by FINSEQ_1:def 4; then card rng f <= card Seg n by NAT_1:44; then n+1 <= card Seg n by A4,FINSEQ_4:77; then n+1 <= n+0 by FINSEQ_1:78; hence contradiction by XREAL_1:8; end; then consider d1 being Element of NAT such that A23: d1 in dom f1 & f1.d1 = n+1; set f2 = Swap(f,d1,n+1); A24: len f2 = n+1 by A4,FINSEQ_7:20; then A25: f2 <> {}; then consider f3 being FinSequence of NAT,b being Element of NAT such that A26: f2 = f3^<*b*> by HILBERT2:4; A27: n+1 = len f3 +1 by A24,A26,FINSEQ_2:19; d1>=1 & d1<=n by A4,A7,A23,FINSEQ_3:27; then A28: 1 <= d1 & d1 <= len f by A4,NAT_1:13; A29: 0+1 <= n+1 & n+1 <= len f by A4,XREAL_1:8; then f2/.(n+1) = f/.d1 by A28,FINSEQ_7:33; then f2/.(n+1) = f.d1 by A28,FINSEQ_4:24; then f2.(n+1) = f.d1 by A24,A29,FINSEQ_4:24; then A30: f2.(n+1) = n+1 by A6,A23,FINSEQ_1:def 7; A31: f2 is one-to-one by A4,Th39; then A32: f3 is one-to-one by A26,FINSEQ_3:98; A33: b = n+1 by A26,A27,A30,FINSEQ_1:59; for d st d in dom f3 holds f3.d>0 & f3.d<=n proof let d; assume A34: d in dom f3; then A35: d in dom f2 by A26,FINSEQ_2:18; then f2.d in rng f2 by FUNCT_1:12; then f2.d in rng f by FINSEQ_7:24; then consider e being Nat such that A36: e in dom f & f2.d = f.e by FINSEQ_2:11; f2.d >0 & f2.d<=n+1 by A4,A36; then A37: f3.d>0 & f3.d<=n+1 by A26,A34,FINSEQ_1:def 7; now assume f3.d=n+1; then A38: f2.d = n+1 by A26,A34,FINSEQ_1:def 7; d<=n by A27,A34,FINSEQ_3:27; then A39: d < n+1 by XREAL_1:147; n+1 in dom f2 by A24,A25,FINSEQ_5:6; hence contradiction by A30,A31,A35,A38,A39,FUNCT_1:def 8; end; then f3.d>0 & f3.d by A26,FINSEQ_1:44 .= Seg n \/ {n+1} by A33,A40,FINSEQ_1:55 .= Seg (n+1) by FINSEQ_1:11; hence thesis by FINSEQ_7:24; end; end; hence thesis; end; for n be Element of NAT holds P[n] from NAT_1:sch 1(A1,A2); hence thesis; end; reserve a,m for Nat; theorem Th41: for f be FinSequence of NAT st p>2 & a hcf 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 A1: p>2 & a hcf 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}; then A2: a|^((p-'1) div 2),Lege(a,p) are_congruent_mod p by Th28,INT_1:35; set p' = (p-'1) div 2; set f1 = f mod p; set f2 = Sgm rng f1; set X = {k where k is Element of NAT:k in rng f1 & k > p/2}; A4: rng idseq p' = Seg p' by RELAT_1:71; then reconsider I = idseq p' as FinSequence of NAT by FINSEQ_1:def 4; dom f = dom I by A1,VALUED_1:def 5; then A5: len f = len I by FINSEQ_3:31 .= p' by FINSEQ_2:55; (Product f1) mod p = (Product f) mod p by EULER_2:26; then A6: Product f1,Product f are_congruent_mod p by INT_3:12; I is Element of p'-tuples_on NAT by FINSEQ_2:131; then I is Element of p'-tuples_on REAL by FINSEQ_2:129; then A7: Product f = (Product (p'|->a))*(Product I) by A1,RVSUM_1:138 .= (a|^p') * (Product I) by NEWTON:def 1; A8: p>1 by INT_2:def 5; then A9: p-'1 = p-1 by BINARITH:50; p >= 2+1 by A1,NAT_1:13; then p-1 >= 3-1 by XREAL_1:11; then A10: p' >= 1 by A9,NAT_2:15; p is odd by A1,PEPIN:17; then A11: p-'1 is even by A9,HILBERT3:2; then 2 divides (p-'1) by PEPIN:22; then A12: p-'1 = 2*p' by NAT_D:3; then A13: p' divides (p-'1) by NAT_D:def 3; p-'1>0 by A8,A9,XREAL_1:52; then p' <= (p-'1) by A13,NAT_D:7; then A14: p' < p by A9,XREAL_1:148,XXREAL_0:2; A15: p' = ((p-'1)+1) div 2 by A11,NAT_2:28 .= p div 2 by A8,BINARITH:53; for d being Nat st d in dom I holds I.d hcf p = 1 proof let d be Nat; assume d in dom I; then d in Seg len I by FINSEQ_1:def 3; then A16: d in Seg p' by FINSEQ_2:55; then A17: I.d = d by A10,FINSEQ_2:57; d >= 1 & d <= p' by A16,FINSEQ_1:3; then d >= 1 & d < p by A14,XXREAL_0:2; then d,p are_relative_prime by EULER_1:3; hence thesis by A17,INT_2:def 4; end; then A18: (Product I) hcf p = 1 by WSIERP_1:43; A19: for d st d in dom f holds f.d = a*d proof let d; assume A20: d in dom f; then d in dom I by A1,VALUED_1:def 5; then d in Seg len I by FINSEQ_1:def 3; then A21: d is Element of Seg p' by FINSEQ_2:55; thus f.d = a * I.d by A1,A20,VALUED_1:def 5 .= a*d by A10,A21,FINSEQ_2:57; end; A22: len f1 = len f by EULER_2:def 1; then A23: dom f1 = dom f by FINSEQ_3:31; f1 <> {} by A5,A10,A22; then rng f1 is non empty Subset of NAT by FINSEQ_1:def 4; then consider n1 being Element of NAT such that A24: rng f1 c= Seg n1 \/ {0} by HEYTING3:3; not 0 in rng f1 proof assume 0 in rng f1; then consider n be Nat such that A25: n in dom f1 & f1.n = 0 by FINSEQ_2:11; reconsider a as Element of NAT by ORDINAL1:def 13; 0 = (f.n) mod p by A23,A25,EULER_2:def 1 .= (a*n) mod p by A19,A23,A25; then A26: p divides (a*n) by PEPIN:6; A27: n >= 1 & n <= p' by A5,A22,A25,FINSEQ_3:27; then p <= n by A1,A26,NAT_D:7,WSIERP_1:37; hence contradiction by A14,A27,XXREAL_0:2; end; then A28: {0} misses rng f1 by ZFMISC_1:56; then A29: rng f1 c= Seg n1 by A24,XBOOLE_1:73; then A30: rng f1 = rng f2 by FINSEQ_1:def 13; for x being set st x in X holds x in rng f1 proof let x be set; assume x in X; then consider k being Element of NAT such that A31: x = k & k in rng f1 & k > p/2; thus thesis by A31; end; then A32: X c= rng f1 by TARSKI:def 3; then reconsider X as finite set; A33: rng f1 c= NAT by FINSEQ_1:def 4; then reconsider X as finite Subset of NAT by A32,XBOOLE_1:1; card X is Element of NAT; then reconsider m as Element of NAT by A1; A34: rng f1 \ X c= rng f1 by XBOOLE_1:36; then reconsider Y = rng f1 \ X as finite Subset of NAT by A33,XBOOLE_1:1; A35: for d,e being Element of NAT st 1<=d & d f1.e proof let d,e be Element of NAT; assume A36: 1<=d & d 0 by A36; abs p = p & abs dd = dd by ABSVALUE:def 1; then A41: p <= dd by A1,A39,A40,INT_4:6,WSIERP_1:36; A42: dd <= p' - 1 by A5,A22,A36,XREAL_1:15; p'-1

0 & f1.d <= p' proof let d; assume A50: d in dom f1; reconsider d as Element of NAT by ORDINAL1:def 13; reconsider f1 as FinSequence of NAT qua set; f1.d in rng f1 & not f1.d in X by A49,A50,FUNCT_1:12; then A51: f1.d <= p/2; A52: f1.d in rng f1 by A50,FUNCT_1:12; then f1.d in {0} \/ rng f1 by XBOOLE_0:def 2; then not f1.d in {0} by A28,A52,XBOOLE_0:5; then f1.d <> 0 by TARSKI:def 1; hence thesis by A15,A51,INT_1:81; end; then rng f1 = rng I by A4,A5,A22,A45,Th40; then Product f1 = Product I by A45,EULER_2:25,RFINSEQ:39; then p divides (1 * Product I - a|^p' * Product I) by A6,A7,INT_2:19; then p divides (1 - a|^p')*Product I; then p divides (1 - a|^p') by A18,WSIERP_1:36; then 1,a|^p' are_congruent_mod p by INT_2:19; then A53: 1,Lege(a,p) are_congruent_mod p by A2,INT_1:36; now assume Lege(a,p) = -1; then p divides (1-(-1)) by A53,INT_2:19; hence contradiction by A1,NAT_D:7; end; then Lege(a,p) = 1 by Th25; hence thesis by A1,A49,CARD_1:47,NEWTON:9; end; suppose A54: X is non empty; A55: f2 = (Sgm Y)^(Sgm X) proof for k,l being Element of NAT st k in Y & l in X holds k < l proof let k,l be Element of NAT; assume A56: k in Y & l in X; then k in rng f1 & not k in X by XBOOLE_0:def 4; then A57: k <= p/2; ex l1 being Element of NAT st l1 = l & l1 in rng f1 & l1>p/2 by A56; hence thesis by A57,XXREAL_0:2; end; then Sgm (Y\/X) = (Sgm Y)^(Sgm X) by A48,FINSEQ_3:48; then Sgm (rng f1 \/ X) = (Sgm Y)^(Sgm X) by XBOOLE_1:39; hence thesis by A32,XBOOLE_1:12; end; A58: len Sgm Y = n proof len Sgm Y = card Y by A29,A34,FINSEQ_3:44,XBOOLE_1:1 .= p' - m by A1,A5,A22,A32,A44,CARD_2:63; hence thesis; end; then A59: f2/^n = Sgm X by A55,FINSEQ_5:40; f2 = (f2|n)^(f2/^n) by RFINSEQ:21; then A60: f2|n is one-to-one & f2/^n is one-to-one by A46,FINSEQ_3:98; A61: f2|n = Sgm Y by A55,A58,FINSEQ_3:122,FINSEQ_6:12; A62: m <> 0 by A1,A54; A63: len f2 = p' by A5,A22,A24,A28,A44,FINSEQ_3:44,XBOOLE_1:73; then A64: n <= len f2 by XREAL_1:45; A65: len(f2|n) = n by A63,FINSEQ_1:80,XREAL_1:45; set f3 = (len (f2/^n) |-> p) - (f2/^n); set f4 = (f2|n) ^ f3; A66: 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 .= (Seg len(f2/^n))/\dom(f2/^n) by FINSEQ_2:69 .= dom(f2/^n) /\ dom(f2/^n) by FINSEQ_1:def 3 .= dom(f2/^n); then A67: len f3 = len(f2/^n) by FINSEQ_3:31; A68: len(f2/^n) = (len f2 -' n) by BINARITH:76 .= len f2 - n by A63,BINARITH:50,XREAL_1:45 .= m by A63; A69: for d st d in dom f3 holds f3.d = p - (f2/^n).d proof let d; assume A70: d in dom f3; then A71: d in Seg len(f2/^n) by A66,FINSEQ_1:def 3; (len (f2/^n) |-> p).d = p by A62,A68,A71,FINSEQ_2:71; hence thesis by A70,VALUED_1:13; end; A72: for d st d in dom f3 holds f3.d > 0 & f3.d <= p' proof let d; assume A73: d in dom f3; then A74: f3.d = p - (f2/^n).d by A69; reconsider w = f3.d as Element of INT by INT_1:def 2; (Sgm X).d in rng Sgm X by A59,A66,A73,FUNCT_1:12; then (Sgm X).d in X by A48,FINSEQ_1:def 13; then consider ll be Element of NAT such that A75: ll = (Sgm X).d & ll in rng f1 & ll > p/2; A76: w < p - p/2 by A59,A74,A75,XREAL_1:12; consider e being Nat such that A77: e in dom f1 & f1.e = (f2/^n).d by A59,A75,FINSEQ_2:11; (f2/^n).d = f.e mod p by A23,A77,EULER_2:def 1; then (f2/^n).d < p by NAT_D:1; hence thesis by A15,A74,A76,INT_1:81,XREAL_1:52; end; for d being Nat st d in dom f3 holds f3.d in NAT proof let d be Nat; assume d in dom f3; then f3.d = p - (f2/^n).d & f3.d > 0 by A69,A72; hence thesis by INT_1:16; end; then reconsider f3 as FinSequence of NAT by FINSEQ_2:14; for d,e being Element of NAT st 1<=d & d f3.e proof let d,e be Element of NAT; assume A78: 1<=d & d= 1 & d1 <= p' & e1 >= 1 & e1 <= p' by A5,A22,A83,A87,FINSEQ_3:27; then d1+e1 >= 1+1 & d1+e1 <= p'+p' by XREAL_1:9; then d1+e1>0 & d1+e1 < p by A9,A12,XREAL_1:148,XXREAL_0:2; hence contradiction by A1,A89,NAT_D:7,WSIERP_1:37; end; then A90: f4 is one-to-one by A60,A80,FINSEQ_3:98; for d st d in dom f4 holds f4.d>0 & f4.d <= p' proof let d; assume A91: d in dom f4; per cases by A91,FINSEQ_1:38; suppose A92: d in dom(f2|n); reconsider d as Element of NAT by ORDINAL1:def 13; (f2|n).d in rng Sgm Y by A61,A92,FUNCT_1:12; then (f2|n).d in Y by A48,FINSEQ_1:def 13; then A93: (f2|n).d in rng f1 & not (f2|n).d in X by XBOOLE_0:def 4; then (f2|n).d <= p/2; then A94: (f2|n).d <= p' by A15,INT_1:81; not (f2|n).d in {0} by A28,A93,XBOOLE_0:3; then (f2|n).d <> 0 by TARSKI:def 1; then (f2|n).d > 0; hence thesis by A92,A94,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 A95: l in dom f3 & d = len(f2|n)+ l; f4.d = f3.l by A95,FINSEQ_1:def 7; hence thesis by A72,A95; end; end; then rng f4 = rng I by A4,A5,A81,A90,Th40; then Product f4 = Product I by A90,EULER_2:25,RFINSEQ:39; then A96: (Product(f2|n)) * (Product f3) = Product I by RVSUM_1:127; A97: f3 is FinSequence of INT & f2/^n is FinSequence of INT by FINSEQ_2:27,NUMBERS:17; 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 A69 .= (1*p + (-(f2/^n).d)) mod p .= (-(f2/^n).d) mod p by EULER_1:13; hence thesis by INT_3:12; end; then Product f3,(-1)|^m * Product(f2/^n) are_congruent_mod p by A67,A68,A97,Th33; then (Product f3)*(Product(f2|n)),(-1)|^m * Product(f2/^n)*(Product(f2|n)) are_congruent_mod p by 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 A96,RVSUM_1:127; then A98: Product I,(-1)|^m * Product f1 are_congruent_mod p by A47,RFINSEQ :21; (-1)|^m * Product f1,(-1)|^m * Product f are_congruent_mod p by A6,INT_4:11; then Product I,(-1)|^m * (a|^p') * (Product I) are_congruent_mod p by A7,A98,INT_1:36; then p divides (1*Product I-((-1)|^m * (a|^p')) * (Product I)) by INT_2:19; then p divides (1-((-1)|^m * (a|^p')))* Product I; then p divides (1-((-1)|^m * (a|^p'))) by A18,WSIERP_1:36; then p divides (-1)|^m * (1-((-1)|^m * (a|^p'))) by INT_2:12; then A99: p divides ((-1)|^m - (-1)|^m * (-1)|^m * (a|^p')); (-1)|^m * (-1)|^m = (-1)|^(m+m) by NEWTON:13 .= (-1)|^(2*m) .= ((-1)|^2)|^m by NEWTON:14 .= (1|^2)|^m by WSIERP_1:2 .= 1|^m by NEWTON:100,SQUARE_1:59 .= 1 by NEWTON:15; then (-1)|^m,a|^p' are_congruent_mod p by A99,INT_2:19; then A100: (-1)|^m,Lege(a,p) are_congruent_mod p by A2,INT_1:36; abs ((-1)|^m) = 1 by SERIES_2:1; then A101: (-1)|^m = 1 or -((-1)|^m) = 1 by ABSVALUE:1; per cases by A101; suppose A102: (-1)|^m = 1; now assume Lege(a,p) = -1; then p divides (1-(-1)) by A100,A102,INT_2:19; hence contradiction by A1,NAT_D:7; end; hence thesis by A102,Th25; end; suppose A103: (-1)|^m = -1; now assume Lege(a,p) = 1; then p divides (-1-1) by A100,A103,INT_2:19; then p divides (-2); then p divides 2 by INT_2:14; hence contradiction by A1,NAT_D:7; end; hence thesis by A103,Th25; end; end; end; theorem Th42: p>2 implies Lege(2,p) = (-1)|^((p^2 -'1) div 8) proof assume A1: p>2; then 2,p are_relative_prime by EULER_1:3; then A2: 2 hcf p = 1 by INT_2:def 4; set p' = (p-'1) div 2; set I = idseq p'; set fp = 2 * I; p is odd by A1,PEPIN:17; then A3: p-1 is even by HILBERT3:2; A4: p>1 by INT_2:def 5; then A5: p-1 = p-'1 by BINARITH:50; then 2 divides (p-'1) by A3,PEPIN:22; then A6: p-'1 = 2*p' by NAT_D:3; A7: p' = ((p-'1)+1) div 2 by A3,A5,NAT_2:28 .= p div 2 by A4,BINARITH:53; A8: p div 2 >= 1 by A1,NAT_2:15; p div 2 < p by INT_1:83; then (p div 2) div 2 <= p div 2 by NAT_2:26; then A9: p div (2*2) <= p div 2 by NAT_2:29; A10: for d st d in dom fp holds fp.d = 2*d proof let d; assume A11: 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 A12: d is Element of Seg p' by FINSEQ_2:55; thus fp.d = 2 * I.d by A11,VALUED_1:def 5 .= 2 * d by A7,A8,A12,FINSEQ_2:57; end; 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 = 2*d by A10; hence thesis; end; then reconsider fp as FinSequence of NAT by FINSEQ_2:14; dom fp = dom I by VALUED_1:def 5; then A13: len fp = len I by FINSEQ_3:31 .= p' by FINSEQ_2:55; set f = fp mod p; set X = {k where k is Element of NAT:k in rng f & k > p/2}; set m = Card X; set Y = {d where d is Element of NAT:d in dom f & f.d > p/2}; set Z = seq((p div 4),p'-'(p div 4)); for x be set st x in Y holds x in dom f proof let x be set; assume x in Y; then consider k be Element of NAT such that A14: x = k & k in dom f & f.k > p/2; thus thesis by A14; end; then Y c= dom f by TARSKI:def 3; then reconsider Y as finite Subset of NAT by XBOOLE_1:1; for x being set st x in X holds x in rng f proof let x be set; assume x in X; then consider k being Element of NAT such that A15: x = k & k in rng f & k > p/2; thus thesis by A15; end; then A16: X c= rng f by TARSKI:def 3; then reconsider X as finite set; card X is Element of NAT; then reconsider m as Element of NAT; A17: Lege(2,p) = (-1)|^m by A1,A2,Th41; rng f c= NAT by FINSEQ_1:def 4; then reconsider X as finite Subset of NAT by A16,XBOOLE_1:1; A18: len f = len fp by EULER_2:def 1; then A19: dom f = dom fp by FINSEQ_3:31; A20: for d st d in dom f holds f.d = 2*d proof let d; assume A21: d in dom f; then d<= p' by A13,A18,FINSEQ_3:27; then 2*d<=(p-'1) by A6,XREAL_1:66; then 2*d

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

-p by A26,XREAL_1:26; then d-e > -p by A25,XXREAL_0:2; hence contradiction by A24,A27,SEQ_2:9; end; hence thesis; end; deffunc F(Nat) = f1.$1 div p; consider f2 be FinSequence such that A28: len f2 = p' & for d being Nat st d in dom f2 holds f2.d = F(d) from FINSEQ_1:sch 2; 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 A28; hence thesis; end; then reconsider f2 as FinSequence of NAT by FINSEQ_2:14; set f3 = f1 mod p; A29: len f3 = len f1 by EULER_2:def 1; then A30: dom f1 = dom f3 by FINSEQ_3:31; A31: dom f1 = dom f2 by A6,A28,FINSEQ_3:31; A32: 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 A30,A31; A33: for d st d in dom f1 holds f1.d = f2.d * p + f3.d proof let d; assume d in dom f1; then f2.d = f1.d div p & f3.d = f1.d mod p by A28,A31,EULER_2:def 1; hence f1.d = f2.d * p + f3.d by NAT_D:2; end; for d being Nat st d in dom f1 holds f1.d = (p*f2+f3).d proof let d be Nat; assume A34: d in dom f1; then A35: (p*f2+f3).d = (p*f2).d + f3.d by A32,VALUED_1:def 1; d in dom (p*f2) by A31,A34,VALUED_1:def 5; hence (p*f2+f3).d = p * f2.d + f3.d by A35,VALUED_1:def 5 .= f1.d by A33,A34; end; then A36: f1 = p*f2 + f3 by A32,FINSEQ_1:17; A37: p*f2 is Element of NAT* & f3 is Element of NAT* by FINSEQ_1:def 11; dom(p*f2) = dom f2 by VALUED_1:def 5; then len(p*f2) = p' & len f3 = p' by A5,A28,A29,FINSEQ_2:55,FINSEQ_3:31; then p*f2 in p'-tuples_on NAT & f3 in p'-tuples_on NAT by A37; then p*f2 is Element of p'-tuples_on REAL & f3 is Element of p'-tuples_on REAL by FINSEQ_2:129; then A38: Sum f1 = Sum(p*f2) + Sum f3 by A36,RVSUM_1:119 .= p*(Sum f2) + Sum f3 by RVSUM_1:117; then A39: q*(Sum idseq p') = p*(Sum f2) + Sum f3 by RVSUM_1:117; f3 <> {} by A6,A9,A29; then rng f3 is finite non empty Subset of NAT by FINSEQ_1:def 4; then consider n1 be Element of NAT such that A40: rng f3 c= Seg n1 \/ {0} by HEYTING3:3; not 0 in rng f3 proof assume 0 in rng f3; then consider a be Nat such that A41: a in dom f3 & f3.a = 0 by FINSEQ_2:11; f1.a = f2.a * p + 0 by A30,A33,A41; then q*a = f2.a *p by A17,A30,A41; then A42: p divides q*a by NAT_D:def 3; A43: a >= 1 & a <= p' by A6,A29,A41,FINSEQ_3:27; then p <= a by A2,A42,NAT_D:7,PEPIN:3; hence contradiction by A14,A43,XXREAL_0:2; end; then A44: {0} misses rng f3 by ZFMISC_1:56; then A45: rng f3 c= Seg n1 by A40,XBOOLE_1:73; for x,y be set st x in dom f3 & y in dom f3 & f3.x=f3.y holds x=y proof let x,y be set; assume A46: x in dom f3 & y in dom f3 & f3.x=f3.y; then reconsider x,y as Element of NAT; f1.x = f2.x * p + f3.x & f1.y = f2.y * p + f3.y by A30,A33,A46; then f1.x - f1.y = (f2.x - f2.y) * p by A46; then p divides (f1.x - f1.y) by INT_1:def 9; hence thesis by A20,A30,A46; end; then A47: f3 is one-to-one by FUNCT_1:def 8; set f4 = Sgm rng f3; set X = {k where k is Element of NAT:k in rng f4 & k>p/2}; A48: rng f4 = rng f3 by A45,FINSEQ_1:def 13; A49: f4 is one-to-one by A40,A44,FINSEQ_3:99,XBOOLE_1:73; f4 is FinSequence of REAL & f3 is FinSequence of REAL by FINSEQ_2:27; then A50: Sum f4 = Sum f3 by A47,A48,A49,RFINSEQ:22,39; for x being set st x in X holds x in rng f4 proof let x be set; assume x in X; then consider k being Element of NAT such that A51: x = k & k in rng f4 & k > p/2; thus thesis by A51; end; then A52: X c= rng f4 by TARSKI:def 3; then reconsider X as finite Subset of NAT by XBOOLE_1:1; A53: X c= Seg n1 by A45,A48,A52,XBOOLE_1:1; reconsider Y = rng f4 \ X as finite Subset of NAT; A54: rng f4 \ X c= rng f4 by XBOOLE_1:36; then A55: Y c= Seg n1 by A45,A48,XBOOLE_1:1; set m = card X; A56: len f3 = card rng f4 by A47,A48,FINSEQ_4:77; then reconsider n = p' - m as Element of NAT by A6,A29,A52,NAT_1:21,44; len f3 = card rng f3 by A47,FINSEQ_4:77; then A57: len f4 = p' by A6,A29,A40,A44,FINSEQ_3:44,XBOOLE_1:73; A58: f4 = (Sgm Y)^(Sgm X) proof for k,l being Element of NAT st k in Y & l in X holds k < l proof let k,l be Element of NAT; assume A59: k in Y & l in X; then k in rng f4 & not k in X by XBOOLE_0:def 4; then A60: k <= p/2; ex l1 being Element of NAT st l1 = l & l1 in rng f4 & l1>p/2 by A59; hence thesis by A60,XXREAL_0:2; end; then Sgm (Y\/X) = (Sgm Y)^(Sgm X) by A53,A55,FINSEQ_3:48; then Sgm (rng f4 \/ X) = (Sgm Y)^(Sgm X) by XBOOLE_1:39; hence thesis by A48,A52,XBOOLE_1:12; end; then Sum f4 = Sum(Sgm Y) + Sum(Sgm X) by RVSUM_1:105; then A61: q*(Sum idseq p')=p*(Sum f2)+Sum(Sgm Y) + Sum(Sgm X) by A38,A50,RVSUM_1:117; A62: len Sgm Y = n proof len Sgm Y = card Y by A45,A48,A54,FINSEQ_3:44,XBOOLE_1:1 .= p' - m by A6,A29,A52,A56,CARD_2:63; hence thesis; end; then A63: f4/^n = Sgm X by A58,FINSEQ_5:40; f4 = (f4|n)^(f4/^n) by RFINSEQ:21; then A64: f4|n is one-to-one & f4/^n is one-to-one by A49,FINSEQ_3:98; A65: f4|n = Sgm Y by A58,A62,FINSEQ_3:122,FINSEQ_6:12; for d being Nat st d in dom idseq p' holds (idseq p').d in NAT proof let d be Nat; assume A66: d in dom idseq p'; then d in Seg len idseq p' by FINSEQ_1:def 3; then d is Element of Seg p' by FINSEQ_2:55; then (idseq p').d = d by A9,FINSEQ_2:57; hence thesis by A66; end; then idseq p' is FinSequence of NAT by FINSEQ_2:14; then reconsider M = Sum idseq p' as Element of NAT by Lm3; A67: Lege(q,p) = (-1)|^(Sum f2) proof per cases; suppose A68: X is empty; for d st d in dom f4 holds f4.d > 0 & f4.d <= p' proof let d; assume A69: d in dom f4; A70: not f4.d in X by A68; f4.d in rng f4 by A69,FUNCT_1:12; then A71: f4.d <= p/2 by A70; A72: f4.d in rng f3 by A48,A69,FUNCT_1:12; then f4.d in (rng f3)\/{0} by XBOOLE_0:def 2; then not f4.d in {0} by A44,A72,XBOOLE_0:5; then f4.d <> 0 by TARSKI:def 1; hence thesis by A15,A71,INT_1:81; end; then Sgm rng f3 = Sgm(Seg p') by A48,A49,A57,Th40; then q*(Sum idseq p') = p*(Sum f2) + Sum idseq p' by A39,A50,FINSEQ_3:54; then A73: q*(Sum idseq p') - Sum idseq p' = p*(Sum f2); 2 divides (q-'1)*M by A11,NAT_D:9; then 2 divides ((Sum f2)-0) by A4,A8,A73,PEPIN:3; then Sum f2,0 are_congruent_mod 2 by INT_2:19; then (Sum f2) mod 2 = 0 mod 2 by INT_3:12; then (-1)|^m = (-1)|^(Sum f2) by A68,Th45,CARD_1:47; hence thesis by A1,A3,A48,Th41; end; suppose X is non empty; then A74: m <> 0; A75: n <= len f4 by A57,XREAL_1:45; A76: len(f4|n) = n by A57,FINSEQ_1:80,XREAL_1:45; A77: len(f4/^n) = (len f4 -' n) by BINARITH:76 .= len f4 - n by A57,BINARITH:50,XREAL_1:45 .= m by A57; set f5 = (m|->p)-(f4/^n); set f6 = (f4|n)^f5; A78: dom f5 = dom(m |-> p) /\ dom(f4/^n) by VALUED_1:12 .= (Seg len (m |-> p)) /\ dom(f4/^n) by FINSEQ_1:def 3 .= (Seg len(f4/^n))/\dom(f4/^n) by A77,FINSEQ_2:69 .= dom(f4/^n) /\ dom(f4/^n) by FINSEQ_1:def 3 .= dom(f4/^n); then A79: len f5 = len(f4/^n) by FINSEQ_3:31; A80: for d st d in dom f5 holds f5.d = p - (f4/^n).d proof let d; assume A81: d in dom f5; then d in Seg m by A77,A78,FINSEQ_1:def 3; then (m |-> p).d = p by A74,FINSEQ_2:71; hence thesis by A81,VALUED_1:13; end; A82: for d st d in dom f5 holds f5.d > 0 & f5.d <= p' proof let d; assume A83: d in dom f5; then A84: f5.d = p - (f4/^n).d by A80; reconsider w = f5.d as Element of INT by INT_1:def 2; (Sgm X).d in rng Sgm X by A63,A78,A83,FUNCT_1:12; then (Sgm X).d in X by A53,FINSEQ_1:def 13; then consider ll be Element of NAT such that A85: ll = (Sgm X).d & ll in rng f3 & ll > p/2 by A48; A86: w < p - p/2 by A63,A84,A85,XREAL_1:12; consider e being Nat such that A87: e in dom f3 & f3.e = (f4/^n).d by A63,A85,FINSEQ_2:11; (f4/^n).d = f1.e mod p by A30,A87,EULER_2:def 1; then (f4/^n).d < p by NAT_D:1; hence thesis by A15,A84,A86,INT_1:81,XREAL_1:52; end; for d being Nat st d in dom f5 holds f5.d in NAT proof let d be Nat; assume d in dom f5; then f5.d = p - (f4/^n).d & f5.d > 0 by A80,A82; hence thesis by INT_1:16; end; then reconsider f5 as FinSequence of NAT by FINSEQ_2:14; for d,e being Element of NAT st 1<=d & d f5. e proof let d,e be Element of NAT; assume A88: 1<=d & d= 1 & d1 <= p' & e1 >= 1 & e1 <= p' by A6,A29,A94,A98,FINSEQ_3:27; then d1+e1 >= 1+1 & d1+e1 <= p'+p' by XREAL_1:9; then d1+e1>0 & d1+e1 < p by A8,A12,XREAL_1:148,XXREAL_0:2; hence contradiction by A2,A99,NAT_D:7,PEPIN:3; end; then A100: f6 is one-to-one by A64,A90,FINSEQ_3:98; for d st d in dom f6 holds f6.d>0 & f6.d <= p' proof let d; assume A101: d in dom f6; per cases by A101,FINSEQ_1:38; suppose A102: d in dom(f4|n); then (f4|n).d in rng Sgm Y by A65,FUNCT_1:12; then (f4|n).d in Y by A55,FINSEQ_1:def 13; then A103: (f4|n).d in rng f4 & not (f4|n).d in X by XBOOLE_0:def 4; then (f4|n).d <= p/2; then A104: (f4|n).d <= p' by A15,INT_1:81; not (f4|n).d in {0} by A44,A48,A103,XBOOLE_0:3; then (f4|n).d <> 0 by TARSKI:def 1; then (f4|n).d > 0; hence thesis by A102,A104,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 A105: l in dom f5 & d = len(f4|n)+ l; f6.d = f5.l by A105,FINSEQ_1:def 7; hence thesis by A82,A105; end; end; then A106: rng f6 = rng idseq p' by A91,A92,A100,Th40; A107: f6 is FinSequence of REAL & f4/^n is FinSequence of REAL by FINSEQ_2:27; then M = Sum f6 by A100,A106,RFINSEQ:22,39 .= Sum(f4|n) + Sum f5 by RVSUM_1:105 .= Sum(f4|n) + (m*p - Sum(f4/^n)) by A77,A107,Th47 .= Sum(f4|n) + m*p - Sum(f4/^n); then (q-1)*M = p*(Sum f2) + 2*Sum(Sgm X) - m*p by A61,A63,A65; then A108: (q-'1)*M mod 2 = ((p*(Sum f2)-m*p) + 2*Sum(Sgm X)) mod 2 by A7,BINARITH:50 .= (p*(Sum f2)-m*p) mod 2 by EULER_1:13; 2 divides (q-'1)*M by A11,NAT_D:9; then (q-'1)*M mod 2 = 0 by PEPIN:6; then 2 divides (p*((Sum f2)-m)) by A108,Lm1; then 2 divides ((Sum f2) - m) by A4,INT_2:40; then (Sum f2),m are_congruent_mod 2 by INT_2:19; then (Sum f2) mod 2 = m mod 2 by INT_3:12; then (-1)|^(Sum f2) = (-1)|^m by Th45; hence thesis by A1,A3,A48,Th41; end; end; set g1 = p*idseq q'; dom g1 = dom idseq q' by VALUED_1:def 5; then len g1 = len idseq q' by FINSEQ_3:31; then A109: len g1 = q' by FINSEQ_2:55; A110: for d st d in dom g1 holds g1.d = p*d proof let d; assume A111: d in dom g1; then A112: g1.d = p * (idseq q').d by VALUED_1:def 5; d in dom idseq q' by A111,VALUED_1:def 5; then d in Seg len idseq q' by FINSEQ_1:def 3; then d is Element of Seg q' by FINSEQ_2:55; hence thesis by A9,A112,FINSEQ_2:57; end; for d being Nat st d in dom g1 holds g1.d in NAT proof let d be Nat; assume d in dom g1; then g1.d = p*d by A110; hence thesis; end; then reconsider g1 as FinSequence of NAT by FINSEQ_2:14; A113: for d,e st d in dom g1 & e in dom g1 & q divides (g1.d-g1.e) holds d=e proof let d,e; assume A114: d in dom g1 & e in dom g1 & q divides (g1.d-g1.e); then g1.d = p*d & g1.e = p*e by A110; then A115: q divides (d-e)*p by A114; A116: q,(p qua Integer) are_relative_prime by A1,INT_2:47; now assume d <> e; then d-e <> 0; then abs(q) <= abs(d-e) by A115,A116,INT_2:40,INT_4:6; then A117: q <= abs(d-e) by ABSVALUE:def 1; d>=1 & d<=q' & e>=1 & e<=q' by A109,A114,FINSEQ_3:27; then A118: d-e<=q'-1 & d-e>=1-q' by XREAL_1:15; A119: q'-1 -q by A119,XREAL_1:26; then d-e > -q by A118,XXREAL_0:2; hence contradiction by A117,A120,SEQ_2:9; end; hence thesis; end; deffunc F(Nat) = g1.$1 div q; consider g2 be FinSequence such that A121: len g2 = q' & 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 A121; hence thesis; end; then reconsider g2 as FinSequence of NAT by FINSEQ_2:14; set g3 = g1 mod q; A122: len g3 = len g1 by EULER_2:def 1; then A123: dom g1 = dom g3 by FINSEQ_3:31; A124: dom g1 = dom g2 by A109,A121,FINSEQ_3:31; A125: 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 A123,A124; A126: for d st d in dom g1 holds g1.d = g2.d * q + g3.d proof let d; assume d in dom g1; then g2.d = g1.d div q & g3.d = g1.d mod q by A121,A124,EULER_2:def 1; hence g1.d = g2.d * q + g3.d by NAT_D:2; end; for d being Nat st d in dom g1 holds g1.d = (q*g2+g3).d proof let d be Nat; assume A127: d in dom g1; then A128: (q*g2+g3).d = (q*g2).d + g3.d by A125,VALUED_1:def 1; d in dom (q*g2) by A124,A127,VALUED_1:def 5; hence (q*g2+g3).d = q * g2.d + g3.d by A128,VALUED_1:def 5 .= g1.d by A126,A127; end; then A129: g1 = q*g2 + g3 by A125,FINSEQ_1:17; A130: q*g2 is Element of NAT* & g3 is Element of NAT* by FINSEQ_1:def 11; dom(q*g2) = dom g2 by VALUED_1:def 5; then len(q*g2) = q' & len g3 = q' by A109,A121,EULER_2:def 1,FINSEQ_3:31; then q*g2 in q'-tuples_on NAT & g3 in q'-tuples_on NAT by A130; then q*g2 is Element of q'-tuples_on REAL & g3 is Element of q'-tuples_on REAL by FINSEQ_2:129; then A131: Sum g1 = Sum(q*g2) + Sum g3 by A129,RVSUM_1:119 .= q*(Sum g2) + Sum g3 by RVSUM_1:117; len g3 >=1 by A9,A109,EULER_2:def 1; then g3 <> {}; then rng g3 is finite non empty Subset of NAT by FINSEQ_1:def 4; then consider n2 be Element of NAT such that A132: rng g3 c= Seg n2 \/ {0} by HEYTING3:3; not 0 in rng g3 proof assume 0 in rng g3; then consider a be Nat such that A133: a in dom g3 & g3.a = 0 by FINSEQ_2:11; a in dom g1 by A122,A133,FINSEQ_3:31; then A134: g1.a = g2.a * q + 0 by A126,A133; a in dom g1 by A122,A133,FINSEQ_3:31; then p*a = g2.a * q by A110,A134; then A135: q divides p*a by NAT_D:def 3; A136: a >= 1 & a <= q' by A109,A122,A133,FINSEQ_3:27; then q <= a by A2,A135,NAT_D:7,PEPIN:3; hence contradiction by A14,A136,XXREAL_0:2; end; then A137: {0} misses rng g3 by ZFMISC_1:56; then A138: rng g3 c= Seg n2 by A132,XBOOLE_1:73; for x,y be set st x in dom g3 & y in dom g3 & g3.x=g3.y holds x=y proof let x,y be set; assume A139: x in dom g3 & y in dom g3 & g3.x=g3.y; then reconsider x,y as Element of NAT; g1.x = g2.x * q + g3.x & g1.y = g2.y * q + g3.y by A123,A126,A139; then g1.x - g1.y = (g2.x - g2.y) * q by A139; then q divides (g1.x - g1.y) by INT_1:def 9; hence thesis by A113,A123,A139; end; then A140: g3 is one-to-one by FUNCT_1:def 8; set g4 = Sgm rng g3; set XX = {k where k is Element of NAT:k in rng g4 & k>q/2}; A141: rng g4 = rng g3 by A138,FINSEQ_1:def 13; A142: g4 is one-to-one by A132,A137,FINSEQ_3:99,XBOOLE_1:73; g4 is FinSequence of REAL & g3 is FinSequence of REAL by FINSEQ_2:27; then A143: Sum g4 = Sum g3 by A140,A141,A142,RFINSEQ:22,39; for x being set st x in XX holds x in rng g4 proof let x be set; assume x in XX; then consider k being Element of NAT such that A144: x = k & k in rng g4 & k > q/2; thus thesis by A144; end; then A145: XX c= rng g4 by TARSKI:def 3; then reconsider XX as finite Subset of NAT by XBOOLE_1:1; reconsider YY = rng g4 \ XX as finite Subset of NAT; A146: rng g4 \ XX c= rng g4