Metamath Proof Explorer

Theorem lo1mul

Description: The product of an eventually upper bounded function and a positive eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses o1add2.1 
|- ( ( ph /\ x e. A ) -> B e. V )
o1add2.2 
|- ( ( ph /\ x e. A ) -> C e. V )
lo1add.3 
|- ( ph -> ( x e. A |-> B ) e. <_O(1) )
lo1add.4 
|- ( ph -> ( x e. A |-> C ) e. <_O(1) )
lo1mul.5 
|- ( ( ph /\ x e. A ) -> 0 <_ B )
Assertion lo1mul 
|- ( ph -> ( x e. A |-> ( B x. C ) ) e. <_O(1) )

Proof

Step Hyp Ref Expression
1 o1add2.1 
 |-  ( ( ph /\ x e. A ) -> B e. V )
2 o1add2.2 
 |-  ( ( ph /\ x e. A ) -> C e. V )
3 lo1add.3 
 |-  ( ph -> ( x e. A |-> B ) e. <_O(1) )
4 lo1add.4 
 |-  ( ph -> ( x e. A |-> C ) e. <_O(1) )
5 lo1mul.5 
 |-  ( ( ph /\ x e. A ) -> 0 <_ B )
6 reeanv 
 |-  ( E. m e. RR E. n e. RR ( E. c e. RR A. x e. A ( c <_ x -> B <_ m ) /\ E. c e. RR A. x e. A ( c <_ x -> C <_ n ) ) <-> ( E. m e. RR E. c e. RR A. x e. A ( c <_ x -> B <_ m ) /\ E. n e. RR E. c e. RR A. x e. A ( c <_ x -> C <_ n ) ) )
7 1 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 lo1dm 
 |-  ( ( x e. A |-> B ) e. <_O(1) -> dom ( x e. A |-> B ) C_ RR )
11 3 10 syl 
 |-  ( ph -> dom ( x e. A |-> B ) C_ RR )
12 9 11 eqsstrrd 
 |-  ( ph -> A C_ RR )
13 12 adantr 
 |-  ( ( ph /\ ( m e. RR /\ n e. RR ) ) -> A C_ RR )
14 rexanre 
 |-  ( A C_ RR -> ( E. c e. RR A. x e. A ( c <_ x -> ( B <_ m /\ C <_ n ) ) <-> ( E. c e. RR A. x e. A ( c <_ x -> B <_ m ) /\ E. c e. RR A. x e. A ( c <_ x -> C <_ n ) ) ) )
15 13 14 syl 
 |-  ( ( ph /\ ( m e. RR /\ n e. RR ) ) -> ( E. c e. RR A. x e. A ( c <_ x -> ( B <_ m /\ C <_ n ) ) <-> ( E. c e. RR A. x e. A ( c <_ x -> B <_ m ) /\ E. c e. RR A. x e. A ( c <_ x -> C <_ n ) ) ) )
16 simprl 
 |-  ( ( ph /\ ( m e. RR /\ n e. RR ) ) -> m e. RR )
17 simprr 
 |-  ( ( ph /\ ( m e. RR /\ n e. RR ) ) -> n e. RR )
18 0re 
 |-  0 e. RR
19 ifcl 
 |-  ( ( n e. RR /\ 0 e. RR ) -> if ( 0 <_ n , n , 0 ) e. RR )
20 17 18 19 sylancl 
 |-  ( ( ph /\ ( m e. RR /\ n e. RR ) ) -> if ( 0 <_ n , n , 0 ) e. RR )
21 16 20 remulcld 
 |-  ( ( ph /\ ( m e. RR /\ n e. RR ) ) -> ( m x. if ( 0 <_ n , n , 0 ) ) e. RR )
22 simplrr 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> n e. RR )
23 max2 
 |-  ( ( 0 e. RR /\ n e. RR ) -> n <_ if ( 0 <_ n , n , 0 ) )
24 18 22 23 sylancr 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> n <_ if ( 0 <_ n , n , 0 ) )
25 2 4 lo1mptrcl 
 |-  ( ( ph /\ x e. A ) -> C e. RR )
