dirker2re

Description: The Dirichlet kernel value is a real if the argument is not a multiple of π . (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	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 ℝ$

Proof

Step	Hyp	Ref	Expression
1		nnre	$⊢ N \in ℕ \to N \in ℝ$
2	1	ad2antrr	$⊢ ((N \in ℕ \land S \in ℝ) \land \neg S \mod 2 π = 0) \to N \in ℝ$
3		1red	$⊢ ((N \in ℕ \land S \in ℝ) \land \neg S \mod 2 π = 0) \to 1 \in ℝ$
4	3	rehalfcld	$⊢ ((N \in ℕ \land S \in ℝ) \land \neg S \mod 2 π = 0) \to \frac{1}{2} \in ℝ$
5	2 4	readdcld	$⊢ ((N \in ℕ \land S \in ℝ) \land \neg S \mod 2 π = 0) \to N + (\frac{1}{2}) \in ℝ$
6		simplr	$⊢ ((N \in ℕ \land S \in ℝ) \land \neg S \mod 2 π = 0) \to S \in ℝ$
7	5 6	remulcld	$⊢ ((N \in ℕ \land S \in ℝ) \land \neg S \mod 2 π = 0) \to (N + (\frac{1}{2})) S \in ℝ$
8	7	resincld	$⊢ ((N \in ℕ \land S \in ℝ) \land \neg S \mod 2 π = 0) \to \sin (N + (\frac{1}{2})) S \in ℝ$
9		2re	$⊢ 2 \in ℝ$
10	9	a1i	$⊢ ((N \in ℕ \land S \in ℝ) \land \neg S \mod 2 π = 0) \to 2 \in ℝ$
11		pire	$⊢ π \in ℝ$
12	11	a1i	$⊢ ((N \in ℕ \land S \in ℝ) \land \neg S \mod 2 π = 0) \to π \in ℝ$
13	10 12	remulcld	$⊢ ((N \in ℕ \land S \in ℝ) \land \neg S \mod 2 π = 0) \to 2 π \in ℝ$
14	6	rehalfcld	$⊢ ((N \in ℕ \land S \in ℝ) \land \neg S \mod 2 π = 0) \to \frac{S}{2} \in ℝ$
15	14	resincld	$⊢ ((N \in ℕ \land S \in ℝ) \land \neg S \mod 2 π = 0) \to \sin (\frac{S}{2}) \in ℝ$
16	13 15	remulcld	$⊢ ((N \in ℕ \land S \in ℝ) \land \neg S \mod 2 π = 0) \to 2 π \sin (\frac{S}{2}) \in ℝ$
17		2cnd	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to 2 \in ℂ$
18		picn	$⊢ π \in ℂ$
19	18	a1i	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to π \in ℂ$
20	17 19	mulcld	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to 2 π \in ℂ$
21		recn	$⊢ S \in ℝ \to S \in ℂ$
22	21	adantr	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to S \in ℂ$
23	22	halfcld	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to \frac{S}{2} \in ℂ$
24	23	sincld	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to \sin (\frac{S}{2}) \in ℂ$
25		2ne0	$⊢ 2 \neq 0$
26	25	a1i	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to 2 \neq 0$
27		0re	$⊢ 0 \in ℝ$
28		pipos	$⊢ 0 < π$
29	27 28	gtneii	$⊢ π \neq 0$
30	29	a1i	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to π \neq 0$
31	17 19 26 30	mulne0d	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to 2 π \neq 0$
32	22 17 19 26 30	divdiv1d	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to \frac{\frac{S}{2}}{π} = \frac{S}{2 π}$
33		simpr	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to \neg S \mod 2 π = 0$
34		2rp	$⊢ 2 \in ℝ^{+}$
35		pirp	$⊢ π \in ℝ^{+}$
36		rpmulcl	$⊢ (2 \in ℝ^{+} \land π \in ℝ^{+}) \to 2 π \in ℝ^{+}$
37	34 35 36	mp2an	$⊢ 2 π \in ℝ^{+}$
38		mod0	$⊢ (S \in ℝ \land 2 π \in ℝ^{+}) \to (S \mod 2 π = 0 \leftrightarrow \frac{S}{2 π} \in ℤ)$
39	37 38	mpan2	$⊢ S \in ℝ \to (S \mod 2 π = 0 \leftrightarrow \frac{S}{2 π} \in ℤ)$
40	39	adantr	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to (S \mod 2 π = 0 \leftrightarrow \frac{S}{2 π} \in ℤ)$
41	33 40	mtbid	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to \neg \frac{S}{2 π} \in ℤ$
42	32 41	eqneltrd	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to \neg \frac{\frac{S}{2}}{π} \in ℤ$
43		sineq0	$⊢ \frac{S}{2} \in ℂ \to (\sin (\frac{S}{2}) = 0 \leftrightarrow \frac{\frac{S}{2}}{π} \in ℤ)$
44	23 43	syl	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to (\sin (\frac{S}{2}) = 0 \leftrightarrow \frac{\frac{S}{2}}{π} \in ℤ)$
45	42 44	mtbird	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to \neg \sin (\frac{S}{2}) = 0$
46	45	neqned	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to \sin (\frac{S}{2}) \neq 0$
47	20 24 31 46	mulne0d	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to 2 π \sin (\frac{S}{2}) \neq 0$
48	47	adantll	$⊢ ((N \in ℕ \land S \in ℝ) \land \neg S \mod 2 π = 0) \to 2 π \sin (\frac{S}{2}) \neq 0$
49	8 16 48	redivcld	$⊢ ((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 ℝ$

Metamath Proof Explorer

Theorem dirker2re

Proof