Metamath Proof Explorer

Theorem fourierdlem71

Description: A periodic piecewise continuous function, possibly undefined on a finite set in each periodic interval, is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem71.dmf 
|- ( ph -> dom F C_ RR )
fourierdlem71.f 
|- ( ph -> F : dom F --> RR )
fourierdlem71.a 
|- ( ph -> A e. RR )
fourierdlem71.b 
|- ( ph -> B e. RR )
fourierdlem71.altb 
|- ( ph -> A < B )
fourierdlem71.t 
|- T = ( B - A )
fourierdlem71.7 
|- ( ph -> M e. NN )
fourierdlem71.q 
|- ( ph -> Q : ( 0 ... M ) --> RR )
fourierdlem71.q0 
|- ( ph -> ( Q ` 0 ) = A )
fourierdlem71.10 
|- ( ph -> ( Q ` M ) = B )
fourierdlem71.fcn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem71.r 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
fourierdlem71.l 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
fourierdlem71.xpt 
|- ( ( ( ph /\ x e. dom F ) /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. dom F )
fourierdlem71.fxpt 
|- ( ( ( ph /\ x e. dom F ) /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) )
fourierdlem71.i 
|- I = ( i e. ( 0 ..^ M ) |-> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
fourierdlem71.e 
|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
Assertion fourierdlem71 
|- ( ph -> E. y e. RR A. x e. dom F ( abs ` ( F ` x ) ) <_ y )

Proof

Step Hyp Ref Expression
1 fourierdlem71.dmf 
 |-  ( ph -> dom F C_ RR )
2 fourierdlem71.f 
 |-  ( ph -> F : dom F --> RR )
3 fourierdlem71.a 
 |-  ( ph -> A e. RR )
4 fourierdlem71.b 
 |-  ( ph -> B e. RR )
5 fourierdlem71.altb 
 |-  ( ph -> A < B )
6 fourierdlem71.t 
 |-  T = ( B - A )
7 fourierdlem71.7 
 |-  ( ph -> M e. NN )
8 fourierdlem71.q 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
9 fourierdlem71.q0 
 |-  ( ph -> ( Q ` 0 ) = A )
10 fourierdlem71.10 
 |-  ( ph -> ( Q ` M ) = B )
11 fourierdlem71.fcn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
12 fourierdlem71.r 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
13 fourierdlem71.l 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
14 fourierdlem71.xpt 
 |-  ( ( ( ph /\ x e. dom F ) /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. dom F )
15 fourierdlem71.fxpt 
 |-  ( ( ( ph /\ x e. dom F ) /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) )
16 fourierdlem71.i 
 |-  I = ( i e. ( 0 ..^ M ) |-> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
17 fourierdlem71.e 
 |-  E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
18 prfi 
 |-  { ( ran Q i^i dom F ) , U. ran I } e. Fin
19 18 a1i 
 |-  ( ph -> { ( ran Q i^i dom F ) , U. ran I } e. Fin )
20 2 adantr 
 |-  ( ( ph /\ x e. U. { ( ran Q i^i dom F ) , U. ran I } ) -> F : dom F --> RR )
21 simpl 
 |-  ( ( ph /\ x e. U. { ( ran Q i^i dom F ) , U. ran I } ) -> ph )
22 simpr 
 |-  ( ( ph /\ x e. U. { ( ran Q i^i dom F ) , U. ran I } ) -> x e. U. { ( ran Q i^i dom F ) , U. ran I } )
23 ovex 
 |-  ( 0 ... M ) e. _V
24 23 a1i 
 |-  ( ph -> ( 0 ... M ) e. _V )
25 8 24 fexd 
 |-  ( ph -> Q e. _V )
26 rnexg 
 |-  ( Q e. _V -> ran Q e. _V )
27 inex1g 
 |-  ( ran Q e. _V -> ( ran Q i^i dom F ) e. _V )
28 25 26 27 3syl 
 |-  ( ph -> ( ran Q i^i dom F ) e. _V )
29 28 adantr 
 |-  ( ( ph /\ x e. U. { ( ran Q i^i dom F ) , U. ran I } ) -> ( ran Q i^i dom F ) e. _V )
30 ovex 
 |-  ( 0 ..^ M ) e. _V
31 30 mptex 
 |-  ( i e. ( 0 ..^ M ) |-> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. _V
32 16 31 eqeltri 
 |-  I e. _V
33 32 rnex 
 |-  ran I e. _V
34 33 a1i 
 |-  ( ph -> ran I e. _V )
35 34 uniexd 
 |-  ( ph -> U. ran I e. _V )
36 35 adantr 
 |-  ( ( ph /\ x e. U. { ( ran Q i^i dom F ) , U. ran I } ) -> U. ran I e. _V )
37 uniprg 
 |-  ( ( ( ran Q i^i dom F ) e. _V /\ U. ran I e. _V ) -> U. { ( ran Q i^i dom F ) , U. ran I } = ( ( ran Q i^i dom F ) u. U. ran I ) )
38 29 36 37 syl2anc 
 |-  ( ( ph /\ x e. U. { ( ran Q i^i dom F ) , U. ran I } ) -> U. { ( ran Q i^i dom F ) , U. ran I } = ( ( ran Q i^i dom F ) u. U. ran I ) )
39 22 38 eleqtrd 
 |-  ( ( ph /\ x e. U. { ( ran Q i^i dom F ) , U. ran I } ) -> x e. ( ( ran Q i^i dom F ) u. U. ran I ) )
40 elinel2 
 |-  ( x e. ( ran Q i^i dom F ) -> x e. dom F )
41 40 adantl 
 |-  ( ( ( ph /\ x e. ( ( ran Q i^i dom F ) u. U. ran I ) ) /\ x e. ( ran Q i^i dom F ) ) -> x e. dom F )
42 simpll 
 |-  ( ( ( ph /\ x e. ( ( ran Q i^i dom F ) u. U. ran I ) ) /\ -. x e. ( ran Q i^i dom F ) ) -> ph )
43 elunnel1 
 |-  ( ( x e. ( ( ran Q i^i dom F ) u. U. ran I ) /\ -. x e. ( ran Q i^i dom F ) ) -> x e. U. ran I )
44 43 adantll 
 |-  ( ( ( ph /\ x e. ( ( ran Q i^i dom F ) u. U. ran I ) ) /\ -. x e. ( ran Q i^i dom F ) ) -> x e. U. ran I )
45 16 funmpt2 
 |-  Fun I
46 elunirn 
 |-  ( Fun I -> ( x e. U. ran I <-> E. i e. dom I x e. ( I ` i ) ) )
47 45 46 ax-mp 
 |-  ( x e. U. ran I <-> E. i e. dom I x e. ( I ` i ) )
48 47 bilani 
 |-  ( ( ph /\ x e. U. ran I ) -> E. i e. dom I x e. ( I ` i ) )
49 id 
 |-  ( i e. dom I -> i e. dom I )
50 ovex 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) e. _V
51 50 16 dmmpti 
 |-  dom I = ( 0 ..^ M )
52 49 51 eleqtrdi 
 |-  ( i e. dom I -> i e. ( 0 ..^ M ) )
53 52 adantl 
 |-  ( ( ph /\ i e. dom I ) -> i e. ( 0 ..^ M ) )
54 50 a1i 
 |-  ( ( ph /\ i e. dom I ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) e. _V )
55 16 fvmpt2 
 |-  ( ( i e. ( 0 ..^ M ) /\ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) e. _V ) -> ( I ` i ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
56 53 54 55 syl2anc 
 |-  ( ( ph /\ i e. dom I ) -> ( I ` i ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
57 cncff 
 |-  ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
58 fdm 
 |-  ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
59 11 57 58 3syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
60 52 59 sylan2 
 |-  ( ( ph /\ i e. dom I ) -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
61 ssdmres 
 |-  ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F <-> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
62 60 61 sylibr 
 |-  ( ( ph /\ i e. dom I ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
63 56 62 eqsstrd 
 |-  ( ( ph /\ i e. dom I ) -> ( I ` i ) C_ dom F )
64 63 3adant3 
 |-  ( ( ph /\ i e. dom I /\ x e. ( I ` i ) ) -> ( I ` i ) C_ dom F )
65 simp3 
 |-  ( ( ph /\ i e. dom I /\ x e. ( I ` i ) ) -> x e. ( I ` i ) )
66 64 65 sseldd 
 |-  ( ( ph /\ i e. dom I /\ x e. ( I ` i ) ) -> x e. dom F )
67 66 3exp 
 |-  ( ph -> ( i e. dom I -> ( x e. ( I ` i ) -> x e. dom F ) ) )
68 67 adantr 
 |-  ( ( ph /\ x e. U. ran I ) -> ( i e. dom I -> ( x e. ( I ` i ) -> x e. dom F ) ) )
69 68 rexlimdv 
 |-  ( ( ph /\ x e. U. ran I ) -> ( E. i e. dom I x e. ( I ` i ) -> x e. dom F ) )
70 48 69 mpd 
 |-  ( ( ph /\ x e. U. ran I ) -> x e. dom F )
71 42 44 70 syl2anc 
 |-  ( ( ( ph /\ x e. ( ( ran Q i^i dom F ) u. U. ran I ) ) /\ -. x e. ( ran Q i^i dom F ) ) -> x e. dom F )
72 41 71 pm2.61dan 
 |-  ( ( ph /\ x e. ( ( ran Q i^i dom F ) u. U. ran I ) ) -> x e. dom F )
73 21 39 72 syl2anc 
 |-  ( ( ph /\ x e. U. { ( ran Q i^i dom F ) , U. ran I } ) -> x e. dom F )
74 20 73 ffvelcdmd 
 |-  ( ( ph /\ x e. U. { ( ran Q i^i dom F ) , U. ran I } ) -> ( F ` x ) e. RR )
75 74 recnd 
 |-  ( ( ph /\ x e. U. { ( ran Q i^i dom F ) , U. ran I } ) -> ( F ` x ) e. CC )
76 75 abscld 
 |-  ( ( ph /\ x e. U. { ( ran Q i^i dom F ) , U. ran I } ) -> ( abs ` ( F ` x ) ) e. RR )
77 simpr 
 |-  ( ( ph /\ w = ( ran Q i^i dom F ) ) -> w = ( ran Q i^i dom F ) )
78 fzfid 
 |-  ( ph -> ( 0 ... M ) e. Fin )
79 rnffi 
 |-  ( ( Q : ( 0 ... M ) --> RR /\ ( 0 ... M ) e. Fin ) -> ran Q e. Fin )
80 8 78 79 syl2anc 
 |-  ( ph -> ran Q e. Fin )
81 infi 
 |-  ( ran Q e. Fin -> ( ran Q i^i dom F ) e. Fin )
82 80 81 syl 
 |-  ( ph -> ( ran Q i^i dom F ) e. Fin )
83 82 adantr 
 |-  ( ( ph /\ w = ( ran Q i^i dom F ) ) -> ( ran Q i^i dom F ) e. Fin )
84 77 83 eqeltrd 
 |-  ( ( ph /\ w = ( ran Q i^i dom F ) ) -> w e. Fin )
85 simpll 
 |-  ( ( ( ph /\ w = ( ran Q i^i dom F ) ) /\ x e. w ) -> ph )
86 simpr 
 |-  ( ( w = ( ran Q i^i dom F ) /\ x e. w ) -> x e. w )
87 simpl 
 |-  ( ( w = ( ran Q i^i dom F ) /\ x e. w ) -> w = ( ran Q i^i dom F ) )
88 86 87 eleqtrd 
 |-  ( ( w = ( ran Q i^i dom F ) /\ x e. w ) -> x e. ( ran Q i^i dom F ) )
89 88 adantll 
 |-  ( ( ( ph /\ w = ( ran Q i^i dom F ) ) /\ x e. w ) -> x e. ( ran Q i^i dom F ) )
90 2 adantr 
 |-  ( ( ph /\ x e. ( ran Q i^i dom F ) ) -> F : dom F --> RR )
91 40 adantl 
 |-  ( ( ph /\ x e. ( ran Q i^i dom F ) ) -> x e. dom F )
92 90 91 ffvelcdmd 
 |-  ( ( ph /\ x e. ( ran Q i^i dom F ) ) -> ( F ` x ) e. RR )
93 92 recnd 
 |-  ( ( ph /\ x e. ( ran Q i^i dom F ) ) -> ( F ` x ) e. CC )
94 93 abscld 
 |-  ( ( ph /\ x e. ( ran Q i^i dom F ) ) -> ( abs ` ( F ` x ) ) e. RR )
95 85 89 94 syl2anc 
 |-  ( ( ( ph /\ w = ( ran Q i^i dom F ) ) /\ x e. w ) -> ( abs ` ( F ` x ) ) e. RR )
96 95 ralrimiva 
 |-  ( ( ph /\ w = ( ran Q i^i dom F ) ) -> A. x e. w ( abs ` ( F ` x ) ) e. RR )
97 fimaxre3 
 |-  ( ( w e. Fin /\ A. x e. w ( abs ` ( F ` x ) ) e. RR ) -> E. y e. RR A. x e. w ( abs ` ( F ` x ) ) <_ y )
98 84 96 97 syl2anc 
 |-  ( ( ph /\ w = ( ran Q i^i dom F ) ) -> E. y e. RR A. x e. w ( abs ` ( F ` x ) ) <_ y )
99 98 adantlr 
 |-  ( ( ( ph /\ w e. { ( ran Q i^i dom F ) , U. ran I } ) /\ w = ( ran Q i^i dom F ) ) -> E. y e. RR A. x e. w ( abs ` ( F ` x ) ) <_ y )
100 simpll 
 |-  ( ( ( ph /\ w e. { ( ran Q i^i dom F ) , U. ran I } ) /\ -. w = ( ran Q i^i dom F ) ) -> ph )
101 neqne 
 |-  ( -. w = ( ran Q i^i dom F ) -> w =/= ( ran Q i^i dom F ) )
102 elprn1 
 |-  ( ( w e. { ( ran Q i^i dom F ) , U. ran I } /\ w =/= ( ran Q i^i dom F ) ) -> w = U. ran I )
103 101 102 sylan2 
 |-  ( ( w e. { ( ran Q i^i dom F ) , U. ran I } /\ -. w = ( ran Q i^i dom F ) ) -> w = U. ran I )
104 103 adantll 
 |-  ( ( ( ph /\ w e. { ( ran Q i^i dom F ) , U. ran I } ) /\ -. w = ( ran Q i^i dom F ) ) -> w = U. ran I )
105 fzofi 
 |-  ( 0 ..^ M ) e. Fin
106 16 rnmptfi 
 |-  ( ( 0 ..^ M ) e. Fin -> ran I e. Fin )
107 105 106 ax-mp 
 |-  ran I e. Fin
108 107 a1i 
 |-  ( ( ph /\ w = U. ran I ) -> ran I e. Fin )
109 2 adantr 
 |-  ( ( ph /\ x e. U. ran I ) -> F : dom F --> RR )
110 109 70 ffvelcdmd 
 |-  ( ( ph /\ x e. U. ran I ) -> ( F ` x ) e. RR )
111 110 recnd 
 |-  ( ( ph /\ x e. U. ran I ) -> ( F ` x ) e. CC )
112 111 adantlr 
 |-  ( ( ( ph /\ w = U. ran I ) /\ x e. U. ran I ) -> ( F ` x ) e. CC )
113 112 abscld 
 |-  ( ( ( ph /\ w = U. ran I ) /\ x e. U. ran I ) -> ( abs ` ( F ` x ) ) e. RR )
114 50 16 fnmpti 
 |-  I Fn ( 0 ..^ M )
115 fvelrnb 
 |-  ( I Fn ( 0 ..^ M ) -> ( t e. ran I <-> E. i e. ( 0 ..^ M ) ( I ` i ) = t ) )
116 114 115 ax-mp 
 |-  ( t e. ran I <-> E. i e. ( 0 ..^ M ) ( I ` i ) = t )
117 116 bilani 
 |-  ( ( ph /\ t e. ran I ) -> E. i e. ( 0 ..^ M ) ( I ` i ) = t )
118 8 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
119 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
120 119 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
121 118 120 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
122 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
123 122 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
124 118 123 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
125 121 124 11 13 12 cncfioobd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> E. b e. RR A. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) <_ b )
126 125 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( I ` i ) = t ) -> E. b e. RR A. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) <_ b )
127 fvres 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) = ( F ` x ) )
128 127 fveq2d 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( abs ` ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) = ( abs ` ( F ` x ) ) )
129 128 breq1d 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( abs ` ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) <_ b <-> ( abs ` ( F ` x ) ) <_ b ) )
130 129 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( abs ` ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) <_ b <-> ( abs ` ( F ` x ) ) <_ b ) )
131 130 ralbidva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( A. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) <_ b <-> A. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( F ` x ) ) <_ b ) )
132 131 rexbidv 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( E. b e. RR A. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) <_ b <-> E. b e. RR A. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( F ` x ) ) <_ b ) )
133 132 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( I ` i ) = t ) -> ( E. b e. RR A. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) <_ b <-> E. b e. RR A. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( F ` x ) ) <_ b ) )
134 50 55 mpan2 
 |-  ( i e. ( 0 ..^ M ) -> ( I ` i ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
135 id 
 |-  ( ( I ` i ) = t -> ( I ` i ) = t )
136 134 135 sylan9req 
 |-  ( ( i e. ( 0 ..^ M ) /\ ( I ` i ) = t ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = t )
137 136 3adant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( I ` i ) = t ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = t )
138 137 raleqdv 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( I ` i ) = t ) -> ( A. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( F ` x ) ) <_ b <-> A. x e. t ( abs ` ( F ` x ) ) <_ b ) )
139 138 rexbidv 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( I ` i ) = t ) -> ( E. b e. RR A. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( F ` x ) ) <_ b <-> E. b e. RR A. x e. t ( abs ` ( F ` x ) ) <_ b ) )
140 133 139 bitrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( I ` i ) = t ) -> ( E. b e. RR A. x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) <_ b <-> E. b e. RR A. x e. t ( abs ` ( F ` x ) ) <_ b ) )
141 126 140 mpbid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ ( I ` i ) = t ) -> E. b e. RR A. x e. t ( abs ` ( F ` x ) ) <_ b )
142 141 3exp 
 |-  ( ph -> ( i e. ( 0 ..^ M ) -> ( ( I ` i ) = t -> E. b e. RR A. x e. t ( abs ` ( F ` x ) ) <_ b ) ) )
143 142 adantr 
 |-  ( ( ph /\ t e. ran I ) -> ( i e. ( 0 ..^ M ) -> ( ( I ` i ) = t -> E. b e. RR A. x e. t ( abs ` ( F ` x ) ) <_ b ) ) )
