Proof of Theorem itgsinexplem1
Step | Hyp | Ref
| Expression |
1 | | 0m0e0 12093 |
. . . . 5
⊢ (0
− 0) = 0 |
2 | 1 | oveq1i 7285 |
. . . 4
⊢ ((0
− 0) − ∫(0(,)π)(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥) = (0 − ∫(0(,)π)(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥) |
3 | | 0re 10977 |
. . . . . 6
⊢ 0 ∈
ℝ |
4 | 3 | a1i 11 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℝ) |
5 | | pire 25615 |
. . . . . 6
⊢ π
∈ ℝ |
6 | 5 | a1i 11 |
. . . . 5
⊢ (𝜑 → π ∈
ℝ) |
7 | | pipos 25617 |
. . . . . . 7
⊢ 0 <
π |
8 | 3, 5, 7 | ltleii 11098 |
. . . . . 6
⊢ 0 ≤
π |
9 | 8 | a1i 11 |
. . . . 5
⊢ (𝜑 → 0 ≤
π) |
10 | 3, 5 | pm3.2i 471 |
. . . . . . . . . . . . 13
⊢ (0 ∈
ℝ ∧ π ∈ ℝ) |
11 | | iccssre 13161 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ π ∈ ℝ) → (0[,]π) ⊆
ℝ) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(0[,]π) ⊆ ℝ |
13 | | ax-resscn 10928 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ |
14 | 12, 13 | sstri 3930 |
. . . . . . . . . . 11
⊢
(0[,]π) ⊆ ℂ |
15 | 14 | sseli 3917 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0[,]π) → 𝑥 ∈
ℂ) |
16 | 15 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → 𝑥 ∈ ℂ) |
17 | 15 | sincld 15839 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0[,]π) →
(sin‘𝑥) ∈
ℂ) |
18 | 17 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (sin‘𝑥) ∈
ℂ) |
19 | | itgsinexplem1.7 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℕ) |
20 | 19 | nnnn0d 12293 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
21 | 20 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → 𝑁 ∈
ℕ0) |
22 | 18, 21 | expcld 13864 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑𝑁) ∈ ℂ) |
23 | | itgsinexplem1.1 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) |
24 | 23 | fvmpt2 6886 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
((sin‘𝑥)↑𝑁) ∈ ℂ) → (𝐹‘𝑥) = ((sin‘𝑥)↑𝑁)) |
25 | 16, 22, 24 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (𝐹‘𝑥) = ((sin‘𝑥)↑𝑁)) |
26 | 25 | eqcomd 2744 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑𝑁) = (𝐹‘𝑥)) |
27 | 26 | mpteq2dva 5174 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) = (𝑥 ∈ (0[,]π) ↦ (𝐹‘𝑥))) |
28 | | nfmpt1 5182 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) |
29 | 23, 28 | nfcxfr 2905 |
. . . . . . 7
⊢
Ⅎ𝑥𝐹 |
30 | | nfcv 2907 |
. . . . . . . . 9
⊢
Ⅎ𝑥sin |
31 | | sincn 25603 |
. . . . . . . . . 10
⊢ sin
∈ (ℂ–cn→ℂ) |
32 | 31 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → sin ∈
(ℂ–cn→ℂ)) |
33 | 30, 32, 20 | expcnfg 43132 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) ∈ (ℂ–cn→ℂ)) |
34 | 23, 33 | eqeltrid 2843 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ)) |
35 | 14 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (0[,]π) ⊆
ℂ) |
36 | 29, 34, 35 | cncfmptss 43128 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (𝐹‘𝑥)) ∈ ((0[,]π)–cn→ℂ)) |
37 | 27, 36 | eqeltrd 2839 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) ∈ ((0[,]π)–cn→ℂ)) |
38 | 15 | coscld 15840 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0[,]π) →
(cos‘𝑥) ∈
ℂ) |
39 | 38 | negcld 11319 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0[,]π) →
-(cos‘𝑥) ∈
ℂ) |
40 | | itgsinexplem1.2 |
. . . . . . . . . . 11
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ -(cos‘𝑥)) |
41 | 40 | fvmpt2 6886 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧
-(cos‘𝑥) ∈
ℂ) → (𝐺‘𝑥) = -(cos‘𝑥)) |
42 | 15, 39, 41 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0[,]π) → (𝐺‘𝑥) = -(cos‘𝑥)) |
43 | 42 | eqcomd 2744 |
. . . . . . . 8
⊢ (𝑥 ∈ (0[,]π) →
-(cos‘𝑥) = (𝐺‘𝑥)) |
44 | 43 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → -(cos‘𝑥) = (𝐺‘𝑥)) |
45 | 44 | mpteq2dva 5174 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ -(cos‘𝑥)) = (𝑥 ∈ (0[,]π) ↦ (𝐺‘𝑥))) |
46 | | nfmpt1 5182 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑥 ∈ ℂ ↦ -(cos‘𝑥)) |
47 | 40, 46 | nfcxfr 2905 |
. . . . . . 7
⊢
Ⅎ𝑥𝐺 |
48 | | coscn 25604 |
. . . . . . . . 9
⊢ cos
∈ (ℂ–cn→ℂ) |
49 | 48 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → cos ∈
(ℂ–cn→ℂ)) |
50 | 40 | negfcncf 24086 |
. . . . . . . 8
⊢ (cos
∈ (ℂ–cn→ℂ)
→ 𝐺 ∈
(ℂ–cn→ℂ)) |
51 | 49, 50 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ (ℂ–cn→ℂ)) |
52 | 47, 51, 35 | cncfmptss 43128 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (𝐺‘𝑥)) ∈ ((0[,]π)–cn→ℂ)) |
53 | 45, 52 | eqeltrd 2839 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ -(cos‘𝑥)) ∈
((0[,]π)–cn→ℂ)) |
54 | | itgsinexplem1.3 |
. . . . . 6
⊢ 𝐻 = (𝑥 ∈ ℂ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥))) |
55 | | ssidd 3944 |
. . . . . . . . . 10
⊢ (𝜑 → ℂ ⊆
ℂ) |
56 | 19 | nncnd 11989 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℂ) |
57 | 55, 56, 55 | constcncfg 43413 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝑁) ∈ (ℂ–cn→ℂ)) |
58 | | nnm1nn0 12274 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
59 | 19, 58 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
60 | 30, 32, 59 | expcnfg 43132 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 1))) ∈ (ℂ–cn→ℂ)) |
61 | 57, 60 | mulcncf 24610 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (𝑁 · ((sin‘𝑥)↑(𝑁 − 1)))) ∈ (ℂ–cn→ℂ)) |
62 | | cosf 15834 |
. . . . . . . . . . 11
⊢
cos:ℂ⟶ℂ |
63 | 62 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 →
cos:ℂ⟶ℂ) |
64 | 63 | feqmptd 6837 |
. . . . . . . . 9
⊢ (𝜑 → cos = (𝑥 ∈ ℂ ↦ (cos‘𝑥))) |
65 | 64, 48 | eqeltrrdi 2848 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (cos‘𝑥)) ∈ (ℂ–cn→ℂ)) |
66 | 61, 65 | mulcncf 24610 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥))) ∈ (ℂ–cn→ℂ)) |
67 | 54, 66 | eqeltrid 2843 |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ (ℂ–cn→ℂ)) |
68 | | ioosscn 13141 |
. . . . . . 7
⊢
(0(,)π) ⊆ ℂ |
69 | 68 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (0(,)π) ⊆
ℂ) |
70 | 56 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → 𝑁 ∈ ℂ) |
71 | 68 | sseli 3917 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0(,)π) → 𝑥 ∈
ℂ) |
72 | 71 | sincld 15839 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0(,)π) →
(sin‘𝑥) ∈
ℂ) |
73 | 72 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (sin‘𝑥) ∈
ℂ) |
74 | 59 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (𝑁 − 1) ∈
ℕ0) |
75 | 73, 74 | expcld 13864 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑(𝑁 − 1)) ∈
ℂ) |
76 | 70, 75 | mulcld 10995 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) ∈
ℂ) |
77 | 71 | coscld 15840 |
. . . . . . . 8
⊢ (𝑥 ∈ (0(,)π) →
(cos‘𝑥) ∈
ℂ) |
78 | 77 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (cos‘𝑥) ∈
ℂ) |
79 | 76, 78 | mulcld 10995 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) ∈
ℂ) |
80 | 54, 67, 69, 55, 79 | cncfmptssg 43412 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥))) ∈
((0(,)π)–cn→ℂ)) |
81 | 30, 32, 69 | cncfmptss 43128 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0(,)π) ↦ (sin‘𝑥)) ∈
((0(,)π)–cn→ℂ)) |
82 | | ioossicc 13165 |
. . . . . . 7
⊢
(0(,)π) ⊆ (0[,]π) |
83 | 82 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (0(,)π) ⊆
(0[,]π)) |
84 | | ioombl 24729 |
. . . . . . 7
⊢
(0(,)π) ∈ dom vol |
85 | 84 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (0(,)π) ∈ dom
vol) |
86 | 22, 18 | mulcld 10995 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (((sin‘𝑥)↑𝑁) · (sin‘𝑥)) ∈ ℂ) |
87 | | itgsinexplem1.4 |
. . . . . . . . . . . 12
⊢ 𝐼 = (𝑥 ∈ ℂ ↦ (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) |
88 | 87 | fvmpt2 6886 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧
(((sin‘𝑥)↑𝑁) · (sin‘𝑥)) ∈ ℂ) → (𝐼‘𝑥) = (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) |
89 | 16, 86, 88 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (𝐼‘𝑥) = (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) |
90 | 89 | eqcomd 2744 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (((sin‘𝑥)↑𝑁) · (sin‘𝑥)) = (𝐼‘𝑥)) |
91 | 90 | mpteq2dva 5174 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) = (𝑥 ∈ (0[,]π) ↦ (𝐼‘𝑥))) |
92 | | nfmpt1 5182 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑥 ∈ ℂ ↦ (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) |
93 | 87, 92 | nfcxfr 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝐼 |
94 | | sinf 15833 |
. . . . . . . . . . . . . 14
⊢
sin:ℂ⟶ℂ |
95 | 94 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
sin:ℂ⟶ℂ) |
96 | 95 | feqmptd 6837 |
. . . . . . . . . . . 12
⊢ (𝜑 → sin = (𝑥 ∈ ℂ ↦ (sin‘𝑥))) |
97 | 96, 31 | eqeltrrdi 2848 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (sin‘𝑥)) ∈ (ℂ–cn→ℂ)) |
98 | 33, 97 | mulcncf 24610 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) ∈ (ℂ–cn→ℂ)) |
99 | 87, 98 | eqeltrid 2843 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ (ℂ–cn→ℂ)) |
100 | 93, 99, 35 | cncfmptss 43128 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (𝐼‘𝑥)) ∈ ((0[,]π)–cn→ℂ)) |
101 | 91, 100 | eqeltrd 2839 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) ∈ ((0[,]π)–cn→ℂ)) |
102 | | cniccibl 25005 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ π ∈ ℝ ∧ (𝑥 ∈ (0[,]π) ↦ (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) ∈ ((0[,]π)–cn→ℂ)) → (𝑥 ∈ (0[,]π) ↦ (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) ∈
𝐿1) |
103 | 4, 6, 101, 102 | syl3anc 1370 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) ∈
𝐿1) |
104 | 83, 85, 86, 103 | iblss 24969 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0(,)π) ↦ (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) ∈
𝐿1) |
105 | 56 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → 𝑁 ∈ ℂ) |
106 | 59 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (𝑁 − 1) ∈
ℕ0) |
107 | 18, 106 | expcld 13864 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑(𝑁 − 1)) ∈
ℂ) |
108 | 105, 107 | mulcld 10995 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) ∈
ℂ) |
109 | 38 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (cos‘𝑥) ∈
ℂ) |
110 | 108, 109 | mulcld 10995 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) ∈
ℂ) |
111 | 39 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → -(cos‘𝑥) ∈
ℂ) |
112 | 110, 111 | mulcld 10995 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) ∈
ℂ) |
113 | | itgsinexplem1.5 |
. . . . . . . 8
⊢ 𝐿 = (𝑥 ∈ ℂ ↦ (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥))) |
114 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ ↦
-(cos‘𝑥)) = (𝑥 ∈ ℂ ↦
-(cos‘𝑥)) |
115 | 114 | negfcncf 24086 |
. . . . . . . . . . 11
⊢ (cos
∈ (ℂ–cn→ℂ)
→ (𝑥 ∈ ℂ
↦ -(cos‘𝑥))
∈ (ℂ–cn→ℂ)) |
116 | 49, 115 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ -(cos‘𝑥)) ∈ (ℂ–cn→ℂ)) |
117 | 66, 116 | mulcncf 24610 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥))) ∈ (ℂ–cn→ℂ)) |
118 | 113, 117 | eqeltrid 2843 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ (ℂ–cn→ℂ)) |
119 | 113, 118,
35, 55, 112 | cncfmptssg 43412 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥))) ∈
((0[,]π)–cn→ℂ)) |
120 | | cniccibl 25005 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ π ∈ ℝ ∧ (𝑥 ∈ (0[,]π) ↦ (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥))) ∈
((0[,]π)–cn→ℂ)) →
(𝑥 ∈ (0[,]π)
↦ (((𝑁 ·
((sin‘𝑥)↑(𝑁 − 1))) ·
(cos‘𝑥)) ·
-(cos‘𝑥))) ∈
𝐿1) |
121 | 4, 6, 119, 120 | syl3anc 1370 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥))) ∈
𝐿1) |
122 | 83, 85, 112, 121 | iblss 24969 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0(,)π) ↦ (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥))) ∈
𝐿1) |
123 | | reelprrecn 10963 |
. . . . . . 7
⊢ ℝ
∈ {ℝ, ℂ} |
124 | 123 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
125 | | recn 10961 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
126 | 125 | sincld 15839 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ →
(sin‘𝑥) ∈
ℂ) |
127 | 126 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (sin‘𝑥) ∈
ℂ) |
128 | 20 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑁 ∈
ℕ0) |
129 | 127, 128 | expcld 13864 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((sin‘𝑥)↑𝑁) ∈ ℂ) |
130 | 56 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑁 ∈ ℂ) |
131 | 59 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑁 − 1) ∈
ℕ0) |
132 | 127, 131 | expcld 13864 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((sin‘𝑥)↑(𝑁 − 1)) ∈
ℂ) |
133 | 130, 132 | mulcld 10995 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) ∈
ℂ) |
134 | 125 | coscld 15840 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ →
(cos‘𝑥) ∈
ℂ) |
135 | 134 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (cos‘𝑥) ∈
ℂ) |
136 | 133, 135 | mulcld 10995 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) ∈
ℂ) |
137 | | sincl 15835 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℂ →
(sin‘𝑥) ∈
ℂ) |
138 | 137 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (sin‘𝑥) ∈
ℂ) |
139 | 20 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑁 ∈
ℕ0) |
140 | 138, 139 | expcld 13864 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((sin‘𝑥)↑𝑁) ∈ ℂ) |
141 | 140, 23 | fmptd 6988 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
142 | 125 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) |
143 | | elex 3450 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) ∈ ℂ → ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) ∈ V) |
144 | 136, 143 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) ∈ V) |
145 | | rabid 3310 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {𝑥 ∈ ℂ ∣ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) ∈ V} ↔ (𝑥 ∈ ℂ ∧ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) ∈ V)) |
146 | 142, 144,
145 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ {𝑥 ∈ ℂ ∣ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) ∈ V}) |
147 | 54 | dmmpt 6143 |
. . . . . . . . . . . . 13
⊢ dom 𝐻 = {𝑥 ∈ ℂ ∣ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) ∈ V} |
148 | 146, 147 | eleqtrrdi 2850 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ dom 𝐻) |
149 | 148 | ex 413 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℝ → 𝑥 ∈ dom 𝐻)) |
150 | 149 | alrimiv 1930 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥(𝑥 ∈ ℝ → 𝑥 ∈ dom 𝐻)) |
151 | | nfcv 2907 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥ℝ |
152 | | nfmpt1 5182 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑥 ∈ ℂ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥))) |
153 | 54, 152 | nfcxfr 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝐻 |
154 | 153 | nfdm 5860 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥dom
𝐻 |
155 | 151, 154 | dfss2f 3911 |
. . . . . . . . . 10
⊢ (ℝ
⊆ dom 𝐻 ↔
∀𝑥(𝑥 ∈ ℝ → 𝑥 ∈ dom 𝐻)) |
156 | 150, 155 | sylibr 233 |
. . . . . . . . 9
⊢ (𝜑 → ℝ ⊆ dom 𝐻) |
157 | 19 | dvsinexp 43452 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁))) = (𝑥 ∈ ℂ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)))) |
158 | 23 | oveq2i 7286 |
. . . . . . . . . . 11
⊢ (ℂ
D 𝐹) = (ℂ D (𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁))) |
159 | 157, 158,
54 | 3eqtr4g 2803 |
. . . . . . . . . 10
⊢ (𝜑 → (ℂ D 𝐹) = 𝐻) |
160 | 159 | dmeqd 5814 |
. . . . . . . . 9
⊢ (𝜑 → dom (ℂ D 𝐹) = dom 𝐻) |
161 | 156, 160 | sseqtrrd 3962 |
. . . . . . . 8
⊢ (𝜑 → ℝ ⊆ dom
(ℂ D 𝐹)) |
162 | | dvres3 25077 |
. . . . . . . 8
⊢
(((ℝ ∈ {ℝ, ℂ} ∧ 𝐹:ℂ⟶ℂ) ∧ (ℂ
⊆ ℂ ∧ ℝ ⊆ dom (ℂ D 𝐹))) → (ℝ D (𝐹 ↾ ℝ)) = ((ℂ D 𝐹) ↾
ℝ)) |
163 | 124, 141,
55, 161, 162 | syl22anc 836 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝐹 ↾ ℝ)) = ((ℂ D
𝐹) ↾
ℝ)) |
164 | 23 | reseq1i 5887 |
. . . . . . . . . 10
⊢ (𝐹 ↾ ℝ) = ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁)) ↾
ℝ) |
165 | | resmpt 5945 |
. . . . . . . . . . 11
⊢ (ℝ
⊆ ℂ → ((𝑥
∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) ↾ ℝ) = (𝑥 ∈ ℝ ↦ ((sin‘𝑥)↑𝑁))) |
166 | 13, 165 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁)) ↾ ℝ) = (𝑥 ∈ ℝ ↦
((sin‘𝑥)↑𝑁)) |
167 | 164, 166 | eqtri 2766 |
. . . . . . . . 9
⊢ (𝐹 ↾ ℝ) = (𝑥 ∈ ℝ ↦
((sin‘𝑥)↑𝑁)) |
168 | 167 | oveq2i 7286 |
. . . . . . . 8
⊢ (ℝ
D (𝐹 ↾ ℝ)) =
(ℝ D (𝑥 ∈
ℝ ↦ ((sin‘𝑥)↑𝑁))) |
169 | 168 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝐹 ↾ ℝ)) = (ℝ D
(𝑥 ∈ ℝ ↦
((sin‘𝑥)↑𝑁)))) |
170 | 159 | reseq1d 5890 |
. . . . . . . 8
⊢ (𝜑 → ((ℂ D 𝐹) ↾ ℝ) = (𝐻 ↾
ℝ)) |
171 | 54 | reseq1i 5887 |
. . . . . . . . 9
⊢ (𝐻 ↾ ℝ) = ((𝑥 ∈ ℂ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥))) ↾
ℝ) |
172 | | resmpt 5945 |
. . . . . . . . . 10
⊢ (ℝ
⊆ ℂ → ((𝑥
∈ ℂ ↦ ((𝑁
· ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)))) |
173 | 13, 172 | ax-mp 5 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥))) |
174 | 171, 173 | eqtri 2766 |
. . . . . . . 8
⊢ (𝐻 ↾ ℝ) = (𝑥 ∈ ℝ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥))) |
175 | 170, 174 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝜑 → ((ℂ D 𝐹) ↾ ℝ) = (𝑥 ∈ ℝ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)))) |
176 | 163, 169,
175 | 3eqtr3d 2786 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦
((sin‘𝑥)↑𝑁))) = (𝑥 ∈ ℝ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)))) |
177 | 12 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (0[,]π) ⊆
ℝ) |
178 | | eqid 2738 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
179 | 178 | tgioo2 23966 |
. . . . . 6
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
180 | 10 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (0 ∈ ℝ ∧
π ∈ ℝ)) |
181 | | iccntr 23984 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ π ∈ ℝ) → ((int‘(topGen‘ran
(,)))‘(0[,]π)) = (0(,)π)) |
182 | 180, 181 | syl 17 |
. . . . . 6
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(0[,]π)) =
(0(,)π)) |
183 | 124, 129,
136, 176, 177, 179, 178, 182 | dvmptres2 25126 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ (0[,]π) ↦
((sin‘𝑥)↑𝑁))) = (𝑥 ∈ (0(,)π) ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)))) |
184 | 134 | negcld 11319 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ →
-(cos‘𝑥) ∈
ℂ) |
185 | 184 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -(cos‘𝑥) ∈
ℂ) |
186 | 126 | negcld 11319 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ →
-(sin‘𝑥) ∈
ℂ) |
187 | 186 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -(sin‘𝑥) ∈
ℂ) |
188 | | dvcosre 43453 |
. . . . . . . . 9
⊢ (ℝ
D (𝑥 ∈ ℝ ↦
(cos‘𝑥))) = (𝑥 ∈ ℝ ↦
-(sin‘𝑥)) |
189 | 188 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦
(cos‘𝑥))) = (𝑥 ∈ ℝ ↦
-(sin‘𝑥))) |
190 | 124, 135,
187, 189 | dvmptneg 25130 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦
-(cos‘𝑥))) = (𝑥 ∈ ℝ ↦
--(sin‘𝑥))) |
191 | 126 | negnegd 11323 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ →
--(sin‘𝑥) =
(sin‘𝑥)) |
192 | 191 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → --(sin‘𝑥) = (sin‘𝑥)) |
193 | 192 | mpteq2dva 5174 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ --(sin‘𝑥)) = (𝑥 ∈ ℝ ↦ (sin‘𝑥))) |
194 | 190, 193 | eqtrd 2778 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦
-(cos‘𝑥))) = (𝑥 ∈ ℝ ↦
(sin‘𝑥))) |
195 | 124, 185,
127, 194, 177, 179, 178, 182 | dvmptres2 25126 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ (0[,]π) ↦
-(cos‘𝑥))) = (𝑥 ∈ (0(,)π) ↦
(sin‘𝑥))) |
196 | | fveq2 6774 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (sin‘𝑥) =
(sin‘0)) |
197 | | sin0 15858 |
. . . . . . . . . . 11
⊢
(sin‘0) = 0 |
198 | 196, 197 | eqtrdi 2794 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (sin‘𝑥) = 0) |
199 | 198 | oveq1d 7290 |
. . . . . . . . 9
⊢ (𝑥 = 0 → ((sin‘𝑥)↑𝑁) = (0↑𝑁)) |
200 | 199 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 0) → ((sin‘𝑥)↑𝑁) = (0↑𝑁)) |
201 | 19 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 0) → 𝑁 ∈ ℕ) |
202 | 201 | 0expd 13857 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 0) → (0↑𝑁) = 0) |
203 | 200, 202 | eqtrd 2778 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 0) → ((sin‘𝑥)↑𝑁) = 0) |
204 | 203 | oveq1d 7290 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 0) → (((sin‘𝑥)↑𝑁) · -(cos‘𝑥)) = (0 · -(cos‘𝑥))) |
205 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → 𝑥 = 0) |
206 | | 0cn 10967 |
. . . . . . . . . 10
⊢ 0 ∈
ℂ |
207 | 205, 206 | eqeltrdi 2847 |
. . . . . . . . 9
⊢ (𝑥 = 0 → 𝑥 ∈ ℂ) |
208 | | coscl 15836 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ →
(cos‘𝑥) ∈
ℂ) |
209 | 208 | negcld 11319 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ →
-(cos‘𝑥) ∈
ℂ) |
210 | 207, 209 | syl 17 |
. . . . . . . 8
⊢ (𝑥 = 0 → -(cos‘𝑥) ∈
ℂ) |
211 | 210 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 0) → -(cos‘𝑥) ∈ ℂ) |
212 | 211 | mul02d 11173 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 0) → (0 · -(cos‘𝑥)) = 0) |
213 | 204, 212 | eqtrd 2778 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 0) → (((sin‘𝑥)↑𝑁) · -(cos‘𝑥)) = 0) |
214 | | fveq2 6774 |
. . . . . . . . . . 11
⊢ (𝑥 = π → (sin‘𝑥) =
(sin‘π)) |
215 | | sinpi 25614 |
. . . . . . . . . . 11
⊢
(sin‘π) = 0 |
216 | 214, 215 | eqtrdi 2794 |
. . . . . . . . . 10
⊢ (𝑥 = π → (sin‘𝑥) = 0) |
217 | 216 | oveq1d 7290 |
. . . . . . . . 9
⊢ (𝑥 = π → ((sin‘𝑥)↑𝑁) = (0↑𝑁)) |
218 | 217 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = π) → ((sin‘𝑥)↑𝑁) = (0↑𝑁)) |
219 | 19 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = π) → 𝑁 ∈ ℕ) |
220 | 219 | 0expd 13857 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = π) → (0↑𝑁) = 0) |
221 | 218, 220 | eqtrd 2778 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = π) → ((sin‘𝑥)↑𝑁) = 0) |
222 | 221 | oveq1d 7290 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = π) → (((sin‘𝑥)↑𝑁) · -(cos‘𝑥)) = (0 · -(cos‘𝑥))) |
223 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 = π → 𝑥 = π) |
224 | | picn 25616 |
. . . . . . . . . . 11
⊢ π
∈ ℂ |
225 | 223, 224 | eqeltrdi 2847 |
. . . . . . . . . 10
⊢ (𝑥 = π → 𝑥 ∈
ℂ) |
226 | 225 | coscld 15840 |
. . . . . . . . 9
⊢ (𝑥 = π → (cos‘𝑥) ∈
ℂ) |
227 | 226 | negcld 11319 |
. . . . . . . 8
⊢ (𝑥 = π → -(cos‘𝑥) ∈
ℂ) |
228 | 227 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = π) → -(cos‘𝑥) ∈
ℂ) |
229 | 228 | mul02d 11173 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = π) → (0 · -(cos‘𝑥)) = 0) |
230 | 222, 229 | eqtrd 2778 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = π) → (((sin‘𝑥)↑𝑁) · -(cos‘𝑥)) = 0) |
231 | 4, 6, 9, 37, 53, 80, 81, 104, 122, 183, 195, 213, 230 | itgparts 25211 |
. . . 4
⊢ (𝜑 →
∫(0(,)π)(((sin‘𝑥)↑𝑁) · (sin‘𝑥)) d𝑥 = ((0 − 0) −
∫(0(,)π)(((𝑁
· ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥)) |
232 | | df-neg 11208 |
. . . . 5
⊢
-∫(0(,)π)(((𝑁
· ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥 = (0 − ∫(0(,)π)(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥) |
233 | 232 | a1i 11 |
. . . 4
⊢ (𝜑 → -∫(0(,)π)(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥 = (0 − ∫(0(,)π)(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥)) |
234 | 2, 231, 233 | 3eqtr4a 2804 |
. . 3
⊢ (𝜑 →
∫(0(,)π)(((sin‘𝑥)↑𝑁) · (sin‘𝑥)) d𝑥 = -∫(0(,)π)(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥) |
235 | 76, 78, 78 | mulassd 10998 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · (cos‘𝑥)) = ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · ((cos‘𝑥) · (cos‘𝑥)))) |
236 | | sqval 13835 |
. . . . . . . . . . . . . 14
⊢
((cos‘𝑥)
∈ ℂ → ((cos‘𝑥)↑2) = ((cos‘𝑥) · (cos‘𝑥))) |
237 | 236 | eqcomd 2744 |
. . . . . . . . . . . . 13
⊢
((cos‘𝑥)
∈ ℂ → ((cos‘𝑥) · (cos‘𝑥)) = ((cos‘𝑥)↑2)) |
238 | 77, 237 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (0(,)π) →
((cos‘𝑥) ·
(cos‘𝑥)) =
((cos‘𝑥)↑2)) |
239 | 238 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((cos‘𝑥) · (cos‘𝑥)) = ((cos‘𝑥)↑2)) |
240 | 239 | oveq2d 7291 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · ((cos‘𝑥) · (cos‘𝑥))) = ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · ((cos‘𝑥)↑2))) |
241 | 77 | sqcld 13862 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (0(,)π) →
((cos‘𝑥)↑2)
∈ ℂ) |
242 | 241 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((cos‘𝑥)↑2) ∈
ℂ) |
243 | 70, 75, 242 | mulassd 10998 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · ((cos‘𝑥)↑2)) = (𝑁 · (((sin‘𝑥)↑(𝑁 − 1)) · ((cos‘𝑥)↑2)))) |
244 | 240, 243 | eqtrd 2778 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · ((cos‘𝑥) · (cos‘𝑥))) = (𝑁 · (((sin‘𝑥)↑(𝑁 − 1)) · ((cos‘𝑥)↑2)))) |
245 | 75, 242 | mulcomd 10996 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (((sin‘𝑥)↑(𝑁 − 1)) · ((cos‘𝑥)↑2)) = (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) |
246 | 245 | oveq2d 7291 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (𝑁 · (((sin‘𝑥)↑(𝑁 − 1)) · ((cos‘𝑥)↑2))) = (𝑁 · (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 1))))) |
247 | 235, 244,
246 | 3eqtrd 2782 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · (cos‘𝑥)) = (𝑁 · (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 1))))) |
248 | 247 | negeqd 11215 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → -(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · (cos‘𝑥)) = -(𝑁 · (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 1))))) |
249 | 79, 78 | mulneg2d 11429 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) = -(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · (cos‘𝑥))) |
250 | 242, 75 | mulcld 10995 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) ∈
ℂ) |
251 | 70, 250 | mulneg1d 11428 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (-𝑁 · (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) = -(𝑁 · (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))))) |
252 | 248, 249,
251 | 3eqtr4d 2788 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) = (-𝑁 · (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 1))))) |
253 | 252 | itgeq2dv 24946 |
. . . . 5
⊢ (𝜑 → ∫(0(,)π)(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥 = ∫(0(,)π)(-𝑁 · (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 1)))) d𝑥) |
254 | 56 | negcld 11319 |
. . . . . 6
⊢ (𝜑 → -𝑁 ∈ ℂ) |
255 | 38 | sqcld 13862 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0[,]π) →
((cos‘𝑥)↑2)
∈ ℂ) |
256 | 255 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((cos‘𝑥)↑2) ∈
ℂ) |
257 | 256, 107 | mulcld 10995 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) ∈
ℂ) |
258 | | itgsinexplem1.6 |
. . . . . . . . . . . . 13
⊢ 𝑀 = (𝑥 ∈ ℂ ↦ (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) |
259 | 258 | fvmpt2 6886 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧
(((cos‘𝑥)↑2)
· ((sin‘𝑥)↑(𝑁 − 1))) ∈ ℂ) → (𝑀‘𝑥) = (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 1)))) |
260 | 16, 257, 259 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (𝑀‘𝑥) = (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 1)))) |
261 | 260 | eqcomd 2744 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) = (𝑀‘𝑥)) |
262 | 261 | mpteq2dva 5174 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) = (𝑥 ∈ (0[,]π) ↦
(𝑀‘𝑥))) |
263 | | nfmpt1 5182 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑥 ∈ ℂ ↦ (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) |
264 | 258, 263 | nfcxfr 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑀 |
265 | | nfcv 2907 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥cos |
266 | | 2nn0 12250 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ0 |
267 | 266 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 2 ∈
ℕ0) |
268 | 265, 49, 267 | expcnfg 43132 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((cos‘𝑥)↑2)) ∈
(ℂ–cn→ℂ)) |
269 | 268, 60 | mulcncf 24610 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) ∈
(ℂ–cn→ℂ)) |
270 | 258, 269 | eqeltrid 2843 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ (ℂ–cn→ℂ)) |
271 | 264, 270,
35 | cncfmptss 43128 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (𝑀‘𝑥)) ∈ ((0[,]π)–cn→ℂ)) |
272 | 262, 271 | eqeltrd 2839 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) ∈
((0[,]π)–cn→ℂ)) |
273 | | cniccibl 25005 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ π ∈ ℝ ∧ (𝑥 ∈ (0[,]π) ↦ (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) ∈
((0[,]π)–cn→ℂ)) →
(𝑥 ∈ (0[,]π)
↦ (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 1)))) ∈
𝐿1) |
274 | 4, 6, 272, 273 | syl3anc 1370 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) ∈
𝐿1) |
275 | 83, 85, 257, 274 | iblss 24969 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0(,)π) ↦ (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) ∈
𝐿1) |
276 | 254, 250,
275 | itgmulc2 24998 |
. . . . 5
⊢ (𝜑 → (-𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥) = ∫(0(,)π)(-𝑁 · (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) d𝑥) |
277 | 253, 276 | eqtr4d 2781 |
. . . 4
⊢ (𝜑 → ∫(0(,)π)(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥 = (-𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥)) |
278 | 277 | negeqd 11215 |
. . 3
⊢ (𝜑 → -∫(0(,)π)(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥 = -(-𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥)) |
279 | 234, 278 | eqtrd 2778 |
. 2
⊢ (𝜑 →
∫(0(,)π)(((sin‘𝑥)↑𝑁) · (sin‘𝑥)) d𝑥 = -(-𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥)) |
280 | 250, 275 | itgcl 24948 |
. . . 4
⊢ (𝜑 →
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 1))) d𝑥 ∈ ℂ) |
281 | 56, 280 | mulneg1d 11428 |
. . 3
⊢ (𝜑 → (-𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥) = -(𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥)) |
282 | 281 | negeqd 11215 |
. 2
⊢ (𝜑 → -(-𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥) = --(𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥)) |
283 | 56, 280 | mulcld 10995 |
. . 3
⊢ (𝜑 → (𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥) ∈
ℂ) |
284 | 283 | negnegd 11323 |
. 2
⊢ (𝜑 → --(𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥) = (𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥)) |
285 | 279, 282,
284 | 3eqtrd 2782 |
1
⊢ (𝜑 →
∫(0(,)π)(((sin‘𝑥)↑𝑁) · (sin‘𝑥)) d𝑥 = (𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥)) |