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 )