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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climsuselem1.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climsuselem1.3 ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑀 ) ∈ 𝑍 )
climsuselem1.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐼 ‘ ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ ( ( 𝐼 ‘ 𝑘 ) + 1 ) ) )
Assertion climsuselem1 ( ( 𝜑 ∧ 𝐾 ∈ 𝑍 ) → ( 𝐼 ‘ 𝐾 ) ∈ ( ℤ≥ ‘ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 climsuselem1.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 climsuselem1.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 climsuselem1.3 ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑀 ) ∈ 𝑍 )
4 climsuselem1.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐼 ‘ ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ ( ( 𝐼 ‘ 𝑘 ) + 1 ) ) )
5 1 eleq2i ⊢ ( 𝐾 ∈ 𝑍 ↔ 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
6 5 biimpi ⊢ ( 𝐾 ∈ 𝑍 → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
7 6 adantl ⊢ ( ( 𝜑 ∧ 𝐾 ∈ 𝑍 ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
8 simpl ⊢ ( ( 𝜑 ∧ 𝐾 ∈ 𝑍 ) → 𝜑 )
9 fveq2 ⊢ ( 𝑗 = 𝑀 → ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑀 ) )
10 fveq2 ⊢ ( 𝑗 = 𝑀 → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ 𝑀 ) )
11 9 10 eleq12d ⊢ ( 𝑗 = 𝑀 → ( ( 𝐼 ‘ 𝑗 ) ∈ ( ℤ≥ ‘ 𝑗 ) ↔ ( 𝐼 ‘ 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
12 11 imbi2d ⊢ ( 𝑗 = 𝑀 → ( ( 𝜑 → ( 𝐼 ‘ 𝑗 ) ∈ ( ℤ≥ ‘ 𝑗 ) ) ↔ ( 𝜑 → ( 𝐼 ‘ 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ) )
13 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑘 ) )
14 fveq2 ⊢ ( 𝑗 = 𝑘 → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ 𝑘 ) )
15 13 14 eleq12d ⊢ ( 𝑗 = 𝑘 → ( ( 𝐼 ‘ 𝑗 ) ∈ ( ℤ≥ ‘ 𝑗 ) ↔ ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) )
16 15 imbi2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝜑 → ( 𝐼 ‘ 𝑗 ) ∈ ( ℤ≥ ‘ 𝑗 ) ) ↔ ( 𝜑 → ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) ) )
17 fveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ ( 𝑘 + 1 ) ) )
18 fveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ ( 𝑘 + 1 ) ) )
19 17 18 eleq12d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝐼 ‘ 𝑗 ) ∈ ( ℤ≥ ‘ 𝑗 ) ↔ ( 𝐼 ‘ ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) )
20 19 imbi2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝜑 → ( 𝐼 ‘ 𝑗 ) ∈ ( ℤ≥ ‘ 𝑗 ) ) ↔ ( 𝜑 → ( 𝐼 ‘ ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) ) )
21 fveq2 ⊢ ( 𝑗 = 𝐾 → ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝐾 ) )
22 fveq2 ⊢ ( 𝑗 = 𝐾 → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ 𝐾 ) )
23 21 22 eleq12d ⊢ ( 𝑗 = 𝐾 → ( ( 𝐼 ‘ 𝑗 ) ∈ ( ℤ≥ ‘ 𝑗 ) ↔ ( 𝐼 ‘ 𝐾 ) ∈ ( ℤ≥ ‘ 𝐾 ) ) )
24 23 imbi2d ⊢ ( 𝑗 = 𝐾 → ( ( 𝜑 → ( 𝐼 ‘ 𝑗 ) ∈ ( ℤ≥ ‘ 𝑗 ) ) ↔ ( 𝜑 → ( 𝐼 ‘ 𝐾 ) ∈ ( ℤ≥ ‘ 𝐾 ) ) ) )
25 3 1 eleqtrdi ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
26 25 a1i ⊢ ( 𝑀 ∈ ℤ → ( 𝜑 → ( 𝐼 ‘ 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
27 simpr ⊢ ( ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 → ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) ) ∧ 𝜑 ) → 𝜑 )
28 simpll ⊢ ( ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 → ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) ) ∧ 𝜑 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
29 simplr ⊢ ( ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 → ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) ) ∧ 𝜑 ) → ( 𝜑 → ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) )
30 27 29 mpd ⊢ ( ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 → ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) ) ∧ 𝜑 ) → ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) )
31 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℤ )
32 31 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑘 ∈ ℤ )
33 32 peano2zd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝑘 + 1 ) ∈ ℤ )
34 33 zred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝑘 + 1 ) ∈ ℝ )
35 eluzelre ⊢ ( ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) → ( 𝐼 ‘ 𝑘 ) ∈ ℝ )
36 35 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝐼 ‘ 𝑘 ) ∈ ℝ )
37 1red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) → 1 ∈ ℝ )
38 36 37 readdcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( ( 𝐼 ‘ 𝑘 ) + 1 ) ∈ ℝ )
39 1 eqimss2i ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ 𝑍
40 39 a1i ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑀 ) ⊆ 𝑍 )
41 40 sseld ⊢ ( 𝜑 → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ 𝑍 ) )
42 41 imdistani ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) )
43 42 4 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐼 ‘ ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ ( ( 𝐼 ‘ 𝑘 ) + 1 ) ) )
44 43 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝐼 ‘ ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ ( ( 𝐼 ‘ 𝑘 ) + 1 ) ) )
45 eluzelz ⊢ ( ( 𝐼 ‘ ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ ( ( 𝐼 ‘ 𝑘 ) + 1 ) ) → ( 𝐼 ‘ ( 𝑘 + 1 ) ) ∈ ℤ )
46 44 45 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝐼 ‘ ( 𝑘 + 1 ) ) ∈ ℤ )
47 46 zred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝐼 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
48 32 zred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑘 ∈ ℝ )
49 eluzle ⊢ ( ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) → 𝑘 ≤ ( 𝐼 ‘ 𝑘 ) )
50 49 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑘 ≤ ( 𝐼 ‘ 𝑘 ) )
51 48 36 37 50 leadd1dd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝑘 + 1 ) ≤ ( ( 𝐼 ‘ 𝑘 ) + 1 ) )
52 eluzle ⊢ ( ( 𝐼 ‘ ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ ( ( 𝐼 ‘ 𝑘 ) + 1 ) ) → ( ( 𝐼 ‘ 𝑘 ) + 1 ) ≤ ( 𝐼 ‘ ( 𝑘 + 1 ) ) )
53 44 52 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( ( 𝐼 ‘ 𝑘 ) + 1 ) ≤ ( 𝐼 ‘ ( 𝑘 + 1 ) ) )
54 34 38 47 51 53 letrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝑘 + 1 ) ≤ ( 𝐼 ‘ ( 𝑘 + 1 ) ) )
55 eluz ⊢ ( ( ( 𝑘 + 1 ) ∈ ℤ ∧ ( 𝐼 ‘ ( 𝑘 + 1 ) ) ∈ ℤ ) → ( ( 𝐼 ‘ ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ↔ ( 𝑘 + 1 ) ≤ ( 𝐼 ‘ ( 𝑘 + 1 ) ) ) )
56 33 46 55 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( ( 𝐼 ‘ ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ↔ ( 𝑘 + 1 ) ≤ ( 𝐼 ‘ ( 𝑘 + 1 ) ) ) )
57 54 56 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝐼 ‘ ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) )
58 27 28 30 57 syl3anc ⊢ ( ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝜑 → ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) ) ∧ 𝜑 ) → ( 𝐼 ‘ ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) )
59 58 exp31 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝜑 → ( 𝐼 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝜑 → ( 𝐼 ‘ ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) ) )
60 12 16 20 24 26 59 uzind4 ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( 𝐼 ‘ 𝐾 ) ∈ ( ℤ≥ ‘ 𝐾 ) ) )
61 7 8 60 sylc ⊢ ( ( 𝜑 ∧ 𝐾 ∈ 𝑍 ) → ( 𝐼 ‘ 𝐾 ) ∈ ( ℤ≥ ‘ 𝐾 ) )