Metamath Proof Explorer

Theorem fourierdlem70

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

Ref Expression
Hypotheses fourierdlem70.a 
|- ( ph -> A e. RR )
fourierdlem70.2 
|- ( ph -> B e. RR )
fourierdlem70.aleb 
|- ( ph -> A <_ B )
fourierdlem70.f 
|- ( ph -> F : ( A [,] B ) --> RR )
fourierdlem70.m 
|- ( ph -> M e. NN )
fourierdlem70.q 
|- ( ph -> Q : ( 0 ... M ) --> RR )
fourierdlem70.q0 
|- ( ph -> ( Q ` 0 ) = A )
fourierdlem70.qm 
|- ( ph -> ( Q ` M ) = B )
fourierdlem70.qlt 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
fourierdlem70.fcn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem70.r 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
fourierdlem70.l 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
fourierdlem70.i 
|- I = ( i e. ( 0 ..^ M ) |-> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
Assertion fourierdlem70 
|- ( ph -> E. x e. RR A. s e. ( A [,] B ) ( abs ` ( F ` s ) ) <_ x )

Proof

Step Hyp Ref Expression
1 fourierdlem70.a 
 |-  ( ph -> A e. RR )
2 fourierdlem70.2 
 |-  ( ph -> B e. RR )
3 fourierdlem70.aleb 
 |-  ( ph -> A <_ B )
4 fourierdlem70.f 
 |-  ( ph -> F : ( A [,] B ) --> RR )
5 fourierdlem70.m 
 |-  ( ph -> M e. NN )
6 fourierdlem70.q 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
7 fourierdlem70.q0 
 |-  ( ph -> ( Q ` 0 ) = A )
8 fourierdlem70.qm 
 |-  ( ph -> ( Q ` M ) = B )
