The Sum of two Convergent Sequences is Convergent

Manuel Kauers

December 17, 2002

Abstract This document provides a formal proof of the well known fact that the sum of two convergent sequences itself is convergent, using the tableau method of Smullyan and Fitting.

1 Goal

We want to prove the limit theorem G under the assumptions A1–A8 using a tableau calculus for first order predicat logic.

A1 ∀_{{f \atop seq[f]}}(conv[f] ↔ ∃_{a∈ℝ} ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |f[n] − a| < ε,
A2 ∀_{{f \atop seq[f]}} ∀_{{g \atop seq[g]}} seq[f + g],
A3 ∀_{a∈ℝ} ∀_{b∈ℝ} a + b ∈ ℝ,
A4 ∀_{{x∈ℝ \atop x>0}} x/2 ∈ ℝ ∧ x > 0,
A5 ∀_{x∈ℕ} ∀_{y∈ℕ} max[x, y] ∈ ℕ,
A6 ∀_{x∈ℕ} ∀_{y∈ℕ} ∀_{z∈ℕ} x ≥ max[y, z] → x ≥ y,
A7 ∀_{x∈ℕ} ∀_{y∈ℕ} ∀_{z∈ℕ} x ≥ max[y, z] → x ≥ z,
A8 ∀_{{f \atop seq[f]}} ∀_{{g \atop seq[g]}} ∀_{n∈ℕ} ∀_{ε∈ℝ} ∀_{a∈ℝ} ∀_{b∈ℝ}

(|f[n] − a| < ε/2 ∧ |g[n] − b| < ε/2) → |(f + g)[n] − (a + b)| < ε

G ∀_{{f \atop seq[f]}} ∀_{{g \atop seq[g]}}(conv[f] ∧ conv[g] → conv[f + g]).

2 Notation

We assume the reader to be familiar with the tableau calculus, and make just some remarks about the notation.

• Each node N of the proof tree has the form

n(m) : s F

where n is a label of N, m is the label of the node M which justifies N. (m = G or m = An to refer to goal or assumptions), s is the sign and F is the formula of N. (Recall that s = 0 means F is assumed to be false and s = 1 means F is assumed to be true). Formulae are denoted in Theorema syntax.

• Free variables are denoted in capital (or greek) letters with asterix superscript, constants are denoted by an index subscript without asterix superscript. All other kinds of variables are bounded by some quantifyer. For instance, X^{∗}, ε^{∗}, and N_{2}^{∗} are free variables, a_{0} and N_{1} are constants, and so on.

• Formulae like ∀_{x∈ℝ} F (x) and ∃_{x∈ℝ} F (x) are taken as shortcuts for ∀_{x}(x ∈ ℝ → F (x)) and ∃_{x}(x ∈ ℝ ∧ F (x)), respectively, and behave accordingly.

• If a path that ends with node n is closed by a substitution σ, say σ = {X^{∗} ← x_{0}}, then x_{0} might appear instead of X^{∗} in any node with label m > n. It is therefore strongly recommended to read subtrees within the proof in the order of the labels rather than in any other order.

• Identifiers of free variables which have been assigned to some term in node n might be recycled in subsequent nodes m > n. Also, a variable does not appear as argument of a skolem function, if it has already been assigned to a ground term. (In fact, no skolem function will have arguments due to this rule.)

• Sorry for spoiling the margins, typesetting trees turned out to be a nontrivial task ;-)

0(G): 0 ∀_{{f \atop seq[f]}} ∀_{{g \atop seq[g]}}(conv[f] ∧ conv[g] → conv[f + g]).

1(0): 1 seq[f_{0}].

2(0): 0 ∀_{{g \atop seq[g]}}(conv[f_{0}] ∧ conv[g] → conv[f_{0} + g]).

3(2): 1 seq[g_{0}].

4(2): 0 conv[f_{0}] ∧ conv[g_{0}] → conv[f_{0} + g_{0}].

5(4): 1 conv[f_{0}] ∧ conv[g_{0}].

6(4): 0 conv[f_{0} + g_{0}]. 7(5): 1 conv[f_{0}]. 8(5): 1 conv[g_{0}].

9(A1): 1 ∀_{{f \atop seq[f]}}(conv[f] ↔ ∃_{a∈ℝ} ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |f[n] − a| < ε).

10(9): 1 seq[F^{∗}] → (conv[F^{∗}] ↔ ∃_{a∈ℝ} ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |F^{∗}[n] − a| < ε).

11(10): 0 seq[F^{∗}]._{*(11,1) by {F^{∗} ← f_{0}}}

