Metamath Proof Explorer

Theorem wallispilem5

Description: The sequence H converges to 1. (Contributed by Glauco Siliprandi, 30-Jun-2017)

Ref Expression
Hypotheses wallispilem5.1 
|- F = ( k e. NN |-> ( ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) )
wallispilem5.2 
|- I = ( n e. NN0 |-> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ n ) _d x )
wallispilem5.3 
|- G = ( n e. NN |-> ( ( I ` ( 2 x. n ) ) / ( I ` ( ( 2 x. n ) + 1 ) ) ) )
wallispilem5.4 
|- H = ( n e. NN |-> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) )
wallispilem5.5 
|- L = ( n e. NN |-> ( ( ( 2 x. n ) + 1 ) / ( 2 x. n ) ) )
Assertion wallispilem5 
|- H ~~> 1

Proof

Step Hyp Ref Expression
1 wallispilem5.1 
 |-  F = ( k e. NN |-> ( ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) )
2 wallispilem5.2 
 |-  I = ( n e. NN0 |-> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ n ) _d x )
3 wallispilem5.3 
 |-  G = ( n e. NN |-> ( ( I ` ( 2 x. n ) ) / ( I ` ( ( 2 x. n ) + 1 ) ) ) )
4 wallispilem5.4 
 |-  H = ( n e. NN |-> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) )
5 wallispilem5.5 
 |-  L = ( n e. NN |-> ( ( ( 2 x. n ) + 1 ) / ( 2 x. n ) ) )
6 1 2 3 4 wallispilem4 
 |-  G = H
7 nnuz 
 |-  NN = ( ZZ>= ` 1 )
8 1zzd 
 |-  ( T. -> 1 e. ZZ )
9 2cnd 
 |-  ( T. -> 2 e. CC )
10 2ne0 
 |-  2 =/= 0
11 10 a1i 
 |-  ( T. -> 2 =/= 0 )
12 1cnd 
 |-  ( T. -> 1 e. CC )
13 5 9 11 12 clim1fr1 
 |-  ( T. -> L ~~> 1 )
14 nnex 
 |-  NN e. _V
15 14 mptex 
 |-  ( n e. NN |-> ( ( I ` ( 2 x. n ) ) / ( I ` ( ( 2 x. n ) + 1 ) ) ) ) e. _V
16 3 15 eqeltri 
 |-  G e. _V
17 16 a1i 
 |-  ( T. -> G e. _V )
18 2nn0 
 |-  2 e. NN0
19 18 a1i 
 |-  ( n e. NN -> 2 e. NN0 )
20 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
21 19 20 nn0mulcld 
 |-  ( n e. NN -> ( 2 x. n ) e. NN0 )
22 1nn0 
 |-  1 e. NN0
23 22 a1i 
 |-  ( n e. NN -> 1 e. NN0 )
24 21 23 nn0addcld 
 |-  ( n e. NN -> ( ( 2 x. n ) + 1 ) e. NN0 )
25 24 nn0red 
 |-  ( n e. NN -> ( ( 2 x. n ) + 1 ) e. RR )
26 21 nn0red 
 |-  ( n e. NN -> ( 2 x. n ) e. RR )
27 2cnd 
 |-  ( n e. NN -> 2 e. CC )
28 nncn 
 |-  ( n e. NN -> n e. CC )
29 10 a1i 
 |-  ( n e. NN -> 2 =/= 0 )
30 nnne0 
 |-  ( n e. NN -> n =/= 0 )
31 27 28 29 30 mulne0d 
 |-  ( n e. NN -> ( 2 x. n ) =/= 0 )
32 25 26 31 redivcld 
 |-  ( n e. NN -> ( ( ( 2 x. n ) + 1 ) / ( 2 x. n ) ) e. RR )
33 5 32 fmpti 
 |-  L : NN --> RR
34 33 a1i 
 |-  ( T. -> L : NN --> RR )
35 34 ffvelcdmda 
 |-  ( ( T. /\ k e. NN ) -> ( L ` k ) e. RR )
36 2 wallispilem3 
 |-  ( ( 2 x. n ) e. NN0 -> ( I ` ( 2 x. n ) ) e. RR+ )
37 21 36 syl 
 |-  ( n e. NN -> ( I ` ( 2 x. n ) ) e. RR+ )
38 37 rpred 
 |-  ( n e. NN -> ( I ` ( 2 x. n ) ) e. RR )
39 2 wallispilem3 
 |-  ( ( ( 2 x. n ) + 1 ) e. NN0 -> ( I ` ( ( 2 x. n ) + 1 ) ) e. RR+ )
