This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem climaddc2

Description: Limit of a constant C added to each term of a sequence. (Contributed by NM, 24-Sep-2005) (Revised by Mario Carneiro, 3-Feb-2014)

Ref Expression
Hypotheses climadd.1 
|- Z = ( ZZ>= ` M )
climadd.2 
|- ( ph -> M e. ZZ )
climadd.4 
|- ( ph -> F ~~> A )
climaddc1.5 
|- ( ph -> C e. CC )
climaddc1.6 
|- ( ph -> G e. W )
climaddc1.7 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
climaddc2.h 
|- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( C + ( F ` k ) ) )
Assertion climaddc2 
|- ( ph -> G ~~> ( C + A ) )

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 climaddc1.5 
 |-  ( ph -> C e. CC )
5 climaddc1.6 
 |-  ( ph -> G e. W )
6 climaddc1.7 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
7 climaddc2.h 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) = ( C + ( F ` k ) ) )
8 4 adantr 
 |-  ( ( ph /\ k e. Z ) -> C e. CC )
9 8 6 7 comraddd 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) = ( ( F ` k ) + C ) )
10 1 2 3 4 5 6 9 climaddc1 
 |-  ( ph -> G ~~> ( A + C ) )
11 climcl 
 |-  ( F ~~> A -> A e. CC )
12 3 11 syl 
 |-  ( ph -> A e. CC )
13 12 4 addcomd 
 |-  ( ph -> ( A + C ) = ( C + A ) )
14 10 13 breqtrd 
 |-  ( ph -> G ~~> ( C + A ) )