# Metamath Proof Explorer

## 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 ${⊢}{N}\in ℤ\to \left({M}..^{N}\right)=\left({M}\dots {N}-1\right)$

### Proof

Step Hyp Ref Expression
1 id ${⊢}{m}={M}\to {m}={M}$
2 oveq1 ${⊢}{n}={N}\to {n}-1={N}-1$
3 1 2 oveqan12d ${⊢}\left({m}={M}\wedge {n}={N}\right)\to \left({m}\dots {n}-1\right)=\left({M}\dots {N}-1\right)$
4 df-fzo ${⊢}..^=\left({m}\in ℤ,{n}\in ℤ⟼\left({m}\dots {n}-1\right)\right)$
5 ovex ${⊢}\left({M}\dots {N}-1\right)\in \mathrm{V}$
6 3 4 5 ovmpoa ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}..^{N}\right)=\left({M}\dots {N}-1\right)$
7 simpl ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}\in ℤ$
8 fzof ${⊢}..^:ℤ×ℤ⟶𝒫ℤ$
9 8 fdmi ${⊢}\mathrm{dom}..^=ℤ×ℤ$
10 9 ndmov ${⊢}¬\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}..^{N}\right)=\varnothing$
11 7 10 nsyl5 ${⊢}¬{M}\in ℤ\to \left({M}..^{N}\right)=\varnothing$
12 simpl ${⊢}\left({M}\in ℤ\wedge {N}-1\in ℤ\right)\to {M}\in ℤ$
13 fzf ${⊢}\dots :ℤ×ℤ⟶𝒫ℤ$
14 13 fdmi ${⊢}\mathrm{dom}\dots =ℤ×ℤ$
15 14 ndmov ${⊢}¬\left({M}\in ℤ\wedge {N}-1\in ℤ\right)\to \left({M}\dots {N}-1\right)=\varnothing$
16 12 15 nsyl5 ${⊢}¬{M}\in ℤ\to \left({M}\dots {N}-1\right)=\varnothing$
17 11 16 eqtr4d ${⊢}¬{M}\in ℤ\to \left({M}..^{N}\right)=\left({M}\dots {N}-1\right)$
18 17 adantr ${⊢}\left(¬{M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}..^{N}\right)=\left({M}\dots {N}-1\right)$
19 6 18 pm2.61ian ${⊢}{N}\in ℤ\to \left({M}..^{N}\right)=\left({M}\dots {N}-1\right)$