:: Basel Problem -- Preliminaries :: by Artur Korni{\l}owicz and Karol P\kak :: :: Received June 27, 2017 :: Copyright (c) 2017-2018 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, SEQ_4, ORDINAL2, NUMBERS, REAL_1, RELAT_1, NAT_1, CARD_3, SQUARE_1, SIN_COS, CARD_1, XXREAL_0, SEQ_1, VALUED_0, SEQ_2, VALUED_1, PARTFUN1, XBOOLE_0, ARYTM_1, XXREAL_2, FINSEQ_1, RVSUM_1, INT_1, TARSKI, XXREAL_1, SIN_COS4, ABIAN, RCOMP_1, MEASURE5, REALSET1, INTEGRA1, PREPOWER, POLYEQ_1, COMSEQ_1, FINSEQ_2, BASEL_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NUMBERS, XXREAL_0, XCMPLX_0, COMPLEX1, XREAL_0, INT_1, SQUARE_1, CARD_1, FINSEQ_1, VALUED_0, VALUED_1, RVSUM_1, SEQ_1, SEQ_2, SEQ_4, RFUNCT_1, FCONT_1, RCOMP_1, SERIES_1, PREPOWER, ABIAN, TAYLOR_1, SIN_COS, SIN_COS4, INTEGRA1, MEASURE5, INTEGRA5, POLYEQ_1, FINSEQ_2, COMSEQ_1, COMSEQ_3; constructors SEQ_2, SIN_COS, SQUARE_1, COMSEQ_2, RELSET_1, COMSEQ_3, SIN_COS4, RFUNCT_1, ABIAN, INTEGRA1, INTEGRA5, FCONT_1, TAYLOR_1, PREPOWER, SEQ_4, WSIERP_1, POLYEQ_1; registrations XCMPLX_0, XREAL_0, NAT_1, ORDINAL1, SQUARE_1, VALUED_0, RELSET_1, VALUED_1, MEMBERED, FUNCT_2, INT_1, NUMBERS, SIN_COS, SEQ_2, SIN_COS6, RCOMP_1, FCONT_1, MEASURE5, LEIBNIZ1, DBLSEQ_2, XBOOLE_0, XXREAL_0, RELAT_1, FINSEQ_1, CARD_1, RVSUM_1, NEWTON04, POLYEQ_1, NEWTON; requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL; definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, SEQ_2, CARD_1; equalities SERIES_1, SIN_COS, SIN_COS4, XCMPLX_0, SQUARE_1, FINSEQ_1; expansions TARSKI; theorems SEQ_2, ORDINAL1, PREPOWER, XCMPLX_1, VALUED_1, SEQ_4, XREAL_1, XXREAL_0, TARSKI, FUNCT_1, FINSEQ_3, XXREAL_1, NAT_1, XREAL_0, XBOOLE_1, FINSEQ_1, RVSUM_1, RELAT_1, RCOMP_1, SIN_COS5, RFUNCT_1, ABIAN, INT_1, COMPLEX2, SIN_COS, COMPTRIG, SIN_COS6, INTEGRA2, FUNCT_2, XBOOLE_0, ZFMISC_1, INTEGRA5, PARTFUN1, MEASURE5, DBLSEQ_2, INTEGRA7, TAYLOR_1, FCONT_1, SIN_COS9, JORDAN5A, INTEGRA8, CARD_1, COMPLSP2, RVSUM_2, SQUARE_1, POLYEQ_1, COMSEQ_3, FINSEQ_2; schemes FUNCT_1, FINSEQ_2, COMSEQ_1; begin :: Preliminaries reserve X for set; reserve k,m,n for Nat; reserve i for Integer; reserve a,b,c,d,e,g,p,r,x,y for Real; reserve z for Complex; set p = PI^2/6; theorem Th1: 0 < a implies ex m st 0 < a*m+b proof assume A1: 0 < a; then A2: (-b)/a*a = -b by XCMPLX_1:87; consider m such that A3: -b/a < m by SEQ_4:3; take m; (-b/a)*a < m*a by A1,A3,XREAL_1:68; then -b+b < a*m+b by A2,XREAL_1:8; hence thesis; end; Lm1: for f being FinSequence, h being Function st dom h = dom f holds h is FinSequence proof let f be FinSequence, h be Function such that A1: dom h = dom f; h is FinSequence-like proof take len f; thus thesis by A1,FINSEQ_1:def 3; end; hence thesis; end; Lm2: for f being FinSequence, y being object st y in rng f ex n being Nat st 1 <= n <= len f & y = f.n proof let f be FinSequence; let y be object; assume y in rng f; then consider n being object such that A1: n in dom f and A2: f.n = y by FUNCT_1:def 3; reconsider n as Nat by A1; take n; thus thesis by A1,A2,FINSEQ_3:25; end; Lm3: for f being complex-valued FinSequence holds len(f") = len f proof let f be complex-valued FinSequence; dom(f") = dom f by VALUED_1:def 7; hence thesis by FINSEQ_3:29; end; registration let f be real-valued FinSequence; let n; cluster f|n -> REAL-valued; coherence proof rng(f|Seg n) c= REAL; hence rng(f|n) c= REAL; end; end; registration let f be complex-valued FinSequence; cluster f^2 -> len f-element; coherence proof dom(f^2) = dom f by VALUED_1:11; hence len(f^2) = len f by FINSEQ_3:29; end; cluster f" -> len f-element; coherence proof dom (f") = dom f by VALUED_1:def 7; hence len (f") = len f by FINSEQ_3:29; end; end; registration let f be complex-valued FinSequence; let c be Complex; cluster c+f -> len f-element; coherence proof dom (c+f) = dom f by VALUED_1:def 2; hence len (c+f) = len f by FINSEQ_3:29; end; end; theorem Th2: for c,z being Complex holds c + <*z*> = <*c+z*> proof let c,z be Complex; A1: len <*z*> = 1 by FINSEQ_1:39; A2: len <*c+z*> = 1 by FINSEQ_1:39; A3: len(c+<*z*>) = len <*z*> by CARD_1:def 7; thus len(c+<*z*>) = len <*c+z*> by A1,A2,CARD_1:def 7; let k such that A4: 1 <= k & k <= len(c+<*z*>); A5: k = 1 by A1,A3,A4,XXREAL_0:1; k in dom(c+<*z*>) by A4,FINSEQ_3:25; hence (c+<*z*>).k = c+(<*z*>.k) by VALUED_1:def 2 .= <*c+z*>.k by A5; end; theorem Th3: for f,g being complex-valued FinSequence, c being Complex holds c+(f^g) = (c+f)^(c+g) proof let f,g be complex-valued FinSequence; let c be Complex; A1: len(c+(f^g)) = len(f^g) by CARD_1:def 7; A2: len(c+f) = len f by CARD_1:def 7; A3: len(c+g) = len g by CARD_1:def 7; A4: len(f^g) = len f + len g by FINSEQ_1:22; A5: len((c+f)^(c+g)) = len(c+f) + len(c+g) by FINSEQ_1:22; hence len(c+(f^g)) = len((c+f)^(c+g)) by A2,A3,A4,CARD_1:def 7; let k such that A6: 1 <= k and A7: k <= len(c+(f^g)); k in dom(c+(f^g)) by A6,A7,FINSEQ_3:25; then A8: (c+(f^g)).k = c+((f^g).k) by VALUED_1:def 2; per cases; suppose A9: k <= len f; then A10: (f^g).k = f.k by A6,FINSEQ_1:64; k in dom(c+f) by A2,A6,A9,FINSEQ_3:25; hence (c+(f^g)).k = (c+f).k by A8,A10,VALUED_1:def 2 .= ((c+f)^(c+g)).k by A2,A6,A9,FINSEQ_1:64; end; suppose A11: k > len f; then A12: (f^g).k = g.(k-len f) by A1,A7,FINSEQ_1:24; A13: len f - len f < k - len f by A11,XREAL_1:9; A14: k-len f is Nat by A11,NAT_1:21; then A15: 0+1 <= k-len f by A13,NAT_1:13; k - len f <= len f + len g - len f by A1,A4,A7,XREAL_1:9; then A16: k-len f in dom(c+g) by A14,A15,A3,FINSEQ_3:25; thus (c+(f^g)).k = (c+g).(k-len f) by A8,A12,A16,VALUED_1:def 2 .= ((c+f)^(c+g)).k by A1,A2,A3,A4,A5,A7,A11,FINSEQ_1:24; end; end; theorem for f being complex-valued FinSequence, c being Complex holds Sum(c+f) = (c*len f) + Sum f proof let f be complex-valued FinSequence; let c be Complex; defpred P[complex-valued FinSequence] means Sum(c+$1) = (c*len$1) + Sum $1; A1: P[<*>COMPLEX]; A2: for p being FinSequence of COMPLEX, x being Element of COMPLEX st P[p] holds P[p^<*x*>] proof let p be FinSequence of COMPLEX, x be Element of COMPLEX such that A3: Sum(c+p) = (c*len p) + Sum p; set g = p^<*x*>; A4: len <*x*> = 1 by FINSEQ_1:39; A5: len g = len p + len <*x*> by FINSEQ_1:22; A6: c+<*x*> = <*c+x*> by Th2; A7: Sum g = Sum p + Sum <*x*> by RVSUM_2:32; c+g = (c+p)^(c+<*x*>) by Th3; hence Sum(c+g) = Sum(c+p) + Sum(c+<*x*>) by RVSUM_2:32 .= (c*len g) + Sum g by A3,A4,A5,A6,A7; end; A8: for p being FinSequence of COMPLEX holds P[p] from FINSEQ_2:sch 2(A1,A2); f is FinSequence of COMPLEX by RVSUM_1:146; hence thesis by A8; end; begin :: Limits of sequences$\frac{an+b}{cn+d}$definition let a,b,c,d be Complex; deffunc F(Nat) = Polynom(a,b,$1)/Polynom(c,d,$1); func Rat_Exp_Seq(a,b,c,d) -> Complex_Sequence means :Def1: it.n = Polynom(a,b,n)/Polynom(c,d,n); existence proof ex f being Complex_Sequence st for n holds f.n = F(n) from COMSEQ_1:sch 1; hence thesis; end; uniqueness proof let f,f1 be Complex_Sequence such that A1: f.n = F(n) and A2: f1.n = F(n); let n be Element of NAT; thus f.n = F(n) by A1 .= f1.n by A2; end; end; definition let a,b,c,d; func rseq(a,b,c,d) -> Real_Sequence equals Re (Rat_Exp_Seq(a,b,c,d)); coherence; end; theorem Th5: rseq(a,b,c,d).n = (a*n+b)/(c*n+d) proof A1: dom Re(Rat_Exp_Seq(a,b,c,d)) = NAT & n in NAT by FUNCT_2:def 1, ORDINAL1:def 12; thus rseq(a,b,c,d).n = Re (Rat_Exp_Seq(a,b,c,d).n) by COMSEQ_3:def 3,A1 .= Re (Polynom(a,b,n)/Polynom(c,d,n)) by Def1 .= Re ((a*n+b)/Polynom(c,d,n)) by POLYEQ_1:def 1 .= (a*n+b)/(c*n+d) by POLYEQ_1:def 1; end; theorem Th6: rseq(0,b,0,d).n = b/d proof thus rseq(0,b,0,d).n = (0*n+b)/(0*n+d) by Th5 .= b/d; end; registration let a,b; cluster rseq(a,b,0,0) -> constant; coherence proof set f = rseq(a,b,0,0); let x,y be object; assume x in dom f & y in dom f; then reconsider n = x, m = y as Nat; thus f.x = (a*n+b)/(0*n+0) by Th5 .= (a*m+b)/(0*m+0) .= f.y by Th5; end; end; registration let b,d; cluster rseq(0,b,0,d) -> constant; coherence proof set f = rseq(0,b,0,d); let x,y be object such that A1: x in dom f and A2: y in dom f; thus f.x = b/d by A1,Th6 .= f.y by A2,Th6; end; end; theorem Th7: rseq(0,b,c,d) = b(#)rseq(0,1,c,d) & rseq(0,b,c,d) = (-b)(#)rseq(0,1,-c,-d) proof thus rseq(0,b,c,d) = b(#)rseq(0,1,c,d) proof set f1 = rseq(0,1,c,d); let n be Element of NAT; thus rseq(0,b,c,d).n = (0*n+b)/(c*n+d) by Th5 .= (b)*((0*n+1)/(c*n+d)) .= b*(f1.n) by Th5 .= (b(#)f1).n by VALUED_1:6; end; thus rseq(0,b,c,d) = (-b)(#)rseq(0,1,-c,-d) proof set f1 = rseq(0,1,-c,-d); let n be Element of NAT; thus rseq(0,b,c,d).n = (0*n+b)/(c*n+d) by Th5 .= ((-1)*b)/((-1)*(c*n+d)) by XCMPLX_1:91 .= (-b)*((0*n+1)/((-c)*n+-d)) .= (-b)*(f1.n) by Th5 .= ((-b)(#)f1).n by VALUED_1:6; end; end; theorem Th8: rseq(a,0,c,d) = a(#)rseq(1,0,c,d) & rseq(a,0,c,d) = (-a)(#)rseq(1,0,-c,-d) proof thus rseq(a,0,c,d) = (a)(#)rseq(1,0,c,d) proof set f = rseq(a,0,c,d); set f1 = rseq(1,0,c,d); let n be Element of NAT; A1: f1.n = (1*n+0)/(c*n+d) by Th5; thus f.n = (a*n+0)/(c*n+d) by Th5 .= a*((1*n+0)/(c*n+d)) .= (a(#)f1).n by A1,VALUED_1:6; end; thus rseq(a,0,c,d) = (-a)(#)rseq(1,0,-c,-d) proof set f = rseq(a,0,c,d); set f1 = rseq(1,0,-c,-d); let n be Element of NAT; A2: f1.n = (1*n+0)/((-c)*n+-d) by Th5; thus f.n = (a*n+0)/(c*n+d) by Th5 .= ((-1)*(a*n))/((-1)*(c*n+d)) by XCMPLX_1:91 .= (-a)*((1*n+0)/((-c)*n+-d)) .= ((-a)(#)f1).n by A2,VALUED_1:6; end; end; Lm4: 0 < c implies for p st 0 < p ex n st for m st n <= m holds |.rseq(0,1,c,d).m-0 .| < p proof set f = rseq(0,1,c,d); assume A1: 0 < c; let p such that A2: 0 < p; consider z being Nat such that A3: c*z+d > 0 by A1,Th1; consider n such that A4: n > (1-p*d)/(c*p) by SEQ_4:3; reconsider mm = max(n,z) as Nat by TARSKI:1; take mm; let m such that A5: mm <= m; A6: f.m = (0*m+1)/(c*m+d) by Th5 .= 1/(c*m+d); mm >= z by XXREAL_0:25; then m >= z by A5,XXREAL_0:2; then c*m >= c*z by A1,XREAL_1:64; then A7: c*m+d >= c*z+d by XREAL_1:6; A8: p*(c*m+d)/(c*m+d) = p by A3,A7,XCMPLX_1:89; A9: (1-p*d)/(c*p)*(c*p) = 1-p*d by A1,A2,XCMPLX_1:87; mm >= n by XXREAL_0:25; then (1-p*d)/(c*p) < mm by A4,XXREAL_0:2; then (1-p*d)/(c*p) < m by A5,XXREAL_0:2; then (1-p*d)/(c*p)*(c*p) < m*(c*p) by A1,A2,XREAL_1:68; then 1-p*d+p*d < m*(c*p)+p*d by A9,XREAL_1:8; then A10: 1/(c*m+d) < p by A8,A3,A7,XREAL_1:74; -p < 0 by A2; hence|.f.m-0 .| < p by A3,A7,A6,A10,SEQ_2:1; end; Lm5: 0 < c implies rseq(0,1,c,d) is convergent proof set f = rseq(0,1,c,d); assume A1: 0 < c; take 0; let p; assume 0 0; hence thesis by Lm5; end; suppose A1: c < 0; A2: rseq(0,1,c,d) = (-1)(#)rseq(0,1,-c,-d) by Th7; rseq(0,1,-c,-d) is convergent by A1,Lm5; hence thesis by A2; end; end; Lm7: 0 < c implies lim rseq(0,1,c,d) = 0 proof set f = rseq(0,1,c,d); assume A1: 0 < c; then A2: f is convergent by Lm5; for p st 0 < p ex n st for m st n <= m holds |.f.m-0 .| < p by A1,Lm4; hence thesis by A2,SEQ_2:def 7; end; Lm8: c < 0 implies lim rseq(0,1,c,d) = 0 proof set f = rseq(0,1,c,d); assume A1: c < 0; set f1 = rseq(0,1,-c,-d); A2: f = (-1)(#)f1 by Th7; lim f1 = 0 by A1,Lm7; hence 0 = (-1)*lim f1 .= lim f by A1,A2,Lm5,SEQ_2:8; end; registration let b,c,d; cluster rseq(0,b,c,d) -> convergent; coherence proof set f1 = rseq(0,1,c,d); A1: rseq(0,b,c,d) = b(#)f1 proof let n be Element of NAT; f1.n = (0*n+1)/(c*n+d)by Th5; hence (b(#)f1).n = (0*n+b)/(c*n+d) by VALUED_1:6 .= rseq(0,b,c,d).n by Th5; end; f1 is convergent by Lm6; hence thesis by A1; end; end; theorem lim(rseq(0,b,0,d)) = b/d proof thus lim(rseq(0,b,0,d)) = rseq(0,b,0,d).0 by SEQ_4:26 .= b/d by Th6; end; theorem Th10: for c being non zero Real holds lim(rseq(0,b,c,d)) = 0 proof let c be non zero Real; set f1 = rseq(0,1,c,d); A1: rseq(0,b,c,d) = b(#)f1 proof let n be Element of NAT; f1.n = (0*n+1)/(c*n+d) by Th5; hence (b(#)f1).n = (0*n+b)/(c*n+d) by VALUED_1:6 .= rseq(0,b,c,d).n by Th5; end; c < 0 or 0 < c; then lim f1 = 0 by Lm7,Lm8; hence 0 = b*lim f1 .= lim(rseq(0,b,c,d)) by A1,SEQ_2:8; end; Lm9: 0 < c implies for p st 0 < p ex n st for m st n <= m holds |.rseq(1,0,c,d).m-(1/c).| < p proof set f = rseq(1,0,c,d); assume A1: 0 < c; let p such that A2: 0 < p; set f1 = rseq(0,-d,c*c,c*d); lim f1 = 0 by A1,Th10; then consider n such that A3: for m st n <= m holds |.f1.m-0 .| < p by A2,SEQ_2:def 7; consider m1 being Nat such that A4: 0 < c*m1+d by A1,Th1; reconsider mm = max(m1,n+1) as Nat by TARSKI:1; take mm; let m such that A5: mm <= m; m1 <= mm by XXREAL_0:25; then m1 <= m by A5,XXREAL_0:2; then c*m1 <= c*m by A1,XREAL_1:64; then A6: c*m1+d <= c*m+d by XREAL_1:6; A7: n+0 <= n+1 by XREAL_1:6; n+1 <= mm by XXREAL_0:25; then n <= mm by A7,XXREAL_0:2; then A8: n <= m by A5,XXREAL_0:2; f.m-(1/c) = (1*m+0)/(c*m+d)-1/c by Th5 .= (m*c-1*(c*m+d))/((c*m+d)*c) by A1,A6,A4,XCMPLX_1:130 .= (0*m+-d)/(c*c*m+c*d) .= f1.m-0 by Th5; hence |.f.m-(1/c).| < p by A3,A8; end; Lm10: 0 < c implies rseq(1,0,c,d) is convergent proof assume A1: 0 < c; take 1/c; thus thesis by A1,Lm9; end; Lm11: 0 < c implies lim rseq(1,0,c,d) = 1/c proof assume A1: 0 < c; then A2: rseq(1,0,c,d) is convergent by Lm10; for p st 0 < p ex n st for m st n <= m holds |.rseq(1,0,c,d).m-1/c.| < p by A1,Lm9; hence thesis by A2,SEQ_2:def 7; end; Lm12: for c being non zero Real holds rseq(1,0,c,d) is convergent proof let c be non zero Real; per cases; suppose 0 < c; hence thesis by Lm10; end; suppose A1: c < 0; A2: rseq(1,0,c,d) = (-1)(#)rseq(1,0,-c,-d) by Th8; rseq(1,0,-c,-d) is convergent by A1,Lm10; hence thesis by A2; end; end; Lm13: for c being non zero Real holds lim rseq(1,0,c,d) = 1/c proof let c be non zero Real; per cases; suppose 0 < c; hence thesis by Lm11; end; suppose A1: c < 0; set f = rseq(1,0,c,d); set f1 = rseq(1,0,-c,-d); A2: f = (-1)(#)f1 by Th8; lim f1 = 1/-c by A1,Lm11; hence lim f = (-1)/-c by A2,A1,Lm10,SEQ_2:8 .= 1/c by XCMPLX_1:191; end; end; registration let c be non zero Real; let a,b,d; cluster rseq(a,b,c,d) -> convergent; coherence proof set f2 = rseq(1,0,c,d); set f3 = rseq(0,b,c,d); A1: rseq(a,b,c,d) = a(#)f2+f3 proof let n be Element of NAT; A2: f2.n = (1*n+0)/(c*n+d) by Th5; A3: f3.n = (0*n+b)/(c*n+d) by Th5; (a(#)f2).n = a*f2.n by VALUED_1:6; hence (a(#)f2+f3).n = a*f2.n+f3.n by VALUED_1:1 .= (a*n+b)/(c*n+d) by A2,A3 .= rseq(a,b,c,d).n by Th5; end; f2 is convergent by Lm12; hence thesis by A1; end; end; registration let a,d be positive Real; let b be Real; cluster rseq(a,b,0,d) -> non bounded_above; coherence proof let r; A1: r*d/d = r by XCMPLX_1:89; A2: (d*r-b)/a*a = d*r-b by XCMPLX_1:87; consider n such that A3: n > (d*r-b)/a by SEQ_4:3; take n; A4: rseq(a,b,0,d).n = (a*n+b)/(0*n+d) by Th5; a*n >= a*(d*r-b)/a by A2,A3,XREAL_1:64; then a*n+b >= d*r-b+b by A2,XREAL_1:6; hence thesis by A1,A4,XREAL_1:72; end; end; registration let a,d be negative Real; let b; cluster rseq(a,b,0,d) -> non bounded_above; coherence proof let r; A1: r*d/d = r by XCMPLX_1:89; A2: (d*r-b)/a*a = d*r-b by XCMPLX_1:87; consider n such that A3: n > (d*r-b)/a by SEQ_4:3; take n; A4: rseq(a,b,0,d).n = (a*n+b)/(0*n+d) by Th5; a*n <= a*(d*r-b)/a by A2,A3,XREAL_1:65; then a*n+b <= d*r-b+b by A2,XREAL_1:6; hence thesis by A1,A4,XREAL_1:73; end; end; registration let a be positive Real; let b; let d be negative Real; cluster rseq(a,b,0,d) -> non bounded_below; coherence proof let r; A1: r*d/d = r by XCMPLX_1:89; A2: (d*r-b)/a*a = d*r-b by XCMPLX_1:87; consider n such that A3: n > (d*r-b)/a by SEQ_4:3; take n; A4: rseq(a,b,0,d).n = (a*n+b)/(0*n+d) by Th5; a*n >= d*r-b by A2,A3,XREAL_1:64; then a*n+b >= d*r-b+b by XREAL_1:6; hence thesis by A1,A4,XREAL_1:73; end; end; registration let a be negative Real; let b; let d be positive Real; cluster rseq(a,b,0,d) -> non bounded_below; coherence proof let r; A1: r*d/d = r by XCMPLX_1:89; A2: (d*r-b)/a*a = d*r-b by XCMPLX_1:87; consider n such that A3: n > (d*r-b)/a by SEQ_4:3; take n; A4: rseq(a,b,0,d).n = (a*n+b)/(0*n+d) by Th5; a*n <= a*(d*r-b)/a by A2,A3,XREAL_1:65; then a*n+b <= d*r-b+b by A2,XREAL_1:6; hence thesis by A1,A4,XREAL_1:72; end; end; registration let a,d be non zero Real; let b; cluster rseq(a,b,0,d) -> non bounded; coherence proof (a is positive or a is negative) & (d is positive or d is negative); hence thesis; end; end; registration let a,d be non zero Real; let b; cluster rseq(a,b,0,d) -> non convergent; coherence; end; theorem Th11: for c being non zero Real holds lim(rseq(a,b,c,d)) = a/c proof let c be non zero Real; set f2 = rseq(1,0,c,d); set f3 = rseq(0,b,c,d); A1: rseq(a,b,c,d) = a(#)f2+f3 proof let n be Element of NAT; A2: f2.n = (1*n+0)/(c*n+d) by Th5; A3: f3.n = (0*n+b)/(c*n+d) by Th5; (a(#)f2).n = a*f2.n by VALUED_1:6; hence (a(#)f2+f3).n = a*f2.n+f3.n by VALUED_1:1 .= (a*n+b)/(c*n+d) by A2,A3 .= rseq(a,b,c,d).n by Th5; end; A4: lim f2 = 1/c by Lm13; A5: lim f3 = 0 by Th10; thus lim(rseq(a,b,c,d)) = lim(a(#)f2)+lim f3 by A1,SEQ_2:6 .= a/c by A4,A5,SEQ_2:8; end; theorem Th12: for a being non zero Real holds lim(rseq(a,b,a,d)) = 1 proof let a be non zero Real; thus lim(rseq(a,b,a,d)) = a/a by Th11 .= 1 by XCMPLX_1:60; end; begin :: Trigonometry theorem sin(PI*i) = 0 proof per cases; suppose i is even; then consider j being Integer such that A1: i = 2*j by INT_1:def 3,ABIAN:def 1; thus sin(PI*i) = sin(2*PI*j+0) by A1 .= 0 by SIN_COS:31,COMPLEX2:8; end; suppose i is odd; then consider j being Integer such that A2: i = 2*j+1 by ABIAN:1; thus sin(PI*i) = sin(2*PI*j+PI) by A2 .= 0 by SIN_COS:77,COMPLEX2:8; end; end; theorem Th14: cos(PI/2+PI*i) = 0 proof per cases; suppose i is even; then consider j being Integer such that A1: i = 2*j by INT_1:def 3,ABIAN:def 1; thus cos (PI/2+PI*i) = cos (PI/2+2*PI*j) by A1 .= cos (PI/2) by COMPLEX2:9 .= 0 by SIN_COS:76; end; suppose i is odd; then consider j being Integer such that A2: i = 2*j+1 by ABIAN:1; thus cos (PI/2+PI*i) = cos (PI+PI/2+2*PI*j) by A2 .= cos (PI+PI/2) by COMPLEX2:9 .= 0 by SIN_COS:76; end; end; theorem Th15: tan r = (cot r)" & cot r = (tan r)" proof thus tan r = (sin r*(cos r)")" " .= ((sin r)"*(cos r)" ")" by XCMPLX_1:204 .= (cot r)"; thus cot r = (cos r*(sin r)")" " .= ((cos r)"*(sin r)" ")" by XCMPLX_1:204 .= (tan r)"; end; theorem Th16: dom tan = union the set of all ]. -PI/2+PI*i,PI/2+PI*i .[ where i is Integer proof set S = the set of all ]. -PI/2+PI*i,PI/2+PI*i .[ where i is Integer; set T = dom tan; A1: dom sin = REAL & dom cos = REAL by FUNCT_2:def 1; then T = REAL/\(REAL\cos"{0}) by RFUNCT_1:def 1; then A2: T = REAL \cos"{0} by XBOOLE_1:28; thus T c= union S proof let x be object; assume A3: x in T; then reconsider x as Element of REAL; not x in cos"{0} by A2,A3,XBOOLE_0:def 5; then not cos x in {0} by A1,FUNCT_1:def 7; then A4: cos x <> 0 by TARSKI:def 1; set xP = (x-PI/2)/PI,E = [\xP/]; A5: ]. -PI/2+PI*(E+1),PI/2+PI*(E+1) .[ in S; xP*PI = x-PI/2 by XCMPLX_1:87; then A6: x = PI/2+xP*PI; then A7: E<>xP by Th14,A4; E <= xP < E+1 by INT_1:def 6,29; then E {}; then consider r being object such that A10: r in X /\ cos"{0} by XBOOLE_0:7; reconsider r as Element of REAL by A10; r in cos"{0} by A10,XBOOLE_0:def 4; then A11: cos.r in {0} by FUNCT_1:def 7; cos.r <> 0 proof A12: r in X by A10,XBOOLE_0:def 4; then A13: -PI/2+PI*i < r < PI/2+PI*i by A8,XXREAL_1:4; per cases; suppose i is even; then consider j being Integer such that A14: i= 2*j by INT_1:def 3,ABIAN:def 1; -PI/2 < r-PI*i < PI/2 by A13,XREAL_1:19,20; then r-PI*i in ]. -PI/2,PI/2.[ by XXREAL_1:4; then cos (r+2*PI*(-j)) >0 by A14,COMPTRIG:11; then cos r >0 by COMPLEX2:9; hence thesis; end; suppose i is odd; then consider j being Integer such that A15: i = 2*j+1 by ABIAN:1; -PI/2+PI+2*PI*j < r < PI/2+PI+2*PI* j by A12,A8,XXREAL_1:4,A15; then -PI/2+PI < r-2*PI*j < PI/2+PI by XREAL_1:19,20; then r-2*PI*j in ]. PI/2,3/2*PI.[ by XXREAL_1:4; then cos (r+2*PI*(-j)) <0 by COMPTRIG:13; then cos (r) <0 by COMPLEX2:9; hence thesis; end; end; hence contradiction by A11,TARSKI:def 1; end; X \ cos"{0} c= T by A8,A2,XBOOLE_1:33; hence thesis by A9,XBOOLE_0:def 7,XBOOLE_1:83; end; hence union S c= T by ZFMISC_1:76; end; registration cluster dom tan -> open for Subset of REAL; coherence proof set T = dom tan; for r being Element of REAL st r in T ex N be Neighbourhood of r st N c= T proof let r be Element of REAL; assume r in T; then consider X being set such that A1: r in X & X in the set of all ]. -PI/2+PI*i,PI/2+PI*i .[ where i is Integer by Th16,TARSKI:def 4; consider i being Integer such that A2: X = ]. -PI/2+PI*i,PI/2+PI*i .[ by A1; consider N being Neighbourhood of r such that A3: N c= X by A1,A2,RCOMP_1:18; X c= T by A1,Th16,ZFMISC_1:74; hence thesis by A3,XBOOLE_1:1; end; hence thesis by RCOMP_1:20; end; end; theorem Th17: 0 <= r implies sin.r <= r proof assume 0 <= r; then reconsider A = [.0,r.] as non empty closed_interval Subset of REAL by MEASURE5:def 3,XXREAL_1:1; A1: dom cos = REAL by FUNCT_2:def 1; then dom (cos|A)=A by RELAT_1:62; then cos|A is total by PARTFUN1:def 2; then reconsider cA=cos||A as Function of A,REAL; A2: cA|A is bounded & cA is integrable proof cos|A is continuous; hence thesis by INTEGRA5:def 1,INTEGRA5:11,10,A1; end; A3: integral(cA) = sin.r proof thus integral(cA) = integral(cos,A) by INTEGRA5:def 2 .= integral(cos,0,r) by INTEGRA5:19 .= sin.r - sin.0 by INTEGRA7:24 .= sin.r by SIN_COS:30; end; set Z0 = #Z 0; A4: dom Z0 = REAL by FUNCT_2:def 1; then dom (Z0|A)=A by RELAT_1:62; then Z0|A is total by PARTFUN1:def 2; then reconsider ZA = Z0||A as Function of A,REAL; A5: ZA|A is bounded & ZA is integrable proof Z0|A is continuous; hence thesis by A4,INTEGRA5:def 1,INTEGRA5:11,10; end; A6: integral(ZA) = r proof set Z1 = #Z 1; A7: (0+1)(#)Z0 = Z0 by RFUNCT_1:21; A8: Z1.r = r #Z 1 by TAYLOR_1:def 1 .= r by PREPOWER:35; A9: Z1.0 = 0 #Z 1 by TAYLOR_1:def 1 .= 0 by PREPOWER:35; thus integral(ZA) = integral(Z0,A) by INTEGRA5:def 2 .= integral(Z0,0,r) by INTEGRA5:19 .= Z1.r - Z1.0 by A7,INTEGRA7:30 .= r by A8,A9; end; for r st r in A holds cA.r <= ZA.r proof let r; assume A10: r in A; then ZA.r = Z0.r by FUNCT_1:49; then A11:ZA.r = r #Z 0 by TAYLOR_1:def 1 .= 1 by PREPOWER:34; cos r <= 1 by SIN_COS6:6; hence thesis by A11,A10,FUNCT_1:49; end; hence sin.r <= r by A2,A3,A5,A6,INTEGRA2:34; end; theorem Th18: 0 <= r < PI/2 implies r <= tan.r proof assume A1: 0 <= r < PI/2; then reconsider A=[.0,r.] as non empty closed_interval Subset of REAL by MEASURE5:def 3,XXREAL_1:1; A2: dom cos = REAL by FUNCT_2:def 1; set Z0=#Z 0; A3: dom Z0 = REAL by FUNCT_2:def 1; then dom (Z0|A)=A by RELAT_1:62; then Z0|A is total by PARTFUN1:def 2; then reconsider ZA=Z0||A as Function of A,REAL; A4: ZA|A is bounded & ZA is integrable proof Z0|A is continuous; hence thesis by INTEGRA5:def 1,INTEGRA5:11,10,A3; end; A5: integral(ZA) = r proof set Z1 = #Z 1; A6: (0+1)(#)Z0 = Z0 by RFUNCT_1:21; A7: Z1.r = r #Z 1 by TAYLOR_1:def 1 .= r by PREPOWER:35; A8: Z1.0 = 0 #Z 1 by TAYLOR_1:def 1 .= 0 by PREPOWER:35; thus integral(ZA) = integral(Z0,A) by INTEGRA5:def 2 .= integral(Z0,0,r) by INTEGRA5:19 .= Z1.r - Z1.0 by A6,INTEGRA7:30 .= r by A7,A8; end; set T = dom tan; dom sin = REAL by FUNCT_2:def 1; then T = REAL/\(dom cos \cos"{0}) by RFUNCT_1:def 1; then A9: T = REAL \ cos"{0} by A2,XBOOLE_1:28; set cc = cos(#)cos, ccT = cc|T, Z0ccT = Z0/ccT; dom cc = REAL by FUNCT_2:def 1; then A10: dom ccT = T by RELAT_1:62; then A11: T = dom ccT /\ dom Z0 by A3,XBOOLE_1:28; A12: A c= ].-PI/2,PI/2.[ by A1,XXREAL_1:47; then A13: A c= T by SIN_COS9:1; A14: ccT"{0} = {} proof assume ccT"{0} <> {}; then consider x being object such that A15: x in ccT"{0} by XBOOLE_0:def 1; reconsider x as Element of REAL by A15; A16: x in dom ccT & ccT.x in {0} by A15, FUNCT_1:def 7; then 0 = ccT.x by TARSKI:def 1 .= cc.x by A16,FUNCT_1:47 .= cos.x * cos.x by VALUED_1:5; then cos.x = 0; then cos.x in {0} by TARSKI:def 1; then x in cos"{0} by FUNCT_1:def 7,A2; hence contradiction by A9,A10,A16,XBOOLE_0:def 5; end; then dom ccT\ccT"{0} = dom ccT; then A17: T = dom Z0ccT by A11,RFUNCT_1:def 1; then dom (Z0ccT|A) = A by A13,RELAT_1:62; then Z0ccT|A|A is total & Z0ccT|A|A= Z0ccT|A by PARTFUN1:def 2; then reconsider Z0ccTA = Z0ccT||A as Function of A,REAL; A18: Z0ccT | A is continuous & Z0ccTA|A is bounded & Z0ccTA is integrable proof A19: A c= dom Z0/\dom ccT by A10,A13,A3,XBOOLE_1:28; A20: ccT|A is continuous; Z0|A is continuous; then Z0ccT | A is continuous by A19,FCONT_1:24,A20,A14; hence thesis by INTEGRA5:def 1,INTEGRA5:11,10,A17,A13; end; A21: for s be Real st s in T holds Z0ccT.s = 1/(cos.s)^2 & cos.s <> 0 proof let s be Real such that A22: s in T; A23: Z0.s = s #Z 0 by TAYLOR_1:def 1 .= 1 by PREPOWER:34; ccT.s = cc.s by A22,A10,FUNCT_1:47 .= (cos.s)^2 by VALUED_1:5; hence Z0ccT.s = 1 /(cos.s)^2 by A23,RFUNCT_1:def 1,A22,A17; A24: s in REAL by XREAL_0:def 1; assume cos.s=0; then cos.s in {0} by TARSKI:def 1; then s in cos"{0} by FUNCT_1:def 7,A2,A24; hence thesis by A22, A9,XBOOLE_0:def 5; end; A25: integral(Z0ccTA) = tan.r proof A26: upper_bound A = r & lower_bound A =0 by A1,JORDAN5A:19; thus integral(Z0ccTA) = integral(Z0ccT,A) by INTEGRA5:def 2 .= tan.r-tan.0 by A13,A17,A21,A18,A26,INTEGRA8:59 .= tan.r by SIN_COS9:41; end; for r st r in A holds ZA.r <= Z0ccTA.r proof let r; assume A27: r in A; then A28: Z0ccTA.r = Z0ccT.r & ZA.r = Z0.r by FUNCT_1:49; then A29: ZA.r = r #Z 0 by TAYLOR_1:def 1 .= 1 by PREPOWER:34; A30: Z0ccTA.r = 1/(cos.r)^2 by A28,A27,A21,A13; A31: cos r >0 by A27,A12,COMPTRIG:11; cos r <= 1 & cos.r=cos r by SIN_COS6:6; then (cos.r)^2 <= 1^2 & (cos.r)^2 >0 by XREAL_1:66,A31; then 1" <= ((cos.r)^2)" by XREAL_1:85; hence thesis by A29,A30; end; hence r <= tan.r by A4,A5,A18,A25,INTEGRA2:34; end; begin :: Some special functions and sequences definition let f be real-valued Function; func cot(f) -> Function means :Def3: dom it = dom f & for x being object st x in dom f holds it.x = cot(f.x); existence proof deffunc F(object) = cot(f.$1); thus ex g being Function st dom g = dom f & for x being object st x in dom f holds g.x = F(x) from FUNCT_1:sch 3; end; uniqueness proof let g,h be Function such that A1: dom g = dom f and A2: for x being object st x in dom f holds g.x = cot(f.x) and A3: dom h = dom f and A4: for x being object st x in dom f holds h.x = cot(f.x); thus dom g = dom h by A1,A3; let x be object such that A5: x in dom g; thus g.x = cot(f.x) by A1,A2,A5 .= h.x by A1,A4,A5; end; func cosec(f) -> Function means :Def4: dom it = dom f & for x being object st x in dom f holds it.x = cosec(f.x); existence proof deffunc F(object) = cosec(f.\$1); thus ex g being Function st dom g = dom f & for x being object st x in dom f holds g.x = F(x) from FUNCT_1:sch 3; end; uniqueness proof let g,h be Function such that A6: dom g = dom f and A7: for x being object st x in dom f holds g.x = cosec(f.x) and A8: dom h = dom f and A9: for x being object st x in dom f holds h.x = cosec(f.x); thus dom g = dom h by A6,A8; let x be object such that A10: x in dom g; thus g.x = cosec(f.x) by A6,A7,A10 .= h.x by A6,A9,A10; end; end; registration let f be real-valued Function; cluster cot(f) -> REAL-valued; coherence proof set g = cot(f); thus rng g c= REAL proof let y be object; assume y in rng g; then consider x being object such that A1: x in dom g and A2: y = g.x by FUNCT_1:def 3; dom g = dom f by Def3; then g.x = cot(f.x) by A1,Def3; hence thesis by A2,XREAL_0:def 1; end; end; cluster cosec(f) -> REAL-valued; coherence proof set g = cosec(f); thus rng g c= REAL proof let y be object; assume y in rng g; then consider x being object such that A3: x in dom g and A4: y = g.x by FUNCT_1:def 3; dom g = dom f by Def4; then g.x = cosec(f.x) by A3,Def4; hence thesis by A4,XREAL_0:def 1; end; end; end; registration let f be real-valued FinSequence; cluster cot(f) -> FinSequence-like; coherence proof dom cot f = dom f by Def3; hence thesis by Lm1; end; cluster cosec(f) -> FinSequence-like; coherence proof dom cosec f = dom f by Def4; hence thesis by Lm1; end; end; theorem Lm14: for f being real-valued FinSequence holds len cot f = len f proof let f be real-valued FinSequence; dom cot f = dom f by Def3; hence thesis by FINSEQ_3:29; end; theorem Lm15: for f being real-valued FinSequence holds len cosec f = len f proof let f be real-valued FinSequence; dom cosec f = dom f by Def4; hence thesis by FINSEQ_3:29; end; registration let f be real-valued FinSequence; cluster cot(f) -> len f-element; coherence proof dom cot f = dom f by Def3; hence len cot(f) = len f by FINSEQ_3:29; end; cluster cosec(f) -> len f-element; coherence proof dom cosec f = dom f by Def4; hence len cosec(f) = len f by FINSEQ_3:29; end; end; Lm16: rseq(0,1,1,0).n = 1/n proof thus rseq(0,1,1,0).n = (0*n+1)/(1*n+0) by Th5 .= 1/n; end; Lm17: lim rseq(2,0,2,1) = 1 by Th12; Lm18: lim rseq(2,-1,2,1) = 1 by Th12; Lm19: lim rseq(2,2,2,1) = 1 by Th12; definition let m; func x_r-seq(m) -> FinSequence equals (PI/(2*m+1))(#)(idseq m); coherence; end; theorem Th19: len (x_r-seq m) = m & for k st 1 <= k <= m holds x_r-seq(m).k = k*PI/(2*m+1) proof A1: dom (x_r-seq m) = dom (idseq m) by VALUED_1:def 5; hence len (x_r-seq m)=m by FINSEQ_3:29; let k;assume 1 <= k <= m; then k in dom (x_r-seq m) & k in Seg m by A1,FINSEQ_3:25; then (x_r-seq m).k = (PI/(2*m+1)) * ((idseq m).k) & (idseq m).k = k by VALUED_1:def 5,FINSEQ_2:49; hence thesis; end; theorem Th20: rng x_r-seq(m) c= ].0,PI/2.[ proof set f = x_r-seq(m); let y be object; assume y in rng f; then consider n such that A1: 1 <= n and A2: n <= len f and A3: y = f.n by Lm2; A4: len f = m by Th19; then A5: f.n = n*PI/(2*m+1) by A1,A2,Th19; 2*n <= 2*m by A2,A4,XREAL_1:64; then 2*n+1 <= 2*m+1 by XREAL_1:6; then A6: n*PI/(2*n+1) >= n*PI/(2*m+1) by XREAL_1:118; A7: ((2*n+1)*n")" = (2*n+1)"*n" " by XCMPLX_1:204; A8: 2*n/n = 2 by A1,XCMPLX_1:89; 2+1/n > 2+0 by A1,XREAL_1:8; then ((2*n+1)*n")" < (2*1")" by A8,XREAL_1:88; then PI*(n/(2*n+1)) < PI*(1/2) by A7,XREAL_1:68; then n*PI/(2*m+1) < PI/2 by A6,XXREAL_0:2; hence thesis by A1,A3,A5,XXREAL_1:4; end; registration let m; cluster x_r-seq(m) -> REAL-valued; coherence proof rng x_r-seq(m) c= ].0,PI/2.[ by Th20; hence rng x_r-seq(m) c= REAL by XBOOLE_1:1; end; end; theorem Th21: 1 <= k <= m implies 0 < x_r-seq(m).k < PI/2 proof set f = x_r-seq(m); A1: rng f c= ].0,PI/2.[ by Th20; A2: len f = m by Th19; assume 1 <= k <= m; then k in dom f by A2,FINSEQ_3:25; then f.k in rng f by FUNCT_1:def 3; hence thesis by A1,XXREAL_1:4; end; registration cluster x_r-seq(0) -> empty; coherence; end; theorem 1 <= k <= m implies 2/(k*PI) + (x_r-seq(m))".k = (x_r-seq(m+1))".k proof assume that A1: 1 <= k and A2: k <= m; set f = x_r-seq(m); set g = x_r-seq(m+1); m+0 <= m+1 by XREAL_1:6; then k <= m+1 by A2,XXREAL_0:2; then A3: g.k = k*PI/(2*(m+1)+1) by A1,Th19; f.k = k*PI/(2*m+1) by A1,A2,Th19; then (2*m+1)/(k*PI) = (f.k)" by XCMPLX_1:213 .= f".k by VALUED_1:10; hence 2/(k*PI) + f".k = (2*(m+1)+1)/(k*PI) .= (g.k)" by A3,XCMPLX_1:213 .= g".k by VALUED_1:10; end; theorem 1 <= k <= m implies (2*m+1)*x_r-seq(m).k = k*PI proof assume 1 <= k <= m; then A1: x_r-seq(m).k = k*PI/(2*m+1) by Th19; (2*m+1)*(k*PI)/(2*m+1) = k*PI by XCMPLX_1:89; hence thesis by A1; end; theorem sqr cosec x_r-seq(m) = 1 + sqr cot x_r-seq(m) proof set f = x_r-seq(m); A1: len sqr cosec f = len cosec f by CARD_1:def 7; A2: len cosec f = len f by CARD_1:def 7; A3: len f = m by Th19; A4: len(1 + sqr cot x_r-seq(m)) = len sqr cot x_r-seq(m) by CARD_1:def 7; A5: len sqr cot x_r-seq(m) = len cot x_r-seq(m) by CARD_1:def 7; A6: len cot x_r-seq(m) = len x_r-seq(m) by CARD_1:def 7; thus len sqr cosec f = len(1 + sqr cot x_r-seq(m)) by A1,A2,A4,A5,CARD_1:def 7; let k such that A7: 1 <= k and A8: k <= len sqr cosec f; A9: k in dom f by A1,A2,A7,A8,FINSEQ_3:25; then A10: (cosec f).k = cosec(f.k) by Def4; A11: (sqr cot f).k = ((cot f).k)^2 by VALUED_1:11; A12: (cot f).k = cot(f.k) by A9,Def3; A13: 0 < f.k by A1,A2,A3,A7,A8,Th21; A14: f.k < PI/2 by A1,A2,A3,A7,A8,Th21; PI/2 < PI/1 by XREAL_1:76; then f.k < PI by A14,XXREAL_0:2; then f.k in ].0,PI.[ by A13,XXREAL_1:4; then sin(f.k) <> 0 by COMPTRIG:7; then A15: (cosec(f.k))^2 = 1+(cot(f.k))^2 by SIN_COS5:14; k in dom (1 + sqr cot f) by A1,A2,A4,A5,A6,A7,A8,FINSEQ_3:25; hence (1 + sqr cot f).k = ((cosec f).k)^2 by A10,A11,A12,A15,VALUED_1:def 2 .= (sqr cosec f).k by VALUED_1:11; end; theorem Th25: x_r-seq(n) is one-to-one proof set f= x_r-seq(n); let x1,x2 be object such that A1: x1 in dom f & x2 in dom f & f.x1=f.x2; reconsider x1,x2 as Nat by A1; len f=n by Th19;then 1 <= x1 <= n & 1<= x2 <= n by A1,FINSEQ_3:25; then A2: f.x1= x1*PI/(2*n+1) & f.x2 = x2 *PI/(2*n+1) by Th19; x1*PI=x2 *PI by A1,A2,XCMPLX_1:53; hence thesis by XCMPLX_1:5; end; theorem sqr cot x_r-seq(n) is one-to-one proof set f = x_r-seq(n); A1:f is one-to-one by Th25; let x1,x2 be object such that A2:x1 in dom sqr cot f & x2 in dom sqr cot f & (sqr cot f).x1 = (sqr cot f).x2; reconsider x1,x2 as Nat by A2; A3:len sqr cot f = len cot f = len f =n by CARD_1:def 7; then A4: dom sqr cot f = dom cot f = dom f by FINSEQ_3:29; 1<=x1 <= n & 1<= x2 <=n by FINSEQ_3:25,A3,A2; then A5: 0 < f.x1 < PI/2 & 0 < f.x2 < PI/2 & PI/2 < PI by Th21,COMPTRIG:5; then f.x1 < PI & f.x2 < PI by XXREAL_0:2; then A6: f.x1 in ].0,PI.[ & f.x2 in ].0,PI.[ & f.x1 in ].0,PI/2.[ & f.x2 in ].0,PI/2.[ by A5,XXREAL_1:4; then A7:sin (f.x1) >0 & sin (f.x2) >0 & cos(f.x1) >0 & cos (f.x2) >0 by COMPTRIG:7,SIN_COS:80; A8: (cot f).x1 = cot (f.x1) & (cot f).x2 = cot (f.x2) by Def3,A2,A4; A9: cot (f.x1) = cot (f.x2) proof (sqr cot f).x1 = ((cot f).x1)^2 & (sqr cot f).x2 = ((cot f).x2)^2 by VALUED_1:11; then (cot f).x1 = (cot f).x2 or (cot f).x1 = - (cot f).x2 by A2,SQUARE_1:40; hence thesis by A7,A8; end; f.x1=f.x2 proof A10: cot.(f.x1) = cot (f.x1) & cot.(f.x2) = cot (f.x2) by A6,SIN_COS9:2,RFUNCT_1:def 1; A11: f.x1 in dom (cot| ].0,PI.[) & f.x2 in dom (cot| ].0,PI.[) by A6,SIN_COS9:2,RELAT_1:57; then cot.(f.x1) = (cot| ].0,PI.[).(f.x1) & cot.(f.x2) = (cot| ].0,PI.[).(f.x2) by FUNCT_1:47; hence thesis by A9,A10,A11,FUNCT_1:def 4,SIN_COS9:10; end; hence thesis by A1,A2,A4,FUNCT_1:def 4; end; theorem Sum sqr cot x_r-seq(m) <= Sum ((sqr x_r-seq(m))") proof set f = x_r-seq(m); set f1 = sqr cot f; set f2 = (sqr f)"; A1: len f = m by Th19; A2: len cot f = len f by Lm14; A3: len sqr f = len f by RVSUM_1:143; now let n; assume n in Seg m; then A4: 1 <= n & n <= m by FINSEQ_1:1; then A5: n in dom f by A1,FINSEQ_3:25; A6: f1.n = ((cot f).n)^2 by VALUED_1:11; A7: (cot f).n = cot(f.n) by A5,Def3; A8: f2.n = ((sqr f).n)" by VALUED_1:10; A9: (sqr f).n = (f.n)^2 by VALUED_1:11; A10: (tan(f.n))" = cot(f.n) by Th15; A11: f.n < PI/2 by A4,Th21; A12: 0 < f.n by A4,Th21; then A13: f.n in ]. -PI/2+PI*0,PI/2+PI*0 .[ by A11,XXREAL_1:4; ]. -PI/2+PI*0,PI/2+PI*0 .[ in the set of all ]. -PI/2+PI*i,PI/2+PI*i .[ where i is Integer; then f.n in dom tan by A13,Th16,TARSKI:def 4; then tan.(f.n) = tan(f.n) by RFUNCT_1:def 1; then A14: ((tan.(f.n))^2)" = (cot(f.n))^2 by A10,XCMPLX_1:204; f.n <= tan.(f.n) by A4,A12,Th18,Th21; then (f.n)^2 <= (tan.(f.n))^2 by A12,XREAL_1:66; hence f1.n <= f2.n by A6,A7,A8,A9,A12,A14,XREAL_1:85; end; hence thesis by A1,A2,A3,RVSUM_1:82; end; theorem Sum ((sqr x_r-seq(m))") <= Sum sqr cosec x_r-seq(m) proof set f = x_r-seq(m); set f1 = sqr cosec f; set f2 = (sqr f)"; A1: len f = m by Th19; A2: len cosec f = len f by Lm15; A3: len sqr f = len f by RVSUM_1:143; now let n; assume n in Seg m; then A4: 1 <= n & n <= m by FINSEQ_1:1; then A5: n in dom f by A1,FINSEQ_3:25; A6: f1.n = ((cosec f).n)^2 by VALUED_1:11; A7: (cosec f).n = cosec(f.n) by A5,Def4; A8: f2.n = ((sqr f).n)" by VALUED_1:10; A9: (sqr f).n = (f.n)^2 by VALUED_1:11; A10: f.n < PI/2 by A4,Th21; A11: 0 < f.n by A4,Th21; A12: ((sin.(f.n))^2)" = (cosec(f.n))^2 by XCMPLX_1:204; PI/2 < PI/1 by XREAL_1:76; then f.n < PI by A10,XXREAL_0:2; then f.n in ].0,PI.[ by A11,XXREAL_1:4; then A13: 0 < sin(f.n) by COMPTRIG:7; sin.(f.n) <= f.n by A11,Th17; then (sin.(f.n))^2 <= (f.n)^2 by A13,XREAL_1:66; hence f2.n <= f1.n by A6,A7,A8,A9,A12,A13,XREAL_1:85; end; hence thesis by A1,A2,A3,RVSUM_1:82; end; definition func Basel-seq -> Real_Sequence equals rseq(0,1,1,0) (#) rseq(0,1,1,0); coherence; func Basel-seq1 -> Real_Sequence equals (PI^2/6) (#) rseq(2,0,2,1) (#) rseq(2,-1,2,1); coherence; func Basel-seq2 -> Real_Sequence equals (PI^2/6) (#) rseq(2,0,2,1) (#) rseq(2,2,2,1); coherence; end; theorem Th29: Basel-seq.n = 1 / (n^2) proof rseq(0,1,1,0).n = 1/n by Lm16; hence Basel-seq.n = (1/n)*(1/n) by VALUED_1:5 .= (1*1)/(n*n) by XCMPLX_1:76 .= 1 / (n^2); end; theorem Basel-seq1.n = (PI^2/6) * (2*n/(2*n+1)) * ((2*n-1)/(2*n+1)) proof A1: (p(#)rseq(2,0,2,1)).n = p*rseq(2,0,2,1).n by VALUED_1:6; rseq(2,0,2,1).n = (2*n+0)/(2*n+1) & rseq(2,-1,2,1).n = (2*n-1)/(2*n+1) by Th5; hence thesis by A1,VALUED_1:5; end; theorem Basel-seq2.n = (PI^2/6) * (2*n/(2*n+1)) * ((2*n+2)/(2*n+1)) proof A1: (p(#)rseq(2,0,2,1)).n = p*rseq(2,0,2,1).n by VALUED_1:6; rseq(2,0,2,1).n = (2*n+0)/(2*n+1) & rseq(2,2,2,1).n = (2*n+2)/(2*n+1) by Th5; hence thesis by A1,VALUED_1:5; end; registration cluster Basel-seq -> convergent; coherence; cluster Basel-seq1 -> convergent; coherence; cluster Basel-seq2 -> convergent; coherence; end; theorem lim Basel-seq1 = PI^2/6 = lim Basel-seq2 proof lim(p(#)rseq(2,0,2,1)) = p*lim(rseq(2,0,2,1)) by SEQ_2:8; hence lim Basel-seq1 = PI^2/6 by Lm17,Lm18,SEQ_2:15; lim(p(#)rseq(2,0,2,1)) = p*lim(rseq(2,0,2,1)) by SEQ_2:8; hence thesis by Lm17,Lm19,SEQ_2:15; end; theorem Sum ((sqr x_r-seq(m))") = (2*m+1)^2 / (PI^2) * Sum(Basel-seq,m) proof set a = PI^2; set b = (2*m+1)^2; set B = Basel-seq; set S = Shift(B|Segm(m+1),1); set M = x_r-seq(m); set G = (sqr M)"; set F = <*0*>^G; A1: B.0 = 1/(0^2) by Th29; A2: Sum(B,m) = Sum(S) by DBLSEQ_2:49; A3: dom S = Seg(m+1) by DBLSEQ_2:45; A4: len(G) = len(sqr M) by Lm3 .= len(M) by CARD_1:def 7 .= m by Th19; A5: len F = len <*0*> + len G by FINSEQ_1:22; A6: len <*0*> = 1 by FINSEQ_1:39; A7: F = b/a(#)S proof thus len(F) = len(S) by A4,A5,A6,A3,FINSEQ_1:def 3 .= len(b/a(#)S) by COMPLSP2:3; let k such that A8: 1 <= k and A9: k <= len(F); A10: (b/a(#)S).k = b/a*(S.k) by VALUED_1:6; per cases by A8,XXREAL_0:1; suppose A11: k = 1; 1 <= m+1 by NAT_1:11; then 0+1 in dom S by A3; then S.(0+1) = B.0 by DBLSEQ_2:47; hence (b/a(#)S).k = F.k by A1,A10,A11; end; suppose A12: 1 < k; reconsider s = k-1 as Nat by A8; A13: k = s+1; k in dom S by A3,A4,A5,A6,A8,A9; then A14: S.k = B.s by A13,DBLSEQ_2:47 .= 1/(s^2) by Th29; A15: (sqr M).s = (M.s)^2 by VALUED_1:11; 1-1 < s by A12,XREAL_1:8; then A16: 1 <= s by NAT_1:14; s <= m+1-1 by A4,A5,A6,A9,XREAL_1:9; then A17: M.s = s*PI/(2*m+1) by A16,Th19; thus F.k = G.s by A6,A9,A12,FINSEQ_1:24 .= ((sqr M).s)" by VALUED_1:10 .= ((s*PI)^2 / (2*m+1)^2)" by A15,A17,XCMPLX_1:76 .= ((2*m+1)^2)*1 / ((PI^2)*(k-1)^2) by XCMPLX_1:213 .= b/a*(S.k) by A14,XCMPLX_1:76 .= (b/a(#)S).k by VALUED_1:6; end; end; Sum F = 0 + Sum G by RVSUM_1:76; hence thesis by A2,A7,RVSUM_1:87; end;