40 24 39 syl 
 |-  ( n e. NN -> ( I ` ( ( 2 x. n ) + 1 ) ) e. RR+ )
41 38 40 rerpdivcld 
 |-  ( n e. NN -> ( ( I ` ( 2 x. n ) ) / ( I ` ( ( 2 x. n ) + 1 ) ) ) e. RR )
42 3 41 fmpti 
 |-  G : NN --> RR
43 42 a1i 
 |-  ( T. -> G : NN --> RR )
44 43 ffvelcdmda 
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) e. RR )
45 18 a1i 
 |-  ( k e. NN -> 2 e. NN0 )
46 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
47 45 46 nn0mulcld 
 |-  ( k e. NN -> ( 2 x. k ) e. NN0 )
48 2 wallispilem3 
 |-  ( ( 2 x. k ) e. NN0 -> ( I ` ( 2 x. k ) ) e. RR+ )
49 47 48 syl 
 |-  ( k e. NN -> ( I ` ( 2 x. k ) ) e. RR+ )
50 49 rpred 
 |-  ( k e. NN -> ( I ` ( 2 x. k ) ) e. RR )
51 2nn 
 |-  2 e. NN
52 51 a1i 
 |-  ( k e. NN -> 2 e. NN )
53 id 
 |-  ( k e. NN -> k e. NN )
54 52 53 nnmulcld 
 |-  ( k e. NN -> ( 2 x. k ) e. NN )
55 nnm1nn0 
 |-  ( ( 2 x. k ) e. NN -> ( ( 2 x. k ) - 1 ) e. NN0 )
56 54 55 syl 
 |-  ( k e. NN -> ( ( 2 x. k ) - 1 ) e. NN0 )
57 2 wallispilem3 
 |-  ( ( ( 2 x. k ) - 1 ) e. NN0 -> ( I ` ( ( 2 x. k ) - 1 ) ) e. RR+ )
58 56 57 syl 
 |-  ( k e. NN -> ( I ` ( ( 2 x. k ) - 1 ) ) e. RR+ )
59 58 rpred 
 |-  ( k e. NN -> ( I ` ( ( 2 x. k ) - 1 ) ) e. RR )
60 22 a1i 
 |-  ( k e. NN -> 1 e. NN0 )
61 47 60 nn0addcld 
 |-  ( k e. NN -> ( ( 2 x. k ) + 1 ) e. NN0 )
62 2 wallispilem3 
 |-  ( ( ( 2 x. k ) + 1 ) e. NN0 -> ( I ` ( ( 2 x. k ) + 1 ) ) e. RR+ )
63 61 62 syl 
 |-  ( k e. NN -> ( I ` ( ( 2 x. k ) + 1 ) ) e. RR+ )
64 2cnd 
 |-  ( k e. NN -> 2 e. CC )
65 nncn 
 |-  ( k e. NN -> k e. CC )
66 64 65 mulcld 
 |-  ( k e. NN -> ( 2 x. k ) e. CC )
67 1cnd 
 |-  ( k e. NN -> 1 e. CC )
68 66 67 npcand 
 |-  ( k e. NN -> ( ( ( 2 x. k ) - 1 ) + 1 ) = ( 2 x. k ) )
69 68 fveq2d 
 |-  ( k e. NN -> ( I ` ( ( ( 2 x. k ) - 1 ) + 1 ) ) = ( I ` ( 2 x. k ) ) )
70 2 56 wallispilem1 
 |-  ( k e. NN -> ( I ` ( ( ( 2 x. k ) - 1 ) + 1 ) ) <_ ( I ` ( ( 2 x. k ) - 1 ) ) )
71 69 70 eqbrtrrd 
 |-  ( k e. NN -> ( I ` ( 2 x. k ) ) <_ ( I ` ( ( 2 x. k ) - 1 ) ) )
72 50 59 63 71 lediv1dd 
 |-  ( k e. NN -> ( ( I ` ( 2 x. k ) ) / ( I ` ( ( 2 x. k ) + 1 ) ) ) <_ ( ( I ` ( ( 2 x. k ) - 1 ) ) / ( I ` ( ( 2 x. k ) + 1 ) ) ) )
73 66 67 addcld 
 |-  ( k e. NN -> ( ( 2 x. k ) + 1 ) e. CC )
74 10 a1i 
 |-  ( k e. NN -> 2 =/= 0 )
75 nnne0 
 |-  ( k e. NN -> k =/= 0 )
76 64 65 74 75 mulne0d 
 |-  ( k e. NN -> ( 2 x. k ) =/= 0 )
77 73 66 76 divcld 
 |-  ( k e. NN -> ( ( ( 2 x. k ) + 1 ) / ( 2 x. k ) ) e. CC )
78 63 rpcnd 
 |-  ( k e. NN -> ( I ` ( ( 2 x. k ) + 1 ) ) e. CC )
