Theorem gpg3kgrtriexlem4

Description: Lemma 4 for gpg3kgrtriex . (Contributed by AV, 1-Oct-2025)

	Ref	Expression
Hypothesis	gpg3kgrtriex.n	⊢ 𝑁 = ( 3 · 𝐾 )
Assertion	gpg3kgrtriexlem4	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gpg3kgrtriex.n	⊢ 𝑁 = ( 3 · 𝐾 )
2		id	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℕ )
3	1	oveq1i	⊢ ( 𝑁 / 2 ) = ( ( 3 · 𝐾 ) / 2 )
4		3re	⊢ 3 ∈ ℝ
5	4	a1i	⊢ ( 𝐾 ∈ ℕ → 3 ∈ ℝ )
6		nnre	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℝ )
7	5 6	remulcld	⊢ ( 𝐾 ∈ ℕ → ( 3 · 𝐾 ) ∈ ℝ )
8	7	rehalfcld	⊢ ( 𝐾 ∈ ℕ → ( ( 3 · 𝐾 ) / 2 ) ∈ ℝ )
9	3 8	eqeltrid	⊢ ( 𝐾 ∈ ℕ → ( 𝑁 / 2 ) ∈ ℝ )
10	9	ceilcld	⊢ ( 𝐾 ∈ ℕ → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
11		1red	⊢ ( 𝐾 ∈ ℕ → 1 ∈ ℝ )
12	1 7	eqeltrid	⊢ ( 𝐾 ∈ ℕ → 𝑁 ∈ ℝ )
13	12	rehalfcld	⊢ ( 𝐾 ∈ ℕ → ( 𝑁 / 2 ) ∈ ℝ )
14	13	ceilcld	⊢ ( 𝐾 ∈ ℕ → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
15	14	zred	⊢ ( 𝐾 ∈ ℕ → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℝ )
16		nnge1	⊢ ( 𝐾 ∈ ℕ → 1 ≤ 𝐾 )
17	8	ceilcld	⊢ ( 𝐾 ∈ ℕ → ( ⌈ ‘ ( ( 3 · 𝐾 ) / 2 ) ) ∈ ℤ )
18	17	zred	⊢ ( 𝐾 ∈ ℕ → ( ⌈ ‘ ( ( 3 · 𝐾 ) / 2 ) ) ∈ ℝ )
19		gpg3kgrtriexlem1	⊢ ( 𝐾 ∈ ℕ → 𝐾 < ( ⌈ ‘ ( ( 3 · 𝐾 ) / 2 ) ) )
20	6 18 19	ltled	⊢ ( 𝐾 ∈ ℕ → 𝐾 ≤ ( ⌈ ‘ ( ( 3 · 𝐾 ) / 2 ) ) )
21	3	fveq2i	⊢ ( ⌈ ‘ ( 𝑁 / 2 ) ) = ( ⌈ ‘ ( ( 3 · 𝐾 ) / 2 ) )
22	20 21	breqtrrdi	⊢ ( 𝐾 ∈ ℕ → 𝐾 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
23	11 6 15 16 22	letrd	⊢ ( 𝐾 ∈ ℕ → 1 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
24		elnnz1	⊢ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ↔ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ ∧ 1 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
25	10 23 24	sylanbrc	⊢ ( 𝐾 ∈ ℕ → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ )
26	19 21	breqtrrdi	⊢ ( 𝐾 ∈ ℕ → 𝐾 < ( ⌈ ‘ ( 𝑁 / 2 ) ) )
27		elfzo1	⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ↔ ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝐾 < ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
28	2 25 26 27	syl3anbrc	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )