Proof of Theorem itgsinexplem1
Step | Hyp | Ref
| Expression |
1 | | 0m0e0 11007 |
. . . . 5
⊢ (0
− 0) = 0 |
2 | 1 | oveq1i 6559 |
. . . 4
⊢ ((0
− 0) − ∫(0(,)π)(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥) = (0 − ∫(0(,)π)(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥) |
3 | | 0re 9919 |
. . . . . 6
⊢ 0 ∈
ℝ |
4 | 3 | a1i 11 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℝ) |
5 | | pire 24014 |
. . . . . 6
⊢ π
∈ ℝ |
6 | 5 | a1i 11 |
. . . . 5
⊢ (𝜑 → π ∈
ℝ) |
7 | | pipos 24016 |
. . . . . . 7
⊢ 0 <
π |
8 | 3, 5, 7 | ltleii 10039 |
. . . . . 6
⊢ 0 ≤
π |
9 | 8 | a1i 11 |
. . . . 5
⊢ (𝜑 → 0 ≤
π) |
10 | 3, 5 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ (0 ∈
ℝ ∧ π ∈ ℝ) |
11 | | iccssre 12126 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ π ∈ ℝ) → (0[,]π) ⊆
ℝ) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(0[,]π) ⊆ ℝ |
13 | | ax-resscn 9872 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ |
14 | 12, 13 | sstri 3577 |
. . . . . . . . . . 11
⊢
(0[,]π) ⊆ ℂ |
15 | 14 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0[,]π) → 𝑥 ∈
ℂ) |
16 | 15 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → 𝑥 ∈ ℂ) |
17 | 15 | sincld 14699 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0[,]π) →
(sin‘𝑥) ∈
ℂ) |
18 | 17 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (sin‘𝑥) ∈
ℂ) |
19 | | itgsinexplem1.7 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℕ) |
20 | 19 | nnnn0d 11228 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
21 | 20 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → 𝑁 ∈
ℕ0) |
22 | 18, 21 | expcld 12870 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑𝑁) ∈ ℂ) |
23 | | itgsinexplem1.1 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) |
24 | 23 | fvmpt2 6200 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
((sin‘𝑥)↑𝑁) ∈ ℂ) → (𝐹‘𝑥) = ((sin‘𝑥)↑𝑁)) |
25 | 16, 22, 24 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (𝐹‘𝑥) = ((sin‘𝑥)↑𝑁)) |
26 | 25 | eqcomd 2616 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑𝑁) = (𝐹‘𝑥)) |
27 | 26 | mpteq2dva 4672 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) = (𝑥 ∈ (0[,]π) ↦ (𝐹‘𝑥))) |
28 | | nfmpt1 4675 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) |
29 | 23, 28 | nfcxfr 2749 |
. . . . . . 7
⊢
Ⅎ𝑥𝐹 |
30 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑥sin |
31 | | sincn 24002 |
. . . . . . . . . 10
⊢ sin
∈ (ℂ–cn→ℂ) |
32 | 31 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → sin ∈
(ℂ–cn→ℂ)) |
33 | 30, 32, 20 | expcnfg 38658 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) ∈ (ℂ–cn→ℂ)) |
34 | 23, 33 | syl5eqel 2692 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ)) |
35 | 14 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (0[,]π) ⊆
ℂ) |
36 | 29, 34, 35 | cncfmptss 38654 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (𝐹‘𝑥)) ∈ ((0[,]π)–cn→ℂ)) |
37 | 27, 36 | eqeltrd 2688 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) ∈ ((0[,]π)–cn→ℂ)) |
38 | 15 | coscld 14700 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0[,]π) →
(cos‘𝑥) ∈
ℂ) |
39 | 38 | negcld 10258 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0[,]π) →
-(cos‘𝑥) ∈
ℂ) |
40 | | itgsinexplem1.2 |
. . . . . . . . . . 11
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ -(cos‘𝑥)) |
41 | 40 | fvmpt2 6200 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧
-(cos‘𝑥) ∈
ℂ) → (𝐺‘𝑥) = -(cos‘𝑥)) |
42 | 15, 39, 41 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0[,]π) → (𝐺‘𝑥) = -(cos‘𝑥)) |
43 | 42 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝑥 ∈ (0[,]π) →
-(cos‘𝑥) = (𝐺‘𝑥)) |
44 | 43 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → -(cos‘𝑥) = (𝐺‘𝑥)) |
45 | 44 | mpteq2dva 4672 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ -(cos‘𝑥)) = (𝑥 ∈ (0[,]π) ↦ (𝐺‘𝑥))) |
46 | | nfmpt1 4675 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑥 ∈ ℂ ↦ -(cos‘𝑥)) |
47 | 40, 46 | nfcxfr 2749 |
. . . . . . 7
⊢
Ⅎ𝑥𝐺 |
48 | | coscn 24003 |
. . . . . . . . 9
⊢ cos
∈ (ℂ–cn→ℂ) |
49 | 48 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → cos ∈
(ℂ–cn→ℂ)) |
50 | 40 | negfcncf 22530 |
. . . . . . . 8
⊢ (cos
∈ (ℂ–cn→ℂ)
→ 𝐺 ∈
(ℂ–cn→ℂ)) |
51 | 49, 50 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ (ℂ–cn→ℂ)) |
52 | 47, 51, 35 | cncfmptss 38654 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (𝐺‘𝑥)) ∈ ((0[,]π)–cn→ℂ)) |
53 | 45, 52 | eqeltrd 2688 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ -(cos‘𝑥)) ∈
((0[,]π)–cn→ℂ)) |
54 | | itgsinexplem1.3 |
. . . . . 6
⊢ 𝐻 = (𝑥 ∈ ℂ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥))) |
55 | | ssid 3587 |
. . . . . . . . . . 11
⊢ ℂ
⊆ ℂ |
56 | 55 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℂ ⊆
ℂ) |
57 | 19 | nncnd 10913 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℂ) |
58 | 56, 57, 56 | constcncfg 38756 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝑁) ∈ (ℂ–cn→ℂ)) |
59 | | nnm1nn0 11211 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
60 | 19, 59 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
61 | 30, 32, 60 | expcnfg 38658 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 1))) ∈ (ℂ–cn→ℂ)) |
62 | 58, 61 | mulcncf 23023 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (𝑁 · ((sin‘𝑥)↑(𝑁 − 1)))) ∈ (ℂ–cn→ℂ)) |
63 | | cosf 14694 |
. . . . . . . . . . 11
⊢
cos:ℂ⟶ℂ |
64 | 63 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 →
cos:ℂ⟶ℂ) |
65 | 64 | feqmptd 6159 |
. . . . . . . . 9
⊢ (𝜑 → cos = (𝑥 ∈ ℂ ↦ (cos‘𝑥))) |
66 | 65, 48 | syl6eqelr 2697 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (cos‘𝑥)) ∈ (ℂ–cn→ℂ)) |
67 | 62, 66 | mulcncf 23023 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥))) ∈ (ℂ–cn→ℂ)) |
68 | 54, 67 | syl5eqel 2692 |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ (ℂ–cn→ℂ)) |
69 | | ioosscn 38563 |
. . . . . . 7
⊢
(0(,)π) ⊆ ℂ |
70 | 69 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (0(,)π) ⊆
ℂ) |
71 | 57 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → 𝑁 ∈ ℂ) |
72 | 69 | sseli 3564 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0(,)π) → 𝑥 ∈
ℂ) |
73 | 72 | sincld 14699 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0(,)π) →
(sin‘𝑥) ∈
ℂ) |
74 | 73 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (sin‘𝑥) ∈
ℂ) |
75 | 60 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (𝑁 − 1) ∈
ℕ0) |
76 | 74, 75 | expcld 12870 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑(𝑁 − 1)) ∈
ℂ) |
77 | 71, 76 | mulcld 9939 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) ∈
ℂ) |
78 | 72 | coscld 14700 |
. . . . . . . 8
⊢ (𝑥 ∈ (0(,)π) →
(cos‘𝑥) ∈
ℂ) |
79 | 78 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (cos‘𝑥) ∈
ℂ) |
80 | 77, 79 | mulcld 9939 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) ∈
ℂ) |
81 | 54, 68, 70, 56, 80 | cncfmptssg 38755 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥))) ∈
((0(,)π)–cn→ℂ)) |
82 | 30, 32, 70 | cncfmptss 38654 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0(,)π) ↦ (sin‘𝑥)) ∈
((0(,)π)–cn→ℂ)) |
83 | | ioossicc 12130 |
. . . . . . 7
⊢
(0(,)π) ⊆ (0[,]π) |
84 | 83 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (0(,)π) ⊆
(0[,]π)) |
85 | | ioombl 23140 |
. . . . . . 7
⊢
(0(,)π) ∈ dom vol |
86 | 85 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (0(,)π) ∈ dom
vol) |
87 | 22, 18 | mulcld 9939 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (((sin‘𝑥)↑𝑁) · (sin‘𝑥)) ∈ ℂ) |
88 | | itgsinexplem1.4 |
. . . . . . . . . . . 12
⊢ 𝐼 = (𝑥 ∈ ℂ ↦ (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) |
89 | 88 | fvmpt2 6200 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧
(((sin‘𝑥)↑𝑁) · (sin‘𝑥)) ∈ ℂ) → (𝐼‘𝑥) = (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) |
90 | 16, 87, 89 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (𝐼‘𝑥) = (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) |
91 | 90 | eqcomd 2616 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (((sin‘𝑥)↑𝑁) · (sin‘𝑥)) = (𝐼‘𝑥)) |
92 | 91 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) = (𝑥 ∈ (0[,]π) ↦ (𝐼‘𝑥))) |
93 | | nfmpt1 4675 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑥 ∈ ℂ ↦ (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) |
94 | 88, 93 | nfcxfr 2749 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝐼 |
95 | | sinf 14693 |
. . . . . . . . . . . . . 14
⊢
sin:ℂ⟶ℂ |
96 | 95 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
sin:ℂ⟶ℂ) |
97 | 96 | feqmptd 6159 |
. . . . . . . . . . . 12
⊢ (𝜑 → sin = (𝑥 ∈ ℂ ↦ (sin‘𝑥))) |
98 | 97, 31 | syl6eqelr 2697 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (sin‘𝑥)) ∈ (ℂ–cn→ℂ)) |
99 | 33, 98 | mulcncf 23023 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) ∈ (ℂ–cn→ℂ)) |
100 | 88, 99 | syl5eqel 2692 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ (ℂ–cn→ℂ)) |
101 | 94, 100, 35 | cncfmptss 38654 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (𝐼‘𝑥)) ∈ ((0[,]π)–cn→ℂ)) |
102 | 92, 101 | eqeltrd 2688 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) ∈ ((0[,]π)–cn→ℂ)) |
103 | | cniccibl 23413 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ π ∈ ℝ ∧ (𝑥 ∈ (0[,]π) ↦ (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) ∈ ((0[,]π)–cn→ℂ)) → (𝑥 ∈ (0[,]π) ↦ (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) ∈
𝐿1) |
104 | 4, 6, 102, 103 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) ∈
𝐿1) |
105 | 84, 86, 87, 104 | iblss 23377 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0(,)π) ↦ (((sin‘𝑥)↑𝑁) · (sin‘𝑥))) ∈
𝐿1) |
106 | 57 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → 𝑁 ∈ ℂ) |
107 | 60 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (𝑁 − 1) ∈
ℕ0) |
108 | 18, 107 | expcld 12870 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑(𝑁 − 1)) ∈
ℂ) |
109 | 106, 108 | mulcld 9939 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) ∈
ℂ) |
110 | 38 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (cos‘𝑥) ∈
ℂ) |
111 | 109, 110 | mulcld 9939 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) ∈
ℂ) |
112 | 39 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → -(cos‘𝑥) ∈
ℂ) |
113 | 111, 112 | mulcld 9939 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) ∈
ℂ) |
114 | | itgsinexplem1.5 |
. . . . . . . 8
⊢ 𝐿 = (𝑥 ∈ ℂ ↦ (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥))) |
115 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ ↦
-(cos‘𝑥)) = (𝑥 ∈ ℂ ↦
-(cos‘𝑥)) |
116 | 115 | negfcncf 22530 |
. . . . . . . . . . 11
⊢ (cos
∈ (ℂ–cn→ℂ)
→ (𝑥 ∈ ℂ
↦ -(cos‘𝑥))
∈ (ℂ–cn→ℂ)) |
117 | 49, 116 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ -(cos‘𝑥)) ∈ (ℂ–cn→ℂ)) |
118 | 67, 117 | mulcncf 23023 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥))) ∈ (ℂ–cn→ℂ)) |
119 | 114, 118 | syl5eqel 2692 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ (ℂ–cn→ℂ)) |
120 | 114, 119,
35, 56, 113 | cncfmptssg 38755 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥))) ∈
((0[,]π)–cn→ℂ)) |
121 | | cniccibl 23413 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ π ∈ ℝ ∧ (𝑥 ∈ (0[,]π) ↦ (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥))) ∈
((0[,]π)–cn→ℂ)) →
(𝑥 ∈ (0[,]π)
↦ (((𝑁 ·
((sin‘𝑥)↑(𝑁 − 1))) ·
(cos‘𝑥)) ·
-(cos‘𝑥))) ∈
𝐿1) |
122 | 4, 6, 120, 121 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥))) ∈
𝐿1) |
123 | 84, 86, 113, 122 | iblss 23377 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0(,)π) ↦ (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥))) ∈
𝐿1) |
124 | | reelprrecn 9907 |
. . . . . . 7
⊢ ℝ
∈ {ℝ, ℂ} |
125 | 124 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
126 | | recn 9905 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
127 | 126 | sincld 14699 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ →
(sin‘𝑥) ∈
ℂ) |
128 | 127 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (sin‘𝑥) ∈
ℂ) |
129 | 20 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑁 ∈
ℕ0) |
130 | 128, 129 | expcld 12870 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((sin‘𝑥)↑𝑁) ∈ ℂ) |
131 | 57 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑁 ∈ ℂ) |
132 | 60 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑁 − 1) ∈
ℕ0) |
133 | 128, 132 | expcld 12870 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((sin‘𝑥)↑(𝑁 − 1)) ∈
ℂ) |
134 | 131, 133 | mulcld 9939 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) ∈
ℂ) |
135 | 126 | coscld 14700 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ →
(cos‘𝑥) ∈
ℂ) |
136 | 135 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (cos‘𝑥) ∈
ℂ) |
137 | 134, 136 | mulcld 9939 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) ∈
ℂ) |
138 | | sincl 14695 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℂ →
(sin‘𝑥) ∈
ℂ) |
139 | 138 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (sin‘𝑥) ∈
ℂ) |
140 | 20 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑁 ∈
ℕ0) |
141 | 139, 140 | expcld 12870 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((sin‘𝑥)↑𝑁) ∈ ℂ) |
142 | 141, 23 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
143 | 126 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) |
144 | | elex 3185 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) ∈ ℂ → ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) ∈ V) |
145 | 137, 144 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) ∈ V) |
146 | | rabid 3095 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {𝑥 ∈ ℂ ∣ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) ∈ V} ↔ (𝑥 ∈ ℂ ∧ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) ∈ V)) |
147 | 143, 145,
146 | sylanbrc 695 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ {𝑥 ∈ ℂ ∣ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) ∈ V}) |
148 | 54 | dmmpt 5547 |
. . . . . . . . . . . . 13
⊢ dom 𝐻 = {𝑥 ∈ ℂ ∣ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) ∈ V} |
149 | 147, 148 | syl6eleqr 2699 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ dom 𝐻) |
150 | 149 | ex 449 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℝ → 𝑥 ∈ dom 𝐻)) |
151 | 150 | alrimiv 1842 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥(𝑥 ∈ ℝ → 𝑥 ∈ dom 𝐻)) |
152 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥ℝ |
153 | | nfmpt1 4675 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑥 ∈ ℂ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥))) |
154 | 54, 153 | nfcxfr 2749 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝐻 |
155 | 154 | nfdm 5288 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥dom
𝐻 |
156 | 152, 155 | dfss2f 3559 |
. . . . . . . . . 10
⊢ (ℝ
⊆ dom 𝐻 ↔
∀𝑥(𝑥 ∈ ℝ → 𝑥 ∈ dom 𝐻)) |
157 | 151, 156 | sylibr 223 |
. . . . . . . . 9
⊢ (𝜑 → ℝ ⊆ dom 𝐻) |
158 | 19 | dvsinexp 38798 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁))) = (𝑥 ∈ ℂ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)))) |
159 | 23 | oveq2i 6560 |
. . . . . . . . . . 11
⊢ (ℂ
D 𝐹) = (ℂ D (𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁))) |
160 | 158, 159,
54 | 3eqtr4g 2669 |
. . . . . . . . . 10
⊢ (𝜑 → (ℂ D 𝐹) = 𝐻) |
161 | 160 | dmeqd 5248 |
. . . . . . . . 9
⊢ (𝜑 → dom (ℂ D 𝐹) = dom 𝐻) |
162 | 157, 161 | sseqtr4d 3605 |
. . . . . . . 8
⊢ (𝜑 → ℝ ⊆ dom
(ℂ D 𝐹)) |
163 | | dvres3 23483 |
. . . . . . . 8
⊢
(((ℝ ∈ {ℝ, ℂ} ∧ 𝐹:ℂ⟶ℂ) ∧ (ℂ
⊆ ℂ ∧ ℝ ⊆ dom (ℂ D 𝐹))) → (ℝ D (𝐹 ↾ ℝ)) = ((ℂ D 𝐹) ↾
ℝ)) |
164 | 125, 142,
56, 162, 163 | syl22anc 1319 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝐹 ↾ ℝ)) = ((ℂ D
𝐹) ↾
ℝ)) |
165 | 23 | reseq1i 5313 |
. . . . . . . . . 10
⊢ (𝐹 ↾ ℝ) = ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁)) ↾
ℝ) |
166 | | resmpt 5369 |
. . . . . . . . . . 11
⊢ (ℝ
⊆ ℂ → ((𝑥
∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) ↾ ℝ) = (𝑥 ∈ ℝ ↦ ((sin‘𝑥)↑𝑁))) |
167 | 13, 166 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁)) ↾ ℝ) = (𝑥 ∈ ℝ ↦
((sin‘𝑥)↑𝑁)) |
168 | 165, 167 | eqtri 2632 |
. . . . . . . . 9
⊢ (𝐹 ↾ ℝ) = (𝑥 ∈ ℝ ↦
((sin‘𝑥)↑𝑁)) |
169 | 168 | oveq2i 6560 |
. . . . . . . 8
⊢ (ℝ
D (𝐹 ↾ ℝ)) =
(ℝ D (𝑥 ∈
ℝ ↦ ((sin‘𝑥)↑𝑁))) |
170 | 169 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝐹 ↾ ℝ)) = (ℝ D
(𝑥 ∈ ℝ ↦
((sin‘𝑥)↑𝑁)))) |
171 | 160 | reseq1d 5316 |
. . . . . . . 8
⊢ (𝜑 → ((ℂ D 𝐹) ↾ ℝ) = (𝐻 ↾
ℝ)) |
172 | 54 | reseq1i 5313 |
. . . . . . . . 9
⊢ (𝐻 ↾ ℝ) = ((𝑥 ∈ ℂ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥))) ↾
ℝ) |
173 | | resmpt 5369 |
. . . . . . . . . 10
⊢ (ℝ
⊆ ℂ → ((𝑥
∈ ℂ ↦ ((𝑁
· ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)))) |
174 | 13, 173 | ax-mp 5 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥))) |
175 | 172, 174 | eqtri 2632 |
. . . . . . . 8
⊢ (𝐻 ↾ ℝ) = (𝑥 ∈ ℝ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥))) |
176 | 171, 175 | syl6eq 2660 |
. . . . . . 7
⊢ (𝜑 → ((ℂ D 𝐹) ↾ ℝ) = (𝑥 ∈ ℝ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)))) |
177 | 164, 170,
176 | 3eqtr3d 2652 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦
((sin‘𝑥)↑𝑁))) = (𝑥 ∈ ℝ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)))) |
178 | 12 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (0[,]π) ⊆
ℝ) |
179 | | eqid 2610 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
180 | 179 | tgioo2 22414 |
. . . . . 6
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
181 | 10 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (0 ∈ ℝ ∧
π ∈ ℝ)) |
182 | | iccntr 22432 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ π ∈ ℝ) → ((int‘(topGen‘ran
(,)))‘(0[,]π)) = (0(,)π)) |
183 | 181, 182 | syl 17 |
. . . . . 6
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(0[,]π)) =
(0(,)π)) |
184 | 125, 130,
137, 177, 178, 180, 179, 183 | dvmptres2 23531 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ (0[,]π) ↦
((sin‘𝑥)↑𝑁))) = (𝑥 ∈ (0(,)π) ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)))) |
185 | 135 | negcld 10258 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ →
-(cos‘𝑥) ∈
ℂ) |
186 | 185 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -(cos‘𝑥) ∈
ℂ) |
187 | 127 | negcld 10258 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ →
-(sin‘𝑥) ∈
ℂ) |
188 | 187 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -(sin‘𝑥) ∈
ℂ) |
189 | | dvcosre 38799 |
. . . . . . . . 9
⊢ (ℝ
D (𝑥 ∈ ℝ ↦
(cos‘𝑥))) = (𝑥 ∈ ℝ ↦
-(sin‘𝑥)) |
190 | 189 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦
(cos‘𝑥))) = (𝑥 ∈ ℝ ↦
-(sin‘𝑥))) |
191 | 125, 136,
188, 190 | dvmptneg 23535 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦
-(cos‘𝑥))) = (𝑥 ∈ ℝ ↦
--(sin‘𝑥))) |
192 | 127 | negnegd 10262 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ →
--(sin‘𝑥) =
(sin‘𝑥)) |
193 | 192 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → --(sin‘𝑥) = (sin‘𝑥)) |
194 | 193 | mpteq2dva 4672 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ --(sin‘𝑥)) = (𝑥 ∈ ℝ ↦ (sin‘𝑥))) |
195 | 191, 194 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦
-(cos‘𝑥))) = (𝑥 ∈ ℝ ↦
(sin‘𝑥))) |
196 | 125, 186,
128, 195, 178, 180, 179, 183 | dvmptres2 23531 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ (0[,]π) ↦
-(cos‘𝑥))) = (𝑥 ∈ (0(,)π) ↦
(sin‘𝑥))) |
197 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (sin‘𝑥) =
(sin‘0)) |
198 | | sin0 14718 |
. . . . . . . . . . 11
⊢
(sin‘0) = 0 |
199 | 197, 198 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (sin‘𝑥) = 0) |
200 | 199 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑥 = 0 → ((sin‘𝑥)↑𝑁) = (0↑𝑁)) |
201 | 200 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 0) → ((sin‘𝑥)↑𝑁) = (0↑𝑁)) |
202 | 19 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 0) → 𝑁 ∈ ℕ) |
203 | 202 | 0expd 12886 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 0) → (0↑𝑁) = 0) |
204 | 201, 203 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 0) → ((sin‘𝑥)↑𝑁) = 0) |
205 | 204 | oveq1d 6564 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 0) → (((sin‘𝑥)↑𝑁) · -(cos‘𝑥)) = (0 · -(cos‘𝑥))) |
206 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → 𝑥 = 0) |
207 | | 0cn 9911 |
. . . . . . . . . 10
⊢ 0 ∈
ℂ |
208 | 206, 207 | syl6eqel 2696 |
. . . . . . . . 9
⊢ (𝑥 = 0 → 𝑥 ∈ ℂ) |
209 | | coscl 14696 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ →
(cos‘𝑥) ∈
ℂ) |
210 | 209 | negcld 10258 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ →
-(cos‘𝑥) ∈
ℂ) |
211 | 208, 210 | syl 17 |
. . . . . . . 8
⊢ (𝑥 = 0 → -(cos‘𝑥) ∈
ℂ) |
212 | 211 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 0) → -(cos‘𝑥) ∈ ℂ) |
213 | 212 | mul02d 10113 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 0) → (0 · -(cos‘𝑥)) = 0) |
214 | 205, 213 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 0) → (((sin‘𝑥)↑𝑁) · -(cos‘𝑥)) = 0) |
215 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = π → (sin‘𝑥) =
(sin‘π)) |
216 | | sinpi 24013 |
. . . . . . . . . . 11
⊢
(sin‘π) = 0 |
217 | 215, 216 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝑥 = π → (sin‘𝑥) = 0) |
218 | 217 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑥 = π → ((sin‘𝑥)↑𝑁) = (0↑𝑁)) |
219 | 218 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = π) → ((sin‘𝑥)↑𝑁) = (0↑𝑁)) |
220 | 19 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = π) → 𝑁 ∈ ℕ) |
221 | 220 | 0expd 12886 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = π) → (0↑𝑁) = 0) |
222 | 219, 221 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = π) → ((sin‘𝑥)↑𝑁) = 0) |
223 | 222 | oveq1d 6564 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = π) → (((sin‘𝑥)↑𝑁) · -(cos‘𝑥)) = (0 · -(cos‘𝑥))) |
224 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 = π → 𝑥 = π) |
225 | | picn 24015 |
. . . . . . . . . . 11
⊢ π
∈ ℂ |
226 | 224, 225 | syl6eqel 2696 |
. . . . . . . . . 10
⊢ (𝑥 = π → 𝑥 ∈
ℂ) |
227 | 226 | coscld 14700 |
. . . . . . . . 9
⊢ (𝑥 = π → (cos‘𝑥) ∈
ℂ) |
228 | 227 | negcld 10258 |
. . . . . . . 8
⊢ (𝑥 = π → -(cos‘𝑥) ∈
ℂ) |
229 | 228 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = π) → -(cos‘𝑥) ∈
ℂ) |
230 | 229 | mul02d 10113 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = π) → (0 · -(cos‘𝑥)) = 0) |
231 | 223, 230 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = π) → (((sin‘𝑥)↑𝑁) · -(cos‘𝑥)) = 0) |
232 | 4, 6, 9, 37, 53, 81, 82, 105, 123, 184, 196, 214, 231 | itgparts 23614 |
. . . 4
⊢ (𝜑 →
∫(0(,)π)(((sin‘𝑥)↑𝑁) · (sin‘𝑥)) d𝑥 = ((0 − 0) −
∫(0(,)π)(((𝑁
· ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥)) |
233 | | df-neg 10148 |
. . . . 5
⊢
-∫(0(,)π)(((𝑁
· ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥 = (0 − ∫(0(,)π)(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥) |
234 | 233 | a1i 11 |
. . . 4
⊢ (𝜑 → -∫(0(,)π)(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥 = (0 − ∫(0(,)π)(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥)) |
235 | 2, 232, 234 | 3eqtr4a 2670 |
. . 3
⊢ (𝜑 →
∫(0(,)π)(((sin‘𝑥)↑𝑁) · (sin‘𝑥)) d𝑥 = -∫(0(,)π)(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥) |
236 | 77, 79, 79 | mulassd 9942 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · (cos‘𝑥)) = ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · ((cos‘𝑥) · (cos‘𝑥)))) |
237 | | sqval 12784 |
. . . . . . . . . . . . . 14
⊢
((cos‘𝑥)
∈ ℂ → ((cos‘𝑥)↑2) = ((cos‘𝑥) · (cos‘𝑥))) |
238 | 237 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢
((cos‘𝑥)
∈ ℂ → ((cos‘𝑥) · (cos‘𝑥)) = ((cos‘𝑥)↑2)) |
239 | 78, 238 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (0(,)π) →
((cos‘𝑥) ·
(cos‘𝑥)) =
((cos‘𝑥)↑2)) |
240 | 239 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((cos‘𝑥) · (cos‘𝑥)) = ((cos‘𝑥)↑2)) |
241 | 240 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · ((cos‘𝑥) · (cos‘𝑥))) = ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · ((cos‘𝑥)↑2))) |
242 | 78 | sqcld 12868 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (0(,)π) →
((cos‘𝑥)↑2)
∈ ℂ) |
243 | 242 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((cos‘𝑥)↑2) ∈
ℂ) |
244 | 71, 76, 243 | mulassd 9942 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · ((cos‘𝑥)↑2)) = (𝑁 · (((sin‘𝑥)↑(𝑁 − 1)) · ((cos‘𝑥)↑2)))) |
245 | 241, 244 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · ((cos‘𝑥) · (cos‘𝑥))) = (𝑁 · (((sin‘𝑥)↑(𝑁 − 1)) · ((cos‘𝑥)↑2)))) |
246 | 76, 243 | mulcomd 9940 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (((sin‘𝑥)↑(𝑁 − 1)) · ((cos‘𝑥)↑2)) = (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) |
247 | 246 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (𝑁 · (((sin‘𝑥)↑(𝑁 − 1)) · ((cos‘𝑥)↑2))) = (𝑁 · (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 1))))) |
248 | 236, 245,
247 | 3eqtrd 2648 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · (cos‘𝑥)) = (𝑁 · (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 1))))) |
249 | 248 | negeqd 10154 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → -(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · (cos‘𝑥)) = -(𝑁 · (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 1))))) |
250 | 80, 79 | mulneg2d 10363 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) = -(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · (cos‘𝑥))) |
251 | 243, 76 | mulcld 9939 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) ∈
ℂ) |
252 | 71, 251 | mulneg1d 10362 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (-𝑁 · (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) = -(𝑁 · (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))))) |
253 | 249, 250,
252 | 3eqtr4d 2654 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) = (-𝑁 · (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 1))))) |
254 | 253 | itgeq2dv 23354 |
. . . . 5
⊢ (𝜑 → ∫(0(,)π)(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥 = ∫(0(,)π)(-𝑁 · (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 1)))) d𝑥) |
255 | 57 | negcld 10258 |
. . . . . 6
⊢ (𝜑 → -𝑁 ∈ ℂ) |
256 | 38 | sqcld 12868 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0[,]π) →
((cos‘𝑥)↑2)
∈ ℂ) |
257 | 256 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((cos‘𝑥)↑2) ∈
ℂ) |
258 | 257, 108 | mulcld 9939 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) ∈
ℂ) |
259 | | itgsinexplem1.6 |
. . . . . . . . . . . . 13
⊢ 𝑀 = (𝑥 ∈ ℂ ↦ (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) |
260 | 259 | fvmpt2 6200 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧
(((cos‘𝑥)↑2)
· ((sin‘𝑥)↑(𝑁 − 1))) ∈ ℂ) → (𝑀‘𝑥) = (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 1)))) |
261 | 16, 258, 260 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (𝑀‘𝑥) = (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 1)))) |
262 | 261 | eqcomd 2616 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) = (𝑀‘𝑥)) |
263 | 262 | mpteq2dva 4672 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) = (𝑥 ∈ (0[,]π) ↦
(𝑀‘𝑥))) |
264 | | nfmpt1 4675 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑥 ∈ ℂ ↦ (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) |
265 | 259, 264 | nfcxfr 2749 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑀 |
266 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥cos |
267 | | 2nn0 11186 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ0 |
268 | 267 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 2 ∈
ℕ0) |
269 | 266, 49, 268 | expcnfg 38658 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((cos‘𝑥)↑2)) ∈
(ℂ–cn→ℂ)) |
270 | 269, 61 | mulcncf 23023 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) ∈
(ℂ–cn→ℂ)) |
271 | 259, 270 | syl5eqel 2692 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ (ℂ–cn→ℂ)) |
272 | 265, 271,
35 | cncfmptss 38654 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (𝑀‘𝑥)) ∈ ((0[,]π)–cn→ℂ)) |
273 | 263, 272 | eqeltrd 2688 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) ∈
((0[,]π)–cn→ℂ)) |
274 | | cniccibl 23413 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ π ∈ ℝ ∧ (𝑥 ∈ (0[,]π) ↦ (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) ∈
((0[,]π)–cn→ℂ)) →
(𝑥 ∈ (0[,]π)
↦ (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 1)))) ∈
𝐿1) |
275 | 4, 6, 273, 274 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) ∈
𝐿1) |
276 | 84, 86, 258, 275 | iblss 23377 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0(,)π) ↦ (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) ∈
𝐿1) |
277 | 255, 251,
276 | itgmulc2 23406 |
. . . . 5
⊢ (𝜑 → (-𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥) = ∫(0(,)π)(-𝑁 · (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1)))) d𝑥) |
278 | 254, 277 | eqtr4d 2647 |
. . . 4
⊢ (𝜑 → ∫(0(,)π)(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥 = (-𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥)) |
279 | 278 | negeqd 10154 |
. . 3
⊢ (𝜑 → -∫(0(,)π)(((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)) d𝑥 = -(-𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥)) |
280 | 235, 279 | eqtrd 2644 |
. 2
⊢ (𝜑 →
∫(0(,)π)(((sin‘𝑥)↑𝑁) · (sin‘𝑥)) d𝑥 = -(-𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥)) |
281 | 251, 276 | itgcl 23356 |
. . . 4
⊢ (𝜑 →
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 1))) d𝑥 ∈ ℂ) |
282 | 57, 281 | mulneg1d 10362 |
. . 3
⊢ (𝜑 → (-𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥) = -(𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥)) |
283 | 282 | negeqd 10154 |
. 2
⊢ (𝜑 → -(-𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥) = --(𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥)) |
284 | 57, 281 | mulcld 9939 |
. . 3
⊢ (𝜑 → (𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥) ∈
ℂ) |
285 | 284 | negnegd 10262 |
. 2
⊢ (𝜑 → --(𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥) = (𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥)) |
286 | 280, 283,
285 | 3eqtrd 2648 |
1
⊢ (𝜑 →
∫(0(,)π)(((sin‘𝑥)↑𝑁) · (sin‘𝑥)) d𝑥 = (𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 1))) d𝑥)) |