Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem78 Structured version   Unicode version

Theorem fourierdlem78 31808
Description:  G is continuous when restricted on an interval not containing  0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem78.f  |-  ( ph  ->  F : RR --> RR )
fourierdlem78.a  |-  ( ph  ->  A  e.  ( -u pi [,] pi ) )
fourierdlem78.b  |-  ( ph  ->  B  e.  ( -u pi [,] pi ) )
fourierdlem78.x  |-  ( ph  ->  X  e.  RR )
fourierdlem78.nxelab  |-  ( ph  ->  -.  0  e.  ( A (,) B ) )
fourierdlem78.fcn  |-  ( ph  ->  ( F  |`  (
( A  +  X
) (,) ( B  +  X ) ) )  e.  ( ( ( A  +  X
) (,) ( B  +  X ) )
-cn-> CC ) )
fourierdlem78.y  |-  ( ph  ->  Y  e.  RR )
fourierdlem78.w  |-  ( ph  ->  W  e.  RR )
fourierdlem78.h  |-  H  =  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  / 
s ) ) )
fourierdlem78.k  |-  K  =  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )
fourierdlem78.u  |-  U  =  ( s  e.  (
-u pi [,] pi )  |->  ( ( H `
 s )  x.  ( K `  s
) ) )
fourierdlem78.n  |-  ( ph  ->  N  e.  RR )
fourierdlem78.s  |-  S  =  ( s  e.  (
-u pi [,] pi )  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  s ) ) )
fourierdlem78.g  |-  G  =  ( s  e.  (
-u pi [,] pi )  |->  ( ( U `
 s )  x.  ( S `  s
) ) )
Assertion
Ref Expression
fourierdlem78  |-  ( ph  ->  ( G  |`  ( A (,) B ) )  e.  ( ( A (,) B ) -cn-> RR ) )
Distinct variable groups:    A, s    B, s    F, s    N, s    W, s    X, s    Y, s    ph, s
Allowed substitution hints:    S( s)    U( s)    G( s)    H( s)    K( s)

Proof of Theorem fourierdlem78
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 fourierdlem78.g . . . . 5  |-  G  =  ( s  e.  (
-u pi [,] pi )  |->  ( ( U `
 s )  x.  ( S `  s
) ) )
21a1i 11 . . . 4  |-  ( ph  ->  G  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( U `  s )  x.  ( S `  s ) ) ) )
32reseq1d 5278 . . 3  |-  ( ph  ->  ( G  |`  ( A (,) B ) )  =  ( ( s  e.  ( -u pi [,] pi )  |->  ( ( U `  s )  x.  ( S `  s ) ) )  |`  ( A (,) B
) ) )
4 pire 22718 . . . . . . . . 9  |-  pi  e.  RR
54renegcli 9892 . . . . . . . 8  |-  -u pi  e.  RR
65a1i 11 . . . . . . 7  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  -u pi  e.  RR )
74a1i 11 . . . . . . 7  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  pi  e.  RR )
8 ioossre 11598 . . . . . . . . 9  |-  ( A (,) B )  C_  RR
98sseli 3505 . . . . . . . 8  |-  ( s  e.  ( A (,) B )  ->  s  e.  RR )
109adantl 466 . . . . . . 7  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  s  e.  RR )
115a1i 11 . . . . . . . . . . . 12  |-  ( ph  -> 
-u pi  e.  RR )
124a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  pi  e.  RR )
13 iccssre 11618 . . . . . . . . . . . 12  |-  ( (
-u pi  e.  RR  /\  pi  e.  RR )  ->  ( -u pi [,] pi )  C_  RR )
1411, 12, 13syl2anc 661 . . . . . . . . . . 11  |-  ( ph  ->  ( -u pi [,] pi )  C_  RR )
15 fourierdlem78.a . . . . . . . . . . 11  |-  ( ph  ->  A  e.  ( -u pi [,] pi ) )
1614, 15sseldd 3510 . . . . . . . . . 10  |-  ( ph  ->  A  e.  RR )
1716adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  A  e.  RR )
18 elicc2 11601 . . . . . . . . . . . . 13  |-  ( (
-u pi  e.  RR  /\  pi  e.  RR )  ->  ( A  e.  ( -u pi [,] pi )  <->  ( A  e.  RR  /\  -u pi  <_  A  /\  A  <_  pi ) ) )
195, 4, 18mp2an 672 . . . . . . . . . . . 12  |-  ( A  e.  ( -u pi [,] pi )  <->  ( A  e.  RR  /\  -u pi  <_  A  /\  A  <_  pi ) )
2019simp2bi 1012 . . . . . . . . . . 11  |-  ( A  e.  ( -u pi [,] pi )  ->  -u pi  <_  A )
2115, 20syl 16 . . . . . . . . . 10  |-  ( ph  -> 
-u pi  <_  A
)
2221adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  -u pi  <_  A )
2317rexrd 9655 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  A  e.  RR* )
24 fourierdlem78.b . . . . . . . . . . . . 13  |-  ( ph  ->  B  e.  ( -u pi [,] pi ) )
2514, 24sseldd 3510 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  RR )
2625rexrd 9655 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  RR* )
2726adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  B  e.  RR* )
28 simpr 461 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  s  e.  ( A (,) B ) )
29 ioogtlb 31415 . . . . . . . . . 10  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  s  e.  ( A (,) B
) )  ->  A  <  s )
3023, 27, 28, 29syl3anc 1228 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  A  <  s )
316, 17, 10, 22, 30lelttrd 9751 . . . . . . . 8  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  -u pi  <  s )
326, 10, 31ltled 9744 . . . . . . 7  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  -u pi  <_  s )
3325adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  B  e.  RR )
34 iooltub 31435 . . . . . . . . . 10  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  s  e.  ( A (,) B
) )  ->  s  <  B )
3523, 27, 28, 34syl3anc 1228 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  s  <  B )
36 elicc2 11601 . . . . . . . . . . . . 13  |-  ( (
-u pi  e.  RR  /\  pi  e.  RR )  ->  ( B  e.  ( -u pi [,] pi )  <->  ( B  e.  RR  /\  -u pi  <_  B  /\  B  <_  pi ) ) )
375, 4, 36mp2an 672 . . . . . . . . . . . 12  |-  ( B  e.  ( -u pi [,] pi )  <->  ( B  e.  RR  /\  -u pi  <_  B  /\  B  <_  pi ) )
3837simp3bi 1013 . . . . . . . . . . 11  |-  ( B  e.  ( -u pi [,] pi )  ->  B  <_  pi )
3924, 38syl 16 . . . . . . . . . 10  |-  ( ph  ->  B  <_  pi )
4039adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  B  <_  pi )
4110, 33, 7, 35, 40ltletrd 9753 . . . . . . . 8  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  s  <  pi )
4210, 7, 41ltled 9744 . . . . . . 7  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  s  <_  pi )
436, 7, 10, 32, 42eliccd 31425 . . . . . 6  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  s  e.  ( -u pi [,] pi ) )
4443ex 434 . . . . 5  |-  ( ph  ->  ( s  e.  ( A (,) B )  ->  s  e.  (
-u pi [,] pi ) ) )
4544ssrdv 3515 . . . 4  |-  ( ph  ->  ( A (,) B
)  C_  ( -u pi [,] pi ) )
46 resmpt 5329 . . . 4  |-  ( ( A (,) B ) 
C_  ( -u pi [,] pi )  ->  (
( s  e.  (
-u pi [,] pi )  |->  ( ( U `
 s )  x.  ( S `  s
) ) )  |`  ( A (,) B ) )  =  ( s  e.  ( A (,) B )  |->  ( ( U `  s )  x.  ( S `  s ) ) ) )
4745, 46syl 16 . . 3  |-  ( ph  ->  ( ( s  e.  ( -u pi [,] pi )  |->  ( ( U `  s )  x.  ( S `  s ) ) )  |`  ( A (,) B
) )  =  ( s  e.  ( A (,) B )  |->  ( ( U `  s
)  x.  ( S `
 s ) ) ) )
