Theorem ge2halflem1

Description: Half of an integer greater than 1 is less than or equal to the integer minus 1. (Contributed by AV, 1-Sep-2025)

	Ref	Expression
Assertion	ge2halflem1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 / 2 ) ≤ ( 𝑁 − 1 ) )

Proof

Step	Hyp	Ref	Expression
1		2re	⊢ 2 ∈ ℝ
2	1	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℝ )
3		eluzelre	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℝ )
4	2 3	remulcld	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · 𝑁 ) ∈ ℝ )
5		eluzle	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ 𝑁 )
6		2m1e1	⊢ ( 2 − 1 ) = 1
7	6	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 − 1 ) = 1 )
8	7	oveq1d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 − 1 ) · 𝑁 ) = ( 1 · 𝑁 ) )
9		eluzelcn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℂ )
10	9	mullidd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 1 · 𝑁 ) = 𝑁 )
11	8 10	eqtrd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 − 1 ) · 𝑁 ) = 𝑁 )
12	5 11	breqtrrd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ ( ( 2 − 1 ) · 𝑁 ) )
13		2cnd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℂ )
14	13 9	mulsubfacd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 · 𝑁 ) − 𝑁 ) = ( ( 2 − 1 ) · 𝑁 ) )
15	12 14	breqtrrd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ ( ( 2 · 𝑁 ) − 𝑁 ) )
16	2 4 3 15	lesubd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ≤ ( ( 2 · 𝑁 ) − 2 ) )
17	13 9	muls1d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( 𝑁 − 1 ) ) = ( ( 2 · 𝑁 ) − 2 ) )
18	16 17	breqtrrd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ≤ ( 2 · ( 𝑁 − 1 ) ) )
19		1red	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ℝ )
20	3 19	resubcld	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 1 ) ∈ ℝ )
21		2rp	⊢ 2 ∈ ℝ+
22	21	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℝ+ )
23	3 20 22	ledivmuld	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 / 2 ) ≤ ( 𝑁 − 1 ) ↔ 𝑁 ≤ ( 2 · ( 𝑁 − 1 ) ) ) )
24	18 23	mpbird	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 / 2 ) ≤ ( 𝑁 − 1 ) )