Metamath Proof Explorer

Theorem iseraltlem1

Description: Lemma for iseralt . A decreasing sequence with limit zero consists of positive terms. (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypotheses iseralt.1 
|- Z = ( ZZ>= ` M )
iseralt.2 
|- ( ph -> M e. ZZ )
iseralt.3 
|- ( ph -> G : Z --> RR )
iseralt.4 
|- ( ( ph /\ k e. Z ) -> ( G ` ( k + 1 ) ) <_ ( G ` k ) )
iseralt.5 
|- ( ph -> G ~~> 0 )
Assertion iseraltlem1 
|- ( ( ph /\ N e. Z ) -> 0 <_ ( G ` N ) )

Proof

Step Hyp Ref Expression
1 iseralt.1 
 |-  Z = ( ZZ>= ` M )
2 iseralt.2 
 |-  ( ph -> M e. ZZ )
3 iseralt.3 
 |-  ( ph -> G : Z --> RR )
4 iseralt.4 
 |-  ( ( ph /\ k e. Z ) -> ( G ` ( k + 1 ) ) <_ ( G ` k ) )
5 iseralt.5 
 |-  ( ph -> G ~~> 0 )
6 eqid 
 |-  ( ZZ>= ` N ) = ( ZZ>= ` N )
7 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
8 7 1 eleq2s 
 |-  ( N e. Z -> N e. ZZ )
9 8 adantl 
 |-  ( ( ph /\ N e. Z ) -> N e. ZZ )
10 5 adantr 
 |-  ( ( ph /\ N e. Z ) -> G ~~> 0 )
11 3 ffvelrnda 
 |-  ( ( ph /\ N e. Z ) -> ( G ` N ) e. RR )
12 11 recnd 
 |-  ( ( ph /\ N e. Z ) -> ( G ` N ) e. CC )
13 1z 
 |-  1 e. ZZ
14 uzssz 
 |-  ( ZZ>= ` 1 ) C_ ZZ
15 zex 
 |-  ZZ e. _V
16 14 15 climconst2 
 |-  ( ( ( G ` N ) e. CC /\ 1 e. ZZ ) -> ( ZZ X. { ( G ` N ) } ) ~~> ( G ` N ) )
17 12 13 16 sylancl 
 |-  ( ( ph /\ N e. Z ) -> ( ZZ X. { ( G ` N ) } ) ~~> ( G ` N ) )
18 3 ad2antrr 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. ( ZZ>= ` N ) ) -> G : Z --> RR )
19 1 uztrn2 
 |-  ( ( N e. Z /\ n e. ( ZZ>= ` N ) ) -> n e. Z )
20 19 adantll 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. ( ZZ>= ` N ) ) -> n e. Z )
21 18 20 ffvelrnd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. ( ZZ>= ` N ) ) -> ( G ` n ) e. RR )
22 eluzelz 
 |-  ( n e. ( ZZ>= ` N ) -> n e. ZZ )
23 22 adantl 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. ( ZZ>= ` N ) ) -> n e. ZZ )
24 fvex 
 |-  ( G ` N ) e. _V
25 24 fvconst2 
 |-  ( n e. ZZ -> ( ( ZZ X. { ( G ` N ) } ) ` n ) = ( G ` N ) )
26 23 25 syl 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. ( ZZ>= ` N ) ) -> ( ( ZZ X. { ( G ` N ) } ) ` n ) = ( G ` N ) )
27 11 adantr 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. ( ZZ>= ` N ) ) -> ( G ` N ) e. RR )
28 26 27 eqeltrd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. ( ZZ>= ` N ) ) -> ( ( ZZ X. { ( G ` N ) } ) ` n ) e. RR )
29 simpr 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. ( ZZ>= ` N ) ) -> n e. ( ZZ>= ` N ) )
30 18 adantr 
 |-  ( ( ( ( ph /\ N e. Z ) /\ n e. ( ZZ>= ` N ) ) /\ k e. ( N ... n ) ) -> G : Z --> RR )
31 simplr 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. ( ZZ>= ` N ) ) -> N e. Z )
32 elfzuz 
 |-  ( k e. ( N ... n ) -> k e. ( ZZ>= ` N ) )
33 1 uztrn2 
 |-  ( ( N e. Z /\ k e. ( ZZ>= ` N ) ) -> k e. Z )
34 31 32 33 syl2an 
 |-  ( ( ( ( ph /\ N e. Z ) /\ n e. ( ZZ>= ` N ) ) /\ k e. ( N ... n ) ) -> k e. Z )
35 30 34 ffvelrnd 
 |-  ( ( ( ( ph /\ N e. Z ) /\ n e. ( ZZ>= ` N ) ) /\ k e. ( N ... n ) ) -> ( G ` k ) e. RR )
36 simpl 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. ( ZZ>= ` N ) ) -> ( ph /\ N e. Z ) )
37 elfzuz 
 |-  ( k e. ( N ... ( n - 1 ) ) -> k e. ( ZZ>= ` N ) )
38 33 adantll 
 |-  ( ( ( ph /\ N e. Z ) /\ k e. ( ZZ>= ` N ) ) -> k e. Z )
39 4 adantlr 
 |-  ( ( ( ph /\ N e. Z ) /\ k e. Z ) -> ( G ` ( k + 1 ) ) <_ ( G ` k ) )
40 38 39 syldan 
 |-  ( ( ( ph /\ N e. Z ) /\ k e. ( ZZ>= ` N ) ) -> ( G ` ( k + 1 ) ) <_ ( G ` k ) )
41 36 37 40 syl2an 
 |-  ( ( ( ( ph /\ N e. Z ) /\ n e. ( ZZ>= ` N ) ) /\ k e. ( N ... ( n - 1 ) ) ) -> ( G ` ( k + 1 ) ) <_ ( G ` k ) )
42 29 35 41 monoord2 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. ( ZZ>= ` N ) ) -> ( G ` n ) <_ ( G ` N ) )
43 42 26 breqtrrd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. ( ZZ>= ` N ) ) -> ( G ` n ) <_ ( ( ZZ X. { ( G ` N ) } ) ` n ) )
44 6 9 10 17 21 28 43 climle 
 |-  ( ( ph /\ N e. Z ) -> 0 <_ ( G ` N ) )