This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑁 ∈ ℤ → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 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 ) ) )