Step |
Hyp |
Ref |
Expression |
1 |
|
1z |
⊢ 1 ∈ ℤ |
2 |
|
fzsubel |
⊢ ( ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝐾 ∈ ( 1 ... 𝑁 ) ↔ ( 𝐾 − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ) ) |
3 |
1 2
|
mpanl1 |
⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝐾 ∈ ( 1 ... 𝑁 ) ↔ ( 𝐾 − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ) ) |
4 |
1 3
|
mpanr2 |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ∈ ( 1 ... 𝑁 ) ↔ ( 𝐾 − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ) ) |
5 |
|
1m1e0 |
⊢ ( 1 − 1 ) = 0 |
6 |
5
|
oveq1i |
⊢ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) = ( 0 ... ( 𝑁 − 1 ) ) |
7 |
6
|
eleq2i |
⊢ ( ( 𝐾 − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ↔ ( 𝐾 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) |
8 |
4 7
|
bitrdi |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ∈ ( 1 ... 𝑁 ) ↔ ( 𝐾 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ) |
9 |
8
|
ancoms |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 1 ... 𝑁 ) ↔ ( 𝐾 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ) |