Theorem fllt

Description: The floor function value is less than the next integer. (Contributed by NM, 24-Feb-2005)

	Ref	Expression
Assertion	fllt	|- ( ( A e. RR /\ B e. ZZ ) -> ( A < B <-> ( |_ ` A ) < B ) )

Proof

Step	Hyp	Ref	Expression
1		flge	|- ( ( A e. RR /\ B e. ZZ ) -> ( B <_ A <-> B <_ ( |_ ` A ) ) )
2		zre	|- ( B e. ZZ -> B e. RR )
3		lenlt	|- ( ( B e. RR /\ A e. RR ) -> ( B <_ A <-> -. A < B ) )
4	2 3	sylan	|- ( ( B e. ZZ /\ A e. RR ) -> ( B <_ A <-> -. A < B ) )
5	4	ancoms	|- ( ( A e. RR /\ B e. ZZ ) -> ( B <_ A <-> -. A < B ) )
6		reflcl	|- ( A e. RR -> ( |_ ` A ) e. RR )
7		lenlt	|- ( ( B e. RR /\ ( |_ ` A ) e. RR ) -> ( B <_ ( |_ ` A ) <-> -. ( |_ ` A ) < B ) )
8	2 6 7	syl2anr	|- ( ( A e. RR /\ B e. ZZ ) -> ( B <_ ( |_ ` A ) <-> -. ( |_ ` A ) < B ) )
9	1 5 8	3bitr3d	|- ( ( A e. RR /\ B e. ZZ ) -> ( -. A < B <-> -. ( |_ ` A ) < B ) )
10	9	con4bid	|- ( ( A e. RR /\ B e. ZZ ) -> ( A < B <-> ( |_ ` A ) < B ) )