144 143 rexlimdv 
 |-  ( ( ph /\ t e. ran I ) -> ( E. i e. ( 0 ..^ M ) ( I ` i ) = t -> E. b e. RR A. x e. t ( abs ` ( F ` x ) ) <_ b ) )
145 117 144 mpd 
 |-  ( ( ph /\ t e. ran I ) -> E. b e. RR A. x e. t ( abs ` ( F ` x ) ) <_ b )
146 145 adantlr 
 |-  ( ( ( ph /\ w = U. ran I ) /\ t e. ran I ) -> E. b e. RR A. x e. t ( abs ` ( F ` x ) ) <_ b )
147 eqimss 
 |-  ( w = U. ran I -> w C_ U. ran I )
148 147 adantl 
 |-  ( ( ph /\ w = U. ran I ) -> w C_ U. ran I )
149 108 113 146 148 ssfiunibd 
 |-  ( ( ph /\ w = U. ran I ) -> E. y e. RR A. x e. w ( abs ` ( F ` x ) ) <_ y )
150 100 104 149 syl2anc 
 |-  ( ( ( ph /\ w e. { ( ran Q i^i dom F ) , U. ran I } ) /\ -. w = ( ran Q i^i dom F ) ) -> E. y e. RR A. x e. w ( abs ` ( F ` x ) ) <_ y )
151 99 150 pm2.61dan 
 |-  ( ( ph /\ w e. { ( ran Q i^i dom F ) , U. ran I } ) -> E. y e. RR A. x e. w ( abs ` ( F ` x ) ) <_ y )
152 simpr 
 |-  ( ( ( ph /\ x e. ( ( A [,] B ) i^i dom F ) ) /\ x e. ran Q ) -> x e. ran Q )
153 elinel2 
 |-  ( x e. ( ( A [,] B ) i^i dom F ) -> x e. dom F )
154 153 ad2antlr 
 |-  ( ( ( ph /\ x e. ( ( A [,] B ) i^i dom F ) ) /\ x e. ran Q ) -> x e. dom F )
155 152 154 elind 
 |-  ( ( ( ph /\ x e. ( ( A [,] B ) i^i dom F ) ) /\ x e. ran Q ) -> x e. ( ran Q i^i dom F ) )
156 elun1 
 |-  ( x e. ( ran Q i^i dom F ) -> x e. ( ( ran Q i^i dom F ) u. U. ran I ) )
157 155 156 syl 
 |-  ( ( ( ph /\ x e. ( ( A [,] B ) i^i dom F ) ) /\ x e. ran Q ) -> x e. ( ( ran Q i^i dom F ) u. U. ran I ) )
158 7 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( A [,] B ) i^i dom F ) ) /\ -. x e. ran Q ) -> M e. NN )
159 8 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( A [,] B ) i^i dom F ) ) /\ -. x e. ran Q ) -> Q : ( 0 ... M ) --> RR )
160 elinel1 
 |-  ( x e. ( ( A [,] B ) i^i dom F ) -> x e. ( A [,] B ) )
161 160 adantl 
 |-  ( ( ph /\ x e. ( ( A [,] B ) i^i dom F ) ) -> x e. ( A [,] B ) )
162 9 eqcomd 
 |-  ( ph -> A = ( Q ` 0 ) )
163 162 adantr 
 |-  ( ( ph /\ x e. ( ( A [,] B ) i^i dom F ) ) -> A = ( Q ` 0 ) )
164 10 eqcomd 
 |-  ( ph -> B = ( Q ` M ) )
165 164 adantr 
 |-  ( ( ph /\ x e. ( ( A [,] B ) i^i dom F ) ) -> B = ( Q ` M ) )
166 163 165 oveq12d 
 |-  ( ( ph /\ x e. ( ( A [,] B ) i^i dom F ) ) -> ( A [,] B ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
167 161 166 eleqtrd 
 |-  ( ( ph /\ x e. ( ( A [,] B ) i^i dom F ) ) -> x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
168 167 adantr 
 |-  ( ( ( ph /\ x e. ( ( A [,] B ) i^i dom F ) ) /\ -. x e. ran Q ) -> x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
169 simpr 
 |-  ( ( ( ph /\ x e. ( ( A [,] B ) i^i dom F ) ) /\ -. x e. ran Q ) -> -. x e. ran Q )
170 fveq2 
 |-  ( k = j -> ( Q ` k ) = ( Q ` j ) )
171 170 breq1d 
 |-  ( k = j -> ( ( Q ` k ) < x <-> ( Q ` j ) < x ) )
172 171 cbvrabv 
 |-  { k e. ( 0 ..^ M ) | ( Q ` k ) < x } = { j e. ( 0 ..^ M ) | ( Q ` j ) < x }
173 172 supeq1i 
 |-  sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) < x } , RR , < ) = sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) < x } , RR , < )
174 158 159 168 169 173 fourierdlem25 
 |-  ( ( ( ph /\ x e. ( ( A [,] B ) i^i dom F ) ) /\ -. x e. ran Q ) -> E. i e. ( 0 ..^ M ) x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
175 52 ad2antrl 
 |-  ( ( ph /\ ( i e. dom I /\ x e. ( I ` i ) ) ) -> i e. ( 0 ..^ M ) )
176 simprr 
 |-  ( ( ph /\ ( i e. dom I /\ x e. ( I ` i ) ) ) -> x e. ( I ` i ) )
177 175 134 syl 
 |-  ( ( ph /\ ( i e. dom I /\ x e. ( I ` i ) ) ) -> ( I ` i ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
178 176 177 eleqtrd 
 |-  ( ( ph /\ ( i e. dom I /\ x e. ( I ` i ) ) ) -> x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
179 175 178 jca 
 |-  ( ( ph /\ ( i e. dom I /\ x e. ( I ` i ) ) ) -> ( i e. ( 0 ..^ M ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
180 id 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ..^ M ) )
181 180 51 eleqtrrdi 
 |-  ( i e. ( 0 ..^ M ) -> i e. dom I )
182 181 ad2antrl 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) -> i e. dom I )
183 simprr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) -> x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
184 134 eqcomd 
 |-  ( i e. ( 0 ..^ M ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( I ` i ) )
185 184 ad2antrl 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( I ` i ) )
186 183 185 eleqtrd 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) -> x e. ( I ` i ) )
187 182 186 jca 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) -> ( i e. dom I /\ x e. ( I ` i ) ) )
188 179 187 impbida 
 |-  ( ph -> ( ( i e. dom I /\ x e. ( I ` i ) ) <-> ( i e. ( 0 ..^ M ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) )
189 188 rexbidv2 
 |-  ( ph -> ( E. i e. dom I x e. ( I ` i ) <-> E. i e. ( 0 ..^ M ) x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
190 189 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( A [,] B ) i^i dom F ) ) /\ -. x e. ran Q ) -> ( E. i e. dom I x e. ( I ` i ) <-> E. i e. ( 0 ..^ M ) x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
191 174 190 mpbird 
 |-  ( ( ( ph /\ x e. ( ( A [,] B ) i^i dom F ) ) /\ -. x e. ran Q ) -> E. i e. dom I x e. ( I ` i ) )
192 191 47 sylibr 
 |-  ( ( ( ph /\ x e. ( ( A [,] B ) i^i dom F ) ) /\ -. x e. ran Q ) -> x e. U. ran I )
193 elun2 
 |-  ( x e. U. ran I -> x e. ( ( ran Q i^i dom F ) u. U. ran I ) )
194 192 193 syl 
 |-  ( ( ( ph /\ x e. ( ( A [,] B ) i^i dom F ) ) /\ -. x e. ran Q ) -> x e. ( ( ran Q i^i dom F ) u. U. ran I ) )
195 157 194 pm2.61dan 
 |-  ( ( ph /\ x e. ( ( A [,] B ) i^i dom F ) ) -> x e. ( ( ran Q i^i dom F ) u. U. ran I ) )
196 195 ralrimiva 
 |-  ( ph -> A. x e. ( ( A [,] B ) i^i dom F ) x e. ( ( ran Q i^i dom F ) u. U. ran I ) )
197 dfss3 
 |-  ( ( ( A [,] B ) i^i dom F ) C_ ( ( ran Q i^i dom F ) u. U. ran I ) <-> A. x e. ( ( A [,] B ) i^i dom F ) x e. ( ( ran Q i^i dom F ) u. U. ran I ) )
198 196 197 sylibr 
 |-  ( ph -> ( ( A [,] B ) i^i dom F ) C_ ( ( ran Q i^i dom F ) u. U. ran I ) )
199 28 35 37 syl2anc 
 |-  ( ph -> U. { ( ran Q i^i dom F ) , U. ran I } = ( ( ran Q i^i dom F ) u. U. ran I ) )
200 198 199 sseqtrrd 
 |-  ( ph -> ( ( A [,] B ) i^i dom F ) C_ U. { ( ran Q i^i dom F ) , U. ran I } )
201 19 76 151 200 ssfiunibd 
 |-  ( ph -> E. y e. RR A. x e. ( ( A [,] B ) i^i dom F ) ( abs ` ( F ` x ) ) <_ y )
202 nfv 
 |-  F/ x ph
203 nfra1 
 |-  F/ x A. x e. ( ( A [,] B ) i^i dom F ) ( abs ` ( F ` x ) ) <_ y
204 202 203 nfan 
 |-  F/ x ( ph /\ A. x e. ( ( A [,] B ) i^i dom F ) ( abs ` ( F ` x ) ) <_ y )
205 1 sselda 
 |-  ( ( ph /\ x e. dom F ) -> x e. RR )
206 4 adantr 
 |-  ( ( ph /\ x e. dom F ) -> B e. RR )
207 206 205 resubcld 
 |-  ( ( ph /\ x e. dom F ) -> ( B - x ) e. RR )
208 4 3 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
209 6 208 eqeltrid 
 |-  ( ph -> T e. RR )
210 209 adantr 
 |-  ( ( ph /\ x e. dom F ) -> T e. RR )
211 3 4 posdifd 
 |-  ( ph -> ( A < B <-> 0 < ( B - A ) ) )
212 5 211 mpbid 
 |-  ( ph -> 0 < ( B - A ) )
213 212 6 breqtrrdi 
 |-  ( ph -> 0 < T )
214 213 gt0ne0d 
 |-  ( ph -> T =/= 0 )
215 214 adantr 
 |-  ( ( ph /\ x e. dom F ) -> T =/= 0 )
216 207 210 215 redivcld 
 |-  ( ( ph /\ x e. dom F ) -> ( ( B - x ) / T ) e. RR )
217 216 flcld 
 |-  ( ( ph /\ x e. dom F ) -> ( |_ ` ( ( B - x ) / T ) ) e. ZZ )
218 217 zred 
 |-  ( ( ph /\ x e. dom F ) -> ( |_ ` ( ( B - x ) / T ) ) e. RR )
219 218 210 remulcld 
 |-  ( ( ph /\ x e. dom F ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. RR )
220 205 219 readdcld 
 |-  ( ( ph /\ x e. dom F ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. RR )
221 17 fvmpt2 
 |-  ( ( x e. RR /\ ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. RR ) -> ( E ` x ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
222 205 220 221 syl2anc 
 |-  ( ( ph /\ x e. dom F ) -> ( E ` x ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
223 222 fveq2d 
 |-  ( ( ph /\ x e. dom F ) -> ( F ` ( E ` x ) ) = ( F ` ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
224 fvex 
 |-  ( |_ ` ( ( B - x ) / T ) ) e. _V
225 eleq1 
 |-  ( k = ( |_ ` ( ( B - x ) / T ) ) -> ( k e. ZZ <-> ( |_ ` ( ( B - x ) / T ) ) e. ZZ ) )
226 225 anbi2d 
 |-  ( k = ( |_ ` ( ( B - x ) / T ) ) -> ( ( ( ph /\ x e. dom F ) /\ k e. ZZ ) <-> ( ( ph /\ x e. dom F ) /\ ( |_ ` ( ( B - x ) / T ) ) e. ZZ ) ) )
227 oveq1 
 |-  ( k = ( |_ ` ( ( B - x ) / T ) ) -> ( k x. T ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
228 227 oveq2d 
 |-  ( k = ( |_ ` ( ( B - x ) / T ) ) -> ( x + ( k x. T ) ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
229 228 fveq2d 
 |-  ( k = ( |_ ` ( ( B - x ) / T ) ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
230 229 eqeq1d 
 |-  ( k = ( |_ ` ( ( B - x ) / T ) ) -> ( ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) <-> ( F ` ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) = ( F ` x ) ) )
231 226 230 imbi12d 
 |-  ( k = ( |_ ` ( ( B - x ) / T ) ) -> ( ( ( ( ph /\ x e. dom F ) /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) ) <-> ( ( ( ph /\ x e. dom F ) /\ ( |_ ` ( ( B - x ) / T ) ) e. ZZ ) -> ( F ` ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) = ( F ` x ) ) ) )
232 224 231 15 vtocl 
 |-  ( ( ( ph /\ x e. dom F ) /\ ( |_ ` ( ( B - x ) / T ) ) e. ZZ ) -> ( F ` ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) = ( F ` x ) )
233 217 232 mpdan 
 |-  ( ( ph /\ x e. dom F ) -> ( F ` ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) = ( F ` x ) )
234 223 233 eqtr2d 
 |-  ( ( ph /\ x e. dom F ) -> ( F ` x ) = ( F ` ( E ` x ) ) )
235 234 fveq2d 
 |-  ( ( ph /\ x e. dom F ) -> ( abs ` ( F ` x ) ) = ( abs ` ( F ` ( E ` x ) ) ) )
236 235 adantlr 
 |-  ( ( ( ph /\ A. x e. ( ( A [,] B ) i^i dom F ) ( abs ` ( F ` x ) ) <_ y ) /\ x e. dom F ) -> ( abs ` ( F ` x ) ) = ( abs ` ( F ` ( E ` x ) ) ) )
237 fveq2 
 |-  ( x = w -> ( F ` x ) = ( F ` w ) )
238 237 fveq2d 
 |-  ( x = w -> ( abs ` ( F ` x ) ) = ( abs ` ( F ` w ) ) )
239 238 breq1d 
 |-  ( x = w -> ( ( abs ` ( F ` x ) ) <_ y <-> ( abs ` ( F ` w ) ) <_ y ) )
