Metamath Proof Explorer

Theorem fourierdlem43

Description: K is a real function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis fourierdlem43.1 ⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
Assertion fourierdlem43 𝐾 : ( - π [,] π ) ⟶ ℝ

Proof

Step Hyp Ref Expression
1 fourierdlem43.1 ⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
2 1red ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ 𝑠 = 0 ) → 1 ∈ ℝ )
3 pire ⊢ π ∈ ℝ
4 3 a1i ⊢ ( 𝑠 ∈ ( - π [,] π ) → π ∈ ℝ )
5 4 renegcld ⊢ ( 𝑠 ∈ ( - π [,] π ) → - π ∈ ℝ )
6 id ⊢ ( 𝑠 ∈ ( - π [,] π ) → 𝑠 ∈ ( - π [,] π ) )
7 eliccre ⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝑠 ∈ ℝ )
8 5 4 6 7 syl3anc ⊢ ( 𝑠 ∈ ( - π [,] π ) → 𝑠 ∈ ℝ )
9 8 adantr ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → 𝑠 ∈ ℝ )
10 2re ⊢ 2 ∈ ℝ
11 10 a1i ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → 2 ∈ ℝ )
12 9 rehalfcld ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → ( 𝑠 / 2 ) ∈ ℝ )
13 12 resincld ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℝ )
14 11 13 remulcld ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℝ )
15 2cnd ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → 2 ∈ ℂ )
16 13 recnd ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
17 2ne0 ⊢ 2 ≠ 0
18 17 a1i ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → 2 ≠ 0 )
19 0xr ⊢ 0 ∈ ℝ*
20 19 a1i ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ 0 < 𝑠 ) → 0 ∈ ℝ* )
21 10 3 remulcli ⊢ ( 2 · π ) ∈ ℝ
22 21 rexri ⊢ ( 2 · π ) ∈ ℝ*
23 22 a1i ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ 0 < 𝑠 ) → ( 2 · π ) ∈ ℝ* )
24 8 adantr ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ 0 < 𝑠 ) → 𝑠 ∈ ℝ )
25 simpr ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ 0 < 𝑠 ) → 0 < 𝑠 )
26 21 a1i ⊢ ( 𝑠 ∈ ( - π [,] π ) → ( 2 · π ) ∈ ℝ )
27 5 rexrd ⊢ ( 𝑠 ∈ ( - π [,] π ) → - π ∈ ℝ* )
28 4 rexrd ⊢ ( 𝑠 ∈ ( - π [,] π ) → π ∈ ℝ* )
29 iccleub ⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝑠 ≤ π )
30 27 28 6 29 syl3anc ⊢ ( 𝑠 ∈ ( - π [,] π ) → 𝑠 ≤ π )
31 pirp ⊢ π ∈ ℝ+
32 2timesgt ⊢ ( π ∈ ℝ+ → π < ( 2 · π ) )
33 31 32 ax-mp ⊢ π < ( 2 · π )
34 33 a1i ⊢ ( 𝑠 ∈ ( - π [,] π ) → π < ( 2 · π ) )
35 8 4 26 30 34 lelttrd ⊢ ( 𝑠 ∈ ( - π [,] π ) → 𝑠 < ( 2 · π ) )
36 35 adantr ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ 0 < 𝑠 ) → 𝑠 < ( 2 · π ) )
37 20 23 24 25 36 eliood ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ 0 < 𝑠 ) → 𝑠 ∈ ( 0 (,) ( 2 · π ) ) )
38 sinaover2ne0 ⊢ ( 𝑠 ∈ ( 0 (,) ( 2 · π ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
39 37 38 syl ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ 0 < 𝑠 ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
40 39 adantlr ⊢ ( ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) ∧ 0 < 𝑠 ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
41 8 ad2antrr ⊢ ( ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) ∧ ¬ 0 < 𝑠 ) → 𝑠 ∈ ℝ )
42 iccgelb ⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝑠 ∈ ( - π [,] π ) ) → - π ≤ 𝑠 )
43 27 28 6 42 syl3anc ⊢ ( 𝑠 ∈ ( - π [,] π ) → - π ≤ 𝑠 )
44 43 ad2antrr ⊢ ( ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) ∧ ¬ 0 < 𝑠 ) → - π ≤ 𝑠 )
45 0red ⊢ ( ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) ∧ ¬ 0 < 𝑠 ) → 0 ∈ ℝ )
46 neqne ⊢ ( ¬ 𝑠 = 0 → 𝑠 ≠ 0 )
47 46 ad2antlr ⊢ ( ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) ∧ ¬ 0 < 𝑠 ) → 𝑠 ≠ 0 )
48 simpr ⊢ ( ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) ∧ ¬ 0 < 𝑠 ) → ¬ 0 < 𝑠 )
49 41 45 47 48 lttri5d ⊢ ( ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) ∧ ¬ 0 < 𝑠 ) → 𝑠 < 0 )
50 5 ad2antrr ⊢ ( ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) ∧ ¬ 0 < 𝑠 ) → - π ∈ ℝ )
51 elico2 ⊢ ( ( - π ∈ ℝ ∧ 0 ∈ ℝ* ) → ( 𝑠 ∈ ( - π [,) 0 ) ↔ ( 𝑠 ∈ ℝ ∧ - π ≤ 𝑠 ∧ 𝑠 < 0 ) ) )
52 50 19 51 sylancl ⊢ ( ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) ∧ ¬ 0 < 𝑠 ) → ( 𝑠 ∈ ( - π [,) 0 ) ↔ ( 𝑠 ∈ ℝ ∧ - π ≤ 𝑠 ∧ 𝑠 < 0 ) ) )
53 41 44 49 52 mpbir3and ⊢ ( ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) ∧ ¬ 0 < 𝑠 ) → 𝑠 ∈ ( - π [,) 0 ) )
54 3 renegcli ⊢ - π ∈ ℝ
55 elicore ⊢ ( ( - π ∈ ℝ ∧ 𝑠 ∈ ( - π [,) 0 ) ) → 𝑠 ∈ ℝ )
56 54 55 mpan ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → 𝑠 ∈ ℝ )
57 56 recnd ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → 𝑠 ∈ ℂ )
58 2cnd ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → 2 ∈ ℂ )
59 17 a1i ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → 2 ≠ 0 )
60 57 58 59 divnegd ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → - ( 𝑠 / 2 ) = ( - 𝑠 / 2 ) )
61 60 eqcomd ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → ( - 𝑠 / 2 ) = - ( 𝑠 / 2 ) )
62 61 fveq2d ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → ( sin ‘ ( - 𝑠 / 2 ) ) = ( sin ‘ - ( 𝑠 / 2 ) ) )
63 62 negeqd ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → - ( sin ‘ ( - 𝑠 / 2 ) ) = - ( sin ‘ - ( 𝑠 / 2 ) ) )
64 57 halfcld ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → ( 𝑠 / 2 ) ∈ ℂ )
65 sinneg ⊢ ( ( 𝑠 / 2 ) ∈ ℂ → ( sin ‘ - ( 𝑠 / 2 ) ) = - ( sin ‘ ( 𝑠 / 2 ) ) )
66 64 65 syl ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → ( sin ‘ - ( 𝑠 / 2 ) ) = - ( sin ‘ ( 𝑠 / 2 ) ) )
67 66 negeqd ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → - ( sin ‘ - ( 𝑠 / 2 ) ) = - - ( sin ‘ ( 𝑠 / 2 ) ) )
68 64 sincld ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
69 68 negnegd ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → - - ( sin ‘ ( 𝑠 / 2 ) ) = ( sin ‘ ( 𝑠 / 2 ) ) )
70 63 67 69 3eqtrd ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → - ( sin ‘ ( - 𝑠 / 2 ) ) = ( sin ‘ ( 𝑠 / 2 ) ) )
71 57 negcld ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → - 𝑠 ∈ ℂ )
72 71 halfcld ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → ( - 𝑠 / 2 ) ∈ ℂ )
73 72 sincld ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → ( sin ‘ ( - 𝑠 / 2 ) ) ∈ ℂ )
74 19 a1i ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → 0 ∈ ℝ* )
75 22 a1i ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → ( 2 · π ) ∈ ℝ* )
76 56 renegcld ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → - 𝑠 ∈ ℝ )
77 54 a1i ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → - π ∈ ℝ )
78 77 rexrd ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → - π ∈ ℝ* )
79 id ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → 𝑠 ∈ ( - π [,) 0 ) )
80 icoltub ⊢ ( ( - π ∈ ℝ* ∧ 0 ∈ ℝ* ∧ 𝑠 ∈ ( - π [,) 0 ) ) → 𝑠 < 0 )
81 78 74 79 80 syl3anc ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → 𝑠 < 0 )
82 56 lt0neg1d ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → ( 𝑠 < 0 ↔ 0 < - 𝑠 ) )
83 81 82 mpbid ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → 0 < - 𝑠 )
84 3 a1i ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → π ∈ ℝ )
85 21 a1i ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → ( 2 · π ) ∈ ℝ )
86 icogelb ⊢ ( ( - π ∈ ℝ* ∧ 0 ∈ ℝ* ∧ 𝑠 ∈ ( - π [,) 0 ) ) → - π ≤ 𝑠 )
87 78 74 79 86 syl3anc ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → - π ≤ 𝑠 )
88 84 56 87 lenegcon1d ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → - 𝑠 ≤ π )
89 33 a1i ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → π < ( 2 · π ) )
90 76 84 85 88 89 lelttrd ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → - 𝑠 < ( 2 · π ) )
91 74 75 76 83 90 eliood ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → - 𝑠 ∈ ( 0 (,) ( 2 · π ) ) )
92 sinaover2ne0 ⊢ ( - 𝑠 ∈ ( 0 (,) ( 2 · π ) ) → ( sin ‘ ( - 𝑠 / 2 ) ) ≠ 0 )
93 91 92 syl ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → ( sin ‘ ( - 𝑠 / 2 ) ) ≠ 0 )
94 73 93 negne0d ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → - ( sin ‘ ( - 𝑠 / 2 ) ) ≠ 0 )
95 70 94 eqnetrrd ⊢ ( 𝑠 ∈ ( - π [,) 0 ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
96 53 95 syl ⊢ ( ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) ∧ ¬ 0 < 𝑠 ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
97 40 96 pm2.61dan ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
98 15 16 18 97 mulne0d ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ≠ 0 )
99 9 14 98 redivcld ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ℝ )
100 2 99 ifclda ⊢ ( 𝑠 ∈ ( - π [,] π ) → if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ℝ )
101 1 100 fmpti ⊢ 𝐾 : ( - π [,] π ) ⟶ ℝ