Theorem fzoval

Description: Value of the half-open integer set in terms of the closed integer set. (Contributed by Stefan O'Rear, 14-Aug-2015)

	Ref	Expression
Assertion	fzoval	⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑚 = 𝑀 → 𝑚 = 𝑀 )
2		oveq1	⊢ ( 𝑛 = 𝑁 → ( 𝑛 − 1 ) = ( 𝑁 − 1 ) )
3	1 2	oveqan12d	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) → ( 𝑚 ... ( 𝑛 − 1 ) ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
4		df-fzo	⊢ ..^ = ( 𝑚 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( 𝑚 ... ( 𝑛 − 1 ) ) )
5		ovex	⊢ ( 𝑀 ... ( 𝑁 − 1 ) ) ∈ V
6	3 4 5	ovmpoa	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
7		simpl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℤ )
8		fzof	⊢ ..^ : ( ℤ × ℤ ) ⟶ 𝒫 ℤ
9	8	fdmi	⊢ dom ..^ = ( ℤ × ℤ )
10	9	ndmov	⊢ ( ¬ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ..^ 𝑁 ) = ∅ )
11	7 10	nsyl5	⊢ ( ¬ 𝑀 ∈ ℤ → ( 𝑀 ..^ 𝑁 ) = ∅ )
12		simpl	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) → 𝑀 ∈ ℤ )
13		fzf	⊢ ... : ( ℤ × ℤ ) ⟶ 𝒫 ℤ
14	13	fdmi	⊢ dom ... = ( ℤ × ℤ )
15	14	ndmov	⊢ ( ¬ ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 𝑀 ... ( 𝑁 − 1 ) ) = ∅ )
16	12 15	nsyl5	⊢ ( ¬ 𝑀 ∈ ℤ → ( 𝑀 ... ( 𝑁 − 1 ) ) = ∅ )
17	11 16	eqtr4d	⊢ ( ¬ 𝑀 ∈ ℤ → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
18	17	adantr	⊢ ( ( ¬ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
19	6 18	pm2.61ian	⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )