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