Theorem climsubc2mpt

Description: Limit of the difference of two converging sequences. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	climsubc2mpt.k	⊢ Ⅎ 𝑘 𝜑
	climsubc2mpt.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climsubc2mpt.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climsubc2mpt.a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
	climsubc2mpt.c	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ⇝ 𝐶 )
	climsubc2mpt.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
Assertion	climsubc2mpt	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 − 𝐵 ) ) ⇝ ( 𝐶 − 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		climsubc2mpt.k	⊢ Ⅎ 𝑘 𝜑
2		climsubc2mpt.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		climsubc2mpt.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		climsubc2mpt.a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
5		climsubc2mpt.c	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ⇝ 𝐶 )
6		climsubc2mpt.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
7	6	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
8	3 2 6	climconstmpt	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ⇝ 𝐵 )
9	1 2 3 4 7 5 8	climsubmpt	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 − 𝐵 ) ) ⇝ ( 𝐶 − 𝐵 ) )