Theorem zmulcl 9305

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

Assertion

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

Proof of Theorem zmulcl

Step	Hyp	Ref	Expression
1		elznn0 9267	. 2 |- ( M e. ZZ <-> ( M e. RR /\ ( M e. NN0 \/ -u M e. NN0 ) ) )
2		elznn0 9267	. 2 |- ( N e. ZZ <-> ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) )
3		nn0mulcl 9211	. . . . . . . . 9 |- ( ( M e. NN0 /\ N e. NN0 ) -> ( M x. N ) e. NN0 )
4	3	orcd 733	. . . . . . . 8 |- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( M x. N ) e. NN0 \/ -u ( M x. N ) e. NN0 ) )
5	4	a1i 9	. . . . . . 7 |- ( ( 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 7938	. . . . . . 7 |- ( ( M e. RR /\ N e. RR ) -> ( M x. N ) e. RR )
7	5, 6	jctild 316	. . . . . 6 |- ( ( 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 9211	. . . . . . . . 9 |- ( ( -u M e. NN0 /\ N e. NN0 ) -> ( -u M x. N ) e. NN0 )
9		recn 7943	. . . . . . . . . . 11 |- ( M e. RR -> M e. CC )
10		recn 7943	. . . . . . . . . . 11 |- ( N e. RR -> N e. CC )
11		mulneg1 8351	. . . . . . . . . . 11 |- ( ( M e. CC /\ N e. CC ) -> ( -u M x. N ) = -u ( M x. N ) )
12	9, 10, 11	syl2an 289	. . . . . . . . . 10 |- ( ( M e. RR /\ N e. RR ) -> ( -u M x. N ) = -u ( M x. N ) )
13	12	eleq1d 2246	. . . . . . . . 9 |- ( ( M e. RR /\ N e. RR ) -> ( ( -u M x. N ) e. NN0 <-> -u ( M x. N ) e. NN0 ) )
14	8, 13	imbitrid 154	. . . . . . . 8 |- ( ( M e. RR /\ N e. RR ) -> ( ( -u M e. NN0 /\ N e. NN0 ) -> -u ( M x. N ) e. NN0 ) )
15		olc 711	. . . . . . . 8 |- ( -u ( M x. N ) e. NN0 -> ( ( M x. N ) e. NN0 \/ -u ( M x. N ) e. NN0 ) )
16	14, 15	syl6 33	. . . . . . 7 |- ( ( 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 316	. . . . . 6 |- ( ( 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 9211	. . . . . . . . 9 |- ( ( M e. NN0 /\ -u N e. NN0 ) -> ( M x. -u N ) e. NN0 )
19		mulneg2 8352	. . . . . . . . . . 11 |- ( ( M e. CC /\ N e. CC ) -> ( M x. -u N ) = -u ( M x. N ) )
20	9, 10, 19	syl2an 289	. . . . . . . . . 10 |- ( ( M e. RR /\ N e. RR ) -> ( M x. -u N ) = -u ( M x. N ) )
21	20	eleq1d 2246	. . . . . . . . 9 |- ( ( M e. RR /\ N e. RR ) -> ( ( M x. -u N ) e. NN0 <-> -u ( M x. N ) e. NN0 ) )
22	18, 21	imbitrid 154	. . . . . . . 8 |- ( ( M e. RR /\ N e. RR ) -> ( ( M e. NN0 /\ -u N e. NN0 ) -> -u ( M x. N ) e. NN0 ) )
23	22, 15	syl6 33	. . . . . . 7 |- ( ( 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 316	. . . . . 6 |- ( ( 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 9211	. . . . . . . . 9 |- ( ( -u M e. NN0 /\ -u N e. NN0 ) -> ( -u M x. -u N ) e. NN0 )
26		mul2neg 8354	. . . . . . . . . . 11 |- ( ( M e. CC /\ N e. CC ) -> ( -u M x. -u N ) = ( M x. N ) )
27	9, 10, 26	syl2an 289	. . . . . . . . . 10 |- ( ( M e. RR /\ N e. RR ) -> ( -u M x. -u N ) = ( M x. N ) )
28	27	eleq1d 2246	. . . . . . . . 9 |- ( ( M e. RR /\ N e. RR ) -> ( ( -u M x. -u N ) e. NN0 <-> ( M x. N ) e. NN0 ) )
29	25, 28	imbitrid 154	. . . . . . . 8 |- ( ( M e. RR /\ N e. RR ) -> ( ( -u M e. NN0 /\ -u N e. NN0 ) -> ( M x. N ) e. NN0 ) )
30		orc 712	. . . . . . . 8 |- ( ( M x. N ) e. NN0 -> ( ( M x. N ) e. NN0 \/ -u ( M x. N ) e. NN0 ) )
31	29, 30	syl6 33	. . . . . . 7 |- ( ( 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 316	. . . . . 6 |- ( ( 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 965	. . . . 5 |- ( ( 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 9267	. . . . 5 |- ( ( 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 162	. . . 4 |- ( ( 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 124	. . 3 |- ( ( ( 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 588	. 2 |- ( ( ( 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 291	1 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ )

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 708   = wceq 1353   e. wcel 2148  (class class class)co 5874   CCcc 7808   RRcr 7809   x. cmul 7815   -ucneg 8128   NN0cn0 9175   ZZcz 9252

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-pr 4209  ax-setind 4536  ax-cnex 7901  ax-resscn 7902  ax-1cn 7903  ax-1re 7904  ax-icn 7905  ax-addcl 7906  ax-addrcl 7907  ax-mulcl 7908  ax-mulrcl 7909  ax-addcom 7910  ax-mulcom 7911  ax-addass 7912  ax-mulass 7913  ax-distr 7914  ax-i2m1 7915  ax-1rid 7917  ax-0id 7918  ax-rnegex 7919  ax-cnre 7921

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-br 4004  df-opab 4065  df-id 4293  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-iota 5178  df-fun 5218  df-fv 5224  df-riota 5830  df-ov 5877  df-oprab 5878  df-mpo 5879  df-sub 8129  df-neg 8130  df-inn 8919  df-n0 9176  df-z 9253

This theorem is referenced by:  zdivmul  9342  msqznn  9352  zmulcld  9380  uz2mulcl  9607  qaddcl  9634  qmulcl  9636  qreccl  9641  fzctr  10132  flqmulnn0  10298  zexpcl  10534  iexpcyc  10624  zesq  10638  fprodzcl  11616  dvdsmul1  11819  dvdsmul2  11820  muldvds1  11822  muldvds2  11823  dvdscmul  11824  dvdsmulc  11825  dvds2ln  11830  dvdstr  11834  dvdsmultr1  11837  dvdsmultr2  11839  3dvdsdec  11869  3dvds2dec  11870  oexpneg  11881  mulsucdiv2z  11889  divalgb  11929  divalgmod  11931  ndvdsi  11937  absmulgcd  12017  gcdmultiple  12020  gcdmultiplez  12021  dvdsmulgcd  12025  rpmulgcd  12026  lcmcllem  12066  rpmul  12097  cncongr1  12102  cncongr2  12103  modprminv  12248  modprminveq  12249  modprm0  12253  pythagtriplem4  12267  pcpremul  12292  pcmul  12300  gzmulcl  12375  zsubrg  13445  dvdsrzring  13463  lgslem3  14373  lgsval  14375  lgsval2lem  14381  lgsval4a  14393  lgsneg  14395  lgsdir2  14404  lgsdir  14406  lgsdilem2  14407  lgsdi  14408  lgsne0  14409  lgseisenlem1  14420  lgseisenlem2  14421  2lgsoddprmlem2  14424