This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem halfpos

Description: A positive number is greater than its half. (Contributed by NM, 28-Oct-2004) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion halfpos 
|- ( A e. RR -> ( 0 < A <-> ( A / 2 ) < A ) )

Proof

Step Hyp Ref Expression
1 halfpos2 
 |-  ( A e. RR -> ( 0 < A <-> 0 < ( A / 2 ) ) )
2 rehalfcl 
 |-  ( A e. RR -> ( A / 2 ) e. RR )
3 2 2 ltaddposd 
 |-  ( A e. RR -> ( 0 < ( A / 2 ) <-> ( A / 2 ) < ( ( A / 2 ) + ( A / 2 ) ) ) )
4 recn 
 |-  ( A e. RR -> A e. CC )
5 2halves 
 |-  ( A e. CC -> ( ( A / 2 ) + ( A / 2 ) ) = A )
6 4 5 syl 
 |-  ( A e. RR -> ( ( A / 2 ) + ( A / 2 ) ) = A )
7 6 breq2d 
 |-  ( A e. RR -> ( ( A / 2 ) < ( ( A / 2 ) + ( A / 2 ) ) <-> ( A / 2 ) < A ) )
8 1 3 7 3bitrd 
 |-  ( A e. RR -> ( 0 < A <-> ( A / 2 ) < A ) )