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	⊢ ( 𝑋 ∈ ( 2 [,) +∞ ) → 1 ≤ ( 𝑋 / 2 ) )

Proof

Step	Hyp	Ref	Expression
1		2cn	⊢ 2 ∈ ℂ
2	1	mullidi	⊢ ( 1 · 2 ) = 2
3		2re	⊢ 2 ∈ ℝ
4	3	rexri	⊢ 2 ∈ ℝ*
5	4	a1i	⊢ ( 𝑋 ∈ ( 2 [,) +∞ ) → 2 ∈ ℝ* )
6		pnfxr	⊢ +∞ ∈ ℝ*
7	6	a1i	⊢ ( 𝑋 ∈ ( 2 [,) +∞ ) → +∞ ∈ ℝ* )
8		id	⊢ ( 𝑋 ∈ ( 2 [,) +∞ ) → 𝑋 ∈ ( 2 [,) +∞ ) )
9	5 7 8	icogelbd	⊢ ( 𝑋 ∈ ( 2 [,) +∞ ) → 2 ≤ 𝑋 )
10	2 9	eqbrtrid	⊢ ( 𝑋 ∈ ( 2 [,) +∞ ) → ( 1 · 2 ) ≤ 𝑋 )
11		1red	⊢ ( 𝑋 ∈ ( 2 [,) +∞ ) → 1 ∈ ℝ )
12		0le2	⊢ 0 ≤ 2
13		0xr	⊢ 0 ∈ ℝ*
14	13	a1i	⊢ ( 0 ≤ 2 → 0 ∈ ℝ* )
15	6	a1i	⊢ ( 0 ≤ 2 → +∞ ∈ ℝ* )
16		id	⊢ ( 0 ≤ 2 → 0 ≤ 2 )
17	14 15 16	icossico2d	⊢ ( 0 ≤ 2 → ( 2 [,) +∞ ) ⊆ ( 0 [,) +∞ ) )
18	12 17	ax-mp	⊢ ( 2 [,) +∞ ) ⊆ ( 0 [,) +∞ )
19		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
20	18 19	sstri	⊢ ( 2 [,) +∞ ) ⊆ ℝ
21	20	sseli	⊢ ( 𝑋 ∈ ( 2 [,) +∞ ) → 𝑋 ∈ ℝ )
22		2rp	⊢ 2 ∈ ℝ+
23	22	a1i	⊢ ( 𝑋 ∈ ( 2 [,) +∞ ) → 2 ∈ ℝ+ )
24	11 21 23	lemuldivd	⊢ ( 𝑋 ∈ ( 2 [,) +∞ ) → ( ( 1 · 2 ) ≤ 𝑋 ↔ 1 ≤ ( 𝑋 / 2 ) ) )
25	10 24	mpbid	⊢ ( 𝑋 ∈ ( 2 [,) +∞ ) → 1 ≤ ( 𝑋 / 2 ) )