12(10): 1 conv[f_{0}] ↔ ∃_{a∈ℝ} ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |f_{0}[n] − a| < ε.

15(10): 1 conv[f_{0}].

16(10): 1 ∃_{a∈ℝ} ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |f_{0}[n] − a| < ε.

17(9): 1 seq[G^{∗}] → (conv[G^{∗}] ↔ ∃_{a∈ℝ} ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |G^{∗}[n] − a| < ε).

19(17): 1 conv[G^{∗}] ↔ ∃_{a∈ℝ} ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |g_{0}[n] − a| < ε.

20(19): 0 conv[g_{0}]. 21(19): 0 ∃_{a∈ℝ} ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |g_{0}[n] − a| < ε._{{*(20,8) \atop by \{\}}}

22(19): 1 ∃_{a∈ℝ} ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |g_{0}[n] − a| < ε.

23(19): 1 conv[g_{0}].

24(9): 1 seq[H^{∗}] → (conv[H^{∗}] ↔ ∃_{a∈ℝ} ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |H^{∗}[n] − a| < ε).

25(24): 1 conv[H^{∗}] ↔ ∃_{a∈ℝ} ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |H^{∗}[n] − a| < ε).

32(25): 1 conv[f_{0} + g_{0}]. 33(25): 1 ∃_{a∈ℝ} ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |(f_{0} + g_{0})[n] − a| < ε)._{{*(6,32) \atop by \{\}}}

34(25): 0 ∃_{a∈ℝ} ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |(f_{0} + g_{0})[n] − a| < ε).

35(25): 0 conv[f_{0} + g_{0}]. next page

26(24): 0 seq[H^{∗}].
27(A2): 1 ∀_{{f \atop seq[f]}} ∀_{{g \atop seq[g]}} seq[f + g].

29(27): 1 ∀_{{g \atop seq[g]}} seq[f_{0} + g].

30(29): 0 seq[G^{∗∗}]._{{*(3,30) \atop by \{G^{∗∗} ← g_{0}\}}} 31(29): 1 seq[f_{0} + g_{0}]._{{*(26,31) \atop by \{H^{∗} ← f_{0} + g_{0}\}}}

28(27): 0 seq[F^{∗∗}]._{{*(1,28) \atop by \{F^{∗∗} ← f_{0}\}}}

18(17): 0 seq[G^{∗}]._{*(3,18) by {G^{∗} ← g_{0}}}

13(10): 0 ∃_{a∈ℝ} ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |f_{0}[n] − a| < ε. 14(10): 0 conv[f_{0}]._{*(7,14) by \{\}}

⋮

35(25): 0 conv[f_{0} + g_{0}].

36(16): 1 a_{0} ∈ ℝ ∧ ( ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |f_{0}[n] − a_{0}| < ε).

37(36): 1 a_{0} ∈ ℝ.

38(36): 1 ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |f_{0}[n] − a_{0}| < ε.

39(22): 1 b_{0} ∈ ℝ ∧ ( ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |g_{0}[n] − b_{0}| < ε).

40(39): 1 b_{0} ∈ ℝ.

41(39): 1 ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |g_{0}[n] − b_{0}| < ε.

42(34): 0 C^{∗} ∈ ℝ ∧ ( ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |(f_{0} + g_{0})[n] − C^{∗}| < ε).

51(42): 0 ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |(f_{0} + g_{0})[n] − (a_{0} + b_{0})| < ε.

52(51): 0 (ε_{0} ∈ ℝ ∧ ε_{0} > 0) → ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |(f_{0} + g_{0})[n] − (a_{0} + b_{0})| < ε_{0}.

53(52): 1 ε_{0} ∈ ℝ ∧ ε_{0} > 0.

54(52): 0 ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |(f_{0} + g_{0})[n] − (a_{0} + b_{0})| < ε_{0}.

55(53): 1 ε_{0} ∈ ℝ.

56(53): 1 ε_{0} > 0.

57(38): 1 (E_{1}^{∗} ∈ ℝ ∧ E_{1}^{∗} > 0) → ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |f_{0}[n] − a_{0}| < E_{1}^{∗}.

58(A4): 1 ∀_{{x∈ℝ \atop x>0}} x/2 ∈ ℝ ∧ x/2 > 0.

69(57): 1 ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |f_{0}[n] − a_{0}| < ε_{0}/2.

70(41): 1 (E_{2}^{∗} ∈ ℝ ∧ E_{2}^{∗} > 0) → ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |g_{0}[n] − b_{0}| < E_{2}^{∗}).

next page

59(57): 0 E_{1}^{∗} ∈ ℝ ∧ E_{1}^{∗} > 0.

