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