Proof of Theorem itgsinexp
| Step | Hyp | Ref
| Expression |
| 1 | | itgsinexp.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘2)) |
| 2 | | eluzelz 12888 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℤ) |
| 3 | | zcn 12618 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
| 4 | 1, 2, 3 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 5 | | 1cnd 11256 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℂ) |
| 6 | 4, 5 | npcand 11624 |
. . . . . 6
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
| 7 | 6 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 → 𝑁 = ((𝑁 − 1) + 1)) |
| 8 | 7 | oveq1d 7446 |
. . . 4
⊢ (𝜑 → (𝑁 · (𝐼‘𝑁)) = (((𝑁 − 1) + 1) · (𝐼‘𝑁))) |
| 9 | | uz2m1nn 12965 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 1) ∈ ℕ) |
| 10 | 1, 9 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑁 − 1) ∈ ℕ) |
| 11 | 10 | nncnd 12282 |
. . . . 5
⊢ (𝜑 → (𝑁 − 1) ∈ ℂ) |
| 12 | | itgsinexp.1 |
. . . . . . . 8
⊢ 𝐼 = (𝑛 ∈ ℕ0 ↦
∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥) |
| 13 | 12 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐼 = (𝑛 ∈ ℕ0 ↦
∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)) |
| 14 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → ((sin‘𝑥)↑𝑛) = ((sin‘𝑥)↑𝑁)) |
| 15 | 14 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑𝑛) = ((sin‘𝑥)↑𝑁)) |
| 16 | 15 | itgeq2dv 25817 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥 = ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥) |
| 17 | | 2cnd 12344 |
. . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℂ) |
| 18 | | npcan 11517 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ) → ((𝑁 −
2) + 2) = 𝑁) |
| 19 | 18 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ) → 𝑁 = ((𝑁 − 2) +
2)) |
| 20 | 4, 17, 19 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 = ((𝑁 − 2) + 2)) |
| 21 | | uznn0sub 12917 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 2) ∈
ℕ0) |
| 22 | 1, 21 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 − 2) ∈
ℕ0) |
| 23 | | 2nn0 12543 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
| 24 | 23 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℕ0) |
| 25 | 22, 24 | nn0addcld 12591 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 − 2) + 2) ∈
ℕ0) |
| 26 | 20, 25 | eqeltrd 2841 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 27 | | itgex 25805 |
. . . . . . . 8
⊢
∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥 ∈ V |
| 28 | 27 | a1i 11 |
. . . . . . 7
⊢ (𝜑 →
∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥 ∈ V) |
| 29 | 13, 16, 26, 28 | fvmptd 7023 |
. . . . . 6
⊢ (𝜑 → (𝐼‘𝑁) = ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥) |
| 30 | | ioosscn 13449 |
. . . . . . . . . . 11
⊢
(0(,)π) ⊆ ℂ |
| 31 | 30 | sseli 3979 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0(,)π) → 𝑥 ∈
ℂ) |
| 32 | 31 | sincld 16166 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0(,)π) →
(sin‘𝑥) ∈
ℂ) |
| 33 | 32 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (sin‘𝑥) ∈
ℂ) |
| 34 | 26 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → 𝑁 ∈
ℕ0) |
| 35 | 33, 34 | expcld 14186 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑𝑁) ∈ ℂ) |
| 36 | | ioossicc 13473 |
. . . . . . . . 9
⊢
(0(,)π) ⊆ (0[,]π) |
| 37 | 36 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (0(,)π) ⊆
(0[,]π)) |
| 38 | | ioombl 25600 |
. . . . . . . . 9
⊢
(0(,)π) ∈ dom vol |
| 39 | 38 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (0(,)π) ∈ dom
vol) |
| 40 | | 0re 11263 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
| 41 | | pire 26500 |
. . . . . . . . . . . . . 14
⊢ π
∈ ℝ |
| 42 | | iccssre 13469 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ π ∈ ℝ) → (0[,]π) ⊆
ℝ) |
| 43 | 40, 41, 42 | mp2an 692 |
. . . . . . . . . . . . 13
⊢
(0[,]π) ⊆ ℝ |
| 44 | | ax-resscn 11212 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℂ |
| 45 | 43, 44 | sstri 3993 |
. . . . . . . . . . . 12
⊢
(0[,]π) ⊆ ℂ |
| 46 | 45 | sseli 3979 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0[,]π) → 𝑥 ∈
ℂ) |
| 47 | 46 | sincld 16166 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0[,]π) →
(sin‘𝑥) ∈
ℂ) |
| 48 | 47 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (sin‘𝑥) ∈
ℂ) |
| 49 | 26 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → 𝑁 ∈
ℕ0) |
| 50 | 48, 49 | expcld 14186 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑𝑁) ∈ ℂ) |
| 51 | 40 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℝ) |
| 52 | 41 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → π ∈
ℝ) |
| 53 | 46 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → 𝑥 ∈ ℂ) |
| 54 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁)) = (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) |
| 55 | 54 | fvmpt2 7027 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧
((sin‘𝑥)↑𝑁) ∈ ℂ) → ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁))‘𝑥) = ((sin‘𝑥)↑𝑁)) |
| 56 | 53, 50, 55 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁))‘𝑥) = ((sin‘𝑥)↑𝑁)) |
| 57 | 56 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑𝑁) = ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁))‘𝑥)) |
| 58 | 57 | mpteq2dva 5242 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) = (𝑥 ∈ (0[,]π) ↦ ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁))‘𝑥))) |
| 59 | | nfmpt1 5250 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) |
| 60 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥sin |
| 61 | | sincn 26488 |
. . . . . . . . . . . . 13
⊢ sin
∈ (ℂ–cn→ℂ) |
| 62 | 61 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → sin ∈
(ℂ–cn→ℂ)) |
| 63 | 60, 62, 26 | expcnfg 45606 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) ∈ (ℂ–cn→ℂ)) |
| 64 | 45 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (0[,]π) ⊆
ℂ) |
| 65 | 59, 63, 64 | cncfmptss 45602 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁))‘𝑥)) ∈ ((0[,]π)–cn→ℂ)) |
| 66 | 58, 65 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) ∈ ((0[,]π)–cn→ℂ)) |
| 67 | | cniccibl 25876 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ π ∈ ℝ ∧ (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) ∈ ((0[,]π)–cn→ℂ)) → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) ∈
𝐿1) |
| 68 | 51, 52, 66, 67 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) ∈
𝐿1) |
| 69 | 37, 39, 50, 68 | iblss 25840 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((sin‘𝑥)↑𝑁)) ∈
𝐿1) |
| 70 | 35, 69 | itgcl 25819 |
. . . . . 6
⊢ (𝜑 →
∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥 ∈ ℂ) |
| 71 | 29, 70 | eqeltrd 2841 |
. . . . 5
⊢ (𝜑 → (𝐼‘𝑁) ∈ ℂ) |
| 72 | 11, 71 | adddirp1d 11287 |
. . . 4
⊢ (𝜑 → (((𝑁 − 1) + 1) · (𝐼‘𝑁)) = (((𝑁 − 1) · (𝐼‘𝑁)) + (𝐼‘𝑁))) |
| 73 | | eluz2b2 12963 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁)) |
| 74 | 1, 73 | sylib 218 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 1 < 𝑁)) |
| 75 | 74 | simpld 494 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 76 | | expm1t 14131 |
. . . . . . . . . 10
⊢
(((sin‘𝑥)
∈ ℂ ∧ 𝑁
∈ ℕ) → ((sin‘𝑥)↑𝑁) = (((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥))) |
| 77 | 32, 75, 76 | syl2anr 597 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑𝑁) = (((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥))) |
| 78 | 77 | itgeq2dv 25817 |
. . . . . . . 8
⊢ (𝜑 →
∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥 = ∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥)) d𝑥) |
| 79 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ ↦
((sin‘𝑥)↑(𝑁 − 1))) = (𝑥 ∈ ℂ ↦
((sin‘𝑥)↑(𝑁 − 1))) |
| 80 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ ↦
-(cos‘𝑥)) = (𝑥 ∈ ℂ ↦
-(cos‘𝑥)) |
| 81 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ ↦ (((𝑁 − 1) ·
((sin‘𝑥)↑((𝑁 − 1) − 1)))
· (cos‘𝑥))) =
(𝑥 ∈ ℂ ↦
(((𝑁 − 1) ·
((sin‘𝑥)↑((𝑁 − 1) − 1)))
· (cos‘𝑥))) |
| 82 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ ↦
(((sin‘𝑥)↑(𝑁 − 1)) ·
(sin‘𝑥))) = (𝑥 ∈ ℂ ↦
(((sin‘𝑥)↑(𝑁 − 1)) ·
(sin‘𝑥))) |
| 83 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ ↦
((((𝑁 − 1) ·
((sin‘𝑥)↑((𝑁 − 1) − 1)))
· (cos‘𝑥))
· -(cos‘𝑥))) =
(𝑥 ∈ ℂ ↦
((((𝑁 − 1) ·
((sin‘𝑥)↑((𝑁 − 1) − 1)))
· (cos‘𝑥))
· -(cos‘𝑥))) |
| 84 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ ↦
(((cos‘𝑥)↑2)
· ((sin‘𝑥)↑((𝑁 − 1) − 1)))) = (𝑥 ∈ ℂ ↦
(((cos‘𝑥)↑2)
· ((sin‘𝑥)↑((𝑁 − 1) − 1)))) |
| 85 | 79, 80, 81, 82, 83, 84, 10 | itgsinexplem1 45969 |
. . . . . . . . 9
⊢ (𝜑 →
∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥)) d𝑥 = ((𝑁 − 1) ·
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) d𝑥)) |
| 86 | 4, 5, 5 | subsub4d 11651 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑁 − 1) − 1) = (𝑁 − (1 + 1))) |
| 87 | | 1p1e2 12391 |
. . . . . . . . . . . . . . . . 17
⊢ (1 + 1) =
2 |
| 88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 + 1) =
2) |
| 89 | 88 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 − (1 + 1)) = (𝑁 − 2)) |
| 90 | 86, 89 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 − 1) − 1) = (𝑁 − 2)) |
| 91 | 90 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((𝑁 − 1) − 1) = (𝑁 − 2)) |
| 92 | 91 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑((𝑁 − 1) − 1)) = ((sin‘𝑥)↑(𝑁 − 2))) |
| 93 | 92 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑((𝑁 − 1) − 1))) =
(((cos‘𝑥)↑2)
· ((sin‘𝑥)↑(𝑁 − 2)))) |
| 94 | 93 | itgeq2dv 25817 |
. . . . . . . . . 10
⊢ (𝜑 →
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) d𝑥 = ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 2))) d𝑥) |
| 95 | 94 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 − 1) ·
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) d𝑥) = ((𝑁 − 1) ·
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥)) |
| 96 | | sincossq 16212 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ →
(((sin‘𝑥)↑2) +
((cos‘𝑥)↑2)) =
1) |
| 97 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ → 1 ∈
ℂ) |
| 98 | | sincl 16162 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ →
(sin‘𝑥) ∈
ℂ) |
| 99 | 98 | sqcld 14184 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ →
((sin‘𝑥)↑2)
∈ ℂ) |
| 100 | | coscl 16163 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ →
(cos‘𝑥) ∈
ℂ) |
| 101 | 100 | sqcld 14184 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ →
((cos‘𝑥)↑2)
∈ ℂ) |
| 102 | 97, 99, 101 | subaddd 11638 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → ((1
− ((sin‘𝑥)↑2)) = ((cos‘𝑥)↑2) ↔ (((sin‘𝑥)↑2) + ((cos‘𝑥)↑2)) =
1)) |
| 103 | 96, 102 | mpbird 257 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (1
− ((sin‘𝑥)↑2)) = ((cos‘𝑥)↑2)) |
| 104 | 103 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ →
((cos‘𝑥)↑2) = (1
− ((sin‘𝑥)↑2))) |
| 105 | 31, 104 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (0(,)π) →
((cos‘𝑥)↑2) = (1
− ((sin‘𝑥)↑2))) |
| 106 | 105 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (0(,)π) →
(((cos‘𝑥)↑2)
· ((sin‘𝑥)↑(𝑁 − 2))) = ((1 −
((sin‘𝑥)↑2))
· ((sin‘𝑥)↑(𝑁 − 2)))) |
| 107 | 106 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 2))) = ((1 −
((sin‘𝑥)↑2))
· ((sin‘𝑥)↑(𝑁 − 2)))) |
| 108 | 107 | itgeq2dv 25817 |
. . . . . . . . . . 11
⊢ (𝜑 →
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥 = ∫(0(,)π)((1 −
((sin‘𝑥)↑2))
· ((sin‘𝑥)↑(𝑁 − 2))) d𝑥) |
| 109 | | 1cnd 11256 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → 1 ∈
ℂ) |
| 110 | 32 | sqcld 14184 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0(,)π) →
((sin‘𝑥)↑2)
∈ ℂ) |
| 111 | 110 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑2) ∈
ℂ) |
| 112 | 90 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 − 2) = ((𝑁 − 1) − 1)) |
| 113 | | nnm1nn0 12567 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 − 1) ∈ ℕ
→ ((𝑁 − 1)
− 1) ∈ ℕ0) |
| 114 | 10, 113 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑁 − 1) − 1) ∈
ℕ0) |
| 115 | 112, 114 | eqeltrd 2841 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 − 2) ∈
ℕ0) |
| 116 | 115 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (𝑁 − 2) ∈
ℕ0) |
| 117 | 33, 116 | expcld 14186 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑(𝑁 − 2)) ∈
ℂ) |
| 118 | 109, 111,
117 | subdird 11720 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((1 −
((sin‘𝑥)↑2))
· ((sin‘𝑥)↑(𝑁 − 2))) = ((1 ·
((sin‘𝑥)↑(𝑁 − 2))) −
(((sin‘𝑥)↑2)
· ((sin‘𝑥)↑(𝑁 − 2))))) |
| 119 | 117 | mullidd 11279 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (1 ·
((sin‘𝑥)↑(𝑁 − 2))) =
((sin‘𝑥)↑(𝑁 − 2))) |
| 120 | 23 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → 2 ∈
ℕ0) |
| 121 | 33, 116, 120 | expaddd 14188 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑(2 + (𝑁 − 2))) = (((sin‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 2)))) |
| 122 | 17, 4 | pncan3d 11623 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 + (𝑁 − 2)) = 𝑁) |
| 123 | 122 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((sin‘𝑥)↑(2 + (𝑁 − 2))) = ((sin‘𝑥)↑𝑁)) |
| 124 | 123 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑(2 + (𝑁 − 2))) = ((sin‘𝑥)↑𝑁)) |
| 125 | 121, 124 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (((sin‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 2))) =
((sin‘𝑥)↑𝑁)) |
| 126 | 119, 125 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((1 ·
((sin‘𝑥)↑(𝑁 − 2))) −
(((sin‘𝑥)↑2)
· ((sin‘𝑥)↑(𝑁 − 2)))) = (((sin‘𝑥)↑(𝑁 − 2)) − ((sin‘𝑥)↑𝑁))) |
| 127 | 118, 126 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((1 −
((sin‘𝑥)↑2))
· ((sin‘𝑥)↑(𝑁 − 2))) = (((sin‘𝑥)↑(𝑁 − 2)) − ((sin‘𝑥)↑𝑁))) |
| 128 | 127 | itgeq2dv 25817 |
. . . . . . . . . . 11
⊢ (𝜑 → ∫(0(,)π)((1 −
((sin‘𝑥)↑2))
· ((sin‘𝑥)↑(𝑁 − 2))) d𝑥 = ∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 2)) − ((sin‘𝑥)↑𝑁)) d𝑥) |
| 129 | 115 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (𝑁 − 2) ∈
ℕ0) |
| 130 | 48, 129 | expcld 14186 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑(𝑁 − 2)) ∈
ℂ) |
| 131 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ ↦
((sin‘𝑥)↑(𝑁 − 2))) = (𝑥 ∈ ℂ ↦
((sin‘𝑥)↑(𝑁 − 2))) |
| 132 | 131 | fvmpt2 7027 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℂ ∧
((sin‘𝑥)↑(𝑁 − 2)) ∈ ℂ)
→ ((𝑥 ∈ ℂ
↦ ((sin‘𝑥)↑(𝑁 − 2)))‘𝑥) = ((sin‘𝑥)↑(𝑁 − 2))) |
| 133 | 53, 130, 132 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑(𝑁 − 2)))‘𝑥) = ((sin‘𝑥)↑(𝑁 − 2))) |
| 134 | 133 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑(𝑁 − 2)) = ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2)))‘𝑥)) |
| 135 | 134 | mpteq2dva 5242 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) = (𝑥 ∈ (0[,]π) ↦ ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑(𝑁 − 2)))‘𝑥))) |
| 136 | | nfmpt1 5250 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2))) |
| 137 | 60, 62, 115 | expcnfg 45606 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈ (ℂ–cn→ℂ)) |
| 138 | 136, 137,
64 | cncfmptss 45602 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑(𝑁 − 2)))‘𝑥)) ∈
((0[,]π)–cn→ℂ)) |
| 139 | 135, 138 | eqeltrd 2841 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈ ((0[,]π)–cn→ℂ)) |
| 140 | | cniccibl 25876 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ π ∈ ℝ ∧ (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈ ((0[,]π)–cn→ℂ)) → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈
𝐿1) |
| 141 | 51, 52, 139, 140 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈
𝐿1) |
| 142 | 37, 39, 130, 141 | iblss 25840 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈
𝐿1) |
| 143 | 117, 142,
35, 69 | itgsub 25861 |
. . . . . . . . . . 11
⊢ (𝜑 →
∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 2)) − ((sin‘𝑥)↑𝑁)) d𝑥 = (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥)) |
| 144 | 108, 128,
143 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ (𝜑 →
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥 = (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥)) |
| 145 | 144 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 − 1) ·
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥) = ((𝑁 − 1) ·
(∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥))) |
| 146 | 85, 95, 145 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (𝜑 →
∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥)) d𝑥 = ((𝑁 − 1) ·
(∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥))) |
| 147 | 29, 78, 146 | 3eqtrd 2781 |
. . . . . . 7
⊢ (𝜑 → (𝐼‘𝑁) = ((𝑁 − 1) ·
(∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥))) |
| 148 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑁 − 2) → ((sin‘𝑥)↑𝑛) = ((sin‘𝑥)↑(𝑁 − 2))) |
| 149 | 148 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑛 = (𝑁 − 2) ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑𝑛) = ((sin‘𝑥)↑(𝑁 − 2))) |
| 150 | 149 | itgeq2dv 25817 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑁 − 2) →
∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥 = ∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥) |
| 151 | | itgex 25805 |
. . . . . . . . . . 11
⊢
∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 ∈ V |
| 152 | 151 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 →
∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 ∈ V) |
| 153 | 12, 150, 115, 152 | fvmptd3 7039 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼‘(𝑁 − 2)) =
∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥) |
| 154 | 153, 29 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝜑 → ((𝐼‘(𝑁 − 2)) − (𝐼‘𝑁)) = (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥)) |
| 155 | 154 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 − 1) · ((𝐼‘(𝑁 − 2)) − (𝐼‘𝑁))) = ((𝑁 − 1) ·
(∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥))) |
| 156 | 117, 142 | itgcl 25819 |
. . . . . . . . 9
⊢ (𝜑 →
∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 ∈ ℂ) |
| 157 | 153, 156 | eqeltrd 2841 |
. . . . . . . 8
⊢ (𝜑 → (𝐼‘(𝑁 − 2)) ∈
ℂ) |
| 158 | 11, 157, 71 | subdid 11719 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 − 1) · ((𝐼‘(𝑁 − 2)) − (𝐼‘𝑁))) = (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) − ((𝑁 − 1) · (𝐼‘𝑁)))) |
| 159 | 147, 155,
158 | 3eqtr2d 2783 |
. . . . . 6
⊢ (𝜑 → (𝐼‘𝑁) = (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) − ((𝑁 − 1) · (𝐼‘𝑁)))) |
| 160 | 159 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 → (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) − ((𝑁 − 1) · (𝐼‘𝑁))) = (𝐼‘𝑁)) |
| 161 | 11, 157 | mulcld 11281 |
. . . . . 6
⊢ (𝜑 → ((𝑁 − 1) · (𝐼‘(𝑁 − 2))) ∈
ℂ) |
| 162 | 11, 71 | mulcld 11281 |
. . . . . 6
⊢ (𝜑 → ((𝑁 − 1) · (𝐼‘𝑁)) ∈ ℂ) |
| 163 | 161, 162,
71 | subaddd 11638 |
. . . . 5
⊢ (𝜑 → ((((𝑁 − 1) · (𝐼‘(𝑁 − 2))) − ((𝑁 − 1) · (𝐼‘𝑁))) = (𝐼‘𝑁) ↔ (((𝑁 − 1) · (𝐼‘𝑁)) + (𝐼‘𝑁)) = ((𝑁 − 1) · (𝐼‘(𝑁 − 2))))) |
| 164 | 160, 163 | mpbid 232 |
. . . 4
⊢ (𝜑 → (((𝑁 − 1) · (𝐼‘𝑁)) + (𝐼‘𝑁)) = ((𝑁 − 1) · (𝐼‘(𝑁 − 2)))) |
| 165 | 8, 72, 164 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → (𝑁 · (𝐼‘𝑁)) = ((𝑁 − 1) · (𝐼‘(𝑁 − 2)))) |
| 166 | 165 | oveq1d 7446 |
. 2
⊢ (𝜑 → ((𝑁 · (𝐼‘𝑁)) / 𝑁) = (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) / 𝑁)) |
| 167 | 75 | nnne0d 12316 |
. . 3
⊢ (𝜑 → 𝑁 ≠ 0) |
| 168 | 71, 4, 167 | divcan3d 12048 |
. 2
⊢ (𝜑 → ((𝑁 · (𝐼‘𝑁)) / 𝑁) = (𝐼‘𝑁)) |
| 169 | 11, 157, 4, 167 | div23d 12080 |
. 2
⊢ (𝜑 → (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) / 𝑁) = (((𝑁 − 1) / 𝑁) · (𝐼‘(𝑁 − 2)))) |
| 170 | 166, 168,
169 | 3eqtr3d 2785 |
1
⊢ (𝜑 → (𝐼‘𝑁) = (((𝑁 − 1) / 𝑁) · (𝐼‘(𝑁 − 2)))) |