9 fourierdlem70.qlt 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
10 fourierdlem70.fcn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
11 fourierdlem70.r 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
12 fourierdlem70.l 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
13 fourierdlem70.i 
 |-  I = ( i e. ( 0 ..^ M ) |-> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
14 prfi 
 |-  { ran Q , U. ran I } e. Fin
15 14 a1i 
 |-  ( ph -> { ran Q , U. ran I } e. Fin )
16 simpr 
 |-  ( ( ph /\ s e. U. { ran Q , U. ran I } ) -> s e. U. { ran Q , U. ran I } )
17 ovex 
 |-  ( 0 ... M ) e. _V
18 fex 
 |-  ( ( Q : ( 0 ... M ) --> RR /\ ( 0 ... M ) e. _V ) -> Q e. _V )
19 6 17 18 sylancl 
 |-  ( ph -> Q e. _V )
20 rnexg 
 |-  ( Q e. _V -> ran Q e. _V )
21 19 20 syl 
 |-  ( ph -> ran Q e. _V )
22 fzofi 
 |-  ( 0 ..^ M ) e. Fin
23 13 rnmptfi 
 |-  ( ( 0 ..^ M ) e. Fin -> ran I e. Fin )
24 22 23 ax-mp 
 |-  ran I e. Fin
25 24 elexi 
 |-  ran I e. _V
26 25 uniex 
 |-  U. ran I e. _V
27 uniprg 
 |-  ( ( ran Q e. _V /\ U. ran I e. _V ) -> U. { ran Q , U. ran I } = ( ran Q u. U. ran I ) )
28 21 26 27 sylancl 
 |-  ( ph -> U. { ran Q , U. ran I } = ( ran Q u. U. ran I ) )
29 28 adantr 
 |-  ( ( ph /\ s e. U. { ran Q , U. ran I } ) -> U. { ran Q , U. ran I } = ( ran Q u. U. ran I ) )
30 16 29 eleqtrd 
 |-  ( ( ph /\ s e. U. { ran Q , U. ran I } ) -> s e. ( ran Q u. U. ran I ) )
31 eqid 
 |-  ( y e. NN |-> { v e. ( RR ^m ( 0 ... y ) ) | ( ( ( v ` 0 ) = A /\ ( v ` y ) = B ) /\ A. i e. ( 0 ..^ y ) ( v ` i ) < ( v ` ( i + 1 ) ) ) } ) = ( y e. NN |-> { v e. ( RR ^m ( 0 ... y ) ) | ( ( ( v ` 0 ) = A /\ ( v ` y ) = B ) /\ A. i e. ( 0 ..^ y ) ( v ` i ) < ( v ` ( i + 1 ) ) ) } )
32 reex 
 |-  RR e. _V
33 32 17 elmap 
 |-  ( Q e. ( RR ^m ( 0 ... M ) ) <-> Q : ( 0 ... M ) --> RR )
34 6 33 sylibr 
 |-  ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
35 7 8 jca 
 |-  ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
36 9 ralrimiva 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
37 34 35 36 jca32 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
38 31 fourierdlem2 
 |-  ( M e. NN -> ( Q e. ( ( y e. NN |-> { v e. ( RR ^m ( 0 ... y ) ) | ( ( ( v ` 0 ) = A /\ ( v ` y ) = B ) /\ A. i e. ( 0 ..^ y ) ( v ` i ) < ( v ` ( i + 1 ) ) ) } ) ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
39 5 38 syl 
 |-  ( ph -> ( Q e. ( ( y e. NN |-> { v e. ( RR ^m ( 0 ... y ) ) | ( ( ( v ` 0 ) = A /\ ( v ` y ) = B ) /\ A. i e. ( 0 ..^ y ) ( v ` i ) < ( v ` ( i + 1 ) ) ) } ) ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
40 37 39 mpbird 
 |-  ( ph -> Q e. ( ( y e. NN |-> { v e. ( RR ^m ( 0 ... y ) ) | ( ( ( v ` 0 ) = A /\ ( v ` y ) = B ) /\ A. i e. ( 0 ..^ y ) ( v ` i ) < ( v ` ( i + 1 ) ) ) } ) ` M ) )
41 31 5 40 fourierdlem15 
 |-  ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )
42 41 frnd 
 |-  ( ph -> ran Q C_ ( A [,] B ) )
43 42 sselda 
 |-  ( ( ph /\ s e. ran Q ) -> s e. ( A [,] B ) )
44 43 adantlr 
 |-  ( ( ( ph /\ s e. ( ran Q u. U. ran I ) ) /\ s e. ran Q ) -> s e. ( A [,] B ) )
45 simpll 
 |-  ( ( ( ph /\ s e. ( ran Q u. U. ran I ) ) /\ -. s e. ran Q ) -> ph )
46 elunnel1 
 |-  ( ( s e. ( ran Q u. U. ran I ) /\ -. s e. ran Q ) -> s e. U. ran I )
47 46 adantll 
 |-  ( ( ( ph /\ s e. ( ran Q u. U. ran I ) ) /\ -. s e. ran Q ) -> s e. U. ran I )
48 simpr 
 |-  ( ( ph /\ s e. U. ran I ) -> s e. U. ran I )
49 13 funmpt2 
 |-  Fun I
50 elunirn 
 |-  ( Fun I -> ( s e. U. ran I <-> E. i e. dom I s e. ( I ` i ) ) )
51 49 50 mp1i 
 |-  ( ( ph /\ s e. U. ran I ) -> ( s e. U. ran I <-> E. i e. dom I s e. ( I ` i ) ) )
52 48 51 mpbid 
 |-  ( ( ph /\ s e. U. ran I ) -> E. i e. dom I s e. ( I ` i ) )
53 id 
 |-  ( i e. dom I -> i e. dom I )
54 ovex 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) e. _V
55 54 13 dmmpti 
 |-  dom I = ( 0 ..^ M )
56 53 55 eleqtrdi 
 |-  ( i e. dom I -> i e. ( 0 ..^ M ) )
57 13 fvmpt2 
 |-  ( ( i e. ( 0 ..^ M ) /\ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) e. _V ) -> ( I ` i ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
58 56 54 57 sylancl 
 |-  ( i e. dom I -> ( I ` i ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
59 58 adantl 
 |-  ( ( ph /\ i e. dom I ) -> ( I ` i ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
60 ioossicc 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
61 1 rexrd 
 |-  ( ph -> A e. RR* )
62 61 adantr 
 |-  ( ( ph /\ i e. dom I ) -> A e. RR* )
63 2 rexrd 
 |-  ( ph -> B e. RR* )
64 63 adantr 
 |-  ( ( ph /\ i e. dom I ) -> B e. RR* )
65 41 adantr 
 |-  ( ( ph /\ i e. dom I ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
66 56 adantl 
 |-  ( ( ph /\ i e. dom I ) -> i e. ( 0 ..^ M ) )
67 62 64 65 66 fourierdlem8 
 |-  ( ( ph /\ i e. dom I ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( A [,] B ) )
68 60 67 sstrid 
 |-  ( ( ph /\ i e. dom I ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( A [,] B ) )
69 59 68 eqsstrd 
 |-  ( ( ph /\ i e. dom I ) -> ( I ` i ) C_ ( A [,] B ) )
70 69 3adant3 
 |-  ( ( ph /\ i e. dom I /\ s e. ( I ` i ) ) -> ( I ` i ) C_ ( A [,] B ) )
71 simp3 
 |-  ( ( ph /\ i e. dom I /\ s e. ( I ` i ) ) -> s e. ( I ` i ) )
72 70 71 sseldd 
 |-  ( ( ph /\ i e. dom I /\ s e. ( I ` i ) ) -> s e. ( A [,] B ) )
73 72 3exp 
 |-  ( ph -> ( i e. dom I -> ( s e. ( I ` i ) -> s e. ( A [,] B ) ) ) )
74 73 adantr 
 |-  ( ( ph /\ s e. U. ran I ) -> ( i e. dom I -> ( s e. ( I ` i ) -> s e. ( A [,] B ) ) ) )
75 74 rexlimdv 
 |-  ( ( ph /\ s e. U. ran I ) -> ( E. i e. dom I s e. ( I ` i ) -> s e. ( A [,] B ) ) )
76 52 75 mpd 
 |-  ( ( ph /\ s e. U. ran I ) -> s e. ( A [,] B ) )
77 45 47 76 syl2anc 
 |-  ( ( ( ph /\ s e. ( ran Q u. U. ran I ) ) /\ -. s e. ran Q ) -> s e. ( A [,] B ) )
78 44 77 pm2.61dan 
 |-  ( ( ph /\ s e. ( ran Q u. U. ran I ) ) -> s e. ( A [,] B ) )
79 30 78 syldan 
 |-  ( ( ph /\ s e. U. { ran Q , U. ran I } ) -> s e. ( A [,] B ) )
80 4 ffvelcdmda 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> ( F ` s ) e. RR )
81 79 80 syldan 
 |-  ( ( ph /\ s e. U. { ran Q , U. ran I } ) -> ( F ` s ) e. RR )
82 81 recnd 
 |-  ( ( ph /\ s e. U. { ran Q , U. ran I } ) -> ( F ` s ) e. CC )
83 82 abscld 
 |-  ( ( ph /\ s e. U. { ran Q , U. ran I } ) -> ( abs ` ( F ` s ) ) e. RR )
84 simpr 
 |-  ( ( ph /\ w = ran Q ) -> w = ran Q )
85 6 adantr 
 |-  ( ( ph /\ w = ran Q ) -> Q : ( 0 ... M ) --> RR )
86 fzfid 
 |-  ( ( ph /\ w = ran Q ) -> ( 0 ... M ) e. Fin )
87 rnffi 
 |-  ( ( Q : ( 0 ... M ) --> RR /\ ( 0 ... M ) e. Fin ) -> ran Q e. Fin )
88 85 86 87 syl2anc 
 |-  ( ( ph /\ w = ran Q ) -> ran Q e. Fin )
89 84 88 eqeltrd 
 |-  ( ( ph /\ w = ran Q ) -> w e. Fin )
90 89 adantlr 
 |-  ( ( ( ph /\ w e. { ran Q , U. ran I } ) /\ w = ran Q ) -> w e. Fin )
91 4 ad2antrr 
 |-  ( ( ( ph /\ w = ran Q ) /\ s e. w ) -> F : ( A [,] B ) --> RR )
92 simpll 
 |-  ( ( ( ph /\ w = ran Q ) /\ s e. w ) -> ph )
93 simpr 
 |-  ( ( w = ran Q /\ s e. w ) -> s e. w )
94 simpl 
 |-  ( ( w = ran Q /\ s e. w ) -> w = ran Q )
95 93 94 eleqtrd 
 |-  ( ( w = ran Q /\ s e. w ) -> s e. ran Q )
96 95 adantll 
 |-  ( ( ( ph /\ w = ran Q ) /\ s e. w ) -> s e. ran Q )
97 92 96 43 syl2anc 
 |-  ( ( ( ph /\ w = ran Q ) /\ s e. w ) -> s e. ( A [,] B ) )
98 91 97 ffvelcdmd 
 |-  ( ( ( ph /\ w = ran Q ) /\ s e. w ) -> ( F ` s ) e. RR )
99 98 recnd 
 |-  ( ( ( ph /\ w = ran Q ) /\ s e. w ) -> ( F ` s ) e. CC )
100 99 abscld 
 |-  ( ( ( ph /\ w = ran Q ) /\ s e. w ) -> ( abs ` ( F ` s ) ) e. RR )
101 100 ralrimiva 
 |-  ( ( ph /\ w = ran Q ) -> A. s e. w ( abs ` ( F ` s ) ) e. RR )
102 101 adantlr 
 |-  ( ( ( ph /\ w e. { ran Q , U. ran I } ) /\ w = ran Q ) -> A. s e. w ( abs ` ( F ` s ) ) e. RR )
103 fimaxre3 
 |-  ( ( w e. Fin /\ A. s e. w ( abs ` ( F ` s ) ) e. RR ) -> E. z e. RR A. s e. w ( abs ` ( F ` s ) ) <_ z )
104 90 102 103 syl2anc 
 |-  ( ( ( ph /\ w e. { ran Q , U. ran I } ) /\ w = ran Q ) -> E. z e. RR A. s e. w ( abs ` ( F ` s ) ) <_ z )
105 simpll 
 |-  ( ( ( ph /\ w e. { ran Q , U. ran I } ) /\ -. w = ran Q ) -> ph )
106 neqne 
 |-  ( -. w = ran Q -> w =/= ran Q )
107 elprn1 
 |-  ( ( w e. { ran Q , U. ran I } /\ w =/= ran Q ) -> w = U. ran I )
108 106 107 sylan2 
 |-  ( ( w e. { ran Q , U. ran I } /\ -. w = ran Q ) -> w = U. ran I )
109 108 adantll 
 |-  ( ( ( ph /\ w e. { ran Q , U. ran I } ) /\ -. w = ran Q ) -> w = U. ran I )
110 22 23 mp1i 
 |-  ( ( ph /\ w = U. ran I ) -> ran I e. Fin )
111 ax-resscn 
 |-  RR C_ CC
112 111 a1i 
 |-  ( ph -> RR C_ CC )
113 4 112 fssd 
 |-  ( ph -> F : ( A [,] B ) --> CC )
114 113 ad2antrr 
 |-  ( ( ( ph /\ w = U. ran I ) /\ s e. U. ran I ) -> F : ( A [,] B ) --> CC )
115 76 adantlr 
 |-  ( ( ( ph /\ w = U. ran I ) /\ s e. U. ran I ) -> s e. ( A [,] B ) )
116 114 115 ffvelcdmd 
 |-  ( ( ( ph /\ w = U. ran I ) /\ s e. U. ran I ) -> ( F ` s ) e. CC )
117 116 abscld 
 |-  ( ( ( ph /\ w = U. ran I ) /\ s e. U. ran I ) -> ( abs ` ( F ` s ) ) e. RR )
118 54 13 fnmpti 
 |-  I Fn ( 0 ..^ M )
119 fvelrnb 
 |-  ( I Fn ( 0 ..^ M ) -> ( t e. ran I <-> E. i e. ( 0 ..^ M ) ( I ` i ) = t ) )
120 118 119 ax-mp 
 |-  ( t e. ran I <-> E. i e. ( 0 ..^ M ) ( I ` i ) = t )
121 120 bilani 
 |-  ( ( ph /\ t e. ran I ) -> E. i e. ( 0 ..^ M ) ( I ` i ) = t )
122 6 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
123 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
124 123 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
125 122 124 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
126 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
127 126 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
128 122 127 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
129 125 128 10 12 11 cncfioobd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> E. b e. RR A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` s ) ) <_ b )
130 fvres 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` s ) = ( F ` s ) )
131 130 fveq2d 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( abs ` ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` s ) ) = ( abs ` ( F ` s ) ) )
132 131 breq1d 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( abs ` ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` s ) ) <_ b <-> ( abs ` ( F ` s ) ) <_ b ) )
133 132 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( abs ` ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` s ) ) <_ b <-> ( abs ` ( F ` s ) ) <_ b ) )
134 133 ralbidva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` s ) ) <_ b <-> A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( F ` s ) ) <_ b ) )
135 134 rexbidv 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( E. b e. RR A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` s ) ) <_ b <-> E. b e. RR A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( F ` s ) ) <_ b ) )
136 129 135 mpbid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> E. b e. RR A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( F ` s ) ) <_ b )
137 136 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( I ` i ) = t ) -> E. b e. RR A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( F ` s ) ) <_ b )
138 54 57 mpan2 
 |-  ( i e. ( 0 ..^ M ) -> ( I ` i ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
139 138 eqcomd 
 |-  ( i e. ( 0 ..^ M ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( I ` i ) )
140 139 adantr 
 |-  ( ( i e. ( 0 ..^ M ) /\ ( I ` i ) = t ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( I ` i ) )
141 simpr 
 |-  ( ( i e. ( 0 ..^ M ) /\ ( I ` i ) = t ) -> ( I ` i ) = t )
142 140 141 eqtrd 
 |-  ( ( i e. ( 0 ..^ M ) /\ ( I ` i ) = t ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = t )
143 142 raleqdv 
 |-  ( ( i e. ( 0 ..^ M ) /\ ( I ` i ) = t ) -> ( A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( F ` s ) ) <_ b <-> A. s e. t ( abs ` ( F ` s ) ) <_ b ) )
