Metamath Proof Explorer

Theorem ulmbdd

Description: A uniform limit of bounded functions is bounded. (Contributed by Mario Carneiro, 27-Feb-2015)

Ref Expression
Hypotheses ulmbdd.z 
|- Z = ( ZZ>= ` M )
ulmbdd.m 
|- ( ph -> M e. ZZ )
ulmbdd.f 
|- ( ph -> F : Z --> ( CC ^m S ) )
ulmbdd.b 
|- ( ( ph /\ k e. Z ) -> E. x e. RR A. z e. S ( abs ` ( ( F ` k ) ` z ) ) <_ x )
ulmbdd.u 
|- ( ph -> F ( ~~>u ` S ) G )
Assertion ulmbdd 
|- ( ph -> E. x e. RR A. z e. S ( abs ` ( G ` z ) ) <_ x )

Proof

Step Hyp Ref Expression
1 ulmbdd.z 
 |-  Z = ( ZZ>= ` M )
2 ulmbdd.m 
 |-  ( ph -> M e. ZZ )
3 ulmbdd.f 
 |-  ( ph -> F : Z --> ( CC ^m S ) )
4 ulmbdd.b 
 |-  ( ( ph /\ k e. Z ) -> E. x e. RR A. z e. S ( abs ` ( ( F ` k ) ` z ) ) <_ x )
5 ulmbdd.u 
 |-  ( ph -> F ( ~~>u ` S ) G )
6 eqidd 
 |-  ( ( ph /\ ( k e. Z /\ z e. S ) ) -> ( ( F ` k ) ` z ) = ( ( F ` k ) ` z ) )
7 eqidd 
 |-  ( ( ph /\ z e. S ) -> ( G ` z ) = ( G ` z ) )
8 1rp 
 |-  1 e. RR+
9 8 a1i 
 |-  ( ph -> 1 e. RR+ )
10 1 2 3 6 7 5 9 ulmi 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 )
11 1 r19.2uz 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 -> E. k e. Z A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 )
12 r19.26 
 |-  ( A. z e. S ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) <-> ( A. z e. S ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) )
13 peano2re 
 |-  ( x e. RR -> ( x + 1 ) e. RR )
14 13 adantl 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. RR ) -> ( x + 1 ) e. RR )
15 ulmcl 
 |-  ( F ( ~~>u ` S ) G -> G : S --> CC )
16 5 15 syl 
 |-  ( ph -> G : S --> CC )
17 16 ad3antrrr 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> G : S --> CC )
18 simprl 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> z e. S )
19 17 18 ffvelcdmd 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( G ` z ) e. CC )
20 19 abscld 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( abs ` ( G ` z ) ) e. RR )
21 3 ad3antrrr 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> F : Z --> ( CC ^m S ) )
22 simpllr 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> k e. Z )
23 21 22 ffvelcdmd 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( F ` k ) e. ( CC ^m S ) )
24 elmapi 
 |-  ( ( F ` k ) e. ( CC ^m S ) -> ( F ` k ) : S --> CC )
25 23 24 syl 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( F ` k ) : S --> CC )
26 25 18 ffvelcdmd 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( ( F ` k ) ` z ) e. CC )
27 26 abscld 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( abs ` ( ( F ` k ) ` z ) ) e. RR )
28 19 26 subcld 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( ( G ` z ) - ( ( F ` k ) ` z ) ) e. CC )
29 28 abscld 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( abs ` ( ( G ` z ) - ( ( F ` k ) ` z ) ) ) e. RR )
30 27 29 readdcld 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( ( abs ` ( ( F ` k ) ` z ) ) + ( abs ` ( ( G ` z ) - ( ( F ` k ) ` z ) ) ) ) e. RR )
31 14 adantr 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( x + 1 ) e. RR )
32 26 19 pncan3d 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( ( ( F ` k ) ` z ) + ( ( G ` z ) - ( ( F ` k ) ` z ) ) ) = ( G ` z ) )
33 32 fveq2d 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( abs ` ( ( ( F ` k ) ` z ) + ( ( G ` z ) - ( ( F ` k ) ` z ) ) ) ) = ( abs ` ( G ` z ) ) )
34 26 28 abstrid 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( abs ` ( ( ( F ` k ) ` z ) + ( ( G ` z ) - ( ( F ` k ) ` z ) ) ) ) <_ ( ( abs ` ( ( F ` k ) ` z ) ) + ( abs ` ( ( G ` z ) - ( ( F ` k ) ` z ) ) ) ) )
35 33 34 eqbrtrrd 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( abs ` ( G ` z ) ) <_ ( ( abs ` ( ( F ` k ) ` z ) ) + ( abs ` ( ( G ` z ) - ( ( F ` k ) ` z ) ) ) ) )
36 simplr 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> x e. RR )
37 1re 
 |-  1 e. RR
38 37 a1i 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> 1 e. RR )
39 simprrl 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( abs ` ( ( F ` k ) ` z ) ) <_ x )
40 19 26 abssubd 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( abs ` ( ( G ` z ) - ( ( F ` k ) ` z ) ) ) = ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) )
41 simprrr 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 )
42 40 41 eqbrtrd 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( abs ` ( ( G ` z ) - ( ( F ` k ) ` z ) ) ) < 1 )
43 ltle 
 |-  ( ( ( abs ` ( ( G ` z ) - ( ( F ` k ) ` z ) ) ) e. RR /\ 1 e. RR ) -> ( ( abs ` ( ( G ` z ) - ( ( F ` k ) ` z ) ) ) < 1 -> ( abs ` ( ( G ` z ) - ( ( F ` k ) ` z ) ) ) <_ 1 ) )
