Theorem fourierdlem29

Description: Explicit function value for K applied to A . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypothesis	fourierdlem29.1	$$⊢K=\left(s\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left(s=0,1,\frac{s}{2\sin \left(\frac{s}{2}\right)}\right)\right)$$
Assertion	fourierdlem29	$$⊢A\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\to K\left(A\right)=if\left(A=0,1,\frac{A}{2\sin \left(\frac{A}{2}\right)}\right)$$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem29.1	$$⊢K=\left(s\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left(s=0,1,\frac{s}{2\sin \left(\frac{s}{2}\right)}\right)\right)$$
2		eqeq1	$$⊢s=A\to \left(s=0\leftrightarrow A=0\right)$$
3		id	$$⊢s=A\to s=A$$
4		fvoveq1	$$⊢s=A\to \sin \left(\frac{s}{2}\right)=\sin \left(\frac{A}{2}\right)$$
5	4	oveq2d	$$⊢s=A\to 2\sin \left(\frac{s}{2}\right)=2\sin \left(\frac{A}{2}\right)$$
6	3 5	oveq12d	$$⊢s=A\to \frac{s}{2\sin \left(\frac{s}{2}\right)}=\frac{A}{2\sin \left(\frac{A}{2}\right)}$$
7	2 6	ifbieq2d	$$⊢s=A\to if\left(s=0,1,\frac{s}{2\sin \left(\frac{s}{2}\right)}\right)=if\left(A=0,1,\frac{A}{2\sin \left(\frac{A}{2}\right)}\right)$$
8		1ex	$$⊢1\in \mathrm{V}$$
9		ovex	$$⊢\frac{A}{2\sin \left(\frac{A}{2}\right)}\in \mathrm{V}$$
10	8 9	ifex	$$⊢if\left(A=0,1,\frac{A}{2\sin \left(\frac{A}{2}\right)}\right)\in \mathrm{V}$$
11	7 1 10	fvmpt	$$⊢A\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\to K\left(A\right)=if\left(A=0,1,\frac{A}{2\sin \left(\frac{A}{2}\right)}\right)$$