# Metamath Proof Explorer

## Theorem 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}=\left({n}\in {ℕ}_{0}⟼{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{sin}{x}}^{{n}}d{x}\right)$
itgsinexp.2 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge 2}$
Assertion itgsinexp ${⊢}{\phi }\to {I}\left({N}\right)=\left(\frac{{N}-1}{{N}}\right){I}\left({N}-2\right)$

### Proof

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