This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem climconst2

Description: A constant sequence converges to its value. (Contributed by NM, 6-Feb-2008) (Revised by Mario Carneiro, 31-Jan-2014)

Ref Expression
Hypotheses climconst2.1 
|- ( ZZ>= ` M ) C_ Z
climconst2.2 
|- Z e. _V
Assertion climconst2 
|- ( ( A e. CC /\ M e. ZZ ) -> ( Z X. { A } ) ~~> A )

Proof

Step Hyp Ref Expression
1 climconst2.1 
 |-  ( ZZ>= ` M ) C_ Z
2 climconst2.2 
 |-  Z e. _V
3 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
4 simpr 
 |-  ( ( A e. CC /\ M e. ZZ ) -> M e. ZZ )
5 snex 
 |-  { A } e. _V
6 2 5 xpex 
 |-  ( Z X. { A } ) e. _V
7 6 a1i 
 |-  ( ( A e. CC /\ M e. ZZ ) -> ( Z X. { A } ) e. _V )
8 simpl 
 |-  ( ( A e. CC /\ M e. ZZ ) -> A e. CC )
9 1 sseli 
 |-  ( k e. ( ZZ>= ` M ) -> k e. Z )
10 fvconst2g 
 |-  ( ( A e. CC /\ k e. Z ) -> ( ( Z X. { A } ) ` k ) = A )
11 8 9 10 syl2an 
 |-  ( ( ( A e. CC /\ M e. ZZ ) /\ k e. ( ZZ>= ` M ) ) -> ( ( Z X. { A } ) ` k ) = A )
12 3 4 7 8 11 climconst 
 |-  ( ( A e. CC /\ M e. ZZ ) -> ( Z X. { A } ) ~~> A )