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

Metamath Proof Explorer

Theorem climlec2

Description: Comparison of a constant to the limit of a sequence. (Contributed by NM, 28-Feb-2008) (Revised by Mario Carneiro, 1-Feb-2014)

Ref Expression
Hypotheses clim2ser.1 
|- Z = ( ZZ>= ` M )
climlec2.2 
|- ( ph -> M e. ZZ )
climlec2.3 
|- ( ph -> A e. RR )
climlec2.4 
|- ( ph -> F ~~> B )
climlec2.5 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
climlec2.6 
|- ( ( ph /\ k e. Z ) -> A <_ ( F ` k ) )
Assertion climlec2 
|- ( ph -> A <_ B )

Proof

Step Hyp Ref Expression
1 clim2ser.1 
 |-  Z = ( ZZ>= ` M )
2 climlec2.2 
 |-  ( ph -> M e. ZZ )
3 climlec2.3 
 |-  ( ph -> A e. RR )
4 climlec2.4 
 |-  ( ph -> F ~~> B )
5 climlec2.5 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
6 climlec2.6 
 |-  ( ( ph /\ k e. Z ) -> A <_ ( F ` k ) )
7 3 recnd 
 |-  ( ph -> A e. CC )
8 0z 
 |-  0 e. ZZ
9 uzssz 
 |-  ( ZZ>= ` 0 ) C_ ZZ
10 zex 
 |-  ZZ e. _V
11 9 10 climconst2 
 |-  ( ( A e. CC /\ 0 e. ZZ ) -> ( ZZ X. { A } ) ~~> A )
12 7 8 11 sylancl 
 |-  ( ph -> ( ZZ X. { A } ) ~~> A )
13 eluzelz 
 |-  ( k e. ( ZZ>= ` M ) -> k e. ZZ )
14 13 1 eleq2s 
 |-  ( k e. Z -> k e. ZZ )
15 fvconst2g 
 |-  ( ( A e. RR /\ k e. ZZ ) -> ( ( ZZ X. { A } ) ` k ) = A )
16 3 14 15 syl2an 
 |-  ( ( ph /\ k e. Z ) -> ( ( ZZ X. { A } ) ` k ) = A )
17 3 adantr 
 |-  ( ( ph /\ k e. Z ) -> A e. RR )
18 16 17 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( ( ZZ X. { A } ) ` k ) e. RR )
19 16 6 eqbrtrd 
 |-  ( ( ph /\ k e. Z ) -> ( ( ZZ X. { A } ) ` k ) <_ ( F ` k ) )
20 1 2 12 4 18 5 19 climle 
 |-  ( ph -> A <_ B )