Metamath Proof Explorer

Theorem gpg3kgrtriexlem4

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

Ref Expression
Hypothesis gpg3kgrtriex.n ⊢ N = 3 ⁢ K
Assertion gpg3kgrtriexlem4 ⊢ K ∈ ℕ → K ∈ 1 ..^ N 2

Proof

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