Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . . . . . 7
⊢ ((𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ) → 𝑚 = 𝑁) |
2 | 1 | oveq2d 7187 |
. . . . . 6
⊢ ((𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ) → (2 · 𝑚) = (2 · 𝑁)) |
3 | 2 | oveq1d 7186 |
. . . . 5
⊢ ((𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ) → ((2 · 𝑚) + 1) = ((2 · 𝑁) + 1)) |
4 | 3 | oveq1d 7186 |
. . . 4
⊢ ((𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ) → (((2 · 𝑚) + 1) / (2 · π)) =
(((2 · 𝑁) + 1) / (2
· π))) |
5 | 1 | oveq1d 7186 |
. . . . . 6
⊢ ((𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ) → (𝑚 + (1 / 2)) = (𝑁 + (1 / 2))) |
6 | 5 | fvoveq1d 7193 |
. . . . 5
⊢ ((𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ) → (sin‘((𝑚 + (1 / 2)) · 𝑠)) = (sin‘((𝑁 + (1 / 2)) · 𝑠))) |
7 | 6 | oveq1d 7186 |
. . . 4
⊢ ((𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ) → ((sin‘((𝑚 + (1 / 2)) · 𝑠)) / ((2 · π) ·
(sin‘(𝑠 / 2)))) =
((sin‘((𝑁 + (1 / 2))
· 𝑠)) / ((2 ·
π) · (sin‘(𝑠 / 2))))) |
8 | 4, 7 | ifeq12d 4436 |
. . 3
⊢ ((𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ) → if((𝑠 mod (2 · π)) = 0,
(((2 · 𝑚) + 1) / (2
· π)), ((sin‘((𝑚 + (1 / 2)) · 𝑠)) / ((2 · π) ·
(sin‘(𝑠 / 2))))) =
if((𝑠 mod (2 ·
π)) = 0, (((2 · 𝑁) + 1) / (2 · π)),
((sin‘((𝑁 + (1 / 2))
· 𝑠)) / ((2 ·
π) · (sin‘(𝑠 / 2)))))) |
9 | 8 | mpteq2dva 5126 |
. 2
⊢ (𝑚 = 𝑁 → (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0,
(((2 · 𝑚) + 1) / (2
· π)), ((sin‘((𝑚 + (1 / 2)) · 𝑠)) / ((2 · π) ·
(sin‘(𝑠 / 2)))))) =
(𝑠 ∈ ℝ ↦
if((𝑠 mod (2 ·
π)) = 0, (((2 · 𝑁) + 1) / (2 · π)),
((sin‘((𝑁 + (1 / 2))
· 𝑠)) / ((2 ·
π) · (sin‘(𝑠 / 2))))))) |
10 | | dirkerval.1 |
. . 3
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0,
(((2 · 𝑛) + 1) / (2
· π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) ·
(sin‘(𝑠 /
2))))))) |
11 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ) → 𝑛 = 𝑚) |
12 | 11 | oveq2d 7187 |
. . . . . . . 8
⊢ ((𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ) → (2 · 𝑛) = (2 · 𝑚)) |
13 | 12 | oveq1d 7186 |
. . . . . . 7
⊢ ((𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ) → ((2 · 𝑛) + 1) = ((2 · 𝑚) + 1)) |
14 | 13 | oveq1d 7186 |
. . . . . 6
⊢ ((𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ) → (((2 · 𝑛) + 1) / (2 · π)) =
(((2 · 𝑚) + 1) / (2
· π))) |
15 | 11 | oveq1d 7186 |
. . . . . . . 8
⊢ ((𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ) → (𝑛 + (1 / 2)) = (𝑚 + (1 / 2))) |
16 | 15 | fvoveq1d 7193 |
. . . . . . 7
⊢ ((𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ) → (sin‘((𝑛 + (1 / 2)) · 𝑠)) = (sin‘((𝑚 + (1 / 2)) · 𝑠))) |
17 | 16 | oveq1d 7186 |
. . . . . 6
⊢ ((𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ) → ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) ·
(sin‘(𝑠 / 2)))) =
((sin‘((𝑚 + (1 / 2))
· 𝑠)) / ((2 ·
π) · (sin‘(𝑠 / 2))))) |
18 | 14, 17 | ifeq12d 4436 |
. . . . 5
⊢ ((𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ) → if((𝑠 mod (2 · π)) = 0,
(((2 · 𝑛) + 1) / (2
· π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) ·
(sin‘(𝑠 / 2))))) =
if((𝑠 mod (2 ·
π)) = 0, (((2 · 𝑚) + 1) / (2 · π)),
((sin‘((𝑚 + (1 / 2))
· 𝑠)) / ((2 ·
π) · (sin‘(𝑠 / 2)))))) |
19 | 18 | mpteq2dva 5126 |
. . . 4
⊢ (𝑛 = 𝑚 → (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0,
(((2 · 𝑛) + 1) / (2
· π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) ·
(sin‘(𝑠 / 2)))))) =
(𝑠 ∈ ℝ ↦
if((𝑠 mod (2 ·
π)) = 0, (((2 · 𝑚) + 1) / (2 · π)),
((sin‘((𝑚 + (1 / 2))
· 𝑠)) / ((2 ·
π) · (sin‘(𝑠 / 2))))))) |
20 | 19 | cbvmptv 5134 |
. . 3
⊢ (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦
if((𝑠 mod (2 ·
π)) = 0, (((2 · 𝑛) + 1) / (2 · π)),
((sin‘((𝑛 + (1 / 2))
· 𝑠)) / ((2 ·
π) · (sin‘(𝑠 / 2))))))) = (𝑚 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0,
(((2 · 𝑚) + 1) / (2
· π)), ((sin‘((𝑚 + (1 / 2)) · 𝑠)) / ((2 · π) ·
(sin‘(𝑠 /
2))))))) |
21 | 10, 20 | eqtri 2761 |
. 2
⊢ 𝐷 = (𝑚 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0,
(((2 · 𝑚) + 1) / (2
· π)), ((sin‘((𝑚 + (1 / 2)) · 𝑠)) / ((2 · π) ·
(sin‘(𝑠 /
2))))))) |
22 | | reex 10707 |
. . 3
⊢ ℝ
∈ V |
23 | 22 | mptex 6997 |
. 2
⊢ (𝑠 ∈ ℝ ↦
if((𝑠 mod (2 ·
π)) = 0, (((2 · 𝑁) + 1) / (2 · π)),
((sin‘((𝑁 + (1 / 2))
· 𝑠)) / ((2 ·
π) · (sin‘(𝑠 / 2)))))) ∈ V |
24 | 9, 21, 23 | fvmpt 6776 |
1
⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁) = (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0,
(((2 · 𝑁) + 1) / (2
· π)), ((sin‘((𝑁 + (1 / 2)) · 𝑠)) / ((2 · π) ·
(sin‘(𝑠 /
2))))))) |