240 239 cbvralvw 
 |-  ( A. x e. ( ( A [,] B ) i^i dom F ) ( abs ` ( F ` x ) ) <_ y <-> A. w e. ( ( A [,] B ) i^i dom F ) ( abs ` ( F ` w ) ) <_ y )
241 240 biimpi 
 |-  ( A. x e. ( ( A [,] B ) i^i dom F ) ( abs ` ( F ` x ) ) <_ y -> A. w e. ( ( A [,] B ) i^i dom F ) ( abs ` ( F ` w ) ) <_ y )
242 241 ad2antlr 
 |-  ( ( ( ph /\ A. x e. ( ( A [,] B ) i^i dom F ) ( abs ` ( F ` x ) ) <_ y ) /\ x e. dom F ) -> A. w e. ( ( A [,] B ) i^i dom F ) ( abs ` ( F ` w ) ) <_ y )
243 iocssicc 
 |-  ( A (,] B ) C_ ( A [,] B )
244 3 adantr 
 |-  ( ( ph /\ x e. dom F ) -> A e. RR )
245 5 adantr 
 |-  ( ( ph /\ x e. dom F ) -> A < B )
246 id 
 |-  ( x = y -> x = y )
247 oveq2 
 |-  ( x = y -> ( B - x ) = ( B - y ) )
