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 ∈ ℤ → M ..^ N = M … N − 1

Proof

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