Metamath Proof Explorer

Theorem climsuselem1

Description: The subsequence index I has the expected properties: it belongs to the same upper integers as the original index, and it is always greater than or equal to the original index. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses climsuselem1.1 
|- Z = ( ZZ>= ` M )
climsuselem1.2 
|- ( ph -> M e. ZZ )
climsuselem1.3 
|- ( ph -> ( I ` M ) e. Z )
climsuselem1.4 
|- ( ( ph /\ k e. Z ) -> ( I ` ( k + 1 ) ) e. ( ZZ>= ` ( ( I ` k ) + 1 ) ) )
Assertion climsuselem1 
|- ( ( ph /\ K e. Z ) -> ( I ` K ) e. ( ZZ>= ` K ) )

Proof

Step Hyp Ref Expression
1 climsuselem1.1 
 |-  Z = ( ZZ>= ` M )
2 climsuselem1.2 
 |-  ( ph -> M e. ZZ )
3 climsuselem1.3 
 |-  ( ph -> ( I ` M ) e. Z )
4 climsuselem1.4 
 |-  ( ( ph /\ k e. Z ) -> ( I ` ( k + 1 ) ) e. ( ZZ>= ` ( ( I ` k ) + 1 ) ) )
5 1 eleq2i 
 |-  ( K e. Z <-> K e. ( ZZ>= ` M ) )
6 5 biimpi 
 |-  ( K e. Z -> K e. ( ZZ>= ` M ) )
7 6 adantl 
 |-  ( ( ph /\ K e. Z ) -> K e. ( ZZ>= ` M ) )
8 simpl 
 |-  ( ( ph /\ K e. Z ) -> ph )
9 fveq2 
 |-  ( j = M -> ( I ` j ) = ( I ` M ) )
10 fveq2 
 |-  ( j = M -> ( ZZ>= ` j ) = ( ZZ>= ` M ) )
11 9 10 eleq12d 
 |-  ( j = M -> ( ( I ` j ) e. ( ZZ>= ` j ) <-> ( I ` M ) e. ( ZZ>= ` M ) ) )
12 11 imbi2d 
 |-  ( j = M -> ( ( ph -> ( I ` j ) e. ( ZZ>= ` j ) ) <-> ( ph -> ( I ` M ) e. ( ZZ>= ` M ) ) ) )
13 fveq2 
 |-  ( j = k -> ( I ` j ) = ( I ` k ) )
14 fveq2 
 |-  ( j = k -> ( ZZ>= ` j ) = ( ZZ>= ` k ) )
15 13 14 eleq12d 
 |-  ( j = k -> ( ( I ` j ) e. ( ZZ>= ` j ) <-> ( I ` k ) e. ( ZZ>= ` k ) ) )
16 15 imbi2d 
 |-  ( j = k -> ( ( ph -> ( I ` j ) e. ( ZZ>= ` j ) ) <-> ( ph -> ( I ` k ) e. ( ZZ>= ` k ) ) ) )
17 fveq2 
 |-  ( j = ( k + 1 ) -> ( I ` j ) = ( I ` ( k + 1 ) ) )
18 fveq2 
 |-  ( j = ( k + 1 ) -> ( ZZ>= ` j ) = ( ZZ>= ` ( k + 1 ) ) )
19 17 18 eleq12d 
 |-  ( j = ( k + 1 ) -> ( ( I ` j ) e. ( ZZ>= ` j ) <-> ( I ` ( k + 1 ) ) e. ( ZZ>= ` ( k + 1 ) ) ) )
20 19 imbi2d 
 |-  ( j = ( k + 1 ) -> ( ( ph -> ( I ` j ) e. ( ZZ>= ` j ) ) <-> ( ph -> ( I ` ( k + 1 ) ) e. ( ZZ>= ` ( k + 1 ) ) ) ) )
21 fveq2 
 |-  ( j = K -> ( I ` j ) = ( I ` K ) )
22 fveq2 
 |-  ( j = K -> ( ZZ>= ` j ) = ( ZZ>= ` K ) )
23 21 22 eleq12d 
 |-  ( j = K -> ( ( I ` j ) e. ( ZZ>= ` j ) <-> ( I ` K ) e. ( ZZ>= ` K ) ) )
24 23 imbi2d 
 |-  ( j = K -> ( ( ph -> ( I ` j ) e. ( ZZ>= ` j ) ) <-> ( ph -> ( I ` K ) e. ( ZZ>= ` K ) ) ) )
25 3 1 eleqtrdi 
 |-  ( ph -> ( I ` M ) e. ( ZZ>= ` M ) )
26 25 a1i 
 |-  ( M e. ZZ -> ( ph -> ( I ` M ) e. ( ZZ>= ` M ) ) )
27 simpr 
 |-  ( ( ( k e. ( ZZ>= ` M ) /\ ( ph -> ( I ` k ) e. ( ZZ>= ` k ) ) ) /\ ph ) -> ph )