248 247 oveq1d 
 |-  ( x = y -> ( ( B - x ) / T ) = ( ( B - y ) / T ) )
249 248 fveq2d 
 |-  ( x = y -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - y ) / T ) ) )
250 249 oveq1d 
 |-  ( x = y -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - y ) / T ) ) x. T ) )
251 246 250 oveq12d 
 |-  ( x = y -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( y + ( ( |_ ` ( ( B - y ) / T ) ) x. T ) ) )
252 251 cbvmptv 
 |-  ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) = ( y e. RR |-> ( y + ( ( |_ ` ( ( B - y ) / T ) ) x. T ) ) )
253 17 252 eqtri 
 |-  E = ( y e. RR |-> ( y + ( ( |_ ` ( ( B - y ) / T ) ) x. T ) ) )
254 244 206 245 6 253 fourierdlem4 
 |-  ( ( ph /\ x e. dom F ) -> E : RR --> ( A (,] B ) )
255 254 205 ffvelcdmd 
 |-  ( ( ph /\ x e. dom F ) -> ( E ` x ) e. ( A (,] B ) )
256 243 255 sselid 
 |-  ( ( ph /\ x e. dom F ) -> ( E ` x ) e. ( A [,] B ) )
257 228 eleq1d 
 |-  ( k = ( |_ ` ( ( B - x ) / T ) ) -> ( ( x + ( k x. T ) ) e. dom F <-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. dom F ) )
258 226 257 imbi12d 
 |-  ( k = ( |_ ` ( ( B - x ) / T ) ) -> ( ( ( ( ph /\ x e. dom F ) /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. dom F ) <-> ( ( ( ph /\ x e. dom F ) /\ ( |_ ` ( ( B - x ) / T ) ) e. ZZ ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. dom F ) ) )
