Theorem rphalfltd

Description: Half of a positive real is less than the original number. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypothesis	rphalfltd.1	$$⊢\phi \to A\in {ℝ}^{+}$$
Assertion	rphalfltd	$$⊢\phi \to \frac{A}{2}<A$$

Proof

Step	Hyp	Ref	Expression
1		rphalfltd.1	$$⊢\phi \to A\in {ℝ}^{+}$$
2		rphalflt	$$⊢A\in {ℝ}^{+}\to \frac{A}{2}<A$$
3	1 2	syl	$$⊢\phi \to \frac{A}{2}<A$$