Theorem climsubc2mpt

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

	Ref	Expression
Hypotheses	climsubc2mpt.k	|- F/ k ph
	climsubc2mpt.z	|- Z = ( ZZ>= ` M )
	climsubc2mpt.m	|- ( ph -> M e. ZZ )
	climsubc2mpt.a	|- ( ( ph /\ k e. Z ) -> A e. CC )
	climsubc2mpt.c	|- ( ph -> ( k e. Z |-> A ) ~~> C )
	climsubc2mpt.b	|- ( ph -> B e. CC )
Assertion	climsubc2mpt	|- ( ph -> ( k e. Z |-> ( A - B ) ) ~~> ( C - B ) )

Proof

Step	Hyp	Ref	Expression
1		climsubc2mpt.k	|- F/ k ph
2		climsubc2mpt.z	|- Z = ( ZZ>= ` M )
3		climsubc2mpt.m	|- ( ph -> M e. ZZ )
4		climsubc2mpt.a	|- ( ( ph /\ k e. Z ) -> A e. CC )
5		climsubc2mpt.c	|- ( ph -> ( k e. Z |-> A ) ~~> C )
6		climsubc2mpt.b	|- ( ph -> B e. CC )
7	6	adantr	|- ( ( ph /\ k e. Z ) -> B e. CC )
8	3 2 6	climconstmpt	|- ( ph -> ( k e. Z |-> B ) ~~> B )
9	1 2 3 4 7 5 8	climsubmpt	|- ( ph -> ( k e. Z |-> ( A - B ) ) ~~> ( C - B ) )