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\in ℝ\to \left(0<A\leftrightarrow \frac{A}{2}<A\right)$$

Proof

Step	Hyp	Ref	Expression
1		halfpos2	$$⊢A\in ℝ\to \left(0<A\leftrightarrow 0<\frac{A}{2}\right)$$
2		rehalfcl	$$⊢A\in ℝ\to \frac{A}{2}\in ℝ$$
3	2 2	ltaddposd	$$⊢A\in ℝ\to \left(0<\frac{A}{2}\leftrightarrow \frac{A}{2}<\left(\frac{A}{2}\right)+\left(\frac{A}{2}\right)\right)$$
4		recn	$$⊢A\in ℝ\to A\in ℂ$$
5		2halves	$$⊢A\in ℂ\to \left(\frac{A}{2}\right)+\left(\frac{A}{2}\right)=A$$
6	4 5	syl	$$⊢A\in ℝ\to \left(\frac{A}{2}\right)+\left(\frac{A}{2}\right)=A$$
7	6	breq2d	$$⊢A\in ℝ\to \left(\frac{A}{2}<\left(\frac{A}{2}\right)+\left(\frac{A}{2}\right)\leftrightarrow \frac{A}{2}<A\right)$$
8	1 3 7	3bitrd	$$⊢A\in ℝ\to \left(0<A\leftrightarrow \frac{A}{2}<A\right)$$