Metamath Proof Explorer

Theorem ceilhalfelfzo1

Description: A positive integer less than (the ceiling of) half of another integer is in the half-open range of positive integers up to the other integer. (Contributed by AV, 7-Sep-2025)

		Ref	Expression
	Hypothesis	ceilhalfelfzo1.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
	Assertion	ceilhalfelfzo1	$⊢ N \in ℕ \to (K \in J \to K \in (1 ..^N))$

Proof

Step	Hyp	Ref	Expression
1		ceilhalfelfzo1.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
2	1	eleq2i	$⊢ K \in J \leftrightarrow K \in (1 ..^⌈\frac{N}{2}⌉)$
3		nnre	$⊢ N \in ℕ \to N \in ℝ$
4	3	rehalfcld	$⊢ N \in ℕ \to \frac{N}{2} \in ℝ$
5	4	ceilcld	$⊢ N \in ℕ \to ⌈\frac{N}{2}⌉ \in ℤ$
6		nnz	$⊢ N \in ℕ \to N \in ℤ$
7		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
8		2nn	$⊢ 2 \in ℕ$
9		nn0ledivnn	$⊢ (N \in ℕ_{0} \land 2 \in ℕ) \to \frac{N}{2} \leq N$
10	7 8 9	sylancl	$⊢ N \in ℕ \to \frac{N}{2} \leq N$
11		ceille	$⊢ (\frac{N}{2} \in ℝ \land N \in ℤ \land \frac{N}{2} \leq N) \to ⌈\frac{N}{2}⌉ \leq N$
12	4 6 10 11	syl3anc	$⊢ N \in ℕ \to ⌈\frac{N}{2}⌉ \leq N$
13		eluz2	$⊢ N \in ℤ_{\geq ⌈\frac{N}{2}⌉} \leftrightarrow (⌈\frac{N}{2}⌉ \in ℤ \land N \in ℤ \land ⌈\frac{N}{2}⌉ \leq N)$
14	5 6 12 13	syl3anbrc	$⊢ N \in ℕ \to N \in ℤ_{\geq ⌈\frac{N}{2}⌉}$
15		fzoss2	$⊢ N \in ℤ_{\geq ⌈\frac{N}{2}⌉} \to (1 ..^⌈\frac{N}{2}⌉) \subseteq (1 ..^N)$
16	14 15	syl	$⊢ N \in ℕ \to (1 ..^⌈\frac{N}{2}⌉) \subseteq (1 ..^N)$
17	16	sseld	$⊢ N \in ℕ \to (K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in (1 ..^N))$
18	2 17	biimtrid	$⊢ N \in ℕ \to (K \in J \to K \in (1 ..^N))$