let n be non zero Nat; (sqrt Wallis_Seq) . (n -' 1) = ((sqrt n) * ((2 * n) !)) / ((4 |^ n) * ((n !) |^ 2))
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);
Product (odd-seq n) = ((2 * n) !) / ((2 |^ n) * (n !))
by Th12;
then A4: (Product (odd-seq n)) / (Product (even-seq n)) =
(((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 ((((Product (odd-seq n)) |^ 2) / ((Product (even-seq n)) |^ 2)) * n)
by A1, Def7
.=
(sqrt (((Product (odd-seq n)) |^ 2) / ((Product (even-seq n)) |^ 2))) * (sqrt n)
by SQUARE_1:29
.=
((sqrt ((Product (odd-seq n)) |^ 2)) / (sqrt ((Product (even-seq n)) |^ 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
(sqrt Wallis_Seq) . (n -' 1) = ((sqrt n) * ((2 * n) !)) / ((4 |^ n) * ((n !) |^ 2))
; verum