Metamath Proof Explorer

Theorem fourierdlem38

Description: The function F is continuous on every interval induced by the partition Q . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem38.cn 
|- ( ph -> F e. ( dom F -cn-> CC ) )
fourierdlem38.p 
|- P = ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` n ) = _pi ) /\ A. i e. ( 0 ..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem38.m 
|- ( ph -> M e. NN )
fourierdlem38.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem38.h 
|- H = ( A u. ( ( -u _pi [,] _pi ) \ dom F ) )
fourierdlem38.ranq 
|- ( ph -> ran Q = H )
Assertion fourierdlem38 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 fourierdlem38.cn 
 |-  ( ph -> F e. ( dom F -cn-> CC ) )
2 fourierdlem38.p 
 |-  P = ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` n ) = _pi ) /\ A. i e. ( 0 ..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
3 fourierdlem38.m 
 |-  ( ph -> M e. NN )
4 fourierdlem38.q 
 |-  ( ph -> Q e. ( P ` M ) )
5 fourierdlem38.h 
 |-  H = ( A u. ( ( -u _pi [,] _pi ) \ dom F ) )
6 fourierdlem38.ranq 
 |-  ( ph -> ran Q = H )
7 simplr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ -. x e. dom F ) -> x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
8 simplll 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ -. x e. dom F ) -> ph )
9 ioossicc 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
10 pire 
 |-  _pi e. RR
11 10 renegcli 
 |-  -u _pi e. RR
12 11 rexri 
 |-  -u _pi e. RR*
13 12 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> -u _pi e. RR* )
14 10 rexri 
 |-  _pi e. RR*
15 14 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> _pi e. RR* )
16 2 3 4 fourierdlem15 
 |-  ( ph -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) )
17 16 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) )
18 simpr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ..^ M ) )
19 13 15 17 18 fourierdlem8 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
20 9 19 sstrid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
21 20 sselda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x e. ( -u _pi [,] _pi ) )
22 21 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ -. x e. dom F ) -> x e. ( -u _pi [,] _pi ) )
23 simpr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ -. x e. dom F ) -> -. x e. dom F )
24 simpllr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ -. x e. dom F ) -> i e. ( 0 ..^ M ) )
25 3 3ad2ant1 
 |-  ( ( ph /\ x e. ( -u _pi [,] _pi ) /\ -. x e. dom F ) -> M e. NN )
26 4 3ad2ant1 
 |-  ( ( ph /\ x e. ( -u _pi [,] _pi ) /\ -. x e. dom F ) -> Q e. ( P ` M ) )
27 simp2 
 |-  ( ( ph /\ x e. ( -u _pi [,] _pi ) /\ -. x e. dom F ) -> x e. ( -u _pi [,] _pi ) )
28 simp3 
 |-  ( ( ph /\ x e. ( -u _pi [,] _pi ) /\ -. x e. dom F ) -> -. x e. dom F )
29 27 28 eldifd 
 |-  ( ( ph /\ x e. ( -u _pi [,] _pi ) /\ -. x e. dom F ) -> x e. ( ( -u _pi [,] _pi ) \ dom F ) )
30 elun2 
 |-  ( x e. ( ( -u _pi [,] _pi ) \ dom F ) -> x e. ( A u. ( ( -u _pi [,] _pi ) \ dom F ) ) )
31 29 30 syl 
 |-  ( ( ph /\ x e. ( -u _pi [,] _pi ) /\ -. x e. dom F ) -> x e. ( A u. ( ( -u _pi [,] _pi ) \ dom F ) ) )
32 6 5 eqtr2di 
 |-  ( ph -> ( A u. ( ( -u _pi [,] _pi ) \ dom F ) ) = ran Q )
33 32 3ad2ant1 
 |-  ( ( ph /\ x e. ( -u _pi [,] _pi ) /\ -. x e. dom F ) -> ( A u. ( ( -u _pi [,] _pi ) \ dom F ) ) = ran Q )
34 31 33 eleqtrd 
 |-  ( ( ph /\ x e. ( -u _pi [,] _pi ) /\ -. x e. dom F ) -> x e. ran Q )
35 2 25 26 34 fourierdlem12 
 |-  ( ( ( ph /\ x e. ( -u _pi [,] _pi ) /\ -. x e. dom F ) /\ i e. ( 0 ..^ M ) ) -> -. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
36 8 22 23 24 35 syl31anc 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ -. x e. dom F ) -> -. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
37 7 36 condan 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x e. dom F )
38 37 ralrimiva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x e. dom F )
39 dfss3 
 |-  ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F <-> A. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x e. dom F )
40 38 39 sylibr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
41 1 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> F e. ( dom F -cn-> CC ) )
42 rescncf 
 |-  ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F -> ( F e. ( dom F -cn-> CC ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) ) )
43 40 41 42 sylc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )