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

Theorem itgsinexp 41670
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 12062 . . . . . . . 8 (𝑁 ∈ (ℤ‘2) → 𝑁 ∈ ℤ)
3 zcn 11792 . . . . . . . 8 (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
41, 2, 33syl 18 . . . . . . 7 (𝜑𝑁 ∈ ℂ)
5 1cnd 10428 . . . . . . 7 (𝜑 → 1 ∈ ℂ)
64, 5npcand 10796 . . . . . 6 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
76eqcomd 2778 . . . . 5 (𝜑𝑁 = ((𝑁 − 1) + 1))
87oveq1d 6985 . . . 4 (𝜑 → (𝑁 · (𝐼𝑁)) = (((𝑁 − 1) + 1) · (𝐼𝑁)))
9 uz2m1nn 12131 . . . . . . 7 (𝑁 ∈ (ℤ‘2) → (𝑁 − 1) ∈ ℕ)
101, 9syl 17 . . . . . 6 (𝜑 → (𝑁 − 1) ∈ ℕ)
1110nncnd 11451 . . . . 5 (𝜑 → (𝑁 − 1) ∈ ℂ)
12 itgsinexp.1 . . . . . . . 8 𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)
1312a1i 11 . . . . . . 7 (𝜑𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥))
14 oveq2 6978 . . . . . . . . 9 (𝑛 = 𝑁 → ((sin‘𝑥)↑𝑛) = ((sin‘𝑥)↑𝑁))
1514ad2antlr 714 . . . . . . . 8 (((𝜑𝑛 = 𝑁) ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑𝑛) = ((sin‘𝑥)↑𝑁))
1615itgeq2dv 24079 . . . . . . 7 ((𝜑𝑛 = 𝑁) → ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥 = ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥)
17 2cnd 11512 . . . . . . . . 9 (𝜑 → 2 ∈ ℂ)
18 npcan 10690 . . . . . . . . . 10 ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑁 − 2) + 2) = 𝑁)
1918eqcomd 2778 . . . . . . . . 9 ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ) → 𝑁 = ((𝑁 − 2) + 2))
204, 17, 19syl2anc 576 . . . . . . . 8 (𝜑𝑁 = ((𝑁 − 2) + 2))
21 uznn0sub 12085 . . . . . . . . . 10 (𝑁 ∈ (ℤ‘2) → (𝑁 − 2) ∈ ℕ0)
221, 21syl 17 . . . . . . . . 9 (𝜑 → (𝑁 − 2) ∈ ℕ0)
23 2nn0 11720 . . . . . . . . . 10 2 ∈ ℕ0
2423a1i 11 . . . . . . . . 9 (𝜑 → 2 ∈ ℕ0)
2522, 24nn0addcld 11765 . . . . . . . 8 (𝜑 → ((𝑁 − 2) + 2) ∈ ℕ0)
2620, 25eqeltrd 2860 . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
27 itgex 24068 . . . . . . . 8 ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥 ∈ V
2827a1i 11 . . . . . . 7 (𝜑 → ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥 ∈ V)
2913, 16, 26, 28fvmptd 6595 . . . . . 6 (𝜑 → (𝐼𝑁) = ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥)
30 ioosscn 41200 . . . . . . . . . . 11 (0(,)π) ⊆ ℂ
3130sseli 3848 . . . . . . . . . 10 (𝑥 ∈ (0(,)π) → 𝑥 ∈ ℂ)
3231sincld 15337 . . . . . . . . 9 (𝑥 ∈ (0(,)π) → (sin‘𝑥) ∈ ℂ)
3332adantl 474 . . . . . . . 8 ((𝜑𝑥 ∈ (0(,)π)) → (sin‘𝑥) ∈ ℂ)
3426adantr 473 . . . . . . . 8 ((𝜑𝑥 ∈ (0(,)π)) → 𝑁 ∈ ℕ0)
3533, 34expcld 13319 . . . . . . 7 ((𝜑𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑𝑁) ∈ ℂ)
36 ioossicc 12632 . . . . . . . . 9 (0(,)π) ⊆ (0[,]π)
3736a1i 11 . . . . . . . 8 (𝜑 → (0(,)π) ⊆ (0[,]π))
38 ioombl 23863 . . . . . . . . 9 (0(,)π) ∈ dom vol
3938a1i 11 . . . . . . . 8 (𝜑 → (0(,)π) ∈ dom vol)
40 0re 10435 . . . . . . . . . . . . . 14 0 ∈ ℝ
41 pire 24741 . . . . . . . . . . . . . 14 π ∈ ℝ
42 iccssre 12628 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ π ∈ ℝ) → (0[,]π) ⊆ ℝ)
4340, 41, 42mp2an 679 . . . . . . . . . . . . 13 (0[,]π) ⊆ ℝ
44 ax-resscn 10386 . . . . . . . . . . . . 13 ℝ ⊆ ℂ
4543, 44sstri 3861 . . . . . . . . . . . 12 (0[,]π) ⊆ ℂ
4645sseli 3848 . . . . . . . . . . 11 (𝑥 ∈ (0[,]π) → 𝑥 ∈ ℂ)
4746sincld 15337 . . . . . . . . . 10 (𝑥 ∈ (0[,]π) → (sin‘𝑥) ∈ ℂ)
4847adantl 474 . . . . . . . . 9 ((𝜑𝑥 ∈ (0[,]π)) → (sin‘𝑥) ∈ ℂ)
4926adantr 473 . . . . . . . . 9 ((𝜑𝑥 ∈ (0[,]π)) → 𝑁 ∈ ℕ0)
5048, 49expcld 13319 . . . . . . . 8 ((𝜑𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑𝑁) ∈ ℂ)
5140a1i 11 . . . . . . . . 9 (𝜑 → 0 ∈ ℝ)
5241a1i 11 . . . . . . . . 9 (𝜑 → π ∈ ℝ)
5346adantl 474 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0[,]π)) → 𝑥 ∈ ℂ)
54 eqid 2772 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) = (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁))
5554fvmpt2 6599 . . . . . . . . . . . . 13 ((𝑥 ∈ ℂ ∧ ((sin‘𝑥)↑𝑁) ∈ ℂ) → ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁))‘𝑥) = ((sin‘𝑥)↑𝑁))
5653, 50, 55syl2anc 576 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0[,]π)) → ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁))‘𝑥) = ((sin‘𝑥)↑𝑁))
5756eqcomd 2778 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑𝑁) = ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁))‘𝑥))
5857mpteq2dva 5016 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) = (𝑥 ∈ (0[,]π) ↦ ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁))‘𝑥)))
59 nfmpt1 5019 . . . . . . . . . . 11 𝑥(𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁))
60 nfcv 2926 . . . . . . . . . . . 12 𝑥sin
61 sincn 24729 . . . . . . . . . . . . 13 sin ∈ (ℂ–cn→ℂ)
6261a1i 11 . . . . . . . . . . . 12 (𝜑 → sin ∈ (ℂ–cn→ℂ))
6360, 62, 26expcnfg 41303 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) ∈ (ℂ–cn→ℂ))
6445a1i 11 . . . . . . . . . . 11 (𝜑 → (0[,]π) ⊆ ℂ)
6559, 63, 64cncfmptss 41299 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁))‘𝑥)) ∈ ((0[,]π)–cn→ℂ))
6658, 65eqeltrd 2860 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) ∈ ((0[,]π)–cn→ℂ))
67 cniccibl 24138 . . . . . . . . 9 ((0 ∈ ℝ ∧ π ∈ ℝ ∧ (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) ∈ ((0[,]π)–cn→ℂ)) → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) ∈ 𝐿1)
6851, 52, 66, 67syl3anc 1351 . . . . . . . 8 (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) ∈ 𝐿1)
6937, 39, 50, 68iblss 24102 . . . . . . 7 (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((sin‘𝑥)↑𝑁)) ∈ 𝐿1)
7035, 69itgcl 24081 . . . . . 6 (𝜑 → ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥 ∈ ℂ)
7129, 70eqeltrd 2860 . . . . 5 (𝜑 → (𝐼𝑁) ∈ ℂ)
7211, 71adddirp1d 10460 . . . 4 (𝜑 → (((𝑁 − 1) + 1) · (𝐼𝑁)) = (((𝑁 − 1) · (𝐼𝑁)) + (𝐼𝑁)))
73 eluz2b2 12129 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁))
741, 73sylib 210 . . . . . . . . . . 11 (𝜑 → (𝑁 ∈ ℕ ∧ 1 < 𝑁))
7574simpld 487 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
76 expm1t 13266 . . . . . . . . . 10 (((sin‘𝑥) ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((sin‘𝑥)↑𝑁) = (((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥)))
7732, 75, 76syl2anr 587 . . . . . . . . 9 ((𝜑𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑𝑁) = (((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥)))
7877itgeq2dv 24079 . . . . . . . 8 (𝜑 → ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥 = ∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥)) d𝑥)
79 eqid 2772 . . . . . . . . . 10 (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 1))) = (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 1)))
80 eqid 2772 . . . . . . . . . 10 (𝑥 ∈ ℂ ↦ -(cos‘𝑥)) = (𝑥 ∈ ℂ ↦ -(cos‘𝑥))
81 eqid 2772 . . . . . . . . . 10 (𝑥 ∈ ℂ ↦ (((𝑁 − 1) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) · (cos‘𝑥))) = (𝑥 ∈ ℂ ↦ (((𝑁 − 1) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) · (cos‘𝑥)))
82 eqid 2772 . . . . . . . . . 10 (𝑥 ∈ ℂ ↦ (((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥))) = (𝑥 ∈ ℂ ↦ (((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥)))
83 eqid 2772 . . . . . . . . . 10 (𝑥 ∈ ℂ ↦ ((((𝑁 − 1) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) · (cos‘𝑥)) · -(cos‘𝑥))) = (𝑥 ∈ ℂ ↦ ((((𝑁 − 1) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) · (cos‘𝑥)) · -(cos‘𝑥)))
84 eqid 2772 . . . . . . . . . 10 (𝑥 ∈ ℂ ↦ (((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1)))) = (𝑥 ∈ ℂ ↦ (((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1))))
8579, 80, 81, 82, 83, 84, 10itgsinexplem1 41669 . . . . . . . . 9 (𝜑 → ∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥)) d𝑥 = ((𝑁 − 1) · ∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) d𝑥))
864, 5, 5subsub4d 10823 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑁 − 1) − 1) = (𝑁 − (1 + 1)))
87 1p1e2 11566 . . . . . . . . . . . . . . . . 17 (1 + 1) = 2
8887a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (1 + 1) = 2)
8988oveq2d 6986 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 − (1 + 1)) = (𝑁 − 2))
9086, 89eqtrd 2808 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 − 1) − 1) = (𝑁 − 2))
9190adantr 473 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0(,)π)) → ((𝑁 − 1) − 1) = (𝑁 − 2))
9291oveq2d 6986 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑((𝑁 − 1) − 1)) = ((sin‘𝑥)↑(𝑁 − 2)))
9392oveq2d 6986 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0(,)π)) → (((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) = (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))))
9493itgeq2dv 24079 . . . . . . . . . 10 (𝜑 → ∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) d𝑥 = ∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥)
9594oveq2d 6986 . . . . . . . . 9 (𝜑 → ((𝑁 − 1) · ∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) d𝑥) = ((𝑁 − 1) · ∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥))
96 sincossq 15383 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → (((sin‘𝑥)↑2) + ((cos‘𝑥)↑2)) = 1)
97 1cnd 10428 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → 1 ∈ ℂ)
98 sincl 15333 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℂ → (sin‘𝑥) ∈ ℂ)
9998sqcld 13317 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → ((sin‘𝑥)↑2) ∈ ℂ)
100 coscl 15334 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℂ → (cos‘𝑥) ∈ ℂ)
101100sqcld 13317 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → ((cos‘𝑥)↑2) ∈ ℂ)
10297, 99, 101subaddd 10810 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → ((1 − ((sin‘𝑥)↑2)) = ((cos‘𝑥)↑2) ↔ (((sin‘𝑥)↑2) + ((cos‘𝑥)↑2)) = 1))
10396, 102mpbird 249 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → (1 − ((sin‘𝑥)↑2)) = ((cos‘𝑥)↑2))
104103eqcomd 2778 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → ((cos‘𝑥)↑2) = (1 − ((sin‘𝑥)↑2)))
10531, 104syl 17 . . . . . . . . . . . . . 14 (𝑥 ∈ (0(,)π) → ((cos‘𝑥)↑2) = (1 − ((sin‘𝑥)↑2)))
106105oveq1d 6985 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) = ((1 − ((sin‘𝑥)↑2)) · ((sin‘𝑥)↑(𝑁 − 2))))
107106adantl 474 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0(,)π)) → (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) = ((1 − ((sin‘𝑥)↑2)) · ((sin‘𝑥)↑(𝑁 − 2))))
108107itgeq2dv 24079 . . . . . . . . . . 11 (𝜑 → ∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥 = ∫(0(,)π)((1 − ((sin‘𝑥)↑2)) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥)
109 1cnd 10428 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0(,)π)) → 1 ∈ ℂ)
11032sqcld 13317 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0(,)π) → ((sin‘𝑥)↑2) ∈ ℂ)
111110adantl 474 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑2) ∈ ℂ)
11290eqcomd 2778 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁 − 2) = ((𝑁 − 1) − 1))
113 nnm1nn0 11744 . . . . . . . . . . . . . . . . . 18 ((𝑁 − 1) ∈ ℕ → ((𝑁 − 1) − 1) ∈ ℕ0)
11410, 113syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑁 − 1) − 1) ∈ ℕ0)
115112, 114eqeltrd 2860 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 − 2) ∈ ℕ0)
116115adantr 473 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (0(,)π)) → (𝑁 − 2) ∈ ℕ0)
11733, 116expcld 13319 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑(𝑁 − 2)) ∈ ℂ)
118109, 111, 117subdird 10892 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0(,)π)) → ((1 − ((sin‘𝑥)↑2)) · ((sin‘𝑥)↑(𝑁 − 2))) = ((1 · ((sin‘𝑥)↑(𝑁 − 2))) − (((sin‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2)))))
119117mulid2d 10452 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0(,)π)) → (1 · ((sin‘𝑥)↑(𝑁 − 2))) = ((sin‘𝑥)↑(𝑁 − 2)))
12023a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0(,)π)) → 2 ∈ ℕ0)
12133, 116, 120expaddd 13321 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑(2 + (𝑁 − 2))) = (((sin‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))))
12217, 4pncan3d 10795 . . . . . . . . . . . . . . . . 17 (𝜑 → (2 + (𝑁 − 2)) = 𝑁)
123122oveq2d 6986 . . . . . . . . . . . . . . . 16 (𝜑 → ((sin‘𝑥)↑(2 + (𝑁 − 2))) = ((sin‘𝑥)↑𝑁))
124123adantr 473 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑(2 + (𝑁 − 2))) = ((sin‘𝑥)↑𝑁))
125121, 124eqtr3d 2810 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0(,)π)) → (((sin‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) = ((sin‘𝑥)↑𝑁))
126119, 125oveq12d 6988 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0(,)π)) → ((1 · ((sin‘𝑥)↑(𝑁 − 2))) − (((sin‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2)))) = (((sin‘𝑥)↑(𝑁 − 2)) − ((sin‘𝑥)↑𝑁)))
127118, 126eqtrd 2808 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0(,)π)) → ((1 − ((sin‘𝑥)↑2)) · ((sin‘𝑥)↑(𝑁 − 2))) = (((sin‘𝑥)↑(𝑁 − 2)) − ((sin‘𝑥)↑𝑁)))
128127itgeq2dv 24079 . . . . . . . . . . 11 (𝜑 → ∫(0(,)π)((1 − ((sin‘𝑥)↑2)) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥 = ∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 2)) − ((sin‘𝑥)↑𝑁)) d𝑥)
129115adantr 473 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0[,]π)) → (𝑁 − 2) ∈ ℕ0)
13048, 129expcld 13319 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑(𝑁 − 2)) ∈ ℂ)
131 eqid 2772 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2))) = (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2)))
132131fvmpt2 6599 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ∧ ((sin‘𝑥)↑(𝑁 − 2)) ∈ ℂ) → ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2)))‘𝑥) = ((sin‘𝑥)↑(𝑁 − 2)))
13353, 130, 132syl2anc 576 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0[,]π)) → ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2)))‘𝑥) = ((sin‘𝑥)↑(𝑁 − 2)))
134133eqcomd 2778 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑(𝑁 − 2)) = ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2)))‘𝑥))
135134mpteq2dva 5016 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) = (𝑥 ∈ (0[,]π) ↦ ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2)))‘𝑥)))
136 nfmpt1 5019 . . . . . . . . . . . . . . . 16 𝑥(𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2)))
13760, 62, 115expcnfg 41303 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈ (ℂ–cn→ℂ))
138136, 137, 64cncfmptss 41299 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2)))‘𝑥)) ∈ ((0[,]π)–cn→ℂ))
139135, 138eqeltrd 2860 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈ ((0[,]π)–cn→ℂ))
140 cniccibl 24138 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ π ∈ ℝ ∧ (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈ ((0[,]π)–cn→ℂ)) → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈ 𝐿1)
14151, 52, 139, 140syl3anc 1351 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈ 𝐿1)
14237, 39, 130, 141iblss 24102 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈ 𝐿1)
143117, 142, 35, 69itgsub 24123 . . . . . . . . . . 11 (𝜑 → ∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 2)) − ((sin‘𝑥)↑𝑁)) d𝑥 = (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥))
144108, 128, 1433eqtrd 2812 . . . . . . . . . 10 (𝜑 → ∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥 = (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥))
145144oveq2d 6986 . . . . . . . . 9 (𝜑 → ((𝑁 − 1) · ∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥) = ((𝑁 − 1) · (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥)))
14685, 95, 1453eqtrd 2812 . . . . . . . 8 (𝜑 → ∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥)) d𝑥 = ((𝑁 − 1) · (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥)))
14729, 78, 1463eqtrd 2812 . . . . . . 7 (𝜑 → (𝐼𝑁) = ((𝑁 − 1) · (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥)))
148 oveq2 6978 . . . . . . . . . . . 12 (𝑛 = (𝑁 − 2) → ((sin‘𝑥)↑𝑛) = ((sin‘𝑥)↑(𝑁 − 2)))
149148adantr 473 . . . . . . . . . . 11 ((𝑛 = (𝑁 − 2) ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑𝑛) = ((sin‘𝑥)↑(𝑁 − 2)))
150149itgeq2dv 24079 . . . . . . . . . 10 (𝑛 = (𝑁 − 2) → ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥 = ∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥)
151 itgex 24068 . . . . . . . . . . 11 ∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 ∈ V
152151a1i 11 . . . . . . . . . 10 (𝜑 → ∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 ∈ V)
15312, 150, 115, 152fvmptd3 6611 . . . . . . . . 9 (𝜑 → (𝐼‘(𝑁 − 2)) = ∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥)
154153, 29oveq12d 6988 . . . . . . . 8 (𝜑 → ((𝐼‘(𝑁 − 2)) − (𝐼𝑁)) = (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥))
155154oveq2d 6986 . . . . . . 7 (𝜑 → ((𝑁 − 1) · ((𝐼‘(𝑁 − 2)) − (𝐼𝑁))) = ((𝑁 − 1) · (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥)))
156117, 142itgcl 24081 . . . . . . . . 9 (𝜑 → ∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 ∈ ℂ)
157153, 156eqeltrd 2860 . . . . . . . 8 (𝜑 → (𝐼‘(𝑁 − 2)) ∈ ℂ)
15811, 157, 71subdid 10891 . . . . . . 7 (𝜑 → ((𝑁 − 1) · ((𝐼‘(𝑁 − 2)) − (𝐼𝑁))) = (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) − ((𝑁 − 1) · (𝐼𝑁))))
159147, 155, 1583eqtr2d 2814 . . . . . 6 (𝜑 → (𝐼𝑁) = (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) − ((𝑁 − 1) · (𝐼𝑁))))
160159eqcomd 2778 . . . . 5 (𝜑 → (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) − ((𝑁 − 1) · (𝐼𝑁))) = (𝐼𝑁))
16111, 157mulcld 10454 . . . . . 6 (𝜑 → ((𝑁 − 1) · (𝐼‘(𝑁 − 2))) ∈ ℂ)
16211, 71mulcld 10454 . . . . . 6 (𝜑 → ((𝑁 − 1) · (𝐼𝑁)) ∈ ℂ)
163161, 162, 71subaddd 10810 . . . . 5 (𝜑 → ((((𝑁 − 1) · (𝐼‘(𝑁 − 2))) − ((𝑁 − 1) · (𝐼𝑁))) = (𝐼𝑁) ↔ (((𝑁 − 1) · (𝐼𝑁)) + (𝐼𝑁)) = ((𝑁 − 1) · (𝐼‘(𝑁 − 2)))))
164160, 163mpbid 224 . . . 4 (𝜑 → (((𝑁 − 1) · (𝐼𝑁)) + (𝐼𝑁)) = ((𝑁 − 1) · (𝐼‘(𝑁 − 2))))
1658, 72, 1643eqtrd 2812 . . 3 (𝜑 → (𝑁 · (𝐼𝑁)) = ((𝑁 − 1) · (𝐼‘(𝑁 − 2))))
166165oveq1d 6985 . 2 (𝜑 → ((𝑁 · (𝐼𝑁)) / 𝑁) = (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) / 𝑁))
16775nnne0d 11484 . . 3 (𝜑𝑁 ≠ 0)
16871, 4, 167divcan3d 11216 . 2 (𝜑 → ((𝑁 · (𝐼𝑁)) / 𝑁) = (𝐼𝑁))
16911, 157, 4, 167div23d 11248 . 2 (𝜑 → (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) / 𝑁) = (((𝑁 − 1) / 𝑁) · (𝐼‘(𝑁 − 2))))
170166, 168, 1693eqtr3d 2816 1 (𝜑 → (𝐼𝑁) = (((𝑁 − 1) / 𝑁) · (𝐼‘(𝑁 − 2))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387   = wceq 1507  wcel 2050  Vcvv 3409  wss 3823   class class class wbr 4923  cmpt 5002  dom cdm 5401  cfv 6182  (class class class)co 6970  cc 10327  cr 10328  0cc0 10329  1c1 10330   + caddc 10332   · cmul 10334   < clt 10468  cmin 10664  -cneg 10665   / cdiv 11092  cn 11433  2c2 11489  0cn0 11701  cz 11787  cuz 12052  (,)cioo 12548  [,]cicc 12551  cexp 13238  sincsin 15271  cosccos 15272  πcpi 15274  cnccncf 23181  volcvol 23761  𝐿1cibl 23915  citg 23916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-inf2 8892  ax-cc 9649  ax-cnex 10385  ax-resscn 10386  ax-1cn 10387  ax-icn 10388  ax-addcl 10389  ax-addrcl 10390  ax-mulcl 10391  ax-mulrcl 10392  ax-mulcom 10393  ax-addass 10394  ax-mulass 10395  ax-distr 10396  ax-i2m1 10397  ax-1ne0 10398  ax-1rid 10399  ax-rnegex 10400  ax-rrecex 10401  ax-cnre 10402  ax-pre-lttri 10403  ax-pre-lttrn 10404  ax-pre-ltadd 10405  ax-pre-mulgt0 10406  ax-pre-sup 10407  ax-addf 10408  ax-mulf 10409
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3676  df-csb 3781  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-pss 3839  df-symdif 4100  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4707  df-int 4744  df-iun 4788  df-iin 4789  df-disj 4892  df-br 4924  df-opab 4986  df-mpt 5003  df-tr 5025  df-id 5306  df-eprel 5311  df-po 5320  df-so 5321  df-fr 5360  df-se 5361  df-we 5362  df-xp 5407  df-rel 5408  df-cnv 5409  df-co 5410  df-dm 5411  df-rn 5412  df-res 5413  df-ima 5414  df-pred 5980  df-ord 6026  df-on 6027  df-lim 6028  df-suc 6029  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-isom 6191  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-of 7221  df-ofr 7222  df-om 7391  df-1st 7495  df-2nd 7496  df-supp 7628  df-wrecs 7744  df-recs 7806  df-rdg 7844  df-1o 7899  df-2o 7900  df-oadd 7903  df-omul 7904  df-er 8083  df-map 8202  df-pm 8203  df-ixp 8254  df-en 8301  df-dom 8302  df-sdom 8303  df-fin 8304  df-fsupp 8623  df-fi 8664  df-sup 8695  df-inf 8696  df-oi 8763  df-dju 9118  df-card 9156  df-acn 9159  df-cda 9382  df-pnf 10470  df-mnf 10471  df-xr 10472  df-ltxr 10473  df-le 10474  df-sub 10666  df-neg 10667  df-div 11093  df-nn 11434  df-2 11497  df-3 11498  df-4 11499  df-5 11500  df-6 11501  df-7 11502  df-8 11503  df-9 11504  df-n0 11702  df-z 11788  df-dec 11906  df-uz 12053  df-q 12157  df-rp 12199  df-xneg 12318  df-xadd 12319  df-xmul 12320  df-ioo 12552  df-ioc 12553  df-ico 12554  df-icc 12555  df-fz 12703  df-fzo 12844  df-fl 12971  df-mod 13047  df-seq 13179  df-exp 13239  df-fac 13443  df-bc 13472  df-hash 13500  df-shft 14281  df-cj 14313  df-re 14314  df-im 14315  df-sqrt 14449  df-abs 14450  df-limsup 14683  df-clim 14700  df-rlim 14701  df-sum 14898  df-ef 15275  df-sin 15277  df-cos 15278  df-pi 15280  df-struct 16335  df-ndx 16336  df-slot 16337  df-base 16339  df-sets 16340  df-ress 16341  df-plusg 16428  df-mulr 16429  df-starv 16430  df-sca 16431  df-vsca 16432  df-ip 16433  df-tset 16434  df-ple 16435  df-ds 16437  df-unif 16438  df-hom 16439  df-cco 16440  df-rest 16546  df-topn 16547  df-0g 16565  df-gsum 16566  df-topgen 16567  df-pt 16568  df-prds 16571  df-xrs 16625  df-qtop 16630  df-imas 16631  df-xps 16633  df-mre 16709  df-mrc 16710  df-acs 16712  df-mgm 17704  df-sgrp 17746  df-mnd 17757  df-submnd 17798  df-mulg 18006  df-cntz 18212  df-cmn 18662  df-psmet 20233  df-xmet 20234  df-met 20235  df-bl 20236  df-mopn 20237  df-fbas 20238  df-fg 20239  df-cnfld 20242  df-top 21200  df-topon 21217  df-topsp 21239  df-bases 21252  df-cld 21325  df-ntr 21326  df-cls 21327  df-nei 21404  df-lp 21442  df-perf 21443  df-cn 21533  df-cnp 21534  df-haus 21621  df-cmp 21693  df-tx 21868  df-hmeo 22061  df-fil 22152  df-fm 22244  df-flim 22245  df-flf 22246  df-xms 22627  df-ms 22628  df-tms 22629  df-cncf 23183  df-ovol 23762  df-vol 23763  df-mbf 23917  df-itg1 23918  df-itg2 23919  df-ibl 23920  df-itg 23921  df-0p 23968  df-limc 24161  df-dv 24162
This theorem is referenced by:  wallispilem2  41782  wallispilem4  41784  wallispilem5  41785
  Copyright terms: Public domain W3C validator