60(58): 1 (X^{∗} ∈ ℝ ∧ X^{∗} > 0) → (X^{∗}/2 ∈ ℝ ∧ X^{∗}/2 > 0).
64(60): 1 ε_{0}/2 ∈ ℝ ∧ ε_{0}/2 > 0. ; 65(64): 1 ε_{0}/2 ∈ ℝ. ; \begin{matrix}66(64): 1 ε_{0}/2 > 0. \\ 67(59): 0 E_{1}^{∗} ∈ ℝ._{{*(65,67) \atop by \{E_{1}^{∗} ← ε_{0}/2\}}} & 68(59): 0 ε_{0}/2 > 0._{{*(66,68) \atop by \{\}}} \end{matrix} \begin{matrix}61(60): 0 X^{∗} ∈ ℝ ∧ X^{∗} > 0. \\ 62(61): 0 X^{∗} ∈ ℝ._{{*(55,62) \atop by \{X^{∗} ← ε_{0}\}}} & 63(61): 0 ε_{0} > 0._{{*(56,63) \atop by \{\}}} \end{matrix}

43(42): 0 C^{∗} ∈ ℝ. 44(A3): 1 ∀_{a∈ℝ} ∀_{b∈ℝ} a + b ∈ ℝ. ; 45(44): 1 A^{∗} ∈ ℝ → ∀_{b∈ℝ} A^{∗} + b ∈ ℝ. ; 46(45): 0 A^{∗} ∈ ℝ._{{*(37,46) \atop by \{A^{∗} ← a_{0}\}}} ; 47(45): 1 ∀_{b∈ℝ} a_{0} + b ∈ ℝ. ; \begin{matrix}48(47): 1 B^{∗} ∈ ℝ → a_{0} + B^{∗} ∈ ℝ. \\ 49(48): 0 B^{∗} ∈ ℝ._{{*(40,49) \atop by \{B^{∗} ← b_{0}\}}} & 50(48): 1 a_{0} + b_{0} ∈ ℝ._{{*(43,50) \atop by \{C^{∗} ← a_{0} + b_{0}\}}} \end{matrix}

⋮

70(41): 1 (E_{2}^{∗} ∈ ℝ ∧ E_{2}^{∗} > 0) → ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |g_{0}[n] − b_{0}| < E_{2}^{∗}).

71(70): 0 E_{2}^{∗} ∈ ℝ ∧ E_{2}^{∗} > 0.

72(58): 1 (X^{∗} ∈ ℝ ∧ X^{∗} > 0) → (X^{∗}/2 ∈ ℝ ∧ X^{∗}/2 > 0).

76(72): 1 ε_{0}/2 ∈ ℝ ∧ ε_{0}/2 > 0. ; 77(76): 1 ε_{0}/2 ∈ ℝ. ; \begin{matrix}78(76): 1 ε_{0}/2 > 0. \\ 79(71): 0 E_{2}^{∗} ∈ ℝ._{{*(77,79) \atop by \{E_{2}^{∗} ← ε_{0}/2\}}} & 80(71): 0 ε_{0}/2 > 0._{{*(78,80) \atop by \{\}}} \end{matrix} \begin{matrix}73(72): 0 X^{∗} ∈ ℝ ∧ X^{∗} > 0. \\ 74(73): 0 X^{∗} ∈ ℝ._{{*(55,74) \atop by \{X^{∗} ← ε_{0}\}}} & 75(73): 0 ε_{0} > 0._{{*(56,75) \atop by \{\}}} \end{matrix}

81(70): 1 ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |g_{0}[n] − b_{0}| < E_{2}^{∗}.

82(69): 1 N_{1} ∈ ℕ ∧ ∀_{{n∈ℕ \atop n≥N_{1}}} |f_{0}[n] − a_{0}| < ε_{0}/2.

83(82): 1 N_{1} ∈ ℕ.

84(82): 1 ∀_{{n∈ℕ \atop n≥N_{1}}} |f_{0}[n] − a_{0}| < ε_{0}/2.

85(81): 1 N_{2} ∈ ℕ ∧ ∀_{{n∈ℕ \atop n≥N_{2}}} |g_{0}[n] − b_{0}| < ε_{0}/2.

86(85): 1 N_{2} ∈ ℕ.

87(85): 1 ∀_{{n∈ℕ \atop n≥N_{2}}} |g_{0}[n] − b_{0}| < ε_{0}/2.

88(54): 0 N^{∗} ∈ ℕ ∧ ∀_{{n∈ℕ \atop n≥N^{∗}}} |(f_{0} + g_{0})[n] − (a_{0} + b_{0})| < ε_{0}.

