Theorem rphalflt

Description: Half of a positive real is less than the original number. (Contributed by Mario Carneiro, 21-May-2014)

	Ref	Expression
Assertion	rphalflt	⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 / 2 ) < 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elrp	⊢ ( 𝐴 ∈ ℝ+ ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
2		halfpos	⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 ↔ ( 𝐴 / 2 ) < 𝐴 ) )
3	2	biimpa	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 𝐴 / 2 ) < 𝐴 )
4	1 3	sylbi	⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 / 2 ) < 𝐴 )