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 ) )