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

Proof

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