This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wallispi

Description: Wallis' formula for π : Wallis' product converges to π / 2 . (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses wallispi.1 
|- F = ( k e. NN |-> ( ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) )
wallispi.2 
|- W = ( n e. NN |-> ( seq 1 ( x. , F ) ` n ) )
Assertion wallispi 
|- W ~~> ( _pi / 2 )

Proof

Step Hyp Ref Expression
1 wallispi.1 
 |-  F = ( k e. NN |-> ( ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) )
2 wallispi.2 
 |-  W = ( n e. NN |-> ( seq 1 ( x. , F ) ` n ) )
3 nnuz 
 |-  NN = ( ZZ>= ` 1 )
4 1zzd 
 |-  ( T. -> 1 e. ZZ )
5 eqid 
 |-  ( n e. NN0 |-> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ n ) _d x ) = ( n e. NN0 |-> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ n ) _d x )
6 eqid 
 |-  ( n e. NN |-> ( ( ( n e. NN0 |-> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ n ) _d x ) ` ( 2 x. n ) ) / ( ( n e. NN0 |-> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ n ) _d x ) ` ( ( 2 x. n ) + 1 ) ) ) ) = ( n e. NN |-> ( ( ( n e. NN0 |-> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ n ) _d x ) ` ( 2 x. n ) ) / ( ( n e. NN0 |-> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ n ) _d x ) ` ( ( 2 x. n ) + 1 ) ) ) )
7 eqid 
 |-  ( n e. NN |-> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ) = ( n e. NN |-> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) )
8 eqid 
 |-  ( n e. NN |-> ( ( ( 2 x. n ) + 1 ) / ( 2 x. n ) ) ) = ( n e. NN |-> ( ( ( 2 x. n ) + 1 ) / ( 2 x. n ) ) )
9 1 5 6 7 8 wallispilem5 
 |-  ( n e. NN |-> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ) ~~> 1
10 9 a1i 
 |-  ( T. -> ( n e. NN |-> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ) ~~> 1 )
11 2cnd 
 |-  ( T. -> 2 e. CC )
12 picn 
 |-  _pi e. CC
13 12 a1i 
 |-  ( T. -> _pi e. CC )
14 pire 
 |-  _pi e. RR
15 pipos 
 |-  0 < _pi
16 14 15 gt0ne0ii 
 |-  _pi =/= 0
17 16 a1i 
 |-  ( T. -> _pi =/= 0 )
18 11 13 17 divcld 
 |-  ( T. -> ( 2 / _pi ) e. CC )
19 nnex 
 |-  NN e. _V
20 19 mptex 
 |-  ( n e. NN |-> ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) e. _V
21 20 a1i 
 |-  ( T. -> ( n e. NN |-> ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) e. _V )
22 12 a1i 
 |-  ( n e. NN -> _pi e. CC )
23 22 halfcld 
 |-  ( n e. NN -> ( _pi / 2 ) e. CC )
24 elnnuz 
 |-  ( n e. NN <-> n e. ( ZZ>= ` 1 ) )