26 25 adantlr 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> C e. RR )
27 22 18 19 sylancl 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> if ( 0 <_ n , n , 0 ) e. RR )
28 letr 
 |-  ( ( C e. RR /\ n e. RR /\ if ( 0 <_ n , n , 0 ) e. RR ) -> ( ( C <_ n /\ n <_ if ( 0 <_ n , n , 0 ) ) -> C <_ if ( 0 <_ n , n , 0 ) ) )
29 26 22 27 28 syl3anc 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> ( ( C <_ n /\ n <_ if ( 0 <_ n , n , 0 ) ) -> C <_ if ( 0 <_ n , n , 0 ) ) )
30 24 29 mpan2d 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> ( C <_ n -> C <_ if ( 0 <_ n , n , 0 ) ) )
31 1 3 lo1mptrcl 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
32 31 adantlr 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> B e. RR )
33 5 adantlr 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> 0 <_ B )
34 32 33 jca 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> ( B e. RR /\ 0 <_ B ) )
35 simplrl 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> m e. RR )
36 max1 
 |-  ( ( 0 e. RR /\ n e. RR ) -> 0 <_ if ( 0 <_ n , n , 0 ) )
37 18 22 36 sylancr 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> 0 <_ if ( 0 <_ n , n , 0 ) )
38 27 37 jca 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> ( if ( 0 <_ n , n , 0 ) e. RR /\ 0 <_ if ( 0 <_ n , n , 0 ) ) )
39 lemul12b 
 |-  ( ( ( ( B e. RR /\ 0 <_ B ) /\ m e. RR ) /\ ( C e. RR /\ ( if ( 0 <_ n , n , 0 ) e. RR /\ 0 <_ if ( 0 <_ n , n , 0 ) ) ) ) -> ( ( B <_ m /\ C <_ if ( 0 <_ n , n , 0 ) ) -> ( B x. C ) <_ ( m x. if ( 0 <_ n , n , 0 ) ) ) )
40 34 35 26 38 39 syl22anc 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> ( ( B <_ m /\ C <_ if ( 0 <_ n , n , 0 ) ) -> ( B x. C ) <_ ( m x. if ( 0 <_ n , n , 0 ) ) ) )
41 30 40 sylan2d 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> ( ( B <_ m /\ C <_ n ) -> ( B x. C ) <_ ( m x. if ( 0 <_ n , n , 0 ) ) ) )
42 41 imim2d 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> ( ( c <_ x -> ( B <_ m /\ C <_ n ) ) -> ( c <_ x -> ( B x. C ) <_ ( m x. if ( 0 <_ n , n , 0 ) ) ) ) )
43 42 ralimdva 
 |-  ( ( ph /\ ( m e. RR /\ n e. RR ) ) -> ( A. x e. A ( c <_ x -> ( B <_ m /\ C <_ n ) ) -> A. x e. A ( c <_ x -> ( B x. C ) <_ ( m x. if ( 0 <_ n , n , 0 ) ) ) ) )
44 breq2 
 |-  ( p = ( m x. if ( 0 <_ n , n , 0 ) ) -> ( ( B x. C ) <_ p <-> ( B x. C ) <_ ( m x. if ( 0 <_ n , n , 0 ) ) ) )
45 44 imbi2d 
 |-  ( p = ( m x. if ( 0 <_ n , n , 0 ) ) -> ( ( c <_ x -> ( B x. C ) <_ p ) <-> ( c <_ x -> ( B x. C ) <_ ( m x. if ( 0 <_ n , n , 0 ) ) ) ) )
46 45 ralbidv 
 |-  ( p = ( m x. if ( 0 <_ n , n , 0 ) ) -> ( A. x e. A ( c <_ x -> ( B x. C ) <_ p ) <-> A. x e. A ( c <_ x -> ( B x. C ) <_ ( m x. if ( 0 <_ n , n , 0 ) ) ) ) )
47 46 rspcev 
 |-  ( ( ( m x. if ( 0 <_ n , n , 0 ) ) e. RR /\ A. x e. A ( c <_ x -> ( B x. C ) <_ ( m x. if ( 0 <_ n , n , 0 ) ) ) ) -> E. p e. RR A. x e. A ( c <_ x -> ( B x. C ) <_ p ) )
