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) )