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 ) )

Metamath Proof Explorer

Theorem climadd

Proof