Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . . . . 7
⊢ ((𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ) → 𝑚 = 𝑁) |
2 | 1 | oveq2d 6666 |
. . . . . 6
⊢ ((𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ) → (2 · 𝑚) = (2 · 𝑁)) |
3 | 2 | oveq1d 6665 |
. . . . 5
⊢ ((𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ) → ((2 · 𝑚) + 1) = ((2 · 𝑁) + 1)) |
4 | 3 | oveq1d 6665 |
. . . 4
⊢ ((𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ) → (((2 · 𝑚) + 1) / (2 · π)) =
(((2 · 𝑁) + 1) / (2
· π))) |
5 | 1 | oveq1d 6665 |
. . . . . . 7
⊢ ((𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ) → (𝑚 + (1 / 2)) = (𝑁 + (1 / 2))) |
6 | 5 | oveq1d 6665 |
. . . . . 6
⊢ ((𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ) → ((𝑚 + (1 / 2)) · 𝑠) = ((𝑁 + (1 / 2)) · 𝑠)) |
7 | 6 | fveq2d 6195 |
. . . . 5
⊢ ((𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ) → (sin‘((𝑚 + (1 / 2)) · 𝑠)) = (sin‘((𝑁 + (1 / 2)) · 𝑠))) |
8 | 7 | oveq1d 6665 |
. . . 4
⊢ ((𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ) → ((sin‘((𝑚 + (1 / 2)) · 𝑠)) / ((2 · π) ·
(sin‘(𝑠 / 2)))) =
((sin‘((𝑁 + (1 / 2))
· 𝑠)) / ((2 ·
π) · (sin‘(𝑠 / 2))))) |
9 | 4, 8 | ifeq12d 4106 |
. . 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)))))) |
10 | 9 | mpteq2dva 4744 |
. 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))))))) |
11 | | dirkerval.1 |
. . 3
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0,
(((2 · 𝑛) + 1) / (2
· π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) ·
(sin‘(𝑠 /
2))))))) |
12 | | simpl 473 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ) → 𝑛 = 𝑚) |
13 | 12 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ) → (2 · 𝑛) = (2 · 𝑚)) |
14 | 13 | oveq1d 6665 |
. . . . . . 7
⊢ ((𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ) → ((2 · 𝑛) + 1) = ((2 · 𝑚) + 1)) |
15 | 14 | oveq1d 6665 |
. . . . . 6
⊢ ((𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ) → (((2 · 𝑛) + 1) / (2 · π)) =
(((2 · 𝑚) + 1) / (2
· π))) |
16 | 12 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ) → (𝑛 + (1 / 2)) = (𝑚 + (1 / 2))) |
17 | 16 | oveq1d 6665 |
. . . . . . . 8
⊢ ((𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ) → ((𝑛 + (1 / 2)) · 𝑠) = ((𝑚 + (1 / 2)) · 𝑠)) |
18 | 17 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ) → (sin‘((𝑛 + (1 / 2)) · 𝑠)) = (sin‘((𝑚 + (1 / 2)) · 𝑠))) |
19 | 18 | oveq1d 6665 |
. . . . . 6
⊢ ((𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ) → ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) ·
(sin‘(𝑠 / 2)))) =
((sin‘((𝑚 + (1 / 2))
· 𝑠)) / ((2 ·
π) · (sin‘(𝑠 / 2))))) |
20 | 15, 19 | ifeq12d 4106 |
. . . . 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)))))) |
21 | 20 | mpteq2dva 4744 |
. . . 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))))))) |
22 | 21 | cbvmptv 4750 |
. . 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))))))) |
23 | 11, 22 | eqtri 2644 |
. 2
⊢ 𝐷 = (𝑚 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0,
(((2 · 𝑚) + 1) / (2
· π)), ((sin‘((𝑚 + (1 / 2)) · 𝑠)) / ((2 · π) ·
(sin‘(𝑠 /
2))))))) |
24 | | reex 10027 |
. . 3
⊢ ℝ
∈ V |
25 | 24 | mptex 6486 |
. 2
⊢ (𝑠 ∈ ℝ ↦
if((𝑠 mod (2 ·
π)) = 0, (((2 · 𝑁) + 1) / (2 · π)),
((sin‘((𝑁 + (1 / 2))
· 𝑠)) / ((2 ·
π) · (sin‘(𝑠 / 2)))))) ∈ V |
26 | 10, 23, 25 | fvmpt 6282 |
1
⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁) = (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0,
(((2 · 𝑁) + 1) / (2
· π)), ((sin‘((𝑁 + (1 / 2)) · 𝑠)) / ((2 · π) ·
(sin‘(𝑠 /
2))))))) |