itgsinexp

Description: A recursive formula for the integral of sin^N on the interval (0,π) . (Contributed by Glauco Siliprandi, 29-Jun-2017)

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

Proof

Step	Hyp	Ref	Expression
1		itgsinexp.1	$⊢ I = (n \in ℕ_{0} ⟼ \int_{(0, π)} {\sin x}^{n} d x)$
2		itgsinexp.2	$⊢ φ \to N \in ℤ_{\geq 2}$
3		eluzelz	$⊢ N \in ℤ_{\geq 2} \to N \in ℤ$
4		zcn	$⊢ N \in ℤ \to N \in ℂ$
5	2 3 4	3syl	$⊢ φ \to N \in ℂ$
6		1cnd	$⊢ φ \to 1 \in ℂ$
7	5 6	npcand	$⊢ φ \to N - 1 + 1 = N$
8	7	eqcomd	$⊢ φ \to N = N - 1 + 1$
9	8	oveq1d	$⊢ φ \to N I (N) = (N - 1 + 1) I (N)$
10		uz2m1nn	$⊢ N \in ℤ_{\geq 2} \to N - 1 \in ℕ$
11	2 10	syl	$⊢ φ \to N - 1 \in ℕ$
12	11	nncnd	$⊢ φ \to N - 1 \in ℂ$
13	1	a1i	$⊢ φ \to I = (n \in ℕ_{0} ⟼ \int_{(0, π)} {\sin x}^{n} d x)$
14		oveq2	$⊢ n = N \to {\sin x}^{n} = {\sin x}^{N}$
15	14	ad2antlr	$⊢ ((φ \land n = N) \land x \in (0, π)) \to {\sin x}^{n} = {\sin x}^{N}$
16	15	itgeq2dv	$⊢ (φ \land n = N) \to \int_{(0, π)} {\sin x}^{n} d x = \int_{(0, π)} {\sin x}^{N} d x$
17		2cnd	$⊢ φ \to 2 \in ℂ$
18		npcan	$⊢ (N \in ℂ \land 2 \in ℂ) \to N - 2 + 2 = N$
19	18	eqcomd	$⊢ (N \in ℂ \land 2 \in ℂ) \to N = N - 2 + 2$
20	5 17 19	syl2anc	$⊢ φ \to N = N - 2 + 2$
21		uznn0sub	$⊢ N \in ℤ_{\geq 2} \to N - 2 \in ℕ_{0}$
22	2 21	syl	$⊢ φ \to N - 2 \in ℕ_{0}$
23		2nn0	$⊢ 2 \in ℕ_{0}$
24	23	a1i	$⊢ φ \to 2 \in ℕ_{0}$
25	22 24	nn0addcld	$⊢ φ \to N - 2 + 2 \in ℕ_{0}$
26	20 25	eqeltrd	$⊢ φ \to N \in ℕ_{0}$
27		itgex	$⊢ \int_{(0, π)} {\sin x}^{N} d x \in V$
28	27	a1i	$⊢ φ \to \int_{(0, π)} {\sin x}^{N} d x \in V$
29	13 16 26 28	fvmptd	$⊢ φ \to I (N) = \int_{(0, π)} {\sin x}^{N} d x$
30		ioosscn	$⊢ (0, π) \subseteq ℂ$
31	30	sseli	$⊢ x \in (0, π) \to x \in ℂ$
32	31	sincld	$⊢ x \in (0, π) \to \sin x \in ℂ$
33	32	adantl	$⊢ (φ \land x \in (0, π)) \to \sin x \in ℂ$
34	26	adantr	$⊢ (φ \land x \in (0, π)) \to N \in ℕ_{0}$
35	33 34	expcld	$⊢ (φ \land x \in (0, π)) \to {\sin x}^{N} \in ℂ$
36		ioossicc	$⊢ (0, π) \subseteq [0, π]$
37	36	a1i	$⊢ φ \to (0, π) \subseteq [0, π]$
38		ioombl	$⊢ (0, π) \in dom vol$
39	38	a1i	$⊢ φ \to (0, π) \in dom vol$
40		0re	$⊢ 0 \in ℝ$
41		pire	$⊢ π \in ℝ$
42		iccssre	$⊢ (0 \in ℝ \land π \in ℝ) \to [0, π] \subseteq ℝ$
43	40 41 42	mp2an	$⊢ [0, π] \subseteq ℝ$
44		ax-resscn	$⊢ ℝ \subseteq ℂ$
45	43 44	sstri	$⊢ [0, π] \subseteq ℂ$
46	45	sseli	$⊢ x \in [0, π] \to x \in ℂ$
47	46	sincld	$⊢ x \in [0, π] \to \sin x \in ℂ$
48	47	adantl	$⊢ (φ \land x \in [0, π]) \to \sin x \in ℂ$
49	26	adantr	$⊢ (φ \land x \in [0, π]) \to N \in ℕ_{0}$
50	48 49	expcld	$⊢ (φ \land x \in [0, π]) \to {\sin x}^{N} \in ℂ$
51	40	a1i	$⊢ φ \to 0 \in ℝ$
52	41	a1i	$⊢ φ \to π \in ℝ$
53	46	adantl	$⊢ (φ \land x \in [0, π]) \to x \in ℂ$
54		eqid	$⊢ (x \in ℂ ⟼ {\sin x}^{N}) = (x \in ℂ ⟼ {\sin x}^{N})$
55	54	fvmpt2	$⊢ (x \in ℂ \land {\sin x}^{N} \in ℂ) \to (x \in ℂ ⟼ {\sin x}^{N}) (x) = {\sin x}^{N}$
56	53 50 55	syl2anc	$⊢ (φ \land x \in [0, π]) \to (x \in ℂ ⟼ {\sin x}^{N}) (x) = {\sin x}^{N}$
57	56	eqcomd	$⊢ (φ \land x \in [0, π]) \to {\sin x}^{N} = (x \in ℂ ⟼ {\sin x}^{N}) (x)$
58	57	mpteq2dva	$⊢ φ \to (x \in [0, π] ⟼ {\sin x}^{N}) = (x \in [0, π] ⟼ (x \in ℂ ⟼ {\sin x}^{N}) (x))$
59		nfmpt1	$⊢ \underline{Ⅎ} x (x \in ℂ ⟼ {\sin x}^{N})$
60		nfcv	$⊢ \underline{Ⅎ} x \sin$
61		sincn	$⊢ \sin : ℂ \underset{cn}{⟶} ℂ$
62	61	a1i	$⊢ φ \to \sin : ℂ \underset{cn}{⟶} ℂ$
63	60 62 26	expcnfg	$⊢ φ \to (x \in ℂ ⟼ {\sin x}^{N}) : ℂ \underset{cn}{⟶} ℂ$
64	45	a1i	$⊢ φ \to [0, π] \subseteq ℂ$
65	59 63 64	cncfmptss	$⊢ φ \to (x \in [0, π] ⟼ (x \in ℂ ⟼ {\sin x}^{N}) (x)) : [0, π] \underset{cn}{⟶} ℂ$
66	58 65	eqeltrd	$⊢ φ \to (x \in [0, π] ⟼ {\sin x}^{N}) : [0, π] \underset{cn}{⟶} ℂ$
67		cniccibl	$⊢ (0 \in ℝ \land π \in ℝ \land (x \in [0, π] ⟼ {\sin x}^{N}) : [0, π] \underset{cn}{⟶} ℂ) \to (x \in [0, π] ⟼ {\sin x}^{N}) \in 𝐿^{1}$
68	51 52 66 67	syl3anc	$⊢ φ \to (x \in [0, π] ⟼ {\sin x}^{N}) \in 𝐿^{1}$
69	37 39 50 68	iblss	$⊢ φ \to (x \in (0, π) ⟼ {\sin x}^{N}) \in 𝐿^{1}$
70	35 69	itgcl	$⊢ φ \to \int_{(0, π)} {\sin x}^{N} d x \in ℂ$
71	29 70	eqeltrd	$⊢ φ \to I (N) \in ℂ$
72	12 71	adddirp1d	$⊢ φ \to (N - 1 + 1) I (N) = (N - 1) I (N) + I (N)$
73		eluz2b2	$⊢ N \in ℤ_{\geq 2} \leftrightarrow (N \in ℕ \land 1 < N)$
74	2 73	sylib	$⊢ φ \to (N \in ℕ \land 1 < N)$
75	74	simpld	$⊢ φ \to N \in ℕ$
76		expm1t	$⊢ (\sin x \in ℂ \land N \in ℕ) \to {\sin x}^{N} = {\sin x}^{N - 1} \sin x$
77	32 75 76	syl2anr	$⊢ (φ \land x \in (0, π)) \to {\sin x}^{N} = {\sin x}^{N - 1} \sin x$
78	77	itgeq2dv	$⊢ φ \to \int_{(0, π)} {\sin x}^{N} d x = \int_{(0, π)} {\sin x}^{N - 1} \sin x d x$
79		eqid	$⊢ (x \in ℂ ⟼ {\sin x}^{N - 1}) = (x \in ℂ ⟼ {\sin x}^{N - 1})$
80		eqid	$⊢ (x \in ℂ ⟼ - \cos x) = (x \in ℂ ⟼ - \cos x)$
81		eqid	$⊢ (x \in ℂ ⟼ (N - 1) {\sin x}^{N - 1 - 1} \cos x) = (x \in ℂ ⟼ (N - 1) {\sin x}^{N - 1 - 1} \cos x)$
82		eqid	$⊢ (x \in ℂ ⟼ {\sin x}^{N - 1} \sin x) = (x \in ℂ ⟼ {\sin x}^{N - 1} \sin x)$
83		eqid	$⊢ (x \in ℂ ⟼ (N - 1) {\sin x}^{N - 1 - 1} \cos x (- \cos x)) = (x \in ℂ ⟼ (N - 1) {\sin x}^{N - 1 - 1} \cos x (- \cos x))$
84		eqid	$⊢ (x \in ℂ ⟼ {\cos x}^{2} {\sin x}^{N - 1 - 1}) = (x \in ℂ ⟼ {\cos x}^{2} {\sin x}^{N - 1 - 1})$
85	79 80 81 82 83 84 11	itgsinexplem1	$⊢ φ \to \int_{(0, π)} {\sin x}^{N - 1} \sin x d x = (N - 1) \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 1 - 1} d x$
86	5 6 6	subsub4d	$⊢ φ \to N - 1 - 1 = N - (1 + 1)$
87		1p1e2	$⊢ 1 + 1 = 2$
88	87	a1i	$⊢ φ \to 1 + 1 = 2$
89	88	oveq2d	$⊢ φ \to N - (1 + 1) = N - 2$
90	86 89	eqtrd	$⊢ φ \to N - 1 - 1 = N - 2$
91	90	adantr	$⊢ (φ \land x \in (0, π)) \to N - 1 - 1 = N - 2$
92	91	oveq2d	$⊢ (φ \land x \in (0, π)) \to {\sin x}^{N - 1 - 1} = {\sin x}^{N - 2}$
93	92	oveq2d	$⊢ (φ \land x \in (0, π)) \to {\cos x}^{2} {\sin x}^{N - 1 - 1} = {\cos x}^{2} {\sin x}^{N - 2}$
94	93	itgeq2dv	$⊢ φ \to \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 1 - 1} d x = \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 2} d x$
95	94	oveq2d	$⊢ φ \to (N - 1) \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 1 - 1} d x = (N - 1) \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 2} d x$
96		sincossq	$⊢ x \in ℂ \to {\sin x}^{2} + {\cos x}^{2} = 1$
97		1cnd	$⊢ x \in ℂ \to 1 \in ℂ$
98		sincl	$⊢ x \in ℂ \to \sin x \in ℂ$
99	98	sqcld	$⊢ x \in ℂ \to {\sin x}^{2} \in ℂ$
100		coscl	$⊢ x \in ℂ \to \cos x \in ℂ$
101	100	sqcld	$⊢ x \in ℂ \to {\cos x}^{2} \in ℂ$
102	97 99 101	subaddd	$⊢ x \in ℂ \to (1 - {\sin x}^{2} = {\cos x}^{2} \leftrightarrow {\sin x}^{2} + {\cos x}^{2} = 1)$
103	96 102	mpbird	$⊢ x \in ℂ \to 1 - {\sin x}^{2} = {\cos x}^{2}$
104	103	eqcomd	$⊢ x \in ℂ \to {\cos x}^{2} = 1 - {\sin x}^{2}$
105	31 104	syl	$⊢ x \in (0, π) \to {\cos x}^{2} = 1 - {\sin x}^{2}$
106	105	oveq1d	$⊢ x \in (0, π) \to {\cos x}^{2} {\sin x}^{N - 2} = (1 - {\sin x}^{2}) {\sin x}^{N - 2}$
107	106	adantl	$⊢ (φ \land x \in (0, π)) \to {\cos x}^{2} {\sin x}^{N - 2} = (1 - {\sin x}^{2}) {\sin x}^{N - 2}$
108	107	itgeq2dv	$⊢ φ \to \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 2} d x = \int_{(0, π)} (1 - {\sin x}^{2}) {\sin x}^{N - 2} d x$
109		1cnd	$⊢ (φ \land x \in (0, π)) \to 1 \in ℂ$
110	32	sqcld	$⊢ x \in (0, π) \to {\sin x}^{2} \in ℂ$
111	110	adantl	$⊢ (φ \land x \in (0, π)) \to {\sin x}^{2} \in ℂ$
112	90	eqcomd	$⊢ φ \to N - 2 = N - 1 - 1$
113		nnm1nn0	$⊢ N - 1 \in ℕ \to N - 1 - 1 \in ℕ_{0}$
114	11 113	syl	$⊢ φ \to N - 1 - 1 \in ℕ_{0}$
115	112 114	eqeltrd	$⊢ φ \to N - 2 \in ℕ_{0}$
116	115	adantr	$⊢ (φ \land x \in (0, π)) \to N - 2 \in ℕ_{0}$
117	33 116	expcld	$⊢ (φ \land x \in (0, π)) \to {\sin x}^{N - 2} \in ℂ$
118	109 111 117	subdird	$⊢ (φ \land x \in (0, π)) \to (1 - {\sin x}^{2}) {\sin x}^{N - 2} = 1 {\sin x}^{N - 2} - {\sin x}^{2} {\sin x}^{N - 2}$
119	117	mulid2d	$⊢ (φ \land x \in (0, π)) \to 1 {\sin x}^{N - 2} = {\sin x}^{N - 2}$
120	23	a1i	$⊢ (φ \land x \in (0, π)) \to 2 \in ℕ_{0}$
121	33 116 120	expaddd	$⊢ (φ \land x \in (0, π)) \to {\sin x}^{2 + N - 2} = {\sin x}^{2} {\sin x}^{N - 2}$
122	17 5	pncan3d	$⊢ φ \to 2 + N - 2 = N$
123	122	oveq2d	$⊢ φ \to {\sin x}^{2 + N - 2} = {\sin x}^{N}$
124	123	adantr	$⊢ (φ \land x \in (0, π)) \to {\sin x}^{2 + N - 2} = {\sin x}^{N}$
125	121 124	eqtr3d	$⊢ (φ \land x \in (0, π)) \to {\sin x}^{2} {\sin x}^{N - 2} = {\sin x}^{N}$
126	119 125	oveq12d	$⊢ (φ \land x \in (0, π)) \to 1 {\sin x}^{N - 2} - {\sin x}^{2} {\sin x}^{N - 2} = {\sin x}^{N - 2} - {\sin x}^{N}$
127	118 126	eqtrd	$⊢ (φ \land x \in (0, π)) \to (1 - {\sin x}^{2}) {\sin x}^{N - 2} = {\sin x}^{N - 2} - {\sin x}^{N}$
128	127	itgeq2dv	$⊢ φ \to \int_{(0, π)} (1 - {\sin x}^{2}) {\sin x}^{N - 2} d x = \int_{(0, π)} ({\sin x}^{N - 2} - {\sin x}^{N}) d x$
129	115	adantr	$⊢ (φ \land x \in [0, π]) \to N - 2 \in ℕ_{0}$
130	48 129	expcld	$⊢ (φ \land x \in [0, π]) \to {\sin x}^{N - 2} \in ℂ$
131		eqid	$⊢ (x \in ℂ ⟼ {\sin x}^{N - 2}) = (x \in ℂ ⟼ {\sin x}^{N - 2})$
132	131	fvmpt2	$⊢ (x \in ℂ \land {\sin x}^{N - 2} \in ℂ) \to (x \in ℂ ⟼ {\sin x}^{N - 2}) (x) = {\sin x}^{N - 2}$
133	53 130 132	syl2anc	$⊢ (φ \land x \in [0, π]) \to (x \in ℂ ⟼ {\sin x}^{N - 2}) (x) = {\sin x}^{N - 2}$
134	133	eqcomd	$⊢ (φ \land x \in [0, π]) \to {\sin x}^{N - 2} = (x \in ℂ ⟼ {\sin x}^{N - 2}) (x)$
135	134	mpteq2dva	$⊢ φ \to (x \in [0, π] ⟼ {\sin x}^{N - 2}) = (x \in [0, π] ⟼ (x \in ℂ ⟼ {\sin x}^{N - 2}) (x))$
136		nfmpt1	$⊢ \underline{Ⅎ} x (x \in ℂ ⟼ {\sin x}^{N - 2})$
137	60 62 115	expcnfg	$⊢ φ \to (x \in ℂ ⟼ {\sin x}^{N - 2}) : ℂ \underset{cn}{⟶} ℂ$
138	136 137 64	cncfmptss	$⊢ φ \to (x \in [0, π] ⟼ (x \in ℂ ⟼ {\sin x}^{N - 2}) (x)) : [0, π] \underset{cn}{⟶} ℂ$
139	135 138	eqeltrd	$⊢ φ \to (x \in [0, π] ⟼ {\sin x}^{N - 2}) : [0, π] \underset{cn}{⟶} ℂ$
140		cniccibl	$⊢ (0 \in ℝ \land π \in ℝ \land (x \in [0, π] ⟼ {\sin x}^{N - 2}) : [0, π] \underset{cn}{⟶} ℂ) \to (x \in [0, π] ⟼ {\sin x}^{N - 2}) \in 𝐿^{1}$
141	51 52 139 140	syl3anc	$⊢ φ \to (x \in [0, π] ⟼ {\sin x}^{N - 2}) \in 𝐿^{1}$
142	37 39 130 141	iblss	$⊢ φ \to (x \in (0, π) ⟼ {\sin x}^{N - 2}) \in 𝐿^{1}$
143	117 142 35 69	itgsub	$⊢ φ \to \int_{(0, π)} ({\sin x}^{N - 2} - {\sin x}^{N}) d x = \int_{(0, π)} {\sin x}^{N - 2} d x - \int_{(0, π)} {\sin x}^{N} d x$
144	108 128 143	3eqtrd	$⊢ φ \to \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 2} d x = \int_{(0, π)} {\sin x}^{N - 2} d x - \int_{(0, π)} {\sin x}^{N} d x$
145	144	oveq2d	$⊢ φ \to (N - 1) \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 2} d x = (N - 1) (\int_{(0, π)} {\sin x}^{N - 2} d x - \int_{(0, π)} {\sin x}^{N} d x)$
146	85 95 145	3eqtrd	$⊢ φ \to \int_{(0, π)} {\sin x}^{N - 1} \sin x d x = (N - 1) (\int_{(0, π)} {\sin x}^{N - 2} d x - \int_{(0, π)} {\sin x}^{N} d x)$
147	29 78 146	3eqtrd	$⊢ φ \to I (N) = (N - 1) (\int_{(0, π)} {\sin x}^{N - 2} d x - \int_{(0, π)} {\sin x}^{N} d x)$
148		oveq2	$⊢ n = N - 2 \to {\sin x}^{n} = {\sin x}^{N - 2}$
149	148	adantr	$⊢ (n = N - 2 \land x \in (0, π)) \to {\sin x}^{n} = {\sin x}^{N - 2}$
150	149	itgeq2dv	$⊢ n = N - 2 \to \int_{(0, π)} {\sin x}^{n} d x = \int_{(0, π)} {\sin x}^{N - 2} d x$
151		itgex	$⊢ \int_{(0, π)} {\sin x}^{N - 2} d x \in V$
152	151	a1i	$⊢ φ \to \int_{(0, π)} {\sin x}^{N - 2} d x \in V$
153	1 150 115 152	fvmptd3	$⊢ φ \to I (N - 2) = \int_{(0, π)} {\sin x}^{N - 2} d x$
154	153 29	oveq12d	$⊢ φ \to I (N - 2) - I (N) = \int_{(0, π)} {\sin x}^{N - 2} d x - \int_{(0, π)} {\sin x}^{N} d x$
155	154	oveq2d	$⊢ φ \to (N - 1) (I (N - 2) - I (N)) = (N - 1) (\int_{(0, π)} {\sin x}^{N - 2} d x - \int_{(0, π)} {\sin x}^{N} d x)$
156	117 142	itgcl	$⊢ φ \to \int_{(0, π)} {\sin x}^{N - 2} d x \in ℂ$
157	153 156	eqeltrd	$⊢ φ \to I (N - 2) \in ℂ$
158	12 157 71	subdid	$⊢ φ \to (N - 1) (I (N - 2) - I (N)) = (N - 1) I (N - 2) - (N - 1) I (N)$
159	147 155 158	3eqtr2d	$⊢ φ \to I (N) = (N - 1) I (N - 2) - (N - 1) I (N)$
160	159	eqcomd	$⊢ φ \to (N - 1) I (N - 2) - (N - 1) I (N) = I (N)$
161	12 157	mulcld	$⊢ φ \to (N - 1) I (N - 2) \in ℂ$
162	12 71	mulcld	$⊢ φ \to (N - 1) I (N) \in ℂ$
163	161 162 71	subaddd	$⊢ φ \to ((N - 1) I (N - 2) - (N - 1) I (N) = I (N) \leftrightarrow (N - 1) I (N) + I (N) = (N - 1) I (N - 2))$
164	160 163	mpbid	$⊢ φ \to (N - 1) I (N) + I (N) = (N - 1) I (N - 2)$
165	9 72 164	3eqtrd	$⊢ φ \to N I (N) = (N - 1) I (N - 2)$
166	165	oveq1d	$⊢ φ \to \frac{N I (N)}{N} = \frac{(N - 1) I (N - 2)}{N}$
167	75	nnne0d	$⊢ φ \to N \neq 0$
168	71 5 167	divcan3d	$⊢ φ \to \frac{N I (N)}{N} = I (N)$
169	12 157 5 167	div23d	$⊢ φ \to \frac{(N - 1) I (N - 2)}{N} = (\frac{N - 1}{N}) I (N - 2)$
170	166 168 169	3eqtr3d	$⊢ φ \to I (N) = (\frac{N - 1}{N}) I (N - 2)$

Metamath Proof Explorer

Theorem itgsinexp

Proof