:: Basel Problem -- Preliminaries
:: by Artur Korni{\l}owicz and Karol P\kak
::
:: Received June 27, 2017
:: Copyright (c) 2017-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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;
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<p;
then consider n such that
A2: for m st n <= m holds |.f.m-0 .| < p by A1,Lm4;
take n;
thus thesis by A2;
end;
Lm6:
rseq(0,1,c,d) is convergent
proof
set f = rseq(0,1,c,d);
per cases;
suppose c = 0;
hence thesis;
end;
suppose c > 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 <xP <E+1 by A7,XXREAL_0:1;
then E*PI < xP*PI < (E+1)*PI by XREAL_1:68;
then PI/2 + E*PI < x < PI/2+(E+1)*PI by A6,XREAL_1:6;
then x in ]. -PI/2+PI*(E+1),PI/2+PI*(E+1) .[ by XXREAL_1:4;
hence thesis by A5,TARSKI:def 4;
end;
for X being set st X in S holds X c= T
proof
let X be set;
assume X in S;
then consider i being Integer such that
A8: X = ]. -PI/2+PI*i,PI/2+PI*i .[;
A9: X /\ cos"{0} = {}
proof
assume X /\ cos"{0} <> {};
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;
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;