Theorem rlimneg

Description: Limit of the negative of a sequence. (Contributed by Mario Carneiro, 18-May-2016)

	Ref	Expression
Hypotheses	rlimneg.1	|- ( ( ph /\ k e. A ) -> B e. V )
	rlimneg.2	|- ( ph -> ( k e. A |-> B ) ~~>r C )
Assertion	rlimneg	|- ( ph -> ( k e. A |-> -u B ) ~~>r -u C )

Proof

Step	Hyp	Ref	Expression
1		rlimneg.1	|- ( ( ph /\ k e. A ) -> B e. V )
2		rlimneg.2	|- ( ph -> ( k e. A |-> B ) ~~>r C )
3		0cnd	|- ( ( ph /\ k e. A ) -> 0 e. CC )
4	1 2	rlimmptrcl	|- ( ( ph /\ k e. A ) -> B e. CC )
5	1	ralrimiva	|- ( ph -> A. k e. A B e. V )
6		dmmptg	|- ( A. k e. A B e. V -> dom ( k e. A |-> B ) = A )
7	5 6	syl	|- ( ph -> dom ( k e. A |-> B ) = A )
8		rlimss	|- ( ( k e. A |-> B ) ~~>r C -> dom ( k e. A |-> B ) C_ RR )
9	2 8	syl	|- ( ph -> dom ( k e. A |-> B ) C_ RR )
10	7 9	eqsstrrd	|- ( ph -> A C_ RR )
11		0cn	|- 0 e. CC
12		rlimconst	|- ( ( A C_ RR /\ 0 e. CC ) -> ( k e. A |-> 0 ) ~~>r 0 )
13	10 11 12	sylancl	|- ( ph -> ( k e. A |-> 0 ) ~~>r 0 )
14	3 4 13 2	rlimsub	|- ( ph -> ( k e. A |-> ( 0 - B ) ) ~~>r ( 0 - C ) )
15		df-neg	|- -u B = ( 0 - B )
16	15	mpteq2i	|- ( k e. A |-> -u B ) = ( k e. A |-> ( 0 - B ) )
17		df-neg	|- -u C = ( 0 - C )
18	14 16 17	3brtr4g	|- ( ph -> ( k e. A |-> -u B ) ~~>r -u C )