144 143 rexbidv 
 |-  ( ( i e. ( 0 ..^ M ) /\ ( I ` i ) = t ) -> ( E. b e. RR A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( F ` s ) ) <_ b <-> E. b e. RR A. s e. t ( abs ` ( F ` s ) ) <_ b ) )
145 144 3adant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( I ` i ) = t ) -> ( E. b e. RR A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( F ` s ) ) <_ b <-> E. b e. RR A. s e. t ( abs ` ( F ` s ) ) <_ b ) )
146 137 145 mpbid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( I ` i ) = t ) -> E. b e. RR A. s e. t ( abs ` ( F ` s ) ) <_ b )
147 146 3exp 
 |-  ( ph -> ( i e. ( 0 ..^ M ) -> ( ( I ` i ) = t -> E. b e. RR A. s e. t ( abs ` ( F ` s ) ) <_ b ) ) )
148 147 adantr 
 |-  ( ( ph /\ t e. ran I ) -> ( i e. ( 0 ..^ M ) -> ( ( I ` i ) = t -> E. b e. RR A. s e. t ( abs ` ( F ` s ) ) <_ b ) ) )
149 148 rexlimdv 
 |-  ( ( ph /\ t e. ran I ) -> ( E. i e. ( 0 ..^ M ) ( I ` i ) = t -> E. b e. RR A. s e. t ( abs ` ( F ` s ) ) <_ b ) )
150 121 149 mpd 
 |-  ( ( ph /\ t e. ran I ) -> E. b e. RR A. s e. t ( abs ` ( F ` s ) ) <_ b )
