Theorem rlimsub

Description: Limit of the difference of two converging functions. Proposition 12-2.1(b) of Gleason p. 168. (Contributed by Mario Carneiro, 22-Sep-2014)

	Ref	Expression
Hypotheses	rlimadd.3	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
	rlimadd.4	$$⊢\left(\phi \wedge x\in A\right)\to C\in V$$
	rlimadd.5	$$⊢\phi \to \left(x\in A⟼B\right)\underset{ℝ}{⇝}D$$
	rlimadd.6	$$⊢\phi \to \left(x\in A⟼C\right)\underset{ℝ}{⇝}E$$
Assertion	rlimsub	$$⊢\phi \to \left(x\in A⟼B-C\right)\underset{ℝ}{⇝}\left(D-E\right)$$

Proof

Step	Hyp	Ref	Expression
1		rlimadd.3	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
2		rlimadd.4	$$⊢\left(\phi \wedge x\in A\right)\to C\in V$$
3		rlimadd.5	$$⊢\phi \to \left(x\in A⟼B\right)\underset{ℝ}{⇝}D$$
4		rlimadd.6	$$⊢\phi \to \left(x\in A⟼C\right)\underset{ℝ}{⇝}E$$
5	1 3	rlimmptrcl	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℂ$$
6	2 4	rlimmptrcl	$$⊢\left(\phi \wedge x\in A\right)\to C\in ℂ$$
7		rlimcl	$$⊢\left(x\in A⟼B\right)\underset{ℝ}{⇝}D\to D\in ℂ$$
8	3 7	syl	$$⊢\phi \to D\in ℂ$$
9		rlimcl	$$⊢\left(x\in A⟼C\right)\underset{ℝ}{⇝}E\to E\in ℂ$$
10	4 9	syl	$$⊢\phi \to E\in ℂ$$
11		subf	$$⊢-:ℂ\times ℂ⟶ℂ$$
12	11	a1i	$$⊢\phi \to -:ℂ\times ℂ⟶ℂ$$
13		simpr	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to y\in {ℝ}^{+}$$
14	8	adantr	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to D\in ℂ$$
15	10	adantr	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to E\in ℂ$$
16		subcn2	$$⊢\left(y\in {ℝ}^{+}\wedge D\in ℂ\wedge E\in ℂ\right)\to \exists z\in {ℝ}^{+}\exists w\in {ℝ}^{+}\forall u\in ℂ\forall v\in ℂ\left(\left(\left|u-D\right|<z\wedge \left|v-E\right|<w\right)\to \left|u-v-\left(D-E\right)\right|<y\right)$$
17	13 14 15 16	syl3anc	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \exists z\in {ℝ}^{+}\exists w\in {ℝ}^{+}\forall u\in ℂ\forall v\in ℂ\left(\left(\left|u-D\right|<z\wedge \left|v-E\right|<w\right)\to \left|u-v-\left(D-E\right)\right|<y\right)$$
18	5 6 8 10 3 4 12 17	rlimcn2	$$⊢\phi \to \left(x\in A⟼B-C\right)\underset{ℝ}{⇝}\left(D-E\right)$$