28 simpll 
 |-  ( ( ( k e. ( ZZ>= ` M ) /\ ( ph -> ( I ` k ) e. ( ZZ>= ` k ) ) ) /\ ph ) -> k e. ( ZZ>= ` M ) )
29 simplr 
 |-  ( ( ( k e. ( ZZ>= ` M ) /\ ( ph -> ( I ` k ) e. ( ZZ>= ` k ) ) ) /\ ph ) -> ( ph -> ( I ` k ) e. ( ZZ>= ` k ) ) )
30 27 29 mpd 
 |-  ( ( ( k e. ( ZZ>= ` M ) /\ ( ph -> ( I ` k ) e. ( ZZ>= ` k ) ) ) /\ ph ) -> ( I ` k ) e. ( ZZ>= ` k ) )
31 eluzelz 
 |-  ( k e. ( ZZ>= ` M ) -> k e. ZZ )
32 31 3ad2ant2 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) /\ ( I ` k ) e. ( ZZ>= ` k ) ) -> k e. ZZ )
33 32 peano2zd 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) /\ ( I ` k ) e. ( ZZ>= ` k ) ) -> ( k + 1 ) e. ZZ )
34 33 zred 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) /\ ( I ` k ) e. ( ZZ>= ` k ) ) -> ( k + 1 ) e. RR )
35 eluzelre 
 |-  ( ( I ` k ) e. ( ZZ>= ` k ) -> ( I ` k ) e. RR )
36 35 3ad2ant3 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) /\ ( I ` k ) e. ( ZZ>= ` k ) ) -> ( I ` k ) e. RR )
37 1red 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) /\ ( I ` k ) e. ( ZZ>= ` k ) ) -> 1 e. RR )
38 36 37 readdcld 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) /\ ( I ` k ) e. ( ZZ>= ` k ) ) -> ( ( I ` k ) + 1 ) e. RR )
39 1 eqimss2i 
 |-  ( ZZ>= ` M ) C_ Z
40 39 a1i 
 |-  ( ph -> ( ZZ>= ` M ) C_ Z )
41 40 sseld 
 |-  ( ph -> ( k e. ( ZZ>= ` M ) -> k e. Z ) )
42 41 imdistani 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ph /\ k e. Z ) )
43 42 4 syl 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( I ` ( k + 1 ) ) e. ( ZZ>= ` ( ( I ` k ) + 1 ) ) )
44 43 3adant3 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) /\ ( I ` k ) e. ( ZZ>= ` k ) ) -> ( I ` ( k + 1 ) ) e. ( ZZ>= ` ( ( I ` k ) + 1 ) ) )
45 eluzelz 
 |-  ( ( I ` ( k + 1 ) ) e. ( ZZ>= ` ( ( I ` k ) + 1 ) ) -> ( I ` ( k + 1 ) ) e. ZZ )
46 44 45 syl 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) /\ ( I ` k ) e. ( ZZ>= ` k ) ) -> ( I ` ( k + 1 ) ) e. ZZ )
47 46 zred 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) /\ ( I ` k ) e. ( ZZ>= ` k ) ) -> ( I ` ( k + 1 ) ) e. RR )
48 32 zred 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) /\ ( I ` k ) e. ( ZZ>= ` k ) ) -> k e. RR )
49 eluzle 
 |-  ( ( I ` k ) e. ( ZZ>= ` k ) -> k <_ ( I ` k ) )
50 49 3ad2ant3 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) /\ ( I ` k ) e. ( ZZ>= ` k ) ) -> k <_ ( I ` k ) )
51 48 36 37 50 leadd1dd 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) /\ ( I ` k ) e. ( ZZ>= ` k ) ) -> ( k + 1 ) <_ ( ( I ` k ) + 1 ) )
52 eluzle 
 |-  ( ( I ` ( k + 1 ) ) e. ( ZZ>= ` ( ( I ` k ) + 1 ) ) -> ( ( I ` k ) + 1 ) <_ ( I ` ( k + 1 ) ) )
53 44 52 syl 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) /\ ( I ` k ) e. ( ZZ>= ` k ) ) -> ( ( I ` k ) + 1 ) <_ ( I ` ( k + 1 ) ) )
54 34 38 47 51 53 letrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) /\ ( I ` k ) e. ( ZZ>= ` k ) ) -> ( k + 1 ) <_ ( I ` ( k + 1 ) ) )
55 eluz 
 |-  ( ( ( k + 1 ) e. ZZ /\ ( I ` ( k + 1 ) ) e. ZZ ) -> ( ( I ` ( k + 1 ) ) e. ( ZZ>= ` ( k + 1 ) ) <-> ( k + 1 ) <_ ( I ` ( k + 1 ) ) ) )
56 33 46 55 syl2anc 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) /\ ( I ` k ) e. ( ZZ>= ` k ) ) -> ( ( I ` ( k + 1 ) ) e. ( ZZ>= ` ( k + 1 ) ) <-> ( k + 1 ) <_ ( I ` ( k + 1 ) ) ) )
57 54 56 mpbird 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) /\ ( I ` k ) e. ( ZZ>= ` k ) ) -> ( I ` ( k + 1 ) ) e. ( ZZ>= ` ( k + 1 ) ) )
58 27 28 30 57 syl3anc 
 |-  ( ( ( k e. ( ZZ>= ` M ) /\ ( ph -> ( I ` k ) e. ( ZZ>= ` k ) ) ) /\ ph ) -> ( I ` ( k + 1 ) ) e. ( ZZ>= ` ( k + 1 ) ) )
59 58 exp31 
 |-  ( k e. ( ZZ>= ` M ) -> ( ( ph -> ( I ` k ) e. ( ZZ>= ` k ) ) -> ( ph -> ( I ` ( k + 1 ) ) e. ( ZZ>= ` ( k + 1 ) ) ) ) )
60 12 16 20 24 26 59 uzind4 
 |-  ( K e. ( ZZ>= ` M ) -> ( ph -> ( I ` K ) e. ( ZZ>= ` K ) ) )
61 7 8 60 sylc 
 |-  ( ( ph /\ K e. Z ) -> ( I ` K ) e. ( ZZ>= ` K ) )