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 
|- K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
Assertion fourierdlem29 
|- ( A e. ( -u _pi [,] _pi ) -> ( K ` A ) = if ( A = 0 , 1 , ( A / ( 2 x. ( sin ` ( A / 2 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem29.1 
 |-  K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
2 eqeq1 
 |-  ( s = A -> ( s = 0 <-> A = 0 ) )
3 id 
 |-  ( s = A -> s = A )
4 fvoveq1 
 |-  ( s = A -> ( sin ` ( s / 2 ) ) = ( sin ` ( A / 2 ) ) )
5 4 oveq2d 
 |-  ( s = A -> ( 2 x. ( sin ` ( s / 2 ) ) ) = ( 2 x. ( sin ` ( A / 2 ) ) ) )
6 3 5 oveq12d 
 |-  ( s = A -> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( A / ( 2 x. ( sin ` ( A / 2 ) ) ) ) )
7 2 6 ifbieq2d 
 |-  ( s = A -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = if ( A = 0 , 1 , ( A / ( 2 x. ( sin ` ( A / 2 ) ) ) ) ) )
8 1ex 
 |-  1 e. _V
9 ovex 
 |-  ( A / ( 2 x. ( sin ` ( A / 2 ) ) ) ) e. _V
10 8 9 ifex 
 |-  if ( A = 0 , 1 , ( A / ( 2 x. ( sin ` ( A / 2 ) ) ) ) ) e. _V
11 7 1 10 fvmpt 
 |-  ( A e. ( -u _pi [,] _pi ) -> ( K ` A ) = if ( A = 0 , 1 , ( A / ( 2 x. ( sin ` ( A / 2 ) ) ) ) ) )