Metamath Proof Explorer

Theorem 2clim

Description: If two sequences converge to each other, they converge to the same limit. (Contributed by NM, 24-Dec-2005) (Proof shortened by Mario Carneiro, 31-Jan-2014)

Ref Expression
Hypotheses 2clim.1 
|- Z = ( ZZ>= ` M )
2clim.2 
|- ( ph -> M e. ZZ )
2clim.3 
|- ( ph -> G e. V )
2clim.5 
|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
2clim.6 
|- ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < x )
2clim.7 
|- ( ph -> F ~~> A )
Assertion 2clim 
|- ( ph -> G ~~> A )

Proof

Step Hyp Ref Expression
1 2clim.1 
 |-  Z = ( ZZ>= ` M )
2 2clim.2 
 |-  ( ph -> M e. ZZ )
3 2clim.3 
 |-  ( ph -> G e. V )
4 2clim.5 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
5 2clim.6 
 |-  ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < x )
6 2clim.7 
 |-  ( ph -> F ~~> A )
7 rphalfcl 
 |-  ( y e. RR+ -> ( y / 2 ) e. RR+ )
8 breq2 
 |-  ( x = ( y / 2 ) -> ( ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < x <-> ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < ( y / 2 ) ) )
9 8 rexralbidv 
 |-  ( x = ( y / 2 ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < x <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < ( y / 2 ) ) )
10 9 rspccva 
 |-  ( ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < x /\ ( y / 2 ) e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < ( y / 2 ) )
11 5 7 10 syl2an 
 |-  ( ( ph /\ y e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < ( y / 2 ) )
12 2 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> M e. ZZ )
13 7 adantl 
 |-  ( ( ph /\ y e. RR+ ) -> ( y / 2 ) e. RR+ )
14 eqidd 
 |-  ( ( ( ph /\ y e. RR+ ) /\ k e. Z ) -> ( F ` k ) = ( F ` k ) )
15 6 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> F ~~> A )
16 1 12 13 14 15 climi 
 |-  ( ( ph /\ y e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( y / 2 ) ) )
17 1 rexanuz2 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < ( y / 2 ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( y / 2 ) ) ) <-> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < ( y / 2 ) /\ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( y / 2 ) ) ) )
18 11 16 17 sylanbrc 
 |-  ( ( ph /\ y e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < ( y / 2 ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( y / 2 ) ) ) )
19 1 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
20 an12 
 |-  ( ( ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < ( y / 2 ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( y / 2 ) ) ) <-> ( ( F ` k ) e. CC /\ ( ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < ( y / 2 ) /\ ( abs ` ( ( F ` k ) - A ) ) < ( y / 2 ) ) ) )
21 simprr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( k e. Z /\ ( F ` k ) e. CC ) ) -> ( F ` k ) e. CC )
22 4 ad2ant2r 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( k e. Z /\ ( F ` k ) e. CC ) ) -> ( G ` k ) e. CC )
23 21 22 abssubd 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( k e. Z /\ ( F ` k ) e. CC ) ) -> ( abs ` ( ( F ` k ) - ( G ` k ) ) ) = ( abs ` ( ( G ` k ) - ( F ` k ) ) ) )
24 23 breq1d 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( k e. Z /\ ( F ` k ) e. CC ) ) -> ( ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < ( y / 2 ) <-> ( abs ` ( ( G ` k ) - ( F ` k ) ) ) < ( y / 2 ) ) )
25 24 anbi1d 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( k e. Z /\ ( F ` k ) e. CC ) ) -> ( ( ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < ( y / 2 ) /\ ( abs ` ( ( F ` k ) - A ) ) < ( y / 2 ) ) <-> ( ( abs ` ( ( G ` k ) - ( F ` k ) ) ) < ( y / 2 ) /\ ( abs ` ( ( F ` k ) - A ) ) < ( y / 2 ) ) ) )
26 climcl 
 |-  ( F ~~> A -> A e. CC )
27 6 26 syl 
 |-  ( ph -> A e. CC )
28 27 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( k e. Z /\ ( F ` k ) e. CC ) ) -> A e. CC )
29 rpre 
 |-  ( y e. RR+ -> y e. RR )
30 29 ad2antlr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( k e. Z /\ ( F ` k ) e. CC ) ) -> y e. RR )
31 abs3lem 
 |-  ( ( ( ( G ` k ) e. CC /\ A e. CC ) /\ ( ( F ` k ) e. CC /\ y e. RR ) ) -> ( ( ( abs ` ( ( G ` k ) - ( F ` k ) ) ) < ( y / 2 ) /\ ( abs ` ( ( F ` k ) - A ) ) < ( y / 2 ) ) -> ( abs ` ( ( G ` k ) - A ) ) < y ) )
32 22 28 21 30 31 syl22anc 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( k e. Z /\ ( F ` k ) e. CC ) ) -> ( ( ( abs ` ( ( G ` k ) - ( F ` k ) ) ) < ( y / 2 ) /\ ( abs ` ( ( F ` k ) - A ) ) < ( y / 2 ) ) -> ( abs ` ( ( G ` k ) - A ) ) < y ) )
33 25 32 sylbid 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( k e. Z /\ ( F ` k ) e. CC ) ) -> ( ( ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < ( y / 2 ) /\ ( abs ` ( ( F ` k ) - A ) ) < ( y / 2 ) ) -> ( abs ` ( ( G ` k ) - A ) ) < y ) )
34 33 anassrs 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ k e. Z ) /\ ( F ` k ) e. CC ) -> ( ( ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < ( y / 2 ) /\ ( abs ` ( ( F ` k ) - A ) ) < ( y / 2 ) ) -> ( abs ` ( ( G ` k ) - A ) ) < y ) )
35 34 expimpd 
 |-  ( ( ( ph /\ y e. RR+ ) /\ k e. Z ) -> ( ( ( F ` k ) e. CC /\ ( ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < ( y / 2 ) /\ ( abs ` ( ( F ` k ) - A ) ) < ( y / 2 ) ) ) -> ( abs ` ( ( G ` k ) - A ) ) < y ) )
36 20 35 syl5bi 
 |-  ( ( ( ph /\ y e. RR+ ) /\ k e. Z ) -> ( ( ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < ( y / 2 ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( y / 2 ) ) ) -> ( abs ` ( ( G ` k ) - A ) ) < y ) )
37 19 36 sylan2 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < ( y / 2 ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( y / 2 ) ) ) -> ( abs ` ( ( G ` k ) - A ) ) < y ) )
38 37 anassrs 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < ( y / 2 ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( y / 2 ) ) ) -> ( abs ` ( ( G ` k ) - A ) ) < y ) )
39 38 ralimdva 
 |-  ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < ( y / 2 ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( y / 2 ) ) ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( G ` k ) - A ) ) < y ) )
40 39 reximdva 
 |-  ( ( ph /\ y e. RR+ ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < ( y / 2 ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( y / 2 ) ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( G ` k ) - A ) ) < y ) )
41 18 40 mpd 
 |-  ( ( ph /\ y e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( G ` k ) - A ) ) < y )
42 41 ralrimiva 
 |-  ( ph -> A. y e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( G ` k ) - A ) ) < y )
43 eqidd 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) = ( G ` k ) )
44 1 2 3 43 27 4 clim2c 
 |-  ( ph -> ( G ~~> A <-> A. y e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( G ` k ) - A ) ) < y ) )
45 42 44 mpbird 
 |-  ( ph -> G ~~> A )