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