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 ⊢ 𝐼 = ( 𝑛 ∈ ℕ0 ↦ ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) d 𝑥 )
wallispilem1.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion wallispilem1 ( 𝜑 → ( 𝐼 ‘ ( 𝑁 + 1 ) ) ≤ ( 𝐼 ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 wallispilem1.1 ⊢ 𝐼 = ( 𝑛 ∈ ℕ0 ↦ ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) d 𝑥 )
2 wallispilem1.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
3 0re ⊢ 0 ∈ ℝ
4 3 a1i ⊢ ( 𝜑 → 0 ∈ ℝ )
5 pire ⊢ π ∈ ℝ
6 5 a1i ⊢ ( 𝜑 → π ∈ ℝ )
7 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
8 2 7 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
9 iblioosinexp ⊢ ( ( 0 ∈ ℝ ∧ π ∈ ℝ ∧ ( 𝑁 + 1 ) ∈ ℕ0 ) → ( 𝑥 ∈ ( 0 (,) π ) ↦ ( ( sin ‘ 𝑥 ) ↑ ( 𝑁 + 1 ) ) ) ∈ 𝐿1 )
10 4 6 8 9 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) π ) ↦ ( ( sin ‘ 𝑥 ) ↑ ( 𝑁 + 1 ) ) ) ∈ 𝐿1 )
11 iblioosinexp ⊢ ( ( 0 ∈ ℝ ∧ π ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ ( 0 (,) π ) ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ) ∈ 𝐿1 )
12 4 6 2 11 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) π ) ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ) ∈ 𝐿1 )
13 elioore ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 𝑥 ∈ ℝ )
14 13 resincld ⊢ ( 𝑥 ∈ ( 0 (,) π ) → ( sin ‘ 𝑥 ) ∈ ℝ )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( sin ‘ 𝑥 ) ∈ ℝ )
16 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( 𝑁 + 1 ) ∈ ℕ0 )
17 15 16 reexpcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( ( sin ‘ 𝑥 ) ↑ ( 𝑁 + 1 ) ) ∈ ℝ )
18 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → 𝑁 ∈ ℕ0 )
19 15 18 reexpcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ∈ ℝ )
20 2 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
21 uzid ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
22 20 21 syl ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
23 peano2uz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
24 22 23 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
26 14 3 jctil ⊢ ( 𝑥 ∈ ( 0 (,) π ) → ( 0 ∈ ℝ ∧ ( sin ‘ 𝑥 ) ∈ ℝ ) )
27 sinq12gt0 ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 0 < ( sin ‘ 𝑥 ) )
28 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( sin ‘ 𝑥 ) ∈ ℝ ) → ( 0 < ( sin ‘ 𝑥 ) → 0 ≤ ( sin ‘ 𝑥 ) ) )
29 26 27 28 sylc ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 0 ≤ ( sin ‘ 𝑥 ) )
30 29 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → 0 ≤ ( sin ‘ 𝑥 ) )
31 sinbnd ⊢ ( 𝑥 ∈ ℝ → ( - 1 ≤ ( sin ‘ 𝑥 ) ∧ ( sin ‘ 𝑥 ) ≤ 1 ) )
32 13 31 syl ⊢ ( 𝑥 ∈ ( 0 (,) π ) → ( - 1 ≤ ( sin ‘ 𝑥 ) ∧ ( sin ‘ 𝑥 ) ≤ 1 ) )
33 32 simprd ⊢ ( 𝑥 ∈ ( 0 (,) π ) → ( sin ‘ 𝑥 ) ≤ 1 )
34 33 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( sin ‘ 𝑥 ) ≤ 1 )
35 15 18 25 30 34 leexp2rd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( ( sin ‘ 𝑥 ) ↑ ( 𝑁 + 1 ) ) ≤ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) )
36 10 12 17 19 35 itgle ⊢ ( 𝜑 → ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ ( 𝑁 + 1 ) ) d 𝑥 ≤ ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) d 𝑥 )
37 oveq2 ⊢ ( 𝑛 = ( 𝑁 + 1 ) → ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) = ( ( sin ‘ 𝑥 ) ↑ ( 𝑁 + 1 ) ) )
38 37 adantr ⊢ ( ( 𝑛 = ( 𝑁 + 1 ) ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) = ( ( sin ‘ 𝑥 ) ↑ ( 𝑁 + 1 ) ) )
39 38 itgeq2dv ⊢ ( 𝑛 = ( 𝑁 + 1 ) → ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) d 𝑥 = ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ ( 𝑁 + 1 ) ) d 𝑥 )
40 itgex ⊢ ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ ( 𝑁 + 1 ) ) d 𝑥 ∈ V
41 39 1 40 fvmpt ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( 𝐼 ‘ ( 𝑁 + 1 ) ) = ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ ( 𝑁 + 1 ) ) d 𝑥 )
42 8 41 syl ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑁 + 1 ) ) = ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ ( 𝑁 + 1 ) ) d 𝑥 )
43 oveq2 ⊢ ( 𝑛 = 𝑁 → ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) = ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) )
44 43 adantr ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) = ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) )
45 44 itgeq2dv ⊢ ( 𝑛 = 𝑁 → ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) d 𝑥 = ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) d 𝑥 )
46 itgex ⊢ ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) d 𝑥 ∈ V
47 45 1 46 fvmpt ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐼 ‘ 𝑁 ) = ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) d 𝑥 )
48 2 47 syl ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑁 ) = ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) d 𝑥 )
49 36 42 48 3brtr4d ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑁 + 1 ) ) ≤ ( 𝐼 ‘ 𝑁 ) )