Theorem climsubc1mpt

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

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

Proof

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