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 )