This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )