fourierdlem43

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

		Ref	Expression
	Hypothesis	fourierdlem43.1	$⊢ K = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
	Assertion	fourierdlem43	$⊢ K : [- π, π] ⟶ ℝ$

Proof

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

Metamath Proof Explorer

Theorem fourierdlem43

Proof