This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rlimadd

Description: Limit of the sum of two converging functions. Proposition 12-2.1(a) of Gleason p. 168. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Hypotheses rlimadd.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
rlimadd.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
rlimadd.5 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 )
rlimadd.6 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 )
Assertion rlimadd ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ⇝𝑟 ( 𝐷 + 𝐸 ) )

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