259 224 258 14 vtocl 
 |-  ( ( ( ph /\ x e. dom F ) /\ ( |_ ` ( ( B - x ) / T ) ) e. ZZ ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. dom F )
260 217 259 mpdan 
 |-  ( ( ph /\ x e. dom F ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. dom F )
261 222 260 eqeltrd 
 |-  ( ( ph /\ x e. dom F ) -> ( E ` x ) e. dom F )
262 256 261 elind 
 |-  ( ( ph /\ x e. dom F ) -> ( E ` x ) e. ( ( A [,] B ) i^i dom F ) )
263 262 adantlr 
 |-  ( ( ( ph /\ A. x e. ( ( A [,] B ) i^i dom F ) ( abs ` ( F ` x ) ) <_ y ) /\ x e. dom F ) -> ( E ` x ) e. ( ( A [,] B ) i^i dom F ) )
264 fveq2 
 |-  ( w = ( E ` x ) -> ( F ` w ) = ( F ` ( E ` x ) ) )
265 264 fveq2d 
 |-  ( w = ( E ` x ) -> ( abs ` ( F ` w ) ) = ( abs ` ( F ` ( E ` x ) ) ) )
266 265 breq1d 
 |-  ( w = ( E ` x ) -> ( ( abs ` ( F ` w ) ) <_ y <-> ( abs ` ( F ` ( E ` x ) ) ) <_ y ) )