151 150 adantlr 
 |-  ( ( ( ph /\ w = U. ran I ) /\ t e. ran I ) -> E. b e. RR A. s e. t ( abs ` ( F ` s ) ) <_ b )
152 eqimss 
 |-  ( w = U. ran I -> w C_ U. ran I )
153 152 adantl 
 |-  ( ( ph /\ w = U. ran I ) -> w C_ U. ran I )
154 110 117 151 153 ssfiunibd 
 |-  ( ( ph /\ w = U. ran I ) -> E. z e. RR A. s e. w ( abs ` ( F ` s ) ) <_ z )
155 105 109 154 syl2anc 
 |-  ( ( ( ph /\ w e. { ran Q , U. ran I } ) /\ -. w = ran Q ) -> E. z e. RR A. s e. w ( abs ` ( F ` s ) ) <_ z )
156 104 155 pm2.61dan 
 |-  ( ( ph /\ w e. { ran Q , U. ran I } ) -> E. z e. RR A. s e. w ( abs ` ( F ` s ) ) <_ z )
157 5 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A [,] B ) ) /\ -. t e. ran Q ) -> M e. NN )
158 6 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A [,] B ) ) /\ -. t e. ran Q ) -> Q : ( 0 ... M ) --> RR )
159 simpr 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> t e. ( A [,] B ) )
160 7 eqcomd 
 |-  ( ph -> A = ( Q ` 0 ) )
161 8 eqcomd 
 |-  ( ph -> B = ( Q ` M ) )
