Theorem uz2mulcl

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

	Ref	Expression
Assertion	uz2mulcl	⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑀 · 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		eluzelz	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → 𝑀 ∈ ℤ )
2		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℤ )
3		zmulcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
4	1 2 3	syl2an	⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
5		eluz2b1	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑀 ∈ ℤ ∧ 1 < 𝑀 ) )
6		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
7	6	anim1i	⊢ ( ( 𝑀 ∈ ℤ ∧ 1 < 𝑀 ) → ( 𝑀 ∈ ℝ ∧ 1 < 𝑀 ) )
8	5 7	sylbi	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑀 ∈ ℝ ∧ 1 < 𝑀 ) )
9		eluz2b1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℤ ∧ 1 < 𝑁 ) )
10		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
11	10	anim1i	⊢ ( ( 𝑁 ∈ ℤ ∧ 1 < 𝑁 ) → ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) )
12	9 11	sylbi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) )
13		mulgt1	⊢ ( ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ ( 1 < 𝑀 ∧ 1 < 𝑁 ) ) → 1 < ( 𝑀 · 𝑁 ) )
14	13	an4s	⊢ ( ( ( 𝑀 ∈ ℝ ∧ 1 < 𝑀 ) ∧ ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) ) → 1 < ( 𝑀 · 𝑁 ) )
15	8 12 14	syl2an	⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → 1 < ( 𝑀 · 𝑁 ) )
16		eluz2b1	⊢ ( ( 𝑀 · 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( ( 𝑀 · 𝑁 ) ∈ ℤ ∧ 1 < ( 𝑀 · 𝑁 ) ) )
17	4 15 16	sylanbrc	⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑀 · 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) )