Theorem climconstmpt

Description: A constant sequence converges to its value. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	climconstmpt.m	|- ( ph -> M e. ZZ )
	climconstmpt.z	|- Z = ( ZZ>= ` M )
	climconstmpt.a	|- ( ph -> A e. CC )
Assertion	climconstmpt	|- ( ph -> ( x e. Z |-> A ) ~~> A )

Proof

Step	Hyp	Ref	Expression
1		climconstmpt.m	|- ( ph -> M e. ZZ )
2		climconstmpt.z	|- Z = ( ZZ>= ` M )
3		climconstmpt.a	|- ( ph -> A e. CC )
4		fconstmpt	|- ( Z X. { A } ) = ( x e. Z |-> A )
5	2	eqcomi	|- ( ZZ>= ` M ) = Z
6		ssid	|- Z C_ Z
7	5 6	eqsstri	|- ( ZZ>= ` M ) C_ Z
8	2	fvexi	|- Z e. _V
9	7 8	climconst2	|- ( ( A e. CC /\ M e. ZZ ) -> ( Z X. { A } ) ~~> A )
10	3 1 9	syl2anc	|- ( ph -> ( Z X. { A } ) ~~> A )
11	4 10	eqbrtrrid	|- ( ph -> ( x e. Z |-> A ) ~~> A )