Metamath Proof Explorer


Theorem climsqz2

Description: Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 14-Feb-2008) (Revised by Mario Carneiro, 3-Feb-2014)

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

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 climsqz.5
 |-  ( ph -> G e. W )
5 climsqz.6
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
6 climsqz.7
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )
7 climsqz2.8
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) <_ ( F ` k ) )
8 climsqz2.9
 |-  ( ( ph /\ k e. Z ) -> A <_ ( G ` k ) )
9 2 adantr
 |-  ( ( ph /\ x e. RR+ ) -> M e. ZZ )
10 simpr
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR+ )
11 eqidd
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) -> ( F ` k ) = ( F ` k ) )
12 3 adantr
 |-  ( ( ph /\ x e. RR+ ) -> F ~~> A )
13 1 9 10 11 12 climi2
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x )
14 1 uztrn2
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
15 1 2 3 5 climrecl
 |-  ( ph -> A e. RR )
16 15 adantr
 |-  ( ( ph /\ k e. Z ) -> A e. RR )
17 6 5 16 7 lesub1dd
 |-  ( ( ph /\ k e. Z ) -> ( ( G ` k ) - A ) <_ ( ( F ` k ) - A ) )
18 16 6 8 abssubge0d
 |-  ( ( ph /\ k e. Z ) -> ( abs ` ( ( G ` k ) - A ) ) = ( ( G ` k ) - A ) )
19 16 6 5 8 7 letrd
 |-  ( ( ph /\ k e. Z ) -> A <_ ( F ` k ) )
20 16 5 19 abssubge0d
 |-  ( ( ph /\ k e. Z ) -> ( abs ` ( ( F ` k ) - A ) ) = ( ( F ` k ) - A ) )
21 17 18 20 3brtr4d
 |-  ( ( ph /\ k e. Z ) -> ( abs ` ( ( G ` k ) - A ) ) <_ ( abs ` ( ( F ` k ) - A ) ) )
22 21 adantlr
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) -> ( abs ` ( ( G ` k ) - A ) ) <_ ( abs ` ( ( F ` k ) - A ) ) )
23 6 adantlr
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) -> ( G ` k ) e. RR )
24 15 ad2antrr
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) -> A e. RR )
25 23 24 resubcld
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) -> ( ( G ` k ) - A ) e. RR )
26 25 recnd
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) -> ( ( G ` k ) - A ) e. CC )
27 26 abscld
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) -> ( abs ` ( ( G ` k ) - A ) ) e. RR )
28 5 adantlr
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) -> ( F ` k ) e. RR )
29 28 24 resubcld
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) -> ( ( F ` k ) - A ) e. RR )
30 29 recnd
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) -> ( ( F ` k ) - A ) e. CC )
31 30 abscld
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) -> ( abs ` ( ( F ` k ) - A ) ) e. RR )
32 rpre
 |-  ( x e. RR+ -> x e. RR )
33 32 ad2antlr
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) -> x e. RR )
34 lelttr
 |-  ( ( ( abs ` ( ( G ` k ) - A ) ) e. RR /\ ( abs ` ( ( F ` k ) - A ) ) e. RR /\ x e. RR ) -> ( ( ( abs ` ( ( G ` k ) - A ) ) <_ ( abs ` ( ( F ` k ) - A ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < x ) -> ( abs ` ( ( G ` k ) - A ) ) < x ) )
35 27 31 33 34 syl3anc
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) -> ( ( ( abs ` ( ( G ` k ) - A ) ) <_ ( abs ` ( ( F ` k ) - A ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < x ) -> ( abs ` ( ( G ` k ) - A ) ) < x ) )
36 22 35 mpand
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) -> ( ( abs ` ( ( F ` k ) - A ) ) < x -> ( abs ` ( ( G ` k ) - A ) ) < x ) )
37 14 36 sylan2
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( abs ` ( ( F ` k ) - A ) ) < x -> ( abs ` ( ( G ` k ) - A ) ) < x ) )
38 37 anassrs
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( abs ` ( ( F ` k ) - A ) ) < x -> ( abs ` ( ( G ` k ) - A ) ) < x ) )
39 38 ralimdva
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( G ` k ) - A ) ) < x ) )
40 39 reximdva
 |-  ( ( ph /\ x e. RR+ ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( G ` k ) - A ) ) < x ) )
41 13 40 mpd
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( G ` k ) - A ) ) < x )
42 41 ralrimiva
 |-  ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( G ` k ) - A ) ) < x )
43 eqidd
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) = ( G ` k ) )
44 15 recnd
 |-  ( ph -> A e. CC )
45 6 recnd
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
46 1 2 4 43 44 45 clim2c
 |-  ( ph -> ( G ~~> A <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( G ` k ) - A ) ) < x ) )
47 42 46 mpbird
 |-  ( ph -> G ~~> A )