97(88): 0 ∀_{{n∈ℕ \atop n≥max[N_{1},N_{2}]}} |(f_{0} + g_{0})[n] − (a_{0} + b_{0})| < ε_{0}.

98(97): 0 (n_{0} ∈ ℕ ∧ n_{0} ≥ max[N_{1}, N_{2}]) → |(f_{0} + g_{0})[n_{0}] − (a_{0} + b_{0})| < ε_{0}.

99(98): 1 n_{0} ∈ ℕ ∧ n_{0} ≥ max[N_{1}, N_{2}].

100(98): 0 |(f_{0} + g_{0})[n_{0}] − (a_{0} + b_{0})| < ε_{0}.

101(99): 1 n_{0} ∈ ℕ.

102(99): 1 n_{0} ≥ max[N_{1}, N_{2}].

next page

89(88): 0 N^{∗} ∈ ℕ.

90(A5): 1 ∀_{x∈ℕ} ∀_{y∈ℕ} max[x, y] ∈ ℕ.

91(90): 1 X^{∗} ∈ ℕ → ∀_{y∈ℕ} max[X^{∗}, y] ∈ ℕ.

93(91): 1 ∀_{y∈ℕ} max[N_{1}, y] ∈ ℕ.

94(93): 1 Y^{∗} ∈ ℕ → max[N_{1}, Y^{∗}] ∈ ℕ.

95(94): 0 Y^{∗} ∈ ℕ._{{*(86,95) \atop by \{Y^{∗} ← N_{2}\}}} 96(94): 1 max[N_{1}, N_{2}] ∈ ℕ.

{*(89,96) \atop by \{N^{∗} ← max[N_{1}, N_{2}]\}}

92(91): 0 X^{∗} ∈ ℕ._{{*(83,92) \atop by \{X^{∗} ← N_{1}\}}}

⋮

102(99): 1 n_{0} ≥ max[N_{1}, N_{2}].

103(84): 1 (N_{1}^{∗} ∈ ℕ ∧ N_{1}^{∗} ≥ N_{1}) → |f_{0}[N_{1}^{∗}] − a_{0}| < ε_{0}/2.

104(103): 0 N_{1}^{∗} ∈ ℕ ∧ N_{1}^{∗} ≥ N_{1}.

105(104): 0 N_{1}^{∗} ∈ ℕ._{{*(101,105) \atop by \{N_{1}^{∗} ← n_{0}\}}}

106(104): 0 n_{0} ≥ N_{1}.

107(A6): 1 ∀_{x∈ℕ} ∀_{y∈ℕ} ∀_{z∈ℕ} x ≥ max[y, z] → x ≥ y.

108(107): 1 (X^{∗} ∈ ℕ ∧ Y^{∗} ∈ ℕ ∧ Z^{∗} ∈ ℕ) → (X^{∗} ≥ max[Y^{∗}, Z^{∗}] → X^{∗} ≥ Y^{∗}).

109(108): 1 X^{∗} ≥ max[Y^{∗}, Z^{∗}] → X^{∗} ≥ Y^{∗}.

110(109): 0 X^{∗} ≥ max[Y^{∗}, Z^{∗}]._{{*(102,110) \atop by \{X^{∗} ← n_{0}, Y^{∗} ← N_{1}, Z^{∗} ← N_{2}\}}} 111(109): 1 n_{0} ≥ N_{1}._{{*(106,111) \atop by \{\}}}

112(108): 0 n_{0} ∈ ℕ ∧ N_{1} ∈ ℕ ∧ N_{2} ∈ ℕ._{113(112): 0 n_{0} ∈ ℕ._{{*(101,113) \atop by \{\}}} 114(112): 0 N_{1} ∈ ℕ._{{*(83,114) \atop by \{\}}} 115(112): 0 N_{2} ∈ ℕ._{{*(86,115) \atop by \{\}}}}

116(103): 1 |f_{0}[n_{0}] − a_{0}| < ε_{0}/2. next tree

⋮

116(103): 1 |f_{0}[n_{0}] − a_{0}| < ε_{0}/2.

117(87): 1 (N_{2}^{∗} ∈ ℕ ∧ N_{2}^{∗} ≥ N_{2}) → |g_{0}[N_{2}^{∗}] − b_{0}| < ε_{0}/2.

118(117): 0 N_{2}^{∗} ∈ ℕ ∧ N_{2}^{∗} ≥ N_{2}.

119(118): 0 N_{2}^{∗} ∈ ℕ._{{*(101,119) \atop by \{N_{2}^{∗} ← n_{0}\}}}

