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∈ℕ0⟼∫0πsin⁡xndx
wallispilem1.2 ⊢φ→N∈ℕ0
Assertion wallispilem1 ⊢φ→I⁡N+1≤I⁡N

Proof

Step Hyp Ref Expression
1 wallispilem1.1 ⊢I=n∈ℕ0⟼∫0πsin⁡xndx
2 wallispilem1.2 ⊢φ→N∈ℕ0
3 0re ⊢0∈ℝ
4 3 a1i ⊢φ→0∈ℝ
5 pire ⊢π∈ℝ
6 5 a1i ⊢φ→π∈ℝ
7 peano2nn0 ⊢N∈ℕ0→N+1∈ℕ0
8 2 7 syl ⊢φ→N+1∈ℕ0
9 iblioosinexp ⊢0∈ℝ∧π∈ℝ∧N+1∈ℕ0→x∈0π⟼sin⁡xN+1∈𝐿1
10 4 6 8 9 syl3anc ⊢φ→x∈0π⟼sin⁡xN+1∈𝐿1
11 iblioosinexp ⊢0∈ℝ∧π∈ℝ∧N∈ℕ0→x∈0π⟼sin⁡xN∈𝐿1
12 4 6 2 11 syl3anc ⊢φ→x∈0π⟼sin⁡xN∈𝐿1
13 elioore ⊢x∈0π→x∈ℝ
14 13 resincld ⊢x∈0π→sin⁡x∈ℝ
15 14 adantl ⊢φ∧x∈0π→sin⁡x∈ℝ
16 8 adantr ⊢φ∧x∈0π→N+1∈ℕ0
17 15 16 reexpcld ⊢φ∧x∈0π→sin⁡xN+1∈ℝ
18 2 adantr ⊢φ∧x∈0π→N∈ℕ0
19 15 18 reexpcld ⊢φ∧x∈0π→sin⁡xN∈ℝ
20 2 nn0zd ⊢φ→N∈ℤ
21 uzid ⊢N∈ℤ→N∈ℤ≥N
22 20 21 syl ⊢φ→N∈ℤ≥N
23 peano2uz ⊢N∈ℤ≥N→N+1∈ℤ≥N
24 22 23 syl ⊢φ→N+1∈ℤ≥N
25 24 adantr ⊢φ∧x∈0π→N+1∈ℤ≥N
26 14 3 jctil ⊢x∈0π→0∈ℝ∧sin⁡x∈ℝ
27 sinq12gt0 ⊢x∈0π→0<sin⁡x
28 ltle ⊢0∈ℝ∧sin⁡x∈ℝ→0<sin⁡x→0≤sin⁡x
29 26 27 28 sylc ⊢x∈0π→0≤sin⁡x
30 29 adantl ⊢φ∧x∈0π→0≤sin⁡x
31 sinbnd ⊢x∈ℝ→−1≤sin⁡x∧sin⁡x≤1
32 13 31 syl ⊢x∈0π→−1≤sin⁡x∧sin⁡x≤1
33 32 simprd ⊢x∈0π→sin⁡x≤1
34 33 adantl ⊢φ∧x∈0π→sin⁡x≤1
35 15 18 25 30 34 leexp2rd ⊢φ∧x∈0π→sin⁡xN+1≤sin⁡xN
36 10 12 17 19 35 itgle ⊢φ→∫0πsin⁡xN+1dx≤∫0πsin⁡xNdx
37 oveq2 ⊢n=N+1→sin⁡xn=sin⁡xN+1
38 37 adantr ⊢n=N+1∧x∈0π→sin⁡xn=sin⁡xN+1
39 38 itgeq2dv ⊢n=N+1→∫0πsin⁡xndx=∫0πsin⁡xN+1dx
40 itgex ⊢∫0πsin⁡xN+1dx∈V
41 39 1 40 fvmpt ⊢N+1∈ℕ0→I⁡N+1=∫0πsin⁡xN+1dx
42 8 41 syl ⊢φ→I⁡N+1=∫0πsin⁡xN+1dx
43 oveq2 ⊢n=N→sin⁡xn=sin⁡xN
44 43 adantr ⊢n=N∧x∈0π→sin⁡xn=sin⁡xN
45 44 itgeq2dv ⊢n=N→∫0πsin⁡xndx=∫0πsin⁡xNdx
46 itgex ⊢∫0πsin⁡xNdx∈V
47 45 1 46 fvmpt ⊢N∈ℕ0→I⁡N=∫0πsin⁡xNdx
48 2 47 syl ⊢φ→I⁡N=∫0πsin⁡xNdx
49 36 42 48 3brtr4d ⊢φ→I⁡N+1≤I⁡N