:: Formalization of Wallis Infinite Product Formula for $\pi$ and the Wallis
:: Integral
:: by Yasushige Watase
::
:: Received September 17, 2025
:: Copyright (c) 2025-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 4.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/4.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, INTEGRA1, FINSEQ_1, ORDINAL4, CARD_3,
ARYTM_1, ARYTM_3, RELAT_1, FUNCT_1, XXREAL_0, NAT_1, XBOOLE_0, VALUED_1,
TARSKI, XXREAL_2, ORDINAL2, CARD_1, FDIFF_1, XXREAL_1, RCOMP_1, INTEGRA5,
MEASURE5, SIN_COS, GROUP_1, FUNCT_2, FUNCSDOM, XCMPLX_0, SEQ_2, QC_LANG1,
NEWTON, RLVECT_1, SUPINF_2, FUNCOP_1, MESFUNC1, BINOP_1, INTEGRA7, POWER,
PARTFUN3, SEQ_1, COMPLEX1, ASYMPT_1, SQUARE_1, REALSET1, ALGSTR_0,
WALLIS01;
notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2,
BINOP_1, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1,
SQUARE_1, NAT_1, VALUED_0, COMPLEX1, NAT_D, FINSEQ_1, VALUED_1, SEQ_1,
SEQ_2, RVSUM_1, NEWTON, RCOMP_1, FCONT_1, FDIFF_1, POWER, MEASURE5,
SIN_COS, PARTFUN3, INTEGRA5, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1,
FUNCSDOM, BINOM, INTEGRA7;
constructors RELSET_1, REAL_1, SQUARE_1, NAT_D, SEQ_1, COMSEQ_2, FINSEQ_3,
SEQ_2, RVSUM_1, NEWTON, ABIAN, PARTFUN3, VECTSP_1, FUNCSDOM, RCOMP_1,
FCONT_1, FDIFF_1, POWER, SIN_COS, BINOM, INTEGRA5, INTEGRA7;
registrations RELAT_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, RCOMP_1,
VALUED_0, VALUED_1, FUNCT_2, CARD_1, SEQ_2, RELSET_1, MEASURE5, RVSUM_1,
ORDINAL1, FUNCT_1, NAT_1, INT_1, FDIFF_1, NEWTON04, XCMPLX_0, NEWTON,
SIN_COS, RVSUM_4, FUNCSDOM, VECTSP_1, FCONT_1, SQUARE_1, POWER, VECTSP_2,
ABIAN, ABSVALUE, PARTFUN3, NUMPOLY1, FINSEQ_9, FOMODEL0, GROUP_1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities VALUED_1, RLVECT_1, STRUCT_0, ALGSTR_0, FUNCOP_1, SQUARE_1,
XCMPLX_0, FUNCSDOM, FINSEQ_1, XBOOLE_0, SEQ_1;
expansions RLVECT_1, FUNCT_2, TARSKI, FUNCT_1, SEQ_2;
theorems SEQ_4, RFUNCT_1, FUNCT_1, FINSEQ_1, RVSUM_1, SEQ_1, SEQ_2, ABSVALUE,
NAT_1, FINSEQ_2, RCOMP_1, FDIFF_2, XREAL_0, FUNCT_2, XCMPLX_1, XREAL_1,
XXREAL_0, ORDINAL1, VALUED_1, XXREAL_1, INT_1, SIN_COS, FUNCSDOM, BINOM,
FUNCOP_1, FINANCE2, INTEGRA5, COMPTRIG, INTEGRA6, INTEGRA7, INTEGRA8,
NUMBERS, PDLAX, POLYEQ_5, SQUARE_1, NEWTON, VECTSP_2, RLVECT_1, FINSEQ_3,
SEQM_3, WSIERP_1, VALUED_0, POWER, ORDEQ_01, FINSEQ_5, PARTFUN3,
COMPLEX1;
schemes FINSEQ_1, NAT_1, SEQ_1, NUMPOLY1;
begin :: Preliminaries
Lm11:
for seq be positive-yielding Real_Sequence holds
for k be Nat holds seq.k > 0
proof
let seq be positive-yielding Real_Sequence;
let k be Nat;
dom seq = NAT by FUNCT_2:def 1; then
seq.k in rng seq by FUNCT_1:3,ORDINAL1:def 12;
hence thesis;
end;
Lm9:
for n be Nat holds
1/PI - 1/((1+1/(2*(n+1)))*PI) > 0 &
(1+1/(2*(n+1)))*PI > 0 & 1/((1+1/(2*(n+1)))*PI) > 0
proof
let n be Nat;
set s = (1+1/(2*(n+1)))*PI;
(1+1/(2*(n+1)))*PI = PI + (1/(2*(n+1)))*PI; then
1*PI < 1*s by COMPTRIG:5,XREAL_1:39; then
1/s < 1/PI by COMPTRIG:5,XREAL_1:106;
hence thesis by COMPTRIG:5,XREAL_1:50;
end;
theorem Th39:
for n be Nat, x be Real st 0 < x < PI/2 holds 0 < sin.x < 1
proof
let n be Nat, x be Real;
assume
A1: 0 < x < PI/2;
reconsider t = sin.x as Real;
x < PI by A1,XXREAL_0:2,COMPTRIG:5; then
A2: x in ].0,PI.[ by A1,XXREAL_1:4;
A3: x in ].-PI/2,PI/2.[ by A1,XXREAL_1:4; then
A5: x in [.-PI/2,PI/2.] by XXREAL_1:16;
A4: dom sin = REAL by FUNCT_2:def 1; then
A6: x in dom (sin|[.-PI/2,PI/2.]) by XXREAL_1:16,A3;
A7: PI/2 in dom (sin|[.-PI/2,PI/2.]) by A4,XXREAL_1:1,COMPTRIG:5;
reconsider x1 = x, x2 = PI/2 as ExtReal;
sin.x1 = (sin|[.-PI/2,PI/2.] ).x1 &
sin.x2 = (sin|[.-PI/2,PI/2.] ).x2
by A5,COMPTRIG:5,XXREAL_1:1,FUNCT_1:49;
hence thesis by A2,A1,A6,A7,COMPTRIG:7,23,VALUED_0:def 13,SIN_COS:76;
end;
theorem Th40:
for n,m be Nat, x be Real st n < m & 0 < x < 1 holds x|^m < x|^n
proof
let n,m be Nat, x be Real;
assume n < m & 0 < x < 1; then
x to_power n > x to_power m by POWER:40;
hence thesis;
end;
theorem Th41:
for n be non zero Nat, x be Real st 0 < x < PI/2 holds
(sin.x)|^(2*n) < (sin.x)|^(2*n-'1) &
(sin.x)|^(2*n+1) < (sin.x)|^(2*n)
proof
let n be non zero Nat, x be Real;
assume 0 < x < PI/2; then
A2: 0 < sin.x < 1 by Th39;
0 < 0+n; then
1 <= n by NAT_1:19; then
2*n >= 2*1 by XREAL_1:64; then
2*n > 1 by XXREAL_0:2; then
A3: 2*n-'1 < 2*n by XREAL_1:237;
2*n < 2*n +1 by XREAL_1:39;
hence thesis by A3,A2,Th40;
end;
begin
::::::::::::::::::::::::::::::::::::::
:: 1. Some results on double factorial
::::::::::::::::::::::::::::::::::::::
definition
let m be Nat;
func even-seq m -> FinSequence of INT means :Def1:
len it = m & for i be Nat st i in dom it holds it.i = 2*i;
existence
proof
deffunc F(Nat) = 2*$1;
consider z being FinSequence such that
A1: len z = m & for k being Nat st k in dom z holds z.k = F(k)
from FINSEQ_1:sch 2;
take z;
z is FinSequence of INT
proof
A2: for y be object st y in rng z holds y in INT
proof
let y be object;
assume y in rng z; then
consider i be object such that
A3: i in dom z and
A4: y = z.i by FUNCT_1:def 3;
dom z = Seg m by A1,FINSEQ_1:def 3; then
consider i0 be Nat such that
A5: i0 = i and 1 <= i0 and i0 <= m by A3;
reconsider i as Nat by A5;
z.i = 2*i by A1,A3;
hence thesis by A4,INT_1:def 2;
end;
rng z c= INT by A2;
hence thesis by FINSEQ_1:def 4;
end;
hence thesis by A1;
end;
uniqueness
proof
let z1,z2 be FinSequence of INT such that
A7: len z1 = m and
A8: for i be Nat st i in dom z1 holds z1.i = 2*i and
A9: len z2 = m and
A10:for j be Nat st j in dom z2 holds z2.j = 2*j;
A11:dom z1 = Seg len z1 by FINSEQ_1:def 3.= dom z2 by A7,A9,FINSEQ_1:def 3;
for x be Nat st x in dom z1 holds z1.x = z2.x
proof
let x be Nat;
assume
A12: x in dom z1;
hence z1.x = 2*x by A8
.= z2.x by A10,A11,A12;
end;
hence thesis by A11;
end;
end;
definition
let m be non zero Nat;
func odd-seq m -> FinSequence of INT equals
even-seq(m) + ((dom even-seq m) --> -1);
coherence
proof
set h = even-seq(m) + ((dom even-seq m) --> -1);
dom h = (dom even-seq m) /\ dom ((dom even-seq m) --> -1)
by VALUED_1:def 1
.= dom even-seq m; then
A1: dom h = Seg len even-seq m by FINSEQ_1:def 3 .= Seg m by Def1;
A2: rng h c= INT by INT_1:def 2;
h is FinSequence by A1,FINSEQ_1:def 2;
hence thesis by A2,FINSEQ_1:def 4;
end;
end;
theorem Th1:
for n be non zero Nat holds dom even-seq n = Seg n &
dom odd-seq n = Seg n &
len odd-seq n = n & len even-seq n = n
proof
let n be non zero Nat;
A1: dom even-seq n = Seg len even-seq n by FINSEQ_1:def 3
.= Seg(n) by Def1;
set h = even-seq(n) + ((dom even-seq n) --> -1);
dom h = (dom even-seq n) /\ dom ((dom even-seq n) --> -1)
by VALUED_1:def 1
.= dom even-seq n; then
A2: dom h = Seg len even-seq n by FINSEQ_1:def 3 .= Seg n by Def1;
len odd-seq n = len even-seq n by A1,A2,FINSEQ_3:29 .= n by Def1;
hence thesis by Def1,A1,A2;
end;
theorem Th2:
for n be non zero Nat holds
for i be Nat st i in dom odd-seq n holds (odd-seq n).i = 2*i -1
proof
let n be non zero Nat;
let i be Nat;
assume
A1: i in dom odd-seq n; then
i in Seg n by Th1; then
a2: i in dom even-seq n by Th1; then
A3: ((dom even-seq n) --> -1).i = -1 by FUNCOP_1:7;
(odd-seq n).i
= (even-seq n).i +((dom(even-seq n) --> -1)).i by A1,VALUED_1:def 1
.= 2*i -1 by a2,Def1,A3;
hence thesis;
end;
Lm1:
for n be non zero Nat holds even-seq n is positive-yielding
proof
let n be non zero Nat;
for r being Real st r in rng even-seq n holds 0 < r
proof
let r be Real;
assume r in rng even-seq n; then
consider x be object such that
A2: x in dom even-seq(n) & r = (even-seq n).x by FUNCT_1:def 3;
reconsider x0 = x as Nat by A2;
x in Seg n by A2,Th1; then
reconsider x1 = x0 as non zero Nat by FINSEQ_1:1;
r = 2*x1 by A2,Def1;
hence thesis;
end;
hence thesis by PARTFUN3:def 1;
end;
registration
let n be non zero Nat;
cluster even-seq n -> positive-yielding;
coherence by Lm1;
end;
registration
let n be non zero Nat;
cluster even-seq n -> non empty;
coherence
proof
len even-seq n = n by Def1;
hence thesis;
end;
end;
Lm2:
for n be non zero Nat holds odd-seq n is positive-yielding
proof
let n be non zero Nat;
for r being Real st r in rng odd-seq n holds 0 < r
proof
let r be Real;
assume r in rng odd-seq n; then
consider x be object such that
A2: x in dom odd-seq n & r = (odd-seq n).x by FUNCT_1:def 3;
reconsider x0 = x as Nat by A2;
x in Seg n by A2,Th1; then
reconsider x1 = x0 as non zero Nat by FINSEQ_1:1;
r = 2*x1 -1 by A2,Th2;
hence thesis;
end;
hence thesis by PARTFUN3:def 1;
end;
registration
let n be non zero Nat;
cluster odd-seq n -> positive-yielding;
coherence by Lm2;
end;
registration
let n be non zero Nat;
cluster odd-seq n -> non empty;
coherence
proof
dom odd-seq n = Seg n & Seg n = dom even-seq n by Th1; then
len odd-seq n = len even-seq n by FINSEQ_3:29 .= n by Def1;
hence thesis;
end;
end;
Lm3:
for n be non zero Nat holds even-seq n is increasing
proof
let n be non zero Nat;
set F = even-seq n;
for x1,x2 be Nat st x1 in dom F & x2 in dom F & x1 < x2 holds F.x1 < F.x2
proof
let x1,x2 be Nat;
assume
A1: x1 in dom F & x2 in dom F & x1 < x2; then
F.x1 = 2*x1 & F.x2 = 2*x2 by Def1;
hence thesis by A1,XREAL_1:68;
end;
hence thesis by SEQM_3:def 1;
end;
Lm4:
for n be non zero Nat holds odd-seq n is increasing
proof
let n be non zero Nat;
set F = odd-seq n;
for x1,x2 be Nat st x1 in dom F & x2 in dom F & x1 < x2 holds F.x1 < F.x2
proof
let x1,x2 be Nat;
assume
A1: x1 in dom F & x2 in dom F & x1 < x2; then
A2: F.x1 = 2*x1 -1 & F.x2 = 2*x2 -1 by Th2;
2*x1 < 2*x2 by A1,XREAL_1:68;
hence thesis by A2,XREAL_1:8;
end;
hence thesis by SEQM_3:def 1;
end;
registration
let n be non zero Nat;
cluster even-seq n -> increasing;
coherence by Lm3;
cluster odd-seq n -> increasing;
coherence by Lm4;
end;
theorem Th3:
for n be non zero Nat holds
even-seq(n+1) = (even-seq n)^<* 2*(n+1) *>
proof
let n be non zero Nat;
set p = even-seq(n+1);
set q = even-seq n;
set x = <* 2*(n+1)*>;
A1: len p = n+1 by Def1;
A2: len q = n by Def1; then
A3: len p = len (q^<* 2*(n+1)*>) by A1,FINSEQ_2:16;
A4: dom q = Seg n by Th1;
A5: dom p = Seg(n+1) by A1,FINSEQ_1:def 3;
for k be Nat st 1 <= k & k <= len p holds p.k = (q^x).k
proof
let k be Nat;
assume 1 <= k & k <= len p; then
per cases by A1,XXREAL_0:1;
suppose
A7: 1 <= k < n+1; then
k <= n by NAT_1:13; then
A9: k in dom q by A4,A7;
A10: k in dom p by A5,A7;
(q^x).k = q.k by A9,FINSEQ_1:def 7.= 2*k by A9,Def1;
hence thesis by A10,Def1;
end;
suppose
k = n+1;
hence thesis by A2,Def1,A5,FINSEQ_1:4;
end;
end;
hence thesis by A3,FINSEQ_1:14;
end;
theorem
for n be non zero Nat holds
Product even-seq(n+1) = (2*(n+1))*Product(even-seq(n))
proof
let n be non zero Nat;
Product even-seq(n+1)
= Product((even-seq n)^<* 2*(n+1) *>) by Th3
.= (Product(even-seq n))*(2*(n+1)) by RVSUM_1:96;
hence thesis;
end;
theorem Th5:
even-seq(1) = <* 2 *> & even-seq(2) = <* 2,4 *> &
even-seq(3) = <* 2,4,6 *>
proof
A1: len even-seq(1) = 1 by Def1;
dom even-seq(1) = Seg len even-seq(1) by FINSEQ_1:def 3
.= Seg 1 by Def1; then
1 in dom even-seq(1); then
A2: (even-seq(1)).1 = 2*1 by Def1;
A3: even-seq(1+1) = (even-seq 1)^<* 2*(1+1) *> by Th3;
even-seq(2+1) = (even-seq 2)^<* 2*(2+1) *> by Th3;
hence thesis by FINSEQ_1:40,A1,A2,A3;
end;
theorem Th6:
for n be non zero Nat holds
(odd-seq(n+1))|Seg(n) = odd-seq n
proof
let n be non zero Nat;
set X = Seg n;
set ev = even-seq n;
set h = even-seq(n) + ((dom even-seq(n)) --> -1);
set h1 = even-seq(n+1) + ((dom even-seq(n+1)) --> -1);
A1: len ev = n by Def1;
A2: dom even-seq n = Seg len even-seq n by FINSEQ_1:def 3
.= Seg n by Def1;
A3: dom even-seq(n+1) = Seg len even-seq(n+1) by FINSEQ_1:def 3
.= Seg(n+1) by Def1;
A4: (even-seq(n+1))|Seg(n)
= ((even-seq(n))^<* 2*(n+1) *>)|n by Th3
.= even-seq(n) by A1;
min (n,n+1) = n; then
dom(even-seq(n+1))/\ Seg(n)
= dom even-seq n by A2,A3,FINSEQ_2:2; then
(dom even-seq(n+1) --> -1)|Seg(n)
= dom(even-seq n) --> -1 by FUNCOP_1:12;
hence thesis by A4,RFUNCT_1:44;
end;
theorem Th7:
for n be non zero Nat holds
odd-seq(n+1) = (odd-seq(n))^<* 2*n + 1 *>
proof
let n be non zero Nat;
n < n+1 by NAT_1:16; then
A5: n < len odd-seq(n+1) by Th1;
A2: (odd-seq(n+1))|(n+1)
= (odd-seq(n+1))|dom(odd-seq(n+1)) by Th1
.= odd-seq(n+1);
A3: (odd-seq(n+1))|n = odd-seq n by Th6;
A4: dom odd-seq(n+1) = Seg (n+1) by Th1;
A6: dom even-seq(n+1) = Seg len even-seq(n+1) by FINSEQ_1:def 3
.= Seg(n+1) by Def1; then
A7: ((dom (even-seq(n+1))) --> -1).(n+1) = -1 by FUNCOP_1:7,FINSEQ_1:4;
(odd-seq(n+1)).(n+1)
= (even-seq(n+1)).(n+1) + ((dom (even-seq(n+1))) --> -1).(n+1)
by FINSEQ_1:4,A4,VALUED_1:def 1
.= 2*(n+1) - 1 by A6,FINSEQ_1:4,A7,Def1 .= 2*n +1;
hence thesis by A3,A2,A5,FINSEQ_5:83;
end;
theorem Th8:
odd-seq(1) = <* 1 *> & odd-seq(2) = <* 1,3 *> &
odd-seq(3) = <* 1,3,5 *>
proof
dom odd-seq 1 = Seg 1 & dom even-seq 1 = Seg 1 by Th1; then
A2: 1 in dom odd-seq 1 & 1 in dom even-seq 1; then
A3: ((dom even-seq 1) --> -1).1 = -1 by FUNCOP_1:7;
A4: len odd-seq 1 = 1 by Th1;
A5: (odd-seq 1).1
= (even-seq 1).1 + ((dom(even-seq 1) --> -1)).1 by A2,VALUED_1:def 1
.= 2*1 -1 by A2,Def1,A3 .= 1;
A6: odd-seq(1+1) = (odd-seq 1)^<* (2*1) +1 *> by Th7;
odd-seq(2+1) = (odd-seq 2)^<* (2*2) +1 *> by Th7;
hence thesis by A5,A4,FINSEQ_1:40,A6;
end;
theorem Th9:
for n be non zero Nat holds
Product even-seq(n+1) = (2*(n+1))*Product(even-seq n)
proof
let n be non zero Nat;
Product even-seq(n+1)
= Product((even-seq(n))^<* 2*(n+1)*>) by Th3
.= (Product(even-seq(n)))*(2*(n+1)) by RVSUM_1:96;
hence thesis;
end;
theorem Th10:
for n be non zero Nat holds
Product odd-seq(n+1) = (2*n +1)*Product(odd-seq(n))
proof
let n be non zero Nat;
Product odd-seq(n+1)
= Product((odd-seq(n))^<* 2*n +1 *>) by Th7
.= (Product(odd-seq(n)))*(2*n +1) by RVSUM_1:96;
hence thesis;
end;
theorem Th11:
for k be non zero Nat holds
Product even-seq(k) = (2|^k)*(k!)
proof
let k be non zero Nat;
defpred P[Nat] means Product(even-seq($1)) = (2|^$1)*($1!);
A1: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
A3: 2|^(n+1) = (2|^1)*(2|^n) by NEWTON:8
.= 2*(2|^n);
assume P[n]; then
Product(even-seq(n +1))
= (2*(n+1))*((2|^n)*(n!)) by Th9
.= (2|^(n+1))*((n+1)*(n!)) by A3
.= (2|^(n+1))*((n+1)!) by NEWTON:15;
hence thesis;
end;
A4: P[1] by Th5,NEWTON:13;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A4,A1);
hence thesis;
end;
theorem Th12:
for k be non zero Nat holds
Product(odd-seq(k)) = ((2*k)!)/((2|^k)*(k!))
proof
let k be non zero Nat;
defpred P[non zero Nat] means
Product(odd-seq($1)) = ((2*$1)!)/((2|^$1)*($1!));
A1: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A2: P[n];
A3: ((2*(n+1))*(2*n +1))*((2*n)!)
= (2*(n+1))*((2*n +1)*((2*n)!))
.= ((2*n +1)+1)*((2*n +1)!) by NEWTON:15
.= (2*(n+1))! by NEWTON:15;
2|^(n+1) = (2|^1)*(2|^n) by NEWTON:8
.= 2*(2|^n); then
A5: ((2*(n+1))*(2|^n))*(n!)
= (2|^(n+1))*((n+1)*(n!))
.= (2|^(n+1))*((n+1)!) by NEWTON:15;
(2*n+1)*Product(odd-seq(n))
= (((2*(n+1))*(2*n +1))/(2*(n+1)))*(((2*n)!)/((2|^n)*(n!)))
by A2,XCMPLX_1:89
.= ((2*(n+1))!)/((2*(n+1))*((2|^n)*(n!))) by A3,XCMPLX_1:76
.= ((2*(n+1))!)/((2|^(n+1))*((n+1)!)) by A5;
hence thesis by Th10;
end;
A6: P[1] by Th8,NEWTON:14,13;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A6,A1);
hence thesis;
end;
begin
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: 2. Treating a function as Elements of $\mathbb{R}$-algebra
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let A be set;
let f be Element of RAlgebra(A);
func @f -> Element of Funcs(A,REAL) equals
f;
coherence;
end;
definition
let A be set;
let f be Function of A, REAL;
func @f -> Element of RAlgebra(A) equals
f;
coherence by FUNCT_2:8;
end;
registration
let A be set;
let f be Element of RAlgebra A;
reduce @(@f) to f;
reducibility;
end;
registration
let A be set;
let f be Function of A,REAL;
reduce @(@f) to f;
reducibility;
end;
theorem Th13:
for A be non empty set holds
for f,g be Element of RAlgebra(A) holds f*g = @f(#)@g & @(f*g) = @f(#)@g
by FUNCSDOM:29;
theorem Th14:
for A be non empty set holds
for a be Element of REAL, f be Element of RAlgebra(A) holds a(#)@f = a*f
by FUNCSDOM:30;
registration
cluster RAlgebra REAL -> scalar-unital;
coherence
proof
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
for v being Element of RAlgebra REAL holds jj * v = v
proof
let v be Element of RAlgebra REAL;
jj * v = jj (#) @v by Th14 .= v;
hence thesis;
end;
hence thesis;
end;
end;
theorem
RAlgebra REAL is RealLinearSpace;
theorem
for A be non empty set holds
for f,g be Element of RAlgebra(A) holds
(RealFuncAdd(A)).(f,g) = (RealFuncAdd(A)).(@f,@g);
theorem Th17:
for A being non empty set, f be Element of RAlgebra(A) holds
(-1)*f = (-1) (#) @f & @((-1)*f) = -@f & 0.RAlgebra(A) = 0 (#) @f
proof
let A be non empty set, f be Element of RAlgebra(A);
0.RAlgebra(A) = A --> 0 .= 0 (#) @f;
hence thesis by FUNCSDOM:30;
end;
theorem Th18:
for A be non empty set holds
for f,g be Element of RAlgebra(A) holds f + g = @f + @g
by FUNCSDOM:28;
theorem Th19:
for f,g be Element of RAlgebra(REAL) holds f - g = @f - @g
proof
let f,g be Element of RAlgebra(REAL);
A1: @((-1)*g) = -@g by Th17;
f - g = @f + @(-g) by FUNCSDOM:28
.= @f + (-@g) by A1,RLVECT_1:16;
hence thesis;
end;
theorem Th20:
for M be unital associative non empty multMagma
for n be Nat, a be Element of M holds a|^(n+1) = (a|^n) * a
proof
let M be unital associative non empty multMagma;
let n be Nat, a be Element of M;
a|^(n+1) = (a|^n) * (a|^1) by BINOM:10
.= (a|^n) * a by BINOM:8;
hence thesis;
end;
Lm5:
for x be Element of RAlgebra(REAL) holds x|^0 = REAL --> 1
proof
let x be Element of RAlgebra(REAL);
thus x|^0 = 1_RAlgebra(REAL) by BINOM:8
.= REAL --> 1;
end;
Lm6:
for x be Function of REAL,REAL holds (@x)|^0 = REAL --> 1
proof
let x be Function of REAL,REAL;
thus (@x)|^0 = 1_RAlgebra(REAL) by BINOM:8
.= REAL --> 1;
end;
theorem Th21:
for n be Nat, x be Function of REAL,REAL st x is continuous holds
@((@x)|^n) is continuous
proof
let n be Nat, x be Function of REAL,REAL;
assume
A1: x is continuous;
defpred P[Nat] means @((@x)|^$1) is continuous;
A2: for n be Nat holds P[n] implies P[n+1]
proof
let n be Nat;
assume
A3: P[n];
@((@x)|^(n+1)) = ((@x)|^n)*(@x) by Th20
.= @((@x)|^n) (#) @(@x) by Th13;
hence thesis by A1,A3;
end;
A5: P[0] by Lm5;
for n be Nat holds P[n] from NAT_1:sch 2(A5,A2);
hence thesis;
end;
theorem Th22:
for x be Function of REAL,REAL, n be Nat, a be Real st (@(@x)).a > 0
holds
(@((@x)|^n)).a = ((@(@x)).a)|^n
proof
let x be Function of REAL,REAL, n be Nat, a be Real;
assume
A1: (@(@x)).a > 0;
defpred P[Nat] means (@((@x)|^$1)).a = ((@(@x)).a)|^$1;
A2: for n be Nat holds P[n] implies P[n+1]
proof
let n be Nat;
assume
A3: P[n];
@((@x)|^(n+1))
= ((@x)|^n)*(@x) by Th20 .= @((@x)|^n) (#) @(@x) by Th13; then
(@((@x)|^(n+1))).a
= (((@(@x)).a) to_power n)*(((@(@x)).a) to_power 1) by A3,VALUED_1:5
.= ((@(@x)).a) to_power (n+1) by A1,POWER:27
.= ((@(@x)).a)|^(n+1);
hence thesis;
end;
A4: P[0]
proof
A5: ((@(@x)).a)|^0 = ((@(@x)).a) to_power 0 .= 1 by POWER:24;
@((@x)|^0) = REAL --> 1 by Lm5;
hence thesis by A5,XREAL_0:def 1,FUNCOP_1:7;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem Th23:
for x be Function of REAL,REAL, n be non zero Nat, a be Real st (@(@x)).a =0
holds (@((@x)|^n)).a = 0
proof
let x be Function of REAL,REAL, n be non zero Nat, a be Real;
assume
A1: (@(@x)).a = 0;
defpred P[Nat] means (@((@x)|^$1)).a = 0;
A2: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume P[n];
@((@x)|^(n+1)) = ((@x)|^n)*(@x) by Th20
.= @((@x)|^n) (#) @(@x) by Th13; then
(@((@x)|^(n+1))).a = ( @((@x)|^n)).a * (@(@x)).a by VALUED_1:5
.= 0 by A1;
hence thesis;
end;
A3: P[1] by A1,BINOM:8;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A3,A2);
hence thesis;
end;
theorem Th24:
for Z be open Subset of REAL, n be non zero Nat holds
for x be Function of REAL,REAL st x is_differentiable_on Z holds
@((@x)|^n) is_differentiable_on Z
proof
let Z be open Subset of REAL, n be non zero Nat;
let x be Function of REAL,REAL;
assume
A1: x is_differentiable_on Z;
defpred P[Nat] means @((@x)|^$1) is_differentiable_on Z;
A2: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A3: P[n];
@((@x)|^(n+1)) = ((@x)|^n)*(@x) by Th20
.= @((@x)|^n) (#) @(@x) by Th13;
hence thesis by A1,A3,FDIFF_2:20;
end;
A5: P[1] by A1,BINOM:8;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A5,A2);
hence thesis;
end;
theorem Th25:
for n be Nat, I be non empty closed_interval Subset of REAL holds
for x be Function of REAL,REAL st x is continuous holds
@((@x)|^n)|I is continuous & @((@x)|^n) is_integrable_on I &
@((@x)|^n)|I is bounded
proof
let n be Nat, I be non empty closed_interval Subset of REAL;
let x be Function of REAL,REAL;
assume x is continuous; then
A2: @((@x)|^n)|REAL is continuous by Th21;
I c= REAL; then
A4: I c= dom @((@x)|^n) by FUNCT_2:def 1;
@((@x)|^n)|I is continuous by A2;
hence thesis by A4,INTEGRA5:10,11;
end;
reserve r for Real;
theorem Th26:
for n be Nat, I be non empty closed_interval Subset of REAL holds
for x be Function of REAL,REAL st x is continuous holds
(r(#)@((@x)|^n))|I is continuous & r(#)@((@x)|^n) is_integrable_on I &
(r(#)@((@x)|^n))|I is bounded
proof
let n be Nat, I be non empty closed_interval Subset of REAL;
let x be Function of REAL,REAL;
assume x is continuous; then
A2: @((@x)|^n)|REAL is continuous by Th21;
I c= REAL; then
A3: I c= dom (r(#)@((@x)|^n)) by FUNCT_2:def 1;
(r(#)@((@x)|^n))|I is continuous by A2;
hence thesis by A3,INTEGRA5:10,11;
end;
Lm7:
REAL is open Subset of REAL
proof
A1: REAL c= REAL;
now
let r be Element of REAL;
assume r in REAL;
]. r-1,r+1 .[ is Neighbourhood of r by RCOMP_1:def 6;
hence ex N being Neighbourhood of r st N c= REAL;
end;
hence thesis by A1,RCOMP_1:20;
end;
theorem Th27:
for n be non zero Nat holds
(@((@sin)|^n)).0 = 0 & (@((@sin)|^n)).(PI/2) = 1
proof
let n be non zero Nat;
A1: @((@sin)).0 = 0 by SIN_COS:30;
@((@sin)).(PI/2) = 1 by SIN_COS:76; then
(@((@sin)|^n)).(PI/2) = 1|^n by Th22 .= 1;
hence thesis by A1,Th23;
end;
theorem Th28:
for n be non zero Nat holds
@((@sin)|^(n+1)) `|REAL = (n+1)(#)@((@sin)|^n) (#) @(@cos)
proof
let n be non zero Nat;
set Z = REAL;
set x = sin;
defpred P[Nat] means
@((@x)|^($1+1)) `|Z = ($1+1)(#)@((@x)|^$1) (#) @(@cos);
A1: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A2: P[n];
reconsider n1 = n+1 as non zero Nat;
A3: @((@x)|^n1) is_differentiable_on Z &
@((@x)) is_differentiable_on Z by Lm7,SIN_COS:68,Th24;
A4: @((@x)|^n1) = ((@x)|^n)*(@x) by Th20
.= @((@x)|^n) (#) @(@x) by Th13;
reconsider f = @((@x)|^n1) (#) @(@cos) as Function of REAL,REAL;
reconsider f1 = f as Element of RAlgebra(REAL) by FUNCT_2:8;
reconsider r1 = n1 as Element of REAL by NUMBERS:19;
reconsider o1 = 1 as Element of REAL by FINANCE2:1;
A5: f = @f1;
A6: r1(#)@f1 = @(r1*f1) by Th14;
A7: 1(#)@f1 = @(o1*f1) by Th14;
(n1(#)@((@x)|^n) (#) @(@cos) ) (#) @(@x)
= ((n1(#)@((@x)|^n)) (#) @(@x)) (#) @(@cos) by RFUNCT_1:9
.= (n1(#) @((@x)|^n1)) (#) @(@cos) by A4,RFUNCT_1:12; then
A9: (n1(#)@((@x)|^n) (#) @(@cos))(#)@(@x) + @((@x)|^n1) (#) cos
= @(r1*f1) + @(o1*f1) by A7,A6,RFUNCT_1:12
.= r1*f1 + o1*f1 by Th18
.= (r1+o1)*f1 by FUNCSDOM:14
.= (n1 +1)(#)(@((@x)|^n1) (#) @(@cos)) by A5,Th14;
@((@x)|^(n1+1)) = ((@x)|^n1)*(@x) by Th20
.= @((@x)|^n1) (#) @(@x) by Th13; then
@((@x)|^(n1+1)) `|Z = (n1 +1)(#)(@((@x)|^n1) (#) @(@cos))
by A9,A2,A3,Lm7,FDIFF_2:20,INTEGRA8:27
.= (n1 +1)(#)@((@x)|^n1) (#) @(@cos) by RFUNCT_1:12;
hence thesis;
end;
A11: P[1]
proof
A12: @((@x)|^1) = @(@x) by BINOM:8;
@((@x)|^(1+1)) = ((@x)|^1)*(@x) by Th20
.= @((@x)|^1) (#) @(@x) by Th13; then
@((@x)|^(1+1)) `|Z = @(@x) (#)(cos) + @(@x) (#)(cos)
by A12,SIN_COS:68,Lm7,FDIFF_2:20,INTEGRA8:27
.= 2(#)(@((@x)|^1) (#)@(@cos)) by A12,PDLAX:9;
hence thesis by RFUNCT_1:12;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A11,A1);
hence thesis;
end;
begin
::::::::::::::::::::::::::::::::::::
:: 3. Recurrence relation on $\int_0^{\frac{\pi}{2}} \sin^{n} x \ dx$
:: \& Wallis Integral
:::::::::::::::::::::::::::::::::::
theorem
@((@sin)|^1) `|REAL is_differentiable_on REAL
by BINOM:8,INTEGRA8:27,SIN_COS:67;
theorem
for n be non zero Nat holds
@((@sin)|^(n+1)) `|REAL is_differentiable_on REAL
proof
let n be non zero Nat;
set Z = REAL;
set x = sin;
A1: @((@x)|^n) is_differentiable_on Z &
@((@x)) is_differentiable_on Z by Lm7,SIN_COS:68,Th24;
(n+1)(#)@((@sin)|^n) (#) @(@cos) is_differentiable_on Z
proof
reconsider h = @((@x)|^n) (#) @(@cos) as Function of REAL,REAL;
h is_differentiable_on Z by A1,SIN_COS:67,INTEGRA7:6; then
(n+1)(#)(@((@x)|^n) (#) @(@cos)) is_differentiable_on Z
by INTEGRA7:7;
hence thesis by RFUNCT_1:12;
end;
hence thesis by Th28;
end;
theorem Th31:
for n be Nat st n >= 2 holds
@((@sin)|^(n-'1)) is_integral_of
(n-'1)(#)(@((@sin)|^(n-'2))) (#) @(@cos), REAL
proof
set x = sin;
let n be Nat;
assume
A1: n >= 2; then
A2: n -' 2 = n - 2 by XREAL_1:233;
reconsider n2 = n -' 2 as Nat;
A3: n -' 1 = n - 1 by A1,XXREAL_0:2,XREAL_1:233;
reconsider n1 = n -' 1 as Nat;
reconsider f = (n-'1)(#)(@((@sin)|^(n-'2))) (#) @(@cos)
as Function of REAL,REAL;
reconsider F = @((@sin)|^(n-'1)) as Function of REAL,REAL;
per cases by A1,XXREAL_0:1;
suppose
A4: n = 2; then
A5: @((@sin)|^(n-'1)) = x by A3,BINOM:8;
A6: (@x)|^(n-'2) = (@x)|^0 by A4,XREAL_1:232
.= 1_RAlgebra(REAL) by BINOM:8;
(n-'1)(#)(@((@sin)|^(n-'2))) (#) @(@cos)
= ((@x)|^(n-'2)) * (@cos) by Th13,A3,A4
.= cos by A6; then
A8: ((n-'1)(#)(@((@sin)|^(n-'2))) (#) @(@cos))|REAL
= @((@sin)|^(n-'1)) `|REAL by A5,INTEGRA8:27;
@((@sin)|^(n-'1)) in IntegralFuncs(f,REAL)
by A8,A5,SIN_COS:68,INTEGRA7:def 1;
hence thesis by INTEGRA7:def 2;
end;
suppose
A10: n > 2; then
reconsider n2 as non zero Nat by A2;
A11: n2 + 1 = n - 2 +1 by A1,XREAL_1:233 .= n - 1 .= n -' 1
by A1,XXREAL_0:2,XREAL_1:233;
A12: n - 1 > 2 - 1 by A10,XREAL_1:14;
reconsider n1 as non zero Nat by A12,A1,XXREAL_0:2,XREAL_1:233;
A13: @((@x)|^n1) is_differentiable_on REAL by Lm7,SIN_COS:68,Th24;
f|REAL = F `|REAL by Th28,A11; then
@((@sin)|^(n-'1)) in IntegralFuncs(f,REAL)
by A13,INTEGRA7:def 1;
hence thesis by INTEGRA7:def 2;
end;
end;
theorem Th32:
integral(@((@sin)|^0), 0,PI/2) = PI/2
proof
A2: dom @((@sin)|^0) = REAL by FUNCT_2:def 1;
(@sin)|^0 = REAL --> 1 by Lm6; then
A4: for x be Real st x in [' 0,PI/2 '] holds (@((@sin)|^0)).x = 1
by FUNCOP_1:7;
['0,PI/2'] = [.0,PI/2.] by COMPTRIG:5,INTEGRA5:def 3; then
0 in ['0,PI/2'] & PI/2 in ['0,PI/2'] by COMPTRIG:5,XXREAL_1:1; then
integral(@((@sin)|^0),0,PI/2) = 1*(PI/2-0)
by COMPTRIG:5,A2,A4,INTEGRA6:27
.= PI/2;
hence thesis;
end;
theorem Th33:
integral(@((@sin)|^1), 0,PI/2) = 1
proof
@((@sin)|^1) = sin by BINOM:8; then
integral(@((@sin)|^1), 0,PI/2) = 1 - 0 by SIN_COS:76,30,INTEGRA7:26;
hence thesis;
end;
theorem Th34:
(sin (#) sin) + (cos (#) cos) = 1.RAlgebra(REAL)
proof
for o be object st o in dom (REAL -->1) holds
((sin (#) sin) + (cos (#) cos) ).o = (REAL -->1).o
proof
let o be object;
assume
A1: o in dom (REAL -->1); then
reconsider r = o as Element of REAL;
A2: (sin (#) sin).r = (sin).r * (sin).r &
(cos (#) cos).r = (cos).r * (cos).r by RFUNCT_1:56;
((sin (#) sin) + (cos (#) cos)).o
= sin.r * sin.r + cos.r * cos.r by A2,RFUNCT_1:56
.= 1 by SIN_COS:28 .= (REAL-->1).o by A1,FUNCOP_1:7;
hence thesis;
end; then
(sin (#) sin) + (cos (#) cos) = REAL -->1;
hence thesis;
end;
theorem Th35:
(@sin)|^2 + (@cos)|^2 = 1.RAlgebra(REAL) &
(@sin)|^2 = sin (#) sin & (@cos)|^2 = cos (#) cos &
(@sin)|^2 = @sin * (@sin) & (@cos)|^2 = @cos * (@cos)
proof
A1: (@sin)|^2 = (@sin)|^(1+1)
.= (@sin)|^1 * (@sin) by Th20
.= (@sin) * (@sin) by BINOM:8;
A2: (@sin) * (@sin) = @(@sin) (#) @(@sin) by Th13
.= sin (#) sin;
A4: (@cos) * (@cos) = @(@cos) (#) @(@cos) by Th13
.= cos (#) cos;
A3: (@cos)|^2 = (@cos)|^(1+1)
.= (@cos)|^1 * (@cos) by Th20
.= (@cos) * (@cos) by BINOM:8; then
(@sin)|^2 + (@cos)|^2
= @((@sin) * (@sin)) + @((@cos) * (@cos)) by Th18,A1
.= (@(@sin) (#) @(@sin)) + @((@cos) * (@cos)) by Th13
.= (@(@sin) (#) @(@sin)) + (@(@cos) (#) @(@cos)) by Th13
.= (sin(#)sin) + (cos(#)cos);
hence thesis by Th34,A1,A2,A3,A4;
end;
definition
func 'I' -> Real_Sequence means :Def6:
for m be Nat holds it.m = integral(@((@sin)|^m),0,PI/2);
correctness
proof
deffunc F(Nat) = integral(@((@sin)|^$1),0,PI/2);
(ex seq being Real_Sequence st for n being Nat holds seq.n = F(n)) &
(for seq1, seq2 being Real_Sequence st
(for n being Nat holds seq1.n = F(n)) &
(for n being Nat holds seq2.n = F(n)) holds seq1 = seq2)
from NUMPOLY1:sch 1;
hence thesis;
end;
end;
begin
:::::::::::::::::::::::::::::::::
::4. the Wallis Product Formula
::::::::::::::::::::::::::::::::
theorem Th36:
for n be Nat st n >= 2 holds ((n-'1)/n)*('I'.(n-'2)) = 'I'.n
proof
let n be Nat;
assume
A1: n >= 2; then
A2: 1 < n by XXREAL_0:2;
reconsider n0 = n as Element of NAT by ORDINAL1:def 12;
reconsider n1 = n-'1 as Nat;
A3: n1 = n-1 by A1, XXREAL_0:2,XREAL_1:233; then
A4: @((@sin)|^n) = (@sin)|^(n1+1)
.= ((@sin)|^n1)*(@sin) by Th20
.= @((@sin)|^(n-'1)) (#) @(@sin) by Th13;
A5: n1 > 0 by XREAL_1:50,A2,A3;
reconsider n1 as non zero Nat by A1, A3;
reconsider g = (n-'1)(#)(@((@sin)|^(n-'2)))(#)@(@cos) as Function of REAL,REAL;
reconsider G = @((@sin)|^(n-'1)) as Function of REAL,REAL;
reconsider f = @(@sin) as Function of REAL,REAL;
reconsider F = @(@(-cos)) as Function of REAL,REAL;
A6: REAL c= dom sin by FUNCT_2:def 1;
A7: sin|REAL is continuous;
A9: dom g = REAL by FUNCT_2:def 1;
@((@sin)|^(n-'2))|REAL is continuous by Th21; then
A10: g|REAL is continuous;
A11: G is_integral_of g,REAL by A1,Th31;
[.0,PI/2.] c= REAL; then
A13: (F.(PI/2))*(G.(PI/2)) - (F.0)*(G.0)
= integral(f(#)G,0,PI/2)+ integral(F(#)g,0,PI/2)
by INTEGRA7:22,25,COMPTRIG:5,A9,A6,A10,A7,A11;
A14: @(@(-cos)).(PI/2) = -0 by SIN_COS:76,VALUED_1:8;
A15: -@((@cos)|^2) = (-cos) (#) cos by RFUNCT_1:12,Th35;
A16: (@sin)|^2 = 1.RAlgebra(REAL) - (@cos)|^2 by Th35,VECTSP_2:2;
reconsider f = (@cos)|^2 as Element of RAlgebra(REAL);
A17: @((@sin)|^2) - @(1.RAlgebra(REAL))
= (@sin)|^2 - 1.RAlgebra(REAL) by Th19
.= - (@cos)|^2 by A16,VECTSP_2:2
.= @((-1)*(@cos)|^2) by RLVECT_1:16
.= -@((@cos)|^2) by Th17;
set e1 = 1.RAlgebra REAL;
set s1 = (n-'1)(#)@((@sin)|^(n-'2));
A18: @((@sin)|^2) (#)s1
= (n-'1)(#) (@((@sin)|^2) (#) @((@sin)|^(n-'2))) by RFUNCT_1:13
.= (n-'1)(#)@((@sin)|^2 * (@sin)|^(n-'2)) by Th13
.= (n-'1)(#)@((@sin)|^(n-'2+2)) by BINOM:10
.= (n-'1)(#)@((@sin)|^n) by A1,XREAL_1:235;
@e1(#)@((@sin)|^(n-'2)) = e1*((@sin)|^(n-'2)) by Th13
.= @((@sin)|^(n-'2)); then
@e1(#)s1 = (n-'1)(#)@((@sin)|^(n-'2)) by RFUNCT_1:13; then
A21: (@((@sin)|^2)-@e1)(#)s1
= (n-'1)(#)@((@sin)|^n) - (n-'1)(#)@((@sin)|^(n-'2))
by A18,RFUNCT_1:14;
set I1 = @((@sin)|^n);
set I2 = @((@sin)|^(n-'2));
A22: F(#)g = (n-'1)(#)I1 - (n-'1)(#)I2 by A21,A17,A15,RFUNCT_1:9;
A23: ((n-'1)(#)I1)|['0,PI/2'] is continuous &
((n-'1)(#)I1) is_integrable_on ['0,PI/2'] &
((n-'1)(#)I1)|['0,PI/2'] is bounded by Th26;
A24: ((n-'1)(#)I2)|['0,PI/2'] is continuous &
((n-'1)(#)I2) is_integrable_on ['0,PI/2'] &
((n-'1)(#)I2)|['0,PI/2'] is bounded by Th26;
A25: I1|['0,PI/2'] is continuous & I1 is_integrable_on ['0,PI/2'] &
I1|['0,PI/2'] is bounded by Th25;
A26: I2|['0,PI/2'] is continuous & I2 is_integrable_on ['0,PI/2'] &
I2|['0,PI/2'] is bounded by Th25;
['0,PI/2'] = [.0,PI/2.] by COMPTRIG:5, INTEGRA5:def 3; then
A28: 0 in ['0,PI/2'] & PI/2 in ['0,PI/2'] by COMPTRIG:5, XXREAL_1:1;
A30: dom(I1) = REAL & dom(I2) = REAL by FUNCT_2:def 1;
dom((n-'1)(#)I1) = REAL & dom((n-'1)(#)I2) = REAL by FUNCT_2:def 1;
then
A31: integral(F(#)g,0,PI/2)
= integral((n-'1)(#)I1,0,PI/2) - integral((n-'1)(#)I2,0,PI/2)
by COMPTRIG:5,A22,A28,A23,A24,INTEGRA6:24;
A32: integral((n-'1)(#)I2,0,PI/2) = (n-'1)*integral(I2,0,PI/2)
by A26,COMPTRIG:5,A30,INTEGRA6:10;
A33: (F.(PI/2))*(G.(PI/2)) - (F.0)*(G.0)
= 0*(G.(PI/2)) - (F.0)*0 by A14,A5,Th27 .= 0;
integral(I1,0,PI/2)
= -integral((n-'1)(#)I1,0,PI/2) + integral((n-'1)(#)I2,0,PI/2)
by A31,A33,A13,A4
.= -(n-'1)*integral(I1,0,PI/2) + (n-'1)*integral(I2,0,PI/2)
by A25,COMPTRIG:5,A30,INTEGRA6:10,A32; then
A34: (n-'1)*integral(I2,0,PI/2)
= ((n-'1)+ 1)*integral(I1,0,PI/2)
.= n*integral(I1,0,PI/2) by A1, XXREAL_0:2,XREAL_1:235
.= n*('I'.n0) by Def6;
(n-'1)*('I'.(n-'2))/n = n*('I'.n)/n by A34,Def6
.= ('I'.n) by A1,XCMPLX_1:89;
hence thesis;
end;
theorem Th37:
for n be non zero Nat holds
'I'.(2*n+1) = Product(even-seq(n))/(Product(odd-seq(n+1)))
proof
let n be non zero Nat;
defpred P[non zero Nat] means 'I'.(2*$1+1) =
Product(even-seq($1))/Product(odd-seq($1+1));
A1: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A2: P[n];
set Podd1 = Product odd-seq(n+1);
set Peven1 = Product even-seq(n);
A3: 2 < 2*n +1 +2 by XREAL_1:29;
A4: (2*(n+1)+1)*Product(odd-seq(n+1)) = Product(odd-seq((n+1)+1)) by Th10;
'I'.(2*(n+1)+1)
= (((2*(n+1)+1)-'1)/(2*(n+1)+1))*('I'.((2*(n+1)+1)-'2)) by Th36,A3
.= ((2*(n+1))*Peven1)/((2*(n+1)+1)*Podd1) by A2,A3,XCMPLX_1:76
.= Product(even-seq(n+1))/Product(odd-seq((n+1)+1)) by Th9,A4;
hence thesis;
end;
A5: P[1]
proof
set n = 1;
A6: 3 -' 2 = 3 - 2 by XREAL_1:233 .= 1;
3 -' 1 = 3 - 1 by XREAL_1:233 .= 2; then
A8: 'I'.(2*n+1) = (2/3)*('I'.1) by A6,Th36
.= (2/3)*1 by Th33, Def6
.= 2/3;
Product(even-seq(1))/Product(odd-seq(1+1))
= 2/(1*3) by Th5,Th8,RVSUM_1:99 .= 2/3;
hence thesis by A8;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A5,A1);
hence thesis;
end;
theorem Th38:
for n be non zero Nat holds
'I'.(2*n) = (Product(odd-seq(n))/(Product(even-seq(n))))*(PI/2)
proof
let n be non zero Nat;
defpred P[non zero Nat] means
'I'.(2*$1) = (Product(odd-seq($1))/Product(even-seq($1)))*(PI/2);
A1: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A2: P[n];
set Podd1 = Product odd-seq(n);
set Peven1 = Product even-seq(n);
n+1 >= 0+1 by XREAL_1:6; then
A3: 2*(n+1) >= 2*1 by XREAL_1:64; then
A4: 2*(n+1) -'1 = 2*(n+1) -1 by XXREAL_0:2,XREAL_1:233 .= 2*n + 1;
A5: 2*(n+1) -'2 = 2*(n+1) - 2 by A3,XREAL_1:233 .= 2*n;
A6: Product even-seq((n+1)) = (2*(n+1))*Peven1 by Th9;
'I'.(2*(n+1)) = ((2*n+1)/(2*(n+1)))*('I'.(2*n)) by Th36,A3,A4,A5
.= (((2*n+1)/(2*(n+1)))*(Podd1/Peven1))*(PI/2) by A2
.= (((2*n+1)*Podd1)/((2*(n+1))*Peven1))*(PI/2) by XCMPLX_1:76
.= (Product(odd-seq(n+1))/Product(even-seq(n+1)))*(PI/2)
by A6,Th10;
hence thesis;
end;
A7: P[1]
proof
set n = 1;
A8: 2 -' 2 = 2 - 2 by XREAL_1:233 .= 0;
2 -' 1 = 2 - 1 by XREAL_1:233 .= 1; then
'I'.(2*n) = (1/2)*('I'.0) by A8,Th36
.= (1/2)*(PI/2) by Th32, Def6;
hence thesis by Th5,Th8;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A7,A1);
hence thesis;
end;
begin
:::::::::::::::::::::::::
:: Wallis Product
::::::::::::::::::::::::
theorem Th42:
for n be non zero Nat, x be Real st 0< x < PI/2 holds
@((@sin)|^(2*n)).x < @((@sin)|^(2*n-'1)).x &
@((@sin)|^(2*n+1)).x < @((@sin)|^(2*n)).x
proof
let n be non zero Nat, x be Real;
assume
A1: 0 < x < PI/2; then
A2: 0 < (@(@sin)).x by Th39; then
A3: @((@sin)|^(2*n-'1)).x = (sin.x)|^(2*n-'1) by Th22;
A4: @((@sin)|^(2*n)).x = (sin.x)|^(2*n) by A2,Th22;
@((@sin)|^(2*n+1)).x = (sin.x)|^(2*n+1) by A2,Th22;
hence thesis by A3,Th41,A1,A4;
end;
theorem Th43:
for n be non zero Nat holds
'I'.(2*n) <= 'I'.(2*n-'1) & 'I'.(2*n+1) <= 'I'.(2*n)
proof
let n be non zero Nat;
0 < 0+n; then
1 <= n by NAT_1:19; then
2*n >= 2*1 by XREAL_1:64; then
A2: 2*n -'1 = 2*n - 1 by XREAL_1:233,XXREAL_0:2;
set I0 = @((@sin)|^(2*n-'1));
set I1 = @((@sin)|^(2*n));
set I2 = @((@sin)|^(2*n+1));
A3: I0|['0,PI/2'] is continuous &
I0 is_integrable_on ['0,PI/2'] &
I0|['0,PI/2'] is bounded by Th25;
A4: I1|['0,PI/2'] is continuous &
I1 is_integrable_on ['0,PI/2'] &
I1|['0,PI/2'] is bounded by Th25;
A5: I2|['0,PI/2'] is continuous &
I2 is_integrable_on ['0,PI/2'] &
I2|['0,PI/2'] is bounded by Th25;
A6: dom(I0) = REAL & dom(I1) = REAL & dom(I2) = REAL by FUNCT_2:def 1;
A7: for x be Real st x in ['0,PI/2'] holds I2.x <= I1.x
proof
let x be Real;
assume x in ['0,PI/2']; then
x in [.0,PI/2.] by INTEGRA5:def 3, COMPTRIG:5;
then per cases by XXREAL_1:5;
suppose
x in ].0,PI/2.[; then
0 < x < PI/2 by XXREAL_1:4;
hence thesis by Th42;
end;
suppose
x = 0; then
I1.x = 0 & I2.x = 0 by Th27;
hence thesis;
end;
suppose
x = PI/2; then
I1.x = 1 & I2.x = 1 by Th27;
hence thesis;
end;
end;
A16: for x be Real st x in ['0,PI/2'] holds I1.x <= I0.x
proof
let x be Real;
assume
x in ['0,PI/2']; then
x in [.0,PI/2.] by INTEGRA5:def 3,COMPTRIG:5;
then per cases by XXREAL_1:5;
suppose
x in ].0,PI/2.[; then
0 < x < PI/2 by XXREAL_1:4;
hence thesis by Th42;
end;
suppose
x = 0; then
I1.x = 0 & I0.x = 0 & I2.x = 0 by A2,Th27;
hence thesis;
end;
suppose
x = PI/2; then
I1.x = 1 & I0.x = 1 & I2.x = 1 by A2,Th27;
hence thesis;
end;
end;
A25: integral(I1,0,PI/2) <= integral(I0,0,PI/2)
by A3,A4,COMPTRIG:5,A6,A16,ORDEQ_01:48;
A26: integral(I2,0,PI/2) <= integral(I1,0,PI/2)
by A5,A4,COMPTRIG:5,A6,A7,ORDEQ_01:48;
reconsider n0 = 2*n-'1, n1 = 2*n, n2 = 2*n+1
as Element of NAT by ORDINAL1:def 12;
'I'.n1 = integral(I1,0,PI/2) by Def6;
hence thesis by Def6,A26,A25;
end;
theorem Th44:
for n be non zero Nat holds
1 <= 'I'.(2*n)/'I'.(2*n+1) &
'I'.(2*n)/'I'.(2*n+1)
= (Product(odd-seq(n))|^2/(Product(even-seq(n)))|^2)*n*((1+1/(2*n))*PI)
proof
let n be non zero Nat;
set evenn = Product even-seq(n);
set oddn = Product odd-seq(n);
set oddn1 = Product odd-seq(n+1);
A1: 'I'.(2*n) = (oddn/evenn)*(PI/2) by Th38;
A2: (n+1/2) = (n*1+1/2) .= n*(1+ ((1/2)/n)) by XCMPLX_1:235
.= n*(1+ ((1/2)*(1/n))) .= n*(1+ 1/(2*n)) by XCMPLX_1:103;
A3: (oddn*oddn1)/(evenn*evenn)
= (((2*n +1)*oddn)*oddn)/(evenn*evenn) by Th10
.=((2*n +1)*(oddn*oddn))/(evenn|^2) by WSIERP_1:1
.=((2*n +1)*(oddn|^2))/(evenn|^2) by WSIERP_1:1;
A4: 'I'.(2*n)/'I'.(2*n+1) = ((oddn/evenn)*(PI/2))/(evenn/oddn1) by Th37,A1
.=(PI/2)*((oddn/evenn)/(evenn/oddn1))
.= (PI/2)*(((2*n +1)*(oddn|^2))/(evenn|^2)) by A3,XCMPLX_1:84
.= (((oddn|^2))/(evenn|^2))*(n+1/2)*PI
.= (((oddn|^2))/(evenn|^2))*(n*(1+ 1/(2*n)))*PI by A2;
'I'.(2*n+1) = evenn/oddn1 by Th37;
hence thesis by A4,Th43,XREAL_1:181;
end;
theorem Th45:
for n be non zero Nat holds
1/((1+1/(2*n))*PI) <= (Product(odd-seq(n))|^2/(Product(even-seq(n)))|^2)*n
proof
let n be non zero Nat;
set s = (Product(odd-seq(n))|^2/(Product(even-seq(n)))|^2)*n;
1 <= 'I'.(2*n)/'I'.(2*n+1) by Th44; then
A1: 1 <= s*((1+1/(2*n))*PI) by Th44;
(s*((1+1/(2*n))*PI))*(1/((1+1/(2*n))*PI))
= s*(((1+1/(2*n))*PI)*(1/((1+1/(2*n))*PI)))
.= s by COMPTRIG:5,XCMPLX_1:108;
hence thesis by A1,XREAL_1:64;
end;
Lm8:
for n be non zero Nat holds 0 < 'I'.(2*n-'1)
proof
let n be non zero Nat;
set evenn = Product even-seq(n);
set oddn = Product odd-seq(n);
'I'.(2*n) = (oddn/evenn)*(PI/2) by Th38;
hence thesis by Th43,COMPTRIG:5;
end;
theorem Th46:
for n be non zero Nat holds 'I'.(2*n)/'I'.(2*n+1) <= 1 + 1/(2*n)
proof
let n be non zero Nat;
set evenn = Product even-seq n;
set oddn = Product odd-seq n;
set oddn1 = Product odd-seq (n+1);
Product(even-seq n)/Product(odd-seq(n+1)) > 0; then
A1: 'I'.(2*n+1) > 0 by Th37;
0 < 0+n; then
1 <= n by NAT_1:19; then
A2: 2*n >= 2*1 by XREAL_1:64; then
A3: 2*n + 1 > 2 by NAT_1:13; then
A4: (2*n+1)-'2 = (2*n+1)-2 by XREAL_1:233 .= 2*n -1
.= 2*n -'1 by A2,XXREAL_0:2, XREAL_1:233;
A5: 'I'.(2*n+1) = (((2*n+1)-'1)/(2*n+1))*('I'.((2*n+1)-'2)) by A3,Th36
.= (2*n/(2*n+1))*('I'.(2*n-'1)) by A4;
A6: ('I'.(2*n-'1)) <> 0 by Lm8;
set s1 = (2*n)/(2*n+1);
'I'.(2*n-'1)/'I'.(2*n+1)
= 1/('I'.(2*n-'1))*(('I'.(2*n-'1))/s1) by A5,XCMPLX_1:103
.= (('I'.(2*n-'1))*(1/('I'.(2*n-'1))))/s1
.= 1/s1 by A6,XCMPLX_1:106
.= (1+(2*n)*1)/(2*n) by XCMPLX_1:57
.= 1/(2*n) + 1 by XCMPLX_1:113;
hence thesis by A1,Th43,XREAL_1:72;
end;
theorem Th47:
for n be non zero Nat holds
(Product(odd-seq(n))|^2/(Product(even-seq(n)))|^2)*n <= 1/PI
proof
let n be non zero Nat;
set s1 =(Product(odd-seq(n))|^2/(Product(even-seq(n)))|^2)*n;
'I'.(2*n)/'I'.(2*n+1) = s1*((1+1/(2*n))*PI) by Th44; then
A2: (s1*((1+1/(2*n))*PI))*(1/((1+1/(2*n))*PI))
<= (1 + 1/(2*n))*(1/((1+1/(2*n))*PI)) by COMPTRIG:5,Th46, XREAL_1:64;
(1 + 1/(2*n))*(1/((1+1/(2*n))*PI))
= (1 + 1/(2*n))*((1/((1+1/(2*n))))*(1/PI)) by XCMPLX_1:102
.= 1/PI by XCMPLX_1:109;
hence thesis by COMPTRIG:5,XCMPLX_1:107,A2;
end;
definition
func Wallis_Seq -> Real_Sequence means :Def7:
for k be Nat holds
it.k = (Product(odd-seq(k+1))|^2 / (Product(even-seq(k+1)))|^2) * (k+1);
correctness
proof
deffunc F(Nat) =
(Product(odd-seq($1+1))|^2 / (Product(even-seq($1+1)))|^2) * ($1+1);
(ex seq being Real_Sequence st for n being Nat holds seq.n = F(n)) &
(for seq1, seq2 being Real_Sequence st
(for n being Nat holds seq1.n = F(n)) &
(for n being Nat holds seq2.n = F(n)) holds seq1 = seq2)
from NUMPOLY1:sch 1;
hence thesis;
end;
end;
definition
func w_seq -> Real_Sequence means :Def8:
for n be Nat holds it.n = 1/((1+1/(2*(n+1)))*PI);
correctness
proof
deffunc F(Nat) = 1/((1+1/(2*($1+1)))*PI);
(ex seq being Real_Sequence st for n being Nat holds seq.n = F(n)) &
(for seq1, seq2 being Real_Sequence st
(for n being Nat holds seq1.n = F(n)) &
(for n being Nat holds seq2.n = F(n)) holds seq1 = seq2)
from NUMPOLY1:sch 1;
hence thesis;
end;
end;
Lm10:
w_seq is convergent & lim w_seq = 1/PI
proof
deffunc E(Nat) = 1/($1+1);
consider s0 be Real_Sequence such that
A1: for n being Nat holds s0.n = E(n) from SEQ_1:sch 1;
deffunc F(Nat) = 1/(2*($1+1));
consider s1 be Real_Sequence such that
A2: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
deffunc G(Nat) = (1 + 1/(2*($1+1)));
consider s2 be Real_Sequence such that
A3: for n being Nat holds s2.n = G(n) from SEQ_1:sch 1;
deffunc H(Nat) = (s2.$1)*PI;
consider s3 be Real_Sequence such that
A4: for n being Nat holds s3.n = H(n) from SEQ_1:sch 1;
A5: for n be Nat holds s1.n=(1/2)*s0.n
proof
let n be Nat;
s1.n = 1/(2*(n+1)) by A2 .= (1/2)*(1/(n+1)) by XCMPLX_1:102
.= (1/2)*s0.n by A1;
hence thesis;
end;
A6: s1 is convergent & lim s1 = 0
proof
A7: s0 is convergent & lim s0 = 0 by A1, SEQ_4:31; then
(1/2)(#)s0 is convergent & lim((1/2)(#)s0) = (1/2)* lim s0
by SEQ_2:8;
hence thesis by A7,A5,SEQ_1:9;
end;
reconsider s4 = (seq_const 1) as convergent Real_Sequence;
A8: dom((seq_const 1)+s1) = NAT by FUNCT_2:def 1;
A9: for n be Nat holds s2.n = ((seq_const 1) + s1).n
proof
let n be Nat;
s2.n = 1 + 1/(2*(n+1)) by A3
.= 1 + s1.n by A2
.= (seq_const 1).n + s1.n by SEQ_1:57
.= ((seq_const 1) + s1).n by A8,ORDINAL1:def 12,VALUED_1:def 1;
hence thesis;
end;
A10: s2 = (seq_const 1) + s1 by A9; then
A11: lim s2 = (lim (seq_const 1)) + lim s1 by A6,SEQ_2:6
.= 1 + 0 by A6;
A12: for n be Nat holds s3.n <> 0
proof
let n be Nat;
s3.n = (s2.n)*PI by A4 .= (1 + 1/(2*(n+1)))*PI by A3;
hence thesis by Lm9;
end;
for n be Nat holds s3.n = (PI(#)s2).n
proof
let n be Nat;
dom (PI(#)s2) = NAT by FUNCT_2:def 1; then
(PI(#)s2).n = PI*(s2.n) by ORDINAL1:def 12,VALUED_1:def 5
.= s3.n by A4;
hence thesis;
end; then
A15: s3 = PI(#)s2; then
A16: lim s3 = PI*(lim s2) by A10,A6,SEQ_2:8 .= PI by A11;
for n be Nat holds w_seq.n = (s3").n
proof
let n be Nat;
A17: s3.n = (s2.n)*PI by A4 .= (1 + 1/(2*(n+1)))*PI by A3;
(s3.n)" = 1/((1 + 1/(2*(n+1)))*PI) by A17 .= w_seq.n by Def8;
hence thesis by VALUED_1:10;
end; then
w_seq = s3";
hence thesis
by SEQ_2:21,22,SEQ_1:5,A12,A10,A6,A15,A16,COMPTRIG:5;
end;
theorem Th48:
lim Wallis_Seq = 1/PI & Wallis_Seq is convergent
proof
for r be Real st r > 0 ex n0 be Nat st for n be Nat st n0 <= n holds
|. Wallis_Seq.n - 1/PI .| < r
proof
let r be Real;
assume r > 0; then
consider n1 be Nat such that
A2: for m be Nat st n1 <= m holds |. w_seq.m - 1/PI .| < r
by SEQ_2:def 7, Lm10;
ex n0 be Nat st
for m be Nat st n0 <= m holds |. Wallis_Seq.m - 1/PI .| < r
proof
take n1;
let m be Nat;
assume n1 <= m; then
A4: |. w_seq.m - 1/PI .| < r by A2;
A5: w_seq.m = 1/((1+1/(2*(m+1)))*PI) by Def8;
A6: Wallis_Seq.m
= (Product(odd-seq(m+1))|^2/(Product(even-seq(m+1)))|^2)*(m+1)
by Def7; then
A7: 1/PI - Wallis_Seq.m >= 0 by Th47,XREAL_1:48;
A8: 1/PI - w_seq.m > 0 by Lm9,A5;
A9: |. Wallis_Seq.m - 1/PI .| = |.1/PI - Wallis_Seq.m.| by COMPLEX1:60
.= 1/PI - Wallis_Seq.m by A7,ABSVALUE:def 1;
|. w_seq.m - 1/PI .| = |. 1/PI - w_seq.m .| by COMPLEX1:60
.= 1/PI - w_seq.m by A8,ABSVALUE:def 1; then
|. Wallis_Seq.m - 1/PI .| <= |. w_seq.m - 1/PI .|
by A9,XREAL_1:10,A5,A6,Th45;
hence thesis by A4,XXREAL_0:2;
end;
hence thesis;
end; then
consider a be Real such that
A11: a = 1/PI and
A12: for r be Real st r > 0 ex n0 be Nat st for n be Nat st n0 <= n holds
|. Wallis_Seq.n - a .| < r;
Wallis_Seq is convergent by A12;
hence thesis by A11,A12,SEQ_2:def 7;
end;
theorem Th49:
Wallis_Seq is positive-yielding
proof
A1: for k be Nat holds Wallis_Seq.k > 0
proof
let k be Nat;
Wallis_Seq.k
= (Product(odd-seq(k+1))|^2/(Product(even-seq(k+1)))|^2)*(k+1) by Def7;
hence thesis;
end;
for r being Real st r in rng Wallis_Seq holds 0 < r
proof
let r be Real;
assume r in rng Wallis_Seq; then
ex x be object st x in dom Wallis_Seq & r = (Wallis_Seq).x
by FUNCT_1:def 3;
hence thesis by A1;
end;
hence thesis by PARTFUN3:def 1;
end;
registration
cluster Wallis_Seq -> positive-yielding;
coherence by Th49;
end;
theorem Th50:
for seq be positive-yielding Real_Sequence st seq is convergent holds
sqrt seq is convergent & lim sqrt seq = sqrt lim seq
proof
let seq be positive-yielding Real_Sequence;
assume
A1: seq is convergent; then
consider a be Real such that
A2: for r be Real st 0 < r ex n be Nat st for m be Nat st n <= m holds
|. seq.m -a .| < r;
A3: for k be Nat holds seq.k >= 0;
A4: a = lim seq by A1,A2,SEQ_2:def 7;
A5: for k be Nat holds sqrt(seq.k) = (sqrt seq).k
proof
let k be Nat;
dom sqrt seq = NAT by FUNCT_2:def 1;
hence thesis by PARTFUN3:def 5,ORDINAL1:def 12;
end;
sqrt seq is convergent & lim sqrt seq = sqrt lim seq
proof
for r1 be Real st 0 < r1 ex n be Nat st for m be Nat st n <= m holds
|. (sqrt seq).m - sqrt a .| < r1
proof
let r1 be Real;
assume
A7: 0 < r1;
per cases by A1,A3,A4,SEQ_2:17;
suppose
A8: a = 0;
consider n0 be Nat such that
A9: for k be Nat st n0 <= k holds |. seq.k -a .| < r1^2 by A2,A7;
for m be Nat st n0 <= m holds |. (sqrt seq).m - sqrt a .| < r1
proof
let m be Nat;
assume
A10: n0 <= m;
A11: seq.m > 0 & (sqrt seq).m = sqrt (seq.m) by Lm11, A5;
|. seq.m -a .| = seq.m by A8; then
seq.m < r1^2 by A9,A10; then
(sqrt seq).m < sqrt r1^2 by A11,SQUARE_1:27;
hence thesis by A8,A7,SQUARE_1:22;
end;
hence thesis;
end;
suppose
A14: a > 0;
reconsider sqa = sqrt a as Real;
consider n0 be Nat such that
A15: for k be Nat st n0 <= k holds |. seq.k -a .| < sqa*r1
by A2,A14,A7;
for m be Nat st n0 <= m holds |. (sqrt seq).m - sqrt a .| < r1
proof
let m be Nat;
assume n0 <= m; then
A18: |. seq.m -a .| < sqa*r1 by A15;
set sqs1 = (sqrt seq).m;
A17: seq.m > 0 & (sqrt seq).m = sqrt (seq.m) by Lm11, A5;
A19: sqrt a < (sqrt seq).m + sqrt a by Lm11, XREAL_1:29;
A20: |. sqa .| = sqa by A14,COMPLEX1:43; then
A21: |. sqrt a .| < |.(sqrt seq).m + sqrt a .|
by A19,A14,COMPLEX1:43;
(seq.m -a)/(sqs1 + sqa)
= (sqs1 - sqa)*(sqs1 + sqa)*(1/(sqs1 + sqa))
by A17,A14,SQUARE_1:35
.= (sqs1 - sqa) by A14,XCMPLX_1:107; then
A22: |. sqs1 - sqa .|
= |. (seq.m -a).|/|.(sqs1 + sqa) .| by COMPLEX1:67;
0 <= |. (seq.m -a).| by COMPLEX1:46; then
A23: |. (seq.m -a).|/|.(sqs1 + sqa) .| <= |.(seq.m -a).|/|. sqa .|
by XREAL_1:118, A14,A21;
A24: (sqa*r1)/sqa = r1 by A14,XCMPLX_1:89;
|.(seq.m -a).|/|. sqa .| < (sqa*r1)/sqa
by A14,A18,A20,XREAL_1:74;
hence thesis by A22,A24,A23,XXREAL_0:2;
end;
hence thesis;
end;
end; then
consider x be Real such that
A26: x = sqrt a and
A27: for r1 be Real st 0 < r1 ex n be Nat st for m be Nat st n <= m holds
|. (sqrt seq).m - x .| < r1;
sqrt seq is convergent by A27; then
lim sqrt seq = sqrt a by A26,A27,SEQ_2:def 7
.= sqrt lim seq by A1,A2, SEQ_2:def 7;
hence thesis by A27;
end;
hence thesis;
end;
theorem
lim sqrt Wallis_Seq = 1/sqrt(PI)
proof
lim sqrt Wallis_Seq = sqrt (1/PI) by Th48,Th50;
hence thesis by SQUARE_1:32,COMPTRIG:5;
end;
theorem
for n be non zero Nat holds
(sqrt Wallis_Seq).(n-'1) = sqrt(n)*((2*n)!)/((4|^n)*((n!)|^2))
proof
let n be non zero Nat;
A1: (n -' 1) + 1 = n by XREAL_1:235,NAT_1:14;
A2: ((2|^n)*(n!))*((2|^n)*(n!)) = (n!)*(2|^n*2|^n)*(n!)
.= ((n!)*((2*2)|^n))*(n!) by NEWTON:7
.= (4|^n)*((n!)*(n!))
.= (4|^n)*((n!)|^2) by POLYEQ_5:1;
set Podd = Product odd-seq n;
set Peven = Product even-seq n;
Podd = ((2*n)!)/((2|^n)*(n!)) by Th12; then
A4: Podd/Peven = (((2*n)!)/((2|^n)*(n!)))/((2|^n)*(n!)) by Th11
.= ((2*n)!)/((4|^n)*((n!)|^2)) by A2,XCMPLX_1:78;
dom sqrt Wallis_Seq = NAT by FUNCT_2:def 1; then
(sqrt Wallis_Seq).(n-'1) = sqrt(Wallis_Seq.(n-'1)) by PARTFUN3:def 5
.= sqrt((Podd|^2/(Peven)|^2)*n) by A1,Def7
.= sqrt((Podd|^2/(Peven)|^2)) * sqrt(n) by SQUARE_1:29
.= (sqrt(Podd|^2)/sqrt(Peven|^2)) * sqrt(n) by SQUARE_1:30
.= (((2*n)!)/((4|^n)*((n!)|^2)))*sqrt(n) by A4
.= (sqrt(n)*((2*n)!))/((4|^n)*((n!)|^2));
hence thesis;
end;