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 ⊢ N ∈ ℕ ∧ I ∈ 1 … N − 1 → I + 1 ∈ 1 … N

Proof

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