Metamath Proof Explorer

Theorem lo1add

Description: The sum of two eventually upper bounded functions 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) )
Assertion lo1add 
|- ( ph -> ( x e. A |-> ( B + 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 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 ) ) )
6 1 ralrimiva 
 |-  ( ph -> A. x e. A B e. V )
7 dmmptg 
 |-  ( A. x e. A B e. V -> dom ( x e. A |-> B ) = A )
8 6 7 syl 
 |-  ( ph -> dom ( x e. A |-> B ) = A )
9 lo1dm 
 |-  ( ( x e. A |-> B ) e. <_O(1) -> dom ( x e. A |-> B ) C_ RR )
10 3 9 syl 
 |-  ( ph -> dom ( x e. A |-> B ) C_ RR )
11 8 10 eqsstrrd 
 |-  ( ph -> A C_ RR )
12 11 adantr 
 |-  ( ( ph /\ ( m e. RR /\ n e. RR ) ) -> A C_ RR )
13 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 ) ) ) )
14 12 13 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 ) ) ) )
15 readdcl 
 |-  ( ( m e. RR /\ n e. RR ) -> ( m + n ) e. RR )
16 15 adantl 
 |-  ( ( ph /\ ( m e. RR /\ n e. RR ) ) -> ( m + n ) e. RR )
17 1 3 lo1mptrcl 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
18 17 adantlr 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> B e. RR )
19 2 4 lo1mptrcl 
 |-  ( ( ph /\ x e. A ) -> C e. RR )
20 19 adantlr 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> C e. RR )
21 simplrl 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> m e. RR )
22 simplrr 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> n e. RR )
23 le2add 
 |-  ( ( ( B e. RR /\ C e. RR ) /\ ( m e. RR /\ n e. RR ) ) -> ( ( B <_ m /\ C <_ n ) -> ( B + C ) <_ ( m + n ) ) )
24 18 20 21 22 23 syl22anc 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> ( ( B <_ m /\ C <_ n ) -> ( B + C ) <_ ( m + n ) ) )
25 24 imim2d 
 |-  ( ( ( ph /\ ( m e. RR /\ n e. RR ) ) /\ x e. A ) -> ( ( c <_ x -> ( B <_ m /\ C <_ n ) ) -> ( c <_ x -> ( B + C ) <_ ( m + n ) ) ) )
26 25 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 + C ) <_ ( m + n ) ) ) )
27 breq2 
 |-  ( p = ( m + n ) -> ( ( B + C ) <_ p <-> ( B + C ) <_ ( m + n ) ) )
28 27 imbi2d 
 |-  ( p = ( m + n ) -> ( ( c <_ x -> ( B + C ) <_ p ) <-> ( c <_ x -> ( B + C ) <_ ( m + n ) ) ) )
29 28 ralbidv 
 |-  ( p = ( m + n ) -> ( A. x e. A ( c <_ x -> ( B + C ) <_ p ) <-> A. x e. A ( c <_ x -> ( B + C ) <_ ( m + n ) ) ) )
30 29 rspcev 
 |-  ( ( ( m + n ) e. RR /\ A. x e. A ( c <_ x -> ( B + C ) <_ ( m + n ) ) ) -> E. p e. RR A. x e. A ( c <_ x -> ( B + C ) <_ p ) )
31 16 26 30 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 + C ) <_ p ) ) )
32 31 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 + C ) <_ p ) ) )
33 14 32 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 + C ) <_ p ) ) )
34 33 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 + C ) <_ p ) ) )
35 5 34 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 + C ) <_ p ) ) )
36 11 17 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 ) ) )
37 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 ) )
38 36 37 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 ) ) )
39 11 19 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 ) ) )
40 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 ) )
41 39 40 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 ) ) )
42 38 41 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 ) ) ) )
43 17 19 readdcld 
 |-  ( ( ph /\ x e. A ) -> ( B + C ) e. RR )
44 11 43 ello1mpt 
 |-  ( ph -> ( ( x e. A |-> ( B + C ) ) e. <_O(1) <-> E. c e. RR E. p e. RR A. x e. A ( c <_ x -> ( B + C ) <_ p ) ) )
45 35 42 44 3imtr4d 
 |-  ( ph -> ( ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> C ) e. <_O(1) ) -> ( x e. A |-> ( B + C ) ) e. <_O(1) ) )
46 3 4 45 mp2and 
 |-  ( ph -> ( x e. A |-> ( B + C ) ) e. <_O(1) )