Theorem 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	⊢ 𝐼 = ( 𝑛 ∈ ℕ0 ↦ ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) d 𝑥 )
Assertion	wallispilem2	⊢ ( ( 𝐼 ‘ 0 ) = π ∧ ( 𝐼 ‘ 1 ) = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐼 ‘ 𝑁 ) = ( ( ( 𝑁 − 1 ) / 𝑁 ) · ( 𝐼 ‘ ( 𝑁 − 2 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		wallispilem2.1	⊢ 𝐼 = ( 𝑛 ∈ ℕ0 ↦ ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) d 𝑥 )
2		0nn0	⊢ 0 ∈ ℕ0
3		oveq2	⊢ ( 𝑛 = 0 → ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) = ( ( sin ‘ 𝑥 ) ↑ 0 ) )
4	3	adantr	⊢ ( ( 𝑛 = 0 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) = ( ( sin ‘ 𝑥 ) ↑ 0 ) )
5		ioosscn	⊢ ( 0 (,) π ) ⊆ ℂ
6	5	sseli	⊢ ( 𝑥 ∈ ( 0 (,) π ) → 𝑥 ∈ ℂ )
7	6	sincld	⊢ ( 𝑥 ∈ ( 0 (,) π ) → ( sin ‘ 𝑥 ) ∈ ℂ )
8	7	adantl	⊢ ( ( 𝑛 = 0 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( sin ‘ 𝑥 ) ∈ ℂ )
9	8	exp0d	⊢ ( ( 𝑛 = 0 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( ( sin ‘ 𝑥 ) ↑ 0 ) = 1 )
10	4 9	eqtrd	⊢ ( ( 𝑛 = 0 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) = 1 )
11	10	itgeq2dv	⊢ ( 𝑛 = 0 → ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) d 𝑥 = ∫ ( 0 (,) π ) 1 d 𝑥 )
12		ioombl	⊢ ( 0 (,) π ) ∈ dom vol
13		0re	⊢ 0 ∈ ℝ
14		pire	⊢ π ∈ ℝ
15		ioovolcl	⊢ ( ( 0 ∈ ℝ ∧ π ∈ ℝ ) → ( vol ‘ ( 0 (,) π ) ) ∈ ℝ )
16	13 14 15	mp2an	⊢ ( vol ‘ ( 0 (,) π ) ) ∈ ℝ
17		ax-1cn	⊢ 1 ∈ ℂ
18		itgconst	⊢ ( ( ( 0 (,) π ) ∈ dom vol ∧ ( vol ‘ ( 0 (,) π ) ) ∈ ℝ ∧ 1 ∈ ℂ ) → ∫ ( 0 (,) π ) 1 d 𝑥 = ( 1 · ( vol ‘ ( 0 (,) π ) ) ) )
19	12 16 17 18	mp3an	⊢ ∫ ( 0 (,) π ) 1 d 𝑥 = ( 1 · ( vol ‘ ( 0 (,) π ) ) )
20	16	recni	⊢ ( vol ‘ ( 0 (,) π ) ) ∈ ℂ
21	20	mulid2i	⊢ ( 1 · ( vol ‘ ( 0 (,) π ) ) ) = ( vol ‘ ( 0 (,) π ) )
22		pipos	⊢ 0 < π
23	13 14 22	ltleii	⊢ 0 ≤ π
24		volioo	⊢ ( ( 0 ∈ ℝ ∧ π ∈ ℝ ∧ 0 ≤ π ) → ( vol ‘ ( 0 (,) π ) ) = ( π − 0 ) )
25	13 14 23 24	mp3an	⊢ ( vol ‘ ( 0 (,) π ) ) = ( π − 0 )
26	14	recni	⊢ π ∈ ℂ
27	26	subid1i	⊢ ( π − 0 ) = π
28	25 27	eqtri	⊢ ( vol ‘ ( 0 (,) π ) ) = π
29	21 28	eqtri	⊢ ( 1 · ( vol ‘ ( 0 (,) π ) ) ) = π
30	19 29	eqtri	⊢ ∫ ( 0 (,) π ) 1 d 𝑥 = π
31	11 30	eqtrdi	⊢ ( 𝑛 = 0 → ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) d 𝑥 = π )
32	14	elexi	⊢ π ∈ V
33	31 1 32	fvmpt	⊢ ( 0 ∈ ℕ0 → ( 𝐼 ‘ 0 ) = π )
34	2 33	ax-mp	⊢ ( 𝐼 ‘ 0 ) = π
35		1nn0	⊢ 1 ∈ ℕ0
36		simpl	⊢ ( ( 𝑛 = 1 ∧ 𝑥 ∈ ( 0 (,) π ) ) → 𝑛 = 1 )
37	36	oveq2d	⊢ ( ( 𝑛 = 1 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) = ( ( sin ‘ 𝑥 ) ↑ 1 ) )
38	7	adantl	⊢ ( ( 𝑛 = 1 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( sin ‘ 𝑥 ) ∈ ℂ )
39	38	exp1d	⊢ ( ( 𝑛 = 1 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( ( sin ‘ 𝑥 ) ↑ 1 ) = ( sin ‘ 𝑥 ) )
40	37 39	eqtrd	⊢ ( ( 𝑛 = 1 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) = ( sin ‘ 𝑥 ) )
41	40	itgeq2dv	⊢ ( 𝑛 = 1 → ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) d 𝑥 = ∫ ( 0 (,) π ) ( sin ‘ 𝑥 ) d 𝑥 )
42		itgex	⊢ ∫ ( 0 (,) π ) ( sin ‘ 𝑥 ) d 𝑥 ∈ V
43	41 1 42	fvmpt	⊢ ( 1 ∈ ℕ0 → ( 𝐼 ‘ 1 ) = ∫ ( 0 (,) π ) ( sin ‘ 𝑥 ) d 𝑥 )
44	35 43	ax-mp	⊢ ( 𝐼 ‘ 1 ) = ∫ ( 0 (,) π ) ( sin ‘ 𝑥 ) d 𝑥
45		itgsin0pi	⊢ ∫ ( 0 (,) π ) ( sin ‘ 𝑥 ) d 𝑥 = 2
46	44 45	eqtri	⊢ ( 𝐼 ‘ 1 ) = 2
47		id	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
48	1 47	itgsinexp	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐼 ‘ 𝑁 ) = ( ( ( 𝑁 − 1 ) / 𝑁 ) · ( 𝐼 ‘ ( 𝑁 − 2 ) ) ) )
49	34 46 48	3pm3.2i	⊢ ( ( 𝐼 ‘ 0 ) = π ∧ ( 𝐼 ‘ 1 ) = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐼 ‘ 𝑁 ) = ( ( ( 𝑁 − 1 ) / 𝑁 ) · ( 𝐼 ‘ ( 𝑁 − 2 ) ) ) ) )