Theorem rlimneg

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

	Ref	Expression
Hypotheses	rlimneg.1	$$⊢\left(\phi \wedge k\in A\right)\to B\in V$$
	rlimneg.2	$$⊢\phi \to \left(k\in A⟼B\right)\underset{ℝ}{⇝}C$$
Assertion	rlimneg	$$⊢\phi \to \left(k\in A⟼-B\right)\underset{ℝ}{⇝}\left(-C\right)$$

Proof

Step	Hyp	Ref	Expression
1		rlimneg.1	$$⊢\left(\phi \wedge k\in A\right)\to B\in V$$
2		rlimneg.2	$$⊢\phi \to \left(k\in A⟼B\right)\underset{ℝ}{⇝}C$$
3		0cnd	$$⊢\left(\phi \wedge k\in A\right)\to 0\in ℂ$$
4	1 2	rlimmptrcl	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
5	1	ralrimiva	$$⊢\phi \to \forall k\in AB\in V$$
6		dmmptg	$$⊢\forall k\in AB\in V\to \mathrm{dom}\left(k\in A⟼B\right)=A$$
7	5 6	syl	$$⊢\phi \to \mathrm{dom}\left(k\in A⟼B\right)=A$$
8		rlimss	$$⊢\left(k\in A⟼B\right)\underset{ℝ}{⇝}C\to \mathrm{dom}\left(k\in A⟼B\right)\subseteq ℝ$$
9	2 8	syl	$$⊢\phi \to \mathrm{dom}\left(k\in A⟼B\right)\subseteq ℝ$$
10	7 9	eqsstrrd	$$⊢\phi \to A\subseteq ℝ$$
11		0cn	$$⊢0\in ℂ$$
12		rlimconst	$$⊢\left(A\subseteq ℝ\wedge 0\in ℂ\right)\to \left(k\in A⟼0\right)\underset{ℝ}{⇝}0$$
13	10 11 12	sylancl	$$⊢\phi \to \left(k\in A⟼0\right)\underset{ℝ}{⇝}0$$
14	3 4 13 2	rlimsub	$$⊢\phi \to \left(k\in A⟼0-B\right)\underset{ℝ}{⇝}\left(0-C\right)$$
15		df-neg	$$⊢-B=0-B$$
16	15	mpteq2i	$$⊢\left(k\in A⟼-B\right)=\left(k\in A⟼0-B\right)$$
17		df-neg	$$⊢-C=0-C$$
18	14 16 17	3brtr4g	$$⊢\phi \to \left(k\in A⟼-B\right)\underset{ℝ}{⇝}\left(-C\right)$$