Theorem rehalfge1

Description: Half of a real number greater than or equal to two is greater than or equal to one. (Contributed by AV, 2-Nov-2025)

	Ref	Expression
Assertion	rehalfge1	$$⊢X\in \left[2,\mathrm{+\infty }\right)\to 1\le \frac{X}{2}$$

Proof

Step	Hyp	Ref	Expression
1		2cn	$$⊢2\in ℂ$$
2	1	mullidi	$$⊢1\cdot 2=2$$
3		2re	$$⊢2\in ℝ$$
4	3	rexri	$$⊢2\in {ℝ}^{*}$$
5	4	a1i	$$⊢X\in \left[2,\mathrm{+\infty }\right)\to 2\in {ℝ}^{*}$$
6		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
7	6	a1i	$$⊢X\in \left[2,\mathrm{+\infty }\right)\to \mathrm{+\infty }\in {ℝ}^{*}$$
8		id	$$⊢X\in \left[2,\mathrm{+\infty }\right)\to X\in \left[2,\mathrm{+\infty }\right)$$
9	5 7 8	icogelbd	$$⊢X\in \left[2,\mathrm{+\infty }\right)\to 2\le X$$
10	2 9	eqbrtrid	$$⊢X\in \left[2,\mathrm{+\infty }\right)\to 1\cdot 2\le X$$
11		1red	$$⊢X\in \left[2,\mathrm{+\infty }\right)\to 1\in ℝ$$
12		0le2	$$⊢0\le 2$$
13		0xr	$$⊢0\in {ℝ}^{*}$$
14	13	a1i	$$⊢0\le 2\to 0\in {ℝ}^{*}$$
15	6	a1i	$$⊢0\le 2\to \mathrm{+\infty }\in {ℝ}^{*}$$
16		id	$$⊢0\le 2\to 0\le 2$$
17	14 15 16	icossico2d	$$⊢0\le 2\to \left[2,\mathrm{+\infty }\right)\subseteq \left[0,\mathrm{+\infty }\right)$$
18	12 17	ax-mp	$$⊢\left[2,\mathrm{+\infty }\right)\subseteq \left[0,\mathrm{+\infty }\right)$$
19		rge0ssre	$$⊢\left[0,\mathrm{+\infty }\right)\subseteq ℝ$$
20	18 19	sstri	$$⊢\left[2,\mathrm{+\infty }\right)\subseteq ℝ$$
21	20	sseli	$$⊢X\in \left[2,\mathrm{+\infty }\right)\to X\in ℝ$$
22		2rp	$$⊢2\in {ℝ}^{+}$$
23	22	a1i	$$⊢X\in \left[2,\mathrm{+\infty }\right)\to 2\in {ℝ}^{+}$$
24	11 21 23	lemuldivd	$$⊢X\in \left[2,\mathrm{+\infty }\right)\to \left(1\cdot 2\le X\leftrightarrow 1\le \frac{X}{2}\right)$$
25	10 24	mpbid	$$⊢X\in \left[2,\mathrm{+\infty }\right)\to 1\le \frac{X}{2}$$