25 24 biimpi 
 |-  ( n e. NN -> n e. ( ZZ>= ` 1 ) )
26 oveq2 
 |-  ( k = j -> ( 2 x. k ) = ( 2 x. j ) )
27 26 oveq1d 
 |-  ( k = j -> ( ( 2 x. k ) - 1 ) = ( ( 2 x. j ) - 1 ) )
28 26 27 oveq12d 
 |-  ( k = j -> ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) = ( ( 2 x. j ) / ( ( 2 x. j ) - 1 ) ) )
29 26 oveq1d 
 |-  ( k = j -> ( ( 2 x. k ) + 1 ) = ( ( 2 x. j ) + 1 ) )
30 26 29 oveq12d 
 |-  ( k = j -> ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) = ( ( 2 x. j ) / ( ( 2 x. j ) + 1 ) ) )
31 28 30 oveq12d 
 |-  ( k = j -> ( ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) = ( ( ( 2 x. j ) / ( ( 2 x. j ) - 1 ) ) x. ( ( 2 x. j ) / ( ( 2 x. j ) + 1 ) ) ) )
32 elfznn 
 |-  ( j e. ( 1 ... n ) -> j e. NN )
33 2cnd 
 |-  ( j e. NN -> 2 e. CC )
34 nncn 
 |-  ( j e. NN -> j e. CC )
35 33 34 mulcld 
 |-  ( j e. NN -> ( 2 x. j ) e. CC )
36 1cnd 
 |-  ( j e. NN -> 1 e. CC )
37 35 36 subcld 
 |-  ( j e. NN -> ( ( 2 x. j ) - 1 ) e. CC )
38 1red 
 |-  ( j e. NN -> 1 e. RR )
39 1t1e1 
 |-  ( 1 x. 1 ) = 1
40 38 38 remulcld 
 |-  ( j e. NN -> ( 1 x. 1 ) e. RR )
41 2re 
 |-  2 e. RR
42 41 a1i 
 |-  ( j e. NN -> 2 e. RR )
43 42 38 remulcld 
 |-  ( j e. NN -> ( 2 x. 1 ) e. RR )
44 nnre 
 |-  ( j e. NN -> j e. RR )
45 42 44 remulcld 
 |-  ( j e. NN -> ( 2 x. j ) e. RR )
46 1rp 
 |-  1 e. RR+
47 46 a1i 
 |-  ( j e. NN -> 1 e. RR+ )
48 1lt2 
 |-  1 < 2
49 48 a1i 
 |-  ( j e. NN -> 1 < 2 )
50 38 42 47 49 ltmul1dd 
 |-  ( j e. NN -> ( 1 x. 1 ) < ( 2 x. 1 ) )
51 0le2 
 |-  0 <_ 2
52 51 a1i 
 |-  ( j e. NN -> 0 <_ 2 )
53 nnge1 
 |-  ( j e. NN -> 1 <_ j )
54 38 44 42 52 53 lemul2ad 
 |-  ( j e. NN -> ( 2 x. 1 ) <_ ( 2 x. j ) )
55 40 43 45 50 54 ltletrd 
 |-  ( j e. NN -> ( 1 x. 1 ) < ( 2 x. j ) )
56 39 55 eqbrtrrid 
 |-  ( j e. NN -> 1 < ( 2 x. j ) )
57 38 56 gtned 
 |-  ( j e. NN -> ( 2 x. j ) =/= 1 )
58 35 36 57 subne0d 
 |-  ( j e. NN -> ( ( 2 x. j ) - 1 ) =/= 0 )
59 35 37 58 divcld 
 |-  ( j e. NN -> ( ( 2 x. j ) / ( ( 2 x. j ) - 1 ) ) e. CC )
60 35 36 addcld 
 |-  ( j e. NN -> ( ( 2 x. j ) + 1 ) e. CC )
61 0red 
 |-  ( j e. NN -> 0 e. RR )
62 45 38 readdcld 
 |-  ( j e. NN -> ( ( 2 x. j ) + 1 ) e. RR )
63 47 rpgt0d 
 |-  ( j e. NN -> 0 < 1 )
64 2rp 
 |-  2 e. RR+
65 64 a1i 
 |-  ( j e. NN -> 2 e. RR+ )
66 nnrp 
 |-  ( j e. NN -> j e. RR+ )
67 65 66 rpmulcld 
 |-  ( j e. NN -> ( 2 x. j ) e. RR+ )
68 38 67 ltaddrp2d 
 |-  ( j e. NN -> 1 < ( ( 2 x. j ) + 1 ) )
69 61 38 62 63 68 lttrd 
 |-  ( j e. NN -> 0 < ( ( 2 x. j ) + 1 ) )
70 61 69 gtned 
 |-  ( j e. NN -> ( ( 2 x. j ) + 1 ) =/= 0 )
71 35 60 70 divcld 
 |-  ( j e. NN -> ( ( 2 x. j ) / ( ( 2 x. j ) + 1 ) ) e. CC )
72 59 71 mulcld 
 |-  ( j e. NN -> ( ( ( 2 x. j ) / ( ( 2 x. j ) - 1 ) ) x. ( ( 2 x. j ) / ( ( 2 x. j ) + 1 ) ) ) e. CC )
73 32 72 syl 
 |-  ( j e. ( 1 ... n ) -> ( ( ( 2 x. j ) / ( ( 2 x. j ) - 1 ) ) x. ( ( 2 x. j ) / ( ( 2 x. j ) + 1 ) ) ) e. CC )
74 1 31 32 73 fvmptd3 
 |-  ( j e. ( 1 ... n ) -> ( F ` j ) = ( ( ( 2 x. j ) / ( ( 2 x. j ) - 1 ) ) x. ( ( 2 x. j ) / ( ( 2 x. j ) + 1 ) ) ) )
