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