Theorem climsubc1mpt

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

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

Proof

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