Metamath Proof Explorer


Theorem climsub

Description: Limit of the difference of two converging sequences. Proposition 12-2.1(b) of Gleason p. 168. (Contributed by NM, 4-Aug-2007) (Proof shortened by Mario Carneiro, 1-Feb-2014)

Ref Expression
Hypotheses climadd.1
|- Z = ( ZZ>= ` M )
climadd.2
|- ( ph -> M e. ZZ )
climadd.4
|- ( ph -> F ~~> A )
climadd.6
|- ( ph -> H e. X )
climadd.7
|- ( ph -> G ~~> B )
climadd.8
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
climadd.9
|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
climsub.h
|- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) - ( G ` k ) ) )
Assertion climsub
|- ( ph -> H ~~> ( A - B ) )

Proof

Step Hyp Ref Expression
1 climadd.1
 |-  Z = ( ZZ>= ` M )
2 climadd.2
 |-  ( ph -> M e. ZZ )
3 climadd.4
 |-  ( ph -> F ~~> A )
4 climadd.6
 |-  ( ph -> H e. X )
5 climadd.7
 |-  ( ph -> G ~~> B )
6 climadd.8
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
7 climadd.9
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
8 climsub.h
 |-  ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) - ( G ` k ) ) )
9 climcl
 |-  ( F ~~> A -> A e. CC )
10 3 9 syl
 |-  ( ph -> A e. CC )
11 climcl
 |-  ( G ~~> B -> B e. CC )
12 5 11 syl
 |-  ( ph -> B e. CC )
13 subcl
 |-  ( ( u e. CC /\ v e. CC ) -> ( u - v ) e. CC )
14 13 adantl
 |-  ( ( ph /\ ( u e. CC /\ v e. CC ) ) -> ( u - v ) e. CC )
15 simpr
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR+ )
16 10 adantr
 |-  ( ( ph /\ x e. RR+ ) -> A e. CC )
17 12 adantr
 |-  ( ( ph /\ x e. RR+ ) -> B e. CC )
18 subcn2
 |-  ( ( x e. RR+ /\ A e. CC /\ B e. CC ) -> E. y e. RR+ E. z e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u - v ) - ( A - B ) ) ) < x ) )
19 15 16 17 18 syl3anc
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. RR+ E. z e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u - v ) - ( A - B ) ) ) < x ) )
20 1 2 10 12 14 3 5 4 19 6 7 8 climcn2
 |-  ( ph -> H ~~> ( A - B ) )