120(118): 0 n_{0} ≥ N_{2}.

121(A7): 1 ∀_{x∈ℕ} ∀_{y∈ℕ} ∀_{z∈ℕ} x ≥ max[y, z] → x ≥ z.

122(121): 1 (X^{∗} ∈ ℕ ∧ Y^{∗} ∈ ℕ ∧ Z^{∗} ∈ ℕ) → (X^{∗} ≥ max[Y^{∗}, Z^{∗}] → X^{∗} ≥ Z^{∗}).

123(122): 1 X^{∗} ≥ max[Y^{∗}, Z^{∗}] → X^{∗} ≥ Z^{∗}.

124(123): 0 X^{∗} ≥ max[Y^{∗}, Z^{∗}]._{{*(102,124) \atop by \{X^{∗} ← n_{0}, Y^{∗} ← N_{1}, Z^{∗} ← N_{2}\}}} 125(123): 1 n_{0} ≥ N_{2}._{{*(120,125) \atop by \{\}}}

126(122): 0 n_{0} ∈ ℕ ∧ N_{1} ∈ ℕ ∧ N_{2} ∈ ℕ._{127(126): 0 n_{0} ∈ ℕ._{{*(101,127) \atop by \{\}}} 128(126): 0 N_{1} ∈ ℕ._{{*(83,128) \atop by \{\}}} 129(126): 0 N_{2} ∈ ℕ._{{*(86,129) \atop by \{\}}}}

130(117): 1 |g_{0}[n_{0}] − b_{0}| < ε_{0}/2. next tree

⋮

130(117): 1 |g_{0}[n_{0}] − b_{0}| < ε_{0}/2.

131(A8): 1 ∀_{{f \atop seq[f]}} ∀_{{g \atop seq[g]}} ∀_{n∈ℕ} ∀_{ε∈ℝ} ∀_{a∈ℝ} ∀_{b∈ℝ} (|f[n] − a| < ε/2 ∧ |g[n] − b| < ε/2) → |(f + g)[n] − (a + b)| < ε.

132(131): 1 (seq[F^{∗∗}], seq[G^{∗∗}], N^{∗∗} ∈ ℕ, E^{∗∗} ∈ ℝ, A^{∗∗} ∈ ℝ, B^{∗∗} ∈ ℝ) → (|f[n] − a| < ε/2 ∧ |g[n] − b| < ε/2) → |(f + g)[n] − (a + b)| < ε.

133(132): 0 seq[F^{∗∗}], seq[G^{∗∗}], N^{∗∗} ∈ ℕ, E^{∗∗} ∈ ℝ, A^{∗∗} ∈ ℝ, B^{∗∗} ∈ ℝ.

134(133): 0 seq[F^{∗∗}]._{{*(1,134) \atop by \{F^{∗∗} ← f_{0}\}}} 135(133): 0 seq[G^{∗∗}]._{{*(3,135) \atop by \{G^{∗∗} ← g_{0}\}}}_{136(133): 0 N^{∗∗} ∈ ℕ._{{*(101,136) \atop by \{N^{∗∗} ← n_{0}\}}} 137(133): 0 E^{∗∗} ∈ ℝ._{{*(55,137) \atop by \{E^{∗∗} ← ε_{0}\}}} 138(133): 0 A^{∗∗} ∈ ℝ._{{*(37,138) \atop by \{A^{∗∗} ← a_{0}\}}}} 139(133): 0 B^{∗∗} ∈ ℝ._{{*(40,139) \atop by \{B^{∗∗} ← b_{0}\}}}

140(132): 1 (|f_{0}[n_{0}] − a_{0}| < ε_{0}/2 ∧ |g_{0}[n_{0}] − b_{0}| < ε_{0}/2) → |(f_{0} + g_{0})[n_{0}] − (a_{0} + b_{0})| < ε_{0}. \begin{matrix}141(140): 0 |f_{0}[n_{0}] − a_{0}| < ε_{0}/2 ∧ |g_{0}[n_{0}] − b_{0}| < ε_{0}/2. \\ 142(141): 0 |f_{0}[n_{0}] − a_{0}| < ε_{0}/2._{{*(116,142) \atop by \{\}}} & 143(141): 0 |g_{0}[n_{0}] − b_{0}| < ε_{0}/2._{{*(130,143) \atop by \{\}}} \end{matrix} ; 144(140): 1 |(f_{0} + g_{0})[n_{0}] − (a_{0} + b_{0})| < ε_{0}._{{*(100,144) \atop by \{\}}}