dirkerdenne0

Description: The Dirichlet kernel denominator is never 0 . (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	dirkerdenne0	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to 2 π \sin (\frac{S}{2}) \neq 0$

Proof

Step	Hyp	Ref	Expression
1		2cnd	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to 2 \in ℂ$
2		picn	$⊢ π \in ℂ$
3	2	a1i	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to π \in ℂ$
4	1 3	mulcld	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to 2 π \in ℂ$
5		recn	$⊢ S \in ℝ \to S \in ℂ$
6	5	adantr	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to S \in ℂ$
7	6	halfcld	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to \frac{S}{2} \in ℂ$
8	7	sincld	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to \sin (\frac{S}{2}) \in ℂ$
9		2ne0	$⊢ 2 \neq 0$
10	9	a1i	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to 2 \neq 0$
11		0re	$⊢ 0 \in ℝ$
12		pipos	$⊢ 0 < π$
13	11 12	gtneii	$⊢ π \neq 0$
14	13	a1i	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to π \neq 0$
15	1 3 10 14	mulne0d	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to 2 π \neq 0$
16	6 1 3 10 14	divdiv1d	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to \frac{\frac{S}{2}}{π} = \frac{S}{2 π}$
17		simpr	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to \neg S \mod 2 π = 0$
18		2rp	$⊢ 2 \in ℝ^{+}$
19		pirp	$⊢ π \in ℝ^{+}$
20		rpmulcl	$⊢ (2 \in ℝ^{+} \land π \in ℝ^{+}) \to 2 π \in ℝ^{+}$
21	18 19 20	mp2an	$⊢ 2 π \in ℝ^{+}$
22		mod0	$⊢ (S \in ℝ \land 2 π \in ℝ^{+}) \to (S \mod 2 π = 0 \leftrightarrow \frac{S}{2 π} \in ℤ)$
23	21 22	mpan2	$⊢ S \in ℝ \to (S \mod 2 π = 0 \leftrightarrow \frac{S}{2 π} \in ℤ)$
24	23	adantr	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to (S \mod 2 π = 0 \leftrightarrow \frac{S}{2 π} \in ℤ)$
25	17 24	mtbid	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to \neg \frac{S}{2 π} \in ℤ$
26	16 25	eqneltrd	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to \neg \frac{\frac{S}{2}}{π} \in ℤ$
27		sineq0	$⊢ \frac{S}{2} \in ℂ \to (\sin (\frac{S}{2}) = 0 \leftrightarrow \frac{\frac{S}{2}}{π} \in ℤ)$
28	7 27	syl	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to (\sin (\frac{S}{2}) = 0 \leftrightarrow \frac{\frac{S}{2}}{π} \in ℤ)$
29	26 28	mtbird	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to \neg \sin (\frac{S}{2}) = 0$
30	29	neqned	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to \sin (\frac{S}{2}) \neq 0$
31	4 8 15 30	mulne0d	$⊢ (S \in ℝ \land \neg S \mod 2 π = 0) \to 2 π \sin (\frac{S}{2}) \neq 0$

Metamath Proof Explorer

Theorem dirkerdenne0

Proof