Metamath Proof Explorer

Theorem climmulc2

Description: Limit of a sequence multiplied by a constant C . Corollary 12-2.2 of Gleason p. 171. (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 )
climmulc2.h 
|- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( C x. ( F ` k ) ) )
Assertion climmulc2 
|- ( ph -> G ~~> ( C x. 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 climmulc2.h 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) = ( C x. ( F ` k ) ) )
8 0z 
 |-  0 e. ZZ
9 uzssz 
 |-  ( ZZ>= ` 0 ) C_ ZZ
10 zex 
 |-  ZZ e. _V
11 9 10 climconst2 
 |-  ( ( C e. CC /\ 0 e. ZZ ) -> ( ZZ X. { C } ) ~~> C )
12 4 8 11 sylancl 
 |-  ( ph -> ( ZZ X. { C } ) ~~> C )
13 eluzelz 
 |-  ( k e. ( ZZ>= ` M ) -> k e. ZZ )
14 13 1 eleq2s 
 |-  ( k e. Z -> k e. ZZ )
15 fvconst2g 
 |-  ( ( C e. CC /\ k e. ZZ ) -> ( ( ZZ X. { C } ) ` k ) = C )
16 4 14 15 syl2an 
 |-  ( ( ph /\ k e. Z ) -> ( ( ZZ X. { C } ) ` k ) = C )
17 4 adantr 
 |-  ( ( ph /\ k e. Z ) -> C e. CC )
18 16 17 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( ( ZZ X. { C } ) ` k ) e. CC )
19 16 oveq1d 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( ZZ X. { C } ) ` k ) x. ( F ` k ) ) = ( C x. ( F ` k ) ) )
20 7 19 eqtr4d 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) = ( ( ( ZZ X. { C } ) ` k ) x. ( F ` k ) ) )
21 1 2 12 5 3 18 6 20 climmul 
 |-  ( ph -> G ~~> ( C x. A ) )