Metamath Proof Explorer


Theorem rlimsub

Description: Limit of the difference of two converging functions. Proposition 12-2.1(b) 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 rlimsub φ 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 rlimcl x A B D D
8 3 7 syl φ D
9 rlimcl x A C E E
10 4 9 syl φ E
11 subf : ×
12 11 a1i φ : ×
13 simpr φ y + y +
14 8 adantr φ y + D
15 10 adantr φ y + E
16 subcn2 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 8 10 3 4 12 17 rlimcn2 φ x A B C D E