Metamath Proof Explorer

Theorem gpg3kgrtriexlem1

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

Ref Expression
Assertion gpg3kgrtriexlem1 ⊢ K ∈ ℕ → K < 3 ⁢ K 2

Proof

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