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