Metamath Proof Explorer

Theorem climle

Description: Comparison of the limits of two sequences. (Contributed by Paul Chapman, 10-Sep-2007) (Revised by Mario Carneiro, 1-Feb-2014)

Ref Expression
Hypotheses climadd.1 
|- Z = ( ZZ>= ` M )
climadd.2 
|- ( ph -> M e. ZZ )
climadd.4 
|- ( ph -> F ~~> A )
climle.5 
|- ( ph -> G ~~> B )
climle.6 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
climle.7 
|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )
climle.8 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) <_ ( G ` k ) )
Assertion climle 
|- ( ph -> A <_ B )

Proof

Step Hyp Ref Expression
1 climadd.1 
 |-  Z = ( ZZ>= ` M )
2 climadd.2 
 |-  ( ph -> M e. ZZ )
3 climadd.4 
 |-  ( ph -> F ~~> A )
4 climle.5 
 |-  ( ph -> G ~~> B )
5 climle.6 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
6 climle.7 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )
7 climle.8 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) <_ ( G ` k ) )
8 1 fvexi 
 |-  Z e. _V
9 8 mptex 
 |-  ( j e. Z |-> ( ( G ` j ) - ( F ` j ) ) ) e. _V
10 9 a1i 
 |-  ( ph -> ( j e. Z |-> ( ( G ` j ) - ( F ` j ) ) ) e. _V )
11 6 recnd 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
12 5 recnd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
13 fveq2 
 |-  ( j = k -> ( G ` j ) = ( G ` k ) )
14 fveq2 
 |-  ( j = k -> ( F ` j ) = ( F ` k ) )
15 13 14 oveq12d 
 |-  ( j = k -> ( ( G ` j ) - ( F ` j ) ) = ( ( G ` k ) - ( F ` k ) ) )
16 eqid 
 |-  ( j e. Z |-> ( ( G ` j ) - ( F ` j ) ) ) = ( j e. Z |-> ( ( G ` j ) - ( F ` j ) ) )
17 ovex 
 |-  ( ( G ` k ) - ( F ` k ) ) e. _V
18 15 16 17 fvmpt 
 |-  ( k e. Z -> ( ( j e. Z |-> ( ( G ` j ) - ( F ` j ) ) ) ` k ) = ( ( G ` k ) - ( F ` k ) ) )
19 18 adantl 
 |-  ( ( ph /\ k e. Z ) -> ( ( j e. Z |-> ( ( G ` j ) - ( F ` j ) ) ) ` k ) = ( ( G ` k ) - ( F ` k ) ) )
20 1 2 4 10 3 11 12 19 climsub 
 |-  ( ph -> ( j e. Z |-> ( ( G ` j ) - ( F ` j ) ) ) ~~> ( B - A ) )
21 6 5 resubcld 
 |-  ( ( ph /\ k e. Z ) -> ( ( G ` k ) - ( F ` k ) ) e. RR )
22 19 21 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( ( j e. Z |-> ( ( G ` j ) - ( F ` j ) ) ) ` k ) e. RR )
23 6 5 subge0d 
 |-  ( ( ph /\ k e. Z ) -> ( 0 <_ ( ( G ` k ) - ( F ` k ) ) <-> ( F ` k ) <_ ( G ` k ) ) )
24 7 23 mpbird 
 |-  ( ( ph /\ k e. Z ) -> 0 <_ ( ( G ` k ) - ( F ` k ) ) )
25 24 19 breqtrrd 
 |-  ( ( ph /\ k e. Z ) -> 0 <_ ( ( j e. Z |-> ( ( G ` j ) - ( F ` j ) ) ) ` k ) )
26 1 2 20 22 25 climge0 
 |-  ( ph -> 0 <_ ( B - A ) )
27 1 2 4 6 climrecl 
 |-  ( ph -> B e. RR )
28 1 2 3 5 climrecl 
 |-  ( ph -> A e. RR )
29 27 28 subge0d 
 |-  ( ph -> ( 0 <_ ( B - A ) <-> A <_ B ) )
30 26 29 mpbid 
 |-  ( ph -> A <_ B )