75 64 a1i 
 |-  ( j e. ( 1 ... n ) -> 2 e. RR+ )
76 32 nnrpd 
 |-  ( j e. ( 1 ... n ) -> j e. RR+ )
77 75 76 rpmulcld 
 |-  ( j e. ( 1 ... n ) -> ( 2 x. j ) e. RR+ )
78 45 38 resubcld 
 |-  ( j e. NN -> ( ( 2 x. j ) - 1 ) e. RR )
79 1m1e0 
 |-  ( 1 - 1 ) = 0
80 38 45 38 56 ltsub1dd 
 |-  ( j e. NN -> ( 1 - 1 ) < ( ( 2 x. j ) - 1 ) )
81 79 80 eqbrtrrid 
 |-  ( j e. NN -> 0 < ( ( 2 x. j ) - 1 ) )
82 78 81 elrpd 
 |-  ( j e. NN -> ( ( 2 x. j ) - 1 ) e. RR+ )
83 32 82 syl 
 |-  ( j e. ( 1 ... n ) -> ( ( 2 x. j ) - 1 ) e. RR+ )
84 77 83 rpdivcld 
 |-  ( j e. ( 1 ... n ) -> ( ( 2 x. j ) / ( ( 2 x. j ) - 1 ) ) e. RR+ )
85 41 a1i 
 |-  ( j e. ( 1 ... n ) -> 2 e. RR )
86 32 nnred 
 |-  ( j e. ( 1 ... n ) -> j e. RR )
87 85 86 remulcld 
 |-  ( j e. ( 1 ... n ) -> ( 2 x. j ) e. RR )
88 75 rpge0d 
 |-  ( j e. ( 1 ... n ) -> 0 <_ 2 )
89 76 rpge0d 
 |-  ( j e. ( 1 ... n ) -> 0 <_ j )
90 85 86 88 89 mulge0d 
 |-  ( j e. ( 1 ... n ) -> 0 <_ ( 2 x. j ) )
91 87 90 ge0p1rpd 
 |-  ( j e. ( 1 ... n ) -> ( ( 2 x. j ) + 1 ) e. RR+ )
92 77 91 rpdivcld 
 |-  ( j e. ( 1 ... n ) -> ( ( 2 x. j ) / ( ( 2 x. j ) + 1 ) ) e. RR+ )
93 84 92 rpmulcld 
 |-  ( j e. ( 1 ... n ) -> ( ( ( 2 x. j ) / ( ( 2 x. j ) - 1 ) ) x. ( ( 2 x. j ) / ( ( 2 x. j ) + 1 ) ) ) e. RR+ )
94 74 93 eqeltrd 
 |-  ( j e. ( 1 ... n ) -> ( F ` j ) e. RR+ )
95 94 adantl 
 |-  ( ( n e. NN /\ j e. ( 1 ... n ) ) -> ( F ` j ) e. RR+ )
96 rpmulcl 
 |-  ( ( j e. RR+ /\ w e. RR+ ) -> ( j x. w ) e. RR+ )
97 96 adantl 
 |-  ( ( n e. NN /\ ( j e. RR+ /\ w e. RR+ ) ) -> ( j x. w ) e. RR+ )
98 25 95 97 seqcl 
 |-  ( n e. NN -> ( seq 1 ( x. , F ) ` n ) e. RR+ )
99 98 rpcnd 
 |-  ( n e. NN -> ( seq 1 ( x. , F ) ` n ) e. CC )
100 98 rpne0d 
 |-  ( n e. NN -> ( seq 1 ( x. , F ) ` n ) =/= 0 )
101 99 100 reccld 
 |-  ( n e. NN -> ( 1 / ( seq 1 ( x. , F ) ` n ) ) e. CC )
102 23 101 mulcld 
 |-  ( n e. NN -> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) e. CC )
103 7 102 fmpti 
 |-  ( n e. NN |-> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ) : NN --> CC
104 103 a1i 
 |-  ( T. -> ( n e. NN |-> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ) : NN --> CC )
