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 e. ( 2 [,) +oo ) -> 1 <_ ( X / 2 ) )

Proof

Step	Hyp	Ref	Expression
1		2cn	|- 2 e. CC
2	1	mullidi	|- ( 1 x. 2 ) = 2
3		2re	|- 2 e. RR
4	3	rexri	|- 2 e. RR*
5	4	a1i	|- ( X e. ( 2 [,) +oo ) -> 2 e. RR* )
6		pnfxr	|- +oo e. RR*
7	6	a1i	|- ( X e. ( 2 [,) +oo ) -> +oo e. RR* )
8		id	|- ( X e. ( 2 [,) +oo ) -> X e. ( 2 [,) +oo ) )
9	5 7 8	icogelbd	|- ( X e. ( 2 [,) +oo ) -> 2 <_ X )
10	2 9	eqbrtrid	|- ( X e. ( 2 [,) +oo ) -> ( 1 x. 2 ) <_ X )
11		1red	|- ( X e. ( 2 [,) +oo ) -> 1 e. RR )
12		0le2	|- 0 <_ 2
13		0xr	|- 0 e. RR*
14	13	a1i	|- ( 0 <_ 2 -> 0 e. RR* )
15	6	a1i	|- ( 0 <_ 2 -> +oo e. RR* )
16		id	|- ( 0 <_ 2 -> 0 <_ 2 )
17	14 15 16	icossico2d	|- ( 0 <_ 2 -> ( 2 [,) +oo ) C_ ( 0 [,) +oo ) )
18	12 17	ax-mp	|- ( 2 [,) +oo ) C_ ( 0 [,) +oo )
19		rge0ssre	|- ( 0 [,) +oo ) C_ RR
20	18 19	sstri	|- ( 2 [,) +oo ) C_ RR
21	20	sseli	|- ( X e. ( 2 [,) +oo ) -> X e. RR )
22		2rp	|- 2 e. RR+
23	22	a1i	|- ( X e. ( 2 [,) +oo ) -> 2 e. RR+ )
24	11 21 23	lemuldivd	|- ( X e. ( 2 [,) +oo ) -> ( ( 1 x. 2 ) <_ X <-> 1 <_ ( X / 2 ) ) )
25	10 24	mpbid	|- ( X e. ( 2 [,) +oo ) -> 1 <_ ( X / 2 ) )