Theorem fracge0

Description: The fractional part of a real number is nonnegative. (Contributed by NM, 17-Jul-2008)

	Ref	Expression
Assertion	fracge0	|- ( A e. RR -> 0 <_ ( A - ( |_ ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		flle	|- ( A e. RR -> ( |_ ` A ) <_ A )
2		reflcl	|- ( A e. RR -> ( |_ ` A ) e. RR )
3		subge0	|- ( ( A e. RR /\ ( |_ ` A ) e. RR ) -> ( 0 <_ ( A - ( |_ ` A ) ) <-> ( |_ ` A ) <_ A ) )
4	2 3	mpdan	|- ( A e. RR -> ( 0 <_ ( A - ( |_ ` A ) ) <-> ( |_ ` A ) <_ A ) )
5	1 4	mpbird	|- ( A e. RR -> 0 <_ ( A - ( |_ ` A ) ) )