:: 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; notations GROUP_4, INT_1, RVSUM_1, FUNCT_2, FINSET_1, ORDINAL1, CARD_1, NAT_D, INT_2, FUNCT_1, PARTFUN1, 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, RELSET_1, FINSEQ_1, BINARITH, RFINSEQ, FUNCOP_1, CALCUL_2, ZFMISC_1, CARD_3, WSIERP_1, BINOP_1, PROB_3; 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; registrations XXREAL_0, MEMBERED, RELAT_1, FINSEQ_1, ORDINAL1, WSIERP_1, NUMBERS, XBOOLE_0, XREAL_0, NAT_1, INT_1, SEQ_1, FINSET_1, NAT_3, RVSUM_1, FUNCOP_1, CALCUL_2, FUNCT_1, CARD_1, NEWTON, SUBSET_1, POLYNOM1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions INT_1, FUNCT_1, XCMPLX_0, INT_2, SQUARE_1, FINSEQ_2, TARSKI, CALCUL_2, CARD_3, CARD_1; 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, SEQ_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; schemes NAT_1, FINSEQ_5, 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:n1 gcd n2 = n1 hcf n2 proof abs n1 = n1 & abs n2 = n2 by ABSVALUE:def 1; hence thesis; end; Lm2: (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 Element of NAT st d in dom fr holds fr.d = G(d) from FINSEQ_5:sch 1; for d being Nat st d in dom fr holds fr.d in INT proof let d be Nat;assume d in dom fr; then fr.d = (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 proof x in INT by INT_1:def 2;then (Poly-INT fp).x in INT by FUNCT_2:7; hence thesis by INT_1:def 2; end; 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: n+1 in NAT by ORDINAL1:def 13; A8:dom f3 = Seg(n+1) & f = f3^<*f.(n+1+1)*> by A6,FINSEQ_3:60,61; then A9:len f3 = n+1 by A7,FINSEQ_1:def 3; set ff1 = f1|Seg(n+1); reconsider ff1 as FinSequence of REAL by FINSEQ_1:23; A10: 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; A11: 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 A12:d in dom f3; A13: dom f3 c= dom f by A8,FINSEQ_1:39; A14: f3.d = f.d by A8,A12,FINSEQ_1:def 7 .= f1.d - f2.d by A6,A12,A13; d in dom ff1 & d in dom ff2 by A8,A10,A11,A12,FINSEQ_1:def 3; then f1.d = ff1.d & f2.d = ff2.d by A10,A11,FINSEQ_1:def 7; hence thesis by A14; end; 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 + ff1.(n+1) - ff2.1 by A5,A9,A10,A11; ff1 <> {} & ff2 <> {} by A10,A11,FINSEQ_1:25; then 1 in dom ff2 & (n+1) in dom ff1 by A10,FINSEQ_5:6; then ff2.1 = f2.1 & ff1.(n+1) = f1.(n+1) by A10,A11,FINSEQ_1:def 7; then consider f4 being FinSequence of REAL such that A16: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 A15; 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; A17: n+1 in NAT by ORDINAL1:def 13; A18:len f5 = len f4 + 1 by FINSEQ_2:19 .= len f - 1 by A6,A8,A16,A17,FINSEQ_1:def 3; A19:len f4 + 1 = n + 1 by A8,A16,A17,FINSEQ_1:def 3; A20: 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 A21:d in Seg len f4 or d in {len f4 + 1} by XBOOLE_0:def 2; per cases by A21,TARSKI:def 1; suppose A22:d in Seg len f4; then A23:d in dom f4 by FINSEQ_1:def 3; then A24:f5.d = f4.d by FINSEQ_1:def 7 .= ff1.d - ff2.(d+1) by A16,A23; len f4 <= len ff1 & len f4 + 1 <= len ff2 by A6,A9,A10,A16,FINSEQ_3:59,XREAL_1:149; then dom f4 c= dom ff1 by FINSEQ_3:32; then A25:f1.d = ff1.d by A10,A23,FINSEQ_1:def 7; A26: d+1 in Seg(len f4 + 1) by A22,FINSEQ_1:81; d+1 in Seg len ff2 by A6,A9,A16,A26,FINSEQ_3:59; then d+1 in dom ff2 by FINSEQ_1:def 3; hence thesis by A11,A24,A25,FINSEQ_1:def 7; end; suppose A27:d = len f4 + 1; 1 in Seg 1 by FINSEQ_1:4,TARSKI:def 1; then A28:1 in dom <*f1.(n+1) - f2.(n+2)*> by FINSEQ_1:55; f5.d = <*f1.(n+1) - f2.(n+2)*>.1 by A27,A28,FINSEQ_1:def 7 .= f1.d - f2.(d+1) by A19,A27,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 A29: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 A8,A16,RVSUM_1:104 .= Sum f4 + (f1.(n+1) - f2.(n+2)) + f1.((n+1)+1) - f2.1 by A29 .= Sum f5 + f1.((n+1)+1) - f2.1 by RVSUM_1:104; hence thesis by A18,A20; 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 by ORDINAL1:def 13; 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 6(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,FINSEQ_1:25; 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,SEQ_1:def 6; thus f3.k = (x-a)*(f2.k) by A9,SEQ_1:def 6 .= (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 Element of NAT st d in dom f4 holds f4.d=F(d) from FINSEQ_5:sch 1; consider f5 being FinSequence such that A13: len f5 = n+1 & for d being Element of NAT st d in dom f5 holds f5.d=FF(d) from FINSEQ_5:sch 1; f4 <> {} & f5 <> {} by A12,A13,FINSEQ_1:25; 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 SEQ_1:def 6;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; f4.d = (fr.d)*x|^d & f5.d = a*(fr.d) * x|^(d-'1) by A12,A13,A16,A19; 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; d in Seg n by A4,A7,A17,A20,A24,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; thus K.d = (<*f1.1*>^(f6^<*f1.(n+2)*>)).1 by A33,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,FINSEQ_1:25; 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,Lm2; 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,FINSEQ_1:25; 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 A17:((f.d-a)*(Poly-INT fk).(f.d)) mod p = 0 by A14,A16; thus thesis by A17,INT_1:89; end; per cases; suppose A18: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 A19: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 A18,A19,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 A20:d' in dom f & p divides (f.d' - a); set f' = f - {f.d'}; A21: f is one-to-one proof let x1,x2 be set; assume A22: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,A22; hence contradiction by A22,INT_1:32; end; then A23:f' is one-to-one by FINSEQ_3:94; A24: for d st d in dom f' holds not p divides (f'.d - a) proof given k being Nat such that A25: k in dom f' & p divides (f'.k -a); f'.k in rng f' by A25,FUNCT_1:12; then f'.k in rng f \ {f.d'} by FINSEQ_3:72; then A26:f'.k in rng f & not f'.k in {f.d'} by XBOOLE_0:def 4; then consider w being set such that A27: w in dom f & f.w = f'.k by FUNCT_1:def 5; reconsider w as Element of NAT by A27; p divides ((f.w - a)-(f.d' - a)) by A20,A25,A27,Th1; then p divides (f.w - f.d'); then A28:f.w,f.d' are_congruent_mod p by INT_2:19; w <> d' by A26,A27,TARSKI:def 1; hence contradiction by A14,A20,A27,A28; end; A29: for d st d in dom f' holds (Poly-INT fk).(f'.d) mod p = 0 proof let d; assume A30:d in dom f'; f'.d in rng f' by A30,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 A31: w in dom f & f.w = f'.d by FUNCT_1:def 5; reconsider w as Element of NAT by A31; p divides (f'.d -a)*(Poly-INT fk).(f'.d) by A15,A31; then p divides (f'.d -a) or p divides (Poly-INT fk).(f'.d) by Th7; hence thesis by A24,A30,INT_1:89; end; A32: 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 A33: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 A34:f'.d in rng f & f'.e in rng f by XBOOLE_0:def 4; then consider w1 being set such that A35: w1 in dom f & f'.d = f.w1 by FUNCT_1:def 5; consider w2 being set such that A36: w2 in dom f & f'.e = f.w2 by A34,FUNCT_1:def 5; reconsider w1,w2 as Element of NAT by A35,A36; w1 <> w2 by A23,A33,A35,A36,FUNCT_1:def 8; hence thesis by A14,A35,A36; end; f.d' in rng f by A20,FUNCT_1:12; then len f' = len f - 1 by A21,FINSEQ_3:97; then len f' > (n+1)-1 by A14,XREAL_1:11; hence contradiction by A7,A8,A12,A29,A32; 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 Lm2; (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; Lm3:i,p are_relative_prime or p divides i proof A1: p in NAT by ORDINAL1:def 13; 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 A1,EULER_2:1,NAT_D:def 5; end; suppose A2:i<0; then -i>0 by XREAL_1:60; then reconsider m = -i as Element of NAT by INT_1:16; A3: m,p are_relative_prime or (m hcf p) = p by PEPIN:2; per cases by A3,NAT_D:def 5; suppose A4:m,p are_relative_prime; i gcd p = m hcf abs(p) by A2,ABSVALUE:def 1 .= m hcf p by ABSVALUE:def 1 .= 1 by A4,INT_2:def 6; hence thesis by INT_2:def 4; end; suppose p divides m; then consider t being Nat such that A5:m = p * t by NAT_D:def 3; i = p * (-t) by A5; 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; hence thesis by NEWTON:62; end; registration let k be Integer, a be Nat; cluster k |^ a -> integer; coherence proof reconsider a as Element of NAT by ORDINAL1:def 13; k |^ a is integer; hence thesis; end; 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 Lm2; assume not x,p are_relative_prime; then p divides x by Lm3; then p divides x^2 by 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 6; then 2 gcd p = 1 by Lm1; 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 divides 1 by A1,WSIERP_1:36; then p <= 1 by NAT_D:7; 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 proof reconsider d as Element of NAT by ORDINAL1:def 13; fp.d is natural; hence thesis; end; 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; A2: p in NAT by ORDINAL1:def 13; 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 Element of NAT st d in dom fp holds fp.d = F(d) from FINSEQ_5:sch 1; 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; A10: d in NAT by ORDINAL1:def 13; 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 A2,A8,A10,EULER_1:3; hence thesis by INT_2:def 6; end; A11:for d st d in dom fp holds fp.d hcf p = 1 proof let d; assume A12:d in dom fp; A13: d in NAT by ORDINAL1:def 13; d hcf p = 1 by A7,A12; then d^2 hcf p = 1 by A2,A13,WSIERP_1:12; hence thesis by A6,A12; end; A14:for d st d in dom fp holds fp.d is_quadratic_residue_mod p proof let d;assume A15:d in dom fp; then d hcf p = 1 by A7; then d gcd p = 1 by Lm1; then d^2 is_quadratic_residue_mod p by Th9; hence thesis by A6,A15; end; A16: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 A17:d in dom fp & e in dom fp & d<>e; A18: d+e in NAT by ORDINAL1:def 13; d in Seg ((p-'1) div 2) & e in Seg ((p-'1) div 2) by A6,A17,FINSEQ_1:def 3; then A19: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 A2,A18,EULER_1:3; then (d+e) hcf p = 1 by INT_2:def 6; then A20:(d+e) gcd p = 1 by Lm1; 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,A17; then p divides (d^2 - e^2) by A6,A17; then p divides (d - e)*(d+e); then A21:p divides (d - e) by A20,WSIERP_1:36; d-e <> 0 by A17; then abs(p) <= abs(d-e) by A21,INT_4:6; then A22:p <= abs(d-e) by ABSVALUE:def 1; 1-((p-'1) div 2) <= d-e & d-e <= ((p-'1) div 2) - 1 by A19,XREAL_1:15; then -(((p-'1) div 2) - 1) <= d-e & d-e <= ((p-'1) div 2) - 1; then A23: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 A22,A23,XXREAL_0:2; end; take fp; thus thesis by A6,A11,A14,A16; 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 hcf p = s gcd p by Lm1 .= 1 by A5,INT_2:def 4; then s,p are_relative_prime by INT_2:def 6; 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; s' hcf p = s' gcd p by Lm1 .= abs(s) gcd p by A7,ABSVALUE:def 1 .= s gcd p .= 1 by A5,INT_2:def 4; then s',p are_relative_prime by INT_2:def 6; then A8: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,A8,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 hcf p = 1 by A1,Lm1; then b,p are_relative_prime by INT_2:def 6; 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,Lm2; 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 Lm2; 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 Lm2; 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 A41:fp.d hcf p = 1 & fp.d is_quadratic_residue_mod p by A34; then fp.d gcd p = 1 by Lm1; then A42:(fp.d)|^l mod p = 1 mod p by A1,A4,A41,Th17; reconsider k = fp.d as Element of INT by INT_1:def 2; (k|^l - 1) mod p = 0 by A42,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; A43: 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 A44:d in dom f & e in dom f & d<>e; then A45:d>=1 & d<= l+1 & e>=1 & e<=l+1 by A37,FINSEQ_3:27; per cases by A45,REAL_1:def 5; suppose d>=1 & d=1 & d<=l by NAT_1:13; then A46:d in dom fp by A34,FINSEQ_3:27; then A47:f.d = fp.d by FINSEQ_1:def 7; per cases by A45,REAL_1:def 5; suppose e>=1 & e=1 & e<=l by NAT_1:13; then A48:e in dom fp by A34,FINSEQ_3:27; then not fp.d,fp.e are_congruent_mod p by A34,A44,A46; hence thesis by A47,A48,FINSEQ_1:def 7; end; suppose A49:e=l+1; not f.d,b are_congruent_mod p proof assume f.d,b are_congruent_mod p; then A50:p divides (f.d - b) by INT_2:19; A51: f.d is_quadratic_residue_mod p & f.d hcf p = 1 by A34,A46,A47; consider j being Integer such that A52: (j^2 - f.d) mod p = 0 by A51,Def2; p divides (j^2 - f.d) by A52,INT_1:89; then p divides ((j^2 - f.d)+(f.d - b)) by A50,WSIERP_1:9; then (j^2 - b) mod p = 0 by INT_1:89; hence contradiction by A1,Def2; end; hence thesis by A34,A49,FINSEQ_1:59; end; end; suppose A53:d=l+1; e>=1 & e<=l by A44,A45,A53,NAT_1:8; then A54:e in dom fp by A34,FINSEQ_3:27; then f.e = fp.e by FINSEQ_1:def 7;then A55: f.e is_quadratic_residue_mod p & f.e hcf p = 1 by A34,A54; consider j being Integer such that A56: (j^2 - f.e) mod p = 0 by A55,Def2; A57: p divides (j^2 - f.e) by A56,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 A57,Th1; then (j^2 - b) mod p = 0 by INT_1:89; hence contradiction by A1,Def2; end; hence thesis by A34,A53,FINSEQ_1:59; end; end; A58: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,A43,A58,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 A59:(b|^l + 1) = p*k by NAT_D:def 3; -p < -1 by A3,XREAL_1:26; then A60:(-1) mod p = (-1) + p by INT_3:10; b|^l mod p = (p*k + (- 1)) mod p by A59 .= p - 1 by A60,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; l>=0 by INT_1:84; then reconsider l as Element of NAT by INT_1:16; A2:l mod p = a mod p by INT_3:13; then A3:l,a are_congruent_mod p by INT_3:12; then A4:l gcd p = 1 by A1,INT_4:14; not l is_quadratic_residue_mod p by A1,A3,A4,Th11; then l|^((p-'1) div 2) mod p = p - 1 by A1,A4,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; consider i being Integer such that A2:(i^2 - a) mod p =0 by A1,Def2; consider j being Integer such that A3:(j^2 - b) mod p =0 by A1,Def2; p divides (i^2 - a) & p divides (j^2 - b) by A2,A3,INT_1:89; then i^2,a are_congruent_mod p & j^2,b are_congruent_mod p by INT_2:19; then (i^2)*(j^2),a*b are_congruent_mod p by INT_1:39; then p divides ((i*j)^2 - a*b) by INT_2:19; then ((i*j)^2 - a*b) mod p = 0 by INT_1:89; hence thesis by Def2; end; theorem p>2 & a gcd p = 1 & b gcd p = 1 & a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p implies not a*b is_quadratic_residue_mod p proof assume A1:p>2 & a gcd p = 1 & b gcd p = 1 & a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p; then A2:a*b gcd p = 1 by WSIERP_1:11; set l = (p-'1) div 2; (a|^l -1) mod p = 0 & (b|^l + 1) mod p = 0 by A1,Th20,Th21; then A3:p divides (a|^l -1) & p divides (b|^l + 1) by INT_1:89; then A4:p divides (a|^l -1)*(b|^l +1) by INT_2:12; A5:(a|^l -1)*(b|^l +1) = a|^l * b|^l +a|^l*1 -1*b|^l -1*1 .= (a*b)|^l +a|^l*1 -1*b|^l -1*1 by NEWTON:12 .= ((a*b)|^l -1) +(a|^l - 1) -(b|^l - 1); now assume a*b is_quadratic_residue_mod p; then ((a*b)|^l -1) mod p = 0 by A1,A2,Th20; then p divides ((a*b)|^l -1) by INT_1:89; then p divides ((a*b)|^l -1) +(a|^l - 1) by A3,WSIERP_1:9; then p divides (b|^l - 1) by A4,A5,Th2; then p divides ((b|^l +1) - (b|^l -1)) by A3,Th1; hence contradiction by A1,NAT_D:7; end; hence thesis; end; theorem p>2 & a gcd p = 1 & b gcd p = 1 & not a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p implies a*b is_quadratic_residue_mod p proof assume A1:p>2 & a gcd p = 1 & b gcd p = 1 & not a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p; then A2:a*b gcd p = 1 by WSIERP_1:11; set l = (p-'1) div 2; (a|^l +1) mod p = 0 & (b|^l + 1) mod p = 0 by A1,Th21; then A3:p divides (a|^l +1) & p divides (b|^l + 1) by INT_1:89; then A4:p divides (a|^l +1)*(b|^l +1) by INT_2:12; A5:(a|^l +1)*(b|^l +1) = a|^l * b|^l +a|^l*1 +1*b|^l +1*1 .= (a*b)|^l +a|^l + b|^l +1 by NEWTON:12 .= ((a*b)|^l +1) +(a|^l + 1) - (1- b|^l); now assume not a*b is_quadratic_residue_mod p; then ((a*b)|^l +1) mod p = 0 by A1,A2,Th21; then p divides ((a*b)|^l +1) by INT_1:89; then p divides ((a*b)|^l +1) +(a|^l + 1) by A3,WSIERP_1:9; then p divides (1- b|^l) by A4,A5,Th2; then p divides ((b|^l +1) + (1- b|^l)) by A3,WSIERP_1:9; hence contradiction by A1,NAT_D:7; end; hence thesis; end; definition let a be Integer, p be Prime; func Lege (a,p) -> Integer equals :Def3: 1 if a is_quadratic_residue_mod p otherwise -1;:: if not a is_quadratic_residue_mod p; coherence; consistency; end; theorem Th25: Lege (a,p) = 1 or Lege (a,p) = -1 proof per cases; suppose a is_quadratic_residue_mod p; hence thesis by Def3; end; suppose not a is_quadratic_residue_mod p; hence thesis by Def3; end; end; theorem Th26: a gcd p = 1 implies Lege (a^2,p) = 1 proof assume a gcd p = 1; then a^2 is_quadratic_residue_mod p by Th9; hence thesis by Def3; end; theorem Lege (1,p) = 1 proof 1 gcd p = 1 by WSIERP_1:13; then Lege (1^2,p) = 1 by Th26; hence thesis; end; theorem Th28: p>2 & a gcd p =1 implies Lege (a,p),a|^((p-'1) div 2) are_congruent_mod p proof assume A1:p>2 & a gcd p = 1; A2:p>1 by INT_2:def 5; then -p < -1 by XREAL_1:26; then A3:(-1) mod p = p+(-1) by INT_3:10; per cases; suppose A4:a is_quadratic_residue_mod p; then a|^((p-'1) div 2) mod p = 1 by A1,Th17; then a|^((p-'1) div 2) mod p = 1 mod p by A2,NAT_D:14; then a|^((p-'1) div 2) mod p = Lege (a,p) mod p by A4,Def3; hence thesis by INT_3:12; end; suppose A5:not a is_quadratic_residue_mod p; then a|^((p-'1) div 2) mod p = p-1 by A1,Th19 .= Lege (a,p) mod p by A3,A5,Def3; hence thesis by INT_3:12; end; end; theorem p>2 & a gcd p =1 & a,b are_congruent_mod p implies Lege (a,p) = Lege (b,p) proof assume A1:p>2 & a gcd p =1 & a,b are_congruent_mod p; then b gcd p = 1 by INT_4:14; then Lege (a,p),a|^((p-'1) div 2) are_congruent_mod p & Lege (b,p),b|^((p-'1) div 2) are_congruent_mod p by A1,Th28; then A2:Lege (a,p) mod p = a|^((p-'1) div 2) mod p & Lege (b,p) mod p = b|^((p-'1) div 2) mod p by INT_3:12; a mod p = b mod p by A1,INT_3:12; then Lege (a,p) mod p = Lege (b,p) mod p by A2,Th13; then Lege (a,p),Lege (b,p) are_congruent_mod p by INT_3:12; then A3:p divides (Lege (a,p) - Lege (b,p)) by INT_2:19; per cases by Th25; suppose A4:Lege (a,p) = 1; Lege (b,p) <> -1 by A1,A3,A4,NAT_D:7; hence thesis by A4,Th25; end; suppose A5:Lege (a,p) = -1; now assume Lege (b,p) = 1; then p divides -2 by A3,A5; then p divides 2 by INT_2:14; hence contradiction by A1,NAT_D:7; end; hence thesis by A5,Th25; end; end; theorem p>2 & a gcd p=1 & b gcd p=1 implies Lege(a*b,p)=Lege(a,p)*Lege(b,p) proof assume A1:p>2 & a gcd p=1 & b gcd p=1; then Lege(a,p),a|^((p-'1) div 2) are_congruent_mod p & Lege(b,p),b|^((p-'1) div 2) are_congruent_mod p by Th28; then Lege(a,p)*Lege(b,p),(a|^((p-'1) div 2))*(b|^((p-'1) div 2)) are_congruent_mod p by INT_1:39; then Lege(a,p)*Lege(b,p),(a*b)|^((p-'1) div 2) are_congruent_mod p by NEWTON:12; then A2:(a*b)|^((p-'1) div 2),Lege(a,p)*Lege(b,p) are_congruent_mod p by INT_1:35; a*b gcd p = 1 by A1,WSIERP_1:11; then Lege(a*b,p),(a*b)|^((p-'1) div 2) are_congruent_mod p by A1,Th28; then Lege(a*b,p),Lege(a,p)*Lege(b,p) are_congruent_mod p by A2,INT_1:36; then A3:p divides (Lege(a*b,p)-Lege(a,p)*Lege(b,p)) by INT_2:19; A4: (Lege(a,p) = 1 or Lege(a,p) = -1) & (Lege(b,p) = 1 or Lege(b,p) = -1) by Th25; per cases by Th25; suppose Lege(a*b,p) = 1; hence thesis by A1,A3,A4,NAT_D:7; end; suppose A5:Lege(a*b,p) = -1; now assume Lege(a,p)*Lege(b,p) <> -1; then p divides (-2) by A3,A4,A5; then p divides 2 by INT_2:14; hence contradiction by A1,NAT_D:7; end; hence thesis by A5; end; end; theorem Th31: (for d st d in dom fr holds fr.d = 1 or fr.d = -1) implies Product fr = 1 or Product fr = -1 proof defpred P[FinSequence of INT] means (for d st d in dom $1 holds $1.d = 1 or $1.d = -1) implies Product $1 = 1 or Product $1 = -1; A1: P[<*>INT] by RVSUM_1:124; A2: for p being FinSequence of INT, n being Element of INT st P[p] holds P[p^<*n*>] proof let p be FinSequence of INT,i be Element of INT; assume A3:P[p]; set p1 = p^<*i*>; P[p1] proof assume A4:(for d st d in dom p1 holds p1.d = 1 or p1.d = -1); A5: for d st d in dom p holds p.d = 1 or p.d = -1 proof let d;assume A6:d in dom p; then d in dom p1 by FINSEQ_2:18; then p1.d = 1 or p1.d = -1 by A4; hence thesis by A6,FINSEQ_1:def 7; end; A7: len p1 =len p +1 by FINSEQ_2:19; len p1 in dom p1 by FINSEQ_5:6; then A8:p1.(len p + 1) = 1 or p1.(len p + 1) = -1 by A4,A7; A9: Product p1 = (Product p)*i by RVSUM_1:126; per cases by A3,A5,A8,FINSEQ_1:59; suppose Product p = 1 & i =1; hence thesis by A9; end; suppose Product p = 1 & i = -1; hence thesis by A9; end; suppose Product p = -1 & i =1; hence thesis by A9; end; suppose Product p = -1 & i = -1; hence thesis by A9; end; end; hence thesis; end; for p being FinSequence of INT holds P[p] from FINSEQ_2:sch 2(A1,A2); hence thesis; end; reserve m for Integer; theorem Th32: for f,fr st len f = len fr & (for d st d in dom f holds f.d,fr.d are_congruent_mod m) holds Product f,Product fr are_congruent_mod m proof defpred P[Nat] means for f,fr st len f =$1 & len f=len fr & (for d st d in dom f holds f.d,fr.d are_congruent_mod m) holds Product f,Product fr are_congruent_mod m; A1:P[0] proof let f,fr; assume len f = 0 & len f = len fr; then f = <*>INT & fr = <*>INT by FINSEQ_1:25; hence thesis by INT_1:32; end; A2:for n be Element of NAT st P[n] holds P[n+1] proof let n be Element of NAT; assume A3:P[n]; P[n+1] proof let f,fr; assume A4:len f = n+1 & len f = len fr & (for d st d in dom f holds f.d,fr.d are_congruent_mod m); consider f1 being FinSequence of INT,a being Element of INT such that A5:f = f1^<*a*> by A4,FINSEQ_2:22; consider fr1 being FinSequence of INT,b being Element of INT such that A6:fr = fr1^<*b*> by A4,FINSEQ_2:22; A7:n+1 = len f1 +1 & n+1 = len fr1 +1 by A4,A5,A6,FINSEQ_2:19; then A8:dom f1 = dom fr1 by FINSEQ_3:31; for d st d in dom f1 holds f1.d,fr1.d are_congruent_mod m proof let d;assume A9:d in dom f1; then A10:f.d = f1.d & fr.d = fr1.d by A5,A6,A8,FINSEQ_1:def 7; d in dom f & d in dom fr by A5,A6,A8,A9,FINSEQ_2:18; hence thesis by A4,A10; end; then A11:Product f1,Product fr1 are_congruent_mod m by A3,A7; f <> {} by A4,FINSEQ_1:25; then A12:(n+1) in dom f by A4,FINSEQ_5:6; f.(n+1) = a & fr.(n+1) = b by A5,A6,A7,FINSEQ_1:59; then a,b are_congruent_mod m by A4,A12; then (Product f1)*a,(Product fr1)*b are_congruent_mod m by A11,INT_1:39; then Product f,(Product fr1)*b are_congruent_mod m by A5,RVSUM_1:126; hence thesis by A6,RVSUM_1:126; end; hence thesis; end; for n be Element of NAT holds P[n] from NAT_1:sch 1(A1,A2); hence thesis; end; theorem Th33: for f,fr st len f = len fr & (for d st d in dom f holds f.d,-fr.d are_congruent_mod m) holds Product f,((-1)|^(len f))*Product fr are_congruent_mod m proof defpred P[Nat] means for f,fr st len f =$1 & len f=len fr & (for d st d in dom f holds f.d,-fr.d are_congruent_mod m) holds Product f,((-1)|^(len f))* Product fr are_congruent_mod m; A1:P[0] proof let f,fr; assume A2:len f = 0 & len f = len fr; then A3:f = <*>INT & fr = <*>INT by FINSEQ_1:25; (-1)|^(len f) = 1 by A2,NEWTON:9; hence thesis by A3,INT_1:32; end; A4:for n be Element of NAT st P[n] holds P[n+1] proof let n be Element of NAT; assume A5:P[n]; P[n+1] proof let f,fr; assume A6:len f = n+1 & len f = len fr & (for d st d in dom f holds f.d,-fr.d are_congruent_mod m); consider f1 be FinSequence of INT,a be Element of INT such that A7:f = f1^<*a*> by A6,FINSEQ_2:22; consider fr1 be FinSequence of INT,b be Element of INT such that A8: fr = fr1^<*b*> by A6,FINSEQ_2:22; A9:n+1 = len f1 +1 & n+1 = len fr1 +1 by A6,A7,A8,FINSEQ_2:19; then A10:dom f1 = dom fr1 by FINSEQ_3:31; for d st d in dom f1 holds f1.d,-fr1.d are_congruent_mod m proof let d;assume A11:d in dom f1; then A12:f.d = f1.d & fr.d = fr1.d by A7,A8,A10,FINSEQ_1:def 7; d in dom f & d in dom fr by A7,A8,A10,A11,FINSEQ_2:18; hence thesis by A6,A12; end; then A13:Product f1,((-1)|^(len f1))*Product fr1 are_congruent_mod m by A5,A9; f <> {} by A6,FINSEQ_1:25; then A14:(n+1) in dom f by A6,FINSEQ_5:6; f.(n+1) = a & fr.(n+1) = b by A7,A8,A9,FINSEQ_1:59; then a,-b are_congruent_mod m by A6,A14;then (Product f1)*a,((-1)|^(len f1))*(Product fr1)*(-b) are_congruent_mod m by A13,INT_1:39; then Product f,((-1)|^(len f1))*(-1)*((Product fr1)*b) are_congruent_mod m by A7,RVSUM_1:126; then Product f,((-1)|^(len f1 + 1))*((Product fr1)*b) are_congruent_mod m by NEWTON:11; hence thesis by A6,A8,A9,RVSUM_1:126; end; hence thesis; end; for n be Element of NAT holds P[n] from NAT_1:sch 1(A1,A4); hence thesis; end; reserve fp for FinSequence of NAT; theorem Th34: p>2 & (for d st d in dom fp holds fp.d hcf p = 1) implies ex fr being FinSequence of INT st len fr = len fp & (for d st d in dom fr holds fr.d = Lege (fp.d,p)) & Lege (Product fp,p) = Product fr proof assume A1:p>2; assume A2: for d st d in dom fp holds fp.d hcf p = 1; then A3: for d being Element of NAT st d in dom fp holds fp.d hcf p = 1; p in NAT by ORDINAL1:def 13; then Product(fp) hcf p = 1 by A3,WSIERP_1:43; then Product(fp) gcd p = 1 by Lm1;then A4:Lege (Product fp,p),(Product fp)|^((p-'1) div 2) are_congruent_mod p by A1,Th28; set k = (p-'1) div 2; set f = fp|^k; reconsider f as FinSequence of INT by FINSEQ_2:27,NUMBERS:17; deffunc F(Nat) = Lege (fp.$1,p); consider fr being FinSequence such that A5:len fr = len fp & (for d being Element of NAT st d in dom fr holds fr.d = F(d)) from FINSEQ_5:sch 1; for d being Nat st d in dom fr holds fr.d in INT proof let d be Nat; assume d in dom fr; then fr.d = Lege (fp.d,p) by A5; hence thesis by INT_1:def 2; end; then reconsider fr as FinSequence of INT by FINSEQ_2:14; A6:len f = len fp by NAT_3:def 1; for d st d in dom fr holds fr.d,f.d are_congruent_mod p proof let d;assume A7:d in dom fr; then d in dom fp by A5,FINSEQ_3:31; then fp.d hcf p = 1 by A2; then fp.d gcd p = 1 by Lm1; then Lege (fp.d,p),(fp.d)|^k are_congruent_mod p by A1,Th28; then A8:fr.d,(fp.d)|^k are_congruent_mod p by A5,A7; d in dom f by A5,A6,A7,FINSEQ_3:31; hence thesis by A8,NAT_3:def 1; end; then Product fr,Product f are_congruent_mod p by A5,A6,Th32; then A9:Product f,Product fr are_congruent_mod p by INT_1:35; fp is FinSequence of REAL by FINSEQ_2:27; then Lege (Product fp,p),Product f are_congruent_mod p by A4,NAT_3:15; then Lege (Product fp,p),Product fr are_congruent_mod p by A9,INT_1:36; then A10:p divides (Lege (Product fp,p) - Product fr) by INT_2:19; take fr; A11: for d st d in dom fr holds fr.d = 1 or fr.d = -1 proof let d;assume d in dom fr; then fr.d = Lege (fp.d,p) by A5; hence thesis by Th25; end; per cases by Th25; suppose A12:Lege (Product fp,p) = 1; Product fr <> -1 by A1,A10,A12,NAT_D:7; hence thesis by A5,A11,A12,Th31; end; suppose A13:Lege (Product fp,p) = -1; now assume Product fr = 1; then p divides -2 by A10,A13; then p divides 2 by INT_2:14; hence contradiction by A1,NAT_D:7; end; hence thesis by A5,A11,A13,Th31; end; end; theorem p > 2 & d hcf p = 1 & e hcf p = 1 implies Lege((d^2)*e,p) = Lege(e,p) proof assume A1:p > 2 & d hcf p = 1 & e hcf p = 1; then d gcd p = 1 by Lm1; then A2:Lege(d^2,p) = 1 by Th26; reconsider d2=d^2, e as Element of NAT by ORDINAL1:def 13; set fp = <*d2,e*>; reconsider p as prime Element of NAT by ORDINAL1:def 13; reconsider fp as FinSequence of NAT by FINSEQ_2:15; for k st k in dom fp holds fp.k hcf p = 1 proof let k; assume k in dom fp; then k in Seg(len fp) by FINSEQ_1:def 3; then A3:k in Seg 2 by FINSEQ_1:61; A4: d in NAT by ORDINAL1:def 13; per cases by A3,FINSEQ_1:4,TARSKI:def 2; suppose k = 1; then fp.k = d^2 by FINSEQ_1:61; hence thesis by A1,A4,WSIERP_1:12; end; suppose k = 2; hence thesis by A1,FINSEQ_1:61; end; end; then consider fr be FinSequence of INT such that A5: len fr = len fp & (for k be Nat st k in dom fr holds fr.k = Lege (fp.k,p)) & Lege (Product fp,p) = Product fr by A1,Th34; A6: len fr = 2 by A5,FINSEQ_1:61; then 1 in dom fr & 2 in dom fr by FINSEQ_3:27; then fr.1 = Lege(fp.1,p) & fr.2 = Lege(fp.2,p) by A5; then fr.1 = Lege(d^2,p) & fr.2 = Lege(e,p) by FINSEQ_1:61; then fr = <*1,Lege(e,p)*> by A2,A6,FINSEQ_1:61; then Product fr = 1 * Lege(e,p) by RVSUM_1:129; hence thesis by A5,RVSUM_1:129; end; theorem Th36: p>2 implies Lege (-1,p) = (-1)|^((p-'1) div 2) proof assume A1:p>2; (-1) gcd p = abs((-1)|^1) hcf abs(p) by NEWTON:10 .= 1 hcf abs(p) by SERIES_2:1 .= 1 by NEWTON:64; then A2:Lege (-1,p),(-1)|^((p-'1) div 2) are_congruent_mod p by A1,Th28; abs((-1)|^((p-'1) div 2)) = 1 by SERIES_2:1; then A3:(-1)|^((p-'1) div 2) =1 or -(-1)|^((p-'1) div 2) =1 by ABSVALUE:1; per cases by A3; suppose A4:(-1)|^((p-'1) div 2) =1; then A5:p divides (Lege (-1,p) - 1) by A2,INT_2:19; now assume Lege(-1,p) = -1; then p divides -2 by A5; then p divides 2 by INT_2:14; hence contradiction by A1,NAT_D:7; end; hence thesis by A4,Th25; end; suppose A6:(-1)|^((p-'1) div 2) = -1; then A7:p divides (Lege (-1,p) - (-1)) by A2,INT_2:19; Lege(-1,p) <> 1 by A1,A7,NAT_D:7; hence thesis by A6,Th25; end; end; theorem p>2 & p mod 4 = 1 implies (-1) is_quadratic_residue_mod p proof assume A1:p>2 & p mod 4 = 1; then A2:p = (p div 4)*4 + 1 by NAT_D:2; p>1 by INT_2:def 5; then p-'1 = p-1 by BINARITH:50; then p-'1 = 2*(2*(p div 4)) by A2; then (-1)|^((p-'1) div 2) = (-1)|^(2*(p div 4)) by NAT_D:18 .= ((-1)|^2)|^(p div 4) by NEWTON:14 .= (1|^2)|^(p div 4) by WSIERP_1:2 .= 1|^(p div 4) by NEWTON:100,SQUARE_1:59 .= 1 by NEWTON:15; then Lege(-1,p) = 1 by A1,Th36; hence thesis by Def3; end; theorem p>2 & p mod 4 = 3 implies not (-1) is_quadratic_residue_mod p proof assume A1:p>2 & p mod 4 = 3; then A2:p = (p div 4)*4 + 3 by NAT_D:2; p>1 by INT_2:def 5; then p-'1 = p-1 by BINARITH:50; then p-'1 = 2*(2*(p div 4) + 1) by A2; then (-1)|^((p-'1) div 2) = (-1)|^(2*(p div 4) + 1) by NAT_D:18 .= (-1)|^(2*(p div 4)) * (-1) by NEWTON:11 .= ((-1)|^2)|^(p div 4) *(-1) by NEWTON:14 .= (1|^2)|^(p div 4) *(-1) by WSIERP_1:2 .= 1|^(p div 4) *(-1) by NEWTON:100,SQUARE_1:59 .= 1 *(-1) by NEWTON:15; then Lege(-1,p) = -1 by A1,Th36; hence thesis by Def3; end; :: begin :: Gauss Lemma and Law of Quadratic Reciprocity theorem Th39:for D being non empty set,f being FinSequence of D, i,j being Nat holds f is one-to-one iff Swap(f,i,j) is one-to-one proof let D be non empty set,f be FinSequence of D,i,j be Nat; thus f is one-to-one implies Swap(f,i,j) is one-to-one proof assume f is one-to-one; then A1:card(rng f) = len f by FINSEQ_4:77; set ff = Swap(f,i,j); len ff = len f & rng ff = rng f by FINSEQ_7:20,24; hence thesis by A1,FINSEQ_4:77; end; assume Swap(f,i,j) is one-to-one; then card(rng Swap(f,i,j)) = len Swap(f,i,j) by FINSEQ_4:77; then card(rng f) = len Swap(f,i,j) by FINSEQ_7:24; then card(rng f) = len f by FINSEQ_7:20; hence thesis by FINSEQ_4:77; end; theorem Th40: for f being FinSequence of NAT st len f = n & (for d st d in dom f holds f.d>0 & f.d<=n) & f is one-to-one holds rng f = Seg n proof defpred P[Nat] means for f being FinSequence of NAT st len f = $1 & (for d st d in dom f holds f.d>0 & f.d<=$1) & f is one-to-one holds rng f = Seg $1; A1:P[0] proof let f be FinSequence of NAT; assume len f = 0; then f = {} by FINSEQ_1:25; hence thesis by FINSEQ_1:4,27; end; A2:for n be Element of NAT st P[n] holds P[n+1] proof let n be Element of NAT; assume A3:P[n]; P[n+1] proof let f be FinSequence of NAT; assume A4:len f = n+1 & (for d st d in dom f holds f.d>0 & f.d<=n+1) & f is one-to-one; then A5:f <> {} by FINSEQ_1:25;then consider f1 being FinSequence of NAT,a being Element of NAT such that A6: f = f1^<*a*> by HILBERT2:4; A7: len f = len f1 + 1 by A6,FINSEQ_2:19; A8: f1 is one-to-one & rng f1 misses rng <*a*> by A4,A6,FINSEQ_3:98; A9: n+1 in dom f by A4,A5,FINSEQ_5:6; then f.(n+1) > 0 & f.(n+1) <= n+1 by A4; then A10:a>0 & a<=n+1 by A4,A6,A7,FINSEQ_1:59; per cases by A10,REAL_1:def 5; suppose A11:a = n+1; for d st d in dom f1 holds f1.d>0 & f1.d<=n proof let d; assume A12:d in dom f1; then A13:d in dom f by A6,FINSEQ_2:18; then A14:f.d>0 & f.d<=n+1 by A4; then A15:f1.d>0 & f1.d<=n+1 by A6,A12,FINSEQ_1:def 7; now assume A16:f1.d = n+1; A17: d <= n by A4,A7,A12,FINSEQ_3:27; d < n+1 by A17,XREAL_1:147; then f.d <> f.(n+1) by A4,A9,A13,FUNCT_1:def 8; then f1.d <> f.(n+1) by A6,A12,FINSEQ_1:def 7; hence contradiction by A4,A6,A7,A11,A16,FINSEQ_1:59; end; then f1.d < n+1 by A15,REAL_1:def 5; hence thesis by A6,A12,A14,FINSEQ_1:def 7,NAT_1:13; end; then rng f1 = Seg n by A3,A4,A7,A8; then rng f1 \/ {a} = Seg (n+1) by A11,FINSEQ_1:11; then rng f1 \/ rng <*a*> = Seg (n+1) by FINSEQ_1:55; hence thesis by A6,FINSEQ_1:44; end; suppose A18:a > 0 & a < n+1; ex d st d in dom f1 & f1.d = n+1 proof assume A19:for d st d in dom f1 holds f1.d <> n+1; for d being Nat st d in dom f holds f.d in Seg n proof let d be Nat; assume A20:d in dom f; then d in Seg(n+1) by A4,FINSEQ_1:def 3; then A21:d>=1 & d<=n+1 by FINSEQ_1:3; per cases by A21,REAL_1:def 5; suppose d=n+1; then f.d = a by A4,A6,A7,FINSEQ_1:59; then f.d>=0+1 & f.d<=n by A18,NAT_1:13; hence thesis by FINSEQ_1:3; end; suppose d>=1 & d=1 & d<=n by NAT_1:13; then d in Seg n by FINSEQ_1:3; then A22:d in dom f1 by A4,A7,FINSEQ_1:def 3; then f1.d <> n+1 by A19; then A23:f.d <> n+1 by A6,A22,FINSEQ_1:def 7; f.d>0 & f.d <=n+1 by A4,A20; 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 CARD_1:80; 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 A24: d1 in dom f1 & f1.d1 = n+1; set f2 = Swap(f,d1,n+1); A25: len f2 = n+1 by A4,FINSEQ_7:20; then A26:f2 <> {} by FINSEQ_1:25;then consider f3 being FinSequence of NAT,b being Element of NAT such that A27: f2 = f3^<*b*> by HILBERT2:4; A28: n+1 = len f3 +1 by A25,A27,FINSEQ_2:19; d1>=1 & d1<=n by A4,A7,A24,FINSEQ_3:27; then A29:1 <= d1 & d1 <= len f by A4,NAT_1:13; A30: 0+1 <= n+1 & n+1 <= len f by A4,XREAL_1:8; then f2/.(n+1) = f/.d1 by A29,FINSEQ_7:33; then f2/.(n+1) = f.d1 by A29,FINSEQ_4:24; then f2.(n+1) = f.d1 by A25,A30,FINSEQ_4:24; then A31:f2.(n+1) = n+1 by A6,A24,FINSEQ_1:def 7; A32:f2 is one-to-one by A4,Th39;then A33:f3 is one-to-one by A27,FINSEQ_3:98; A34:b = n+1 by A27,A28,A31,FINSEQ_1:59; for d st d in dom f3 holds f3.d>0 & f3.d<=n proof let d; assume A35:d in dom f3; then A36:d in dom f2 by A27,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 A37: e in dom f & f2.d = f.e by FINSEQ_2:11; f2.d >0 & f2.d<=n+1 by A4,A37; then A38:f3.d>0 & f3.d<=n+1 by A27,A35,FINSEQ_1:def 7; now assume f3.d=n+1; then A39:f2.d = n+1 by A27,A35,FINSEQ_1:def 7; d<=n by A28,A35,FINSEQ_3:27;then A40: d < n+1 by XREAL_1:147; n+1 in dom f2 by A25,A26,FINSEQ_5:6; hence contradiction by A31,A32,A36,A39,A40,FUNCT_1:def 8; end; then f3.d>0 & f3.d by A27,FINSEQ_1:44 .= Seg n \/ {n+1} by A34,A41,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; A1: a in NAT by ORDINAL1:def 13; assume A2: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 A3:a gcd p = 1 by Lm1; then Lege(a,p),a|^((p-'1) div 2) are_congruent_mod p by A2,Th28; then A4:a|^((p-'1) div 2),Lege(a,p) are_congruent_mod p by INT_1:35; A5: p in NAT by ORDINAL1:def 13; 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}; A6: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 A2,SEQ_1:def 6; then A7:len f = len I by FINSEQ_3:31 .= p' by FINSEQ_2:55; (Product f1) mod p = (Product f) mod p by A5,EULER_2:26; then A8: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 A9:Product f = (Product (p'|->a))*(Product I) by A2,RVSUM_1:138 .= (a|^p') * (Product I) by NEWTON:def 1; A10:p>1 by INT_2:def 5; then A11:p-'1 = p-1 by BINARITH:50; p >= 2+1 by A2,NAT_1:13; then p-1 >= 3-1 by XREAL_1:11; then A12:p' >= 1 by A11,NAT_2:15; p is odd by A2,PEPIN:17; then A13:p-'1 is even by A11,HILBERT3:2; then 2 divides (p-'1) by PEPIN:22; then A14:p-'1 = 2*p' by NAT_D:3; then A15:p' divides (p-'1) by NAT_D:def 3; p-'1>0 by A10,A11,XREAL_1:52; then A16:p' <= (p-'1) by A15,NAT_D:7; A17:p-1

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

0 & f1.d <= p' proof let d;assume A54:d in dom f1; reconsider d as Element of NAT by ORDINAL1:def 13; f1.d in rng f1 & not f1.d in X by A53,A54,FUNCT_1:12; then A55:f1.d <= p/2; A56: f1.d in rng f1 by A54,FUNCT_1:12; then f1.d in {0} \/ rng f1 by XBOOLE_0:def 2; then not f1.d in {0} by A32,A56,XBOOLE_0:5; then f1.d <> 0 by TARSKI:def 1; hence thesis by A19,A55,INT_1:81; end; then rng f1 = rng I by A6,A7,A26,A49,Th40; then f1,I are_fiberwise_equipotent by A49,RFINSEQ:39; then Product f1 = Product I by EULER_2:25; then p divides (1 * Product I - a|^p' * Product I) by A8,A9,INT_2:19; then p divides (1 - a|^p')*Product I; then p divides (1 - a|^p') by A22,WSIERP_1:36; then 1,a|^p' are_congruent_mod p by INT_2:19; then A57:1,Lege(a,p) are_congruent_mod p by A4,INT_1:36; now assume Lege(a,p) = -1; then p divides (1-(-1)) by A57,INT_2:19; hence contradiction by A2,NAT_D:7; end; then Lege(a,p) = 1 by Th25; hence thesis by A2,A53,CARD_1:78,NEWTON:9; end; suppose A58:X is non empty; A59: f2 = (Sgm Y)^(Sgm X) proof for k,l being Element of NAT st k in Y & l in X holds k < l proof let k,l be Element of NAT; assume A60:k in Y & l in X; then k in rng f1 & not k in X by XBOOLE_0:def 4; then A61:k <= p/2; ex l1 being Element of NAT st l1 = l & l1 in rng f1 & l1>p/2 by A60; hence thesis by A61,XXREAL_0:2; end; then Sgm (Y\/X) = (Sgm Y)^(Sgm X) by A52,FINSEQ_3:48; then Sgm (rng f1 \/ X) = (Sgm Y)^(Sgm X) by XBOOLE_1:39; hence thesis by A36,XBOOLE_1:12; end; A62: len Sgm Y = n proof Y c= Seg n1 by A33,A38,XBOOLE_1:1; then len Sgm Y = card Y by FINSEQ_3:44 .= p' - m by A2,A7,A26,A36,A48,CARD_2:63; hence thesis; end; then A63:f2/^n = Sgm X by A59,FINSEQ_5:40; f2 = (f2|n)^(f2/^n) by RFINSEQ:21; then A64:f2|n is one-to-one & f2/^n is one-to-one by A50,FINSEQ_3:98; Sgm Y c= f2 by A59,FINSEQ_6:12; then A65:f2|n = Sgm Y by A62,FINSEQ_3:122; A66:m <> 0 by A2,A58,CARD_4:17; A67:len f2 = p' by A7,A26,A33,A48,FINSEQ_3:44; then A68:n <= len f2 by XREAL_1:45; then A69:len(f2|n) = n by FINSEQ_1:80; set f3 = (len (f2/^n) |-> p) - (f2/^n); set f4 = (f2|n) ^ f3; A70:dom f3 = dom(len (f2/^n) |-> p)/\dom(f2/^n) by SEQ_1:def 4 .= (Seg len (len(f2/^n) |-> p))/\dom(f2/^n) by FINSEQ_1:def 3 .= (Seg len(f2/^n))/\dom(f2/^n) by FINSEQ_2:69 .= dom(f2/^n) /\ dom(f2/^n) by FINSEQ_1:def 3 .= dom(f2/^n); then A71:len f3 = len(f2/^n) by FINSEQ_3:31; A72:len(f2/^n) = (len f2 -' n) by BINARITH:76 .= len f2 - n by A68,BINARITH:50 .= m by A67; A73:for d st d in dom f3 holds f3.d = p - (f2/^n).d proof let d; assume A74:d in dom f3; then A75: d in Seg len(f2/^n) by A70,A74,FINSEQ_1:def 3; p in NAT by ORDINAL1:def 13; then (len (f2/^n) |-> p).d = p by A66,A72,A75,FINSEQ_2:71; hence thesis by A74,SEQ_1:def 4; end; A76:for d st d in dom f3 holds f3.d > 0 & f3.d <= p' proof let d; assume A77:d in dom f3; then A78:f3.d = p - (f2/^n).d by A73; then reconsider w = f3.d as Element of INT by INT_1:def 2; (Sgm X).d in rng Sgm X by A63,A70,A77,FUNCT_1:12; then (Sgm X).d in X by A52,FINSEQ_1:def 13; then consider ll be Element of NAT such that A79: ll = (Sgm X).d & ll in rng f1 & ll > p/2; A80: w < p - p/2 by A63,A78,A79,XREAL_1:12; consider e being Nat such that A81:e in dom f1 & f1.e = (f2/^n).d by A63,A79,FINSEQ_2:11; (f2/^n).d = f.e mod p by A27,A81,EULER_2:def 1; then (f2/^n).d < p by NAT_D:1; hence thesis by A19,A78,A80,INT_1:81,XREAL_1:52; end; for d being Nat st d in dom f3 holds f3.d in NAT proof let d be Nat; assume d in dom f3; then f3.d = p - (f2/^n).d & f3.d > 0 by A73,A76; hence thesis by INT_1:16; end; then reconsider f3 as FinSequence of NAT by FINSEQ_2:14; for d,e being Element of NAT st 1<=d & d f3.e proof let d,e be Element of NAT;assume A82:1<=d & d= 1 & d1 <= p' & e1 >= 1 & e1 <= p' by A7,A26,A87,A91,FINSEQ_3:27; then d1+e1 >= 1+1 & d1+e1 <= p'+p' by XREAL_1:9; then d1+e1>0 & d1+e1 < p by A11,A14,A17,XXREAL_0:2; hence contradiction by A93,NAT_D:7; end; then A94:f4 is one-to-one by A64,A84,FINSEQ_3:98; for d st d in dom f4 holds f4.d>0 & f4.d <= p' proof let d;assume A95:d in dom f4; per cases by A95,FINSEQ_1:38; suppose A96:d in dom(f2|n); reconsider d as Element of NAT by ORDINAL1:def 13; (f2|n).d in rng Sgm Y by A65,A96,FUNCT_1:12; then (f2|n).d in Y by A52,FINSEQ_1:def 13;then A97: (f2|n).d in rng f1 & not (f2|n).d in X by XBOOLE_0:def 4; then (f2|n).d <= p/2; then A98:(f2|n).d <= p' by A19,INT_1:81; not (f2|n).d in {0} by A32,A97,XBOOLE_0:3; then (f2|n).d <> 0 by TARSKI:def 1; then (f2|n).d > 0; hence thesis by A96,A98,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 A99: l in dom f3 & d = len(f2|n)+ l by ORDINAL1:def 13; f4.d = f3.l by A99,FINSEQ_1:def 7; hence thesis by A76,A99; end; end; then rng f4 = rng I by A6,A7,A85,A94,Th40; then f4, I are_fiberwise_equipotent by A94,RFINSEQ:39; then Product f4 = Product I by EULER_2:25; then A100:(Product(f2|n)) * (Product f3) = Product I by RVSUM_1:127; A101: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 A73 .= (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 A71,A72,A101,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 A100,RVSUM_1:127; then A102:Product I,(-1)|^m * Product f1 are_congruent_mod p by A51,RFINSEQ:21; (-1)|^m * Product f1,(-1)|^m * Product f are_congruent_mod p by A8,INT_4:11; then Product I,(-1)|^m * (a|^p') * (Product I) are_congruent_mod p by A9,A102,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 A22,WSIERP_1:36; then p divides (-1)|^m * (1-((-1)|^m * (a|^p'))) by INT_2:12; then A103: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 A103,INT_2:19; then A104:(-1)|^m,Lege(a,p) are_congruent_mod p by A4,INT_1:36; abs ((-1)|^m) = 1 by SERIES_2:1; then A105:(-1)|^m = 1 or -((-1)|^m) = 1 by ABSVALUE:1; per cases by A105; suppose A106:(-1)|^m = 1; now assume Lege(a,p) = -1; then p divides (1-(-1)) by A104,A106,INT_2:19; hence contradiction by A2,NAT_D:7; end; hence thesis by A106,Th25; end; suppose A107:(-1)|^m = -1; now assume Lege(a,p) = 1; then p divides (-1-1) by A104,A107,INT_2:19; then p divides (-2); then p divides 2 by INT_2:14; hence contradiction by A2,NAT_D:7; end; hence thesis by A107,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 6; 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-'1 < p by NAT_2:11; A8: p' = ((p-'1)+1) div 2 by A3,A5,NAT_2:28 .= p div 2 by A4,BINARITH:53; A9: 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 A10:p div (2*2) <= p div 2 by NAT_2:29; A11: for d st d in dom fp holds fp.d = 2*d proof let d; assume A12:d in dom fp; then d in dom I by SEQ_1:def 6; then d in Seg len I by FINSEQ_1:def 3; then A13:d is Element of Seg p' by FINSEQ_2:55; thus fp.d = 2 * I.d by A12,SEQ_1:def 6 .= 2 * d by A8,A9,A13,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 A11; hence thesis by ORDINAL1:def 13; end; then reconsider fp as FinSequence of NAT by FINSEQ_2:14; dom fp = dom I by SEQ_1:def 6;then A14: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 A15: x = k & k in dom f & f.k > p/2; thus thesis by A15; end; then Y c= dom f by TARSKI:def 3; then reconsider Y as finite Subset of NAT by FINSET_1:13,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 A16: x = k & k in rng f & k > p/2; thus thesis by A16; end; then A17:X c= rng f by TARSKI:def 3; then reconsider X as finite set by FINSET_1:13; card X is Element of NAT; then reconsider m as Element of NAT; A18: 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 A17,XBOOLE_1:1; A19:len f = len fp by EULER_2:def 1;then A20:dom f = dom fp by FINSEQ_3:31; A21: for d st d in dom f holds f.d = 2*d proof let d; assume A22:d in dom f; then d<= p' by A14,A19,FINSEQ_3:27; then 2*d<=(p-'1) by A6,XREAL_1:66; then 2*d

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

-p by A28,XREAL_1:26; then d-e > -p by A27,XXREAL_0:2; hence contradiction by A26,A29,SEQ_2:9; end; hence thesis; end; deffunc F(Nat) = f1.$1 div p; consider f2 be FinSequence such that A30:len f2 = p' & for d being Element of NAT st d in dom f2 holds f2.d = F(d) from FINSEQ_5:sch 1; for d being Nat st d in dom f2 holds f2.d in NAT proof let d be Nat;assume d in dom f2; then f2.d = f1.d div p by A30; hence thesis; end; then reconsider f2 as FinSequence of NAT by FINSEQ_2:14; set f3 = f1 mod p; A31:len f3 = len f1 by EULER_2:def 1; then A32:dom f1 = dom f3 by FINSEQ_3:31; A33: dom f1 = dom f2 by A6,A30,FINSEQ_3:31; A34: dom (p*f2+f3) = dom (p*f2) /\ dom f3 by SEQ_1:def 3 .= dom f2 /\ dom f3 by SEQ_1:def 6 .= dom f1 by A32,A33; A35: for d st d in dom f1 holds f1.d = f2.d * p + f3.d proof let d; assume d in dom f1; then f2.d = f1.d div p & f3.d = f1.d mod p by A30,A33,EULER_2:def 1; hence f1.d = f2.d * p + f3.d by NAT_D:2; end; for d being Nat st d in dom f1 holds f1.d = (p*f2+f3).d proof let d be Nat; assume A36:d in dom f1; then A37:(p*f2+f3).d = (p*f2).d + f3.d by A34,SEQ_1:def 3; d in dom (p*f2) by A33,A36,SEQ_1:def 6; hence (p*f2+f3).d = p * f2.d + f3.d by A37,SEQ_1:def 6 .= f1.d by A35,A36; end; then A38:f1 = p*f2 + f3 by A34,FINSEQ_1:17; A39: p*f2 is Element of NAT* & f3 is Element of NAT* by FINSEQ_1:def 11; dom(p*f2) = dom f2 by SEQ_1:def 6; then len(p*f2) = p' & len f3 = p' by A5,A30,A31,FINSEQ_2:55,FINSEQ_3:31; then p*f2 in p'-tuples_on NAT & f3 in p'-tuples_on NAT by A39; then p*f2 is Element of p'-tuples_on REAL & f3 is Element of p'-tuples_on REAL by FINSEQ_2:129; then A40:Sum f1 = Sum(p*f2) + Sum f3 by A38,RVSUM_1:119 .= p*(Sum f2) + Sum f3 by RVSUM_1:117; then A41:q*(Sum idseq p') = p*(Sum f2) + Sum f3 by RVSUM_1:117; f3 <> {} by A6,A9,A31,FINSEQ_1:28;then rng f3 is finite non empty Subset of NAT by FINSEQ_1:27,def 4; then consider n1 be Element of NAT such that A42: rng f3 c= Seg n1 \/ {0} by HEYTING3:3; not 0 in rng f3 proof assume 0 in rng f3; then consider a be Nat such that A43: a in dom f3 & f3.a = 0 by FINSEQ_2:11; f1.a = f2.a * p + 0 by A32,A35,A43; then q*a = f2.a *p by A19,A32,A43; then p divides q*a by NAT_D:def 3; then A44:p divides a by A2,PEPIN:3; A45: a >= 1 & a <= p' by A6,A31,A43,FINSEQ_3:27; then p <= a by A44,NAT_D:7; hence contradiction by A16,A45,XXREAL_0:2; end; then A46:{0} misses rng f3 by ZFMISC_1:56; then A47:rng f3 c= Seg n1 by A42,XBOOLE_1:73; for x,y be set st x in dom f3 & y in dom f3 & f3.x=f3.y holds x=y proof let x,y be set; assume A48:x in dom f3 & y in dom f3 & f3.x=f3.y; then reconsider x,y as Element of NAT; f1.x = f2.x * p + f3.x & f1.y = f2.y * p + f3.y by A32,A35,A48; then f1.x - f1.y = (f2.x - f2.y) * p by A48; then p divides (f1.x - f1.y) by INT_1:def 9; hence thesis by A22,A32,A48; end; then A49:f3 is one-to-one by FUNCT_1:def 8; set f4 = Sgm rng f3; set X = {k where k is Element of NAT:k in rng f4 & k>p/2}; A50: rng f4 = rng f3 by A47,FINSEQ_1:def 13; A51: f4 is one-to-one by A47,FINSEQ_3:99; then A52:f4,f3 are_fiberwise_equipotent by A49,A50,RFINSEQ:39; f4 is FinSequence of REAL & f3 is FinSequence of REAL by FINSEQ_2:27; then A53:Sum f4 = Sum f3 by A52,RFINSEQ:22; for x being set st x in X holds x in rng f4 proof let x be set; assume x in X; then consider k being Element of NAT such that A54: x = k & k in rng f4 & k > p/2; thus thesis by A54; end; then A55:X c= rng f4 by TARSKI:def 3; then reconsider X as finite Subset of NAT by FINSET_1:13,XBOOLE_1:1; A56:X c= Seg n1 by A47,A50,A55,XBOOLE_1:1; reconsider Y = rng f4 \ X as finite Subset of NAT; rng f4 \ X c= rng f4 by XBOOLE_1:36;then A57:Y c= Seg n1 by A47,A50,XBOOLE_1:1; set m = card X; A58:len f3 = card rng f4 by A49,A50,FINSEQ_4:77; then m <= len f3 by A55,CARD_1:80; then reconsider n = p' - m as Element of NAT by A6,A31,NAT_1:21; len f3 = card rng f3 by A49,FINSEQ_4:77;then A59:len f4 = p' by A6,A31,A47,FINSEQ_3:44; A60:f4 = (Sgm Y)^(Sgm X) proof for k,l being Element of NAT st k in Y & l in X holds k < l proof let k,l be Element of NAT; assume A61:k in Y & l in X; then k in rng f4 & not k in X by XBOOLE_0:def 4; then A62:k <= p/2; ex l1 being Element of NAT st l1 = l & l1 in rng f4 & l1>p/2 by A61; hence thesis by A62,XXREAL_0:2; end; then Sgm (Y\/X) = (Sgm Y)^(Sgm X) by A56,A57,FINSEQ_3:48; then Sgm (rng f4 \/ X) = (Sgm Y)^(Sgm X) by XBOOLE_1:39; hence thesis by A50,A55,XBOOLE_1:12; end; Sum f4 = Sum(Sgm Y) + Sum(Sgm X) by A60,RVSUM_1:105; then A63:q*(Sum idseq p')=p*(Sum f2)+Sum(Sgm Y) + Sum(Sgm X) by A40,A53,RVSUM_1:117; A64: len Sgm Y = n proof len Sgm Y = card Y by A57,FINSEQ_3:44 .= p' - m by A6,A31,A55,A58,CARD_2:63; hence thesis; end; then A65:f4/^n = Sgm X by A60,FINSEQ_5:40; f4 = (f4|n)^(f4/^n) by RFINSEQ:21;then A66:f4|n is one-to-one & f4/^n is one-to-one by A51,FINSEQ_3:98; Sgm Y c= f4 by A60,FINSEQ_6:12; then A67:f4|n = Sgm Y by A64,FINSEQ_3:122; for d being Nat st d in dom idseq p' holds (idseq p').d in NAT proof let d be Nat; assume d in dom idseq p'; then A68: d in Seg len idseq p' by FINSEQ_1:def 3; then d is Element of Seg p' by FINSEQ_2:55; then (idseq p').d = d by A9,FINSEQ_2:57; hence thesis by A68; end; then idseq p' is FinSequence of NAT by FINSEQ_2:14; then reconsider M = Sum idseq p' as Element of NAT by Lm4; A69: Lege(q,p) = (-1)|^(Sum f2) proof per cases; suppose A70:X is empty; for d st d in dom f4 holds f4.d > 0 & f4.d <= p' proof let d; assume A71:d in dom f4; A72: not f4.d in X by A70; f4.d in rng f4 by A71,FUNCT_1:12;then A73: f4.d <= p/2 by A72; A74: f4.d in rng f3 by A50,A71,FUNCT_1:12; then f4.d in (rng f3)\/{0} by XBOOLE_0:def 2; then not f4.d in {0} by A46,A74,XBOOLE_0:5; then f4.d <> 0 by TARSKI:def 1; hence thesis by A17,A73,INT_1:81; end; then Sgm rng f3 = Sgm(Seg p') by A50,A51,A59,Th40; then q*(Sum idseq p') = p*(Sum f2) + Sum idseq p' by A41,A53,FINSEQ_3:54; then A75:q*(Sum idseq p') - Sum idseq p' = p*(Sum f2); 2 divides (q-'1)*M by A11,NAT_D:9; then 2 divides ((Sum f2)-0) by A4,A8,A75,PEPIN:3; then Sum f2,0 are_congruent_mod 2 by INT_2:19; then (Sum f2) mod 2 = 0 mod 2 by INT_3:12; then (-1)|^m = (-1)|^(Sum f2) by A70,Th45,CARD_1:78; hence thesis by A1,A3,A50,Th41; end; suppose X is non empty; then A76:m <> 0 by CARD_4:17; A77: n <= len f4 by A59,XREAL_1:45;then A78: len(f4|n) = n by FINSEQ_1:80; A79: len(f4/^n) = (len f4 -' n) by BINARITH:76 .= len f4 - n by A77,BINARITH:50 .= m by A59; set f5 = (m|->p)-(f4/^n); set f6 = (f4|n)^f5; A80:dom f5 = dom(m |-> p) /\ dom(f4/^n) by SEQ_1:def 4 .= (Seg len (m |-> p)) /\ dom(f4/^n) by FINSEQ_1:def 3 .= (Seg len(f4/^n))/\dom(f4/^n) by A79,FINSEQ_2:69 .= dom(f4/^n) /\ dom(f4/^n) by FINSEQ_1:def 3 .= dom(f4/^n); then A81:len f5 = len(f4/^n) by FINSEQ_3:31; A82:for d st d in dom f5 holds f5.d = p - (f4/^n).d proof let d; assume A83:d in dom f5; then d in Seg m by A79,A80,FINSEQ_1:def 3; then (m |-> p).d = p by A76,FINSEQ_2:71; hence thesis by A83,SEQ_1:def 4; end; A84:for d st d in dom f5 holds f5.d > 0 & f5.d <= p' proof let d; assume A85:d in dom f5; then A86:f5.d = p - (f4/^n).d by A82; then reconsider w = f5.d as Element of INT by INT_1:def 2; (Sgm X).d in rng Sgm X by A65,A80,A85,FUNCT_1:12; then (Sgm X).d in X by A56,FINSEQ_1:def 13; then consider ll be Element of NAT such that A87: ll = (Sgm X).d & ll in rng f3 & ll > p/2 by A50; A88: w < p - p/2 by A65,A86,A87,XREAL_1:12; consider e being Nat such that A89:e in dom f3 & f3.e = (f4/^n).d by A65,A87,FINSEQ_2:11; (f4/^n).d = f1.e mod p by A32,A89,EULER_2:def 1; then (f4/^n).d < p by NAT_D:1; hence thesis by A17,A86,A88,INT_1:81,XREAL_1:52; end; for d being Nat st d in dom f5 holds f5.d in NAT proof let d be Nat; assume d in dom f5; then f5.d = p - (f4/^n).d & f5.d > 0 by A82,A84; hence thesis by INT_1:16; end; then reconsider f5 as FinSequence of NAT by FINSEQ_2:14; for d,e being Element of NAT st 1<=d & d f5.e proof let d,e be Element of NAT;assume A90:1<=d & d= 1 & d1 <= p' & e1 >= 1 & e1 <= p' by A6,A31,A96,A100,FINSEQ_3:27; then d1+e1 >= 1+1 & d1+e1 <= p'+p' by XREAL_1:9; then d1+e1>0 & d1+e1 < p by A12,A15,XXREAL_0:2; hence contradiction by A101,NAT_D:7; end; then A102:f6 is one-to-one by A66,A92,FINSEQ_3:98; for d st d in dom f6 holds f6.d>0 & f6.d <= p' proof let d;assume A103:d in dom f6; per cases by A103,FINSEQ_1:38; suppose A104:d in dom(f4|n); then (f4|n).d in rng Sgm Y by A67,FUNCT_1:12; then (f4|n).d in Y by A57,FINSEQ_1:def 13;then A105: (f4|n).d in rng f4 & not (f4|n).d in X by XBOOLE_0:def 4; then (f4|n).d <= p/2; then A106:(f4|n).d <= p' by A17,INT_1:81; not (f4|n).d in {0} by A46,A50,A105,XBOOLE_0:3; then (f4|n).d <> 0 by TARSKI:def 1; then (f4|n).d > 0; hence thesis by A104,A106,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 A107: l in dom f5 & d = len(f4|n)+ l by ORDINAL1:def 13; f6.d = f5.l by A107,FINSEQ_1:def 7; hence thesis by A84,A107; end; end; then rng f6 = rng idseq p' by A93,A94,A102,Th40; then A108:f6,(idseq p') are_fiberwise_equipotent by A102,RFINSEQ:39; A109:f6 is FinSequence of REAL & f4/^n is FinSequence of REAL by FINSEQ_2:27; then M = Sum f6 by A108,RFINSEQ:22 .= Sum(f4|n) + Sum f5 by RVSUM_1:105 .= Sum(f4|n) + (m*p - Sum(f4/^n)) by A79,A109,Th47 .= Sum(f4|n) + m*p - Sum(f4/^n); then (q-1)*M = p*(Sum f2) + 2*Sum(Sgm X) - m*p by A63,A65,A67; then A110:(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 A111:2 divides (p*((Sum f2)-m)) by A110,Lm2; 2,(p qua Integer) are_relative_prime by A4,EULER_2:1; then 2 divides ((Sum f2) - m) by A111,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,A50,Th41; end; end; set g1 = p*idseq q'; dom g1 = dom idseq q' by SEQ_1:def 6;then len g1 = len idseq q' by FINSEQ_3:31;then A112: len g1 = q' by FINSEQ_2:55; A113: for d st d in dom g1 holds g1.d = p*d proof let d; assume A114:d in dom g1; then A115:g1.d = p * (idseq q').d by SEQ_1:def 6; d in dom idseq q' by A114,SEQ_1:def 6; 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,A115,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 A113; hence thesis by ORDINAL1:def 13; end; then reconsider g1 as FinSequence of NAT by FINSEQ_2:14; A116: 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 A117:d in dom g1 & e in dom g1 & q divides (g1.d-g1.e); then g1.d = p*d & g1.e = p*e by A113; then A118:q divides (d-e)*p by A117; q,(p qua Integer) are_relative_prime by A2,EULER_2:1; then A119:q divides (d - e) by A118,INT_2:40; now assume d <> e; then d-e <> 0; then abs(q) <= abs(d-e) by A119,INT_4:6; then A120:q <= abs(d-e) by ABSVALUE:def 1; d>=1 & d<=q' & e>=1 & e<=q' by A112,A117,FINSEQ_3:27; then A121:d-e<=q'-1 & d-e>=1-q' by XREAL_1:15; A122: q'-1 -q by A122,XREAL_1:26; then d-e > -q by A121,XXREAL_0:2; hence contradiction by A120,A123,SEQ_2:9; end; hence thesis; end; deffunc F(Nat) = g1.$1 div q; consider g2 be FinSequence such that A124:len g2 = q' & for d being Element of NAT st d in dom g2 holds g2.d = F(d) from FINSEQ_5:sch 1; for d being Nat st d in dom g2 holds g2.d in NAT proof let d be Nat;assume d in dom g2; then g2.d = g1.d div q by A124; hence thesis; end; then reconsider g2 as FinSequence of NAT by FINSEQ_2:14; set g3 = g1 mod q; A125: len g3 = len g1 by EULER_2:def 1;then A126: dom g1 = dom g3 by FINSEQ_3:31; A127: dom g1 = dom g2 by A112,A124,FINSEQ_3:31; A128: dom (q*g2+g3) = dom (q*g2) /\ dom g3 by SEQ_1:def 3 .= dom g2 /\ dom g3 by SEQ_1:def 6 .= dom g1 by A126,A127; A129: for d st d in dom g1 holds g1.d = g2.d * q + g3.d proof let d; assume d in dom g1; then g2.d = g1.d div q & g3.d = g1.d mod q by A124,A127,EULER_2:def 1; hence g1.d = g2.d * q + g3.d by NAT_D:2; end; for d being Nat st d in dom g1 holds g1.d = (q*g2+g3).d proof let d be Nat; assume A130:d in dom g1; then A131:(q*g2+g3).d = (q*g2).d + g3.d by A128,SEQ_1:def 3; d in dom (q*g2) by A127,A130,SEQ_1:def 6; hence (q*g2+g3).d = q * g2.d + g3.d by A131,SEQ_1:def 6 .= g1.d by A129,A130; end; then A132:g1 = q*g2 + g3 by A128,FINSEQ_1:17; A133: q*g2 is Element of NAT* & g3 is Element of NAT* by FINSEQ_1:def 11; dom(q*g2) = dom g2 by SEQ_1:def 6; then len(q*g2) = q' & len g3 = q' by A112,A124,EULER_2:def 1,FINSEQ_3:31; then A134:q*g2 in q'-tuples_on NAT & g3 in q'-tuples_on NAT by A133; q*g2 is Element of q'-tuples_on REAL & g3 is Element of q'-tuples_on REAL by A134,FINSEQ_2:129; then A135:Sum g1 = Sum(q*g2) + Sum g3 by A132,RVSUM_1:119 .= q*(Sum g2) + Sum g3 by RVSUM_1:117; len g3 >=1 by A9,A112,EULER_2:def 1; then g3 <> {} by FINSEQ_1:28; then rng g3 is finite non empty Subset of NAT by FINSEQ_1:27,def 4; then consider n2 be Element of NAT such that A136: rng g3 c= Seg n2 \/ {0} by HEYTING3:3; not 0 in rng g3 proof assume 0 in rng g3; then consider a be Nat such that A137: a in dom g3 & g3.a = 0 by FINSEQ_2:11; a in dom g1 by A125,A137,FINSEQ_3:31;then A138: g1.a = g2.a * q + 0 by A129,A137; a in dom g1 by A125,A137,FINSEQ_3:31; then p*a = g2.a * q by A113,A138; then q divides p*a by NAT_D:def 3; then A139:q divides a by A2,PEPIN:3; A140: a >= 1 & a <= q' by A112,A125,A137,FINSEQ_3:27; then q <= a by A139,NAT_D:7; hence contradiction by A16,A140,XXREAL_0:2; end; then A141:{0} misses rng g3 by ZFMISC_1:56; then A142:rng g3 c= Seg n2 by A136,XBOOLE_1:73; for x,y be set st x in dom g3 & y in dom g3 & g3.x=g3.y holds x=y proof let x,y be set; assume A143:x in dom g3 & y in dom g3 & g3.x=g3.y; then reconsider x,y as Element of NAT; g1.x = g2.x * q + g3.x & g1.y = g2.y * q + g3.y by A126,A129,A143; then g1.x - g1.y = (g2.x - g2.y) * q by A143; then q divides (g1.x - g1.y) by INT_1:def 9; hence thesis by A116,A126,A143; end; then A144:g3 is one-to-one by FUNCT_1:def 8; set g4 = Sgm rng g3; set XX = {k where k is Element of NAT:k in rng g4 & k>q/2}; A145: rng g4 = rng g3 by A142,FINSEQ_1:def 13; A146: g4 is one-to-one by A142,FINSEQ_3:99; then A147:g4,g3 are_fiberwise_equipotent by A144,A145,RFINSEQ:39; g4 is FinSequence of REAL & g3 is FinSequence of REAL by FINSEQ_2:27; then A148:Sum g4 = Sum g3 by A147,RFINSEQ:22; for x being set st x in XX holds x in rng g4 proof let x be set; assume x in XX; then consider k being Element of NAT such that A149: x = k & k in rng g4 & k > q/2; thus thesis by A149; end; then A150:XX c= rng g4 by TARSKI:def 3; then reconsider XX as finite Subset of NAT by FINSET_1:13,XBOOLE_1:1; reconsider YY = rng g4 \ XX as finite Subset of NAT; rng g4 \ XX c= rng g4 by XBOOLE_1:36;then A151:YY c= Seg n2 by A142,A145,XBOOLE_1:1; set mm = card XX; A152:len g3 = card rng g4 by A144,A145,FINSEQ_4:77; mm <= card rng g4 by A150,CARD_1:80; then mm <= q' by A112,A152,EULER_2:def 1; then reconsider nn = q' - mm as Element of NAT by NAT_1:21; len g3 = card rng g3 by A144,FINSEQ_4:77;then A153:len g4 = q' by A112,A125,A142,FINSEQ_3:44; A154:XX c= Seg n2 by A142,A145,A150,XBOOLE_1:1; A155:g4 = (Sgm YY)^(Sgm XX) proof per cases; suppose A156:YY is empty; then rng g4 c= XX by XBOOLE_1:37; then XX = rng g4 by A150,XBOOLE_0:def 10; hence g4 = (Sgm YY)^(Sgm XX) by A145,A156,FINSEQ_1:47,FINSEQ_3:49; end; suppose YY is non empty; for k,l being Element of NAT st k in YY & l in XX holds k < l proof let k,l be Element of NAT; assume A157:k in YY & l in XX; then k in rng g4 & not k in XX by XBOOLE_0:def 4; then A158:k <= q/2; ex l1 being Element of NAT st l1 = l & l1 in rng g4 & l1>q/2 by A157; hence thesis by A158,XXREAL_0:2; end; then Sgm (YY\/XX) = (Sgm YY)^(Sgm XX) by A151,A154,FINSEQ_3:48; then Sgm (rng g4 \/ XX) = (Sgm YY)^(Sgm XX) by XBOOLE_1:39; hence thesis by A145,A150,XBOOLE_1:12; end; end; Sum g4 = Sum(Sgm YY) + Sum(Sgm XX) by A155,RVSUM_1:105; then A159:p*(Sum idseq q')=q*(Sum g2)+Sum(Sgm YY)+Sum(Sgm XX) by A135,A148,RVSUM_1:117; A160: len Sgm YY = nn proof len Sgm YY = card YY by A151,FINSEQ_3:44 .= q' - mm by A112,A125,A150,A152,CARD_2:63; hence thesis; end; then A161:g4/^nn = Sgm XX by A155,FINSEQ_5:40; g4 = (g4|nn)^(g4/^nn) by RFINSEQ:21;then A162:g4|nn is one-to-one & g4/^nn is one-to-one by A146,FINSEQ_3:98; Sgm YY c= g4 by A155,FINSEQ_6:12; then A163:g4|nn = Sgm YY by A160,FINSEQ_3:122; for d being Nat st d in dom idseq q' holds (idseq q').d in NAT proof let d be Nat; assume d in dom idseq q'; then d in Seg len idseq q' by FINSEQ_1:def 3; then d is Element of Seg q' by FINSEQ_2:55; then (idseq q').d = d by A9,FINSEQ_2:57; hence thesis by ORDINAL1:def 13; end; then idseq q' is FinSequence of NAT by FINSEQ_2:14; then reconsider N = Sum idseq q' as Element of NAT by Lm4; A164: Lege(p,q) = (-1)|^(Sum g2) proof per cases; suppose A165:XX is empty; for d st d in dom g4 holds g4.d > 0 & g4.d <= q' proof let d; assume d in dom g4; then A166:g4.d in rng g4 by FUNCT_1:12; not g4.d in XX by A165; then A167:g4.d <= q/2 by A166; g4.d in (rng g3)\/{0} by A145,A166,XBOOLE_0:def 2; then not g4.d in {0} by A141,A145,A166,XBOOLE_0:5; then g4.d <> 0 by TARSKI:def 1; hence thesis by A18,A167,INT_1:81; end; then rng g3 = Seg q' by A145,A146,A153,Th40; then g4 = idseq q' by FINSEQ_3:54; then p*N = q*(Sum g2) + N by A135,A148,RVSUM_1:117; then p*N - N = q*(Sum g2); then A168:(p-'1)*N = q*(Sum g2) by A8; 2 divides q*(Sum g2) by A11,A168,NAT_D:9; then 2 divides ((Sum g2)-0) by A4,PEPIN:3; then Sum g2,0 are_congruent_mod 2 by INT_2:19; then (Sum g2) mod 2 = 0 mod 2 by INT_3:12; then (-1)|^mm = (-1)|^(Sum g2) by A165,Th45,CARD_1:78; hence thesis by A1,A3,A145,Th41; end; suppose XX is non empty; then A169:mm <> 0 by CARD_4:17; A170: nn <= len g4 by A153,XREAL_1:45;then A171: len(g4|nn) = nn by FINSEQ_1:80; A172: len(g4/^nn) = (len g4 -' nn) by BINARITH:76 .= len g4 - nn by A170,BINARITH:50 .= mm by A153; set g5 = (mm|->q)-(g4/^nn); set g6 = (g4|nn)^g5; A173:dom g5 = dom(mm |-> q) /\ dom(g4/^nn) by SEQ_1:def 4 .= (Seg len (mm |-> q)) /\ dom(g4/^nn) by FINSEQ_1:def 3 .= (Seg len(g4/^nn))/\dom(g4/^nn) by A172,FINSEQ_2:69 .= dom(g4/^nn) /\ dom(g4/^nn) by FINSEQ_1:def 3 .= dom(g4/^nn); then A174:len g5 = len(g4/^nn) by FINSEQ_3:31; A175:for d st d in dom g5 holds g5.d = q - (g4/^nn).d proof let d; assume A176:d in dom g5; then d in Seg mm by A172,A173,FINSEQ_1:def 3; then (mm |-> q).d = q by A169,FINSEQ_2:71; hence thesis by A176,SEQ_1:def 4; end; A177:for d st d in dom g5 holds g5.d > 0 & g5.d <= q' proof let d; assume A178:d in dom g5; then A179:g5.d = q - (g4/^nn).d by A175; then reconsider w = g5.d as Element of INT by INT_1:def 2; (Sgm XX).d in rng Sgm XX by A161,A173,A178,FUNCT_1:12; then (Sgm XX).d in XX by A154,FINSEQ_1:def 13; then consider ll be Element of NAT such that A180: ll = (Sgm XX).d & ll in rng g3 & ll > q/2 by A145; A181: w < q - q/2 by A161,A179,A180,XREAL_1:12; consider e being Nat such that A182:e in dom g3 & g3.e=(g4/^nn).d by A161,A180,FINSEQ_2:11; (g4/^nn).d = g1.e mod q by A126,A182,EULER_2:def 1; then (g4/^nn).d < q by NAT_D:1; hence thesis by A18,A179,A181,INT_1:81,XREAL_1:52; end; for d being Nat st d in dom g5 holds g5.d in NAT proof let d be Nat; assume d in dom g5; then g5.d = q - (g4/^nn).d & g5.d > 0 by A175,A177; hence thesis by INT_1:16; end; then reconsider g5 as FinSequence of NAT by FINSEQ_2:14; for d,e being Element of NAT st 1<=d & d g5.e proof let d,e be Element of NAT;assume A183:1<=d & d= 1 & d1 <= q' & e1 >= 1 & e1 <= q' by A112,A125,A189,A194, FINSEQ_3:27; then d1+e1 >= 1+1 & d1+e1 <= q'+q' by XREAL_1:9; then d1+e1>0 & d1+e1 < q by A12,A15,XXREAL_0:2; hence contradiction by A196,NAT_D:7; end; then A197:g6 is one-to-one by A162,A185,FINSEQ_3:98; for d st d in dom g6 holds g6.d>0 & g6.d <= q' proof let d;assume A198:d in dom g6; per cases by A198,FINSEQ_1:38; suppose A199:d in dom(g4|nn); then (g4|nn).d in rng Sgm YY by A163,FUNCT_1:12; then (g4|nn).d in YY by A151,FINSEQ_1:def 13;then A200: (g4|nn).d in rng g4 & not (g4|nn).d in XX by XBOOLE_0:def 4; then (g4|nn).d <= q/2; then A201:(g4|nn).d <= q' by A18,INT_1:81; not (g4|nn).d in {0} by A141,A145,A200,XBOOLE_0:3; then (g4|nn).d <> 0 by TARSKI:def 1; then (g4|nn).d > 0; hence thesis by A199,A201,FINSEQ_1:def 7; end; suppose ex l being Nat st l in dom g5 & d=len(g4|nn)+ l; then consider l be Element of NAT such that A202: l in dom g5 & d = len(g4|nn)+ l by ORDINAL1:def 13; g6.d = g5.l by A202,FINSEQ_1:def 7; hence thesis by A177,A202; end; end; then rng g6 = rng idseq q' by A186,A187,A197,Th40; then A203:g6,(idseq q') are_fiberwise_equipotent by A197,RFINSEQ:39; A204:g6 is FinSequence of REAL & g4/^nn is FinSequence of REAL by FINSEQ_2:27; then N = Sum g6 by A203,RFINSEQ:22 .= Sum(g4|nn) + Sum g5 by RVSUM_1:105 .= Sum(g4|nn) + (mm*q - Sum(g4/^nn)) by A172,A204,Th47 .= Sum(g4|nn) + mm*q - Sum(g4/^nn); then (p-1)*N = q*(Sum g2) + 2*Sum(Sgm XX) - mm*q by A159,A161,A163; then A205:(p-'1)*N mod 2 = ((q*(Sum g2)-mm*q) + 2*Sum(Sgm XX)) mod 2 by A7,BINARITH:50 .= (q*(Sum g2)-mm*q) mod 2 by EULER_1:13; 2 divides (p-'1)*N by A11,NAT_D:9; then (q*((Sum g2)-mm)) mod 2 = 0 by A205,PEPIN:6; then A206:2 divides (q*((Sum g2)-mm)) by Lm2; 2,(q qua Integer) are_relative_prime by A4,EULER_2:1; then 2 divides ((Sum g2) - mm) by A206,INT_2:40; then (Sum g2),mm are_congruent_mod 2 by INT_2:19; then (Sum g2) mod 2 = mm mod 2 by INT_3:12; then (-1)|^(Sum g2) = (-1)|^mm by Th45; hence thesis by A1,A3,A145,Th41; end; end; (Sum f2) + (Sum g2) = p' * q' proof reconsider A = Seg p',B = Seg q' as non empty finite Subset of NAT by A9,FINSEQ_1:5; deffunc F(Element of A,Element of B) = $1/p - $2/q; A207: for x be Element of A, y be Element of B holds F(x,y) in REAL by XREAL_0:def 1; consider z being Function of [:A,B:], REAL such that A208: for x be Element of A, y be Element of B holds z.(x,y) = F(x,y) from FUNCT_7:sch 1(A207); defpred G[set,set] means ex x be Element of A st $1=x & $2 = {[x,y] where y is Element of B:z.(x,y)>0}; A209: for d being Nat st d in Seg p' ex x1 be Element of bool dom z st G[d,x1] proof let d be Nat; assume d in Seg p'; then reconsider d as Element of A; take x1 = {[d,y] where y is Element of B:z.(d,y)>0}; x1 c= dom z proof let l be set; assume l in x1; then consider yy be Element of B such that A210: [d,yy] = l & z.(d,yy) > 0; l in [:A,B:] by A210; hence thesis by FUNCT_2:def 1; end; hence thesis; end; consider Pr be FinSequence of bool dom z such that A211: dom Pr = Seg p' & for d being Nat st d in Seg p' holds G[d,Pr.d] from FINSEQ_1:sch 5(A209); A212: len Pr = p' by A211,FINSEQ_1:def 3; for d,e st d in dom Pr & e in dom Pr & d<>e holds Pr.d misses Pr.e proof let d,e; assume A213:d in dom Pr & e in dom Pr & d<>e; then consider x1 be Element of A such that A214: x1=d & Pr.d = {[x1,y] where y is Element of B:z.(x1,y)>0} by A211; consider x2 be Element of A such that A215: x2=e & Pr.e = {[x2,y] where y is Element of B:z.(x2,y)>0} by A211,A213; now assume not Pr.d misses Pr.e; then consider l be set such that A216: l in Pr.d & l in Pr.e by XBOOLE_0:3; consider y1 be Element of B such that A217: l = [x1,y1] & z.(x1,y1) > 0 by A214,A216; consider y2 be Element of B such that A218: l = [x2,y2] & z.(x2,y2) > 0 by A215,A216; thus contradiction by A213,A214,A215,A217,A218,ZFMISC_1:33; end; hence thesis; end; then A219:Card union rng Pr = Sum Card Pr by A212,Th48; defpred K[set,set] means ex y be Element of B st $1=y & $2 = {[x,y] where x is Element of A:z.(x,y)<0}; A220: for d being Nat st d in Seg q' ex x1 be Element of bool dom z st K[d,x1] proof let d be Nat; assume d in Seg q'; then reconsider d as Element of B; take x1 = {[x,d] where x is Element of A:z.(x,d)<0}; x1 c= dom z proof let l be set; assume l in x1; then consider xx be Element of A such that A221: [xx,d] = l & z.(xx,d) < 0; l in [:A,B:] by A221; hence thesis by FUNCT_2:def 1; end; hence thesis; end; consider Pk be FinSequence of bool dom z such that A222: dom Pk = Seg q' & for d being Nat st d in Seg q' holds K[d,Pk.d] from FINSEQ_1:sch 5(A220); A223: len Pk = q' by A222,FINSEQ_1:def 3; for d,e st d in dom Pk & e in dom Pk & d<>e holds Pk.d misses Pk.e proof let d,e; assume A224:d in dom Pk & e in dom Pk & d<>e; then consider y1 be Element of B such that A225: y1=d & Pk.d = {[x,y1] where x is Element of A:z.(x,y1)<0} by A222; consider y2 be Element of B such that A226: y2=e & Pk.e = {[x,y2] where x is Element of A:z.(x,y2)<0} by A222,A224; now assume not Pk.d misses Pk.e; then consider l be set such that A227: l in Pk.d & l in Pk.e by XBOOLE_0:3; consider x1 be Element of A such that A228: l = [x1,y1] & z.(x1,y1) < 0 by A225,A227; consider x2 be Element of A such that A229: l = [x2,y2] & z.(x2,y2) < 0 by A226,A227; thus contradiction by A224,A225,A226,A228,A229,ZFMISC_1:33; end; hence thesis; end; then A230:Card union rng Pk = Sum Card Pk by A223,Th48; reconsider U1 = union rng Pr, U2 = union rng Pk as finite Subset of dom z by FINSET_1:13,PROB_3:53; U1 misses U2 proof assume U1 meets U2; then consider l be set such that A231: l in U1 & l in U2 by XBOOLE_0:3; l in Union Pr by A231; then consider k1 be Nat such that A232: k1 in dom Pr & l in Pr.k1 by PROB_3:54; l in Union Pk by A231; then consider k2 be Nat such that A233: k2 in dom Pk & l in Pk.k2 by PROB_3:54; reconsider k1,k2 as Element of NAT by ORDINAL1:def 13; consider m1 be Element of A such that A234: m1 = k1 & Pr.k1 = {[m1,y] where y is Element of B:z.(m1,y)>0} by A211,A232; consider m2 be Element of B such that A235: l = [m1,m2] & z.(m1,m2) > 0 by A232,A234; consider n1 be Element of B such that A236: n1 = k2 & Pk.k2 = {[x,n1] where x is Element of A:z.(x,n1)<0} by A222,A233; consider n2 be Element of A such that A237: l = [n2,n1] & z.(n2,n1) < 0 by A233,A236; m1 = n2 & m2 = n1 by A235,A237,ZFMISC_1:33; hence contradiction by A235,A237; end; then A238:card(U1 \/ U2) = (Sum Card Pr) + (Sum Card Pk) by A219,A230,CARD_2:53; U1 \/ U2 = dom z proof dom z c= U1 \/ U2 proof let l be set; assume l in dom z; then consider x,y be set such that A239: x in A & y in B & l = [x,y] by ZFMISC_1:def 2; reconsider x as Element of A by A239; reconsider y as Element of B by A239; A240: z.(x,y) <> 0 proof assume z.(x,y) = 0; then x/p - y/q = 0 by A208; then x*q = y*p by XCMPLX_1:96; then p divides x*q by NAT_D:def 3; then A241:p divides x by A3,WSIERP_1:37; A242: x >= 0 + 1 & x <= p' by FINSEQ_1:3; then p <= x by A241,NAT_D:7; hence contradiction by A16,A242,XXREAL_0:2; end; per cases by A240; suppose A243:z.(x,y) > 0; G[x,Pr.x] by A211; then l in Pr.x by A239,A243; then l in Union Pr by A211,PROB_3:54; hence thesis by XBOOLE_0:def 2; end; suppose A244:z.(x,y) < 0; K[y,Pk.y] by A222; then l in Pk.y by A239,A244; then l in Union Pk by A222,PROB_3:54; hence thesis by XBOOLE_0:def 2; end; end; hence thesis by XBOOLE_0:def 10; end; then A245:(Sum Card Pr) + (Sum Card Pk) = card [:A,B:] by A238,FUNCT_2:def 1 .= card A * card B by CARD_2:65 .= p'* card B by FINSEQ_1:78 .= p' * q' by FINSEQ_1:78; A246:Card Pr = f2 proof A247:dom Card Pr = dom Pr by CARD_3:def 2 .= dom f2 by A30,A211,FINSEQ_1:def 3; for d being Nat st d in dom Card Pr holds (Card Pr).d = f2.d proof let d be Nat; assume A248:d in dom Card Pr; then A249:d in dom Pr by CARD_3:def 2; d in Seg p' by A30,A247,A248,FINSEQ_1:def 3; then consider m be Element of A such that A250: m = d & Pr.d = {[m,y] where y is Element of B:z.(m,y)>0} by A211; Pr.d = [:{m},Seg(f2.m):] proof set L = [:{m},Seg(f2.m):]; A251: Pr.d c= L proof let l be set; assume l in Pr.d; then consider y1 be Element of B such that A252: l = [m,y1] & z.(m,y1) > 0 by A250; m/p - y1/q > 0 by A208,A252; then m/p - y1/q + y1/q > 0 + y1/q by XREAL_1:8; then m/p*q > y1/q*q by XREAL_1:70; then (m*q)/p > y1 by XCMPLX_1:88; then A253:((m*q) div p) >= y1 by INT_1:81; m in Seg p';then A254: m in dom f1 by A6,FINSEQ_1:def 3; then ((f1.m) div p) >= y1 by A19,A253;then A255: y1 <= f2.m by A30,A33,A254; y1 >= 1 by FINSEQ_1:3;then A256: y1 in Seg(f2.m) by A255,FINSEQ_1:3; m in {m} by TARSKI:def 1; hence thesis by A252,A256,ZFMISC_1:def 2; end; L c= Pr.d proof let l be set; assume l in L; then consider x,y be set such that A257: x in {m} & y in Seg(f2.m) & l = [x,y] by ZFMISC_1:def 2; m <= p' by FINSEQ_1:3; then m*q <= p'*q by XREAL_1:66;then A258: (m*q) div p <= (p'*q) div p by NAT_2:26; now assume q mod p = 0; then A259:p divides q by PEPIN:6; then p <= q by NAT_D:7; then p < q by A1,REAL_1:def 5; hence contradiction by A7,A259,NAT_4:12; end; then A260: -(q div p) = (-q) div p + 1 by WSIERP_1:49; 2 divides (p-'1)*q by A11,NAT_D:9; then (p-'1)*q mod 2 = 0 by PEPIN:6; then ((p-'1)*q) div 2 = (p-'1)*q/2 by REAL_3:4;then A261: (p'*q) div p = ((p-1)*q) div (2*p) by A8,A12,NAT_2:29 .= ((p*q - q) div p) div 2 by PRE_FF:5 .= (q+(-(q div p)-1)) div 2 by A260,INT_3:8 .= (2*q'+(-(q div p))) div 2 by A8,A12 .= q'+((-(q div p)) div 2) by INT_3:8; (p'*q) div p <= q' proof per cases; suppose (q div p) mod 2 = 0; then (-(q div p)) div 2 = -((q div p) div 2) by WSIERP_1:50 .= -(q div (2*p)) by NAT_2:29; then (p'*q) div p = q'-(q div (2*p)) by A261; hence thesis by XREAL_1:45; end; suppose (q div p) mod 2 <> 0; then -((q div p) div 2) = (-(q div p)) div 2 +1 by WSIERP_1:49; then (-(q div p)) div 2 = -((q div p) div 2)-1 .= -(q div (2*p)) - 1 by NAT_2:29; then (p'*q) div p = q' -((q div (2*p)) + 1) by A261; hence thesis by XREAL_1:45; end; end; then A262:(m*q) div p <= q' by A258,XXREAL_0:2; m in Seg p';then A263: m in dom f1 by A6,FINSEQ_1:def 3; then A264:f2.m = f1.m div p by A30,A33 .= (m*q) div p by A19,A263; reconsider y as Element of NAT by A257; 1 <= y & y <= f2.m by A257,FINSEQ_1:3; then 1 <= y & y <= q' by A262,A264,XXREAL_0:2; then reconsider y as Element of B by FINSEQ_1:3; A265: y <= [\m*q/p/] by A257,A264,FINSEQ_1:3; now assume m*q/p is integer; then p divides m*q by WSIERP_1:22; then A266:p divides m by A3,WSIERP_1:37; A267: 0+1 <= m & m <= p' by FINSEQ_1:3; then p <= m by A266,NAT_D:7; hence contradiction by A16,A267,XXREAL_0:2; end; then [\m*q/p/] < m*q/p by INT_1:48; then y < m*q/p by A265,XXREAL_0:2; then y*p < (m*q)/p*p by XREAL_1:70; then y*p < m*q by XCMPLX_1:88; then y/q < m/p by XREAL_1:108; then m/p - y/q > 0 by XREAL_1:52; then z.(m,y) > 0 by A208; then [m,y] in Pr.d by A250; hence thesis by A257,TARSKI:def 1; end; hence thesis by A251,XBOOLE_0:def 10; end; then Card(Pr.d) = Card [:Seg(f2.m),{m}:] by CARD_2:11 .= Card Seg(f2.m) by CARD_2:13; then Card(Pr.d) = Card(f2.d) by A250,FINSEQ_1:76 .= f2.d by CARD_1:66; hence thesis by A249,CARD_3:def 2; end; hence thesis by A247,FINSEQ_1:17; end; Card Pk = g2 proof A268:dom Card Pk = Seg(len g2) by A124,A222,CARD_3:def 2 .= dom g2 by FINSEQ_1:def 3; for d being Nat st d in dom Card Pk holds (Card Pk).d = g2.d proof let d be Nat; assume A269:d in dom Card Pk; then A270:d in dom Pk by CARD_3:def 2; d in Seg q' by A124,A268,A269,FINSEQ_1:def 3; then consider n be Element of B such that A271: n = d & Pk.d = {[x,n] where x is Element of A:z.(x,n)<0} by A222; Pk.d = [:Seg(g2.n),{n}:] proof set L = [:Seg(g2.n),{n}:]; A272: Pk.d c= L proof let l be set; assume l in Pk.d; then consider x be Element of A such that A273: l = [x,n] & z.(x,n) < 0 by A271; x/p - n/q < 0 by A208,A273; then x/p - n/q + n/q < 0 + n/q by XREAL_1:8; then x/p*p < n/q*p by XREAL_1:70; then x < (n*p)/q by XCMPLX_1:88;then A274: x <= (n*p) div q by INT_1:81; n in Seg q';then A275: n in dom g1 by A112,FINSEQ_1:def 3;then ((g1.n) div q) >= x by A113,A274;then A276: x <= g2.n by A124,A127,A275; x >= 1 by FINSEQ_1:3;then A277: x in Seg(g2.n) by A276,FINSEQ_1:3; n in {n} by TARSKI:def 1; hence thesis by A273,A277,ZFMISC_1:def 2; end; L c= Pk.d proof let l be set; assume l in L; then consider x,y be set such that A278: x in Seg(g2.n) & y in {n} & l = [x,y] by ZFMISC_1:def 2; n <= q' by FINSEQ_1:3; then n*p <= q'*p by XREAL_1:66;then A279: (n*p) div q <= (q'*p) div q by NAT_2:26; now assume p mod q = 0; then A280:q divides p by PEPIN:6; then q <= p by NAT_D:7; then q < p by A1,REAL_1:def 5; hence contradiction by A7,A280,NAT_4:12; end; then A281: -(p div q) = (-p) div q + 1 by WSIERP_1:49; 2 divides (q-'1)*p by A11,NAT_D:9; then (q-'1)*p mod 2 = 0 by PEPIN:6; then ((q-'1)*p) div 2 = (q-'1)*p/2 by REAL_3:4;then A282: (q'*p) div q = ((q-1)*p) div (2*q) by A8,A12,NAT_2:29 .= ((q*p - p) div q) div 2 by PRE_FF:5 .= (p+(-(p div q)-1)) div 2 by A281,INT_3:8 .= (2*p'-(p div q)) div 2 by A8,A12 .= p'+((-(p div q)) div 2) by INT_3:8; (q'*p) div q <= p' proof per cases; suppose (p div q) mod 2 = 0; then (-(p div q)) div 2 = -((p div q) div 2) by WSIERP_1:50 .= -(p div (2*q)) by NAT_2:29; then (q'*p) div q = p'-(p div (2*q)) by A282; hence thesis by XREAL_1:45; end; suppose (p div q) mod 2 <> 0; then -((p div q) div 2) = (-(p div q)) div 2 +1 by WSIERP_1:49; then (-(p div q)) div 2 = -((p div q) div 2)-1 .= -(p div (2*q)) - 1 by NAT_2:29; then (q'*p) div q = p' -((p div (2*q)) + 1) by A282; hence thesis by XREAL_1:45; end; end; then A283:(n*p) div q <= p' by A279,XXREAL_0:2; n in Seg q';then A284: n in dom g1 by A112,FINSEQ_1:def 3;then A285: g2.n = g1.n div q by A124,A127 .= (n*p) div q by A113,A284; reconsider x as Element of NAT by A278; A286: 1 <= x & x <= g2.n by A278,FINSEQ_1:3; then 1 <= x & x <= p' by A283,A285,XXREAL_0:2; then reconsider x as Element of A by FINSEQ_1:3; now assume n*p/q is integer; then q divides n*p by WSIERP_1:22; then A287:q divides n by A3,WSIERP_1:37; A288: 0+1 <= n & n <= q' by FINSEQ_1:3; then q <= n by A287,NAT_D:7; hence contradiction by A16,A288,XXREAL_0:2; end; then [\n*p/q/] < n*p/q by INT_1:48; then x < n*p/q by A285,A286,XXREAL_0:2; then x*q < (n*p)/q*q by XREAL_1:70; then x*q < n*p by XCMPLX_1:88; then x/p < n/q by XREAL_1:108; then x/p - n/q < 0 by XREAL_1:51; then z.(x,n) < 0 by A208; then [x,n] in Pk.d by A271; hence thesis by A278,TARSKI:def 1; end; hence thesis by A272,XBOOLE_0:def 10; end; then Card(Pk.d) = Card Seg(g2.n) by CARD_2:13; then Card(Pk.d) = Card(g2.d) by A271,FINSEQ_1:76 .= g2.d by CARD_1:66; hence thesis by A270,CARD_3:def 2; end; hence thesis by A268,FINSEQ_1:17; end; hence thesis by A245,A246; end; hence thesis by A69,A164,NEWTON:13; end; theorem p>2 & q>2 & p<>q & p mod 4 = 3 & q mod 4 = 3 implies Lege(p,q) = -Lege(q,p) proof assume A1:p>2 & q>2 & p<>q & p mod 4 = 3 & q mod 4 = 3; then A2:p=4*(p div 4)+3 & q = 4*(q div 4)+3 by NAT_D:2; p>1 & q>1 by INT_2:def 5; then p-'1 = p-1 & q-'1 = q-1 by BINARITH:50; then p-'1 = 2*(2*(p div 4)+1) & q-'1 = 2*(2*(q div 4)+1) by A2; then (p-'1) div 2=2*(p div 4)+1 & (q-'1) div 2=2*(q div 4)+1 by NAT_D:18; then A3:Lege(p,q)*Lege(q,p) =(-1)|^((2*(p div 4)+1)*(2*(q div 4)+1)) by A1,Th49 .=((-1)|^(2*(p div 4)+1))|^(2*(q div 4)+1) by NEWTON:14 .= ((-1)|^(2*(p div 4))*(-1))|^(2*(q div 4)+1) by NEWTON:11 .= ((((-1)|^2)|^(p div 4))*(-1))|^(2*(q div 4)+1) by NEWTON:14 .= ((1|^2)|^(p div 4)*(-1))|^(2*(q div 4)+1) by WSIERP_1:2 .= (1|^(p div 4)*(-1))|^(2*(q div 4)+1) by NEWTON:100,SQUARE_1:59 .= (1*(-1))|^(2*(q div 4)+1) by NEWTON:15 .= (-1)|^(2*(q div 4))*(-1) by NEWTON:11 .= ((-1)|^2)|^(q div 4) * (-1) by NEWTON:14 .= (1|^2)|^(q div 4) *(-1) by WSIERP_1:2 .= 1|^(q div 4) *(-1) by NEWTON:100,SQUARE_1:59 .= 1*(-1) by NEWTON:15; per cases by Th25; suppose Lege(p,q) = 1; hence thesis by A3; end; suppose Lege(p,q) = -1; hence thesis by A3; end; end; theorem p>2 & q>2 & p<>q & (p mod 4 = 1 or q mod 4 = 1) implies Lege(p,q) = Lege(q,p) proof assume A1:p>2 & q>2 & p<>q & (p mod 4 = 1 or q mod 4 = 1); p>1 & q>1 by INT_2:def 5; then A2:p-'1 = p-1 & q-'1 = q-1 by BINARITH:50; per cases by A1; suppose p mod 4 = 1; then p=4*(p div 4)+1 by NAT_D:2; then p-'1 = 2*(2*(p div 4)) by A2; then (p-'1) div 2 = 2*(p div 4) by NAT_D:18; then A3:Lege(p,q)*Lege(q,p) = (-1)|^((2*(p div 4))*((q-'1) div 2)) by A1,Th49 .= ((-1)|^(2*(p div 4)))|^((q-'1) div 2) by NEWTON:14 .= (((-1)|^2)|^(p div 4))|^((q-'1) div 2) by NEWTON:14 .= ((1|^2)|^(p div 4))|^((q-'1) div 2) by WSIERP_1:2 .= (1|^(p div 4))|^((q-'1) div 2) by NEWTON:100,SQUARE_1:59 .= 1|^((q-'1) div 2) by NEWTON:15 .= 1 by NEWTON:15; per cases by Th25; suppose Lege(p,q)=1; hence thesis by A3; end; suppose Lege(p,q)=-1; hence thesis by A3; end; end; suppose q mod 4 = 1; then q=4*(q div 4)+1 by NAT_D:2; then q-'1 = 2*(2*(q div 4)) by A2; then (q-'1) div 2 = 2*(q div 4) by NAT_D:18; then A4:Lege(p,q)*Lege(q,p) = (-1)|^((2*(q div 4))*((p-'1) div 2)) by A1,Th49 .= ((-1)|^(2*(q div 4)))|^((p-'1) div 2) by NEWTON:14 .= (((-1)|^2)|^(q div 4))|^((p-'1) div 2) by NEWTON:14 .= ((1|^2)|^(q div 4))|^((p-'1) div 2) by WSIERP_1:2 .= (1|^(q div 4))|^((p-'1) div 2) by NEWTON:100,SQUARE_1:59 .= 1|^((p-'1) div 2) by NEWTON:15 .= 1 by NEWTON:15; per cases by Th25; suppose Lege(p,q)=1; hence thesis by A4; end; suppose Lege(p,q)=-1; hence thesis by A4; end; end; end;