483, 47eqtrd 2508 . 2  |-  ( ph  ->  ( G  |`  ( A (,) B ) )  =  ( s  e.  ( A (,) B
)  |->  ( ( U `
 s )  x.  ( S `  s
) ) ) )
49 0re 9608 . . . . . . . . . . . 12  |-  0  e.  RR
5049a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  0  e.  RR )
51 fourierdlem78.f . . . . . . . . . . . . . . 15  |-  ( ph  ->  F : RR --> RR )
5251adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  F : RR
--> RR )
53 fourierdlem78.x . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  e.  RR )
5453adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  X  e.  RR )
5554, 10readdcld 9635 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( X  +  s )  e.  RR )
5652, 55ffvelrnd 6033 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( F `  ( X  +  s ) )  e.  RR )
57 fourierdlem78.y . . . . . . . . . . . . . . 15  |-  ( ph  ->  Y  e.  RR )
58 fourierdlem78.w . . . . . . . . . . . . . . 15  |-  ( ph  ->  W  e.  RR )
5957, 58ifcld 3988 . . . . . . . . . . . . . 14  |-  ( ph  ->  if ( 0  < 
s ,  Y ,  W )  e.  RR )
6059adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  if (
0  <  s ,  Y ,  W )  e.  RR )
6156, 60resubcld 9999 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  e.  RR )
62 simpl 457 . . . . . . . . . . . . . . . 16  |-  ( ( s  e.  ( A (,) B )  /\  s  =  0 )  ->  s  e.  ( A (,) B ) )
63 eleq1 2539 . . . . . . . . . . . . . . . . 17  |-  ( s  =  0  ->  (
s  e.  ( A (,) B )  <->  0  e.  ( A (,) B ) ) )
6463adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( s  e.  ( A (,) B )  /\  s  =  0 )  ->  ( s  e.  ( A (,) B
)  <->  0  e.  ( A (,) B ) ) )
6562, 64mpbid 210 . . . . . . . . . . . . . . 15  |-  ( ( s  e.  ( A (,) B )  /\  s  =  0 )  ->  0  e.  ( A (,) B ) )
6665adantll 713 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  s  e.  ( A (,) B
) )  /\  s  =  0 )  -> 
0  e.  ( A (,) B ) )
67 fourierdlem78.nxelab . . . . . . . . . . . . . . 15  |-  ( ph  ->  -.  0  e.  ( A (,) B ) )
6867ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  s  e.  ( A (,) B
) )  /\  s  =  0 )  ->  -.  0  e.  ( A (,) B ) )
6966, 68pm2.65da 576 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  -.  s  =  0 )
70 neqne 31339 . . . . . . . . . . . . 13  |-  ( -.  s  =  0  -> 
s  =/=  0 )
7169, 70syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  s  =/=  0 )
7261, 10, 71redivcld 10384 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( (
( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s )  e.  RR )
7350, 72ifcld 3988 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  if (
s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )  e.  RR )
74 fourierdlem78.h . . . . . . . . . . 11  |-  H  =  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  / 
s ) ) )
7574fvmpt2 5964 . . . . . . . . . 10  |-  ( ( s  e.  ( -u pi [,] pi )  /\  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )  e.  RR )  ->  ( H `  s )  =  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )
7643, 73, 75syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( H `  s )  =  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )
7776, 73eqeltrd 2555 . . . . . . . 8  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( H `  s )  e.  RR )
78 1re 9607 . . . . . . . . . . . 12  |-  1  e.  RR
7978a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  1  e.  RR )
80 2re 10617 . . . . . . . . . . . . . . 15  |-  2  e.  RR
8180a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  2  e.  RR )
82 rehalfcl 10777 . . . . . . . . . . . . . . . 16  |-  ( s  e.  RR  ->  (
s  /  2 )  e.  RR )
8310, 82syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( s  /  2 )  e.  RR )
84 resincl 13753 . . . . . . . . . . . . . . 15  |-  ( ( s  /  2 )  e.  RR  ->  ( sin `  ( s  / 
2 ) )  e.  RR )
8583, 84syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( sin `  ( s  /  2
) )  e.  RR )
8681, 85jca 532 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( 2  e.  RR  /\  ( sin `  ( s  / 
2 ) )  e.  RR ) )
87 remulcl 9589 . . . . . . . . . . . . 13  |-  ( ( 2  e.  RR  /\  ( sin `  ( s  /  2 ) )  e.  RR )  -> 
( 2  x.  ( sin `  ( s  / 
2 ) ) )  e.  RR )
8886, 87syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( 2  x.  ( sin `  (
s  /  2 ) ) )  e.  RR )
8981recnd 9634 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  2  e.  CC )
9085recnd 9634 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( sin `  ( s  /  2
) )  e.  CC )
91 2ne0 10640 . . . . . . . . . . . . . 14  |-  2  =/=  0
9291a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  2  =/=  0 )
93 fourierdlem44 31774 . . . . . . . . . . . . . 14  |-  ( ( s  e.  ( -u pi [,] pi )  /\  s  =/=  0 )  -> 
( sin `  (
s  /  2 ) )  =/=  0 )
9443, 71, 93syl2anc 661 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( sin `  ( s  /  2
) )  =/=  0
)
9589, 90, 92, 94mulne0d 10213 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( 2  x.  ( sin `  (
s  /  2 ) ) )  =/=  0
)
9610, 88, 95redivcld 10384 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) )  e.  RR )
9779, 96ifcld 3988 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  if (
s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )  e.  RR )
98 fourierdlem78.k . . . . . . . . . . 11  |-  K  =  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )
9998fvmpt2 5964 . . . . . . . . . 10  |-  ( ( s  e.  ( -u pi [,] pi )  /\  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )  e.  RR )  -> 
( K `  s
)  =  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
10043, 97, 99syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( K `  s )  =  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
101100, 97eqeltrd 2555 . . . . . . . 8  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( K `  s )  e.  RR )
10277, 101remulcld 9636 . . . . . . 7  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( ( H `  s )  x.  ( K `  s
) )  e.  RR )
103 fourierdlem78.u . . . . . . . 8  |-  U  =  ( s  e.  (
-u pi [,] pi )  |->  ( ( H `
 s )  x.  ( K `  s
) ) )
104103fvmpt2 5964 . . . . . . 7  |-  ( ( s  e.  ( -u pi [,] pi )  /\  ( ( H `  s )  x.  ( K `  s )
)  e.  RR )  ->  ( U `  s )  =  ( ( H `  s
)  x.  ( K `
 s ) ) )
10543, 102, 104syl2anc 661 . . . . . 6  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( U `  s )  =  ( ( H `  s
)  x.  ( K `
 s ) ) )
