:: Basel Problem :: by Karol P\kak and Artur Korni{\l}owicz :: :: Received June 27, 2017 :: Copyright (c) 2017-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XCMPLX_0, SUBSET_1, FUNCT_1, ARYTM_3, ORDINAL4, COMPLEX1, NUMBERS, RELAT_1, NEWTON, NAT_1, CARD_3, SQUARE_1, SIN_COS, CARD_1, XXREAL_0, SEQ_1, VALUED_0, SERIES_1, PARTFUN1, XBOOLE_0, ARYTM_1, FINSEQ_1, RVSUM_1, TARSKI, XXREAL_1, SIN_COS4, ABIAN, ALGSTR_1, ALGSTR_0, VECTSP_1, SUPINF_2, BINOP_1, MESFUNC1, STRUCT_0, RLVECT_1, LATTICES, GROUP_1, POLYNOM3, ALGSEQ_1, POLYNOM1, POLYNOM2, QC_LANG1, FUNCSDOM, HAHNBAN1, COMPLFLD, AFINSQ_1, CQC_LANG, POLYNOM5, HURWITZ2, XREAL_0, UPROOTS, VECTSP_2, POLYVIE1, BASEL_1, BASEL_2; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, NUMBERS, XXREAL_0, XCMPLX_0, COMPLEX1, XREAL_0, NAT_1, NAT_D, SQUARE_1, CARD_1, FINSEQ_1, VALUED_0, VALUED_1, RVSUM_1, SEQ_1, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, NORMSP_1, ALGSTR_1, ALGSEQ_1, COMPLFLD, HAHNBAN1, RCOMP_1, SERIES_1, NEWTON, ABIAN, SIN_COS, SIN_COS4, BINOM, HURWITZ2, POLYNOM3, POLYNOM4, POLYNOM5, UPROOTS, VECTSP_2, NIVEN, POLYVIE1, BASEL_1; constructors SEQ_2, REAL_1, SIN_COS, SQUARE_1, COMSEQ_2, RELSET_1, COMSEQ_3, SIN_COS4, ABIAN, INTEGRA1, NAT_D, ALGSEQ_1, ALGSTR_1, HAHNBAN1, POLYNOM4, POLYNOM5, BINOM, BINOP_2, HURWITZ2, NIVEN, WSIERP_1, REALSET2, POLYVIE1, BASEL_1; registrations XCMPLX_0, NEWTON, XREAL_0, NAT_1, ORDINAL1, SQUARE_1, VALUED_0, RELSET_1, VALUED_1, MEMBERED, INT_1, SIN_COS, SIN_COS6, ABIAN, XBOOLE_0, XXREAL_0, FINSEQ_1, CARD_1, RVSUM_1, STRUCT_0, VECTSP_1, ALGSTR_1, POLYNOM3, ALGSTR_0, NEWTON01, COMPLEX1, COMPLFLD, POLYNOM5, HURWITZ2, NIVEN, ALGSEQ_1, RLVECT_1, UPROOTS, INT_6, FINSET_1, POLYNOM4, NEWTON04, BASEL_1; requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL; begin :: Preliminaries reserve k,m,n for Nat; reserve R for commutative Ring, p,q for Polynomial of R, z0,z1 for Element of R; registration let L be right_zeroed non empty doubleLoopStr; let n; reduce n * 0.L to 0.L; end; theorem :: BASEL_2:1 for z being Complex, e being Element of F_Complex st z = e holds n*z = n*e; registration let e be Element of F_Complex, z be Complex; let n; identify n*e with n*z when e = z; end; theorem :: BASEL_2:2 for Z being complex-valued FinSequence, E being FinSequence of F_Complex st E=Z holds Sum Z = Sum E; theorem :: BASEL_2:3 (1_F_Complex) |^ n = 1_F_Complex; theorem :: BASEL_2:4 for L being left_zeroed right_zeroed non empty addLoopStr for z0,z1 being Element of L holds <% z0,z1 %> = <%z0%> + <%0.L,z1%>; theorem :: BASEL_2:5 for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr for a,b,c,d being Element of L holds <%a,b%> *' <%c,d%> = <%a*c,a*d+b*c,b*d%>; theorem :: BASEL_2:6 for L being Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr holds <%0.L,0.L,1.L%> = <%0.L,1.L%>`^2; theorem :: BASEL_2:7 for L being right_zeroed add-associative right_complementable right-distributive non empty doubleLoopStr for z being Element of L, p being Polynomial of L holds (p*' <%z%>).n = (p.n) * z; theorem :: BASEL_2:8 for L being Abelian add-associative right_zeroed right_complementable well-unital associative commutative distributive non empty doubleLoopStr for x being Element of L holds <%x%>`^n = <%x|^n%>; theorem :: BASEL_2:9 (<%z0,z1%>`^0).0 = 1.R & (n >0 implies (<%0.R,z1%>`^n).n = z1|^n) & (k<>n implies (<%0.R,z1%>`^n).k = 0.R); theorem :: BASEL_2:10 (<%0.R,0.R,1_R%>`^n).(2*n) = 1_R & for k st k <> 2*n holds (<%0.R,0.R,1_R%>`^n).k = 0.R; theorem :: BASEL_2:11 for L being domRing, p being non-zero Polynomial of L holds card Roots p < len p; definition let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, a be Polynomial of L; func @a -> Element of Polynom-Ring L equals :: BASEL_2:def 1 a; end; definition let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, a be Polynomial of L; let n be Nat; func n * a -> Polynomial of L equals :: BASEL_2:def 2 n * @a; end; theorem :: BASEL_2:12 for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr for a being Polynomial of L holds (n * a).k = n * (a.k); theorem :: BASEL_2:13 (<% z0,z1 %>`^n).k = (n choose k) * ((z1|^k) * (z0|^(n-'k))); begin :: Imaginary complex numbers definition let z be Complex; attr z is imaginary means :: BASEL_2:def 3 Re z = 0; end; registration cluster -> imaginary; cluster real imaginary -> zero for Complex; cluster zero -> imaginary for Complex; end; registration let z1,z2 be imaginary Complex; cluster z1 * z2 -> real; cluster z1 + z2 -> imaginary; end; registration let z be imaginary Complex; let r be real Complex; cluster z*r -> imaginary; end; registration cluster 0.F_Complex -> real imaginary; end; registration cluster real imaginary for Element of F_Complex; end; registration let z be real Element of F_Complex; let n be Nat; cluster n * z -> real; end; registration let z be imaginary Element of F_Complex; let n be Nat; cluster n * z -> imaginary; end; registration let z be imaginary Complex; let n be even Nat; cluster (power F_Complex).(z,n) -> real; end; registration let z be imaginary Complex; let n be odd Nat; cluster (power F_Complex).(z,n) -> imaginary for Complex; end; registration let r be real Element of F_Complex; let n be Nat; cluster (power F_Complex).(r,n) -> real; end; registration cluster zero -> imaginary real for Element of F_Complex; end; definition let p be sequence of F_Complex; attr p is imaginary means :: BASEL_2:def 4 for i being Nat holds p.i is imaginary; end; registration let im1 be imaginary Element of F_Complex; cluster <%im1%> -> imaginary; let im2 be imaginary Element of F_Complex; cluster <%im1,im2%> -> imaginary; end; registration cluster imaginary for Polynomial of F_Complex; end; theorem :: BASEL_2:14 for I being imaginary Polynomial of F_Complex for r being real Element of F_Complex holds eval(I,r) is imaginary; theorem :: BASEL_2:15 for R being real Polynomial of F_Complex for r being real Element of F_Complex holds eval(R,r) is real; theorem :: BASEL_2:16 for im being imaginary Element of F_Complex, r being real Element of F_Complex st n is even holds even_part (<% im,r %>`^n) is real & odd_part (<% im,r %>`^n) is imaginary; theorem :: BASEL_2:17 for im being imaginary Element of F_Complex, r being real Element of F_Complex st n is odd holds even_part (<% im,r %>`^n) is imaginary & odd_part (<% im,r %>`^n) is real; theorem :: BASEL_2:18 for L being non empty ZeroStr for p being Polynomial of L st len even_part p <> 0 holds len even_part p is odd; begin :: Main facts definition let L be non empty set; let p be sequence of L; let m be Nat; func sieve(p,m) -> sequence of L means :: BASEL_2:def 5 for i being Nat holds it.i = p.(m*i); end; registration let L be non empty ZeroStr; let p be finite-Support sequence of L; let m be non zero Nat; cluster sieve(p,m) -> finite-Support; end; theorem :: BASEL_2:19 for L being non empty ZeroStr for p being sequence of L holds sieve(p,2*k) = sieve(even_part p,2*k); theorem :: BASEL_2:20 for L being non empty ZeroStr for p being Polynomial of L st len even_part p is odd holds 2 * len sieve(p,2) = len even_part p+1; theorem :: BASEL_2:21 for L being non empty ZeroStr for p being Polynomial of L st len even_part p = 0 for n be non zero Nat holds len sieve(p,2*n) = 0; theorem :: BASEL_2:22 for L being Field for p being Polynomial of L holds even_part p = Subst(sieve(p,2),<% 0.L,0.L,1_L%>); theorem :: BASEL_2:23 sieve (<%i_FC,1.F_Complex%> `^ (2*n+1),2).n = ((2*n+1) choose 1) * i_FC; theorem :: BASEL_2:24 n >= 1 implies sieve (<%i_FC,1.F_Complex%> `^ (2*n+1),2).(n-1) = ((2*n+1) choose 3) * (-i_FC); theorem :: BASEL_2:25 len sieve (<%i_FC,1.F_Complex%> `^ (2*n+1),2) = n + 1; registration let n be Nat; cluster sieve (<%i_FC,1.F_Complex%> `^ (2*n+1),2) -> non-zero; end; theorem :: BASEL_2:26 rng sqr cot x_r-seq(n) c= Roots (sieve (<%i_FC,1.F_Complex%> `^ (2*n+1),2)); theorem :: BASEL_2:27 Roots (sieve (<%i_FC,1.F_Complex%> `^ (2*n+1),2)) = rng sqr cot x_r-seq(n); theorem :: BASEL_2:28 Sum sqr cot x_r-seq(m) = 2*m*(2*m-1)/6; theorem :: BASEL_2:29 Sum sqr cosec x_r-seq(m) = 2*m*(2*m+2)/6; theorem :: BASEL_2:30 Basel-seq1.m <= Sum(Basel-seq,m); theorem :: BASEL_2:31 Sum(Basel-seq,m) <= Basel-seq2.m; ::$N Basel problem theorem :: BASEL_2:32 Sum Basel-seq = PI^2/6; registration cluster Partial_Sums(Basel-seq) -> non summable for Real_Sequence; end;