Metamath Proof Explorer

Theorem fznatpl1

Description: Shift membership in a finite sequence of naturals. (Contributed by Scott Fenton, 17-Jul-2013)

Ref Expression
Assertion fznatpl1 ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝐼 + 1 ) ∈ ( 1 ... 𝑁 ) )

Proof

Step Hyp Ref Expression
1 1red ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 1 ∈ ℝ )
2 elfzelz ⊢ ( 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝐼 ∈ ℤ )
3 2 zred ⊢ ( 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝐼 ∈ ℝ )
4 3 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝐼 ∈ ℝ )
5 peano2re ⊢ ( 𝐼 ∈ ℝ → ( 𝐼 + 1 ) ∈ ℝ )
6 4 5 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝐼 + 1 ) ∈ ℝ )
7 peano2re ⊢ ( 1 ∈ ℝ → ( 1 + 1 ) ∈ ℝ )
8 1 7 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 1 + 1 ) ∈ ℝ )
9 1 ltp1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 1 < ( 1 + 1 ) )
10 elfzle1 ⊢ ( 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 1 ≤ 𝐼 )
11 10 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 1 ≤ 𝐼 )
12 1re ⊢ 1 ∈ ℝ
13 leadd1 ⊢ ( ( 1 ∈ ℝ ∧ 𝐼 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 1 ≤ 𝐼 ↔ ( 1 + 1 ) ≤ ( 𝐼 + 1 ) ) )
14 12 12 13 mp3an13 ⊢ ( 𝐼 ∈ ℝ → ( 1 ≤ 𝐼 ↔ ( 1 + 1 ) ≤ ( 𝐼 + 1 ) ) )
15 4 14 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 1 ≤ 𝐼 ↔ ( 1 + 1 ) ≤ ( 𝐼 + 1 ) ) )
16 11 15 mpbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 1 + 1 ) ≤ ( 𝐼 + 1 ) )
17 1 8 6 9 16 ltletrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 1 < ( 𝐼 + 1 ) )
18 1 6 17 ltled ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 1 ≤ ( 𝐼 + 1 ) )
19 elfzle2 ⊢ ( 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝐼 ≤ ( 𝑁 − 1 ) )
20 19 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝐼 ≤ ( 𝑁 − 1 ) )
21 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
22 21 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℤ )
23 22 zred ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℝ )
24 leaddsub ⊢ ( ( 𝐼 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝐼 + 1 ) ≤ 𝑁 ↔ 𝐼 ≤ ( 𝑁 − 1 ) ) )
25 12 24 mp3an2 ⊢ ( ( 𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝐼 + 1 ) ≤ 𝑁 ↔ 𝐼 ≤ ( 𝑁 − 1 ) ) )
26 3 23 25 syl2an2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐼 + 1 ) ≤ 𝑁 ↔ 𝐼 ≤ ( 𝑁 − 1 ) ) )
27 20 26 mpbird ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝐼 + 1 ) ≤ 𝑁 )
28 2 peano2zd ⊢ ( 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 𝐼 + 1 ) ∈ ℤ )
29 1z ⊢ 1 ∈ ℤ
30 elfz ⊢ ( ( ( 𝐼 + 1 ) ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐼 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ ( 𝐼 + 1 ) ∧ ( 𝐼 + 1 ) ≤ 𝑁 ) ) )
31 29 30 mp3an2 ⊢ ( ( ( 𝐼 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐼 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ ( 𝐼 + 1 ) ∧ ( 𝐼 + 1 ) ≤ 𝑁 ) ) )
32 28 22 31 syl2an2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐼 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ ( 𝐼 + 1 ) ∧ ( 𝐼 + 1 ) ≤ 𝑁 ) ) )
33 18 27 32 mpbir2and ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝐼 + 1 ) ∈ ( 1 ... 𝑁 ) )