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