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 = ( 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 )
	climadd.h	|- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) + ( G ` k ) ) )
Assertion	climadd	|- ( 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		climadd.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		addcl	|- ( ( 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		addcn2	|- ( ( 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 ) )