This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )