Theorem flge0nn0

Description: The floor of a number greater than or equal to 0 is a nonnegative integer. (Contributed by NM, 26-Apr-2005)

	Ref	Expression
Assertion	flge0nn0	|- ( ( A e. RR /\ 0 <_ A ) -> ( |_ ` A ) e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		flcl	|- ( A e. RR -> ( |_ ` A ) e. ZZ )
2	1	adantr	|- ( ( A e. RR /\ 0 <_ A ) -> ( |_ ` A ) e. ZZ )
3		0z	|- 0 e. ZZ
4		flge	|- ( ( A e. RR /\ 0 e. ZZ ) -> ( 0 <_ A <-> 0 <_ ( |_ ` A ) ) )
5	3 4	mpan2	|- ( A e. RR -> ( 0 <_ A <-> 0 <_ ( |_ ` A ) ) )
6	5	biimpa	|- ( ( A e. RR /\ 0 <_ A ) -> 0 <_ ( |_ ` A ) )
7		elnn0z	|- ( ( |_ ` A ) e. NN0 <-> ( ( |_ ` A ) e. ZZ /\ 0 <_ ( |_ ` A ) ) )
8	2 6 7	sylanbrc	|- ( ( A e. RR /\ 0 <_ A ) -> ( |_ ` A ) e. NN0 )