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 \in ℕ_{0} ⟼ \int_{(0, π)} {\sin x}^{n} d x)$
	wallispilem1.2	$⊢ φ \to N \in ℕ_{0}$
Assertion	wallispilem1	$⊢ φ \to I (N + 1) \leq I (N)$

Proof

Step	Hyp	Ref	Expression
1		wallispilem1.1	$⊢ I = (n \in ℕ_{0} ⟼ \int_{(0, π)} {\sin x}^{n} d x)$
2		wallispilem1.2	$⊢ φ \to N \in ℕ_{0}$
3		0re	$⊢ 0 \in ℝ$
4	3	a1i	$⊢ φ \to 0 \in ℝ$
5		pire	$⊢ π \in ℝ$
6	5	a1i	$⊢ φ \to π \in ℝ$
7		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
8	2 7	syl	$⊢ φ \to N + 1 \in ℕ_{0}$
9		iblioosinexp	$⊢ (0 \in ℝ \land π \in ℝ \land N + 1 \in ℕ_{0}) \to (x \in (0, π) ⟼ {\sin x}^{N + 1}) \in 𝐿^{1}$
10	4 6 8 9	syl3anc	$⊢ φ \to (x \in (0, π) ⟼ {\sin x}^{N + 1}) \in 𝐿^{1}$
11		iblioosinexp	$⊢ (0 \in ℝ \land π \in ℝ \land N \in ℕ_{0}) \to (x \in (0, π) ⟼ {\sin x}^{N}) \in 𝐿^{1}$
12	4 6 2 11	syl3anc	$⊢ φ \to (x \in (0, π) ⟼ {\sin x}^{N}) \in 𝐿^{1}$
13		elioore	$⊢ x \in (0, π) \to x \in ℝ$
14	13	resincld	$⊢ x \in (0, π) \to \sin x \in ℝ$
15	14	adantl	$⊢ (φ \land x \in (0, π)) \to \sin x \in ℝ$
16	8	adantr	$⊢ (φ \land x \in (0, π)) \to N + 1 \in ℕ_{0}$
17	15 16	reexpcld	$⊢ (φ \land x \in (0, π)) \to {\sin x}^{N + 1} \in ℝ$
18	2	adantr	$⊢ (φ \land x \in (0, π)) \to N \in ℕ_{0}$
19	15 18	reexpcld	$⊢ (φ \land x \in (0, π)) \to {\sin x}^{N} \in ℝ$
20	2	nn0zd	$⊢ φ \to N \in ℤ$
21		uzid	$⊢ N \in ℤ \to N \in ℤ_{\geq N}$
22	20 21	syl	$⊢ φ \to N \in ℤ_{\geq N}$
23		peano2uz	$⊢ N \in ℤ_{\geq N} \to N + 1 \in ℤ_{\geq N}$
24	22 23	syl	$⊢ φ \to N + 1 \in ℤ_{\geq N}$
25	24	adantr	$⊢ (φ \land x \in (0, π)) \to N + 1 \in ℤ_{\geq N}$
26	14 3	jctil	$⊢ x \in (0, π) \to (0 \in ℝ \land \sin x \in ℝ)$
27		sinq12gt0	$⊢ x \in (0, π) \to 0 < \sin x$
28		ltle	$⊢ (0 \in ℝ \land \sin x \in ℝ) \to (0 < \sin x \to 0 \leq \sin x)$
29	26 27 28	sylc	$⊢ x \in (0, π) \to 0 \leq \sin x$
30	29	adantl	$⊢ (φ \land x \in (0, π)) \to 0 \leq \sin x$
31		sinbnd	$⊢ x \in ℝ \to (- 1 \leq \sin x \land \sin x \leq 1)$
32	13 31	syl	$⊢ x \in (0, π) \to (- 1 \leq \sin x \land \sin x \leq 1)$
33	32	simprd	$⊢ x \in (0, π) \to \sin x \leq 1$
34	33	adantl	$⊢ (φ \land x \in (0, π)) \to \sin x \leq 1$
35	15 18 25 30 34	leexp2rd	$⊢ (φ \land x \in (0, π)) \to {\sin x}^{N + 1} \leq {\sin x}^{N}$
36	10 12 17 19 35	itgle	$⊢ φ \to \int_{(0, π)} {\sin x}^{N + 1} d x \leq \int_{(0, π)} {\sin x}^{N} d x$
37		oveq2	$⊢ n = N + 1 \to {\sin x}^{n} = {\sin x}^{N + 1}$
38	37	adantr	$⊢ (n = N + 1 \land x \in (0, π)) \to {\sin x}^{n} = {\sin x}^{N + 1}$
39	38	itgeq2dv	$⊢ n = N + 1 \to \int_{(0, π)} {\sin x}^{n} d x = \int_{(0, π)} {\sin x}^{N + 1} d x$
40		itgex	$⊢ \int_{(0, π)} {\sin x}^{N + 1} d x \in V$
41	39 1 40	fvmpt	$⊢ N + 1 \in ℕ_{0} \to I (N + 1) = \int_{(0, π)} {\sin x}^{N + 1} d x$
42	8 41	syl	$⊢ φ \to I (N + 1) = \int_{(0, π)} {\sin x}^{N + 1} d x$
43		oveq2	$⊢ n = N \to {\sin x}^{n} = {\sin x}^{N}$
44	43	adantr	$⊢ (n = N \land x \in (0, π)) \to {\sin x}^{n} = {\sin x}^{N}$
45	44	itgeq2dv	$⊢ n = N \to \int_{(0, π)} {\sin x}^{n} d x = \int_{(0, π)} {\sin x}^{N} d x$
46		itgex	$⊢ \int_{(0, π)} {\sin x}^{N} d x \in V$
47	45 1 46	fvmpt	$⊢ N \in ℕ_{0} \to I (N) = \int_{(0, π)} {\sin x}^{N} d x$
48	2 47	syl	$⊢ φ \to I (N) = \int_{(0, π)} {\sin x}^{N} d x$
49	36 42 48	3brtr4d	$⊢ φ \to I (N + 1) \leq I (N)$

Metamath Proof Explorer

Theorem wallispilem1

Proof