Theorem climsubc1mpt

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

	Ref	Expression
Hypotheses	climsubc1mpt.k	$$⊢Ⅎk\phi$$
	climsubc1mpt.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climsubc1mpt.m	$$⊢\phi \to M\in \mathbb{Z}$$
	climsubc1mpt.b	$$⊢\phi \to A\in ℂ$$
	climsubc1mpt.a	$$⊢\left(\phi \wedge k\in Z\right)\to B\in ℂ$$
	climsubc1mpt.c	$$⊢\phi \to \left(k\in Z⟼B\right)⇝C$$
Assertion	climsubc1mpt	$$⊢\phi \to \left(k\in Z⟼A-B\right)⇝\left(A-C\right)$$

Proof

Step	Hyp	Ref	Expression
1		climsubc1mpt.k	$$⊢Ⅎk\phi$$
2		climsubc1mpt.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3		climsubc1mpt.m	$$⊢\phi \to M\in \mathbb{Z}$$
4		climsubc1mpt.b	$$⊢\phi \to A\in ℂ$$
5		climsubc1mpt.a	$$⊢\left(\phi \wedge k\in Z\right)\to B\in ℂ$$
6		climsubc1mpt.c	$$⊢\phi \to \left(k\in Z⟼B\right)⇝C$$
7	4	adantr	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℂ$$
8	3 2 4	climconstmpt	$$⊢\phi \to \left(k\in Z⟼A\right)⇝A$$
9	1 2 3 7 5 8 6	climsubmpt	$$⊢\phi \to \left(k\in Z⟼A-B\right)⇝\left(A-C\right)$$