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 M 2 N 2 M N 2

Proof

Step Hyp Ref Expression
1 eluzelz M 2 M
2 eluzelz N 2 N
3 zmulcl M N M N
4 1 2 3 syl2an M 2 N 2 M N
5 eluz2b1 M 2 M 1 < M
6 zre M M
7 6 anim1i M 1 < M M 1 < M
8 5 7 sylbi M 2 M 1 < M
9 eluz2b1 N 2 N 1 < N
10 zre N N
11 10 anim1i N 1 < N N 1 < N
12 9 11 sylbi N 2 N 1 < N
13 mulgt1 M N 1 < M 1 < N 1 < M N
14 13 an4s M 1 < M N 1 < N 1 < M N
15 8 12 14 syl2an M 2 N 2 1 < M N
16 eluz2b1 M N 2 M N 1 < M N
17 4 15 16 sylanbrc M 2 N 2 M N 2