Metamath Proof Explorer

Theorem lmmcvg

Description: Convergence property of a converging sequence. (Contributed by NM, 1-Jun-2007) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses lmmbr.2 
|- J = ( MetOpen ` D )
lmmbr.3 
|- ( ph -> D e. ( *Met ` X ) )
lmmbr3.5 
|- Z = ( ZZ>= ` M )
lmmbr3.6 
|- ( ph -> M e. ZZ )
lmmbrf.7 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
lmmcvg.8 
|- ( ph -> F ( ~~>t ` J ) P )
lmmcvg.9 
|- ( ph -> R e. RR+ )
Assertion lmmcvg 
|- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( A e. X /\ ( A D P ) < R ) )

Proof

Step Hyp Ref Expression
1 lmmbr.2 
 |-  J = ( MetOpen ` D )
2 lmmbr.3 
 |-  ( ph -> D e. ( *Met ` X ) )
3 lmmbr3.5 
 |-  Z = ( ZZ>= ` M )
4 lmmbr3.6 
 |-  ( ph -> M e. ZZ )
5 lmmbrf.7 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
6 lmmcvg.8 
 |-  ( ph -> F ( ~~>t ` J ) P )
7 lmmcvg.9 
 |-  ( ph -> R e. RR+ )
8 breq2 
 |-  ( x = R -> ( ( ( F ` k ) D P ) < x <-> ( ( F ` k ) D P ) < R ) )
9 8 3anbi3d 
 |-  ( x = R -> ( ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) <-> ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < R ) ) )
10 9 rexralbidv 
 |-  ( x = R -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < R ) ) )
11 1 2 3 4 lmmbr3 
 |-  ( ph -> ( F ( ~~>t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) ) )
12 6 11 mpbid 
 |-  ( ph -> ( F e. ( X ^pm CC ) /\ P e. X /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) )
13 12 simp3d 
 |-  ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) )
14 10 13 7 rspcdva 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < R ) )
15 3 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
16 3simpc 
 |-  ( ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < R ) -> ( ( F ` k ) e. X /\ ( ( F ` k ) D P ) < R ) )
17 5 eleq1d 
 |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) e. X <-> A e. X ) )
18 5 oveq1d 
 |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) D P ) = ( A D P ) )
19 18 breq1d 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( F ` k ) D P ) < R <-> ( A D P ) < R ) )
20 17 19 anbi12d 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( F ` k ) e. X /\ ( ( F ` k ) D P ) < R ) <-> ( A e. X /\ ( A D P ) < R ) ) )
21 16 20 imbitrid 
 |-  ( ( ph /\ k e. Z ) -> ( ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < R ) -> ( A e. X /\ ( A D P ) < R ) ) )
22 15 21 sylan2 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < R ) -> ( A e. X /\ ( A D P ) < R ) ) )
23 22 anassrs 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < R ) -> ( A e. X /\ ( A D P ) < R ) ) )
24 23 ralimdva 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < R ) -> A. k e. ( ZZ>= ` j ) ( A e. X /\ ( A D P ) < R ) ) )
25 24 reximdva 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < R ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( A e. X /\ ( A D P ) < R ) ) )
26 14 25 mpd 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( A e. X /\ ( A D P ) < R ) )