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

Metamath Proof Explorer

Theorem fourierdlem9

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

Ref Expression
Hypotheses fourierdlem9.f 
|- ( ph -> F : RR --> RR )
fourierdlem9.x 
|- ( ph -> X e. RR )
fourierdlem9.r 
|- ( ph -> Y e. RR )
fourierdlem9.w 
|- ( ph -> W e. RR )
fourierdlem9.h 
|- H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
Assertion fourierdlem9 
|- ( ph -> H : ( -u _pi [,] _pi ) --> RR )

Proof

Step Hyp Ref Expression
1 fourierdlem9.f 
 |-  ( ph -> F : RR --> RR )
2 fourierdlem9.x 
 |-  ( ph -> X e. RR )
3 fourierdlem9.r 
 |-  ( ph -> Y e. RR )
4 fourierdlem9.w 
 |-  ( ph -> W e. RR )
5 fourierdlem9.h 
 |-  H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
6 0red 
 |-  ( ( ( ph /\ s e. ( -u _pi [,] _pi ) ) /\ s = 0 ) -> 0 e. RR )
7 1 adantr 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> F : RR --> RR )
8 2 adantr 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> X e. RR )
9 pire 
 |-  _pi e. RR
10 9 renegcli 
 |-  -u _pi e. RR
11 iccssre 
 |-  ( ( -u _pi e. RR /\ _pi e. RR ) -> ( -u _pi [,] _pi ) C_ RR )
12 10 9 11 mp2an 
 |-  ( -u _pi [,] _pi ) C_ RR
13 12 sseli 
 |-  ( s e. ( -u _pi [,] _pi ) -> s e. RR )
14 13 adantl 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> s e. RR )
15 8 14 readdcld 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( X + s ) e. RR )
16 7 15 ffvelcdmd 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( F ` ( X + s ) ) e. RR )
17 16 adantr 
 |-  ( ( ( ph /\ s e. ( -u _pi [,] _pi ) ) /\ -. s = 0 ) -> ( F ` ( X + s ) ) e. RR )
18 3 4 ifcld 
 |-  ( ph -> if ( 0 < s , Y , W ) e. RR )
19 18 ad2antrr 
 |-  ( ( ( ph /\ s e. ( -u _pi [,] _pi ) ) /\ -. s = 0 ) -> if ( 0 < s , Y , W ) e. RR )
20 17 19 resubcld 
 |-  ( ( ( ph /\ s e. ( -u _pi [,] _pi ) ) /\ -. s = 0 ) -> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) e. RR )
21 14 adantr 
 |-  ( ( ( ph /\ s e. ( -u _pi [,] _pi ) ) /\ -. s = 0 ) -> s e. RR )
22 neqne 
 |-  ( -. s = 0 -> s =/= 0 )
23 22 adantl 
 |-  ( ( ( ph /\ s e. ( -u _pi [,] _pi ) ) /\ -. s = 0 ) -> s =/= 0 )
24 20 21 23 redivcld 
 |-  ( ( ( ph /\ s e. ( -u _pi [,] _pi ) ) /\ -. s = 0 ) -> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) e. RR )
25 6 24 ifclda 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) e. RR )
26 25 5 fmptd 
 |-  ( ph -> H : ( -u _pi [,] _pi ) --> RR )