Theorem climconstmpt

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

	Ref	Expression
Hypotheses	climconstmpt.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climconstmpt.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climconstmpt.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
Assertion	climconstmpt	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ⇝ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		climconstmpt.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		climconstmpt.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		climconstmpt.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
4		fconstmpt	⊢ ( 𝑍 × { 𝐴 } ) = ( 𝑥 ∈ 𝑍 ↦ 𝐴 )
5	2	eqcomi	⊢ ( ℤ≥ ‘ 𝑀 ) = 𝑍
6		ssid	⊢ 𝑍 ⊆ 𝑍
7	5 6	eqsstri	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ 𝑍
8	2	fvexi	⊢ 𝑍 ∈ V
9	7 8	climconst2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℤ ) → ( 𝑍 × { 𝐴 } ) ⇝ 𝐴 )
10	3 1 9	syl2anc	⊢ ( 𝜑 → ( 𝑍 × { 𝐴 } ) ⇝ 𝐴 )
11	4 10	eqbrtrrid	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ⇝ 𝐴 )