Metamath Proof Explorer


Theorem wallispilem2

Description: A first set of properties for the sequence I that will be used in the proof of the Wallis product formula. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypothesis wallispilem2.1 I = n 0 0 π sin x n dx
Assertion wallispilem2 I 0 = π I 1 = 2 N 2 I N = N 1 N I N 2

Proof

Step Hyp Ref Expression
1 wallispilem2.1 I = n 0 0 π sin x n dx
2 0nn0 0 0
3 oveq2 n = 0 sin x n = sin x 0
4 3 adantr n = 0 x 0 π sin x n = sin x 0
5 ioosscn 0 π
6 5 sseli x 0 π x
7 6 sincld x 0 π sin x
8 7 adantl n = 0 x 0 π sin x
9 8 exp0d n = 0 x 0 π sin x 0 = 1
10 4 9 eqtrd n = 0 x 0 π sin x n = 1
11 10 itgeq2dv n = 0 0 π sin x n dx = 0 π 1 dx
12 ioombl 0 π dom vol
13 0re 0
14 pire π
15 ioovolcl 0 π vol 0 π
16 13 14 15 mp2an vol 0 π
17 ax-1cn 1
18 itgconst 0 π dom vol vol 0 π 1 0 π 1 dx = 1 vol 0 π
19 12 16 17 18 mp3an 0 π 1 dx = 1 vol 0 π
20 16 recni vol 0 π
21 20 mulid2i 1 vol 0 π = vol 0 π
22 pipos 0 < π
23 13 14 22 ltleii 0 π
24 volioo 0 π 0 π vol 0 π = π 0
25 13 14 23 24 mp3an vol 0 π = π 0
26 14 recni π
27 26 subid1i π 0 = π
28 25 27 eqtri vol 0 π = π
29 21 28 eqtri 1 vol 0 π = π
30 19 29 eqtri 0 π 1 dx = π
31 11 30 eqtrdi n = 0 0 π sin x n dx = π
32 14 elexi π V
33 31 1 32 fvmpt 0 0 I 0 = π
34 2 33 ax-mp I 0 = π
35 1nn0 1 0
36 simpl n = 1 x 0 π n = 1
37 36 oveq2d n = 1 x 0 π sin x n = sin x 1
38 7 adantl n = 1 x 0 π sin x
39 38 exp1d n = 1 x 0 π sin x 1 = sin x
40 37 39 eqtrd n = 1 x 0 π sin x n = sin x
41 40 itgeq2dv n = 1 0 π sin x n dx = 0 π sin x dx
42 itgex 0 π sin x dx V
43 41 1 42 fvmpt 1 0 I 1 = 0 π sin x dx
44 35 43 ax-mp I 1 = 0 π sin x dx
45 itgsin0pi 0 π sin x dx = 2
46 44 45 eqtri I 1 = 2
47 id N 2 N 2
48 1 47 itgsinexp N 2 I N = N 1 N I N 2
49 34 46 48 3pm3.2i I 0 = π I 1 = 2 N 2 I N = N 1 N I N 2