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	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
Assertion	ceilhalfelfzo1	⊢ ( 𝑁 ∈ ℕ → ( 𝐾 ∈ 𝐽 → 𝐾 ∈ ( 1 ..^ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ceilhalfelfzo1.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
2	1	eleq2i	⊢ ( 𝐾 ∈ 𝐽 ↔ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
3		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
4	3	rehalfcld	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 / 2 ) ∈ ℝ )
5	4	ceilcld	⊢ ( 𝑁 ∈ ℕ → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
6		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
7		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
8		2nn	⊢ 2 ∈ ℕ
9		nn0ledivnn	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ∈ ℕ ) → ( 𝑁 / 2 ) ≤ 𝑁 )
10	7 8 9	sylancl	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 / 2 ) ≤ 𝑁 )
11		ceille	⊢ ( ( ( 𝑁 / 2 ) ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 / 2 ) ≤ 𝑁 ) → ( ⌈ ‘ ( 𝑁 / 2 ) ) ≤ 𝑁 )
12	4 6 10 11	syl3anc	⊢ ( 𝑁 ∈ ℕ → ( ⌈ ‘ ( 𝑁 / 2 ) ) ≤ 𝑁 )
13		eluz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ↔ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ≤ 𝑁 ) )
14	5 6 12 13	syl3anbrc	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ℤ≥ ‘ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
15		fzoss2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ⊆ ( 1 ..^ 𝑁 ) )
16	14 15	syl	⊢ ( 𝑁 ∈ ℕ → ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ⊆ ( 1 ..^ 𝑁 ) )
17	16	sseld	⊢ ( 𝑁 ∈ ℕ → ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ∈ ( 1 ..^ 𝑁 ) ) )
18	2 17	biimtrid	⊢ ( 𝑁 ∈ ℕ → ( 𝐾 ∈ 𝐽 → 𝐾 ∈ ( 1 ..^ 𝑁 ) ) )