105 104 ffvelcdmda 
 |-  ( ( T. /\ j e. NN ) -> ( ( n e. NN |-> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ) ` j ) e. CC )
106 fveq2 
 |-  ( n = j -> ( seq 1 ( x. , F ) ` n ) = ( seq 1 ( x. , F ) ` j ) )
107 106 eleq1d 
 |-  ( n = j -> ( ( seq 1 ( x. , F ) ` n ) e. RR+ <-> ( seq 1 ( x. , F ) ` j ) e. RR+ ) )
108 107 98 vtoclga 
 |-  ( j e. NN -> ( seq 1 ( x. , F ) ` j ) e. RR+ )
109 108 rpcnd 
 |-  ( j e. NN -> ( seq 1 ( x. , F ) ` j ) e. CC )
110 108 rpne0d 
 |-  ( j e. NN -> ( seq 1 ( x. , F ) ` j ) =/= 0 )
111 36 109 110 divrecd 
 |-  ( j e. NN -> ( 1 / ( seq 1 ( x. , F ) ` j ) ) = ( 1 x. ( 1 / ( seq 1 ( x. , F ) ` j ) ) ) )
112 12 a1i 
 |-  ( j e. NN -> _pi e. CC )
113 65 rpne0d 
 |-  ( j e. NN -> 2 =/= 0 )
114 16 a1i 
 |-  ( j e. NN -> _pi =/= 0 )
115 33 112 113 114 divcan6d 
 |-  ( j e. NN -> ( ( 2 / _pi ) x. ( _pi / 2 ) ) = 1 )
116 115 eqcomd 
 |-  ( j e. NN -> 1 = ( ( 2 / _pi ) x. ( _pi / 2 ) ) )
117 116 oveq1d 
 |-  ( j e. NN -> ( 1 x. ( 1 / ( seq 1 ( x. , F ) ` j ) ) ) = ( ( ( 2 / _pi ) x. ( _pi / 2 ) ) x. ( 1 / ( seq 1 ( x. , F ) ` j ) ) ) )
118 33 112 114 divcld 
 |-  ( j e. NN -> ( 2 / _pi ) e. CC )
119 112 halfcld 
 |-  ( j e. NN -> ( _pi / 2 ) e. CC )
120 109 110 reccld 
 |-  ( j e. NN -> ( 1 / ( seq 1 ( x. , F ) ` j ) ) e. CC )
121 118 119 120 mulassd 
 |-  ( j e. NN -> ( ( ( 2 / _pi ) x. ( _pi / 2 ) ) x. ( 1 / ( seq 1 ( x. , F ) ` j ) ) ) = ( ( 2 / _pi ) x. ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` j ) ) ) ) )
122 111 117 121 3eqtrd 
 |-  ( j e. NN -> ( 1 / ( seq 1 ( x. , F ) ` j ) ) = ( ( 2 / _pi ) x. ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` j ) ) ) ) )
123 eqidd 
 |-  ( j e. NN -> ( n e. NN |-> ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) = ( n e. NN |-> ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) )
124 106 oveq2d 
 |-  ( n = j -> ( 1 / ( seq 1 ( x. , F ) ` n ) ) = ( 1 / ( seq 1 ( x. , F ) ` j ) ) )
125 124 adantl 
 |-  ( ( j e. NN /\ n = j ) -> ( 1 / ( seq 1 ( x. , F ) ` n ) ) = ( 1 / ( seq 1 ( x. , F ) ` j ) ) )
126 id 
 |-  ( j e. NN -> j e. NN )
127 108 rpreccld 
 |-  ( j e. NN -> ( 1 / ( seq 1 ( x. , F ) ` j ) ) e. RR+ )
128 123 125 126 127 fvmptd 
 |-  ( j e. NN -> ( ( n e. NN |-> ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ` j ) = ( 1 / ( seq 1 ( x. , F ) ` j ) ) )
129 eqidd 
 |-  ( j e. NN -> ( n e. NN |-> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ) = ( n e. NN |-> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ) )
130 125 oveq2d 
 |-  ( ( j e. NN /\ n = j ) -> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` j ) ) ) )
131 119 120 mulcld 
 |-  ( j e. NN -> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` j ) ) ) e. CC )
132 129 130 126 131 fvmptd 
 |-  ( j e. NN -> ( ( n e. NN |-> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ) ` j ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` j ) ) ) )
133 132 oveq2d 
 |-  ( j e. NN -> ( ( 2 / _pi ) x. ( ( n e. NN |-> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ) ` j ) ) = ( ( 2 / _pi ) x. ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` j ) ) ) ) )
