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	⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 ↔ ( 𝐴 / 2 ) < 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		halfpos2	⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 ↔ 0 < ( 𝐴 / 2 ) ) )
2		rehalfcl	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 / 2 ) ∈ ℝ )
3	2 2	ltaddposd	⊢ ( 𝐴 ∈ ℝ → ( 0 < ( 𝐴 / 2 ) ↔ ( 𝐴 / 2 ) < ( ( 𝐴 / 2 ) + ( 𝐴 / 2 ) ) ) )
4		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
5		2halves	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 / 2 ) + ( 𝐴 / 2 ) ) = 𝐴 )
6	4 5	syl	⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 / 2 ) + ( 𝐴 / 2 ) ) = 𝐴 )
7	6	breq2d	⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 / 2 ) < ( ( 𝐴 / 2 ) + ( 𝐴 / 2 ) ) ↔ ( 𝐴 / 2 ) < 𝐴 ) )
8	1 3 7	3bitrd	⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 ↔ ( 𝐴 / 2 ) < 𝐴 ) )