Theorem flltnz

Description: The floor of a non-integer real is less than it. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	flltnz	$$⊢\left(A\in ℝ\wedge \neg A\in \mathbb{Z}\right)\to ⌊A⌋<A$$

Proof

Step	Hyp	Ref	Expression
1		reflcl	$$⊢A\in ℝ\to ⌊A⌋\in ℝ$$
2	1	adantr	$$⊢\left(A\in ℝ\wedge \neg A\in \mathbb{Z}\right)\to ⌊A⌋\in ℝ$$
3		simpl	$$⊢\left(A\in ℝ\wedge \neg A\in \mathbb{Z}\right)\to A\in ℝ$$
4		fllelt	$$⊢A\in ℝ\to \left(⌊A⌋\le A\wedge A<⌊A⌋+1\right)$$
5	4	adantr	$$⊢\left(A\in ℝ\wedge \neg A\in \mathbb{Z}\right)\to \left(⌊A⌋\le A\wedge A<⌊A⌋+1\right)$$
6	5	simpld	$$⊢\left(A\in ℝ\wedge \neg A\in \mathbb{Z}\right)\to ⌊A⌋\le A$$
7		simpr	$$⊢\left(A\in ℝ\wedge \neg A\in \mathbb{Z}\right)\to \neg A\in \mathbb{Z}$$
8		flidz	$$⊢A\in ℝ\to \left(⌊A⌋=A\leftrightarrow A\in \mathbb{Z}\right)$$
9	8	adantr	$$⊢\left(A\in ℝ\wedge \neg A\in \mathbb{Z}\right)\to \left(⌊A⌋=A\leftrightarrow A\in \mathbb{Z}\right)$$
10	7 9	mtbird	$$⊢\left(A\in ℝ\wedge \neg A\in \mathbb{Z}\right)\to \neg ⌊A⌋=A$$
11	10	neqned	$$⊢\left(A\in ℝ\wedge \neg A\in \mathbb{Z}\right)\to ⌊A⌋\ne A$$
12	11	necomd	$$⊢\left(A\in ℝ\wedge \neg A\in \mathbb{Z}\right)\to A\ne ⌊A⌋$$
13	2 3 6 12	leneltd	$$⊢\left(A\in ℝ\wedge \neg A\in \mathbb{Z}\right)\to ⌊A⌋<A$$