44 29 37 43 sylancl 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( ( abs ` ( ( G ` z ) - ( ( F ` k ) ` z ) ) ) < 1 -> ( abs ` ( ( G ` z ) - ( ( F ` k ) ` z ) ) ) <_ 1 ) )
45 42 44 mpd 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( abs ` ( ( G ` z ) - ( ( F ` k ) ` z ) ) ) <_ 1 )
46 27 29 36 38 39 45 le2addd 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( ( abs ` ( ( F ` k ) ` z ) ) + ( abs ` ( ( G ` z ) - ( ( F ` k ) ` z ) ) ) ) <_ ( x + 1 ) )
47 20 30 31 35 46 letrd 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ ( z e. S /\ ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) ) ) -> ( abs ` ( G ` z ) ) <_ ( x + 1 ) )
48 47 expr 
 |-  ( ( ( ( ph /\ k e. Z ) /\ x e. RR ) /\ z e. S ) -> ( ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) -> ( abs ` ( G ` z ) ) <_ ( x + 1 ) ) )
49 48 ralimdva 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. RR ) -> ( A. z e. S ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) -> A. z e. S ( abs ` ( G ` z ) ) <_ ( x + 1 ) ) )
50 brralrspcev 
 |-  ( ( ( x + 1 ) e. RR /\ A. z e. S ( abs ` ( G ` z ) ) <_ ( x + 1 ) ) -> E. y e. RR A. z e. S ( abs ` ( G ` z ) ) <_ y )
51 14 49 50 syl6an 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. RR ) -> ( A. z e. S ( ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) -> E. y e. RR A. z e. S ( abs ` ( G ` z ) ) <_ y ) )
52 12 51 biimtrrid 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. RR ) -> ( ( A. z e. S ( abs ` ( ( F ` k ) ` z ) ) <_ x /\ A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 ) -> E. y e. RR A. z e. S ( abs ` ( G ` z ) ) <_ y ) )
53 52 expd 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. RR ) -> ( A. z e. S ( abs ` ( ( F ` k ) ` z ) ) <_ x -> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 -> E. y e. RR A. z e. S ( abs ` ( G ` z ) ) <_ y ) ) )
54 53 rexlimdva 
 |-  ( ( ph /\ k e. Z ) -> ( E. x e. RR A. z e. S ( abs ` ( ( F ` k ) ` z ) ) <_ x -> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 -> E. y e. RR A. z e. S ( abs ` ( G ` z ) ) <_ y ) ) )
55 4 54 mpd 
 |-  ( ( ph /\ k e. Z ) -> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 -> E. y e. RR A. z e. S ( abs ` ( G ` z ) ) <_ y ) )
56 breq2 
 |-  ( y = x -> ( ( abs ` ( G ` z ) ) <_ y <-> ( abs ` ( G ` z ) ) <_ x ) )
57 56 ralbidv 
 |-  ( y = x -> ( A. z e. S ( abs ` ( G ` z ) ) <_ y <-> A. z e. S ( abs ` ( G ` z ) ) <_ x ) )
58 57 cbvrexvw 
 |-  ( E. y e. RR A. z e. S ( abs ` ( G ` z ) ) <_ y <-> E. x e. RR A. z e. S ( abs ` ( G ` z ) ) <_ x )
59 55 58 imbitrdi 
 |-  ( ( ph /\ k e. Z ) -> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 -> E. x e. RR A. z e. S ( abs ` ( G ` z ) ) <_ x ) )
60 59 rexlimdva 
 |-  ( ph -> ( E. k e. Z A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 -> E. x e. RR A. z e. S ( abs ` ( G ` z ) ) <_ x ) )
61 11 60 syl5 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < 1 -> E. x e. RR A. z e. S ( abs ` ( G ` z ) ) <_ x ) )
62 10 61 mpd 
 |-  ( ph -> E. x e. RR A. z e. S ( abs ` ( G ` z ) ) <_ x )