Theorem flge1nn

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

	Ref	Expression
Assertion	flge1nn	|- ( ( A e. RR /\ 1 <_ A ) -> ( |_ ` A ) e. NN )

Proof

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