Metamath Proof Explorer


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 ) ) )