Theorem climmul

Description: Limit of the product of two converging sequences. Proposition 12-2.1(c) of Gleason p. 168. (Contributed by NM, 27-Dec-2005) (Proof shortened by Mario Carneiro, 1-Feb-2014)

	Ref	Expression
Hypotheses	climadd.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climadd.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climadd.4	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
	climadd.6	⊢ ( 𝜑 → 𝐻 ∈ 𝑋 )
	climadd.7	⊢ ( 𝜑 → 𝐺 ⇝ 𝐵 )
	climadd.8	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
	climadd.9	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
	climmul.h	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
Assertion	climmul	⊢ ( 𝜑 → 𝐻 ⇝ ( 𝐴 · 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		climadd.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		climadd.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		climadd.4	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
4		climadd.6	⊢ ( 𝜑 → 𝐻 ∈ 𝑋 )
5		climadd.7	⊢ ( 𝜑 → 𝐺 ⇝ 𝐵 )
6		climadd.8	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
7		climadd.9	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
8		climmul.h	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
9		climcl	⊢ ( 𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ )
10	3 9	syl	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
11		climcl	⊢ ( 𝐺 ⇝ 𝐵 → 𝐵 ∈ ℂ )
12	5 11	syl	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
13		mulcl	⊢ ( ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) → ( 𝑢 · 𝑣 ) ∈ ℂ )
14	13	adantl	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( 𝑢 · 𝑣 ) ∈ ℂ )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
16	10	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
17	12	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
18		mulcn2	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 · 𝑣 ) − ( 𝐴 · 𝐵 ) ) ) < 𝑥 ) )
19	15 16 17 18	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 · 𝑣 ) − ( 𝐴 · 𝐵 ) ) ) < 𝑥 ) )
20	1 2 10 12 14 3 5 4 19 6 7 8	climcn2	⊢ ( 𝜑 → 𝐻 ⇝ ( 𝐴 · 𝐵 ) )