Metamath Proof Explorer


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 ( 𝜑𝐻 ⇝ ( 𝐴 · 𝐵 ) )