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	7	con3i	⊢ ( ¬ 𝑀 ∈ ℤ → ¬ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
9		fzof	⊢ ..^ : ( ℤ × ℤ ) ⟶ 𝒫 ℤ
10	9	fdmi	⊢ dom ..^ = ( ℤ × ℤ )
11	10	ndmov	⊢ ( ¬ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ..^ 𝑁 ) = ∅ )
12	8 11	syl	⊢ ( ¬ 𝑀 ∈ ℤ → ( 𝑀 ..^ 𝑁 ) = ∅ )
13		simpl	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) → 𝑀 ∈ ℤ )
14	13	con3i	⊢ ( ¬ 𝑀 ∈ ℤ → ¬ ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) )
15		fzf	⊢ ... : ( ℤ × ℤ ) ⟶ 𝒫 ℤ
16	15	fdmi	⊢ dom ... = ( ℤ × ℤ )
17	16	ndmov	⊢ ( ¬ ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 𝑀 ... ( 𝑁 − 1 ) ) = ∅ )
18	14 17	syl	⊢ ( ¬ 𝑀 ∈ ℤ → ( 𝑀 ... ( 𝑁 − 1 ) ) = ∅ )
19	12 18	eqtr4d	⊢ ( ¬ 𝑀 ∈ ℤ → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
20	19	adantr	⊢ ( ( ¬ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
21	6 20	pm2.61ian	⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )