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	5 6	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
8		rlimcl	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 → 𝐷 ∈ ℂ )
9	3 8	syl	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
10		rlimcl	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 → 𝐸 ∈ ℂ )
11	4 10	syl	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
12	9 11	mulcld	⊢ ( 𝜑 → ( 𝐷 · 𝐸 ) ∈ ℂ )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ )
14	9	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐷 ∈ ℂ )
15	11	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐸 ∈ ℂ )
16		mulcn2	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ) → ∃ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐷 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑢 · 𝑣 ) − ( 𝐷 · 𝐸 ) ) ) < 𝑦 ) )
17	13 14 15 16	syl3anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐷 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑢 · 𝑣 ) − ( 𝐷 · 𝐸 ) ) ) < 𝑦 ) )
18	5 6 7 12 3 4 17	rlimcn3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ⇝𝑟 ( 𝐷 · 𝐸 ) )