106105, 102eqeltrd 2555 . . . . 5  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( U `  s )  e.  RR )
107 fourierdlem78.n . . . . . . . . . . 11  |-  ( ph  ->  N  e.  RR )
108107adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  N  e.  RR )
10981, 92rereccld 10383 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( 1  /  2 )  e.  RR )
110108, 109readdcld 9635 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( N  +  ( 1  / 
2 ) )  e.  RR )
111110, 10remulcld 9636 . . . . . . . 8  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( ( N  +  ( 1  /  2 ) )  x.  s )  e.  RR )
112111resincld 13756 . . . . . . 7  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  s
) )  e.  RR )
113 fourierdlem78.s . . . . . . . 8  |-  S  =  ( s  e.  (
-u pi [,] pi )  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  s ) ) )
114113fvmpt2 5964 . . . . . . 7  |-  ( ( s  e.  ( -u pi [,] pi )  /\  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  s ) )  e.  RR )  -> 
( S `  s
)  =  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  s
) ) )
11543, 112, 114syl2anc 661 . . . . . 6  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( S `  s )  =  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  s ) ) )
116115, 112eqeltrd 2555 . . . . 5  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( S `  s )  e.  RR )
117106, 116remulcld 9636 . . . 4  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( ( U `  s )  x.  ( S `  s
) )  e.  RR )
118 eqid 2467 . . . 4  |-  ( s  e.  ( A (,) B )  |->  ( ( U `  s )  x.  ( S `  s ) ) )  =  ( s  e.  ( A (,) B
)  |->  ( ( U `
 s )  x.  ( S `  s
) ) )
119117, 118fmptd 6056 . . 3  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( ( U `  s )  x.  ( S `  s )
) ) : ( A (,) B ) --> RR )
120 ax-resscn 9561 . . . . 5  |-  RR  C_  CC
121120a1i 11 . . . 4  |-  ( ph  ->  RR  C_  CC )
122105mpteq2dva 4539 . . . . . 6  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( U `  s
) )  =  ( s  e.  ( A (,) B )  |->  ( ( H `  s
)  x.  ( K `
 s ) ) ) )
123 iffalse 3954 . . . . . . . . . . 11  |-  ( -.  s  =  0  ->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )  =  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )
12469, 123syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  if (
s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )  =  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )
125120, 61sseldi 3507 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  e.  CC )
126120, 10sseldi 3507 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  s  e.  CC )
127125, 126, 71divrecd 10335 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( (
( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s )  =  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  x.  ( 1  /  s
) ) )
12876, 124, 1273eqtrd 2512 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( H `  s )  =  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  x.  ( 1  /  s ) ) )
129128mpteq2dva 4539 . . . . . . . 8  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( H `  s
) )  =  ( s  e.  ( A (,) B )  |->  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  x.  ( 1  /  s ) ) ) )
130120, 56sseldi 3507 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
131120, 60sseldi 3507 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  if (
0  <  s ,  Y ,  W )  e.  CC )
132130, 131negsubd 9948 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( ( F `  ( X  +  s ) )  +  -u if ( 0  <  s ,  Y ,  W ) )  =  ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) ) )
133132eqcomd 2475 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  =  ( ( F `  ( X  +  s
) )  +  -u if ( 0  <  s ,  Y ,  W ) ) )
134133mpteq2dva 4539 . . . . . . . . . 10  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) ) )  =  ( s  e.  ( A (,) B )  |->  ( ( F `  ( X  +  s )
)  +  -u if ( 0  <  s ,  Y ,  W ) ) ) )
13516, 53readdcld 9635 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( A  +  X
)  e.  RR )
136135rexrd 9655 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A  +  X
)  e.  RR* )
137136adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( A  +  X )  e.  RR* )
13825, 53readdcld 9635 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( B  +  X
)  e.  RR )
139138rexrd 9655 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( B  +  X
)  e.  RR* )
140139adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( B  +  X )  e.  RR* )
141120, 16sseldi 3507 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  e.  CC )
142120, 53sseldi 3507 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  X  e.  CC )
143141, 142addcomd 9793 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( A  +  X
)  =  ( X  +  A ) )
144143adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( A  +  X )  =  ( X  +  A ) )
14517, 10, 54, 30ltadd2dd 9752 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( X  +  A )  <  ( X  +  s )
)
146144, 145eqbrtrd 4473 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( A  +  X )  <  ( X  +  s )
)
14710, 33, 54, 35ltadd2dd 9752 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( X  +  s )  < 
( X  +  B
) )
148120, 25sseldi 3507 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  B  e.  CC )
149142, 148addcomd 9793 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( X  +  B
)  =  ( B  +  X ) )
150149adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( X  +  B )  =  ( B  +  X ) )
151147, 150breqtrd 4477 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( X  +  s )  < 
( B  +  X
) )
152137, 140, 55, 146, 151eliood 31418 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( X  +  s )  e.  ( ( A  +  X ) (,) ( B  +  X )
) )
153 fvres 5886 . . . . . . . . . . . . . . 15  |-  ( ( X  +  s )  e.  ( ( A  +  X ) (,) ( B  +  X
) )  ->  (
( F  |`  (
( A  +  X
) (,) ( B  +  X ) ) ) `  ( X  +  s ) )  =  ( F `  ( X  +  s
) ) )
154152, 153syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( ( F  |`  ( ( A  +  X ) (,) ( B  +  X
) ) ) `  ( X  +  s
) )  =  ( F `  ( X  +  s ) ) )
155154eqcomd 2475 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( F `  ( X  +  s ) )  =  ( ( F  |`  (
( A  +  X
) (,) ( B  +  X ) ) ) `  ( X  +  s ) ) )
156155mpteq2dva 4539 . . . . . . . . . . . 12  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( F `  ( X  +  s )
) )  =  ( s  e.  ( A (,) B )  |->  ( ( F  |`  (
( A  +  X
) (,) ( B  +  X ) ) ) `  ( X  +  s ) ) ) )
157 ioosscn 31414 . . . . . . . . . . . . . 14  |-  ( ( A  +  X ) (,) ( B  +  X ) )  C_  CC
158157a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( A  +  X ) (,) ( B  +  X )
)  C_  CC )
159 fourierdlem78.fcn . . . . . . . . . . . . 13  |-  ( ph  ->  ( F  |`  (
( A  +  X
) (,) ( B  +  X ) ) )  e.  ( ( ( A  +  X
) (,) ( B  +  X ) )
-cn-> CC ) )
1608, 120sstri 3518 . . . . . . . . . . . . . 14  |-  ( A (,) B )  C_  CC
161160a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A (,) B
)  C_  CC )
162158, 159, 161, 142, 152fourierdlem23 31753 . . . . . . . . . . . 12  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( ( F  |`  ( ( A  +  X ) (,) ( B  +  X )
) ) `  ( X  +  s )
) )  e.  ( ( A (,) B
) -cn-> CC ) )
163156, 162eqeltrd 2555 . . . . . . . . . . 11  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( F `  ( X  +  s )
) )  e.  ( ( A (,) B
) -cn-> CC ) )
16449a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  0  <_  A )  /\  s  e.  ( A (,) B
) )  ->  0  e.  RR )
16517adantlr 714 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  0  <_  A )  /\  s  e.  ( A (,) B
) )  ->  A  e.  RR )
1669adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  0  <_  A )  /\  s  e.  ( A (,) B
) )  ->  s  e.  RR )
167 simplr 754 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  0  <_  A )  /\  s  e.  ( A (,) B
) )  ->  0  <_  A )
16830adantlr 714 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  0  <_  A )  /\  s  e.  ( A (,) B
) )  ->  A  <  s )
169164, 165, 166, 167, 168lelttrd 9751 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  0  <_  A )  /\  s  e.  ( A (,) B
) )  ->  0  <  s )
170169iftrued 3953 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  0  <_  A )  /\  s  e.  ( A (,) B
) )  ->  if ( 0  <  s ,  Y ,  W )  =  Y )
171170negeqd 9826 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  0  <_  A )  /\  s  e.  ( A (,) B
) )  ->  -u if ( 0  <  s ,  Y ,  W )  =  -u Y )
172171mpteq2dva 4539 . . . . . . . . . . . . 13  |-  ( (
ph  /\  0  <_  A )  ->  ( s  e.  ( A (,) B
)  |->  -u if ( 0  <  s ,  Y ,  W ) )  =  ( s  e.  ( A (,) B ) 
|->  -u Y ) )
173 eqid 2467 . . . . . . . . . . . . . . 15  |-  ( s  e.  CC  |->  -u Y
)  =  ( s  e.  CC  |->  -u Y
)
17457renegcld 9998 . . . . . . . . . . . . . . . . 17  |-  ( ph  -> 
-u Y  e.  RR )
175120, 174sseldi 3507 . . . . . . . . . . . . . . . 16  |-  ( ph  -> 
-u Y  e.  CC )
176 ssid 3528 . . . . . . . . . . . . . . . . . 18  |-  CC  C_  CC
177176a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( -u Y  e.  CC  ->  CC  C_  CC )
178 id 22 . . . . . . . . . . . . . . . . 17  |-  ( -u Y  e.  CC  ->  -u Y  e.  CC )
179177, 178, 177constcncfg 31532 . . . . . . . . . . . . . . . 16  |-  ( -u Y  e.  CC  ->  ( s  e.  CC  |->  -u Y )  e.  ( CC -cn-> CC ) )
180175, 179syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( s  e.  CC  |->  -u Y )  e.  ( CC -cn-> CC ) )
181176a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  CC  C_  CC )
18257adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  Y  e.  RR )
183182renegcld 9998 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  -u Y  e.  RR )
184120, 183sseldi 3507 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  -u Y  e.  CC )
185173, 180, 161, 181, 184cncfmptssg 31531 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  -u Y )  e.  ( ( A (,) B ) -cn-> CC ) )
186185adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  0  <_  A )  ->  ( s  e.  ( A (,) B
)  |->  -u Y )  e.  ( ( A (,) B ) -cn-> CC ) )
187172, 186eqeltrd 2555 . . . . . . . . . . . 12  |-  ( (
ph  /\  0  <_  A )  ->  ( s  e.  ( A (,) B
)  |->  -u if ( 0  <  s ,  Y ,  W ) )  e.  ( ( A (,) B ) -cn-> CC ) )
188 simpl 457 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  0  <_  A )  ->  ph )
18916rexrd 9655 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A  e.  RR* )
190189ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  -.  0  <_  A )  /\  -.  B  <_  0 )  ->  A  e.  RR* )
19126ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  -.  0  <_  A )  /\  -.  B  <_  0 )  ->  B  e.  RR* )
19249a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  -.  0  <_  A )  /\  -.  B  <_  0 )  ->  0  e.  RR )
193 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  -.  0  <_  A )  ->  -.  0  <_  A )
194188, 16syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  -.  0  <_  A )  ->  A  e.  RR )
19549a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  -.  0  <_  A )  ->  0  e.  RR )
196194, 195ltnled 9743 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  -.  0  <_  A )  ->  ( A  <  0  <->  -.  0  <_  A ) )
197193, 196mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  0  <_  A )  ->  A  <  0 )
198197adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  -.  0  <_  A )  /\  -.  B  <_  0 )  ->  A  <  0
)
199 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  -.  B  <_  0 )  ->  -.  B  <_  0 )
20049a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  -.  B  <_  0 )  ->  0  e.  RR )
20125adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  -.  B  <_  0 )  ->  B  e.  RR )
202200, 201ltnled 9743 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  -.  B  <_  0 )  ->  (
0  <  B  <->  -.  B  <_  0 ) )
203199, 202mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  B  <_  0 )  ->  0  <  B )
204203adantlr 714 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  -.  0  <_  A )  /\  -.  B  <_  0 )  ->  0  <  B
)
205190, 191, 192, 198, 204eliood 31418 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  -.  0  <_  A )  /\  -.  B  <_  0 )  ->  0  e.  ( A (,) B ) )
20667ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  -.  0  <_  A )  /\  -.  B  <_  0 )  ->  -.  0  e.  ( A (,) B ) )
207205, 206condan 792 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  0  <_  A )  ->  B  <_  0 )
208188, 207jca 532 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  0  <_  A )  ->  ( ph  /\  B  <_  0
) )
2099adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  B  <_  0 )  /\  s  e.  ( A (,) B
) )  ->  s  e.  RR )
21049a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  B  <_  0 )  /\  s  e.  ( A (,) B
) )  ->  0  e.  RR )
21133adantlr 714 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  B  <_  0 )  /\  s  e.  ( A (,) B
) )  ->  B  e.  RR )
21235adantlr 714 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  B  <_  0 )  /\  s  e.  ( A (,) B
) )  ->  s  <  B )
213 simplr 754 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  B  <_  0 )  /\  s  e.  ( A (,) B
) )  ->  B  <_  0 )
214209, 211, 210, 212, 213ltletrd 9753 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  B  <_  0 )  /\  s  e.  ( A (,) B
) )  ->  s  <  0 )
215209, 210, 214ltled 9744 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  B  <_  0 )  /\  s  e.  ( A (,) B
) )  ->  s  <_  0 )
216209, 210lenltd 9742 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  B  <_  0 )  /\  s  e.  ( A (,) B
) )  ->  (
s  <_  0  <->  -.  0  <  s ) )
217215, 216mpbid 210 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  B  <_  0 )  /\  s  e.  ( A (,) B
) )  ->  -.  0  <  s )
218217iffalsed 3956 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  B  <_  0 )  /\  s  e.  ( A (,) B
) )  ->  if ( 0  <  s ,  Y ,  W )  =  W )
219218negeqd 9826 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  B  <_  0 )  /\  s  e.  ( A (,) B
) )  ->  -u if ( 0  <  s ,  Y ,  W )  =  -u W )
220219mpteq2dva 4539 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  B  <_  0 )  ->  ( s  e.  ( A (,) B
)  |->  -u if ( 0  <  s ,  Y ,  W ) )  =  ( s  e.  ( A (,) B ) 
|->  -u W ) )
221 eqid 2467 . . . . . . . . . . . . . . . 16  |-  ( s  e.  CC  |->  -u W
)  =  ( s  e.  CC  |->  -u W
)
222120, 58sseldi 3507 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  W  e.  CC )
223222negcld 9929 . . . . . . . . . . . . . . . . 17  |-  ( ph  -> 
-u W  e.  CC )
224176a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( -u W  e.  CC  ->  CC  C_  CC )
225 id 22 . . . . . . . . . . . . . . . . . 18  |-  ( -u W  e.  CC  ->  -u W  e.  CC )
226224, 225, 224constcncfg 31532 . . . . . . . . . . . . . . . . 17  |-  ( -u W  e.  CC  ->  ( s  e.  CC  |->  -u W )  e.  ( CC -cn-> CC ) )
227223, 226syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( s  e.  CC  |->  -u W )  e.  ( CC -cn-> CC ) )
22858adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  W  e.  RR )
229228renegcld 9998 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  -u W  e.  RR )
230120, 229sseldi 3507 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  -u W  e.  CC )
231221, 227, 161, 181, 230cncfmptssg 31531 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  -u W )  e.  ( ( A (,) B ) -cn-> CC ) )
232231adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  B  <_  0 )  ->  ( s  e.  ( A (,) B
)  |->  -u W )  e.  ( ( A (,) B ) -cn-> CC ) )
233220, 232eqeltrd 2555 . . . . . . . . . . . . 13  |-  ( (
ph  /\  B  <_  0 )  ->  ( s  e.  ( A (,) B
)  |->  -u if ( 0  <  s ,  Y ,  W ) )  e.  ( ( A (,) B ) -cn-> CC ) )
234208, 233syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  0  <_  A )  ->  (
s  e.  ( A (,) B )  |->  -u if ( 0  <  s ,  Y ,  W ) )  e.  ( ( A (,) B )
-cn-> CC ) )
235187, 234pm2.61dan 789 . . . . . . . . . . 11  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  -u if ( 0  <  s ,  Y ,  W ) )  e.  ( ( A (,) B ) -cn-> CC ) )
236163, 235addcncf 31534 . . . . . . . . . 10  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( ( F `  ( X  +  s
) )  +  -u if ( 0  <  s ,  Y ,  W ) ) )  e.  ( ( A (,) B
) -cn-> CC ) )
237134, 236eqeltrd 2555 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) ) )  e.  ( ( A (,) B
) -cn-> CC ) )
238 eqid 2467 . . . . . . . . . 10  |-  ( s  e.  ( CC  \  { 0 } ) 
|->  ( 1  /  s
) )  =  ( s  e.  ( CC 
\  { 0 } )  |->  ( 1  / 
s ) )
239 ax-1cn 9562 . . . . . . . . . . . 12  |-  1  e.  CC
240239a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  1  e.  CC )
241238cdivcncf 21289 . . . . . . . . . . 11  |-  ( 1  e.  CC  ->  (
s  e.  ( CC 
\  { 0 } )  |->  ( 1  / 
s ) )  e.  ( ( CC  \  { 0 } )
-cn-> CC ) )
242240, 241syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( s  e.  ( CC  \  { 0 } )  |->  ( 1  /  s ) )  e.  ( ( CC 
\  { 0 } ) -cn-> CC ) )
243 elsn 4047 . . . . . . . . . . . . . 14  |-  ( s  e.  { 0 }  <-> 
s  =  0 )
24469, 243sylnibr 305 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  -.  s  e.  { 0 } )
245126, 244eldifd 3492 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  s  e.  ( CC  \  { 0 } ) )
246245ralrimiva 2881 . . . . . . . . . . 11  |-  ( ph  ->  A. s  e.  ( A (,) B ) s  e.  ( CC 
\  { 0 } ) )
247 dfss3 3499 . . . . . . . . . . 11  |-  ( ( A (,) B ) 
C_  ( CC  \  { 0 } )  <->  A. s  e.  ( A (,) B ) s  e.  ( CC  \  { 0 } ) )
248246, 247sylibr 212 . . . . . . . . . 10  |-  ( ph  ->  ( A (,) B
)  C_  ( CC  \  { 0 } ) )
24910, 71rereccld 10383 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( 1  /  s )  e.  RR )
250120, 249sseldi 3507 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( 1  /  s )  e.  CC )
251238, 242, 248, 181, 250cncfmptssg 31531 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( 1  /  s
) )  e.  ( ( A (,) B
) -cn-> CC ) )
252237, 251mulcncf 21727 . . . . . . . 8  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( ( ( F `
 ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  x.  ( 1  /  s ) ) )  e.  ( ( A (,) B )
-cn-> CC ) )
253129, 252eqeltrd 2555 . . . . . . 7  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( H `  s
) )  e.  ( ( A (,) B
) -cn-> CC ) )
254 iffalse 3954 . . . . . . . . . . 11  |-  ( -.  s  =  0  ->  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )  =  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) )
25569, 254syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  if (
s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )  =  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) )
256120, 88sseldi 3507 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( 2  x.  ( sin `  (
s  /  2 ) ) )  e.  CC )
257126, 256, 95divrecd 10335 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) )  =  ( s  x.  (
1  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
258100, 255, 2573eqtrd 2512 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( K `  s )  =  ( s  x.  ( 1  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
259258mpteq2dva 4539 . . . . . . . 8  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( K `  s
) )  =  ( s  e.  ( A (,) B )  |->  ( s  x.  ( 1  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) ) )
260255, 257eqtr2d 2509 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( s  x.  ( 1  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) )  =  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
261260mpteq2dva 4539 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( s  x.  (
1  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )  =  ( s  e.  ( A (,) B )  |->  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) ) )
262 eqid 2467 . . . . . . . . . 10  |-  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
263 cncfss 21271 . . . . . . . . . . . 12  |-  ( ( RR  C_  CC  /\  CC  C_  CC )  ->  (
( -u pi [,] pi ) -cn-> RR )  C_  (
( -u pi [,] pi ) -cn-> CC ) )
264120, 176, 263mp2an 672 . . . . . . . . . . 11  |-  ( (
-u pi [,] pi ) -cn-> RR )  C_  (
( -u pi [,] pi ) -cn-> CC )
265262fourierdlem62 31792 . . . . . . . . . . . 12  |-  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )  e.  ( (
-u pi [,] pi ) -cn-> RR )
266265a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )  e.  ( ( -u pi [,] pi ) -cn-> RR ) )
267264, 266sseldi 3507 . . . . . . . . . 10  |-  ( ph  ->  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )  e.  ( ( -u pi [,] pi ) -cn-> CC ) )
268120, 97sseldi 3507 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  if (
s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )  e.  CC )
269262, 267, 45, 181, 268cncfmptssg 31531 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  if ( s  =  0 ,  1 ,  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) ) )  e.  ( ( A (,) B
) -cn-> CC ) )
270261, 269eqeltrd 2555 . . . . . . . 8  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( s  x.  (
1  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )  e.  ( ( A (,) B )
-cn-> CC ) )
271259, 270eqeltrd 2555 . . . . . . 7  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( K `  s
) )  e.  ( ( A (,) B
) -cn-> CC ) )
272253, 271mulcncf 21727 . . . . . 6  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( ( H `  s )  x.  ( K `  s )
) )  e.  ( ( A (,) B
) -cn-> CC ) )
273122, 272eqeltrd 2555 . . . . 5  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( U `  s
) )  e.  ( ( A (,) B
) -cn-> CC ) )
274115mpteq2dva 4539 . . . . . 6  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( S `  s
) )  =  ( s  e.  ( A (,) B )  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  s ) ) ) )
275 sinf 13737 . . . . . . . . . 10  |-  sin : CC
--> CC
276275a1i 11 . . . . . . . . 9  |-  ( ph  ->  sin : CC --> CC )
277120, 111sseldi 3507 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A (,) B ) )  ->  ( ( N  +  ( 1  /  2 ) )  x.  s )  e.  CC )
278 eqid 2467 . . . . . . . . . 10  |-  ( s  e.  ( A (,) B )  |->  ( ( N  +  ( 1  /  2 ) )  x.  s ) )  =  ( s  e.  ( A (,) B
)  |->  ( ( N  +  ( 1  / 
2 ) )  x.  s ) )
279277, 278fmptd 6056 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( ( N  +  ( 1  /  2
) )  x.  s
) ) : ( A (,) B ) --> CC )
280 fcompt 6068 . . . . . . . . 9  |-  ( ( sin : CC --> CC  /\  ( s  e.  ( A (,) B ) 
|->  ( ( N  +  ( 1  /  2
) )  x.  s
) ) : ( A (,) B ) --> CC )  ->  ( sin  o.  ( s  e.  ( A (,) B
)  |->  ( ( N  +  ( 1  / 
2 ) )  x.  s ) ) )  =  ( x  e.  ( A (,) B
)  |->  ( sin `  (
( s  e.  ( A (,) B ) 
|->  ( ( N  +  ( 1  /  2
) )  x.  s
) ) `  x
) ) ) )
281276, 279, 280syl2anc 661 . . . . . . . 8  |-  ( ph  ->  ( sin  o.  (
s  e.  ( A (,) B )  |->  ( ( N  +  ( 1  /  2 ) )  x.  s ) ) )  =  ( x  e.  ( A (,) B )  |->  ( sin `  ( ( s  e.  ( A (,) B )  |->  ( ( N  +  ( 1  /  2 ) )  x.  s ) ) `  x ) ) ) )
282 eqidd 2468 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( s  e.  ( A (,) B
)  |->  ( ( N  +  ( 1  / 
2 ) )  x.  s ) )  =  ( s  e.  ( A (,) B ) 
|->  ( ( N  +  ( 1  /  2
) )  x.  s
) ) )
283 oveq2 6303 . . . . . . . . . . . 12  |-  ( s  =  x  ->  (
( N  +  ( 1  /  2 ) )  x.  s )  =  ( ( N  +  ( 1  / 
2 ) )  x.  x ) )
284283adantl 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( A (,) B
) )  /\  s  =  x )  ->  (
( N  +  ( 1  /  2 ) )  x.  s )  =  ( ( N  +  ( 1  / 
2 ) )  x.  x ) )
285 simpr 461 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  x  e.  ( A (,) B ) )
28678rehalfcli 10799 . . . . . . . . . . . . . . . 16  |-  ( 1  /  2 )  e.  RR
287286a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  /  2
)  e.  RR )
288107, 287jca 532 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( N  e.  RR  /\  ( 1  /  2
)  e.  RR ) )
289 readdcl 9587 . . . . . . . . . . . . . 14  |-  ( ( N  e.  RR  /\  ( 1  /  2
)  e.  RR )  ->  ( N  +  ( 1  /  2
) )  e.  RR )
290288, 289syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  +  ( 1  /  2 ) )  e.  RR )
291290adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( N  +  ( 1  / 
2 ) )  e.  RR )
2928, 285sseldi 3507 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  x  e.  RR )
293291, 292remulcld 9636 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( ( N  +  ( 1  /  2 ) )  x.  x )  e.  RR )
294282, 284, 285, 293fvmptd 5962 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( (
s  e.  ( A (,) B )  |->  ( ( N  +  ( 1  /  2 ) )  x.  s ) ) `  x )  =  ( ( N  +  ( 1  / 
2 ) )  x.  x ) )
295294fveq2d 5876 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( sin `  ( ( s  e.  ( A (,) B
)  |->  ( ( N  +  ( 1  / 
2 ) )  x.  s ) ) `  x ) )  =  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  x ) ) )
296295mpteq2dva 4539 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( A (,) B ) 
|->  ( sin `  (
( s  e.  ( A (,) B ) 
|->  ( ( N  +  ( 1  /  2
) )  x.  s
) ) `  x
) ) )  =  ( x  e.  ( A (,) B ) 
|->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  x ) ) ) )
297 oveq2 6303 . . . . . . . . . . 11  |-  ( x  =  s  ->  (
( N  +  ( 1  /  2 ) )  x.  x )  =  ( ( N  +  ( 1  / 
2 ) )  x.  s ) )
298297fveq2d 5876 . . . . . . . . . 10  |-  ( x  =  s  ->  ( sin `  ( ( N  +  ( 1  / 
2 ) )  x.  x ) )  =  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  s ) ) )
299298cbvmptv 4544 . . . . . . . . 9  |-  ( x  e.  ( A (,) B )  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  x
) ) )  =  ( s  e.  ( A (,) B ) 
|->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  s ) ) )
300299a1i 11 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( A (,) B ) 
|->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  x ) ) )  =  ( s  e.  ( A (,) B )  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  s ) ) ) )
301281, 296, 3003eqtrrd 2513 . . . . . . 7  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  s ) ) )  =  ( sin  o.  ( s  e.  ( A (,) B )  |->  ( ( N  +  ( 1  /  2 ) )  x.  s ) ) ) )
30280, 91rereccli 10321 . . . . . . . . . . . . 13  |-  ( 1  /  2 )  e.  RR
303302a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  /  2
)  e.  RR )
304107, 303readdcld 9635 . . . . . . . . . . 11  |-  ( ph  ->  ( N  +  ( 1  /  2 ) )  e.  RR )
305120, 304sseldi 3507 . . . . . . . . . 10  |-  ( ph  ->  ( N  +  ( 1  /  2 ) )  e.  CC )
306 cncfmptc 21283 . . . . . . . . . 10  |-  ( ( ( N  +  ( 1  /  2 ) )  e.  CC  /\  ( A (,) B ) 
C_  CC  /\  CC  C_  CC )  ->  ( s  e.  ( A (,) B )  |->  ( N  +  ( 1  / 
2 ) ) )  e.  ( ( A (,) B ) -cn-> CC ) )
307305, 161, 181, 306syl3anc 1228 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( N  +  ( 1  /  2 ) ) )  e.  ( ( A (,) B
) -cn-> CC ) )
308 cncfmptid 21284 . . . . . . . . . 10  |-  ( ( ( A (,) B
)  C_  CC  /\  CC  C_  CC )  ->  (
s  e.  ( A (,) B )  |->  s )  e.  ( ( A (,) B )
-cn-> CC ) )
309161, 181, 308syl2anc 661 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  s )  e.  ( ( A (,) B
) -cn-> CC ) )
310307, 309mulcncf 21727 . . . . . . . 8  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( ( N  +  ( 1  /  2
) )  x.  s
) )  e.  ( ( A (,) B
) -cn-> CC ) )
311 sincn 22706 . . . . . . . . 9  |-  sin  e.  ( CC -cn-> CC )
312311a1i 11 . . . . . . . 8  |-  ( ph  ->  sin  e.  ( CC
-cn-> CC ) )
313310, 312cncfco 21279 . . . . . . 7  |-  ( ph  ->  ( sin  o.  (
s  e.  ( A (,) B )  |->  ( ( N  +  ( 1  /  2 ) )  x.  s ) ) )  e.  ( ( A (,) B
) -cn-> CC ) )
314301, 313eqeltrd 2555 . . . . . 6  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  s ) ) )  e.  ( ( A (,) B
) -cn-> CC ) )
315274, 314eqeltrd 2555 . . . . 5  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( S `  s
) )  e.  ( ( A (,) B
) -cn-> CC ) )
316273, 315mulcncf 21727 . . . 4  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( ( U `  s )  x.  ( S `  s )
) )  e.  ( ( A (,) B
) -cn-> CC ) )
317 cncffvrn 21270 . . . 4  |-  ( ( RR  C_  CC  /\  (
s  e.  ( A (,) B )  |->  ( ( U `  s
)  x.  ( S `
 s ) ) )  e.  ( ( A (,) B )
-cn-> CC ) )  -> 
( ( s  e.  ( A (,) B
)  |->  ( ( U `
 s )  x.  ( S `  s
) ) )  e.  ( ( A (,) B ) -cn-> RR )  <-> 
( s  e.  ( A (,) B ) 
|->  ( ( U `  s )  x.  ( S `  s )
) ) : ( A (,) B ) --> RR ) )
318121, 316, 317syl2anc 661 . . 3  |-  ( ph  ->  ( ( s  e.  ( A (,) B
)  |->  ( ( U `
 s )  x.  ( S `  s
) ) )  e.  ( ( A (,) B ) -cn-> RR )  <-> 
( s  e.  ( A (,) B ) 
|->  ( ( U `  s )  x.  ( S `  s )
) ) : ( A (,) B ) --> RR ) )
319119, 318mpbird 232 . 2  |-  ( ph  ->  ( s  e.  ( A (,) B ) 
|->  ( ( U `  s )  x.  ( S `  s )
) )  e.  ( ( A (,) B
) -cn-> RR ) )
32048, 319eqeltrd 2555 1  |-  ( ph  ->  ( G  |`  ( A (,) B ) )  e.  ( ( A (,) B ) -cn-> RR ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 973    = wceq 1379    e. wcel 1767    =/= wne 2662   A.wral 2817    \ cdif 3478    C_ wss 3481   ifcif 3945   {csn 4033   class class class wbr 4453    |-> cmpt 4511    |` cres 5007    o. ccom 5009   -->wf 5590   ` cfv 5594  (class class class)co 6295   CCcc 9502   RRcr 9503   0cc0 9504   1c1 9505    + caddc 9507    x. cmul 9509   RR*cxr 9639    < clt 9640    <_ cle 9641    - cmin 9817   -ucneg 9818    / cdiv 10218   2c2 10597   (,)cioo 11541   [,]cicc 11544   sincsin 13678   picpi 13681   -cn->ccncf 21248
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-inf2 8070  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581  ax-pre-sup 9582  ax-addf 9583  ax-mulf 9584
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-iin 4334  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-se 4845  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-of 6535  df-om 6696  df-1st 6795  df-2nd 6796  df-supp 6914  df-recs 7054  df-rdg 7088  df-1o 7142  df-2o 7143  df-oadd 7146  df-er 7323  df-map 7434  df-pm 7435  df-ixp 7482  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-fsupp 7842  df-fi 7883  df-sup 7913  df-oi 7947  df-card 8332  df-cda 8560  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-div 10219  df-nn 10549  df-2 10606  df-3 10607  df-4 10608  df-5 10609  df-6 10610  df-7 10611  df-8 10612  df-9 10613  df-10 10614  df-n0 10808  df-z 10877  df-dec 10989  df-uz 11095  df-q 11195  df-rp 11233  df-xneg 11330  df-xadd 11331  df-xmul 11332  df-ioo 11545  df-ioc 11546  df-ico 11547  df-icc 11548  df-fz 11685  df-fzo 11805  df-fl 11909  df-mod 11977  df-seq 12088  df-exp 12147  df-fac 12334  df-bc 12361  df-hash 12386  df-shft 12880  df-cj 12912  df-re 12913  df-im 12914  df-sqrt 13048  df-abs 13049  df-limsup 13274  df-clim 13291  df-rlim 13292  df-sum 13489  df-ef 13682  df-sin 13684  df-cos 13685  df-pi 13687  df-struct 14509  df-ndx 14510  df-slot 14511  df-base 14512  df-sets 14513  df-ress 14514  df-plusg 14585  df-mulr 14586  df-starv 14587  df-sca 14588  df-vsca 14589  df-ip 14590  df-tset 14591  df-ple 14592  df-ds 14594  df-unif 14595  df-hom 14596  df-cco 14597  df-rest 14695  df-topn 14696  df-0g 14714  df-gsum 14715  df-topgen 14716  df-pt 14717  df-prds 14720  df-xrs 14774  df-qtop 14779  df-imas 14780  df-xps 14782  df-mre 14858  df-mrc 14859  df-acs 14861  df-mgm 15746  df-sgrp 15785  df-mnd 15795  df-submnd 15840  df-mulg 15932  df-cntz 16227  df-cmn 16673  df-psmet 18281  df-xmet 18282  df-met 18283  df-bl 18284  df-mopn 18285  df-fbas 18286  df-fg 18287  df-cnfld 18291  df-top 19268  df-bases 19270  df-topon 19271  df-topsp 19272  df-cld 19388  df-ntr 19389  df-cls 19390  df-nei 19467  df-lp 19505  df-perf 19506  df-cn 19596  df-cnp 19597  df-t1 19683  df-haus 19684  df-cmp 19755  df-tx 19931  df-hmeo 20124  df-fil 20215  df-fm 20307  df-flim 20308  df-flf 20309  df-xms 20691  df-ms 20692  df-tms 20693  df-cncf 21250  df-limc 22138  df-dv 22139
This theorem is referenced by:  fourierdlem88  31818
  Copyright terms: Public domain W3C validator