Theorem rlimmul

Description: Limit of the product of two converging functions. Proposition 12-2.1(c) 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	rlimmul	$$⊢\phi \to \left(x\in A⟼BC\right)\underset{ℝ}{⇝}DE$$

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		ax-mulf	$$⊢\times :ℂ\times ℂ⟶ℂ$$
12	11	a1i	$$⊢\phi \to \times :ℂ\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		mulcn2	$$⊢\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|uv-DE\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|uv-DE\right|<y\right)$$
18	5 6 8 10 3 4 12 17	rlimcn2	$$⊢\phi \to \left(x\in A⟼BC\right)\underset{ℝ}{⇝}DE$$