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