Metamath Proof Explorer

Theorem fourierdlem69

Description: A piecewise continuous function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem69.p 
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem69.m 
|- ( ph -> M e. NN )
fourierdlem69.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem69.f 
|- ( ph -> F : ( A [,] B ) --> CC )
fourierdlem69.fcn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem69.r 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
fourierdlem69.l 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
Assertion fourierdlem69 
|- ( ph -> F e. L^1 )

Proof

Step Hyp Ref Expression
1 fourierdlem69.p 
 |-  P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
2 fourierdlem69.m 
 |-  ( ph -> M e. NN )
3 fourierdlem69.q 
 |-  ( ph -> Q e. ( P ` M ) )
4 fourierdlem69.f 
 |-  ( ph -> F : ( A [,] B ) --> CC )
5 fourierdlem69.fcn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
6 fourierdlem69.r 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
7 fourierdlem69.l 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
8 1 fourierdlem2 
 |-  ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
9 2 8 syl 
 |-  ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
10 3 9 mpbid 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
11 10 simprd 
 |-  ( ph -> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
12 11 simpld 
 |-  ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
13 12 simpld 
 |-  ( ph -> ( Q ` 0 ) = A )
14 12 simprd 
 |-  ( ph -> ( Q ` M ) = B )
15 13 14 oveq12d 
 |-  ( ph -> ( ( Q ` 0 ) [,] ( Q ` M ) ) = ( A [,] B ) )
16 15 feq2d 
 |-  ( ph -> ( F : ( ( Q ` 0 ) [,] ( Q ` M ) ) --> CC <-> F : ( A [,] B ) --> CC ) )
17 4 16 mpbird 
 |-  ( ph -> F : ( ( Q ` 0 ) [,] ( Q ` M ) ) --> CC )
18 17 feqmptd 
 |-  ( ph -> F = ( x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) |-> ( F ` x ) ) )
19 nfv 
 |-  F/ x ph
20 0zd 
 |-  ( ph -> 0 e. ZZ )
21 nnuz 
 |-  NN = ( ZZ>= ` 1 )
22 1e0p1 
 |-  1 = ( 0 + 1 )
23 22 fveq2i 
 |-  ( ZZ>= ` 1 ) = ( ZZ>= ` ( 0 + 1 ) )
24 21 23 eqtri 
 |-  NN = ( ZZ>= ` ( 0 + 1 ) )
25 2 24 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` ( 0 + 1 ) ) )
26 10 simpld 
 |-  ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
27 elmapi 
 |-  ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
28 26 27 syl 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
29 28 ffvelrnda 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
30 11 simprd 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
31 30 r19.21bi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
32 4 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> F : ( A [,] B ) --> CC )
33 simpr 
 |-  ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
34 13 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( Q ` 0 ) = A )
35 14 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( Q ` M ) = B )
36 34 35 oveq12d 
 |-  ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( ( Q ` 0 ) [,] ( Q ` M ) ) = ( A [,] B ) )
37 33 36 eleqtrd 
 |-  ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> x e. ( A [,] B ) )
38 32 37 ffvelrnd 
 |-  ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( F ` x ) e. CC )
39 28 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
40 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
41 40 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
42 39 41 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
43 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
44 43 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
45 39 44 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
46 4 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> F : ( A [,] B ) --> CC )
47 ioossicc 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
48 1 2 3 fourierdlem11 
 |-  ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )
49 48 simp1d 
 |-  ( ph -> A e. RR )
50 49 rexrd 
 |-  ( ph -> A e. RR* )
51 50 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A e. RR* )
52 48 simp2d 
 |-  ( ph -> B e. RR )
53 52 rexrd 
 |-  ( ph -> B e. RR* )
54 53 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> B e. RR* )
55 1 2 3 fourierdlem15 
 |-  ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )
56 55 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
57 simpr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ..^ M ) )
58 51 54 56 57 fourierdlem8 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( A [,] B ) )
59 47 58 sstrid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( A [,] B ) )
60 46 59 feqresmpt 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) )
61 60 5 eqeltrrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
62 60 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) = ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) limCC ( Q ` ( i + 1 ) ) ) )
63 7 62 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) limCC ( Q ` ( i + 1 ) ) ) )
64 60 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) = ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) limCC ( Q ` i ) ) )
65 6 64 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) limCC ( Q ` i ) ) )
66 42 45 61 63 65 iblcncfioo 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. L^1 )
67 46 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> F : ( A [,] B ) --> CC )
68 58 sselda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. ( A [,] B ) )
69 67 68 ffvelrnd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( F ` x ) e. CC )
70 42 45 66 69 ibliooicc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. L^1 )
71 19 20 25 29 31 38 70 iblspltprt 
 |-  ( ph -> ( x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) |-> ( F ` x ) ) e. L^1 )
72 18 71 eqeltrd 
 |-  ( ph -> F e. L^1 )