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	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{N}{2}\le N-1$$

Proof

Step	Hyp	Ref	Expression
1		2re	$$⊢2\in ℝ$$
2	1	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\in ℝ$$
3		eluzelre	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in ℝ$$
4	2 3	remulcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
5		eluzle	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\le N$$
6		2m1e1	$$⊢2-1=1$$
7	6	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2-1=1$$
8	7	oveq1d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(2-1\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
9		eluzelcn	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in ℂ$$
10	9	mullidd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N$$
11	8 10	eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(2-1\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N$$
12	5 11	breqtrrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\le \left(2-1\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
13		2cnd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\in ℂ$$
14	13 9	mulsubfacd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-N=\left(2-1\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
15	12 14	breqtrrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-N$$
16	2 4 3 15	lesubd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-2$$
17	13 9	muls1d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\left(N-1\right)=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-2$$
18	16 17	breqtrrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\le 2\left(N-1\right)$$
19		1red	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1\in ℝ$$
20	3 19	resubcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-1\in ℝ$$
21		2rp	$$⊢2\in {ℝ}^{+}$$
22	21	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\in {ℝ}^{+}$$
23	3 20 22	ledivmuld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(\frac{N}{2}\le N-1\leftrightarrow N\le 2\left(N-1\right)\right)$$
24	18 23	mpbird	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{N}{2}\le N-1$$