Description: Expressing a singleton as a half-open range. (Contributed by Stefan O'Rear, 23-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fzosn | ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ..^ ( 𝐴 + 1 ) ) = { 𝐴 } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fzval3 | ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ... 𝐴 ) = ( 𝐴 ..^ ( 𝐴 + 1 ) ) ) | |
2 | fzsn | ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ... 𝐴 ) = { 𝐴 } ) | |
3 | 1 2 | eqtr3d | ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ..^ ( 𝐴 + 1 ) ) = { 𝐴 } ) |