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	⊢ 𝐾 : ( - π [,] π ) ⟶ ℝ