162 160 161 oveq12d 
 |-  ( ph -> ( A [,] B ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
163 162 adantr 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( A [,] B ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
164 159 163 eleqtrd 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
165 164 adantr 
 |-  ( ( ( ph /\ t e. ( A [,] B ) ) /\ -. t e. ran Q ) -> t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
166 simpr 
 |-  ( ( ( ph /\ t e. ( A [,] B ) ) /\ -. t e. ran Q ) -> -. t e. ran Q )
167 fveq2 
 |-  ( k = j -> ( Q ` k ) = ( Q ` j ) )
168 167 breq1d 
 |-  ( k = j -> ( ( Q ` k ) < t <-> ( Q ` j ) < t ) )
169 168 cbvrabv 
 |-  { k e. ( 0 ..^ M ) | ( Q ` k ) < t } = { j e. ( 0 ..^ M ) | ( Q ` j ) < t }
170 169 supeq1i 
 |-  sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) < t } , RR , < ) = sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) < t } , RR , < )
171 157 158 165 166 170 fourierdlem25 
 |-  ( ( ( ph /\ t e. ( A [,] B ) ) /\ -. t e. ran Q ) -> E. i e. ( 0 ..^ M ) t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
172 138 eleq2d 
 |-  ( i e. ( 0 ..^ M ) -> ( t e. ( I ` i ) <-> t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
173 172 rexbiia 
 |-  ( E. i e. ( 0 ..^ M ) t e. ( I ` i ) <-> E. i e. ( 0 ..^ M ) t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
174 171 173 sylibr 
 |-  ( ( ( ph /\ t e. ( A [,] B ) ) /\ -. t e. ran Q ) -> E. i e. ( 0 ..^ M ) t e. ( I ` i ) )
175 55 eqcomi 
 |-  ( 0 ..^ M ) = dom I
176 175 rexeqi 
 |-  ( E. i e. ( 0 ..^ M ) t e. ( I ` i ) <-> E. i e. dom I t e. ( I ` i ) )
177 174 176 sylib 
 |-  ( ( ( ph /\ t e. ( A [,] B ) ) /\ -. t e. ran Q ) -> E. i e. dom I t e. ( I ` i ) )
178 elunirn 
 |-  ( Fun I -> ( t e. U. ran I <-> E. i e. dom I t e. ( I ` i ) ) )
179 49 178 mp1i 
 |-  ( ( ( ph /\ t e. ( A [,] B ) ) /\ -. t e. ran Q ) -> ( t e. U. ran I <-> E. i e. dom I t e. ( I ` i ) ) )
180 177 179 mpbird 
 |-  ( ( ( ph /\ t e. ( A [,] B ) ) /\ -. t e. ran Q ) -> t e. U. ran I )
181 180 ex 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( -. t e. ran Q -> t e. U. ran I ) )
182 181 orrd 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( t e. ran Q \/ t e. U. ran I ) )
183 elun 
 |-  ( t e. ( ran Q u. U. ran I ) <-> ( t e. ran Q \/ t e. U. ran I ) )
184 182 183 sylibr 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> t e. ( ran Q u. U. ran I ) )
185 184 ralrimiva 
 |-  ( ph -> A. t e. ( A [,] B ) t e. ( ran Q u. U. ran I ) )
186 dfss3 
 |-  ( ( A [,] B ) C_ ( ran Q u. U. ran I ) <-> A. t e. ( A [,] B ) t e. ( ran Q u. U. ran I ) )
187 185 186 sylibr 
 |-  ( ph -> ( A [,] B ) C_ ( ran Q u. U. ran I ) )
188 187 28 sseqtrrd 
 |-  ( ph -> ( A [,] B ) C_ U. { ran Q , U. ran I } )
189 15 83 156 188 ssfiunibd 
 |-  ( ph -> E. x e. RR A. s e. ( A [,] B ) ( abs ` ( F ` s ) ) <_ x )