79 63 rpne0d 
 |-  ( k e. NN -> ( I ` ( ( 2 x. k ) + 1 ) ) =/= 0 )
80 77 78 79 divcan4d 
 |-  ( k e. NN -> ( ( ( ( ( 2 x. k ) + 1 ) / ( 2 x. k ) ) x. ( I ` ( ( 2 x. k ) + 1 ) ) ) / ( I ` ( ( 2 x. k ) + 1 ) ) ) = ( ( ( 2 x. k ) + 1 ) / ( 2 x. k ) ) )
81 2re 
 |-  2 e. RR
82 81 a1i 
 |-  ( k e. NN -> 2 e. RR )
83 nnre 
 |-  ( k e. NN -> k e. RR )
84 82 83 remulcld 
 |-  ( k e. NN -> ( 2 x. k ) e. RR )
85 1red 
 |-  ( k e. NN -> 1 e. RR )
86 84 85 readdcld 
 |-  ( k e. NN -> ( ( 2 x. k ) + 1 ) e. RR )
87 45 nn0ge0d 
 |-  ( k e. NN -> 0 <_ 2 )
88 nnge1 
 |-  ( k e. NN -> 1 <_ k )
89 82 83 87 88 lemulge11d 
 |-  ( k e. NN -> 2 <_ ( 2 x. k ) )
90 84 ltp1d 
 |-  ( k e. NN -> ( 2 x. k ) < ( ( 2 x. k ) + 1 ) )
91 82 84 86 89 90 lelttrd 
 |-  ( k e. NN -> 2 < ( ( 2 x. k ) + 1 ) )
92 82 86 91 ltled 
 |-  ( k e. NN -> 2 <_ ( ( 2 x. k ) + 1 ) )
93 45 nn0zd 
 |-  ( k e. NN -> 2 e. ZZ )
94 61 nn0zd 
 |-  ( k e. NN -> ( ( 2 x. k ) + 1 ) e. ZZ )
95 eluz 
 |-  ( ( 2 e. ZZ /\ ( ( 2 x. k ) + 1 ) e. ZZ ) -> ( ( ( 2 x. k ) + 1 ) e. ( ZZ>= ` 2 ) <-> 2 <_ ( ( 2 x. k ) + 1 ) ) )
96 93 94 95 syl2anc 
 |-  ( k e. NN -> ( ( ( 2 x. k ) + 1 ) e. ( ZZ>= ` 2 ) <-> 2 <_ ( ( 2 x. k ) + 1 ) ) )
97 92 96 mpbird 
 |-  ( k e. NN -> ( ( 2 x. k ) + 1 ) e. ( ZZ>= ` 2 ) )
98 2 97 itgsinexp 
 |-  ( k e. NN -> ( I ` ( ( 2 x. k ) + 1 ) ) = ( ( ( ( ( 2 x. k ) + 1 ) - 1 ) / ( ( 2 x. k ) + 1 ) ) x. ( I ` ( ( ( 2 x. k ) + 1 ) - 2 ) ) ) )
99 66 67 pncand 
 |-  ( k e. NN -> ( ( ( 2 x. k ) + 1 ) - 1 ) = ( 2 x. k ) )
100 99 oveq1d 
 |-  ( k e. NN -> ( ( ( ( 2 x. k ) + 1 ) - 1 ) / ( ( 2 x. k ) + 1 ) ) = ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) )
101 1e2m1 
 |-  1 = ( 2 - 1 )
102 101 a1i 
 |-  ( k e. NN -> 1 = ( 2 - 1 ) )
103 102 oveq2d 
 |-  ( k e. NN -> ( ( 2 x. k ) - 1 ) = ( ( 2 x. k ) - ( 2 - 1 ) ) )
104 66 64 67 subsub3d 
 |-  ( k e. NN -> ( ( 2 x. k ) - ( 2 - 1 ) ) = ( ( ( 2 x. k ) + 1 ) - 2 ) )
105 103 104 eqtr2d 
 |-  ( k e. NN -> ( ( ( 2 x. k ) + 1 ) - 2 ) = ( ( 2 x. k ) - 1 ) )
106 105 fveq2d 
 |-  ( k e. NN -> ( I ` ( ( ( 2 x. k ) + 1 ) - 2 ) ) = ( I ` ( ( 2 x. k ) - 1 ) ) )
