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 ⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) )
itgsinexplem1.2 ⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ - ( cos ‘ 𝑥 ) )
itgsinexplem1.3 ⊢ 𝐻 = ( 𝑥 ∈ ℂ ↦ ( ( 𝑁 · ( ( sin ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · ( cos ‘ 𝑥 ) ) )
itgsinexplem1.4 ⊢ 𝐼 = ( 𝑥 ∈ ℂ ↦ ( ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) · ( sin ‘ 𝑥 ) ) )
itgsinexplem1.5 ⊢ 𝐿 = ( 𝑥 ∈ ℂ ↦ ( ( ( 𝑁 · ( ( sin ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · ( cos ‘ 𝑥 ) ) · - ( cos ‘ 𝑥 ) ) )
itgsinexplem1.6 ⊢ 𝑀 = ( 𝑥 ∈ ℂ ↦ ( ( ( cos ‘ 𝑥 ) ↑ 2 ) · ( ( sin ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
itgsinexplem1.7 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion itgsinexplem1 ( 𝜑 → ∫ ( 0 (,) π ) ( ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) · ( sin ‘ 𝑥 ) ) d 𝑥 = ( 𝑁 · ∫ ( 0 (,) π ) ( ( ( cos ‘ 𝑥 ) ↑ 2 ) · ( ( sin ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) d 𝑥 ) )

Proof

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