Metamath Proof Explorer


Theorem wallispilem1

Description: I is monotone: increasing the exponent, the integral decreases. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses wallispilem1.1
|- I = ( n e. NN0 |-> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ n ) _d x )
wallispilem1.2
|- ( ph -> N e. NN0 )
Assertion wallispilem1
|- ( ph -> ( I ` ( N + 1 ) ) <_ ( I ` N ) )

Proof

Step Hyp Ref Expression
1 wallispilem1.1
 |-  I = ( n e. NN0 |-> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ n ) _d x )
2 wallispilem1.2
 |-  ( ph -> N e. NN0 )
3 0re
 |-  0 e. RR
4 3 a1i
 |-  ( ph -> 0 e. RR )
5 pire
 |-  _pi e. RR
6 5 a1i
 |-  ( ph -> _pi e. RR )
7 peano2nn0
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
8 2 7 syl
 |-  ( ph -> ( N + 1 ) e. NN0 )
9 iblioosinexp
 |-  ( ( 0 e. RR /\ _pi e. RR /\ ( N + 1 ) e. NN0 ) -> ( x e. ( 0 (,) _pi ) |-> ( ( sin ` x ) ^ ( N + 1 ) ) ) e. L^1 )
10 4 6 8 9 syl3anc
 |-  ( ph -> ( x e. ( 0 (,) _pi ) |-> ( ( sin ` x ) ^ ( N + 1 ) ) ) e. L^1 )
11 iblioosinexp
 |-  ( ( 0 e. RR /\ _pi e. RR /\ N e. NN0 ) -> ( x e. ( 0 (,) _pi ) |-> ( ( sin ` x ) ^ N ) ) e. L^1 )
12 4 6 2 11 syl3anc
 |-  ( ph -> ( x e. ( 0 (,) _pi ) |-> ( ( sin ` x ) ^ N ) ) e. L^1 )
13 elioore
 |-  ( x e. ( 0 (,) _pi ) -> x e. RR )
14 13 resincld
 |-  ( x e. ( 0 (,) _pi ) -> ( sin ` x ) e. RR )
15 14 adantl
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( sin ` x ) e. RR )
16 8 adantr
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( N + 1 ) e. NN0 )
17 15 16 reexpcld
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( sin ` x ) ^ ( N + 1 ) ) e. RR )
18 2 adantr
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> N e. NN0 )
19 15 18 reexpcld
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( sin ` x ) ^ N ) e. RR )
20 2 nn0zd
 |-  ( ph -> N e. ZZ )
21 uzid
 |-  ( N e. ZZ -> N e. ( ZZ>= ` N ) )
22 20 21 syl
 |-  ( ph -> N e. ( ZZ>= ` N ) )
23 peano2uz
 |-  ( N e. ( ZZ>= ` N ) -> ( N + 1 ) e. ( ZZ>= ` N ) )
24 22 23 syl
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` N ) )
25 24 adantr
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( N + 1 ) e. ( ZZ>= ` N ) )
26 14 3 jctil
 |-  ( x e. ( 0 (,) _pi ) -> ( 0 e. RR /\ ( sin ` x ) e. RR ) )
27 sinq12gt0
 |-  ( x e. ( 0 (,) _pi ) -> 0 < ( sin ` x ) )
28 ltle
 |-  ( ( 0 e. RR /\ ( sin ` x ) e. RR ) -> ( 0 < ( sin ` x ) -> 0 <_ ( sin ` x ) ) )
29 26 27 28 sylc
 |-  ( x e. ( 0 (,) _pi ) -> 0 <_ ( sin ` x ) )
30 29 adantl
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> 0 <_ ( sin ` x ) )
31 sinbnd
 |-  ( x e. RR -> ( -u 1 <_ ( sin ` x ) /\ ( sin ` x ) <_ 1 ) )
32 13 31 syl
 |-  ( x e. ( 0 (,) _pi ) -> ( -u 1 <_ ( sin ` x ) /\ ( sin ` x ) <_ 1 ) )
33 32 simprd
 |-  ( x e. ( 0 (,) _pi ) -> ( sin ` x ) <_ 1 )
34 33 adantl
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( sin ` x ) <_ 1 )
35 15 18 25 30 34 leexp2rd
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( sin ` x ) ^ ( N + 1 ) ) <_ ( ( sin ` x ) ^ N ) )
36 10 12 17 19 35 itgle
 |-  ( ph -> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ ( N + 1 ) ) _d x <_ S. ( 0 (,) _pi ) ( ( sin ` x ) ^ N ) _d x )
37 oveq2
 |-  ( n = ( N + 1 ) -> ( ( sin ` x ) ^ n ) = ( ( sin ` x ) ^ ( N + 1 ) ) )
38 37 adantr
 |-  ( ( n = ( N + 1 ) /\ x e. ( 0 (,) _pi ) ) -> ( ( sin ` x ) ^ n ) = ( ( sin ` x ) ^ ( N + 1 ) ) )
39 38 itgeq2dv
 |-  ( n = ( N + 1 ) -> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ n ) _d x = S. ( 0 (,) _pi ) ( ( sin ` x ) ^ ( N + 1 ) ) _d x )
40 itgex
 |-  S. ( 0 (,) _pi ) ( ( sin ` x ) ^ ( N + 1 ) ) _d x e. _V
41 39 1 40 fvmpt
 |-  ( ( N + 1 ) e. NN0 -> ( I ` ( N + 1 ) ) = S. ( 0 (,) _pi ) ( ( sin ` x ) ^ ( N + 1 ) ) _d x )
42 8 41 syl
 |-  ( ph -> ( I ` ( N + 1 ) ) = S. ( 0 (,) _pi ) ( ( sin ` x ) ^ ( N + 1 ) ) _d x )
43 oveq2
 |-  ( n = N -> ( ( sin ` x ) ^ n ) = ( ( sin ` x ) ^ N ) )
44 43 adantr
 |-  ( ( n = N /\ x e. ( 0 (,) _pi ) ) -> ( ( sin ` x ) ^ n ) = ( ( sin ` x ) ^ N ) )
45 44 itgeq2dv
 |-  ( n = N -> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ n ) _d x = S. ( 0 (,) _pi ) ( ( sin ` x ) ^ N ) _d x )
46 itgex
 |-  S. ( 0 (,) _pi ) ( ( sin ` x ) ^ N ) _d x e. _V
47 45 1 46 fvmpt
 |-  ( N e. NN0 -> ( I ` N ) = S. ( 0 (,) _pi ) ( ( sin ` x ) ^ N ) _d x )
48 2 47 syl
 |-  ( ph -> ( I ` N ) = S. ( 0 (,) _pi ) ( ( sin ` x ) ^ N ) _d x )
49 36 42 48 3brtr4d
 |-  ( ph -> ( I ` ( N + 1 ) ) <_ ( I ` N ) )