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	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	rlimadd.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
	rlimadd.5	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 )
	rlimadd.6	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 )
Assertion	rlimmul	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ⇝𝑟 ( 𝐷 · 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		rlimadd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2		rlimadd.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
3		rlimadd.5	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 )
4		rlimadd.6	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 )
5	1 3	rlimmptrcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
6	2 4	rlimmptrcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
7		rlimcl	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 → 𝐷 ∈ ℂ )
8	3 7	syl	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
9		rlimcl	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 → 𝐸 ∈ ℂ )
10	4 9	syl	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
11		ax-mulf	⊢ · : ( ℂ × ℂ ) ⟶ ℂ
12	11	a1i	⊢ ( 𝜑 → · : ( ℂ × ℂ ) ⟶ ℂ )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ )
14	8	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐷 ∈ ℂ )
15	10	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐸 ∈ ℂ )
16		mulcn2	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ) → ∃ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐷 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑢 · 𝑣 ) − ( 𝐷 · 𝐸 ) ) ) < 𝑦 ) )
17	13 14 15 16	syl3anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐷 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑢 · 𝑣 ) − ( 𝐷 · 𝐸 ) ) ) < 𝑦 ) )
18	5 6 8 10 3 4 12 17	rlimcn2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ⇝𝑟 ( 𝐷 · 𝐸 ) )