Theorem gpg3kgrtriexlem3

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

	Ref	Expression
Hypothesis	gpg3kgrtriex.n	⊢ 𝑁 = ( 3 · 𝐾 )
Assertion	gpg3kgrtriexlem3	⊢ ( 𝐾 ∈ ℕ → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )

Proof

Step	Hyp	Ref	Expression
1		gpg3kgrtriex.n	⊢ 𝑁 = ( 3 · 𝐾 )
2		3z	⊢ 3 ∈ ℤ
3	2	a1i	⊢ ( 𝐾 ∈ ℕ → 3 ∈ ℤ )
4		nnz	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℤ )
5	3 4	zmulcld	⊢ ( 𝐾 ∈ ℕ → ( 3 · 𝐾 ) ∈ ℤ )
6		3t1e3	⊢ ( 3 · 1 ) = 3
7		nnge1	⊢ ( 𝐾 ∈ ℕ → 1 ≤ 𝐾 )
8		1re	⊢ 1 ∈ ℝ
9		nnre	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℝ )
10		3re	⊢ 3 ∈ ℝ
11		3pos	⊢ 0 < 3
12	10 11	pm3.2i	⊢ ( 3 ∈ ℝ ∧ 0 < 3 )
13	12	a1i	⊢ ( 𝐾 ∈ ℕ → ( 3 ∈ ℝ ∧ 0 < 3 ) )
14		lemul2	⊢ ( ( 1 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ ( 3 ∈ ℝ ∧ 0 < 3 ) ) → ( 1 ≤ 𝐾 ↔ ( 3 · 1 ) ≤ ( 3 · 𝐾 ) ) )
15	8 9 13 14	mp3an2i	⊢ ( 𝐾 ∈ ℕ → ( 1 ≤ 𝐾 ↔ ( 3 · 1 ) ≤ ( 3 · 𝐾 ) ) )
16	7 15	mpbid	⊢ ( 𝐾 ∈ ℕ → ( 3 · 1 ) ≤ ( 3 · 𝐾 ) )
17	6 16	eqbrtrrid	⊢ ( 𝐾 ∈ ℕ → 3 ≤ ( 3 · 𝐾 ) )
18		eluz2	⊢ ( ( 3 · 𝐾 ) ∈ ( ℤ≥ ‘ 3 ) ↔ ( 3 ∈ ℤ ∧ ( 3 · 𝐾 ) ∈ ℤ ∧ 3 ≤ ( 3 · 𝐾 ) ) )
19	3 5 17 18	syl3anbrc	⊢ ( 𝐾 ∈ ℕ → ( 3 · 𝐾 ) ∈ ( ℤ≥ ‘ 3 ) )
20	1 19	eqeltrid	⊢ ( 𝐾 ∈ ℕ → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )