# 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 )`
` |-  ( j e. NN -> ( ( 2 x. j ) + 1 ) e. CC )`
61 0red
` |-  ( j e. NN -> 0 e. RR )`
` |-  ( 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+ )`
` |-  ( 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+ )`
` |-  ( ( n e. NN /\ j e. ( 1 ... n ) ) -> ( F ` j ) e. RR+ )`
96 rpmulcl
` |-  ( ( j e. RR+ /\ w e. RR+ ) -> ( j x. w ) e. RR+ )`
` |-  ( ( 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 ffvelrnda
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 mulid1i
` |-  ( ( 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 } ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 )`