Theorem flge

Description: The floor function value is the greatest integer less than or equal to its argument. (Contributed by NM, 15-Nov-2004) (Proof shortened by Fan Zheng, 14-Jul-2016)

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

Proof

Step	Hyp	Ref	Expression
1		flltp1	|- ( A e. RR -> A < ( ( |_ ` A ) + 1 ) )
2	1	adantr	|- ( ( A e. RR /\ B e. ZZ ) -> A < ( ( |_ ` A ) + 1 ) )
3		simpr	|- ( ( A e. RR /\ B e. ZZ ) -> B e. ZZ )
4	3	zred	|- ( ( A e. RR /\ B e. ZZ ) -> B e. RR )
5		simpl	|- ( ( A e. RR /\ B e. ZZ ) -> A e. RR )
6	5	flcld	|- ( ( A e. RR /\ B e. ZZ ) -> ( |_ ` A ) e. ZZ )
7	6	peano2zd	|- ( ( A e. RR /\ B e. ZZ ) -> ( ( |_ ` A ) + 1 ) e. ZZ )
8	7	zred	|- ( ( A e. RR /\ B e. ZZ ) -> ( ( |_ ` A ) + 1 ) e. RR )
9		lelttr	|- ( ( B e. RR /\ A e. RR /\ ( ( |_ ` A ) + 1 ) e. RR ) -> ( ( B <_ A /\ A < ( ( |_ ` A ) + 1 ) ) -> B < ( ( |_ ` A ) + 1 ) ) )
10	4 5 8 9	syl3anc	|- ( ( A e. RR /\ B e. ZZ ) -> ( ( B <_ A /\ A < ( ( |_ ` A ) + 1 ) ) -> B < ( ( |_ ` A ) + 1 ) ) )
11	2 10	mpan2d	|- ( ( A e. RR /\ B e. ZZ ) -> ( B <_ A -> B < ( ( |_ ` A ) + 1 ) ) )
12		zleltp1	|- ( ( B e. ZZ /\ ( |_ ` A ) e. ZZ ) -> ( B <_ ( |_ ` A ) <-> B < ( ( |_ ` A ) + 1 ) ) )
13	3 6 12	syl2anc	|- ( ( A e. RR /\ B e. ZZ ) -> ( B <_ ( |_ ` A ) <-> B < ( ( |_ ` A ) + 1 ) ) )
14	11 13	sylibrd	|- ( ( A e. RR /\ B e. ZZ ) -> ( B <_ A -> B <_ ( |_ ` A ) ) )
15		flle	|- ( A e. RR -> ( |_ ` A ) <_ A )
16	15	adantr	|- ( ( A e. RR /\ B e. ZZ ) -> ( |_ ` A ) <_ A )
17	6	zred	|- ( ( A e. RR /\ B e. ZZ ) -> ( |_ ` A ) e. RR )
18		letr	|- ( ( B e. RR /\ ( |_ ` A ) e. RR /\ A e. RR ) -> ( ( B <_ ( |_ ` A ) /\ ( |_ ` A ) <_ A ) -> B <_ A ) )
19	4 17 5 18	syl3anc	|- ( ( A e. RR /\ B e. ZZ ) -> ( ( B <_ ( |_ ` A ) /\ ( |_ ` A ) <_ A ) -> B <_ A ) )
20	16 19	mpan2d	|- ( ( A e. RR /\ B e. ZZ ) -> ( B <_ ( |_ ` A ) -> B <_ A ) )
21	14 20	impbid	|- ( ( A e. RR /\ B e. ZZ ) -> ( B <_ A <-> B <_ ( |_ ` A ) ) )