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

Metamath Proof Explorer

Theorem climadd

Description: Limit of the sum of two converging sequences. Proposition 12-2.1(a) of Gleason p. 168. (Contributed by NM, 24-Sep-2005) (Proof shortened by Mario Carneiro, 31-Jan-2014)

Ref Expression
Hypotheses climadd.1 ⊢ Z = ℤ ≥ M
climadd.2 ⊢ φ → M ∈ ℤ
climadd.4 ⊢ φ → F ⇝ A
climadd.6 ⊢ φ → H ∈ X
climadd.7 ⊢ φ → G ⇝ B
climadd.8 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
climadd.9 ⊢ φ ∧ k ∈ Z → G ⁡ k ∈ ℂ
climadd.h ⊢ φ ∧ k ∈ Z → H ⁡ k = F ⁡ k + G ⁡ k
Assertion climadd ⊢ φ → H ⇝ A + B

Proof

Step Hyp Ref Expression
1 climadd.1 ⊢ Z = ℤ ≥ M
2 climadd.2 ⊢ φ → M ∈ ℤ
3 climadd.4 ⊢ φ → F ⇝ A
4 climadd.6 ⊢ φ → H ∈ X
5 climadd.7 ⊢ φ → G ⇝ B
6 climadd.8 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
7 climadd.9 ⊢ φ ∧ k ∈ Z → G ⁡ k ∈ ℂ
8 climadd.h ⊢ φ ∧ k ∈ Z → H ⁡ k = F ⁡ k + G ⁡ k
9 climcl ⊢ F ⇝ A → A ∈ ℂ
10 3 9 syl ⊢ φ → A ∈ ℂ
11 climcl ⊢ G ⇝ B → B ∈ ℂ
12 5 11 syl ⊢ φ → B ∈ ℂ
13 addcl ⊢ u ∈ ℂ ∧ v ∈ ℂ → u + v ∈ ℂ
14 13 adantl ⊢ φ ∧ u ∈ ℂ ∧ v ∈ ℂ → u + v ∈ ℂ
15 simpr ⊢ φ ∧ x ∈ ℝ + → x ∈ ℝ +
16 10 adantr ⊢ φ ∧ x ∈ ℝ + → A ∈ ℂ
17 12 adantr ⊢ φ ∧ x ∈ ℝ + → B ∈ ℂ
18 addcn2 ⊢ x ∈ ℝ + ∧ A ∈ ℂ ∧ B ∈ ℂ → ∃ y ∈ ℝ + ∃ z ∈ ℝ + ∀ u ∈ ℂ ∀ v ∈ ℂ u − A < y ∧ v − B < z → u + v - A + B < x
19 15 16 17 18 syl3anc ⊢ φ ∧ x ∈ ℝ + → ∃ y ∈ ℝ + ∃ z ∈ ℝ + ∀ u ∈ ℂ ∀ v ∈ ℂ u − A < y ∧ v − B < z → u + v - A + B < x
20 1 2 10 12 14 3 5 4 19 6 7 8 climcn2 ⊢ φ → H ⇝ A + B