Metamath Proof Explorer


Theorem wallispi2lem2

Description: Two expressions are proven to be equal, and this is used to complete the proof of the second version of Wallis' formula for π . (Contributed by Glauco Siliprandi, 30-Jun-2017)

Ref Expression
Assertion wallispi2lem2 N seq 1 × k 2 k 4 2 k 2 k 1 2 N = 2 4 N N ! 4 2 N ! 2

Proof

Step Hyp Ref Expression
1 fveq2 x = 1 seq 1 × k 2 k 4 2 k 2 k 1 2 x = seq 1 × k 2 k 4 2 k 2 k 1 2 1
2 oveq2 x = 1 4 x = 4 1
3 2 oveq2d x = 1 2 4 x = 2 4 1
4 fveq2 x = 1 x ! = 1 !
5 4 oveq1d x = 1 x ! 4 = 1 ! 4
6 3 5 oveq12d x = 1 2 4 x x ! 4 = 2 4 1 1 ! 4
7 oveq2 x = 1 2 x = 2 1
8 7 fveq2d x = 1 2 x ! = 2 1 !
9 8 oveq1d x = 1 2 x ! 2 = 2 1 ! 2
10 6 9 oveq12d x = 1 2 4 x x ! 4 2 x ! 2 = 2 4 1 1 ! 4 2 1 ! 2
11 1 10 eqeq12d x = 1 seq 1 × k 2 k 4 2 k 2 k 1 2 x = 2 4 x x ! 4 2 x ! 2 seq 1 × k 2 k 4 2 k 2 k 1 2 1 = 2 4 1 1 ! 4 2 1 ! 2
12 fveq2 x = y seq 1 × k 2 k 4 2 k 2 k 1 2 x = seq 1 × k 2 k 4 2 k 2 k 1 2 y
13 oveq2 x = y 4 x = 4 y
14 13 oveq2d x = y 2 4 x = 2 4 y
15 fveq2 x = y x ! = y !
16 15 oveq1d x = y x ! 4 = y ! 4
17 14 16 oveq12d x = y 2 4 x x ! 4 = 2 4 y y ! 4
18 oveq2 x = y 2 x = 2 y
19 18 fveq2d x = y 2 x ! = 2 y !
20 19 oveq1d x = y 2 x ! 2 = 2 y ! 2
21 17 20 oveq12d x = y 2 4 x x ! 4 2 x ! 2 = 2 4 y y ! 4 2 y ! 2
22 12 21 eqeq12d x = y seq 1 × k 2 k 4 2 k 2 k 1 2 x = 2 4 x x ! 4 2 x ! 2 seq 1 × k 2 k 4 2 k 2 k 1 2 y = 2 4 y y ! 4 2 y ! 2
23 fveq2 x = y + 1 seq 1 × k 2 k 4 2 k 2 k 1 2 x = seq 1 × k 2 k 4 2 k 2 k 1 2 y + 1
24 oveq2 x = y + 1 4 x = 4 y + 1
25 24 oveq2d x = y + 1 2 4 x = 2 4 y + 1
26 fveq2 x = y + 1 x ! = y + 1 !
27 26 oveq1d x = y + 1 x ! 4 = y + 1 ! 4
28 25 27 oveq12d x = y + 1 2 4 x x ! 4 = 2 4 y + 1 y + 1 ! 4
29 oveq2 x = y + 1 2 x = 2 y + 1
30 29 fveq2d x = y + 1 2 x ! = 2 y + 1 !
31 30 oveq1d x = y + 1 2 x ! 2 = 2 y + 1 ! 2
32 28 31 oveq12d x = y + 1 2 4 x x ! 4 2 x ! 2 = 2 4 y + 1 y + 1 ! 4 2 y + 1 ! 2
33 23 32 eqeq12d x = y + 1 seq 1 × k 2 k 4 2 k 2 k 1 2 x = 2 4 x x ! 4 2 x ! 2 seq 1 × k 2 k 4 2 k 2 k 1 2 y + 1 = 2 4 y + 1 y + 1 ! 4 2 y + 1 ! 2
34 fveq2 x = N seq 1 × k 2 k 4 2 k 2 k 1 2 x = seq 1 × k 2 k 4 2 k 2 k 1 2 N
35 oveq2 x = N 4 x = 4 N
36 35 oveq2d x = N 2 4 x = 2 4 N
37 fveq2 x = N x ! = N !
38 37 oveq1d x = N x ! 4 = N ! 4
39 36 38 oveq12d x = N 2 4 x x ! 4 = 2 4 N N ! 4
40 oveq2 x = N 2 x = 2 N
41 40 fveq2d x = N 2 x ! = 2 N !
42 41 oveq1d x = N 2 x ! 2 = 2 N ! 2
43 39 42 oveq12d x = N 2 4 x x ! 4 2 x ! 2 = 2 4 N N ! 4 2 N ! 2
44 34 43 eqeq12d x = N seq 1 × k 2 k 4 2 k 2 k 1 2 x = 2 4 x x ! 4 2 x ! 2 seq 1 × k 2 k 4 2 k 2 k 1 2 N = 2 4 N N ! 4 2 N ! 2
45 1z 1
46 seq1 1 seq 1 × k 2 k 4 2 k 2 k 1 2 1 = k 2 k 4 2 k 2 k 1 2 1
47 45 46 ax-mp seq 1 × k 2 k 4 2 k 2 k 1 2 1 = k 2 k 4 2 k 2 k 1 2 1
48 1nn 1
49 oveq2 k = 1 2 k = 2 1
50 49 oveq1d k = 1 2 k 4 = 2 1 4
51 49 oveq1d k = 1 2 k 1 = 2 1 1
52 49 51 oveq12d k = 1 2 k 2 k 1 = 2 1 2 1 1
53 52 oveq1d k = 1 2 k 2 k 1 2 = 2 1 2 1 1 2
54 50 53 oveq12d k = 1 2 k 4 2 k 2 k 1 2 = 2 1 4 2 1 2 1 1 2
55 eqid k 2 k 4 2 k 2 k 1 2 = k 2 k 4 2 k 2 k 1 2
56 ovex 2 1 4 2 1 2 1 1 2 V
57 54 55 56 fvmpt 1 k 2 k 4 2 k 2 k 1 2 1 = 2 1 4 2 1 2 1 1 2
58 48 57 ax-mp k 2 k 4 2 k 2 k 1 2 1 = 2 1 4 2 1 2 1 1 2
59 2t1e2 2 1 = 2
60 59 oveq1i 2 1 4 = 2 4
61 2exp4 2 4 = 16
62 1nn0 1 0
63 6nn0 6 0
64 0nn0 0 0
65 1t1e1 1 1 = 1
66 65 oveq1i 1 1 + 0 = 1 + 0
67 1p0e1 1 + 0 = 1
68 66 67 eqtri 1 1 + 0 = 1
69 6cn 6
70 69 mulid1i 6 1 = 6
71 63 dec0h 6 = 06
72 70 71 eqtri 6 1 = 06
73 62 62 63 61 63 64 68 72 decmul1c 2 4 1 = 16
74 61 73 eqtr4i 2 4 = 2 4 1
75 2nn0 2 0
76 2t2e4 2 2 = 4
77 sq1 1 2 = 1
78 62 75 76 77 65 numexp2x 1 4 = 1
79 78 eqcomi 1 = 1 4
80 79 oveq2i 2 4 1 = 2 4 1 4
81 4cn 4
82 81 mulid1i 4 1 = 4
83 82 eqcomi 4 = 4 1
84 83 oveq2i 2 4 = 2 4 1
85 fac1 1 ! = 1
86 85 eqcomi 1 = 1 !
87 86 oveq1i 1 4 = 1 ! 4
88 84 87 oveq12i 2 4 1 4 = 2 4 1 1 ! 4
89 74 80 88 3eqtri 2 4 = 2 4 1 1 ! 4
90 60 89 eqtri 2 1 4 = 2 4 1 1 ! 4
91 59 oveq1i 2 1 1 = 2 1
92 2m1e1 2 1 = 1
93 91 92 eqtri 2 1 1 = 1
94 93 oveq2i 2 1 2 1 1 = 2 1 1
95 59 oveq1i 2 1 1 = 2 1
96 95 59 eqtri 2 1 1 = 2
97 59 fveq2i 2 1 ! = 2 !
98 fac2 2 ! = 2
99 97 98 eqtri 2 1 ! = 2
100 99 eqcomi 2 = 2 1 !
101 94 96 100 3eqtri 2 1 2 1 1 = 2 1 !
102 101 oveq1i 2 1 2 1 1 2 = 2 1 ! 2
103 90 102 oveq12i 2 1 4 2 1 2 1 1 2 = 2 4 1 1 ! 4 2 1 ! 2
104 47 58 103 3eqtri seq 1 × k 2 k 4 2 k 2 k 1 2 1 = 2 4 1 1 ! 4 2 1 ! 2
105 elnnuz y y 1
106 105 biimpi y y 1
107 106 adantr y seq 1 × k 2 k 4 2 k 2 k 1 2 y = 2 4 y y ! 4 2 y ! 2 y 1
108 seqp1 y 1 seq 1 × k 2 k 4 2 k 2 k 1 2 y + 1 = seq 1 × k 2 k 4 2 k 2 k 1 2 y k 2 k 4 2 k 2 k 1 2 y + 1
109 107 108 syl y seq 1 × k 2 k 4 2 k 2 k 1 2 y = 2 4 y y ! 4 2 y ! 2 seq 1 × k 2 k 4 2 k 2 k 1 2 y + 1 = seq 1 × k 2 k 4 2 k 2 k 1 2 y k 2 k 4 2 k 2 k 1 2 y + 1
110 simpr y seq 1 × k 2 k 4 2 k 2 k 1 2 y = 2 4 y y ! 4 2 y ! 2 seq 1 × k 2 k 4 2 k 2 k 1 2 y = 2 4 y y ! 4 2 y ! 2
111 110 oveq1d y seq 1 × k 2 k 4 2 k 2 k 1 2 y = 2 4 y y ! 4 2 y ! 2 seq 1 × k 2 k 4 2 k 2 k 1 2 y k 2 k 4 2 k 2 k 1 2 y + 1 = 2 4 y y ! 4 2 y ! 2 k 2 k 4 2 k 2 k 1 2 y + 1
112 eqidd y k 2 k 4 2 k 2 k 1 2 = k 2 k 4 2 k 2 k 1 2
113 oveq2 k = y + 1 2 k = 2 y + 1
114 113 oveq1d k = y + 1 2 k 4 = 2 y + 1 4
115 113 oveq1d k = y + 1 2 k 1 = 2 y + 1 1
116 113 115 oveq12d k = y + 1 2 k 2 k 1 = 2 y + 1 2 y + 1 1
117 116 oveq1d k = y + 1 2 k 2 k 1 2 = 2 y + 1 2 y + 1 1 2
118 114 117 oveq12d k = y + 1 2 k 4 2 k 2 k 1 2 = 2 y + 1 4 2 y + 1 2 y + 1 1 2
119 118 adantl y k = y + 1 2 k 4 2 k 2 k 1 2 = 2 y + 1 4 2 y + 1 2 y + 1 1 2
120 peano2nn y y + 1
121 2cnd y 2
122 nncn y y
123 1cnd y 1
124 122 123 addcld y y + 1
125 121 124 mulcld y 2 y + 1
126 4nn0 4 0
127 126 a1i y 4 0
128 125 127 expcld y 2 y + 1 4
129 125 123 subcld y 2 y + 1 1
130 125 129 mulcld y 2 y + 1 2 y + 1 1
131 130 sqcld y 2 y + 1 2 y + 1 1 2
132 2pos 0 < 2
133 132 a1i y 0 < 2
134 133 gt0ne0d y 2 0
135 120 nnne0d y y + 1 0
136 121 124 134 135 mulne0d y 2 y + 1 0
137 1red y 1
138 2re 2
139 138 a1i y 2
140 nnre y y
141 140 137 readdcld y y + 1
142 1lt2 1 < 2
143 142 a1i y 1 < 2
144 nnrp y y +
145 137 144 ltaddrp2d y 1 < y + 1
146 139 141 143 145 mulgt1d y 1 < 2 y + 1
147 137 146 gtned y 2 y + 1 1
148 125 123 147 subne0d y 2 y + 1 1 0
149 125 129 136 148 mulne0d y 2 y + 1 2 y + 1 1 0
150 2z 2
151 150 a1i y 2
152 130 149 151 expne0d y 2 y + 1 2 y + 1 1 2 0
153 128 131 152 divcld y 2 y + 1 4 2 y + 1 2 y + 1 1 2
154 112 119 120 153 fvmptd y k 2 k 4 2 k 2 k 1 2 y + 1 = 2 y + 1 4 2 y + 1 2 y + 1 1 2
155 154 oveq2d y 2 4 y y ! 4 2 y ! 2 k 2 k 4 2 k 2 k 1 2 y + 1 = 2 4 y y ! 4 2 y ! 2 2 y + 1 4 2 y + 1 2 y + 1 1 2
156 nnnn0 y y 0
157 127 156 nn0mulcld y 4 y 0
158 121 157 expcld y 2 4 y
159 faccl y 0 y !
160 nncn y ! y !
161 156 159 160 3syl y y !
162 161 127 expcld y y ! 4
163 158 162 mulcld y 2 4 y y ! 4
164 75 a1i y 2 0
165 164 156 nn0mulcld y 2 y 0
166 faccl 2 y 0 2 y !
167 nncn 2 y ! 2 y !
168 165 166 167 3syl y 2 y !
169 168 sqcld y 2 y ! 2
170 165 166 syl y 2 y !
171 170 nnne0d y 2 y ! 0
172 168 171 151 expne0d y 2 y ! 2 0
173 163 169 128 131 172 152 divmuldivd y 2 4 y y ! 4 2 y ! 2 2 y + 1 4 2 y + 1 2 y + 1 1 2 = 2 4 y y ! 4 2 y + 1 4 2 y ! 2 2 y + 1 2 y + 1 1 2
174 121 124 127 mulexpd y 2 y + 1 4 = 2 4 y + 1 4
175 174 oveq2d y 2 4 y y ! 4 2 y + 1 4 = 2 4 y y ! 4 2 4 y + 1 4
176 121 127 expcld y 2 4
177 124 127 expcld y y + 1 4
178 158 162 176 177 mul4d y 2 4 y y ! 4 2 4 y + 1 4 = 2 4 y 2 4 y ! 4 y + 1 4
179 161 124 127 mulexpd y y ! y + 1 4 = y ! 4 y + 1 4
180 179 eqcomd y y ! 4 y + 1 4 = y ! y + 1 4
181 180 oveq2d y 2 4 y 2 4 y ! 4 y + 1 4 = 2 4 y 2 4 y ! y + 1 4
182 175 178 181 3eqtrd y 2 4 y y ! 4 2 y + 1 4 = 2 4 y 2 4 y ! y + 1 4
183 121 122 mulcld y 2 y
184 183 123 addcld y 2 y + 1
185 125 184 mulcomd y 2 y + 1 2 y + 1 = 2 y + 1 2 y + 1
186 185 oveq2d y 2 y ! 2 y + 1 2 y + 1 = 2 y ! 2 y + 1 2 y + 1
187 121 122 123 adddid y 2 y + 1 = 2 y + 2 1
188 187 oveq1d y 2 y + 1 1 = 2 y + 2 1 - 1
189 59 121 eqeltrid y 2 1
190 183 189 123 addsubassd y 2 y + 2 1 - 1 = 2 y + 2 1 - 1
191 59 a1i y 2 1 = 2
192 191 oveq1d y 2 1 1 = 2 1
193 192 92 eqtrdi y 2 1 1 = 1
194 193 oveq2d y 2 y + 2 1 - 1 = 2 y + 1
195 188 190 194 3eqtrd y 2 y + 1 1 = 2 y + 1
196 195 oveq2d y 2 y + 1 2 y + 1 1 = 2 y + 1 2 y + 1
197 196 oveq2d y 2 y ! 2 y + 1 2 y + 1 1 = 2 y ! 2 y + 1 2 y + 1
198 168 184 125 mulassd y 2 y ! 2 y + 1 2 y + 1 = 2 y ! 2 y + 1 2 y + 1
199 186 197 198 3eqtr4d y 2 y ! 2 y + 1 2 y + 1 1 = 2 y ! 2 y + 1 2 y + 1
200 199 oveq1d y 2 y ! 2 y + 1 2 y + 1 1 2 = 2 y ! 2 y + 1 2 y + 1 2
201 168 130 164 mulexpd y 2 y ! 2 y + 1 2 y + 1 1 2 = 2 y ! 2 2 y + 1 2 y + 1 1 2
202 df-2 2 = 1 + 1
203 202 a1i y 2 = 1 + 1
204 203 oveq2d y 2 y + 2 = 2 y + 1 + 1
205 183 123 123 addassd y 2 y + 1 + 1 = 2 y + 1 + 1
206 204 205 eqtr4d y 2 y + 2 = 2 y + 1 + 1
207 206 fveq2d y 2 y + 2 ! = 2 y + 1 + 1 !
208 62 a1i y 1 0
209 165 208 nn0addcld y 2 y + 1 0
210 facp1 2 y + 1 0 2 y + 1 + 1 ! = 2 y + 1 ! 2 y + 1 + 1
211 209 210 syl y 2 y + 1 + 1 ! = 2 y + 1 ! 2 y + 1 + 1
212 facp1 2 y 0 2 y + 1 ! = 2 y ! 2 y + 1
213 165 212 syl y 2 y + 1 ! = 2 y ! 2 y + 1
214 203 eqcomd y 1 + 1 = 2
215 214 oveq2d y 2 y + 1 + 1 = 2 y + 2
216 214 202 59 3eqtr4g y 2 = 2 1
217 216 oveq2d y 2 y + 2 = 2 y + 2 1
218 217 187 eqtr4d y 2 y + 2 = 2 y + 1
219 205 215 218 3eqtrd y 2 y + 1 + 1 = 2 y + 1
220 213 219 oveq12d y 2 y + 1 ! 2 y + 1 + 1 = 2 y ! 2 y + 1 2 y + 1
221 207 211 220 3eqtrrd y 2 y ! 2 y + 1 2 y + 1 = 2 y + 2 !
222 221 oveq1d y 2 y ! 2 y + 1 2 y + 1 2 = 2 y + 2 ! 2
223 200 201 222 3eqtr3d y 2 y ! 2 2 y + 1 2 y + 1 1 2 = 2 y + 2 ! 2
224 182 223 oveq12d y 2 4 y y ! 4 2 y + 1 4 2 y ! 2 2 y + 1 2 y + 1 1 2 = 2 4 y 2 4 y ! y + 1 4 2 y + 2 ! 2
225 173 224 eqtrd y 2 4 y y ! 4 2 y ! 2 2 y + 1 4 2 y + 1 2 y + 1 1 2 = 2 4 y 2 4 y ! y + 1 4 2 y + 2 ! 2
226 83 a1i y 4 = 4 1
227 226 oveq2d y 4 y + 4 = 4 y + 4 1
228 227 oveq2d y 2 4 y + 4 = 2 4 y + 4 1
229 121 127 157 expaddd y 2 4 y + 4 = 2 4 y 2 4
230 81 a1i y 4
231 230 122 123 adddid y 4 y + 1 = 4 y + 4 1
232 231 eqcomd y 4 y + 4 1 = 4 y + 1
233 232 oveq2d y 2 4 y + 4 1 = 2 4 y + 1
234 228 229 233 3eqtr3d y 2 4 y 2 4 = 2 4 y + 1
235 facp1 y 0 y + 1 ! = y ! y + 1
236 156 235 syl y y + 1 ! = y ! y + 1
237 236 eqcomd y y ! y + 1 = y + 1 !
238 237 oveq1d y y ! y + 1 4 = y + 1 ! 4
239 234 238 oveq12d y 2 4 y 2 4 y ! y + 1 4 = 2 4 y + 1 y + 1 ! 4
240 218 fveq2d y 2 y + 2 ! = 2 y + 1 !
241 240 oveq1d y 2 y + 2 ! 2 = 2 y + 1 ! 2
242 239 241 oveq12d y 2 4 y 2 4 y ! y + 1 4 2 y + 2 ! 2 = 2 4 y + 1 y + 1 ! 4 2 y + 1 ! 2
243 155 225 242 3eqtrd y 2 4 y y ! 4 2 y ! 2 k 2 k 4 2 k 2 k 1 2 y + 1 = 2 4 y + 1 y + 1 ! 4 2 y + 1 ! 2
244 243 adantr y seq 1 × k 2 k 4 2 k 2 k 1 2 y = 2 4 y y ! 4 2 y ! 2 2 4 y y ! 4 2 y ! 2 k 2 k 4 2 k 2 k 1 2 y + 1 = 2 4 y + 1 y + 1 ! 4 2 y + 1 ! 2
245 109 111 244 3eqtrd y seq 1 × k 2 k 4 2 k 2 k 1 2 y = 2 4 y y ! 4 2 y ! 2 seq 1 × k 2 k 4 2 k 2 k 1 2 y + 1 = 2 4 y + 1 y + 1 ! 4 2 y + 1 ! 2
246 245 ex y seq 1 × k 2 k 4 2 k 2 k 1 2 y = 2 4 y y ! 4 2 y ! 2 seq 1 × k 2 k 4 2 k 2 k 1 2 y + 1 = 2 4 y + 1 y + 1 ! 4 2 y + 1 ! 2
247 11 22 33 44 104 246 nnind N seq 1 × k 2 k 4 2 k 2 k 1 2 N = 2 4 N N ! 4 2 N ! 2