Theorem ceilid

Description: An integer is its own ceiling. (Contributed by AV, 30-Nov-2018)

	Ref	Expression
Assertion	ceilid	$$⊢A\in \mathbb{Z}\to ⌈A⌉=A$$

Proof

Step	Hyp	Ref	Expression
1		zre	$$⊢A\in \mathbb{Z}\to A\in ℝ$$
2		ceilval	$$⊢A\in ℝ\to ⌈A⌉=-⌊-A⌋$$
3	1 2	syl	$$⊢A\in \mathbb{Z}\to ⌈A⌉=-⌊-A⌋$$
4		znegcl	$$⊢A\in \mathbb{Z}\to -A\in \mathbb{Z}$$
5		flid	$$⊢-A\in \mathbb{Z}\to ⌊-A⌋=-A$$
6	4 5	syl	$$⊢A\in \mathbb{Z}\to ⌊-A⌋=-A$$
7	6	negeqd	$$⊢A\in \mathbb{Z}\to -⌊-A⌋=-\left(-A\right)$$
8		zcn	$$⊢A\in \mathbb{Z}\to A\in ℂ$$
9	8	negnegd	$$⊢A\in \mathbb{Z}\to -\left(-A\right)=A$$
10	3 7 9	3eqtrd	$$⊢A\in \mathbb{Z}\to ⌈A⌉=A$$