Theorem fourierdlem29

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

	Ref	Expression
Hypothesis	fourierdlem29.1	⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
Assertion	fourierdlem29	⊢ ( 𝐴 ∈ ( - π [,] π ) → ( 𝐾 ‘ 𝐴 ) = if ( 𝐴 = 0 , 1 , ( 𝐴 / ( 2 · ( sin ‘ ( 𝐴 / 2 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem29.1	⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
2		eqeq1	⊢ ( 𝑠 = 𝐴 → ( 𝑠 = 0 ↔ 𝐴 = 0 ) )
3		id	⊢ ( 𝑠 = 𝐴 → 𝑠 = 𝐴 )
4		fvoveq1	⊢ ( 𝑠 = 𝐴 → ( sin ‘ ( 𝑠 / 2 ) ) = ( sin ‘ ( 𝐴 / 2 ) ) )
5	4	oveq2d	⊢ ( 𝑠 = 𝐴 → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) = ( 2 · ( sin ‘ ( 𝐴 / 2 ) ) ) )
6	3 5	oveq12d	⊢ ( 𝑠 = 𝐴 → ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( 𝐴 / ( 2 · ( sin ‘ ( 𝐴 / 2 ) ) ) ) )
7	2 6	ifbieq2d	⊢ ( 𝑠 = 𝐴 → if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = if ( 𝐴 = 0 , 1 , ( 𝐴 / ( 2 · ( sin ‘ ( 𝐴 / 2 ) ) ) ) ) )
8		1ex	⊢ 1 ∈ V
9		ovex	⊢ ( 𝐴 / ( 2 · ( sin ‘ ( 𝐴 / 2 ) ) ) ) ∈ V
10	8 9	ifex	⊢ if ( 𝐴 = 0 , 1 , ( 𝐴 / ( 2 · ( sin ‘ ( 𝐴 / 2 ) ) ) ) ) ∈ V
11	7 1 10	fvmpt	⊢ ( 𝐴 ∈ ( - π [,] π ) → ( 𝐾 ‘ 𝐴 ) = if ( 𝐴 = 0 , 1 , ( 𝐴 / ( 2 · ( sin ‘ ( 𝐴 / 2 ) ) ) ) ) )