Proof of Theorem itgsinexp
Step | Hyp | Ref
| Expression |
1 | | itgsinexp.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘2)) |
2 | | eluzelz 12448 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℤ) |
3 | | zcn 12181 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
4 | 1, 2, 3 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℂ) |
5 | | 1cnd 10828 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℂ) |
6 | 4, 5 | npcand 11193 |
. . . . . 6
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
7 | 6 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 → 𝑁 = ((𝑁 − 1) + 1)) |
8 | 7 | oveq1d 7228 |
. . . 4
⊢ (𝜑 → (𝑁 · (𝐼‘𝑁)) = (((𝑁 − 1) + 1) · (𝐼‘𝑁))) |
9 | | uz2m1nn 12519 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 1) ∈ ℕ) |
10 | 1, 9 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑁 − 1) ∈ ℕ) |
11 | 10 | nncnd 11846 |
. . . . 5
⊢ (𝜑 → (𝑁 − 1) ∈ ℂ) |
12 | | itgsinexp.1 |
. . . . . . . 8
⊢ 𝐼 = (𝑛 ∈ ℕ0 ↦
∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥) |
13 | 12 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐼 = (𝑛 ∈ ℕ0 ↦
∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)) |
14 | | oveq2 7221 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → ((sin‘𝑥)↑𝑛) = ((sin‘𝑥)↑𝑁)) |
15 | 14 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 = 𝑁) ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑𝑛) = ((sin‘𝑥)↑𝑁)) |
16 | 15 | itgeq2dv 24679 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥 = ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥) |
17 | | 2cnd 11908 |
. . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℂ) |
18 | | npcan 11087 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ) → ((𝑁 −
2) + 2) = 𝑁) |
19 | 18 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ) → 𝑁 = ((𝑁 − 2) +
2)) |
20 | 4, 17, 19 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 = ((𝑁 − 2) + 2)) |
21 | | uznn0sub 12473 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 2) ∈
ℕ0) |
22 | 1, 21 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 − 2) ∈
ℕ0) |
23 | | 2nn0 12107 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
24 | 23 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℕ0) |
25 | 22, 24 | nn0addcld 12154 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 − 2) + 2) ∈
ℕ0) |
26 | 20, 25 | eqeltrd 2838 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
27 | | itgex 24668 |
. . . . . . . 8
⊢
∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥 ∈ V |
28 | 27 | a1i 11 |
. . . . . . 7
⊢ (𝜑 →
∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥 ∈ V) |
29 | 13, 16, 26, 28 | fvmptd 6825 |
. . . . . 6
⊢ (𝜑 → (𝐼‘𝑁) = ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥) |
30 | | ioosscn 12997 |
. . . . . . . . . . 11
⊢
(0(,)π) ⊆ ℂ |
31 | 30 | sseli 3896 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0(,)π) → 𝑥 ∈
ℂ) |
32 | 31 | sincld 15691 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0(,)π) →
(sin‘𝑥) ∈
ℂ) |
33 | 32 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (sin‘𝑥) ∈
ℂ) |
34 | 26 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → 𝑁 ∈
ℕ0) |
35 | 33, 34 | expcld 13716 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑𝑁) ∈ ℂ) |
36 | | ioossicc 13021 |
. . . . . . . . 9
⊢
(0(,)π) ⊆ (0[,]π) |
37 | 36 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (0(,)π) ⊆
(0[,]π)) |
38 | | ioombl 24462 |
. . . . . . . . 9
⊢
(0(,)π) ∈ dom vol |
39 | 38 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (0(,)π) ∈ dom
vol) |
40 | | 0re 10835 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
41 | | pire 25348 |
. . . . . . . . . . . . . 14
⊢ π
∈ ℝ |
42 | | iccssre 13017 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ π ∈ ℝ) → (0[,]π) ⊆
ℝ) |
43 | 40, 41, 42 | mp2an 692 |
. . . . . . . . . . . . 13
⊢
(0[,]π) ⊆ ℝ |
44 | | ax-resscn 10786 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℂ |
45 | 43, 44 | sstri 3910 |
. . . . . . . . . . . 12
⊢
(0[,]π) ⊆ ℂ |
46 | 45 | sseli 3896 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0[,]π) → 𝑥 ∈
ℂ) |
47 | 46 | sincld 15691 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0[,]π) →
(sin‘𝑥) ∈
ℂ) |
48 | 47 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (sin‘𝑥) ∈
ℂ) |
49 | 26 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → 𝑁 ∈
ℕ0) |
50 | 48, 49 | expcld 13716 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑𝑁) ∈ ℂ) |
51 | 40 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℝ) |
52 | 41 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → π ∈
ℝ) |
53 | 46 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → 𝑥 ∈ ℂ) |
54 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁)) = (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) |
55 | 54 | fvmpt2 6829 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧
((sin‘𝑥)↑𝑁) ∈ ℂ) → ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁))‘𝑥) = ((sin‘𝑥)↑𝑁)) |
56 | 53, 50, 55 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁))‘𝑥) = ((sin‘𝑥)↑𝑁)) |
57 | 56 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑𝑁) = ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁))‘𝑥)) |
58 | 57 | mpteq2dva 5150 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) = (𝑥 ∈ (0[,]π) ↦ ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁))‘𝑥))) |
59 | | nfmpt1 5153 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) |
60 | | nfcv 2904 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥sin |
61 | | sincn 25336 |
. . . . . . . . . . . . 13
⊢ sin
∈ (ℂ–cn→ℂ) |
62 | 61 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → sin ∈
(ℂ–cn→ℂ)) |
63 | 60, 62, 26 | expcnfg 42807 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁)) ∈ (ℂ–cn→ℂ)) |
64 | 45 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (0[,]π) ⊆
ℂ) |
65 | 59, 63, 64 | cncfmptss 42803 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑𝑁))‘𝑥)) ∈ ((0[,]π)–cn→ℂ)) |
66 | 58, 65 | eqeltrd 2838 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑𝑁)) ∈ ((0[,]π)–cn→ℂ)) |
67 | | cniccibl 24738 |
. . . . . . . . 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 24702 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((sin‘𝑥)↑𝑁)) ∈
𝐿1) |
70 | 35, 69 | itgcl 24681 |
. . . . . 6
⊢ (𝜑 →
∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥 ∈ ℂ) |
71 | 29, 70 | eqeltrd 2838 |
. . . . 5
⊢ (𝜑 → (𝐼‘𝑁) ∈ ℂ) |
72 | 11, 71 | adddirp1d 10859 |
. . . 4
⊢ (𝜑 → (((𝑁 − 1) + 1) · (𝐼‘𝑁)) = (((𝑁 − 1) · (𝐼‘𝑁)) + (𝐼‘𝑁))) |
73 | | eluz2b2 12517 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁)) |
74 | 1, 73 | sylib 221 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 1 < 𝑁)) |
75 | 74 | simpld 498 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℕ) |
76 | | expm1t 13663 |
. . . . . . . . . 10
⊢
(((sin‘𝑥)
∈ ℂ ∧ 𝑁
∈ ℕ) → ((sin‘𝑥)↑𝑁) = (((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥))) |
77 | 32, 75, 76 | syl2anr 600 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑𝑁) = (((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥))) |
78 | 77 | itgeq2dv 24679 |
. . . . . . . 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 43170 |
. . . . . . . . 9
⊢ (𝜑 →
∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 1)) · (sin‘𝑥)) d𝑥 = ((𝑁 − 1) ·
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) d𝑥)) |
86 | 4, 5, 5 | subsub4d 11220 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑁 − 1) − 1) = (𝑁 − (1 + 1))) |
87 | | 1p1e2 11955 |
. . . . . . . . . . . . . . . . 17
⊢ (1 + 1) =
2 |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 + 1) =
2) |
89 | 88 | oveq2d 7229 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 − (1 + 1)) = (𝑁 − 2)) |
90 | 86, 89 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 − 1) − 1) = (𝑁 − 2)) |
91 | 90 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((𝑁 − 1) − 1) = (𝑁 − 2)) |
92 | 91 | oveq2d 7229 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑((𝑁 − 1) − 1)) = ((sin‘𝑥)↑(𝑁 − 2))) |
93 | 92 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑((𝑁 − 1) − 1))) =
(((cos‘𝑥)↑2)
· ((sin‘𝑥)↑(𝑁 − 2)))) |
94 | 93 | itgeq2dv 24679 |
. . . . . . . . . 10
⊢ (𝜑 →
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) d𝑥 = ∫(0(,)π)(((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 2))) d𝑥) |
95 | 94 | oveq2d 7229 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 − 1) ·
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑((𝑁 − 1) − 1))) d𝑥) = ((𝑁 − 1) ·
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥)) |
96 | | sincossq 15737 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ →
(((sin‘𝑥)↑2) +
((cos‘𝑥)↑2)) =
1) |
97 | | 1cnd 10828 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ → 1 ∈
ℂ) |
98 | | sincl 15687 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ →
(sin‘𝑥) ∈
ℂ) |
99 | 98 | sqcld 13714 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ →
((sin‘𝑥)↑2)
∈ ℂ) |
100 | | coscl 15688 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ →
(cos‘𝑥) ∈
ℂ) |
101 | 100 | sqcld 13714 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ →
((cos‘𝑥)↑2)
∈ ℂ) |
102 | 97, 99, 101 | subaddd 11207 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → ((1
− ((sin‘𝑥)↑2)) = ((cos‘𝑥)↑2) ↔ (((sin‘𝑥)↑2) + ((cos‘𝑥)↑2)) =
1)) |
103 | 96, 102 | mpbird 260 |
. . . . . . . . . . . . . . . 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 7228 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (0(,)π) →
(((cos‘𝑥)↑2)
· ((sin‘𝑥)↑(𝑁 − 2))) = ((1 −
((sin‘𝑥)↑2))
· ((sin‘𝑥)↑(𝑁 − 2)))) |
107 | 106 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (((cos‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 2))) = ((1 −
((sin‘𝑥)↑2))
· ((sin‘𝑥)↑(𝑁 − 2)))) |
108 | 107 | itgeq2dv 24679 |
. . . . . . . . . . 11
⊢ (𝜑 →
∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 2))) d𝑥 = ∫(0(,)π)((1 −
((sin‘𝑥)↑2))
· ((sin‘𝑥)↑(𝑁 − 2))) d𝑥) |
109 | | 1cnd 10828 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → 1 ∈
ℂ) |
110 | 32 | sqcld 13714 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0(,)π) →
((sin‘𝑥)↑2)
∈ ℂ) |
111 | 110 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑2) ∈
ℂ) |
112 | 90 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 − 2) = ((𝑁 − 1) − 1)) |
113 | | nnm1nn0 12131 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 − 1) ∈ ℕ
→ ((𝑁 − 1)
− 1) ∈ ℕ0) |
114 | 10, 113 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑁 − 1) − 1) ∈
ℕ0) |
115 | 112, 114 | eqeltrd 2838 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 − 2) ∈
ℕ0) |
116 | 115 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (𝑁 − 2) ∈
ℕ0) |
117 | 33, 116 | expcld 13716 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑(𝑁 − 2)) ∈
ℂ) |
118 | 109, 111,
117 | subdird 11289 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((1 −
((sin‘𝑥)↑2))
· ((sin‘𝑥)↑(𝑁 − 2))) = ((1 ·
((sin‘𝑥)↑(𝑁 − 2))) −
(((sin‘𝑥)↑2)
· ((sin‘𝑥)↑(𝑁 − 2))))) |
119 | 117 | mulid2d 10851 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (1 ·
((sin‘𝑥)↑(𝑁 − 2))) =
((sin‘𝑥)↑(𝑁 − 2))) |
120 | 23 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → 2 ∈
ℕ0) |
121 | 33, 116, 120 | expaddd 13718 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑(2 + (𝑁 − 2))) = (((sin‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 2)))) |
122 | 17, 4 | pncan3d 11192 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 + (𝑁 − 2)) = 𝑁) |
123 | 122 | oveq2d 7229 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((sin‘𝑥)↑(2 + (𝑁 − 2))) = ((sin‘𝑥)↑𝑁)) |
124 | 123 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑(2 + (𝑁 − 2))) = ((sin‘𝑥)↑𝑁)) |
125 | 121, 124 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (((sin‘𝑥)↑2) ·
((sin‘𝑥)↑(𝑁 − 2))) =
((sin‘𝑥)↑𝑁)) |
126 | 119, 125 | oveq12d 7231 |
. . . . . . . . . . . . 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 24679 |
. . . . . . . . . . 11
⊢ (𝜑 → ∫(0(,)π)((1 −
((sin‘𝑥)↑2))
· ((sin‘𝑥)↑(𝑁 − 2))) d𝑥 = ∫(0(,)π)(((sin‘𝑥)↑(𝑁 − 2)) − ((sin‘𝑥)↑𝑁)) d𝑥) |
129 | 115 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (𝑁 − 2) ∈
ℕ0) |
130 | 48, 129 | expcld 13716 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑(𝑁 − 2)) ∈
ℂ) |
131 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ ↦
((sin‘𝑥)↑(𝑁 − 2))) = (𝑥 ∈ ℂ ↦
((sin‘𝑥)↑(𝑁 − 2))) |
132 | 131 | fvmpt2 6829 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℂ ∧
((sin‘𝑥)↑(𝑁 − 2)) ∈ ℂ)
→ ((𝑥 ∈ ℂ
↦ ((sin‘𝑥)↑(𝑁 − 2)))‘𝑥) = ((sin‘𝑥)↑(𝑁 − 2))) |
133 | 53, 130, 132 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑(𝑁 − 2)))‘𝑥) = ((sin‘𝑥)↑(𝑁 − 2))) |
134 | 133 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → ((sin‘𝑥)↑(𝑁 − 2)) = ((𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2)))‘𝑥)) |
135 | 134 | mpteq2dva 5150 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) = (𝑥 ∈ (0[,]π) ↦ ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑(𝑁 − 2)))‘𝑥))) |
136 | | nfmpt1 5153 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2))) |
137 | 60, 62, 115 | expcnfg 42807 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈ (ℂ–cn→ℂ)) |
138 | 136, 137,
64 | cncfmptss 42803 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((𝑥 ∈ ℂ ↦
((sin‘𝑥)↑(𝑁 − 2)))‘𝑥)) ∈
((0[,]π)–cn→ℂ)) |
139 | 135, 138 | eqeltrd 2838 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈ ((0[,]π)–cn→ℂ)) |
140 | | cniccibl 24738 |
. . . . . . . . . . . . . 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 24702 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((sin‘𝑥)↑(𝑁 − 2))) ∈
𝐿1) |
143 | 117, 142,
35, 69 | itgsub 24723 |
. . . . . . . . . . 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 7229 |
. . . . . . . . 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 7221 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑁 − 2) → ((sin‘𝑥)↑𝑛) = ((sin‘𝑥)↑(𝑁 − 2))) |
149 | 148 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑛 = (𝑁 − 2) ∧ 𝑥 ∈ (0(,)π)) → ((sin‘𝑥)↑𝑛) = ((sin‘𝑥)↑(𝑁 − 2))) |
150 | 149 | itgeq2dv 24679 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑁 − 2) →
∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥 = ∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥) |
151 | | itgex 24668 |
. . . . . . . . . . 11
⊢
∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 ∈ V |
152 | 151 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 →
∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 ∈ V) |
153 | 12, 150, 115, 152 | fvmptd3 6841 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼‘(𝑁 − 2)) =
∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥) |
154 | 153, 29 | oveq12d 7231 |
. . . . . . . 8
⊢ (𝜑 → ((𝐼‘(𝑁 − 2)) − (𝐼‘𝑁)) = (∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥)) |
155 | 154 | oveq2d 7229 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 − 1) · ((𝐼‘(𝑁 − 2)) − (𝐼‘𝑁))) = ((𝑁 − 1) ·
(∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 − ∫(0(,)π)((sin‘𝑥)↑𝑁) d𝑥))) |
156 | 117, 142 | itgcl 24681 |
. . . . . . . . 9
⊢ (𝜑 →
∫(0(,)π)((sin‘𝑥)↑(𝑁 − 2)) d𝑥 ∈ ℂ) |
157 | 153, 156 | eqeltrd 2838 |
. . . . . . . 8
⊢ (𝜑 → (𝐼‘(𝑁 − 2)) ∈
ℂ) |
158 | 11, 157, 71 | subdid 11288 |
. . . . . . 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 10853 |
. . . . . 6
⊢ (𝜑 → ((𝑁 − 1) · (𝐼‘(𝑁 − 2))) ∈
ℂ) |
162 | 11, 71 | mulcld 10853 |
. . . . . 6
⊢ (𝜑 → ((𝑁 − 1) · (𝐼‘𝑁)) ∈ ℂ) |
163 | 161, 162,
71 | subaddd 11207 |
. . . . 5
⊢ (𝜑 → ((((𝑁 − 1) · (𝐼‘(𝑁 − 2))) − ((𝑁 − 1) · (𝐼‘𝑁))) = (𝐼‘𝑁) ↔ (((𝑁 − 1) · (𝐼‘𝑁)) + (𝐼‘𝑁)) = ((𝑁 − 1) · (𝐼‘(𝑁 − 2))))) |
164 | 160, 163 | mpbid 235 |
. . . 4
⊢ (𝜑 → (((𝑁 − 1) · (𝐼‘𝑁)) + (𝐼‘𝑁)) = ((𝑁 − 1) · (𝐼‘(𝑁 − 2)))) |
165 | 8, 72, 164 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → (𝑁 · (𝐼‘𝑁)) = ((𝑁 − 1) · (𝐼‘(𝑁 − 2)))) |
166 | 165 | oveq1d 7228 |
. 2
⊢ (𝜑 → ((𝑁 · (𝐼‘𝑁)) / 𝑁) = (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) / 𝑁)) |
167 | 75 | nnne0d 11880 |
. . 3
⊢ (𝜑 → 𝑁 ≠ 0) |
168 | 71, 4, 167 | divcan3d 11613 |
. 2
⊢ (𝜑 → ((𝑁 · (𝐼‘𝑁)) / 𝑁) = (𝐼‘𝑁)) |
169 | 11, 157, 4, 167 | div23d 11645 |
. 2
⊢ (𝜑 → (((𝑁 − 1) · (𝐼‘(𝑁 − 2))) / 𝑁) = (((𝑁 − 1) / 𝑁) · (𝐼‘(𝑁 − 2)))) |
170 | 166, 168,
169 | 3eqtr3d 2785 |
1
⊢ (𝜑 → (𝐼‘𝑁) = (((𝑁 − 1) / 𝑁) · (𝐼‘(𝑁 − 2)))) |