Theorem fz1fzo0m1

Description: Translation of one between closed and open integer ranges. (Contributed by Thierry Arnoux, 28-Jul-2020)

	Ref	Expression
Assertion	fz1fzo0m1	⊢ ( 𝑀 ∈ ( 1 ... 𝑁 ) → ( 𝑀 − 1 ) ∈ ( 0 ..^ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzmlbm	⊢ ( 𝑀 ∈ ( 1 ... 𝑁 ) → ( 𝑀 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
2		elfzel2	⊢ ( 𝑀 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ℤ )
3		fzoval	⊢ ( 𝑁 ∈ ℤ → ( 0 ..^ 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )
4	2 3	syl	⊢ ( 𝑀 ∈ ( 1 ... 𝑁 ) → ( 0 ..^ 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )
5	1 4	eleqtrrd	⊢ ( 𝑀 ∈ ( 1 ... 𝑁 ) → ( 𝑀 − 1 ) ∈ ( 0 ..^ 𝑁 ) )