48 21 43 47 syl6an 
 |-  ( ( ph /\ ( m e. RR /\ n e. RR ) ) -> ( A. x e. A ( c <_ x -> ( B <_ m /\ C <_ n ) ) -> E. p e. RR A. x e. A ( c <_ x -> ( B x. C ) <_ p ) ) )
49 48 reximdv 
 |-  ( ( ph /\ ( m e. RR /\ n e. RR ) ) -> ( E. c e. RR A. x e. A ( c <_ x -> ( B <_ m /\ C <_ n ) ) -> E. c e. RR E. p e. RR A. x e. A ( c <_ x -> ( B x. C ) <_ p ) ) )
50 15 49 sylbird 
 |-  ( ( ph /\ ( m e. RR /\ n e. RR ) ) -> ( ( E. c e. RR A. x e. A ( c <_ x -> B <_ m ) /\ E. c e. RR A. x e. A ( c <_ x -> C <_ n ) ) -> E. c e. RR E. p e. RR A. x e. A ( c <_ x -> ( B x. C ) <_ p ) ) )
51 50 rexlimdvva 
 |-  ( ph -> ( E. m e. RR E. n e. RR ( E. c e. RR A. x e. A ( c <_ x -> B <_ m ) /\ E. c e. RR A. x e. A ( c <_ x -> C <_ n ) ) -> E. c e. RR E. p e. RR A. x e. A ( c <_ x -> ( B x. C ) <_ p ) ) )
52 6 51 syl5bir 
 |-  ( ph -> ( ( E. m e. RR E. c e. RR A. x e. A ( c <_ x -> B <_ m ) /\ E. n e. RR E. c e. RR A. x e. A ( c <_ x -> C <_ n ) ) -> E. c e. RR E. p e. RR A. x e. A ( c <_ x -> ( B x. C ) <_ p ) ) )
53 12 31 ello1mpt 
 |-  ( ph -> ( ( x e. A |-> B ) e. <_O(1) <-> E. c e. RR E. m e. RR A. x e. A ( c <_ x -> B <_ m ) ) )
54 rexcom 
 |-  ( E. c e. RR E. m e. RR A. x e. A ( c <_ x -> B <_ m ) <-> E. m e. RR E. c e. RR A. x e. A ( c <_ x -> B <_ m ) )
55 53 54 bitrdi 
 |-  ( ph -> ( ( x e. A |-> B ) e. <_O(1) <-> E. m e. RR E. c e. RR A. x e. A ( c <_ x -> B <_ m ) ) )
56 12 25 ello1mpt 
 |-  ( ph -> ( ( x e. A |-> C ) e. <_O(1) <-> E. c e. RR E. n e. RR A. x e. A ( c <_ x -> C <_ n ) ) )
57 rexcom 
 |-  ( E. c e. RR E. n e. RR A. x e. A ( c <_ x -> C <_ n ) <-> E. n e. RR E. c e. RR A. x e. A ( c <_ x -> C <_ n ) )
58 56 57 bitrdi 
 |-  ( ph -> ( ( x e. A |-> C ) e. <_O(1) <-> E. n e. RR E. c e. RR A. x e. A ( c <_ x -> C <_ n ) ) )
59 55 58 anbi12d 
 |-  ( ph -> ( ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> C ) e. <_O(1) ) <-> ( E. m e. RR E. c e. RR A. x e. A ( c <_ x -> B <_ m ) /\ E. n e. RR E. c e. RR A. x e. A ( c <_ x -> C <_ n ) ) ) )
60 31 25 remulcld 
 |-  ( ( ph /\ x e. A ) -> ( B x. C ) e. RR )
61 12 60 ello1mpt 
 |-  ( ph -> ( ( x e. A |-> ( B x. C ) ) e. <_O(1) <-> E. c e. RR E. p e. RR A. x e. A ( c <_ x -> ( B x. C ) <_ p ) ) )
62 52 59 61 3imtr4d 
 |-  ( ph -> ( ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> C ) e. <_O(1) ) -> ( x e. A |-> ( B x. C ) ) e. <_O(1) ) )
63 3 4 62 mp2and 
 |-  ( ph -> ( x e. A |-> ( B x. C ) ) e. <_O(1) )