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 
|- ( ( ph /\ x e. A ) -> B e. V )
rlimadd.4 
|- ( ( ph /\ x e. A ) -> C e. V )
rlimadd.5 
|- ( ph -> ( x e. A |-> B ) ~~>r D )
rlimadd.6 
|- ( ph -> ( x e. A |-> C ) ~~>r E )
Assertion rlimsub 
|- ( ph -> ( x e. A |-> ( B - C ) ) ~~>r ( D - E ) )

Proof

Step Hyp Ref Expression
1 rlimadd.3 
 |-  ( ( ph /\ x e. A ) -> B e. V )
2 rlimadd.4 
 |-  ( ( ph /\ x e. A ) -> C e. V )
3 rlimadd.5 
 |-  ( ph -> ( x e. A |-> B ) ~~>r D )
4 rlimadd.6 
 |-  ( ph -> ( x e. A |-> C ) ~~>r E )
5 1 3 rlimmptrcl 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
6 2 4 rlimmptrcl 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
7 rlimcl 
 |-  ( ( x e. A |-> B ) ~~>r D -> D e. CC )
8 3 7 syl 
 |-  ( ph -> D e. CC )
9 rlimcl 
 |-  ( ( x e. A |-> C ) ~~>r E -> E e. CC )
10 4 9 syl 
 |-  ( ph -> E e. CC )
11 subf 
 |-  - : ( CC X. CC ) --> CC
12 11 a1i 
 |-  ( ph -> - : ( CC X. CC ) --> CC )
13 simpr 
 |-  ( ( ph /\ y e. RR+ ) -> y e. RR+ )
14 8 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> D e. CC )
15 10 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> E e. CC )
16 subcn2 
 |-  ( ( y e. RR+ /\ D e. CC /\ E e. CC ) -> E. z e. RR+ E. w e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - D ) ) < z /\ ( abs ` ( v - E ) ) < w ) -> ( abs ` ( ( u - v ) - ( D - E ) ) ) < y ) )
17 13 14 15 16 syl3anc 
 |-  ( ( ph /\ y e. RR+ ) -> E. z e. RR+ E. w e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - D ) ) < z /\ ( abs ` ( v - E ) ) < w ) -> ( abs ` ( ( u - v ) - ( D - E ) ) ) < y ) )
18 5 6 8 10 3 4 12 17 rlimcn2 
 |-  ( ph -> ( x e. A |-> ( B - C ) ) ~~>r ( D - E ) )