Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  itgsinexp Structured version   Visualization version   GIF version

Theorem itgsinexp 40691
 Description: A recursive formula for the integral of sin^N on the interval (0,π) . (Contributed by Glauco Siliprandi, 29-Jun-2017.)
Hypotheses
Ref Expression
itgsinexp.1 𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)
itgsinexp.2 (𝜑𝑁 ∈ (ℤ‘2))
Assertion
Ref Expression
itgsinexp (𝜑 → (𝐼𝑁) = (((𝑁 − 1) / 𝑁) · (𝐼‘(𝑁 − 2))))
Distinct variable groups:   𝑥,𝑛,𝑁   𝜑,𝑛,𝑥
Allowed substitution hints:   𝐼(𝑥,𝑛)

Proof of Theorem itgsinexp
StepHypRef Expression
1 itgsinexp.2 . . . . . . . 8 (𝜑𝑁 ∈ (ℤ‘2))
2 eluzelz 11909 . . . . . . . 8 (𝑁 ∈ (ℤ‘2) → 𝑁 ∈ ℤ)
3 zcn 11594 . . . . . . . 8 (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
41, 2, 33syl 18 . . . . . . 7 (𝜑𝑁 ∈ ℂ)
5 1cnd 10268 . . . . . . 7 (𝜑 → 1 ∈ ℂ)
64, 5npcand 10608 . . . . . 6 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
76eqcomd 2766 . . . . 5 (𝜑𝑁 = ((𝑁 − 1) + 1))
87oveq1d 6829 . . . 4 (𝜑 → (𝑁 · (𝐼𝑁)) = (((𝑁 − 1) + 1) · (𝐼𝑁)))
9 uz2m1nn 11976 . . . . . . 7 (𝑁 ∈ (ℤ‘2) → (𝑁 − 1) ∈ ℕ)
101, 9syl 17 . . . . . 6 (𝜑 → (𝑁 − 1) ∈ ℕ)
1110nncnd 11248 . . . . 5 (𝜑 → (𝑁 − 1) ∈ ℂ)
12 itgsinexp.1 . . . . . . . 8 𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)
1312a1i 11 . . . . . . 7 (𝜑𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥))
14 oveq2 6822 . . . . . . . . 9 (𝑛 = 𝑁 → ((sin‘𝑥)↑𝑛) = ((sin‘𝑥)↑𝑁))
1514ad2antlr 765 . . . . . . . 8 (((𝜑𝑛 = 𝑁) ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑𝑛) = ((sin‘𝑥)↑𝑁))
1615itgeq2dv 23767 . . . . . . 7 ((𝜑𝑛 = 𝑁) → ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥 = ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥)
17 2cnd 11305 . . . . . . . . 9 (𝜑 → 2 ∈ ℂ)
18 npcan 10502 . . . . . . . . . 10 ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑁 − 2) + 2) = 𝑁)
1918eqcomd 2766 . . . . . . . . 9 ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ) → 𝑁 = ((𝑁 − 2) + 2))
204, 17, 19syl2anc 696 . . . . . . . 8 (𝜑𝑁 = ((𝑁 − 2) + 2))
21 uznn0sub 11932 . . . . . . . . . 10 (𝑁 ∈ (ℤ‘2) → (𝑁 − 2) ∈ ℕ0)
221, 21syl 17 . . . . . . . . 9 (𝜑 → (𝑁 − 2) ∈ ℕ0)
23 2nn0 11521 . . . . . . . . . 10 2 ∈ ℕ0
2423a1i 11 . . . . . . . . 9 (𝜑 → 2 ∈ ℕ0)
2522, 24nn0addcld 11567 . . . . . . . 8 (𝜑 → ((𝑁 − 2) + 2) ∈ ℕ0)
2620, 25eqeltrd 2839 . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
27 itgex 23756 . . . . . . . 8 ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥 ∈ V
2827a1i 11 . . . . . . 7 (𝜑 → ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥 ∈ V)
2913, 16, 26, 28fvmptd 6451 . . . . . 6 (𝜑 → (𝐼𝑁) = ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥)
30 ioosscn 40237 . . . . . . . . . . 11 (0(,)π) ⊆ ℂ
3130sseli 3740 . . . . . . . . . 10 (𝑥 ∈ (0(,)π) → 𝑥 ∈ ℂ)
3231sincld 15079 . . . . . . . . 9 (𝑥 ∈ (0(,)π) → (sin‘𝑥) ∈ ℂ)
3332adantl 473 . . . . . . . 8 ((𝜑𝑥 ∈ (0(,)π)) → (sin‘𝑥) ∈ ℂ)
3426adantr 472 . . . . . . . 8 ((𝜑𝑥 ∈ (0(,)π)) → 𝑁 ∈ ℕ0)
3533, 34expcld 13222 . . . . . . 7 ((𝜑𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑𝑁) ∈ ℂ)
36 ioossicc 12472 . . . . . . . . 9 (0(,)π) ⊆ (0[,]π)
3736a1i 11 . . . . . . . 8 (𝜑 → (0(,)π) ⊆ (0[,]π))
38 ioombl 23553 . . . . . . . . 9 (0(,)π) ∈ dom vol
3938a1i 11 . . . . . . . 8 (𝜑 → (0(,)π) ∈ dom vol)
40 0re 10252 . . . . . . . . . . . . . 14 0 ∈ ℝ
41 pire 24430 . . . . . . . . . . . . . 14 π ∈ ℝ
42 iccssre 12468 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ π ∈ ℝ) → (0[,]π) ⊆ ℝ)
4340, 41, 42mp2an 710 . . . . . . . . . . . . 13 (0[,]π) ⊆ ℝ
44 ax-resscn 10205 . . . . . . . . . . . . 13 ℝ ⊆ ℂ
4543, 44sstri 3753 . . . . . . . . . . . 12 (0[,]π) ⊆ ℂ
4645sseli 3740 . . . . . . . . . . 11 (𝑥 ∈ (0[,]π) → 𝑥 ∈ ℂ)
4746sincld 15079 . . . . . . . . . 10 (𝑥 ∈ (0[,]π) → (sin‘𝑥) ∈ ℂ)
4847adantl 473 . . . . . . . . 9 ((𝜑𝑥 ∈ (0[,]π)) → (sin‘𝑥) ∈ ℂ)
4926adantr 472 . . . . . . . . 9 ((𝜑𝑥 ∈ (0[,]π)) → 𝑁 ∈ ℕ0)
5048, 49expcld 13222 . . . . . . . 8 ((𝜑𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑𝑁) ∈ ℂ)
5140a1i 11 . . . . . . . . 9 (𝜑 → 0 ∈ ℝ)
5241a1i 11 . . . . . . . . 9 (𝜑 → π ∈ ℝ)
5346adantl 473 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0[,]π)) → 𝑥 ∈ ℂ)
54 eqid 2760 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) = (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁))
5554fvmpt2 6454 . . . . . . . . . . . . 13 ((𝑥 ∈ ℂ ∧ ((sin‘𝑥)↑𝑁) ∈ ℂ) → ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁))‘𝑥) = ((sin‘𝑥)↑𝑁))
5653, 50, 55syl2anc 696 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0[,]π)) → ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁))‘𝑥) = ((sin‘𝑥)↑𝑁))
5756eqcomd 2766 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑𝑁) = ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁))‘𝑥))
5857mpteq2dva 4896 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) = (𝑥 ∈ (0[,]π) ↦ ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁))‘𝑥)))
59 nfmpt1 4899 . . . . . . . . . . 11 𝑥(𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁))
60 nfcv 2902 . . . . . . . . . . . 12 𝑥sin
61 sincn 24417 . . . . . . . . . . . . 13 sin ∈ (ℂ–cn→ℂ)
6261a1i 11 . . . . . . . . . . . 12 (𝜑 → sin ∈ (ℂ–cn→ℂ))
6360, 62, 26expcnfg 40344 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) ∈ (ℂ–cn→ℂ))
6445a1i 11 . . . . . . . . . . 11 (𝜑 → (0[,]π) ⊆ ℂ)
6559, 63, 64cncfmptss 40340 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁))‘𝑥)) ∈ ((0[,]π)–cn→ℂ))
6658, 65eqeltrd 2839 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) ∈ ((0[,]π)–cn→ℂ))
67 cniccibl 23826 . . . . . . . . 9 ((0 ∈ ℝ ∧ π ∈ ℝ ∧ (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) ∈ ((0[,]π)–cn→ℂ)) → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) ∈ 𝐿1)
6851, 52, 66, 67syl3anc 1477 . . . . . . . 8 (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) ∈ 𝐿1)
6937, 39, 50, 68iblss 23790 . . . . . . 7 (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((sin‘𝑥)↑𝑁)) ∈ 𝐿1)
7035, 69itgcl 23769 . . . . . 6 (𝜑 → ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥 ∈ ℂ)
7129, 70eqeltrd 2839 . . . . 5 (𝜑 → (𝐼𝑁) ∈ ℂ)
7211, 71adddirp1d 10278 . . . 4 (𝜑 → (((𝑁 − 1) + 1) · (𝐼𝑁)) = (((𝑁 − 1) · (𝐼𝑁)) + (𝐼𝑁)))
73 eluz2b2 11974 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁))
741, 73sylib 208 . . . . . . . . . . 11 (𝜑 → (𝑁 ∈ ℕ ∧ 1 < 𝑁))
7574simpld 477 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
76 expm1t 13102 . . . . . . . . . 10 (((sin‘𝑥) ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((sin‘𝑥)↑𝑁) = (((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥)))
7732, 75, 76syl2anr 496 . . . . . . . . 9 ((𝜑𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑𝑁) = (((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥)))
7877itgeq2dv 23767 . . . . . . . 8 (𝜑 → ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥 = ∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥)) d𝑥)
79 eqid 2760 . . . . . . . . . 10 (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 1))) = (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 1)))
80 eqid 2760 . . . . . . . . . 10 (𝑥 ∈ ℂ ↦ -(cos‘𝑥)) = (𝑥 ∈ ℂ ↦ -(cos‘𝑥))
81 eqid 2760 . . . . . . . . . 10 (𝑥 ∈ ℂ ↦ (((𝑁 − 1) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) · (cos‘𝑥))) = (𝑥 ∈ ℂ ↦ (((𝑁 − 1) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) · (cos‘𝑥)))
82 eqid 2760 . . . . . . . . . 10 (𝑥 ∈ ℂ ↦ (((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥))) = (𝑥 ∈ ℂ ↦ (((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥)))
83 eqid 2760 . . . . . . . . . 10 (𝑥 ∈ ℂ ↦ ((((𝑁 − 1) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) · (cos‘𝑥)) · -(cos‘𝑥))) = (𝑥 ∈ ℂ ↦ ((((𝑁 − 1) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) · (cos‘𝑥)) · -(cos‘𝑥)))
84 eqid 2760 . . . . . . . . . 10 (𝑥 ∈ ℂ ↦ (((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1)))) = (𝑥 ∈ ℂ ↦ (((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1))))
8579, 80, 81, 82, 83, 84, 10itgsinexplem1 40690 . . . . . . . . 9 (𝜑 → ∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥)) d𝑥 = ((𝑁 − 1) · ∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) d𝑥))
864, 5, 5subsub4d 10635 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑁 − 1) − 1) = (𝑁 − (1 + 1)))
87 1p1e2 11346 . . . . . . . . . . . . . . . . 17 (1 + 1) = 2
8887a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (1 + 1) = 2)
8988oveq2d 6830 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 − (1 + 1)) = (𝑁 − 2))
9086, 89eqtrd 2794 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 − 1) − 1) = (𝑁 − 2))
9190adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0(,)π)) → ((𝑁 − 1) − 1) = (𝑁 − 2))
9291oveq2d 6830 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑((𝑁 − 1) − 1)) = ((sin‘𝑥)↑(𝑁 − 2)))
9392oveq2d 6830 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0(,)π)) → (((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) = (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))))
9493itgeq2dv 23767 . . . . . . . . . 10 (𝜑 → ∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) d𝑥 = ∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥)
9594oveq2d 6830 . . . . . . . . 9 (𝜑 → ((𝑁 − 1) · ∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) d𝑥) = ((𝑁 − 1) · ∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥))
96 sincossq 15125 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → (((sin‘𝑥)↑2) + ((cos‘𝑥)↑2)) = 1)
97 1cnd 10268 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → 1 ∈ ℂ)
98 sincl 15075 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℂ → (sin‘𝑥) ∈ ℂ)
9998sqcld 13220 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → ((sin‘𝑥)↑2) ∈ ℂ)
100 coscl 15076 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℂ → (cos‘𝑥) ∈ ℂ)
101100sqcld 13220 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → ((cos‘𝑥)↑2) ∈ ℂ)
10297, 99, 101subaddd 10622 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → ((1 − ((sin‘𝑥)↑2)) = ((cos‘𝑥)↑2) ↔ (((sin‘𝑥)↑2) + ((cos‘𝑥)↑2)) = 1))
10396, 102mpbird 247 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → (1 − ((sin‘𝑥)↑2)) = ((cos‘𝑥)↑2))
104103eqcomd 2766 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → ((cos‘𝑥)↑2) = (1 − ((sin‘𝑥)↑2)))
10531, 104syl 17 . . . . . . . . . . . . . 14 (𝑥 ∈ (0(,)π) → ((cos‘𝑥)↑2) = (1 − ((sin‘𝑥)↑2)))
106105oveq1d 6829 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) = ((1 − ((sin‘𝑥)↑2)) · ((sin‘𝑥)↑(𝑁 − 2))))
107106adantl 473 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0(,)π)) → (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) = ((1 − ((sin‘𝑥)↑2)) · ((sin‘𝑥)↑(𝑁 − 2))))
108107itgeq2dv 23767 . . . . . . . . . . 11 (𝜑 → ∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥 = ∫(0(,)π)((1 − ((sin‘𝑥)↑2)) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥)
109 1cnd 10268 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0(,)π)) → 1 ∈ ℂ)
11032sqcld 13220 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0(,)π) → ((sin‘𝑥)↑2) ∈ ℂ)
111110adantl 473 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑2) ∈ ℂ)
11290eqcomd 2766 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁 − 2) = ((𝑁 − 1) − 1))
113 nnm1nn0 11546 . . . . . . . . . . . . . . . . . 18 ((𝑁 − 1) ∈ ℕ → ((𝑁 − 1) − 1) ∈ ℕ0)
11410, 113syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑁 − 1) − 1) ∈ ℕ0)
115112, 114eqeltrd 2839 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 − 2) ∈ ℕ0)
116115adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (0(,)π)) → (𝑁 − 2) ∈ ℕ0)
11733, 116expcld 13222 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑(𝑁 − 2)) ∈ ℂ)
118109, 111, 117subdird 10699 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0(,)π)) → ((1 − ((sin‘𝑥)↑2)) · ((sin‘𝑥)↑(𝑁 − 2))) = ((1 · ((sin‘𝑥)↑(𝑁 − 2))) − (((sin‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2)))))
119117mulid2d 10270 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0(,)π)) → (1 · ((sin‘𝑥)↑(𝑁 − 2))) = ((sin‘𝑥)↑(𝑁 − 2)))
12023a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0(,)π)) → 2 ∈ ℕ0)
12133, 116, 120expaddd 13224 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑(2 + (𝑁 − 2))) = (((sin‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))))
12217, 4pncan3d 10607 . . . . . . . . . . . . . . . . 17 (𝜑 → (2 + (𝑁 − 2)) = 𝑁)
123122oveq2d 6830 . . . . . . . . . . . . . . . 16 (𝜑 → ((sin‘𝑥)↑(2 + (𝑁 − 2))) = ((sin‘𝑥)↑𝑁))
124123adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑(2 + (𝑁 − 2))) = ((sin‘𝑥)↑𝑁))
125121, 124eqtr3d 2796 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0(,)π)) → (((sin‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) = ((sin‘𝑥)↑𝑁))
126119, 125oveq12d 6832 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0(,)π)) → ((1 · ((sin‘𝑥)↑(𝑁 − 2))) − (((sin‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2)))) = (((sin‘𝑥)↑(𝑁 − 2)) − ((sin‘𝑥)↑𝑁)))
127118, 126eqtrd 2794 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0(,)π)) → ((1 − ((sin‘𝑥)↑2)) · ((sin‘𝑥)↑(𝑁 − 2))) = (((sin‘𝑥)↑(𝑁 − 2)) − ((sin‘𝑥)↑𝑁)))
128127itgeq2dv 23767 . . . . . . . . . . 11 (𝜑 → ∫(0(,)π)((1 − ((sin‘𝑥)↑2)) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥 = ∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 2)) − ((sin‘𝑥)↑𝑁)) d𝑥)
129115adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0[,]π)) → (𝑁 − 2) ∈ ℕ0)
13048, 129expcld 13222 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑(𝑁 − 2)) ∈ ℂ)
131 eqid 2760 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2))) = (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2)))
132131fvmpt2 6454 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ∧ ((sin‘𝑥)↑(𝑁 − 2)) ∈ ℂ) → ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2)))‘𝑥) = ((sin‘𝑥)↑(𝑁 − 2)))
13353, 130, 132syl2anc 696 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0[,]π)) → ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2)))‘𝑥) = ((sin‘𝑥)↑(𝑁 − 2)))
134133eqcomd 2766 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑(𝑁 − 2)) = ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2)))‘𝑥))
135134mpteq2dva 4896 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) = (𝑥 ∈ (0[,]π) ↦ ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2)))‘𝑥)))
136 nfmpt1 4899 . . . . . . . . . . . . . . . 16 𝑥(𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2)))
13760, 62, 115expcnfg 40344 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈ (ℂ–cn→ℂ))
138136, 137, 64cncfmptss 40340 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2)))‘𝑥)) ∈ ((0[,]π)–cn→ℂ))
139135, 138eqeltrd 2839 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈ ((0[,]π)–cn→ℂ))
140 cniccibl 23826 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ π ∈ ℝ ∧ (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈ ((0[,]π)–cn→ℂ)) → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈ 𝐿1)
14151, 52, 139, 140syl3anc 1477 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈ 𝐿1)
14237, 39, 130, 141iblss 23790 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈ 𝐿1)
143117, 142, 35, 69itgsub 23811 . . . . . . . . . . 11 (𝜑 → ∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 2)) − ((sin‘𝑥)↑𝑁)) d𝑥 = (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥))
144108, 128, 1433eqtrd 2798 . . . . . . . . . 10 (𝜑 → ∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥 = (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥))
145144oveq2d 6830 . . . . . . . . 9 (𝜑 → ((𝑁 − 1) · ∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥) = ((𝑁 − 1) · (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥)))
14685, 95, 1453eqtrd 2798 . . . . . . . 8 (𝜑 → ∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥)) d𝑥 = ((𝑁 − 1) · (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥)))
14729, 78, 1463eqtrd 2798 . . . . . . 7 (𝜑 → (𝐼𝑁) = ((𝑁 − 1) · (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥)))
148 oveq2 6822 . . . . . . . . . . . . 13 (𝑛 = (𝑁 − 2) → ((sin‘𝑥)↑𝑛) = ((sin‘𝑥)↑(𝑁 − 2)))
149148adantr 472 . . . . . . . . . . . 12 ((𝑛 = (𝑁 − 2) ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑𝑛) = ((sin‘𝑥)↑(𝑁 − 2)))
150149itgeq2dv 23767 . . . . . . . . . . 11 (𝑛 = (𝑁 − 2) → ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥 = ∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥)
151150adantl 473 . . . . . . . . . 10 ((𝜑𝑛 = (𝑁 − 2)) → ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥 = ∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥)
152 itgex 23756 . . . . . . . . . . 11 ∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 ∈ V
153152a1i 11 . . . . . . . . . 10 (𝜑 → ∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 ∈ V)
15413, 151, 115, 153fvmptd 6451 . . . . . . . . 9 (𝜑 → (𝐼‘(𝑁 − 2)) = ∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥)
155154, 29oveq12d 6832 . . . . . . . 8 (𝜑 → ((𝐼‘(𝑁 − 2)) − (𝐼𝑁)) = (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥))
156155oveq2d 6830 . . . . . . 7 (𝜑 → ((𝑁 − 1) · ((𝐼‘(𝑁 − 2)) − (𝐼𝑁))) = ((𝑁 − 1) · (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥)))
157117, 142itgcl 23769 . . . . . . . . 9 (𝜑 → ∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 ∈ ℂ)
158154, 157eqeltrd 2839 . . . . . . . 8 (𝜑 → (𝐼‘(𝑁 − 2)) ∈ ℂ)
15911, 158, 71subdid 10698 . . . . . . 7 (𝜑 → ((𝑁 − 1) · ((𝐼‘(𝑁 − 2)) − (𝐼𝑁))) = (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) − ((𝑁 − 1) · (𝐼𝑁))))
160147, 156, 1593eqtr2d 2800 . . . . . 6 (𝜑 → (𝐼𝑁) = (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) − ((𝑁 − 1) · (𝐼𝑁))))
161160eqcomd 2766 . . . . 5 (𝜑 → (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) − ((𝑁 − 1) · (𝐼𝑁))) = (𝐼𝑁))
16211, 158mulcld 10272 . . . . . 6 (𝜑 → ((𝑁 − 1) · (𝐼‘(𝑁 − 2))) ∈ ℂ)
16311, 71mulcld 10272 . . . . . 6 (𝜑 → ((𝑁 − 1) · (𝐼𝑁)) ∈ ℂ)
164162, 163, 71subaddd 10622 . . . . 5 (𝜑 → ((((𝑁 − 1) · (𝐼‘(𝑁 − 2))) − ((𝑁 − 1) · (𝐼𝑁))) = (𝐼𝑁) ↔ (((𝑁 − 1) · (𝐼𝑁)) + (𝐼𝑁)) = ((𝑁 − 1) · (𝐼‘(𝑁 − 2)))))
165161, 164mpbid 222 . . . 4 (𝜑 → (((𝑁 − 1) · (𝐼𝑁)) + (𝐼𝑁)) = ((𝑁 − 1) · (𝐼‘(𝑁 − 2))))
1668, 72, 1653eqtrd 2798 . . 3 (𝜑 → (𝑁 · (𝐼𝑁)) = ((𝑁 − 1) · (𝐼‘(𝑁 − 2))))
167166oveq1d 6829 . 2 (𝜑 → ((𝑁 · (𝐼𝑁)) / 𝑁) = (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) / 𝑁))
16875nnne0d 11277 . . 3 (𝜑𝑁 ≠ 0)
16971, 4, 168divcan3d 11018 . 2 (𝜑 → ((𝑁 · (𝐼𝑁)) / 𝑁) = (𝐼𝑁))
17011, 158, 4, 168div23d 11050 . 2 (𝜑 → (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) / 𝑁) = (((𝑁 − 1) / 𝑁) · (𝐼‘(𝑁 − 2))))
171167, 169, 1703eqtr3d 2802 1 (𝜑 → (𝐼𝑁) = (((𝑁 − 1) / 𝑁) · (𝐼‘(𝑁 − 2))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1632   ∈ wcel 2139  Vcvv 3340   ⊆ wss 3715   class class class wbr 4804   ↦ cmpt 4881  dom cdm 5266  ‘cfv 6049  (class class class)co 6814  ℂcc 10146  ℝcr 10147  0cc0 10148  1c1 10149   + caddc 10151   · cmul 10153   < clt 10286   − cmin 10478  -cneg 10479   / cdiv 10896  ℕcn 11232  2c2 11282  ℕ0cn0 11504  ℤcz 11589  ℤ≥cuz 11899  (,)cioo 12388  [,]cicc 12391  ↑cexp 13074  sincsin 15013  cosccos 15014  πcpi 15016  –cn→ccncf 22900  volcvol 23452  𝐿1cibl 23605  ∫citg 23606 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-inf2 8713  ax-cc 9469  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225  ax-pre-sup 10226  ax-addf 10227  ax-mulf 10228 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-disj 4773  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-of 7063  df-ofr 7064  df-om 7232  df-1st 7334  df-2nd 7335  df-supp 7465  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-1o 7730  df-2o 7731  df-oadd 7734  df-omul 7735  df-er 7913  df-map 8027  df-pm 8028  df-ixp 8077  df-en 8124  df-dom 8125  df-sdom 8126  df-fin 8127  df-fsupp 8443  df-fi 8484  df-sup 8515  df-inf 8516  df-oi 8582  df-card 8975  df-acn 8978  df-cda 9202  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-div 10897  df-nn 11233  df-2 11291  df-3 11292  df-4 11293  df-5 11294  df-6 11295  df-7 11296  df-8 11297  df-9 11298  df-n0 11505  df-z 11590  df-dec 11706  df-uz 11900  df-q 12002  df-rp 12046  df-xneg 12159  df-xadd 12160  df-xmul 12161  df-ioo 12392  df-ioc 12393  df-ico 12394  df-icc 12395  df-fz 12540  df-fzo 12680  df-fl 12807  df-mod 12883  df-seq 13016  df-exp 13075  df-fac 13275  df-bc 13304  df-hash 13332  df-shft 14026  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-limsup 14421  df-clim 14438  df-rlim 14439  df-sum 14636  df-ef 15017  df-sin 15019  df-cos 15020  df-pi 15022  df-struct 16081  df-ndx 16082  df-slot 16083  df-base 16085  df-sets 16086  df-ress 16087  df-plusg 16176  df-mulr 16177  df-starv 16178  df-sca 16179  df-vsca 16180  df-ip 16181  df-tset 16182  df-ple 16183  df-ds 16186  df-unif 16187  df-hom 16188  df-cco 16189  df-rest 16305  df-topn 16306  df-0g 16324  df-gsum 16325  df-topgen 16326  df-pt 16327  df-prds 16330  df-xrs 16384  df-qtop 16389  df-imas 16390  df-xps 16392  df-mre 16468  df-mrc 16469  df-acs 16471  df-mgm 17463  df-sgrp 17505  df-mnd 17516  df-submnd 17557  df-mulg 17762  df-cntz 17970  df-cmn 18415  df-psmet 19960  df-xmet 19961  df-met 19962  df-bl 19963  df-mopn 19964  df-fbas 19965  df-fg 19966  df-cnfld 19969  df-top 20921  df-topon 20938  df-topsp 20959  df-bases 20972  df-cld 21045  df-ntr 21046  df-cls 21047  df-nei 21124  df-lp 21162  df-perf 21163  df-cn 21253  df-cnp 21254  df-haus 21341  df-cmp 21412  df-tx 21587  df-hmeo 21780  df-fil 21871  df-fm 21963  df-flim 21964  df-flf 21965  df-xms 22346  df-ms 22347  df-tms 22348  df-cncf 22902  df-ovol 23453  df-vol 23454  df-mbf 23607  df-itg1 23608  df-itg2 23609  df-ibl 23610  df-itg 23611  df-0p 23656  df-limc 23849  df-dv 23850 This theorem is referenced by:  wallispilem2  40804  wallispilem4  40806  wallispilem5  40807
 Copyright terms: Public domain W3C validator