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