Metamath Proof Explorer

Theorem o1cxp

Description: An eventually bounded function taken to a nonnegative power is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Hypotheses o1cxp.1 
|- ( ph -> C e. CC )
o1cxp.2 
|- ( ph -> 0 <_ ( Re ` C ) )
o1cxp.3 
|- ( ( ph /\ x e. A ) -> B e. V )
o1cxp.4 
|- ( ph -> ( x e. A |-> B ) e. O(1) )
Assertion o1cxp 
|- ( ph -> ( x e. A |-> ( B ^c C ) ) e. O(1) )

Proof

Step Hyp Ref Expression
1 o1cxp.1 
 |-  ( ph -> C e. CC )
2 o1cxp.2 
 |-  ( ph -> 0 <_ ( Re ` C ) )
3 o1cxp.3 
 |-  ( ( ph /\ x e. A ) -> B e. V )
4 o1cxp.4 
 |-  ( ph -> ( x e. A |-> B ) e. O(1) )
5 o1f 
 |-  ( ( x e. A |-> B ) e. O(1) -> ( x e. A |-> B ) : dom ( x e. A |-> B ) --> CC )
6 4 5 syl 
 |-  ( ph -> ( x e. A |-> B ) : dom ( x e. A |-> B ) --> CC )
7 3 ralrimiva 
 |-  ( ph -> A. x e. A B e. V )
8 dmmptg 
 |-  ( A. x e. A B e. V -> dom ( x e. A |-> B ) = A )
9 7 8 syl 
 |-  ( ph -> dom ( x e. A |-> B ) = A )
10 9 feq2d 
 |-  ( ph -> ( ( x e. A |-> B ) : dom ( x e. A |-> B ) --> CC <-> ( x e. A |-> B ) : A --> CC ) )
11 6 10 mpbid 
 |-  ( ph -> ( x e. A |-> B ) : A --> CC )
12 o1bdd 
 |-  ( ( ( x e. A |-> B ) e. O(1) /\ ( x e. A |-> B ) : A --> CC ) -> E. y e. RR E. m e. RR A. z e. A ( y <_ z -> ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m ) )
13 4 11 12 syl2anc 
 |-  ( ph -> E. y e. RR E. m e. RR A. z e. A ( y <_ z -> ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m ) )
14 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
15 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
16 15 fvmpt2 
 |-  ( ( x e. A /\ B e. V ) -> ( ( x e. A |-> B ) ` x ) = B )
17 14 3 16 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B )
18 17 oveq1d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> B ) ` x ) ^c C ) = ( B ^c C ) )
19 ovex 
 |-  ( B ^c C ) e. _V
20 eqid 
 |-  ( x e. A |-> ( B ^c C ) ) = ( x e. A |-> ( B ^c C ) )
21 20 fvmpt2 
 |-  ( ( x e. A /\ ( B ^c C ) e. _V ) -> ( ( x e. A |-> ( B ^c C ) ) ` x ) = ( B ^c C ) )
22 14 19 21 sylancl 
 |-  ( ( ph /\ x e. A ) -> ( ( x e. A |-> ( B ^c C ) ) ` x ) = ( B ^c C ) )
