Proof of Theorem itgsinexp
Step | Hyp | Ref
| Expression |
1 | | itgsinexp.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘2)) |
2 | | eluzelz 11573 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℤ) |
3 | | zcn 11259 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
4 | 1, 2, 3 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℂ) |
5 | | 1cnd 9935 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℂ) |
6 | 4, 5 | npcand 10275 |
. . . . . 6
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
7 | 6 | eqcomd 2616 |
. . . . 5
⊢ (𝜑 → 𝑁 = ((𝑁 − 1) + 1)) |
8 | 7 | oveq1d 6564 |
. . . 4
⊢ (𝜑 → (𝑁 · (𝐼‘𝑁)) = (((𝑁 − 1) + 1) · (𝐼‘𝑁))) |
9 | | uz2m1nn 11639 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 1) ∈ ℕ) |
10 | 1, 9 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑁 − 1) ∈ ℕ) |
11 | 10 | nncnd 10913 |
. . . . 5
⊢ (𝜑 → (𝑁 − 1) ∈ ℂ) |
12 | | itgsinexp.1 |
. . . . . . . 8
⊢ 𝐼 = (𝑛 ∈ ℕ0 ↦
∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥) |
13 | 12 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐼 = (𝑛 ∈ ℕ0 ↦
∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)) |
14 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → ((sin‘𝑥)↑𝑛) = ((sin‘𝑥)↑𝑁)) |
15 | 14 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑𝑛) = ((sin‘𝑥)↑𝑁)) |
16 | 15 | itgeq2dv 23354 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥 = ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥) |
17 | | 2cnd 10970 |
. . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℂ) |
18 | | npcan 10169 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ) → ((𝑁 −
2) + 2) = 𝑁) |
19 | 18 | eqcomd 2616 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ) → 𝑁 = ((𝑁 − 2) +
2)) |
20 | 4, 17, 19 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 = ((𝑁 − 2) + 2)) |
21 | | uznn0sub 11595 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 2) ∈
ℕ0) |
22 | 1, 21 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 − 2) ∈
ℕ0) |
23 | | 2nn0 11186 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
24 | 23 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℕ0) |
25 | 22, 24 | nn0addcld 11232 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 − 2) + 2) ∈
ℕ0) |
26 | 20, 25 | eqeltrd 2688 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
27 | | itgex 23343 |
. . . . . . . 8
⊢
∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥 ∈ V |
28 | 27 | a1i 11 |
. . . . . . 7
⊢ (𝜑 →
∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥 ∈ V) |
29 | 13, 16, 26, 28 | fvmptd 6197 |
. . . . . 6
⊢ (𝜑 → (𝐼‘𝑁) = ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥) |
30 | | ioosscn 38563 |
. . . . . . . . . . 11
⊢
(0(,)π) ⊆ ℂ |
31 | 30 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0(,)π) → 𝑥 ∈
ℂ) |
32 | 31 | sincld 14699 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0(,)π) →
(sin‘𝑥) ∈
ℂ) |
33 | 32 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (sin‘𝑥) ∈
ℂ) |
34 | 26 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → 𝑁 ∈
ℕ0) |
35 | 33, 34 | expcld 12870 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑𝑁) ∈ ℂ) |
36 | | ioossicc 12130 |
. . . . . . . . 9
⊢
(0(,)π) ⊆ (0[,]π) |
37 | 36 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (0(,)π) ⊆
(0[,]π)) |
38 | | ioombl 23140 |
. . . . . . . . 9
⊢
(0(,)π) ∈ dom vol |
39 | 38 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (0(,)π) ∈ dom
vol) |
40 | | 0re 9919 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
41 | | pire 24014 |
. . . . . . . . . . . . . 14
⊢ π
∈ ℝ |
42 | | iccssre 12126 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ π ∈ ℝ) → (0[,]π) ⊆
ℝ) |
43 | 40, 41, 42 | mp2an 704 |
. . . . . . . . . . . . 13
⊢
(0[,]π) ⊆ ℝ |
44 | | ax-resscn 9872 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℂ |
45 | 43, 44 | sstri 3577 |
. . . . . . . . . . . 12
⊢
(0[,]π) ⊆ ℂ |
46 | 45 | sseli 3564 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0[,]π) → 𝑥 ∈
ℂ) |
47 | 46 | sincld 14699 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0[,]π) →
(sin‘𝑥) ∈
ℂ) |
48 | 47 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (sin‘𝑥) ∈
ℂ) |
49 | 26 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → 𝑁 ∈
ℕ0) |
50 | 48, 49 | expcld 12870 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑𝑁) ∈ ℂ) |
51 | 40 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℝ) |
52 | 41 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → π ∈
ℝ) |
53 | 46 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → 𝑥 ∈ ℂ) |
54 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁)) = (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) |
55 | 54 | fvmpt2 6200 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧
((sin‘𝑥)↑𝑁) ∈ ℂ) → ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁))‘𝑥) = ((sin‘𝑥)↑𝑁)) |
56 | 53, 50, 55 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁))‘𝑥) = ((sin‘𝑥)↑𝑁)) |
57 | 56 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑𝑁) = ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁))‘𝑥)) |
58 | 57 | mpteq2dva 4672 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) = (𝑥 ∈ (0[,]π) ↦ ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁))‘𝑥))) |
59 | | nfmpt1 4675 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) |
60 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥sin |
61 | | sincn 24002 |
. . . . . . . . . . . . 13
⊢ sin
∈ (ℂ–cn→ℂ) |
62 | 61 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → sin ∈
(ℂ–cn→ℂ)) |
63 | 60, 62, 26 | expcnfg 38658 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) ∈ (ℂ–cn→ℂ)) |
64 | 45 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (0[,]π) ⊆
ℂ) |
65 | 59, 63, 64 | cncfmptss 38654 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁))‘𝑥)) ∈ ((0[,]π)–cn→ℂ)) |
66 | 58, 65 | eqeltrd 2688 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) ∈ ((0[,]π)–cn→ℂ)) |
67 | | cniccibl 23413 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ π ∈ ℝ ∧ (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) ∈ ((0[,]π)–cn→ℂ)) → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) ∈
𝐿1) |
68 | 51, 52, 66, 67 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) ∈
𝐿1) |
69 | 37, 39, 50, 68 | iblss 23377 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((sin‘𝑥)↑𝑁)) ∈
𝐿1) |
70 | 35, 69 | itgcl 23356 |
. . . . . 6
⊢ (𝜑 →
∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥 ∈ ℂ) |
71 | 29, 70 | eqeltrd 2688 |
. . . . 5
⊢ (𝜑 → (𝐼‘𝑁) ∈ ℂ) |
72 | 11, 71 | adddirp1d 9945 |
. . . 4
⊢ (𝜑 → (((𝑁 − 1) + 1) · (𝐼‘𝑁)) = (((𝑁 − 1) · (𝐼‘𝑁)) + (𝐼‘𝑁))) |
73 | | eluz2b2 11637 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁)) |
74 | 1, 73 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 1 < 𝑁)) |
75 | 74 | simpld 474 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℕ) |
76 | | expm1t 12750 |
. . . . . . . . . 10
⊢
(((sin‘𝑥)
∈ ℂ ∧ 𝑁
∈ ℕ) → ((sin‘𝑥)↑𝑁) = (((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥))) |
77 | 32, 75, 76 | syl2anr 494 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑𝑁) = (((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥))) |
78 | 77 | itgeq2dv 23354 |
. . . . . . . 8
⊢ (𝜑 →
∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥 = ∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥)) d𝑥) |
79 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ ↦
((sin‘𝑥)↑(𝑁 − 1))) = (𝑥 ∈ ℂ ↦
((sin‘𝑥)↑(𝑁 − 1))) |
80 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ ↦
-(cos‘𝑥)) = (𝑥 ∈ ℂ ↦
-(cos‘𝑥)) |
81 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ ↦ (((𝑁 − 1) ·
((sin‘𝑥)↑((𝑁 − 1) − 1)))
· (cos‘𝑥))) =
(𝑥 ∈ ℂ ↦
(((𝑁 − 1) ·
((sin‘𝑥)↑((𝑁 − 1) − 1)))
· (cos‘𝑥))) |
82 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ ↦
(((sin‘𝑥)↑(𝑁 − 1)) ·
(sin‘𝑥))) = (𝑥 ∈ ℂ ↦
(((sin‘𝑥)↑(𝑁 − 1)) ·
(sin‘𝑥))) |
83 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ ↦
((((𝑁 − 1) ·
((sin‘𝑥)↑((𝑁 − 1) − 1)))
· (cos‘𝑥))
· -(cos‘𝑥))) =
(𝑥 ∈ ℂ ↦
((((𝑁 − 1) ·
((sin‘𝑥)↑((𝑁 − 1) − 1)))
· (cos‘𝑥))
· -(cos‘𝑥))) |
84 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ ↦
(((cos‘𝑥)↑2)
· ((sin‘𝑥)↑((𝑁 − 1) − 1)))) = (𝑥 ∈ ℂ ↦
(((cos‘𝑥)↑2)
· ((sin‘𝑥)↑((𝑁 − 1) − 1)))) |
85 | 79, 80, 81, 82, 83, 84, 10 | itgsinexplem1 38845 |
. . . . . . . . 9
⊢ (𝜑 →
∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥)) d𝑥 = ((𝑁 − 1) ·
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) d𝑥)) |
86 | 4, 5, 5 | subsub4d 10302 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑁 − 1) − 1) = (𝑁 − (1 + 1))) |
87 | | 1p1e2 11011 |
. . . . . . . . . . . . . . . . 17
⊢ (1 + 1) =
2 |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 + 1) =
2) |
89 | 88 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 − (1 + 1)) = (𝑁 − 2)) |
90 | 86, 89 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 − 1) − 1) = (𝑁 − 2)) |
91 | 90 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((𝑁 − 1) − 1) = (𝑁 − 2)) |
92 | 91 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑((𝑁 − 1) − 1)) = ((sin‘𝑥)↑(𝑁 − 2))) |
93 | 92 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑((𝑁 − 1) − 1))) =
(((cos‘𝑥)↑2)
· ((sin‘𝑥)↑(𝑁 − 2)))) |
94 | 93 | itgeq2dv 23354 |
. . . . . . . . . 10
⊢ (𝜑 →
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) d𝑥 = ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 2))) d𝑥) |
95 | 94 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 − 1) ·
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) d𝑥) = ((𝑁 − 1) ·
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥)) |
96 | | sincossq 14745 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ →
(((sin‘𝑥)↑2) +
((cos‘𝑥)↑2)) =
1) |
97 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ → 1 ∈
ℂ) |
98 | | sincl 14695 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ →
(sin‘𝑥) ∈
ℂ) |
99 | 98 | sqcld 12868 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ →
((sin‘𝑥)↑2)
∈ ℂ) |
100 | | coscl 14696 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ →
(cos‘𝑥) ∈
ℂ) |
101 | 100 | sqcld 12868 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ →
((cos‘𝑥)↑2)
∈ ℂ) |
102 | 97, 99, 101 | subaddd 10289 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → ((1
− ((sin‘𝑥)↑2)) = ((cos‘𝑥)↑2) ↔ (((sin‘𝑥)↑2) + ((cos‘𝑥)↑2)) =
1)) |
103 | 96, 102 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (1
− ((sin‘𝑥)↑2)) = ((cos‘𝑥)↑2)) |
104 | 103 | eqcomd 2616 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ →
((cos‘𝑥)↑2) = (1
− ((sin‘𝑥)↑2))) |
105 | 31, 104 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (0(,)π) →
((cos‘𝑥)↑2) = (1
− ((sin‘𝑥)↑2))) |
106 | 105 | oveq1d 6564 |
. . . . . . . . . . . . 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 23354 |
. . . . . . . . . . 11
⊢ (𝜑 →
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥 = ∫(0(,)π)((1 −
((sin‘𝑥)↑2))
· ((sin‘𝑥)↑(𝑁 − 2))) d𝑥) |
109 | | 1cnd 9935 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → 1 ∈
ℂ) |
110 | 32 | sqcld 12868 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0(,)π) →
((sin‘𝑥)↑2)
∈ ℂ) |
111 | 110 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑2) ∈
ℂ) |
112 | 90 | eqcomd 2616 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 − 2) = ((𝑁 − 1) − 1)) |
113 | | nnm1nn0 11211 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 − 1) ∈ ℕ
→ ((𝑁 − 1)
− 1) ∈ ℕ0) |
114 | 10, 113 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑁 − 1) − 1) ∈
ℕ0) |
115 | 112, 114 | eqeltrd 2688 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 − 2) ∈
ℕ0) |
116 | 115 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (𝑁 − 2) ∈
ℕ0) |
117 | 33, 116 | expcld 12870 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑(𝑁 − 2)) ∈
ℂ) |
118 | 109, 111,
117 | subdird 10366 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((1 −
((sin‘𝑥)↑2))
· ((sin‘𝑥)↑(𝑁 − 2))) = ((1 ·
((sin‘𝑥)↑(𝑁 − 2))) −
(((sin‘𝑥)↑2)
· ((sin‘𝑥)↑(𝑁 − 2))))) |
119 | 117 | mulid2d 9937 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (1 ·
((sin‘𝑥)↑(𝑁 − 2))) =
((sin‘𝑥)↑(𝑁 − 2))) |
120 | 23 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → 2 ∈
ℕ0) |
121 | 33, 116, 120 | expaddd 12872 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑(2 + (𝑁 − 2))) = (((sin‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 2)))) |
122 | 17, 4 | pncan3d 10274 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 + (𝑁 − 2)) = 𝑁) |
123 | 122 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((sin‘𝑥)↑(2 + (𝑁 − 2))) = ((sin‘𝑥)↑𝑁)) |
124 | 123 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑(2 + (𝑁 − 2))) = ((sin‘𝑥)↑𝑁)) |
125 | 121, 124 | eqtr3d 2646 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (((sin‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 2))) =
((sin‘𝑥)↑𝑁)) |
126 | 119, 125 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((1 ·
((sin‘𝑥)↑(𝑁 − 2))) −
(((sin‘𝑥)↑2)
· ((sin‘𝑥)↑(𝑁 − 2)))) = (((sin‘𝑥)↑(𝑁 − 2)) − ((sin‘𝑥)↑𝑁))) |
127 | 118, 126 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((1 −
((sin‘𝑥)↑2))
· ((sin‘𝑥)↑(𝑁 − 2))) = (((sin‘𝑥)↑(𝑁 − 2)) − ((sin‘𝑥)↑𝑁))) |
128 | 127 | itgeq2dv 23354 |
. . . . . . . . . . 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 12870 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑(𝑁 − 2)) ∈
ℂ) |
131 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ ↦
((sin‘𝑥)↑(𝑁 − 2))) = (𝑥 ∈ ℂ ↦
((sin‘𝑥)↑(𝑁 − 2))) |
132 | 131 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℂ ∧
((sin‘𝑥)↑(𝑁 − 2)) ∈ ℂ)
→ ((𝑥 ∈ ℂ
↦ ((sin‘𝑥)↑(𝑁 − 2)))‘𝑥) = ((sin‘𝑥)↑(𝑁 − 2))) |
133 | 53, 130, 132 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑(𝑁 − 2)))‘𝑥) = ((sin‘𝑥)↑(𝑁 − 2))) |
134 | 133 | eqcomd 2616 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑(𝑁 − 2)) = ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2)))‘𝑥)) |
135 | 134 | mpteq2dva 4672 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) = (𝑥 ∈ (0[,]π) ↦ ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑(𝑁 − 2)))‘𝑥))) |
136 | | nfmpt1 4675 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2))) |
137 | 60, 62, 115 | expcnfg 38658 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈ (ℂ–cn→ℂ)) |
138 | 136, 137,
64 | cncfmptss 38654 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑(𝑁 − 2)))‘𝑥)) ∈
((0[,]π)–cn→ℂ)) |
139 | 135, 138 | eqeltrd 2688 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈ ((0[,]π)–cn→ℂ)) |
140 | | cniccibl 23413 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ π ∈ ℝ ∧ (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈ ((0[,]π)–cn→ℂ)) → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈
𝐿1) |
141 | 51, 52, 139, 140 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈
𝐿1) |
142 | 37, 39, 130, 141 | iblss 23377 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈
𝐿1) |
143 | 117, 142,
35, 69 | itgsub 23398 |
. . . . . . . . . . 11
⊢ (𝜑 →
∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 2)) − ((sin‘𝑥)↑𝑁)) d𝑥 = (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥)) |
144 | 108, 128,
143 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ (𝜑 →
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥 = (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥)) |
145 | 144 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 − 1) ·
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥) = ((𝑁 − 1) ·
(∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥))) |
146 | 85, 95, 145 | 3eqtrd 2648 |
. . . . . . . 8
⊢ (𝜑 →
∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥)) d𝑥 = ((𝑁 − 1) ·
(∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥))) |
147 | 29, 78, 146 | 3eqtrd 2648 |
. . . . . . 7
⊢ (𝜑 → (𝐼‘𝑁) = ((𝑁 − 1) ·
(∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥))) |
148 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑁 − 2) → ((sin‘𝑥)↑𝑛) = ((sin‘𝑥)↑(𝑁 − 2))) |
149 | 148 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑛 = (𝑁 − 2) ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑𝑛) = ((sin‘𝑥)↑(𝑁 − 2))) |
150 | 149 | itgeq2dv 23354 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑁 − 2) →
∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥 = ∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥) |
151 | 150 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 = (𝑁 − 2)) →
∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥 = ∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥) |
152 | | itgex 23343 |
. . . . . . . . . . 11
⊢
∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 ∈ V |
153 | 152 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 →
∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 ∈ V) |
154 | 13, 151, 115, 153 | fvmptd 6197 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼‘(𝑁 − 2)) =
∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥) |
155 | 154, 29 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝜑 → ((𝐼‘(𝑁 − 2)) − (𝐼‘𝑁)) = (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥)) |
156 | 155 | oveq2d 6565 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 − 1) · ((𝐼‘(𝑁 − 2)) − (𝐼‘𝑁))) = ((𝑁 − 1) ·
(∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥))) |
157 | 117, 142 | itgcl 23356 |
. . . . . . . . 9
⊢ (𝜑 →
∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 ∈ ℂ) |
158 | 154, 157 | eqeltrd 2688 |
. . . . . . . 8
⊢ (𝜑 → (𝐼‘(𝑁 − 2)) ∈
ℂ) |
159 | 11, 158, 71 | subdid 10365 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 − 1) · ((𝐼‘(𝑁 − 2)) − (𝐼‘𝑁))) = (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) − ((𝑁 − 1) · (𝐼‘𝑁)))) |
160 | 147, 156,
159 | 3eqtr2d 2650 |
. . . . . 6
⊢ (𝜑 → (𝐼‘𝑁) = (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) − ((𝑁 − 1) · (𝐼‘𝑁)))) |
161 | 160 | eqcomd 2616 |
. . . . 5
⊢ (𝜑 → (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) − ((𝑁 − 1) · (𝐼‘𝑁))) = (𝐼‘𝑁)) |
162 | 11, 158 | mulcld 9939 |
. . . . . 6
⊢ (𝜑 → ((𝑁 − 1) · (𝐼‘(𝑁 − 2))) ∈
ℂ) |
163 | 11, 71 | mulcld 9939 |
. . . . . 6
⊢ (𝜑 → ((𝑁 − 1) · (𝐼‘𝑁)) ∈ ℂ) |
164 | 162, 163,
71 | subaddd 10289 |
. . . . 5
⊢ (𝜑 → ((((𝑁 − 1) · (𝐼‘(𝑁 − 2))) − ((𝑁 − 1) · (𝐼‘𝑁))) = (𝐼‘𝑁) ↔ (((𝑁 − 1) · (𝐼‘𝑁)) + (𝐼‘𝑁)) = ((𝑁 − 1) · (𝐼‘(𝑁 − 2))))) |
165 | 161, 164 | mpbid 221 |
. . . 4
⊢ (𝜑 → (((𝑁 − 1) · (𝐼‘𝑁)) + (𝐼‘𝑁)) = ((𝑁 − 1) · (𝐼‘(𝑁 − 2)))) |
166 | 8, 72, 165 | 3eqtrd 2648 |
. . 3
⊢ (𝜑 → (𝑁 · (𝐼‘𝑁)) = ((𝑁 − 1) · (𝐼‘(𝑁 − 2)))) |
167 | 166 | oveq1d 6564 |
. 2
⊢ (𝜑 → ((𝑁 · (𝐼‘𝑁)) / 𝑁) = (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) / 𝑁)) |
168 | 75 | nnne0d 10942 |
. . 3
⊢ (𝜑 → 𝑁 ≠ 0) |
169 | 71, 4, 168 | divcan3d 10685 |
. 2
⊢ (𝜑 → ((𝑁 · (𝐼‘𝑁)) / 𝑁) = (𝐼‘𝑁)) |
170 | 11, 158, 4, 168 | div23d 10717 |
. 2
⊢ (𝜑 → (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) / 𝑁) = (((𝑁 − 1) / 𝑁) · (𝐼‘(𝑁 − 2)))) |
171 | 167, 169,
170 | 3eqtr3d 2652 |
1
⊢ (𝜑 → (𝐼‘𝑁) = (((𝑁 − 1) / 𝑁) · (𝐼‘(𝑁 − 2)))) |