Metamath Proof Explorer

Theorem elfzo1elm1fzo0

Description: Membership of a positive integer decremented by one in a half-open range of nonnegative integers. (Contributed by AV, 20-Mar-2021)

Ref Expression
Assertion elfzo1elm1fzo0 ⊢ I ∈ 1 ..^ N → I − 1 ∈ 0 ..^ N − 1

Proof

Step Hyp Ref Expression
1 elfzoelz ⊢ I ∈ 1 ..^ N → I ∈ ℤ
2 elfzoel2 ⊢ I ∈ 1 ..^ N → N ∈ ℤ
3 1 2 jca ⊢ I ∈ 1 ..^ N → I ∈ ℤ ∧ N ∈ ℤ
4 elfzom1b ⊢ I ∈ ℤ ∧ N ∈ ℤ → I ∈ 1 ..^ N ↔ I − 1 ∈ 0 ..^ N − 1
5 4 biimpd ⊢ I ∈ ℤ ∧ N ∈ ℤ → I ∈ 1 ..^ N → I − 1 ∈ 0 ..^ N − 1
6 3 5 mpcom ⊢ I ∈ 1 ..^ N → I − 1 ∈ 0 ..^ N − 1