uz2mulcl

Description: Closure of multiplication of integers greater than or equal to 2. (Contributed by Paul Chapman, 26-Oct-2012)

		Ref	Expression
	Assertion	uz2mulcl	$⊢ (M \in ℤ_{\geq 2} \land N \in ℤ_{\geq 2}) \to M \cdot N \in ℤ_{\geq 2}$

Step	Hyp	Ref	Expression
1		eluzelz	$⊢ M \in ℤ_{\geq 2} \to M \in ℤ$
2		eluzelz	$⊢ N \in ℤ_{\geq 2} \to N \in ℤ$
3		zmulcl	$⊢ (M \in ℤ \land N \in ℤ) \to M \cdot N \in ℤ$
4	1 2 3	syl2an	$⊢ (M \in ℤ_{\geq 2} \land N \in ℤ_{\geq 2}) \to M \cdot N \in ℤ$
5		eluz2b1	$⊢ M \in ℤ_{\geq 2} \leftrightarrow (M \in ℤ \land 1 < M)$
6		zre	$⊢ M \in ℤ \to M \in ℝ$
7	6	anim1i	$⊢ (M \in ℤ \land 1 < M) \to (M \in ℝ \land 1 < M)$
8	5 7	sylbi	$⊢ M \in ℤ_{\geq 2} \to (M \in ℝ \land 1 < M)$
9		eluz2b1	$⊢ N \in ℤ_{\geq 2} \leftrightarrow (N \in ℤ \land 1 < N)$
10		zre	$⊢ N \in ℤ \to N \in ℝ$
11	10	anim1i	$⊢ (N \in ℤ \land 1 < N) \to (N \in ℝ \land 1 < N)$
12	9 11	sylbi	$⊢ N \in ℤ_{\geq 2} \to (N \in ℝ \land 1 < N)$
13		mulgt1	$⊢ ((M \in ℝ \land N \in ℝ) \land (1 < M \land 1 < N)) \to 1 < M \cdot N$
14	13	an4s	$⊢ ((M \in ℝ \land 1 < M) \land (N \in ℝ \land 1 < N)) \to 1 < M \cdot N$
15	8 12 14	syl2an	$⊢ (M \in ℤ_{\geq 2} \land N \in ℤ_{\geq 2}) \to 1 < M \cdot N$
16		eluz2b1	$⊢ M \cdot N \in ℤ_{\geq 2} \leftrightarrow (M \cdot N \in ℤ \land 1 < M \cdot N)$
17	4 15 16	sylanbrc	$⊢ (M \in ℤ_{\geq 2} \land N \in ℤ_{\geq 2}) \to M \cdot N \in ℤ_{\geq 2}$

Metamath Proof Explorer