This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) ) ) )