Metamath Proof Explorer

Theorem fzval

Description: The value of a finite set of sequential integers. E.g., 2 ... 5 means the set { 2 , 3 , 4 , 5 } . A special case of this definition (starting at 1) appears as Definition 11-2.1 of Gleason p. 141, where NN_k means our 1 ... k ; he calls these setssegments of the integers. (Contributed by NM, 6-Sep-2005) (Revised by Mario Carneiro, 3-Nov-2013)

Ref Expression
Assertion fzval ⊢ M ∈ ℤ ∧ N ∈ ℤ → M … N = k ∈ ℤ | M ≤ k ∧ k ≤ N

Proof

Step Hyp Ref Expression
1 breq1 ⊢ m = M → m ≤ k ↔ M ≤ k
2 1 anbi1d ⊢ m = M → m ≤ k ∧ k ≤ n ↔ M ≤ k ∧ k ≤ n
3 2 rabbidv ⊢ m = M → k ∈ ℤ | m ≤ k ∧ k ≤ n = k ∈ ℤ | M ≤ k ∧ k ≤ n
4 breq2 ⊢ n = N → k ≤ n ↔ k ≤ N
5 4 anbi2d ⊢ n = N → M ≤ k ∧ k ≤ n ↔ M ≤ k ∧ k ≤ N
6 5 rabbidv ⊢ n = N → k ∈ ℤ | M ≤ k ∧ k ≤ n = k ∈ ℤ | M ≤ k ∧ k ≤ N
7 df-fz ⊢ … = m ∈ ℤ , n ∈ ℤ ⟼ k ∈ ℤ | m ≤ k ∧ k ≤ n
8 zex ⊢ ℤ ∈ V
9 8 rabex ⊢ k ∈ ℤ | M ≤ k ∧ k ≤ N ∈ V
10 3 6 7 9 ovmpo ⊢ M ∈ ℤ ∧ N ∈ ℤ → M … N = k ∈ ℤ | M ≤ k ∧ k ≤ N