107 100 106 oveq12d 
 |-  ( k e. NN -> ( ( ( ( ( 2 x. k ) + 1 ) - 1 ) / ( ( 2 x. k ) + 1 ) ) x. ( I ` ( ( ( 2 x. k ) + 1 ) - 2 ) ) ) = ( ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) x. ( I ` ( ( 2 x. k ) - 1 ) ) ) )
108 98 107 eqtrd 
 |-  ( k e. NN -> ( I ` ( ( 2 x. k ) + 1 ) ) = ( ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) x. ( I ` ( ( 2 x. k ) - 1 ) ) ) )
109 108 oveq2d 
 |-  ( k e. NN -> ( ( ( ( 2 x. k ) + 1 ) / ( 2 x. k ) ) x. ( I ` ( ( 2 x. k ) + 1 ) ) ) = ( ( ( ( 2 x. k ) + 1 ) / ( 2 x. k ) ) x. ( ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) x. ( I ` ( ( 2 x. k ) - 1 ) ) ) ) )
110 54 peano2nnd 
 |-  ( k e. NN -> ( ( 2 x. k ) + 1 ) e. NN )
111 110 nnne0d 
 |-  ( k e. NN -> ( ( 2 x. k ) + 1 ) =/= 0 )
112 66 73 111 divcld 
 |-  ( k e. NN -> ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) e. CC )
113 58 rpcnd 
 |-  ( k e. NN -> ( I ` ( ( 2 x. k ) - 1 ) ) e. CC )
114 77 112 113 mulassd 
 |-  ( k e. NN -> ( ( ( ( ( 2 x. k ) + 1 ) / ( 2 x. k ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) x. ( I ` ( ( 2 x. k ) - 1 ) ) ) = ( ( ( ( 2 x. k ) + 1 ) / ( 2 x. k ) ) x. ( ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) x. ( I ` ( ( 2 x. k ) - 1 ) ) ) ) )
115 73 66 111 76 divcan6d 
 |-  ( k e. NN -> ( ( ( ( 2 x. k ) + 1 ) / ( 2 x. k ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) = 1 )
116 115 oveq1d 
 |-  ( k e. NN -> ( ( ( ( ( 2 x. k ) + 1 ) / ( 2 x. k ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) x. ( I ` ( ( 2 x. k ) - 1 ) ) ) = ( 1 x. ( I ` ( ( 2 x. k ) - 1 ) ) ) )
117 113 mullidd 
 |-  ( k e. NN -> ( 1 x. ( I ` ( ( 2 x. k ) - 1 ) ) ) = ( I ` ( ( 2 x. k ) - 1 ) ) )
118 116 117 eqtrd 
 |-  ( k e. NN -> ( ( ( ( ( 2 x. k ) + 1 ) / ( 2 x. k ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) x. ( I ` ( ( 2 x. k ) - 1 ) ) ) = ( I ` ( ( 2 x. k ) - 1 ) ) )
119 109 114 118 3eqtr2d 
 |-  ( k e. NN -> ( ( ( ( 2 x. k ) + 1 ) / ( 2 x. k ) ) x. ( I ` ( ( 2 x. k ) + 1 ) ) ) = ( I ` ( ( 2 x. k ) - 1 ) ) )
120 119 oveq1d 
 |-  ( k e. NN -> ( ( ( ( ( 2 x. k ) + 1 ) / ( 2 x. k ) ) x. ( I ` ( ( 2 x. k ) + 1 ) ) ) / ( I ` ( ( 2 x. k ) + 1 ) ) ) = ( ( I ` ( ( 2 x. k ) - 1 ) ) / ( I ` ( ( 2 x. k ) + 1 ) ) ) )
121 80 120 eqtr3d 
 |-  ( k e. NN -> ( ( ( 2 x. k ) + 1 ) / ( 2 x. k ) ) = ( ( I ` ( ( 2 x. k ) - 1 ) ) / ( I ` ( ( 2 x. k ) + 1 ) ) ) )
122 72 121 breqtrrd 
 |-  ( k e. NN -> ( ( I ` ( 2 x. k ) ) / ( I ` ( ( 2 x. k ) + 1 ) ) ) <_ ( ( ( 2 x. k ) + 1 ) / ( 2 x. k ) ) )
123 49 63 rpdivcld 
 |-  ( k e. NN -> ( ( I ` ( 2 x. k ) ) / ( I ` ( ( 2 x. k ) + 1 ) ) ) e. RR+ )
124 nfcv 
 |-  F/_ n k
125 nfmpt1 
 |-  F/_ n ( n e. NN0 |-> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ n ) _d x )
126 2 125 nfcxfr 
 |-  F/_ n I
127 nfcv 
 |-  F/_ n ( 2 x. k )
128 126 127 nffv 
 |-  F/_ n ( I ` ( 2 x. k ) )
