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	|- ( ( A e. RR /\ -. A e. ZZ ) -> ( |_ ` A ) < A )

Proof

Step	Hyp	Ref	Expression
1		reflcl	|- ( A e. RR -> ( |_ ` A ) e. RR )
2	1	adantr	|- ( ( A e. RR /\ -. A e. ZZ ) -> ( |_ ` A ) e. RR )
3		simpl	|- ( ( A e. RR /\ -. A e. ZZ ) -> A e. RR )
4		fllelt	|- ( A e. RR -> ( ( |_ ` A ) <_ A /\ A < ( ( |_ ` A ) + 1 ) ) )
5	4	adantr	|- ( ( A e. RR /\ -. A e. ZZ ) -> ( ( |_ ` A ) <_ A /\ A < ( ( |_ ` A ) + 1 ) ) )
6	5	simpld	|- ( ( A e. RR /\ -. A e. ZZ ) -> ( |_ ` A ) <_ A )
7		simpr	|- ( ( A e. RR /\ -. A e. ZZ ) -> -. A e. ZZ )
8		flidz	|- ( A e. RR -> ( ( |_ ` A ) = A <-> A e. ZZ ) )
9	8	adantr	|- ( ( A e. RR /\ -. A e. ZZ ) -> ( ( |_ ` A ) = A <-> A e. ZZ ) )
10	7 9	mtbird	|- ( ( A e. RR /\ -. A e. ZZ ) -> -. ( |_ ` A ) = A )
11	10	neqned	|- ( ( A e. RR /\ -. A e. ZZ ) -> ( |_ ` A ) =/= A )
12	11	necomd	|- ( ( A e. RR /\ -. A e. ZZ ) -> A =/= ( |_ ` A ) )
13	2 3 6 12	leneltd	|- ( ( A e. RR /\ -. A e. ZZ ) -> ( |_ ` A ) < A )