Theorem fzosn

Description: Expressing a singleton as a half-open range. (Contributed by Stefan O'Rear, 23-Aug-2015)

	Ref	Expression
Assertion	fzosn	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ..^ ( 𝐴 + 1 ) ) = { 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		fzval3	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ... 𝐴 ) = ( 𝐴 ..^ ( 𝐴 + 1 ) ) )
2		fzsn	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ... 𝐴 ) = { 𝐴 } )
3	1 2	eqtr3d	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ..^ ( 𝐴 + 1 ) ) = { 𝐴 } )