Theorem flid

Description: An integer is its own floor. (Contributed by NM, 15-Nov-2004)

	Ref	Expression
Assertion	flid	$$⊢A\in \mathbb{Z}\to ⌊A⌋=A$$

Proof

Step	Hyp	Ref	Expression
1		zre	$$⊢A\in \mathbb{Z}\to A\in ℝ$$
2		flle	$$⊢A\in ℝ\to ⌊A⌋\le A$$
3	1 2	syl	$$⊢A\in \mathbb{Z}\to ⌊A⌋\le A$$
4	1	leidd	$$⊢A\in \mathbb{Z}\to A\le A$$
5		flge	$$⊢\left(A\in ℝ\wedge A\in \mathbb{Z}\right)\to \left(A\le A\leftrightarrow A\le ⌊A⌋\right)$$
6	1 5	mpancom	$$⊢A\in \mathbb{Z}\to \left(A\le A\leftrightarrow A\le ⌊A⌋\right)$$
7	4 6	mpbid	$$⊢A\in \mathbb{Z}\to A\le ⌊A⌋$$
8		reflcl	$$⊢A\in ℝ\to ⌊A⌋\in ℝ$$
9	1 8	syl	$$⊢A\in \mathbb{Z}\to ⌊A⌋\in ℝ$$
10	9 1	letri3d	$$⊢A\in \mathbb{Z}\to \left(⌊A⌋=A\leftrightarrow \left(⌊A⌋\le A\wedge A\le ⌊A⌋\right)\right)$$
11	3 7 10	mpbir2and	$$⊢A\in \mathbb{Z}\to ⌊A⌋=A$$