134 122 128 133 3eqtr4d 
 |-  ( j e. NN -> ( ( n e. NN |-> ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ` j ) = ( ( 2 / _pi ) x. ( ( n e. NN |-> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ) ` j ) ) )
135 134 adantl 
 |-  ( ( T. /\ j e. NN ) -> ( ( n e. NN |-> ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ` j ) = ( ( 2 / _pi ) x. ( ( n e. NN |-> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ) ` j ) ) )
136 3 4 10 18 21 105 135 climmulc2 
 |-  ( T. -> ( n e. NN |-> ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ~~> ( ( 2 / _pi ) x. 1 ) )
137 2cn 
 |-  2 e. CC
138 137 12 16 divcli 
 |-  ( 2 / _pi ) e. CC
139 138 mulridi 
 |-  ( ( 2 / _pi ) x. 1 ) = ( 2 / _pi )
140 136 139 breqtrdi 
 |-  ( T. -> ( n e. NN |-> ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ~~> ( 2 / _pi ) )
141 2ne0 
 |-  2 =/= 0
142 137 12 141 16 divne0i 
 |-  ( 2 / _pi ) =/= 0
143 142 a1i 
 |-  ( T. -> ( 2 / _pi ) =/= 0 )
144 128 120 eqeltrd 
 |-  ( j e. NN -> ( ( n e. NN |-> ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ` j ) e. CC )
145 109 110 recne0d 
 |-  ( j e. NN -> ( 1 / ( seq 1 ( x. , F ) ` j ) ) =/= 0 )
146 128 145 eqnetrd 
 |-  ( j e. NN -> ( ( n e. NN |-> ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ` j ) =/= 0 )
147 nelsn 
 |-  ( ( ( n e. NN |-> ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ` j ) =/= 0 -> -. ( ( n e. NN |-> ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ` j ) e. { 0 } )
148 146 147 syl 
 |-  ( j e. NN -> -. ( ( n e. NN |-> ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ` j ) e. { 0 } )
149 144 148 eldifd 
 |-  ( j e. NN -> ( ( n e. NN |-> ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ` j ) e. ( CC \ { 0 } ) )
150 149 adantl 
 |-  ( ( T. /\ j e. NN ) -> ( ( n e. NN |-> ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ` j ) e. ( CC \ { 0 } ) )
151 109 110 recrecd 
 |-  ( j e. NN -> ( 1 / ( 1 / ( seq 1 ( x. , F ) ` j ) ) ) = ( seq 1 ( x. , F ) ` j ) )
152 123 125 126 120 fvmptd 
 |-  ( j e. NN -> ( ( n e. NN |-> ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ` j ) = ( 1 / ( seq 1 ( x. , F ) ` j ) ) )
153 152 oveq2d 
 |-  ( j e. NN -> ( 1 / ( ( n e. NN |-> ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ` j ) ) = ( 1 / ( 1 / ( seq 1 ( x. , F ) ` j ) ) ) )
154 106 2 98 fvmpt3 
 |-  ( j e. NN -> ( W ` j ) = ( seq 1 ( x. , F ) ` j ) )
155 151 153 154 3eqtr4rd 
 |-  ( j e. NN -> ( W ` j ) = ( 1 / ( ( n e. NN |-> ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ` j ) ) )
156 155 adantl 
 |-  ( ( T. /\ j e. NN ) -> ( W ` j ) = ( 1 / ( ( n e. NN |-> ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ` j ) ) )
157 19 mptex 
 |-  ( n e. NN |-> ( seq 1 ( x. , F ) ` n ) ) e. _V
158 2 157 eqeltri 
 |-  W e. _V
159 158 a1i 
 |-  ( T. -> W e. _V )
160 3 4 140 143 150 156 159 climrec 
 |-  ( T. -> W ~~> ( 1 / ( 2 / _pi ) ) )
161 160 mptru 
 |-  W ~~> ( 1 / ( 2 / _pi ) )
162 recdiv 
 |-  ( ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( _pi e. CC /\ _pi =/= 0 ) ) -> ( 1 / ( 2 / _pi ) ) = ( _pi / 2 ) )
163 137 141 12 16 162 mp4an 
 |-  ( 1 / ( 2 / _pi ) ) = ( _pi / 2 )
164 161 163 breqtri 
 |-  W ~~> ( _pi / 2 )