Theorem fourierdlem44

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

	Ref	Expression
Assertion	fourierdlem44	⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 ≠ 0 ) → ( sin ‘ ( 𝐴 / 2 ) ) ≠ 0 )

Proof

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