23 18 22 eqtr4d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> B ) ` x ) ^c C ) = ( ( x e. A |-> ( B ^c C ) ) ` x ) )
24 23 ralrimiva 
 |-  ( ph -> A. x e. A ( ( ( x e. A |-> B ) ` x ) ^c C ) = ( ( x e. A |-> ( B ^c C ) ) ` x ) )
25 nfv 
 |-  F/ z ( ( ( x e. A |-> B ) ` x ) ^c C ) = ( ( x e. A |-> ( B ^c C ) ) ` x )
26 nffvmpt1 
 |-  F/_ x ( ( x e. A |-> B ) ` z )
27 nfcv 
 |-  F/_ x ^c
28 nfcv 
 |-  F/_ x C
29 26 27 28 nfov 
 |-  F/_ x ( ( ( x e. A |-> B ) ` z ) ^c C )
30 nffvmpt1 
 |-  F/_ x ( ( x e. A |-> ( B ^c C ) ) ` z )
31 29 30 nfeq 
 |-  F/ x ( ( ( x e. A |-> B ) ` z ) ^c C ) = ( ( x e. A |-> ( B ^c C ) ) ` z )
32 fveq2 
 |-  ( x = z -> ( ( x e. A |-> B ) ` x ) = ( ( x e. A |-> B ) ` z ) )
33 32 oveq1d 
 |-  ( x = z -> ( ( ( x e. A |-> B ) ` x ) ^c C ) = ( ( ( x e. A |-> B ) ` z ) ^c C ) )
34 fveq2 
 |-  ( x = z -> ( ( x e. A |-> ( B ^c C ) ) ` x ) = ( ( x e. A |-> ( B ^c C ) ) ` z ) )
35 33 34 eqeq12d 
 |-  ( x = z -> ( ( ( ( x e. A |-> B ) ` x ) ^c C ) = ( ( x e. A |-> ( B ^c C ) ) ` x ) <-> ( ( ( x e. A |-> B ) ` z ) ^c C ) = ( ( x e. A |-> ( B ^c C ) ) ` z ) ) )
36 25 31 35 cbvralw 
 |-  ( A. x e. A ( ( ( x e. A |-> B ) ` x ) ^c C ) = ( ( x e. A |-> ( B ^c C ) ) ` x ) <-> A. z e. A ( ( ( x e. A |-> B ) ` z ) ^c C ) = ( ( x e. A |-> ( B ^c C ) ) ` z ) )
37 24 36 sylib 
 |-  ( ph -> A. z e. A ( ( ( x e. A |-> B ) ` z ) ^c C ) = ( ( x e. A |-> ( B ^c C ) ) ` z ) )
38 37 r19.21bi 
 |-  ( ( ph /\ z e. A ) -> ( ( ( x e. A |-> B ) ` z ) ^c C ) = ( ( x e. A |-> ( B ^c C ) ) ` z ) )
39 38 ad2ant2r 
 |-  ( ( ( ph /\ ( y e. RR /\ m e. RR ) ) /\ ( z e. A /\ ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m ) ) -> ( ( ( x e. A |-> B ) ` z ) ^c C ) = ( ( x e. A |-> ( B ^c C ) ) ` z ) )
40 39 fveq2d 
 |-  ( ( ( ph /\ ( y e. RR /\ m e. RR ) ) /\ ( z e. A /\ ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m ) ) -> ( abs ` ( ( ( x e. A |-> B ) ` z ) ^c C ) ) = ( abs ` ( ( x e. A |-> ( B ^c C ) ) ` z ) ) )
41 11 ffvelrnda 
 |-  ( ( ph /\ z e. A ) -> ( ( x e. A |-> B ) ` z ) e. CC )
42 41 ad2ant2r 
 |-  ( ( ( ph /\ ( y e. RR /\ m e. RR ) ) /\ ( z e. A /\ ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m ) ) -> ( ( x e. A |-> B ) ` z ) e. CC )
43 1 ad2antrr 
 |-  ( ( ( ph /\ ( y e. RR /\ m e. RR ) ) /\ ( z e. A /\ ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m ) ) -> C e. CC )
44 2 ad2antrr 
 |-  ( ( ( ph /\ ( y e. RR /\ m e. RR ) ) /\ ( z e. A /\ ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m ) ) -> 0 <_ ( Re ` C ) )
45 simprr 
 |-  ( ( ph /\ ( y e. RR /\ m e. RR ) ) -> m e. RR )
46 0re 
 |-  0 e. RR
47 ifcl 
 |-  ( ( m e. RR /\ 0 e. RR ) -> if ( 0 <_ m , m , 0 ) e. RR )
48 45 46 47 sylancl 
 |-  ( ( ph /\ ( y e. RR /\ m e. RR ) ) -> if ( 0 <_ m , m , 0 ) e. RR )
49 48 adantr 
 |-  ( ( ( ph /\ ( y e. RR /\ m e. RR ) ) /\ ( z e. A /\ ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m ) ) -> if ( 0 <_ m , m , 0 ) e. RR )
50 42 abscld 
 |-  ( ( ( ph /\ ( y e. RR /\ m e. RR ) ) /\ ( z e. A /\ ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m ) ) -> ( abs ` ( ( x e. A |-> B ) ` z ) ) e. RR )
51 45 adantr 
 |-  ( ( ( ph /\ ( y e. RR /\ m e. RR ) ) /\ ( z e. A /\ ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m ) ) -> m e. RR )
52 simprr 
 |-  ( ( ( ph /\ ( y e. RR /\ m e. RR ) ) /\ ( z e. A /\ ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m ) ) -> ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m )
53 max2 
 |-  ( ( 0 e. RR /\ m e. RR ) -> m <_ if ( 0 <_ m , m , 0 ) )
54 46 45 53 sylancr 
 |-  ( ( ph /\ ( y e. RR /\ m e. RR ) ) -> m <_ if ( 0 <_ m , m , 0 ) )
55 54 adantr 
 |-  ( ( ( ph /\ ( y e. RR /\ m e. RR ) ) /\ ( z e. A /\ ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m ) ) -> m <_ if ( 0 <_ m , m , 0 ) )
56 50 51 49 52 55 letrd 
 |-  ( ( ( ph /\ ( y e. RR /\ m e. RR ) ) /\ ( z e. A /\ ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m ) ) -> ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ if ( 0 <_ m , m , 0 ) )
57 42 43 44 49 56 abscxpbnd 
 |-  ( ( ( ph /\ ( y e. RR /\ m e. RR ) ) /\ ( z e. A /\ ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m ) ) -> ( abs ` ( ( ( x e. A |-> B ) ` z ) ^c C ) ) <_ ( ( if ( 0 <_ m , m , 0 ) ^c ( Re ` C ) ) x. ( exp ` ( ( abs ` C ) x. _pi ) ) ) )
58 40 57 eqbrtrrd 
 |-  ( ( ( ph /\ ( y e. RR /\ m e. RR ) ) /\ ( z e. A /\ ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m ) ) -> ( abs ` ( ( x e. A |-> ( B ^c C ) ) ` z ) ) <_ ( ( if ( 0 <_ m , m , 0 ) ^c ( Re ` C ) ) x. ( exp ` ( ( abs ` C ) x. _pi ) ) ) )
