Description: Half of a positive real is less than the original number. (Contributed by Mario Carneiro, 21-May-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | rphalflt | |- ( A e. RR+ -> ( A / 2 ) < A ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrp | |- ( A e. RR+ <-> ( A e. RR /\ 0 < A ) ) |
|
2 | halfpos | |- ( A e. RR -> ( 0 < A <-> ( A / 2 ) < A ) ) |
|
3 | 2 | biimpa | |- ( ( A e. RR /\ 0 < A ) -> ( A / 2 ) < A ) |
4 | 1 3 | sylbi | |- ( A e. RR+ -> ( A / 2 ) < A ) |