wallispilem2

Description: A first set of properties for the sequence I that will be used in the proof of the Wallis product formula. (Contributed by Glauco Siliprandi, 29-Jun-2017)

		Ref	Expression
	Hypothesis	wallispilem2.1	$⊢ I = (n \in ℕ_{0} ⟼ \int_{(0, π)} {\sin x}^{n} d x)$
	Assertion	wallispilem2	$⊢ (I (0) = π \land I (1) = 2 \land (N \in ℤ_{\geq 2} \to I (N) = (\frac{N - 1}{N}) I (N - 2)))$

Proof

Step	Hyp	Ref	Expression
1		wallispilem2.1	$⊢ I = (n \in ℕ_{0} ⟼ \int_{(0, π)} {\sin x}^{n} d x)$
2		0nn0	$⊢ 0 \in ℕ_{0}$
3		oveq2	$⊢ n = 0 \to {\sin x}^{n} = {\sin x}^{0}$
4	3	adantr	$⊢ (n = 0 \land x \in (0, π)) \to {\sin x}^{n} = {\sin x}^{0}$
5		ioosscn	$⊢ (0, π) \subseteq ℂ$
6	5	sseli	$⊢ x \in (0, π) \to x \in ℂ$
7	6	sincld	$⊢ x \in (0, π) \to \sin x \in ℂ$
8	7	adantl	$⊢ (n = 0 \land x \in (0, π)) \to \sin x \in ℂ$
9	8	exp0d	$⊢ (n = 0 \land x \in (0, π)) \to {\sin x}^{0} = 1$
10	4 9	eqtrd	$⊢ (n = 0 \land x \in (0, π)) \to {\sin x}^{n} = 1$
11	10	itgeq2dv	$⊢ n = 0 \to \int_{(0, π)} {\sin x}^{n} d x = \int_{(0, π)} 1 d x$
12		ioombl	$⊢ (0, π) \in dom vol$
13		0re	$⊢ 0 \in ℝ$
14		pire	$⊢ π \in ℝ$
15		ioovolcl	$⊢ (0 \in ℝ \land π \in ℝ) \to vol ((0, π)) \in ℝ$
16	13 14 15	mp2an	$⊢ vol ((0, π)) \in ℝ$
17		ax-1cn	$⊢ 1 \in ℂ$
18		itgconst	$⊢ ((0, π) \in dom vol \land vol ((0, π)) \in ℝ \land 1 \in ℂ) \to \int_{(0, π)} 1 d x = 1 vol ((0, π))$
19	12 16 17 18	mp3an	$⊢ \int_{(0, π)} 1 d x = 1 vol ((0, π))$
20	16	recni	$⊢ vol ((0, π)) \in ℂ$
21	20	mullidi	$⊢ 1 vol ((0, π)) = vol ((0, π))$
22		pipos	$⊢ 0 < π$
23	13 14 22	ltleii	$⊢ 0 \leq π$
24		volioo	$⊢ (0 \in ℝ \land π \in ℝ \land 0 \leq π) \to vol ((0, π)) = π - 0$
25	13 14 23 24	mp3an	$⊢ vol ((0, π)) = π - 0$
26	14	recni	$⊢ π \in ℂ$
27	26	subid1i	$⊢ π - 0 = π$
28	25 27	eqtri	$⊢ vol ((0, π)) = π$
29	21 28	eqtri	$⊢ 1 vol ((0, π)) = π$
30	19 29	eqtri	$⊢ \int_{(0, π)} 1 d x = π$
31	11 30	eqtrdi	$⊢ n = 0 \to \int_{(0, π)} {\sin x}^{n} d x = π$
32	14	elexi	$⊢ π \in V$
33	31 1 32	fvmpt	$⊢ 0 \in ℕ_{0} \to I (0) = π$
34	2 33	ax-mp	$⊢ I (0) = π$
35		1nn0	$⊢ 1 \in ℕ_{0}$
36		simpl	$⊢ (n = 1 \land x \in (0, π)) \to n = 1$
37	36	oveq2d	$⊢ (n = 1 \land x \in (0, π)) \to {\sin x}^{n} = {\sin x}^{1}$
38	7	adantl	$⊢ (n = 1 \land x \in (0, π)) \to \sin x \in ℂ$
39	38	exp1d	$⊢ (n = 1 \land x \in (0, π)) \to {\sin x}^{1} = \sin x$
40	37 39	eqtrd	$⊢ (n = 1 \land x \in (0, π)) \to {\sin x}^{n} = \sin x$
41	40	itgeq2dv	$⊢ n = 1 \to \int_{(0, π)} {\sin x}^{n} d x = \int_{(0, π)} \sin x d x$
42		itgex	$⊢ \int_{(0, π)} \sin x d x \in V$
43	41 1 42	fvmpt	$⊢ 1 \in ℕ_{0} \to I (1) = \int_{(0, π)} \sin x d x$
44	35 43	ax-mp	$⊢ I (1) = \int_{(0, π)} \sin x d x$
45		itgsin0pi	$⊢ \int_{(0, π)} \sin x d x = 2$
46	44 45	eqtri	$⊢ I (1) = 2$
47		id	$⊢ N \in ℤ_{\geq 2} \to N \in ℤ_{\geq 2}$
48	1 47	itgsinexp	$⊢ N \in ℤ_{\geq 2} \to I (N) = (\frac{N - 1}{N}) I (N - 2)$
49	34 46 48	3pm3.2i	$⊢ (I (0) = π \land I (1) = 2 \land (N \in ℤ_{\geq 2} \to I (N) = (\frac{N - 1}{N}) I (N - 2)))$

Metamath Proof Explorer

Theorem wallispilem2

Proof