Theorem gpg3kgrtriexlem1

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

	Ref	Expression
Assertion	gpg3kgrtriexlem1	⊢ ( 𝐾 ∈ ℕ → 𝐾 < ( ⌈ ‘ ( ( 3 · 𝐾 ) / 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nnre	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℝ )
2		3re	⊢ 3 ∈ ℝ
3	2	a1i	⊢ ( 𝐾 ∈ ℕ → 3 ∈ ℝ )
4	3 1	remulcld	⊢ ( 𝐾 ∈ ℕ → ( 3 · 𝐾 ) ∈ ℝ )
5	4	rehalfcld	⊢ ( 𝐾 ∈ ℕ → ( ( 3 · 𝐾 ) / 2 ) ∈ ℝ )
6	5	ceilcld	⊢ ( 𝐾 ∈ ℕ → ( ⌈ ‘ ( ( 3 · 𝐾 ) / 2 ) ) ∈ ℤ )
7	6	zred	⊢ ( 𝐾 ∈ ℕ → ( ⌈ ‘ ( ( 3 · 𝐾 ) / 2 ) ) ∈ ℝ )
8		2re	⊢ 2 ∈ ℝ
9	8	a1i	⊢ ( 𝐾 ∈ ℕ → 2 ∈ ℝ )
10		nnrp	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℝ+ )
11		2lt3	⊢ 2 < 3
12	11	a1i	⊢ ( 𝐾 ∈ ℕ → 2 < 3 )
13	9 3 10 12	ltmul1dd	⊢ ( 𝐾 ∈ ℕ → ( 2 · 𝐾 ) < ( 3 · 𝐾 ) )
14		2pos	⊢ 0 < 2
15	14	a1i	⊢ ( 𝐾 ∈ ℕ → 0 < 2 )
16		ltmuldiv2	⊢ ( ( 𝐾 ∈ ℝ ∧ ( 3 · 𝐾 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · 𝐾 ) < ( 3 · 𝐾 ) ↔ 𝐾 < ( ( 3 · 𝐾 ) / 2 ) ) )
17	1 4 9 15 16	syl112anc	⊢ ( 𝐾 ∈ ℕ → ( ( 2 · 𝐾 ) < ( 3 · 𝐾 ) ↔ 𝐾 < ( ( 3 · 𝐾 ) / 2 ) ) )
18	13 17	mpbid	⊢ ( 𝐾 ∈ ℕ → 𝐾 < ( ( 3 · 𝐾 ) / 2 ) )
19	5	ceilged	⊢ ( 𝐾 ∈ ℕ → ( ( 3 · 𝐾 ) / 2 ) ≤ ( ⌈ ‘ ( ( 3 · 𝐾 ) / 2 ) ) )
20	1 5 7 18 19	ltletrd	⊢ ( 𝐾 ∈ ℕ → 𝐾 < ( ⌈ ‘ ( ( 3 · 𝐾 ) / 2 ) ) )