267 266 rspccva 
 |-  ( ( A. w e. ( ( A [,] B ) i^i dom F ) ( abs ` ( F ` w ) ) <_ y /\ ( E ` x ) e. ( ( A [,] B ) i^i dom F ) ) -> ( abs ` ( F ` ( E ` x ) ) ) <_ y )
268 242 263 267 syl2anc 
 |-  ( ( ( ph /\ A. x e. ( ( A [,] B ) i^i dom F ) ( abs ` ( F ` x ) ) <_ y ) /\ x e. dom F ) -> ( abs ` ( F ` ( E ` x ) ) ) <_ y )
269 236 268 eqbrtrd 
 |-  ( ( ( ph /\ A. x e. ( ( A [,] B ) i^i dom F ) ( abs ` ( F ` x ) ) <_ y ) /\ x e. dom F ) -> ( abs ` ( F ` x ) ) <_ y )
270 269 ex 
 |-  ( ( ph /\ A. x e. ( ( A [,] B ) i^i dom F ) ( abs ` ( F ` x ) ) <_ y ) -> ( x e. dom F -> ( abs ` ( F ` x ) ) <_ y ) )
271 204 270 ralrimi 
 |-  ( ( ph /\ A. x e. ( ( A [,] B ) i^i dom F ) ( abs ` ( F ` x ) ) <_ y ) -> A. x e. dom F ( abs ` ( F ` x ) ) <_ y )
272 271 ex 
 |-  ( ph -> ( A. x e. ( ( A [,] B ) i^i dom F ) ( abs ` ( F ` x ) ) <_ y -> A. x e. dom F ( abs ` ( F ` x ) ) <_ y ) )
273 272 reximdv 
 |-  ( ph -> ( E. y e. RR A. x e. ( ( A [,] B ) i^i dom F ) ( abs ` ( F ` x ) ) <_ y -> E. y e. RR A. x e. dom F ( abs ` ( F ` x ) ) <_ y ) )
274 201 273 mpd 
 |-  ( ph -> E. y e. RR A. x e. dom F ( abs ` ( F ` x ) ) <_ y )