129 nfcv 
 |-  F/_ n /
130 nfcv 
 |-  F/_ n ( ( 2 x. k ) + 1 )
131 126 130 nffv 
 |-  F/_ n ( I ` ( ( 2 x. k ) + 1 ) )
132 128 129 131 nfov 
 |-  F/_ n ( ( I ` ( 2 x. k ) ) / ( I ` ( ( 2 x. k ) + 1 ) ) )
133 oveq2 
 |-  ( n = k -> ( 2 x. n ) = ( 2 x. k ) )
134 133 fveq2d 
 |-  ( n = k -> ( I ` ( 2 x. n ) ) = ( I ` ( 2 x. k ) ) )
135 133 fvoveq1d 
 |-  ( n = k -> ( I ` ( ( 2 x. n ) + 1 ) ) = ( I ` ( ( 2 x. k ) + 1 ) ) )
136 134 135 oveq12d 
 |-  ( n = k -> ( ( I ` ( 2 x. n ) ) / ( I ` ( ( 2 x. n ) + 1 ) ) ) = ( ( I ` ( 2 x. k ) ) / ( I ` ( ( 2 x. k ) + 1 ) ) ) )
137 124 132 136 3 fvmptf 
 |-  ( ( k e. NN /\ ( ( I ` ( 2 x. k ) ) / ( I ` ( ( 2 x. k ) + 1 ) ) ) e. RR+ ) -> ( G ` k ) = ( ( I ` ( 2 x. k ) ) / ( I ` ( ( 2 x. k ) + 1 ) ) ) )
138 123 137 mpdan 
 |-  ( k e. NN -> ( G ` k ) = ( ( I ` ( 2 x. k ) ) / ( I ` ( ( 2 x. k ) + 1 ) ) ) )
139 5 a1i 
 |-  ( k e. NN -> L = ( n e. NN |-> ( ( ( 2 x. n ) + 1 ) / ( 2 x. n ) ) ) )
140 simpr 
 |-  ( ( k e. NN /\ n = k ) -> n = k )
141 140 oveq2d 
 |-  ( ( k e. NN /\ n = k ) -> ( 2 x. n ) = ( 2 x. k ) )
142 141 oveq1d 
 |-  ( ( k e. NN /\ n = k ) -> ( ( 2 x. n ) + 1 ) = ( ( 2 x. k ) + 1 ) )
143 142 141 oveq12d 
 |-  ( ( k e. NN /\ n = k ) -> ( ( ( 2 x. n ) + 1 ) / ( 2 x. n ) ) = ( ( ( 2 x. k ) + 1 ) / ( 2 x. k ) ) )
144 139 143 53 77 fvmptd 
 |-  ( k e. NN -> ( L ` k ) = ( ( ( 2 x. k ) + 1 ) / ( 2 x. k ) ) )
145 122 138 144 3brtr4d 
 |-  ( k e. NN -> ( G ` k ) <_ ( L ` k ) )
146 145 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) <_ ( L ` k ) )
147 78 79 dividd 
 |-  ( k e. NN -> ( ( I ` ( ( 2 x. k ) + 1 ) ) / ( I ` ( ( 2 x. k ) + 1 ) ) ) = 1 )
148 63 rpred 
 |-  ( k e. NN -> ( I ` ( ( 2 x. k ) + 1 ) ) e. RR )
149 2 47 wallispilem1 
 |-  ( k e. NN -> ( I ` ( ( 2 x. k ) + 1 ) ) <_ ( I ` ( 2 x. k ) ) )
150 148 50 63 149 lediv1dd 
 |-  ( k e. NN -> ( ( I ` ( ( 2 x. k ) + 1 ) ) / ( I ` ( ( 2 x. k ) + 1 ) ) ) <_ ( ( I ` ( 2 x. k ) ) / ( I ` ( ( 2 x. k ) + 1 ) ) ) )
151 147 150 eqbrtrrd 
 |-  ( k e. NN -> 1 <_ ( ( I ` ( 2 x. k ) ) / ( I ` ( ( 2 x. k ) + 1 ) ) ) )
152 151 138 breqtrrd 
 |-  ( k e. NN -> 1 <_ ( G ` k ) )
153 152 adantl 
 |-  ( ( T. /\ k e. NN ) -> 1 <_ ( G ` k ) )
154 7 8 13 17 35 44 146 153 climsqz2 
 |-  ( T. -> G ~~> 1 )
155 154 mptru 
 |-  G ~~> 1
156 6 155 eqbrtrri 
 |-  H ~~> 1