fourierdlem44

Description: A condition for having ( sin( A / 2 ) ) nonzero. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	fourierdlem44	$⊢ (A \in [- π, π] \land A \neq 0) \to \sin (\frac{A}{2}) \neq 0$

Proof

Step	Hyp	Ref	Expression
1		0xr	$⊢ 0 \in ℝ^{*}$
2	1	a1i	$⊢ (A \in [- π, π] \land 0 < A) \to 0 \in ℝ^{*}$
3		2re	$⊢ 2 \in ℝ$
4		pire	$⊢ π \in ℝ$
5	3 4	remulcli	$⊢ 2 π \in ℝ$
6	5	rexri	$⊢ 2 π \in ℝ^{*}$
7	6	a1i	$⊢ (A \in [- π, π] \land 0 < A) \to 2 π \in ℝ^{*}$
8	4	renegcli	$⊢ - π \in ℝ$
9	8	a1i	$⊢ A \in [- π, π] \to - π \in ℝ$
10	4	a1i	$⊢ A \in [- π, π] \to π \in ℝ$
11		id	$⊢ A \in [- π, π] \to A \in [- π, π]$
12		eliccre	$⊢ (- π \in ℝ \land π \in ℝ \land A \in [- π, π]) \to A \in ℝ$
13	9 10 11 12	syl3anc	$⊢ A \in [- π, π] \to A \in ℝ$
14	13	adantr	$⊢ (A \in [- π, π] \land 0 < A) \to A \in ℝ$
15		simpr	$⊢ (A \in [- π, π] \land 0 < A) \to 0 < A$
16	5	a1i	$⊢ A \in [- π, π] \to 2 π \in ℝ$
17	9	rexrd	$⊢ A \in [- π, π] \to - π \in ℝ^{*}$
18	10	rexrd	$⊢ A \in [- π, π] \to π \in ℝ^{*}$
19		iccleub	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land A \in [- π, π]) \to A \leq π$
20	17 18 11 19	syl3anc	$⊢ A \in [- π, π] \to A \leq π$
21		pirp	$⊢ π \in ℝ^{+}$
22		2timesgt	$⊢ π \in ℝ^{+} \to π < 2 π$
23	21 22	ax-mp	$⊢ π < 2 π$
24	23	a1i	$⊢ A \in [- π, π] \to π < 2 π$
25	13 10 16 20 24	lelttrd	$⊢ A \in [- π, π] \to A < 2 π$
26	25	adantr	$⊢ (A \in [- π, π] \land 0 < A) \to A < 2 π$
27	2 7 14 15 26	eliood	$⊢ (A \in [- π, π] \land 0 < A) \to A \in (0, 2 π)$
28	27	adantlr	$⊢ ((A \in [- π, π] \land A \neq 0) \land 0 < A) \to A \in (0, 2 π)$
29		sinaover2ne0	$⊢ A \in (0, 2 π) \to \sin (\frac{A}{2}) \neq 0$
30	28 29	syl	$⊢ ((A \in [- π, π] \land A \neq 0) \land 0 < A) \to \sin (\frac{A}{2}) \neq 0$
31		simpll	$⊢ ((A \in [- π, π] \land A \neq 0) \land \neg 0 < A) \to A \in [- π, π]$
32	31 13	syl	$⊢ ((A \in [- π, π] \land A \neq 0) \land \neg 0 < A) \to A \in ℝ$
33		0red	$⊢ ((A \in [- π, π] \land A \neq 0) \land \neg 0 < A) \to 0 \in ℝ$
34		simplr	$⊢ ((A \in [- π, π] \land A \neq 0) \land \neg 0 < A) \to A \neq 0$
35		simpr	$⊢ ((A \in [- π, π] \land A \neq 0) \land \neg 0 < A) \to \neg 0 < A$
36	32 33 34 35	lttri5d	$⊢ ((A \in [- π, π] \land A \neq 0) \land \neg 0 < A) \to A < 0$
37	13	recnd	$⊢ A \in [- π, π] \to A \in ℂ$
38	37	halfcld	$⊢ A \in [- π, π] \to \frac{A}{2} \in ℂ$
39		sinneg	$⊢ \frac{A}{2} \in ℂ \to \sin (- \frac{A}{2}) = - \sin (\frac{A}{2})$
40	38 39	syl	$⊢ A \in [- π, π] \to \sin (- \frac{A}{2}) = - \sin (\frac{A}{2})$
41		2cnd	$⊢ A \in [- π, π] \to 2 \in ℂ$
42		2ne0	$⊢ 2 \neq 0$
43	42	a1i	$⊢ A \in [- π, π] \to 2 \neq 0$
44	37 41 43	divnegd	$⊢ A \in [- π, π] \to - \frac{A}{2} = \frac{- A}{2}$
45	44	fveq2d	$⊢ A \in [- π, π] \to \sin (- \frac{A}{2}) = \sin (\frac{- A}{2})$
46	40 45	eqtr3d	$⊢ A \in [- π, π] \to - \sin (\frac{A}{2}) = \sin (\frac{- A}{2})$
47	46	adantr	$⊢ (A \in [- π, π] \land A < 0) \to - \sin (\frac{A}{2}) = \sin (\frac{- A}{2})$
48	1	a1i	$⊢ (A \in [- π, π] \land A < 0) \to 0 \in ℝ^{*}$
49	6	a1i	$⊢ (A \in [- π, π] \land A < 0) \to 2 π \in ℝ^{*}$
50	13	renegcld	$⊢ A \in [- π, π] \to - A \in ℝ$
51	50	adantr	$⊢ (A \in [- π, π] \land A < 0) \to - A \in ℝ$
52		simpr	$⊢ (A \in [- π, π] \land A < 0) \to A < 0$
53	13	adantr	$⊢ (A \in [- π, π] \land A < 0) \to A \in ℝ$
54	53	lt0neg1d	$⊢ (A \in [- π, π] \land A < 0) \to (A < 0 \leftrightarrow 0 < - A)$
55	52 54	mpbid	$⊢ (A \in [- π, π] \land A < 0) \to 0 < - A$
56	5	renegcli	$⊢ - 2 π \in ℝ$
57	56	a1i	$⊢ (A \in [- π, π] \land A < 0) \to - 2 π \in ℝ$
58	8	a1i	$⊢ (A \in [- π, π] \land A < 0) \to - π \in ℝ$
59	4 5	ltnegi	$⊢ π < 2 π \leftrightarrow - 2 π < - π$
60	23 59	mpbi	$⊢ - 2 π < - π$
61	60	a1i	$⊢ (A \in [- π, π] \land A < 0) \to - 2 π < - π$
62		iccgelb	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land A \in [- π, π]) \to - π \leq A$
63	17 18 11 62	syl3anc	$⊢ A \in [- π, π] \to - π \leq A$
64	63	adantr	$⊢ (A \in [- π, π] \land A < 0) \to - π \leq A$
65	57 58 53 61 64	ltletrd	$⊢ (A \in [- π, π] \land A < 0) \to - 2 π < A$
66	57 53	ltnegd	$⊢ (A \in [- π, π] \land A < 0) \to (- 2 π < A \leftrightarrow - A < - (- 2 π))$
67	65 66	mpbid	$⊢ (A \in [- π, π] \land A < 0) \to - A < - (- 2 π)$
68	16	recnd	$⊢ A \in [- π, π] \to 2 π \in ℂ$
69	68	negnegd	$⊢ A \in [- π, π] \to - (- 2 π) = 2 π$
70	69	adantr	$⊢ (A \in [- π, π] \land A < 0) \to - (- 2 π) = 2 π$
71	67 70	breqtrd	$⊢ (A \in [- π, π] \land A < 0) \to - A < 2 π$
72	48 49 51 55 71	eliood	$⊢ (A \in [- π, π] \land A < 0) \to - A \in (0, 2 π)$
73		sinaover2ne0	$⊢ - A \in (0, 2 π) \to \sin (\frac{- A}{2}) \neq 0$
74	72 73	syl	$⊢ (A \in [- π, π] \land A < 0) \to \sin (\frac{- A}{2}) \neq 0$
75	47 74	eqnetrd	$⊢ (A \in [- π, π] \land A < 0) \to - \sin (\frac{A}{2}) \neq 0$
76	75	neneqd	$⊢ (A \in [- π, π] \land A < 0) \to \neg - \sin (\frac{A}{2}) = 0$
77	38	sincld	$⊢ A \in [- π, π] \to \sin (\frac{A}{2}) \in ℂ$
78	77	adantr	$⊢ (A \in [- π, π] \land A < 0) \to \sin (\frac{A}{2}) \in ℂ$
79	78	negeq0d	$⊢ (A \in [- π, π] \land A < 0) \to (\sin (\frac{A}{2}) = 0 \leftrightarrow - \sin (\frac{A}{2}) = 0)$
80	76 79	mtbird	$⊢ (A \in [- π, π] \land A < 0) \to \neg \sin (\frac{A}{2}) = 0$
81	80	neqned	$⊢ (A \in [- π, π] \land A < 0) \to \sin (\frac{A}{2}) \neq 0$
82	31 36 81	syl2anc	$⊢ ((A \in [- π, π] \land A \neq 0) \land \neg 0 < A) \to \sin (\frac{A}{2}) \neq 0$
83	30 82	pm2.61dan	$⊢ (A \in [- π, π] \land A \neq 0) \to \sin (\frac{A}{2}) \neq 0$

Metamath Proof Explorer

Theorem fourierdlem44

Proof