eluz2b2

Description: Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012)

		Ref	Expression
	Assertion	eluz2b2	$⊢ N \in ℤ_{\geq 2} \leftrightarrow (N \in ℕ \land 1 < N)$

Step	Hyp	Ref	Expression
1		eluz2b1	$⊢ N \in ℤ_{\geq 2} \leftrightarrow (N \in ℤ \land 1 < N)$
2		1re	$⊢ 1 \in ℝ$
3		zre	$⊢ N \in ℤ \to N \in ℝ$
4		ltle	$⊢ (1 \in ℝ \land N \in ℝ) \to (1 < N \to 1 \leq N)$
5	2 3 4	sylancr	$⊢ N \in ℤ \to (1 < N \to 1 \leq N)$
6	5	imdistani	$⊢ (N \in ℤ \land 1 < N) \to (N \in ℤ \land 1 \leq N)$
7		elnnz1	$⊢ N \in ℕ \leftrightarrow (N \in ℤ \land 1 \leq N)$
8	6 7	sylibr	$⊢ (N \in ℤ \land 1 < N) \to N \in ℕ$
9		simpr	$⊢ (N \in ℤ \land 1 < N) \to 1 < N$
10	8 9	jca	$⊢ (N \in ℤ \land 1 < N) \to (N \in ℕ \land 1 < N)$
11		nnz	$⊢ N \in ℕ \to N \in ℤ$
12	11	anim1i	$⊢ (N \in ℕ \land 1 < N) \to (N \in ℤ \land 1 < N)$
13	10 12	impbii	$⊢ (N \in ℤ \land 1 < N) \leftrightarrow (N \in ℕ \land 1 < N)$
14	1 13	bitri	$⊢ N \in ℤ_{\geq 2} \leftrightarrow (N \in ℕ \land 1 < N)$

Metamath Proof Explorer