59 58 expr 
 |-  ( ( ( ph /\ ( y e. RR /\ m e. RR ) ) /\ z e. A ) -> ( ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m -> ( abs ` ( ( x e. A |-> ( B ^c C ) ) ` z ) ) <_ ( ( if ( 0 <_ m , m , 0 ) ^c ( Re ` C ) ) x. ( exp ` ( ( abs ` C ) x. _pi ) ) ) ) )
60 59 imim2d 
 |-  ( ( ( ph /\ ( y e. RR /\ m e. RR ) ) /\ z e. A ) -> ( ( y <_ z -> ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m ) -> ( y <_ z -> ( abs ` ( ( x e. A |-> ( B ^c C ) ) ` z ) ) <_ ( ( if ( 0 <_ m , m , 0 ) ^c ( Re ` C ) ) x. ( exp ` ( ( abs ` C ) x. _pi ) ) ) ) ) )
61 60 ralimdva 
 |-  ( ( ph /\ ( y e. RR /\ m e. RR ) ) -> ( A. z e. A ( y <_ z -> ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m ) -> A. z e. A ( y <_ z -> ( abs ` ( ( x e. A |-> ( B ^c C ) ) ` z ) ) <_ ( ( if ( 0 <_ m , m , 0 ) ^c ( Re ` C ) ) x. ( exp ` ( ( abs ` C ) x. _pi ) ) ) ) ) )
62 3 4 o1mptrcl 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
63 1 adantr 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
64 62 63 cxpcld 
 |-  ( ( ph /\ x e. A ) -> ( B ^c C ) e. CC )
65 64 fmpttd 
 |-  ( ph -> ( x e. A |-> ( B ^c C ) ) : A --> CC )
66 65 adantr 
 |-  ( ( ph /\ ( y e. RR /\ m e. RR ) ) -> ( x e. A |-> ( B ^c C ) ) : A --> CC )
67 o1dm 
 |-  ( ( x e. A |-> B ) e. O(1) -> dom ( x e. A |-> B ) C_ RR )
68 4 67 syl 
 |-  ( ph -> dom ( x e. A |-> B ) C_ RR )
69 9 68 eqsstrrd 
 |-  ( ph -> A C_ RR )
70 69 adantr 
 |-  ( ( ph /\ ( y e. RR /\ m e. RR ) ) -> A C_ RR )
71 simprl 
 |-  ( ( ph /\ ( y e. RR /\ m e. RR ) ) -> y e. RR )
72 max1 
 |-  ( ( 0 e. RR /\ m e. RR ) -> 0 <_ if ( 0 <_ m , m , 0 ) )
73 46 45 72 sylancr 
 |-  ( ( ph /\ ( y e. RR /\ m e. RR ) ) -> 0 <_ if ( 0 <_ m , m , 0 ) )
74 1 adantr 
 |-  ( ( ph /\ ( y e. RR /\ m e. RR ) ) -> C e. CC )
75 74 recld 
 |-  ( ( ph /\ ( y e. RR /\ m e. RR ) ) -> ( Re ` C ) e. RR )
76 48 73 75 recxpcld 
 |-  ( ( ph /\ ( y e. RR /\ m e. RR ) ) -> ( if ( 0 <_ m , m , 0 ) ^c ( Re ` C ) ) e. RR )
77 74 abscld 
 |-  ( ( ph /\ ( y e. RR /\ m e. RR ) ) -> ( abs ` C ) e. RR )
78 pire 
 |-  _pi e. RR
79 remulcl 
 |-  ( ( ( abs ` C ) e. RR /\ _pi e. RR ) -> ( ( abs ` C ) x. _pi ) e. RR )
80 77 78 79 sylancl 
 |-  ( ( ph /\ ( y e. RR /\ m e. RR ) ) -> ( ( abs ` C ) x. _pi ) e. RR )
81 80 reefcld 
 |-  ( ( ph /\ ( y e. RR /\ m e. RR ) ) -> ( exp ` ( ( abs ` C ) x. _pi ) ) e. RR )
82 76 81 remulcld 
 |-  ( ( ph /\ ( y e. RR /\ m e. RR ) ) -> ( ( if ( 0 <_ m , m , 0 ) ^c ( Re ` C ) ) x. ( exp ` ( ( abs ` C ) x. _pi ) ) ) e. RR )
83 elo12r 
 |-  ( ( ( ( x e. A |-> ( B ^c C ) ) : A --> CC /\ A C_ RR ) /\ ( y e. RR /\ ( ( if ( 0 <_ m , m , 0 ) ^c ( Re ` C ) ) x. ( exp ` ( ( abs ` C ) x. _pi ) ) ) e. RR ) /\ A. z e. A ( y <_ z -> ( abs ` ( ( x e. A |-> ( B ^c C ) ) ` z ) ) <_ ( ( if ( 0 <_ m , m , 0 ) ^c ( Re ` C ) ) x. ( exp ` ( ( abs ` C ) x. _pi ) ) ) ) ) -> ( x e. A |-> ( B ^c C ) ) e. O(1) )
84 83 3expia 
 |-  ( ( ( ( x e. A |-> ( B ^c C ) ) : A --> CC /\ A C_ RR ) /\ ( y e. RR /\ ( ( if ( 0 <_ m , m , 0 ) ^c ( Re ` C ) ) x. ( exp ` ( ( abs ` C ) x. _pi ) ) ) e. RR ) ) -> ( A. z e. A ( y <_ z -> ( abs ` ( ( x e. A |-> ( B ^c C ) ) ` z ) ) <_ ( ( if ( 0 <_ m , m , 0 ) ^c ( Re ` C ) ) x. ( exp ` ( ( abs ` C ) x. _pi ) ) ) ) -> ( x e. A |-> ( B ^c C ) ) e. O(1) ) )
85 66 70 71 82 84 syl22anc 
 |-  ( ( ph /\ ( y e. RR /\ m e. RR ) ) -> ( A. z e. A ( y <_ z -> ( abs ` ( ( x e. A |-> ( B ^c C ) ) ` z ) ) <_ ( ( if ( 0 <_ m , m , 0 ) ^c ( Re ` C ) ) x. ( exp ` ( ( abs ` C ) x. _pi ) ) ) ) -> ( x e. A |-> ( B ^c C ) ) e. O(1) ) )
86 61 85 syld 
 |-  ( ( ph /\ ( y e. RR /\ m e. RR ) ) -> ( A. z e. A ( y <_ z -> ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m ) -> ( x e. A |-> ( B ^c C ) ) e. O(1) ) )
87 86 rexlimdvva 
 |-  ( ph -> ( E. y e. RR E. m e. RR A. z e. A ( y <_ z -> ( abs ` ( ( x e. A |-> B ) ` z ) ) <_ m ) -> ( x e. A |-> ( B ^c C ) ) e. O(1) ) )
88 13 87 mpd 
 |-  ( ph -> ( x e. A |-> ( B ^c C ) ) e. O(1) )