Metamath Proof Explorer

Theorem icco1

Description: Derive eventual boundedness from separate upper and lower eventual bounds. (Contributed by Mario Carneiro, 15-Apr-2016)

Ref Expression
Hypotheses icco1.1 
|- ( ph -> A C_ RR )
icco1.2 
|- ( ( ph /\ x e. A ) -> B e. RR )
icco1.3 
|- ( ph -> C e. RR )
icco1.4 
|- ( ph -> M e. RR )
icco1.5 
|- ( ph -> N e. RR )
icco1.6 
|- ( ( ph /\ ( x e. A /\ C <_ x ) ) -> B e. ( M [,] N ) )
Assertion icco1 
|- ( ph -> ( x e. A |-> B ) e. O(1) )

Proof

Step Hyp Ref Expression
1 icco1.1 
 |-  ( ph -> A C_ RR )
2 icco1.2 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
3 icco1.3 
 |-  ( ph -> C e. RR )
4 icco1.4 
 |-  ( ph -> M e. RR )
5 icco1.5 
 |-  ( ph -> N e. RR )
6 icco1.6 
 |-  ( ( ph /\ ( x e. A /\ C <_ x ) ) -> B e. ( M [,] N ) )
7 elicc2 
 |-  ( ( M e. RR /\ N e. RR ) -> ( B e. ( M [,] N ) <-> ( B e. RR /\ M <_ B /\ B <_ N ) ) )
8 4 5 7 syl2anc 
 |-  ( ph -> ( B e. ( M [,] N ) <-> ( B e. RR /\ M <_ B /\ B <_ N ) ) )
9 8 adantr 
 |-  ( ( ph /\ ( x e. A /\ C <_ x ) ) -> ( B e. ( M [,] N ) <-> ( B e. RR /\ M <_ B /\ B <_ N ) ) )
10 6 9 mpbid 
 |-  ( ( ph /\ ( x e. A /\ C <_ x ) ) -> ( B e. RR /\ M <_ B /\ B <_ N ) )
11 10 simp3d 
 |-  ( ( ph /\ ( x e. A /\ C <_ x ) ) -> B <_ N )
12 1 2 3 5 11 ello1d 
 |-  ( ph -> ( x e. A |-> B ) e. <_O(1) )
13 2 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u B e. RR )
14 4 renegcld 
 |-  ( ph -> -u M e. RR )
15 10 simp2d 
 |-  ( ( ph /\ ( x e. A /\ C <_ x ) ) -> M <_ B )
16 4 adantr 
 |-  ( ( ph /\ ( x e. A /\ C <_ x ) ) -> M e. RR )
17 2 adantrr 
 |-  ( ( ph /\ ( x e. A /\ C <_ x ) ) -> B e. RR )
18 16 17 lenegd 
 |-  ( ( ph /\ ( x e. A /\ C <_ x ) ) -> ( M <_ B <-> -u B <_ -u M ) )
19 15 18 mpbid 
 |-  ( ( ph /\ ( x e. A /\ C <_ x ) ) -> -u B <_ -u M )
20 1 13 3 14 19 ello1d 
 |-  ( ph -> ( x e. A |-> -u B ) e. <_O(1) )
21 2 o1lo1 
 |-  ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) ) )
22 12 20 21 mpbir2and 
 |-  ( ph -> ( x e. A |-> B ) e. O(1) )