gpg3kgrtriexlem3

		Ref	Expression
	Hypothesis	gpg3kgrtriex.n	$⊢ N = 3 K$
	Assertion	gpg3kgrtriexlem3	$⊢ K \in ℕ \to N \in ℤ_{\geq 3}$

Step	Hyp	Ref	Expression
1		gpg3kgrtriex.n	$⊢ N = 3 K$
2		3z	$⊢ 3 \in ℤ$
3	2	a1i	$⊢ K \in ℕ \to 3 \in ℤ$
4		nnz	$⊢ K \in ℕ \to K \in ℤ$
5	3 4	zmulcld	$⊢ K \in ℕ \to 3 K \in ℤ$
6		3t1e3	$⊢ 3 \cdot 1 = 3$
7		nnge1	$⊢ K \in ℕ \to 1 \leq K$
8		1re	$⊢ 1 \in ℝ$
9		nnre	$⊢ K \in ℕ \to K \in ℝ$
10		3re	$⊢ 3 \in ℝ$
11		3pos	$⊢ 0 < 3$
12	10 11	pm3.2i	$⊢ (3 \in ℝ \land 0 < 3)$
13	12	a1i	$⊢ K \in ℕ \to (3 \in ℝ \land 0 < 3)$
14		lemul2	$⊢ (1 \in ℝ \land K \in ℝ \land (3 \in ℝ \land 0 < 3)) \to (1 \leq K \leftrightarrow 3 \cdot 1 \leq 3 K)$
15	8 9 13 14	mp3an2i	$⊢ K \in ℕ \to (1 \leq K \leftrightarrow 3 \cdot 1 \leq 3 K)$
16	7 15	mpbid	$⊢ K \in ℕ \to 3 \cdot 1 \leq 3 K$
17	6 16	eqbrtrrid	$⊢ K \in ℕ \to 3 \leq 3 K$
18		eluz2	$⊢ 3 K \in ℤ_{\geq 3} \leftrightarrow (3 \in ℤ \land 3 K \in ℤ \land 3 \leq 3 K)$
19	3 5 17 18	syl3anbrc	$⊢ K \in ℕ \to 3 K \in ℤ_{\geq 3}$
20	1 19	eqeltrid	$⊢ K \in ℕ \to N \in ℤ_{\geq 3}$

Metamath Proof Explorer