# 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}=\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)$
wallispilem5.2 ${⊢}{I}=\left({n}\in {ℕ}_{0}⟼{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{sin}{x}}^{{n}}d{x}\right)$
wallispilem5.3 ${⊢}{G}=\left({n}\in ℕ⟼\frac{{I}\left(2{n}\right)}{{I}\left(2{n}+1\right)}\right)$
wallispilem5.4 ${⊢}{H}=\left({n}\in ℕ⟼\left(\frac{\mathrm{\pi }}{2}\right)\left(\frac{1}{seq1\left(×,{F}\right)\left({n}\right)}\right)\right)$
wallispilem5.5 ${⊢}{L}=\left({n}\in ℕ⟼\frac{2{n}+1}{2{n}}\right)$
Assertion wallispilem5 ${⊢}{H}⇝1$

### Proof

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