Theorem halffl

Description: Floor of ( 1 / 2 ) . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	halffl	$$⊢⌊\frac{1}{2}⌋=0$$

Proof

Step	Hyp	Ref	Expression
1		0re	$$⊢0\in ℝ$$
2		halfre	$$⊢\frac{1}{2}\in ℝ$$
3		halfgt0	$$⊢0<\frac{1}{2}$$
4	1 2 3	ltleii	$$⊢0\le \frac{1}{2}$$
5		halflt1	$$⊢\frac{1}{2}<1$$
6		1e0p1	$$⊢1=0+1$$
7	5 6	breqtri	$$⊢\frac{1}{2}<0+1$$
8		0z	$$⊢0\in \mathbb{Z}$$
9		flbi	$$⊢\left(\frac{1}{2}\in ℝ\wedge 0\in \mathbb{Z}\right)\to \left(⌊\frac{1}{2}⌋=0\leftrightarrow \left(0\le \frac{1}{2}\wedge \frac{1}{2}<0+1\right)\right)$$
10	2 8 9	mp2an	$$⊢⌊\frac{1}{2}⌋=0\leftrightarrow \left(0\le \frac{1}{2}\wedge \frac{1}{2}<0+1\right)$$
11	4 7 10	mpbir2an	$$⊢⌊\frac{1}{2}⌋=0$$