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 )