dirkerval2

Description: The N_th Dirichlet Kernel evaluated at a specific point S . (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Hypothesis	dirkerval2.1	$⊢ D = (n \in ℕ ⟼ (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})))$
	Assertion	dirkerval2	$⊢ (N \in ℕ \land S \in ℝ) \to D (N) (S) = if (S \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) S}{2 π \sin (\frac{S}{2})})$

Proof

Step	Hyp	Ref	Expression
1		dirkerval2.1	$⊢ D = (n \in ℕ ⟼ (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})))$
2	1	dirkerval	$⊢ N \in ℕ \to D (N) = (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}))$
3		oveq1	$⊢ s = t \to s \mod 2 π = t \mod 2 π$
4	3	eqeq1d	$⊢ s = t \to (s \mod 2 π = 0 \leftrightarrow t \mod 2 π = 0)$
5		oveq2	$⊢ s = t \to (N + (\frac{1}{2})) s = (N + (\frac{1}{2})) t$
6	5	fveq2d	$⊢ s = t \to \sin (N + (\frac{1}{2})) s = \sin (N + (\frac{1}{2})) t$
7		fvoveq1	$⊢ s = t \to \sin (\frac{s}{2}) = \sin (\frac{t}{2})$
8	7	oveq2d	$⊢ s = t \to 2 π \sin (\frac{s}{2}) = 2 π \sin (\frac{t}{2})$
9	6 8	oveq12d	$⊢ s = t \to \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})} = \frac{\sin (N + (\frac{1}{2})) t}{2 π \sin (\frac{t}{2})}$
10	4 9	ifbieq2d	$⊢ s = t \to if (s \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}) = if (t \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) t}{2 π \sin (\frac{t}{2})})$
11	10	cbvmptv	$⊢ (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})) = (t \in ℝ ⟼ if (t \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) t}{2 π \sin (\frac{t}{2})}))$
12	2 11	eqtrdi	$⊢ N \in ℕ \to D (N) = (t \in ℝ ⟼ if (t \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) t}{2 π \sin (\frac{t}{2})}))$
13	12	adantr	$⊢ (N \in ℕ \land S \in ℝ) \to D (N) = (t \in ℝ ⟼ if (t \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) t}{2 π \sin (\frac{t}{2})}))$
14		simpr	$⊢ ((N \in ℕ \land S \in ℝ) \land t = S) \to t = S$
15	14	oveq1d	$⊢ ((N \in ℕ \land S \in ℝ) \land t = S) \to t \mod 2 π = S \mod 2 π$
16	15	eqeq1d	$⊢ ((N \in ℕ \land S \in ℝ) \land t = S) \to (t \mod 2 π = 0 \leftrightarrow S \mod 2 π = 0)$
17	14	oveq2d	$⊢ ((N \in ℕ \land S \in ℝ) \land t = S) \to (N + (\frac{1}{2})) t = (N + (\frac{1}{2})) S$
18	17	fveq2d	$⊢ ((N \in ℕ \land S \in ℝ) \land t = S) \to \sin (N + (\frac{1}{2})) t = \sin (N + (\frac{1}{2})) S$
19	14	fvoveq1d	$⊢ ((N \in ℕ \land S \in ℝ) \land t = S) \to \sin (\frac{t}{2}) = \sin (\frac{S}{2})$
20	19	oveq2d	$⊢ ((N \in ℕ \land S \in ℝ) \land t = S) \to 2 π \sin (\frac{t}{2}) = 2 π \sin (\frac{S}{2})$
21	18 20	oveq12d	$⊢ ((N \in ℕ \land S \in ℝ) \land t = S) \to \frac{\sin (N + (\frac{1}{2})) t}{2 π \sin (\frac{t}{2})} = \frac{\sin (N + (\frac{1}{2})) S}{2 π \sin (\frac{S}{2})}$
22	16 21	ifbieq2d	$⊢ ((N \in ℕ \land S \in ℝ) \land t = S) \to if (t \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) t}{2 π \sin (\frac{t}{2})}) = if (S \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) S}{2 π \sin (\frac{S}{2})})$
23		simpr	$⊢ (N \in ℕ \land S \in ℝ) \to S \in ℝ$
24		2re	$⊢ 2 \in ℝ$
25	24	a1i	$⊢ N \in ℕ \to 2 \in ℝ$
26		nnre	$⊢ N \in ℕ \to N \in ℝ$
27	25 26	remulcld	$⊢ N \in ℕ \to 2 \cdot N \in ℝ$
28		1red	$⊢ N \in ℕ \to 1 \in ℝ$
29	27 28	readdcld	$⊢ N \in ℕ \to 2 \cdot N + 1 \in ℝ$
30		pire	$⊢ π \in ℝ$
31	30	a1i	$⊢ N \in ℕ \to π \in ℝ$
32	25 31	remulcld	$⊢ N \in ℕ \to 2 π \in ℝ$
33		2cnd	$⊢ N \in ℕ \to 2 \in ℂ$
34	31	recnd	$⊢ N \in ℕ \to π \in ℂ$
35		2pos	$⊢ 0 < 2$
36	35	a1i	$⊢ N \in ℕ \to 0 < 2$
37	36	gt0ne0d	$⊢ N \in ℕ \to 2 \neq 0$
38		pipos	$⊢ 0 < π$
39	38	a1i	$⊢ N \in ℕ \to 0 < π$
40	39	gt0ne0d	$⊢ N \in ℕ \to π \neq 0$
41	33 34 37 40	mulne0d	$⊢ N \in ℕ \to 2 π \neq 0$
42	29 32 41	redivcld	$⊢ N \in ℕ \to \frac{2 \cdot N + 1}{2 π} \in ℝ$
43	42	ad2antrr	$⊢ ((N \in ℕ \land S \in ℝ) \land S \mod 2 π = 0) \to \frac{2 \cdot N + 1}{2 π} \in ℝ$
44		dirker2re	$⊢ ((N \in ℕ \land S \in ℝ) \land \neg S \mod 2 π = 0) \to \frac{\sin (N + (\frac{1}{2})) S}{2 π \sin (\frac{S}{2})} \in ℝ$
45	43 44	ifclda	$⊢ (N \in ℕ \land S \in ℝ) \to if (S \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) S}{2 π \sin (\frac{S}{2})}) \in ℝ$
46	13 22 23 45	fvmptd	$⊢ (N \in ℕ \land S \in ℝ) \to D (N) (S) = if (S \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) S}{2 π \sin (\frac{S}{2})})$

Metamath Proof Explorer

Theorem dirkerval2

Proof