Step |
Hyp |
Ref |
Expression |
1 |
|
psgnfzto1st.d |
⊢ 𝐷 = ( 1 ... 𝑁 ) |
2 |
|
psgnfzto1st.p |
⊢ 𝑃 = ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐼 , if ( 𝑖 ≤ 𝐼 , ( 𝑖 − 1 ) , 𝑖 ) ) ) |
3 |
|
iftrue |
⊢ ( 𝑖 = 1 → if ( 𝑖 = 1 , 𝐼 , if ( 𝑖 ≤ 𝐼 , ( 𝑖 − 1 ) , 𝑖 ) ) = 𝐼 ) |
4 |
|
elfzuz2 |
⊢ ( 𝐼 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) ) |
5 |
4 1
|
eleq2s |
⊢ ( 𝐼 ∈ 𝐷 → 𝑁 ∈ ( ℤ≥ ‘ 1 ) ) |
6 |
|
eluzfz1 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... 𝑁 ) ) |
7 |
6 1
|
eleqtrrdi |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ 𝐷 ) |
8 |
5 7
|
syl |
⊢ ( 𝐼 ∈ 𝐷 → 1 ∈ 𝐷 ) |
9 |
|
id |
⊢ ( 𝐼 ∈ 𝐷 → 𝐼 ∈ 𝐷 ) |
10 |
2 3 8 9
|
fvmptd3 |
⊢ ( 𝐼 ∈ 𝐷 → ( 𝑃 ‘ 1 ) = 𝐼 ) |