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 ⊢ φ ∧ x ∈ A → B ∈ V
rlimadd.4 ⊢ φ ∧ x ∈ A → C ∈ V
rlimadd.5 ⊢ φ → x ∈ A ⟼ B ⇝ℝ D
rlimadd.6 ⊢ φ → x ∈ A ⟼ C ⇝ℝ E
Assertion rlimadd ⊢ φ → x ∈ A ⟼ B + C ⇝ℝ D + E

Proof

Step Hyp Ref Expression
1 rlimadd.3 ⊢ φ ∧ x ∈ A → B ∈ V
2 rlimadd.4 ⊢ φ ∧ x ∈ A → C ∈ V
3 rlimadd.5 ⊢ φ → x ∈ A ⟼ B ⇝ℝ D
4 rlimadd.6 ⊢ φ → x ∈ A ⟼ C ⇝ℝ E
5 1 3 rlimmptrcl ⊢ φ ∧ x ∈ A → B ∈ ℂ
6 2 4 rlimmptrcl ⊢ φ ∧ x ∈ A → C ∈ ℂ
7 5 6 addcld ⊢ φ ∧ x ∈ A → B + C ∈ ℂ
8 rlimcl ⊢ x ∈ A ⟼ B ⇝ℝ D → D ∈ ℂ
9 3 8 syl ⊢ φ → D ∈ ℂ
10 rlimcl ⊢ x ∈ A ⟼ C ⇝ℝ E → E ∈ ℂ
11 4 10 syl ⊢ φ → E ∈ ℂ
12 9 11 addcld ⊢ φ → D + E ∈ ℂ
13 simpr ⊢ φ ∧ y ∈ ℝ + → y ∈ ℝ +
14 9 adantr ⊢ φ ∧ y ∈ ℝ + → D ∈ ℂ
15 11 adantr ⊢ φ ∧ y ∈ ℝ + → E ∈ ℂ
16 addcn2 ⊢ y ∈ ℝ + ∧ D ∈ ℂ ∧ E ∈ ℂ → ∃ z ∈ ℝ + ∃ w ∈ ℝ + ∀ u ∈ ℂ ∀ v ∈ ℂ u − D < z ∧ v − E < w → u + v - D + E < y
17 13 14 15 16 syl3anc ⊢ φ ∧ y ∈ ℝ + → ∃ z ∈ ℝ + ∃ w ∈ ℝ + ∀ u ∈ ℂ ∀ v ∈ ℂ u − D < z ∧ v − E < w → u + v - D + E < y
18 5 6 7 12 3 4 17 rlimcn3 ⊢ φ → x ∈ A ⟼ B + C ⇝ℝ D + E