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 
|- ( ( M e. ( ZZ>= ` 2 ) /\ N e. ( ZZ>= ` 2 ) ) -> ( M x. N ) e. ( ZZ>= ` 2 ) )

Proof

Step Hyp Ref Expression
1 eluzelz 
 |-  ( M e. ( ZZ>= ` 2 ) -> M e. ZZ )
2 eluzelz 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. ZZ )
3 zmulcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ )
4 1 2 3 syl2an 
 |-  ( ( M e. ( ZZ>= ` 2 ) /\ N e. ( ZZ>= ` 2 ) ) -> ( M x. N ) e. ZZ )
5 eluz2b1 
 |-  ( M e. ( ZZ>= ` 2 ) <-> ( M e. ZZ /\ 1 < M ) )
6 zre 
 |-  ( M e. ZZ -> M e. RR )
7 6 anim1i 
 |-  ( ( M e. ZZ /\ 1 < M ) -> ( M e. RR /\ 1 < M ) )
8 5 7 sylbi 
 |-  ( M e. ( ZZ>= ` 2 ) -> ( M e. RR /\ 1 < M ) )
9 eluz2b1 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. ZZ /\ 1 < N ) )
10 zre 
 |-  ( N e. ZZ -> N e. RR )
11 10 anim1i 
 |-  ( ( N e. ZZ /\ 1 < N ) -> ( N e. RR /\ 1 < N ) )
12 9 11 sylbi 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N e. RR /\ 1 < N ) )
13 mulgt1 
 |-  ( ( ( M e. RR /\ N e. RR ) /\ ( 1 < M /\ 1 < N ) ) -> 1 < ( M x. N ) )
14 13 an4s 
 |-  ( ( ( M e. RR /\ 1 < M ) /\ ( N e. RR /\ 1 < N ) ) -> 1 < ( M x. N ) )
15 8 12 14 syl2an 
 |-  ( ( M e. ( ZZ>= ` 2 ) /\ N e. ( ZZ>= ` 2 ) ) -> 1 < ( M x. N ) )
16 eluz2b1 
 |-  ( ( M x. N ) e. ( ZZ>= ` 2 ) <-> ( ( M x. N ) e. ZZ /\ 1 < ( M x. N ) ) )
17 4 15 16 sylanbrc 
 |-  ( ( M e. ( ZZ>= ` 2 ) /\ N e. ( ZZ>= ` 2 ) ) -> ( M x. N ) e. ( ZZ>= ` 2 ) )