Theorem ceilidz

Description: A real number equals its ceiling iff it is an integer. (Contributed by AV, 30-Nov-2018)

	Ref	Expression
Assertion	ceilidz	$$⊢A\in ℝ\to \left(A\in \mathbb{Z}\leftrightarrow ⌈A⌉=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ceilid	$$⊢A\in \mathbb{Z}\to ⌈A⌉=A$$
2		ceilcl	$$⊢A\in ℝ\to ⌈A⌉\in \mathbb{Z}$$
3		eleq1	$$⊢⌈A⌉=A\to \left(⌈A⌉\in \mathbb{Z}\leftrightarrow A\in \mathbb{Z}\right)$$
4	2 3	syl5ibcom	$$⊢A\in ℝ\to \left(⌈A⌉=A\to A\in \mathbb{Z}\right)$$
5	1 4	impbid2	$$⊢A\in ℝ\to \left(A\in \mathbb{Z}\leftrightarrow ⌈A⌉=A\right)$$