# Metamath Proof Explorer

## Theorem itgsinexplem1

Description: Integration by parts is applied to integrate sin^(N+1). (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses itgsinexplem1.1 ${⊢}{F}=\left({x}\in ℂ⟼{\mathrm{sin}{x}}^{{N}}\right)$
itgsinexplem1.2 ${⊢}{G}=\left({x}\in ℂ⟼-\mathrm{cos}{x}\right)$
itgsinexplem1.3 ${⊢}{H}=\left({x}\in ℂ⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\right)$
itgsinexplem1.4 ${⊢}{I}=\left({x}\in ℂ⟼{\mathrm{sin}{x}}^{{N}}\mathrm{sin}{x}\right)$
itgsinexplem1.5 ${⊢}{L}=\left({x}\in ℂ⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)\right)$
itgsinexplem1.6 ${⊢}{M}=\left({x}\in ℂ⟼{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}\right)$
itgsinexplem1.7 ${⊢}{\phi }\to {N}\in ℕ$
Assertion itgsinexplem1 ${⊢}{\phi }\to {\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{sin}{x}}^{{N}}\mathrm{sin}{x}d{x}={N}{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}d{x}$

### Proof

Step Hyp Ref Expression
1 itgsinexplem1.1 ${⊢}{F}=\left({x}\in ℂ⟼{\mathrm{sin}{x}}^{{N}}\right)$
2 itgsinexplem1.2 ${⊢}{G}=\left({x}\in ℂ⟼-\mathrm{cos}{x}\right)$
3 itgsinexplem1.3 ${⊢}{H}=\left({x}\in ℂ⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\right)$
4 itgsinexplem1.4 ${⊢}{I}=\left({x}\in ℂ⟼{\mathrm{sin}{x}}^{{N}}\mathrm{sin}{x}\right)$
5 itgsinexplem1.5 ${⊢}{L}=\left({x}\in ℂ⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)\right)$
6 itgsinexplem1.6 ${⊢}{M}=\left({x}\in ℂ⟼{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}\right)$
7 itgsinexplem1.7 ${⊢}{\phi }\to {N}\in ℕ$
8 0m0e0 ${⊢}0-0=0$
9 8 oveq1i ${⊢}0-0-{\int }_{\left(0,\mathrm{\pi }\right)}{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)d{x}=0-{\int }_{\left(0,\mathrm{\pi }\right)}{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)d{x}$
10 0re ${⊢}0\in ℝ$
11 10 a1i ${⊢}{\phi }\to 0\in ℝ$
12 pire ${⊢}\mathrm{\pi }\in ℝ$
13 12 a1i ${⊢}{\phi }\to \mathrm{\pi }\in ℝ$
14 pipos ${⊢}0<\mathrm{\pi }$
15 10 12 14 ltleii ${⊢}0\le \mathrm{\pi }$
16 15 a1i ${⊢}{\phi }\to 0\le \mathrm{\pi }$
17 10 12 pm3.2i ${⊢}\left(0\in ℝ\wedge \mathrm{\pi }\in ℝ\right)$
18 iccssre ${⊢}\left(0\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\to \left[0,\mathrm{\pi }\right]\subseteq ℝ$
19 17 18 ax-mp ${⊢}\left[0,\mathrm{\pi }\right]\subseteq ℝ$
20 ax-resscn ${⊢}ℝ\subseteq ℂ$
21 19 20 sstri ${⊢}\left[0,\mathrm{\pi }\right]\subseteq ℂ$
22 21 sseli ${⊢}{x}\in \left[0,\mathrm{\pi }\right]\to {x}\in ℂ$
23 22 adantl ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to {x}\in ℂ$
24 22 sincld ${⊢}{x}\in \left[0,\mathrm{\pi }\right]\to \mathrm{sin}{x}\in ℂ$
25 24 adantl ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to \mathrm{sin}{x}\in ℂ$
26 7 nnnn0d ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
27 26 adantr ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to {N}\in {ℕ}_{0}$
28 25 27 expcld ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to {\mathrm{sin}{x}}^{{N}}\in ℂ$
29 1 fvmpt2 ${⊢}\left({x}\in ℂ\wedge {\mathrm{sin}{x}}^{{N}}\in ℂ\right)\to {F}\left({x}\right)={\mathrm{sin}{x}}^{{N}}$
30 23 28 29 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to {F}\left({x}\right)={\mathrm{sin}{x}}^{{N}}$
31 30 eqcomd ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to {\mathrm{sin}{x}}^{{N}}={F}\left({x}\right)$
32 31 mpteq2dva ${⊢}{\phi }\to \left({x}\in \left[0,\mathrm{\pi }\right]⟼{\mathrm{sin}{x}}^{{N}}\right)=\left({x}\in \left[0,\mathrm{\pi }\right]⟼{F}\left({x}\right)\right)$
33 nfmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in ℂ⟼{\mathrm{sin}{x}}^{{N}}\right)$
34 1 33 nfcxfr ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
35 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{sin}$
36 sincn ${⊢}\mathrm{sin}:ℂ\underset{cn}{⟶}ℂ$
37 36 a1i ${⊢}{\phi }\to \mathrm{sin}:ℂ\underset{cn}{⟶}ℂ$
38 35 37 26 expcnfg ${⊢}{\phi }\to \left({x}\in ℂ⟼{\mathrm{sin}{x}}^{{N}}\right):ℂ\underset{cn}{⟶}ℂ$
39 1 38 eqeltrid ${⊢}{\phi }\to {F}:ℂ\underset{cn}{⟶}ℂ$
40 21 a1i ${⊢}{\phi }\to \left[0,\mathrm{\pi }\right]\subseteq ℂ$
41 34 39 40 cncfmptss ${⊢}{\phi }\to \left({x}\in \left[0,\mathrm{\pi }\right]⟼{F}\left({x}\right)\right):\left[0,\mathrm{\pi }\right]\underset{cn}{⟶}ℂ$
42 32 41 eqeltrd ${⊢}{\phi }\to \left({x}\in \left[0,\mathrm{\pi }\right]⟼{\mathrm{sin}{x}}^{{N}}\right):\left[0,\mathrm{\pi }\right]\underset{cn}{⟶}ℂ$
43 22 coscld ${⊢}{x}\in \left[0,\mathrm{\pi }\right]\to \mathrm{cos}{x}\in ℂ$
44 43 negcld ${⊢}{x}\in \left[0,\mathrm{\pi }\right]\to -\mathrm{cos}{x}\in ℂ$
45 2 fvmpt2 ${⊢}\left({x}\in ℂ\wedge -\mathrm{cos}{x}\in ℂ\right)\to {G}\left({x}\right)=-\mathrm{cos}{x}$
46 22 44 45 syl2anc ${⊢}{x}\in \left[0,\mathrm{\pi }\right]\to {G}\left({x}\right)=-\mathrm{cos}{x}$
47 46 eqcomd ${⊢}{x}\in \left[0,\mathrm{\pi }\right]\to -\mathrm{cos}{x}={G}\left({x}\right)$
48 47 adantl ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to -\mathrm{cos}{x}={G}\left({x}\right)$
49 48 mpteq2dva ${⊢}{\phi }\to \left({x}\in \left[0,\mathrm{\pi }\right]⟼-\mathrm{cos}{x}\right)=\left({x}\in \left[0,\mathrm{\pi }\right]⟼{G}\left({x}\right)\right)$
50 nfmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in ℂ⟼-\mathrm{cos}{x}\right)$
51 2 50 nfcxfr ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{G}$
52 coscn ${⊢}\mathrm{cos}:ℂ\underset{cn}{⟶}ℂ$
53 52 a1i ${⊢}{\phi }\to \mathrm{cos}:ℂ\underset{cn}{⟶}ℂ$
54 2 negfcncf ${⊢}\mathrm{cos}:ℂ\underset{cn}{⟶}ℂ\to {G}:ℂ\underset{cn}{⟶}ℂ$
55 53 54 syl ${⊢}{\phi }\to {G}:ℂ\underset{cn}{⟶}ℂ$
56 51 55 40 cncfmptss ${⊢}{\phi }\to \left({x}\in \left[0,\mathrm{\pi }\right]⟼{G}\left({x}\right)\right):\left[0,\mathrm{\pi }\right]\underset{cn}{⟶}ℂ$
57 49 56 eqeltrd ${⊢}{\phi }\to \left({x}\in \left[0,\mathrm{\pi }\right]⟼-\mathrm{cos}{x}\right):\left[0,\mathrm{\pi }\right]\underset{cn}{⟶}ℂ$
58 ssidd ${⊢}{\phi }\to ℂ\subseteq ℂ$
59 7 nncnd ${⊢}{\phi }\to {N}\in ℂ$
60 58 59 58 constcncfg ${⊢}{\phi }\to \left({x}\in ℂ⟼{N}\right):ℂ\underset{cn}{⟶}ℂ$
61 nnm1nn0 ${⊢}{N}\in ℕ\to {N}-1\in {ℕ}_{0}$
62 7 61 syl ${⊢}{\phi }\to {N}-1\in {ℕ}_{0}$
63 35 37 62 expcnfg ${⊢}{\phi }\to \left({x}\in ℂ⟼{\mathrm{sin}{x}}^{{N}-1}\right):ℂ\underset{cn}{⟶}ℂ$
64 60 63 mulcncf ${⊢}{\phi }\to \left({x}\in ℂ⟼{N}{\mathrm{sin}{x}}^{{N}-1}\right):ℂ\underset{cn}{⟶}ℂ$
65 cosf ${⊢}\mathrm{cos}:ℂ⟶ℂ$
66 65 a1i ${⊢}{\phi }\to \mathrm{cos}:ℂ⟶ℂ$
67 66 feqmptd ${⊢}{\phi }\to \mathrm{cos}=\left({x}\in ℂ⟼\mathrm{cos}{x}\right)$
68 67 52 eqeltrrdi ${⊢}{\phi }\to \left({x}\in ℂ⟼\mathrm{cos}{x}\right):ℂ\underset{cn}{⟶}ℂ$
69 64 68 mulcncf ${⊢}{\phi }\to \left({x}\in ℂ⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\right):ℂ\underset{cn}{⟶}ℂ$
70 3 69 eqeltrid ${⊢}{\phi }\to {H}:ℂ\underset{cn}{⟶}ℂ$
71 ioosscn ${⊢}\left(0,\mathrm{\pi }\right)\subseteq ℂ$
72 71 a1i ${⊢}{\phi }\to \left(0,\mathrm{\pi }\right)\subseteq ℂ$
73 59 adantr ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to {N}\in ℂ$
74 71 sseli ${⊢}{x}\in \left(0,\mathrm{\pi }\right)\to {x}\in ℂ$
75 74 sincld ${⊢}{x}\in \left(0,\mathrm{\pi }\right)\to \mathrm{sin}{x}\in ℂ$
76 75 adantl ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to \mathrm{sin}{x}\in ℂ$
77 62 adantr ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to {N}-1\in {ℕ}_{0}$
78 76 77 expcld ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to {\mathrm{sin}{x}}^{{N}-1}\in ℂ$
79 73 78 mulcld ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to {N}{\mathrm{sin}{x}}^{{N}-1}\in ℂ$
80 74 coscld ${⊢}{x}\in \left(0,\mathrm{\pi }\right)\to \mathrm{cos}{x}\in ℂ$
81 80 adantl ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to \mathrm{cos}{x}\in ℂ$
82 79 81 mulcld ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to {N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\in ℂ$
83 3 70 72 58 82 cncfmptssg ${⊢}{\phi }\to \left({x}\in \left(0,\mathrm{\pi }\right)⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\right):\left(0,\mathrm{\pi }\right)\underset{cn}{⟶}ℂ$
84 35 37 72 cncfmptss ${⊢}{\phi }\to \left({x}\in \left(0,\mathrm{\pi }\right)⟼\mathrm{sin}{x}\right):\left(0,\mathrm{\pi }\right)\underset{cn}{⟶}ℂ$
85 ioossicc ${⊢}\left(0,\mathrm{\pi }\right)\subseteq \left[0,\mathrm{\pi }\right]$
86 85 a1i ${⊢}{\phi }\to \left(0,\mathrm{\pi }\right)\subseteq \left[0,\mathrm{\pi }\right]$
87 ioombl ${⊢}\left(0,\mathrm{\pi }\right)\in \mathrm{dom}vol$
88 87 a1i ${⊢}{\phi }\to \left(0,\mathrm{\pi }\right)\in \mathrm{dom}vol$
89 28 25 mulcld ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to {\mathrm{sin}{x}}^{{N}}\mathrm{sin}{x}\in ℂ$
90 4 fvmpt2 ${⊢}\left({x}\in ℂ\wedge {\mathrm{sin}{x}}^{{N}}\mathrm{sin}{x}\in ℂ\right)\to {I}\left({x}\right)={\mathrm{sin}{x}}^{{N}}\mathrm{sin}{x}$
91 23 89 90 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to {I}\left({x}\right)={\mathrm{sin}{x}}^{{N}}\mathrm{sin}{x}$
92 91 eqcomd ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to {\mathrm{sin}{x}}^{{N}}\mathrm{sin}{x}={I}\left({x}\right)$
93 92 mpteq2dva ${⊢}{\phi }\to \left({x}\in \left[0,\mathrm{\pi }\right]⟼{\mathrm{sin}{x}}^{{N}}\mathrm{sin}{x}\right)=\left({x}\in \left[0,\mathrm{\pi }\right]⟼{I}\left({x}\right)\right)$
94 nfmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in ℂ⟼{\mathrm{sin}{x}}^{{N}}\mathrm{sin}{x}\right)$
95 4 94 nfcxfr ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{I}$
96 sinf ${⊢}\mathrm{sin}:ℂ⟶ℂ$
97 96 a1i ${⊢}{\phi }\to \mathrm{sin}:ℂ⟶ℂ$
98 97 feqmptd ${⊢}{\phi }\to \mathrm{sin}=\left({x}\in ℂ⟼\mathrm{sin}{x}\right)$
99 98 36 eqeltrrdi ${⊢}{\phi }\to \left({x}\in ℂ⟼\mathrm{sin}{x}\right):ℂ\underset{cn}{⟶}ℂ$
100 38 99 mulcncf ${⊢}{\phi }\to \left({x}\in ℂ⟼{\mathrm{sin}{x}}^{{N}}\mathrm{sin}{x}\right):ℂ\underset{cn}{⟶}ℂ$
101 4 100 eqeltrid ${⊢}{\phi }\to {I}:ℂ\underset{cn}{⟶}ℂ$
102 95 101 40 cncfmptss ${⊢}{\phi }\to \left({x}\in \left[0,\mathrm{\pi }\right]⟼{I}\left({x}\right)\right):\left[0,\mathrm{\pi }\right]\underset{cn}{⟶}ℂ$
103 93 102 eqeltrd ${⊢}{\phi }\to \left({x}\in \left[0,\mathrm{\pi }\right]⟼{\mathrm{sin}{x}}^{{N}}\mathrm{sin}{x}\right):\left[0,\mathrm{\pi }\right]\underset{cn}{⟶}ℂ$
104 cniccibl ${⊢}\left(0\in ℝ\wedge \mathrm{\pi }\in ℝ\wedge \left({x}\in \left[0,\mathrm{\pi }\right]⟼{\mathrm{sin}{x}}^{{N}}\mathrm{sin}{x}\right):\left[0,\mathrm{\pi }\right]\underset{cn}{⟶}ℂ\right)\to \left({x}\in \left[0,\mathrm{\pi }\right]⟼{\mathrm{sin}{x}}^{{N}}\mathrm{sin}{x}\right)\in {𝐿}^{1}$
105 11 13 103 104 syl3anc ${⊢}{\phi }\to \left({x}\in \left[0,\mathrm{\pi }\right]⟼{\mathrm{sin}{x}}^{{N}}\mathrm{sin}{x}\right)\in {𝐿}^{1}$
106 86 88 89 105 iblss ${⊢}{\phi }\to \left({x}\in \left(0,\mathrm{\pi }\right)⟼{\mathrm{sin}{x}}^{{N}}\mathrm{sin}{x}\right)\in {𝐿}^{1}$
107 59 adantr ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to {N}\in ℂ$
108 62 adantr ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to {N}-1\in {ℕ}_{0}$
109 25 108 expcld ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to {\mathrm{sin}{x}}^{{N}-1}\in ℂ$
110 107 109 mulcld ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to {N}{\mathrm{sin}{x}}^{{N}-1}\in ℂ$
111 43 adantl ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to \mathrm{cos}{x}\in ℂ$
112 110 111 mulcld ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to {N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\in ℂ$
113 44 adantl ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to -\mathrm{cos}{x}\in ℂ$
114 112 113 mulcld ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to {N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)\in ℂ$
115 eqid ${⊢}\left({x}\in ℂ⟼-\mathrm{cos}{x}\right)=\left({x}\in ℂ⟼-\mathrm{cos}{x}\right)$
116 115 negfcncf ${⊢}\mathrm{cos}:ℂ\underset{cn}{⟶}ℂ\to \left({x}\in ℂ⟼-\mathrm{cos}{x}\right):ℂ\underset{cn}{⟶}ℂ$
117 53 116 syl ${⊢}{\phi }\to \left({x}\in ℂ⟼-\mathrm{cos}{x}\right):ℂ\underset{cn}{⟶}ℂ$
118 69 117 mulcncf ${⊢}{\phi }\to \left({x}\in ℂ⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)\right):ℂ\underset{cn}{⟶}ℂ$
119 5 118 eqeltrid ${⊢}{\phi }\to {L}:ℂ\underset{cn}{⟶}ℂ$
120 5 119 40 58 114 cncfmptssg ${⊢}{\phi }\to \left({x}\in \left[0,\mathrm{\pi }\right]⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)\right):\left[0,\mathrm{\pi }\right]\underset{cn}{⟶}ℂ$
121 cniccibl ${⊢}\left(0\in ℝ\wedge \mathrm{\pi }\in ℝ\wedge \left({x}\in \left[0,\mathrm{\pi }\right]⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)\right):\left[0,\mathrm{\pi }\right]\underset{cn}{⟶}ℂ\right)\to \left({x}\in \left[0,\mathrm{\pi }\right]⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)\right)\in {𝐿}^{1}$
122 11 13 120 121 syl3anc ${⊢}{\phi }\to \left({x}\in \left[0,\mathrm{\pi }\right]⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)\right)\in {𝐿}^{1}$
123 86 88 114 122 iblss ${⊢}{\phi }\to \left({x}\in \left(0,\mathrm{\pi }\right)⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)\right)\in {𝐿}^{1}$
124 reelprrecn ${⊢}ℝ\in \left\{ℝ,ℂ\right\}$
125 124 a1i ${⊢}{\phi }\to ℝ\in \left\{ℝ,ℂ\right\}$
126 recn ${⊢}{x}\in ℝ\to {x}\in ℂ$
127 126 sincld ${⊢}{x}\in ℝ\to \mathrm{sin}{x}\in ℂ$
128 127 adantl ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \mathrm{sin}{x}\in ℂ$
129 26 adantr ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {N}\in {ℕ}_{0}$
130 128 129 expcld ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {\mathrm{sin}{x}}^{{N}}\in ℂ$
131 59 adantr ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {N}\in ℂ$
132 62 adantr ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {N}-1\in {ℕ}_{0}$
133 128 132 expcld ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {\mathrm{sin}{x}}^{{N}-1}\in ℂ$
134 131 133 mulcld ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {N}{\mathrm{sin}{x}}^{{N}-1}\in ℂ$
135 126 coscld ${⊢}{x}\in ℝ\to \mathrm{cos}{x}\in ℂ$
136 135 adantl ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \mathrm{cos}{x}\in ℂ$
137 134 136 mulcld ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\in ℂ$
138 sincl ${⊢}{x}\in ℂ\to \mathrm{sin}{x}\in ℂ$
139 138 adantl ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to \mathrm{sin}{x}\in ℂ$
140 26 adantr ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to {N}\in {ℕ}_{0}$
141 139 140 expcld ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to {\mathrm{sin}{x}}^{{N}}\in ℂ$
142 141 1 fmptd ${⊢}{\phi }\to {F}:ℂ⟶ℂ$
143 126 adantl ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {x}\in ℂ$
144 elex ${⊢}{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\in ℂ\to {N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\in \mathrm{V}$
145 137 144 syl ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\in \mathrm{V}$
146 rabid ${⊢}{x}\in \left\{{x}\in ℂ|{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\in \mathrm{V}\right\}↔\left({x}\in ℂ\wedge {N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\in \mathrm{V}\right)$
147 143 145 146 sylanbrc ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {x}\in \left\{{x}\in ℂ|{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\in \mathrm{V}\right\}$
148 3 dmmpt ${⊢}\mathrm{dom}{H}=\left\{{x}\in ℂ|{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\in \mathrm{V}\right\}$
149 147 148 eleqtrrdi ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {x}\in \mathrm{dom}{H}$
150 149 ex ${⊢}{\phi }\to \left({x}\in ℝ\to {x}\in \mathrm{dom}{H}\right)$
151 150 alrimiv ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in ℝ\to {x}\in \mathrm{dom}{H}\right)$
152 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}ℝ$
153 nfmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in ℂ⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\right)$
154 3 153 nfcxfr ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{H}$
155 154 nfdm ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{H}$
156 152 155 dfss2f ${⊢}ℝ\subseteq \mathrm{dom}{H}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in ℝ\to {x}\in \mathrm{dom}{H}\right)$
157 151 156 sylibr ${⊢}{\phi }\to ℝ\subseteq \mathrm{dom}{H}$
158 7 dvsinexp ${⊢}{\phi }\to \frac{d\left({x}\in ℂ⟼{\mathrm{sin}{x}}^{{N}}\right)}{{d}_{ℂ}{x}}=\left({x}\in ℂ⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\right)$
159 1 oveq2i ${⊢}ℂ\mathrm{D}{F}=\frac{d\left({x}\in ℂ⟼{\mathrm{sin}{x}}^{{N}}\right)}{{d}_{ℂ}{x}}$
160 158 159 3 3eqtr4g ${⊢}{\phi }\to ℂ\mathrm{D}{F}={H}$
161 160 dmeqd ${⊢}{\phi }\to \mathrm{dom}{{F}}_{ℂ}^{\prime }=\mathrm{dom}{H}$
162 157 161 sseqtrrd ${⊢}{\phi }\to ℝ\subseteq \mathrm{dom}{{F}}_{ℂ}^{\prime }$
163 dvres3 ${⊢}\left(\left(ℝ\in \left\{ℝ,ℂ\right\}\wedge {F}:ℂ⟶ℂ\right)\wedge \left(ℂ\subseteq ℂ\wedge ℝ\subseteq \mathrm{dom}{{F}}_{ℂ}^{\prime }\right)\right)\to ℝ\mathrm{D}\left({{F}↾}_{ℝ}\right)={{{F}}_{ℂ}^{\prime }↾}_{ℝ}$
164 125 142 58 162 163 syl22anc ${⊢}{\phi }\to ℝ\mathrm{D}\left({{F}↾}_{ℝ}\right)={{{F}}_{ℂ}^{\prime }↾}_{ℝ}$
165 1 reseq1i ${⊢}{{F}↾}_{ℝ}={\left({x}\in ℂ⟼{\mathrm{sin}{x}}^{{N}}\right)↾}_{ℝ}$
166 resmpt ${⊢}ℝ\subseteq ℂ\to {\left({x}\in ℂ⟼{\mathrm{sin}{x}}^{{N}}\right)↾}_{ℝ}=\left({x}\in ℝ⟼{\mathrm{sin}{x}}^{{N}}\right)$
167 20 166 ax-mp ${⊢}{\left({x}\in ℂ⟼{\mathrm{sin}{x}}^{{N}}\right)↾}_{ℝ}=\left({x}\in ℝ⟼{\mathrm{sin}{x}}^{{N}}\right)$
168 165 167 eqtri ${⊢}{{F}↾}_{ℝ}=\left({x}\in ℝ⟼{\mathrm{sin}{x}}^{{N}}\right)$
169 168 oveq2i ${⊢}ℝ\mathrm{D}\left({{F}↾}_{ℝ}\right)=\frac{d\left({x}\in ℝ⟼{\mathrm{sin}{x}}^{{N}}\right)}{{d}_{ℝ}{x}}$
170 169 a1i ${⊢}{\phi }\to ℝ\mathrm{D}\left({{F}↾}_{ℝ}\right)=\frac{d\left({x}\in ℝ⟼{\mathrm{sin}{x}}^{{N}}\right)}{{d}_{ℝ}{x}}$
171 160 reseq1d ${⊢}{\phi }\to {{{F}}_{ℂ}^{\prime }↾}_{ℝ}={{H}↾}_{ℝ}$
172 3 reseq1i ${⊢}{{H}↾}_{ℝ}={\left({x}\in ℂ⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\right)↾}_{ℝ}$
173 resmpt ${⊢}ℝ\subseteq ℂ\to {\left({x}\in ℂ⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\right)↾}_{ℝ}=\left({x}\in ℝ⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\right)$
174 20 173 ax-mp ${⊢}{\left({x}\in ℂ⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\right)↾}_{ℝ}=\left({x}\in ℝ⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\right)$
175 172 174 eqtri ${⊢}{{H}↾}_{ℝ}=\left({x}\in ℝ⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\right)$
176 171 175 syl6eq ${⊢}{\phi }\to {{{F}}_{ℂ}^{\prime }↾}_{ℝ}=\left({x}\in ℝ⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\right)$
177 164 170 176 3eqtr3d ${⊢}{\phi }\to \frac{d\left({x}\in ℝ⟼{\mathrm{sin}{x}}^{{N}}\right)}{{d}_{ℝ}{x}}=\left({x}\in ℝ⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\right)$
178 19 a1i ${⊢}{\phi }\to \left[0,\mathrm{\pi }\right]\subseteq ℝ$
179 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
180 179 tgioo2 ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ$
181 17 a1i ${⊢}{\phi }\to \left(0\in ℝ\wedge \mathrm{\pi }\in ℝ\right)$
182 iccntr ${⊢}\left(0\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[0,\mathrm{\pi }\right]\right)=\left(0,\mathrm{\pi }\right)$
183 181 182 syl ${⊢}{\phi }\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[0,\mathrm{\pi }\right]\right)=\left(0,\mathrm{\pi }\right)$
184 125 130 137 177 178 180 179 183 dvmptres2 ${⊢}{\phi }\to \frac{d\left({x}\in \left[0,\mathrm{\pi }\right]⟼{\mathrm{sin}{x}}^{{N}}\right)}{{d}_{ℝ}{x}}=\left({x}\in \left(0,\mathrm{\pi }\right)⟼{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\right)$
185 135 negcld ${⊢}{x}\in ℝ\to -\mathrm{cos}{x}\in ℂ$
186 185 adantl ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to -\mathrm{cos}{x}\in ℂ$
187 127 negcld ${⊢}{x}\in ℝ\to -\mathrm{sin}{x}\in ℂ$
188 187 adantl ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to -\mathrm{sin}{x}\in ℂ$
189 dvcosre ${⊢}\frac{d\left({x}\in ℝ⟼\mathrm{cos}{x}\right)}{{d}_{ℝ}{x}}=\left({x}\in ℝ⟼-\mathrm{sin}{x}\right)$
190 189 a1i ${⊢}{\phi }\to \frac{d\left({x}\in ℝ⟼\mathrm{cos}{x}\right)}{{d}_{ℝ}{x}}=\left({x}\in ℝ⟼-\mathrm{sin}{x}\right)$
191 125 136 188 190 dvmptneg ${⊢}{\phi }\to \frac{d\left({x}\in ℝ⟼-\mathrm{cos}{x}\right)}{{d}_{ℝ}{x}}=\left({x}\in ℝ⟼-\left(-\mathrm{sin}{x}\right)\right)$
192 127 negnegd ${⊢}{x}\in ℝ\to -\left(-\mathrm{sin}{x}\right)=\mathrm{sin}{x}$
193 192 adantl ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to -\left(-\mathrm{sin}{x}\right)=\mathrm{sin}{x}$
194 193 mpteq2dva ${⊢}{\phi }\to \left({x}\in ℝ⟼-\left(-\mathrm{sin}{x}\right)\right)=\left({x}\in ℝ⟼\mathrm{sin}{x}\right)$
195 191 194 eqtrd ${⊢}{\phi }\to \frac{d\left({x}\in ℝ⟼-\mathrm{cos}{x}\right)}{{d}_{ℝ}{x}}=\left({x}\in ℝ⟼\mathrm{sin}{x}\right)$
196 125 186 128 195 178 180 179 183 dvmptres2 ${⊢}{\phi }\to \frac{d\left({x}\in \left[0,\mathrm{\pi }\right]⟼-\mathrm{cos}{x}\right)}{{d}_{ℝ}{x}}=\left({x}\in \left(0,\mathrm{\pi }\right)⟼\mathrm{sin}{x}\right)$
197 fveq2 ${⊢}{x}=0\to \mathrm{sin}{x}=\mathrm{sin}0$
198 sin0 ${⊢}\mathrm{sin}0=0$
199 197 198 syl6eq ${⊢}{x}=0\to \mathrm{sin}{x}=0$
200 199 oveq1d ${⊢}{x}=0\to {\mathrm{sin}{x}}^{{N}}={0}^{{N}}$
201 200 adantl ${⊢}\left({\phi }\wedge {x}=0\right)\to {\mathrm{sin}{x}}^{{N}}={0}^{{N}}$
202 7 adantr ${⊢}\left({\phi }\wedge {x}=0\right)\to {N}\in ℕ$
203 202 0expd ${⊢}\left({\phi }\wedge {x}=0\right)\to {0}^{{N}}=0$
204 201 203 eqtrd ${⊢}\left({\phi }\wedge {x}=0\right)\to {\mathrm{sin}{x}}^{{N}}=0$
205 204 oveq1d ${⊢}\left({\phi }\wedge {x}=0\right)\to {\mathrm{sin}{x}}^{{N}}\left(-\mathrm{cos}{x}\right)=0\cdot \left(-\mathrm{cos}{x}\right)$
206 id ${⊢}{x}=0\to {x}=0$
207 0cn ${⊢}0\in ℂ$
208 206 207 eqeltrdi ${⊢}{x}=0\to {x}\in ℂ$
209 coscl ${⊢}{x}\in ℂ\to \mathrm{cos}{x}\in ℂ$
210 209 negcld ${⊢}{x}\in ℂ\to -\mathrm{cos}{x}\in ℂ$
211 208 210 syl ${⊢}{x}=0\to -\mathrm{cos}{x}\in ℂ$
212 211 adantl ${⊢}\left({\phi }\wedge {x}=0\right)\to -\mathrm{cos}{x}\in ℂ$
213 212 mul02d ${⊢}\left({\phi }\wedge {x}=0\right)\to 0\cdot \left(-\mathrm{cos}{x}\right)=0$
214 205 213 eqtrd ${⊢}\left({\phi }\wedge {x}=0\right)\to {\mathrm{sin}{x}}^{{N}}\left(-\mathrm{cos}{x}\right)=0$
215 fveq2 ${⊢}{x}=\mathrm{\pi }\to \mathrm{sin}{x}=\mathrm{sin}\mathrm{\pi }$
216 sinpi ${⊢}\mathrm{sin}\mathrm{\pi }=0$
217 215 216 syl6eq ${⊢}{x}=\mathrm{\pi }\to \mathrm{sin}{x}=0$
218 217 oveq1d ${⊢}{x}=\mathrm{\pi }\to {\mathrm{sin}{x}}^{{N}}={0}^{{N}}$
219 218 adantl ${⊢}\left({\phi }\wedge {x}=\mathrm{\pi }\right)\to {\mathrm{sin}{x}}^{{N}}={0}^{{N}}$
220 7 adantr ${⊢}\left({\phi }\wedge {x}=\mathrm{\pi }\right)\to {N}\in ℕ$
221 220 0expd ${⊢}\left({\phi }\wedge {x}=\mathrm{\pi }\right)\to {0}^{{N}}=0$
222 219 221 eqtrd ${⊢}\left({\phi }\wedge {x}=\mathrm{\pi }\right)\to {\mathrm{sin}{x}}^{{N}}=0$
223 222 oveq1d ${⊢}\left({\phi }\wedge {x}=\mathrm{\pi }\right)\to {\mathrm{sin}{x}}^{{N}}\left(-\mathrm{cos}{x}\right)=0\cdot \left(-\mathrm{cos}{x}\right)$
224 id ${⊢}{x}=\mathrm{\pi }\to {x}=\mathrm{\pi }$
225 picn ${⊢}\mathrm{\pi }\in ℂ$
226 224 225 eqeltrdi ${⊢}{x}=\mathrm{\pi }\to {x}\in ℂ$
227 226 coscld ${⊢}{x}=\mathrm{\pi }\to \mathrm{cos}{x}\in ℂ$
228 227 negcld ${⊢}{x}=\mathrm{\pi }\to -\mathrm{cos}{x}\in ℂ$
229 228 adantl ${⊢}\left({\phi }\wedge {x}=\mathrm{\pi }\right)\to -\mathrm{cos}{x}\in ℂ$
230 229 mul02d ${⊢}\left({\phi }\wedge {x}=\mathrm{\pi }\right)\to 0\cdot \left(-\mathrm{cos}{x}\right)=0$
231 223 230 eqtrd ${⊢}\left({\phi }\wedge {x}=\mathrm{\pi }\right)\to {\mathrm{sin}{x}}^{{N}}\left(-\mathrm{cos}{x}\right)=0$
232 11 13 16 42 57 83 84 106 123 184 196 214 231 itgparts ${⊢}{\phi }\to {\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{sin}{x}}^{{N}}\mathrm{sin}{x}d{x}=0-0-{\int }_{\left(0,\mathrm{\pi }\right)}{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)d{x}$
233 df-neg ${⊢}-{\int }_{\left(0,\mathrm{\pi }\right)}{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)d{x}=0-{\int }_{\left(0,\mathrm{\pi }\right)}{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)d{x}$
234 233 a1i ${⊢}{\phi }\to -{\int }_{\left(0,\mathrm{\pi }\right)}{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)d{x}=0-{\int }_{\left(0,\mathrm{\pi }\right)}{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)d{x}$
235 9 232 234 3eqtr4a ${⊢}{\phi }\to {\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{sin}{x}}^{{N}}\mathrm{sin}{x}d{x}=-{\int }_{\left(0,\mathrm{\pi }\right)}{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)d{x}$
236 79 81 81 mulassd ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to {N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\mathrm{cos}{x}={N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\mathrm{cos}{x}$
237 sqval ${⊢}\mathrm{cos}{x}\in ℂ\to {\mathrm{cos}{x}}^{2}=\mathrm{cos}{x}\mathrm{cos}{x}$
238 237 eqcomd ${⊢}\mathrm{cos}{x}\in ℂ\to \mathrm{cos}{x}\mathrm{cos}{x}={\mathrm{cos}{x}}^{2}$
239 80 238 syl ${⊢}{x}\in \left(0,\mathrm{\pi }\right)\to \mathrm{cos}{x}\mathrm{cos}{x}={\mathrm{cos}{x}}^{2}$
240 239 adantl ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to \mathrm{cos}{x}\mathrm{cos}{x}={\mathrm{cos}{x}}^{2}$
241 240 oveq2d ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to {N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\mathrm{cos}{x}={N}{\mathrm{sin}{x}}^{{N}-1}{\mathrm{cos}{x}}^{2}$
242 80 sqcld ${⊢}{x}\in \left(0,\mathrm{\pi }\right)\to {\mathrm{cos}{x}}^{2}\in ℂ$
243 242 adantl ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to {\mathrm{cos}{x}}^{2}\in ℂ$
244 73 78 243 mulassd ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to {N}{\mathrm{sin}{x}}^{{N}-1}{\mathrm{cos}{x}}^{2}={N}{\mathrm{sin}{x}}^{{N}-1}{\mathrm{cos}{x}}^{2}$
245 241 244 eqtrd ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to {N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\mathrm{cos}{x}={N}{\mathrm{sin}{x}}^{{N}-1}{\mathrm{cos}{x}}^{2}$
246 78 243 mulcomd ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to {\mathrm{sin}{x}}^{{N}-1}{\mathrm{cos}{x}}^{2}={\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}$
247 246 oveq2d ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to {N}{\mathrm{sin}{x}}^{{N}-1}{\mathrm{cos}{x}}^{2}={N}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}$
248 236 245 247 3eqtrd ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to {N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\mathrm{cos}{x}={N}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}$
249 248 negeqd ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to -{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\mathrm{cos}{x}=-{N}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}$
250 82 81 mulneg2d ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to {N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)=-{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\mathrm{cos}{x}$
251 243 78 mulcld ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to {\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}\in ℂ$
252 73 251 mulneg1d ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to -{N}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}=-{N}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}$
253 249 250 252 3eqtr4d ${⊢}\left({\phi }\wedge {x}\in \left(0,\mathrm{\pi }\right)\right)\to {N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)=-{N}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}$
254 253 itgeq2dv ${⊢}{\phi }\to {\int }_{\left(0,\mathrm{\pi }\right)}{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)d{x}={\int }_{\left(0,\mathrm{\pi }\right)}-{N}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}d{x}$
255 59 negcld ${⊢}{\phi }\to -{N}\in ℂ$
256 43 sqcld ${⊢}{x}\in \left[0,\mathrm{\pi }\right]\to {\mathrm{cos}{x}}^{2}\in ℂ$
257 256 adantl ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to {\mathrm{cos}{x}}^{2}\in ℂ$
258 257 109 mulcld ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to {\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}\in ℂ$
259 6 fvmpt2 ${⊢}\left({x}\in ℂ\wedge {\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}\in ℂ\right)\to {M}\left({x}\right)={\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}$
260 23 258 259 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to {M}\left({x}\right)={\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}$
261 260 eqcomd ${⊢}\left({\phi }\wedge {x}\in \left[0,\mathrm{\pi }\right]\right)\to {\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}={M}\left({x}\right)$
262 261 mpteq2dva ${⊢}{\phi }\to \left({x}\in \left[0,\mathrm{\pi }\right]⟼{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}\right)=\left({x}\in \left[0,\mathrm{\pi }\right]⟼{M}\left({x}\right)\right)$
263 nfmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in ℂ⟼{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}\right)$
264 6 263 nfcxfr ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{M}$
265 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{cos}$
266 2nn0 ${⊢}2\in {ℕ}_{0}$
267 266 a1i ${⊢}{\phi }\to 2\in {ℕ}_{0}$
268 265 53 267 expcnfg ${⊢}{\phi }\to \left({x}\in ℂ⟼{\mathrm{cos}{x}}^{2}\right):ℂ\underset{cn}{⟶}ℂ$
269 268 63 mulcncf ${⊢}{\phi }\to \left({x}\in ℂ⟼{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}\right):ℂ\underset{cn}{⟶}ℂ$
270 6 269 eqeltrid ${⊢}{\phi }\to {M}:ℂ\underset{cn}{⟶}ℂ$
271 264 270 40 cncfmptss ${⊢}{\phi }\to \left({x}\in \left[0,\mathrm{\pi }\right]⟼{M}\left({x}\right)\right):\left[0,\mathrm{\pi }\right]\underset{cn}{⟶}ℂ$
272 262 271 eqeltrd ${⊢}{\phi }\to \left({x}\in \left[0,\mathrm{\pi }\right]⟼{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}\right):\left[0,\mathrm{\pi }\right]\underset{cn}{⟶}ℂ$
273 cniccibl ${⊢}\left(0\in ℝ\wedge \mathrm{\pi }\in ℝ\wedge \left({x}\in \left[0,\mathrm{\pi }\right]⟼{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}\right):\left[0,\mathrm{\pi }\right]\underset{cn}{⟶}ℂ\right)\to \left({x}\in \left[0,\mathrm{\pi }\right]⟼{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}\right)\in {𝐿}^{1}$
274 11 13 272 273 syl3anc ${⊢}{\phi }\to \left({x}\in \left[0,\mathrm{\pi }\right]⟼{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}\right)\in {𝐿}^{1}$
275 86 88 258 274 iblss ${⊢}{\phi }\to \left({x}\in \left(0,\mathrm{\pi }\right)⟼{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}\right)\in {𝐿}^{1}$
276 255 251 275 itgmulc2 ${⊢}{\phi }\to -{N}{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}d{x}={\int }_{\left(0,\mathrm{\pi }\right)}-{N}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}d{x}$
277 254 276 eqtr4d ${⊢}{\phi }\to {\int }_{\left(0,\mathrm{\pi }\right)}{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)d{x}=-{N}{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}d{x}$
278 277 negeqd ${⊢}{\phi }\to -{\int }_{\left(0,\mathrm{\pi }\right)}{N}{\mathrm{sin}{x}}^{{N}-1}\mathrm{cos}{x}\left(-\mathrm{cos}{x}\right)d{x}=--{N}{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}d{x}$
279 235 278 eqtrd ${⊢}{\phi }\to {\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{sin}{x}}^{{N}}\mathrm{sin}{x}d{x}=--{N}{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}d{x}$
280 251 275 itgcl ${⊢}{\phi }\to {\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}d{x}\in ℂ$
281 59 280 mulneg1d ${⊢}{\phi }\to -{N}{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}d{x}=-{N}{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}d{x}$
282 281 negeqd ${⊢}{\phi }\to --{N}{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}d{x}=-\left(-{N}{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}d{x}\right)$
283 59 280 mulcld ${⊢}{\phi }\to {N}{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}d{x}\in ℂ$
284 283 negnegd ${⊢}{\phi }\to -\left(-{N}{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}d{x}\right)={N}{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}d{x}$
285 279 282 284 3eqtrd ${⊢}{\phi }\to {\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{sin}{x}}^{{N}}\mathrm{sin}{x}d{x}={N}{\int }_{\left(0,\mathrm{\pi }\right)}{\mathrm{cos}{x}}^{2}{\mathrm{sin}{x}}^{{N}-1}d{x}$