Metamath Proof Explorer

Theorem zmulcl

Description: Closure of multiplication of integers. (Contributed by NM, 30-Jul-2004)

Ref Expression
Assertion zmulcl 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ )

Proof

Step Hyp Ref Expression
1 elznn0 
 |-  ( M e. ZZ <-> ( M e. RR /\ ( M e. NN0 \/ -u M e. NN0 ) ) )
2 elznn0 
 |-  ( N e. ZZ <-> ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) )
3 nn0mulcl 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M x. N ) e. NN0 )
4 3 orcd 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( M x. N ) e. NN0 \/ -u ( M x. N ) e. NN0 ) )
5 4 a1i 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( M e. NN0 /\ N e. NN0 ) -> ( ( M x. N ) e. NN0 \/ -u ( M x. N ) e. NN0 ) ) )
6 remulcl 
 |-  ( ( M e. RR /\ N e. RR ) -> ( M x. N ) e. RR )
7 5 6 jctild 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( M e. NN0 /\ N e. NN0 ) -> ( ( M x. N ) e. RR /\ ( ( M x. N ) e. NN0 \/ -u ( M x. N ) e. NN0 ) ) ) )
8 nn0mulcl 
 |-  ( ( -u M e. NN0 /\ N e. NN0 ) -> ( -u M x. N ) e. NN0 )
9 recn 
 |-  ( M e. RR -> M e. CC )
10 recn 
 |-  ( N e. RR -> N e. CC )
11 mulneg1 
 |-  ( ( M e. CC /\ N e. CC ) -> ( -u M x. N ) = -u ( M x. N ) )
12 9 10 11 syl2an 
 |-  ( ( M e. RR /\ N e. RR ) -> ( -u M x. N ) = -u ( M x. N ) )
13 12 eleq1d 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( -u M x. N ) e. NN0 <-> -u ( M x. N ) e. NN0 ) )
14 8 13 imbitrid 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( -u M e. NN0 /\ N e. NN0 ) -> -u ( M x. N ) e. NN0 ) )
15 olc 
 |-  ( -u ( M x. N ) e. NN0 -> ( ( M x. N ) e. NN0 \/ -u ( M x. N ) e. NN0 ) )
16 14 15 syl6 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( -u M e. NN0 /\ N e. NN0 ) -> ( ( M x. N ) e. NN0 \/ -u ( M x. N ) e. NN0 ) ) )
17 16 6 jctild 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( -u M e. NN0 /\ N e. NN0 ) -> ( ( M x. N ) e. RR /\ ( ( M x. N ) e. NN0 \/ -u ( M x. N ) e. NN0 ) ) ) )
18 nn0mulcl 
 |-  ( ( M e. NN0 /\ -u N e. NN0 ) -> ( M x. -u N ) e. NN0 )
19 mulneg2 
 |-  ( ( M e. CC /\ N e. CC ) -> ( M x. -u N ) = -u ( M x. N ) )
20 9 10 19 syl2an 
 |-  ( ( M e. RR /\ N e. RR ) -> ( M x. -u N ) = -u ( M x. N ) )
21 20 eleq1d 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( M x. -u N ) e. NN0 <-> -u ( M x. N ) e. NN0 ) )
22 18 21 imbitrid 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( M e. NN0 /\ -u N e. NN0 ) -> -u ( M x. N ) e. NN0 ) )
23 22 15 syl6 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( M e. NN0 /\ -u N e. NN0 ) -> ( ( M x. N ) e. NN0 \/ -u ( M x. N ) e. NN0 ) ) )
24 23 6 jctild 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( M e. NN0 /\ -u N e. NN0 ) -> ( ( M x. N ) e. RR /\ ( ( M x. N ) e. NN0 \/ -u ( M x. N ) e. NN0 ) ) ) )
25 nn0mulcl 
 |-  ( ( -u M e. NN0 /\ -u N e. NN0 ) -> ( -u M x. -u N ) e. NN0 )
26 mul2neg 
 |-  ( ( M e. CC /\ N e. CC ) -> ( -u M x. -u N ) = ( M x. N ) )
27 9 10 26 syl2an 
 |-  ( ( M e. RR /\ N e. RR ) -> ( -u M x. -u N ) = ( M x. N ) )
28 27 eleq1d 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( -u M x. -u N ) e. NN0 <-> ( M x. N ) e. NN0 ) )
29 25 28 imbitrid 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( -u M e. NN0 /\ -u N e. NN0 ) -> ( M x. N ) e. NN0 ) )
30 orc 
 |-  ( ( M x. N ) e. NN0 -> ( ( M x. N ) e. NN0 \/ -u ( M x. N ) e. NN0 ) )
31 29 30 syl6 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( -u M e. NN0 /\ -u N e. NN0 ) -> ( ( M x. N ) e. NN0 \/ -u ( M x. N ) e. NN0 ) ) )
32 31 6 jctild 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( -u M e. NN0 /\ -u N e. NN0 ) -> ( ( M x. N ) e. RR /\ ( ( M x. N ) e. NN0 \/ -u ( M x. N ) e. NN0 ) ) ) )
33 7 17 24 32 ccased 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( ( M e. NN0 \/ -u M e. NN0 ) /\ ( N e. NN0 \/ -u N e. NN0 ) ) -> ( ( M x. N ) e. RR /\ ( ( M x. N ) e. NN0 \/ -u ( M x. N ) e. NN0 ) ) ) )
34 elznn0 
 |-  ( ( M x. N ) e. ZZ <-> ( ( M x. N ) e. RR /\ ( ( M x. N ) e. NN0 \/ -u ( M x. N ) e. NN0 ) ) )
35 33 34 imbitrrdi 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( ( M e. NN0 \/ -u M e. NN0 ) /\ ( N e. NN0 \/ -u N e. NN0 ) ) -> ( M x. N ) e. ZZ ) )
36 35 imp 
 |-  ( ( ( M e. RR /\ N e. RR ) /\ ( ( M e. NN0 \/ -u M e. NN0 ) /\ ( N e. NN0 \/ -u N e. NN0 ) ) ) -> ( M x. N ) e. ZZ )
37 36 an4s 
 |-  ( ( ( M e. RR /\ ( M e. NN0 \/ -u M e. NN0 ) ) /\ ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) ) -> ( M x. N ) e. ZZ )
38 1 2 37 syl2anb 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ )