Theorem zmulcl 10913

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 10880	. 2 |- ( M e. ZZ <-> ( M e. RR /\ ( M e. NN0 \/ -u M e. NN0 ) ) )
2		elznn0 10880	. 2 |- ( N e. ZZ <-> ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) )
3		nn0mulcl 10833	. . . . . . . . 9 |- ( ( M e. NN0 /\ N e. NN0 ) -> ( M x. N ) e. NN0 )
4	3	orcd 392	. . . . . . . 8 |- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( M x. N ) e. NN0 \/ -u ( M x. N ) e. NN0 ) )
5	4	a1i 11	. . . . . . 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 9575	. . . . . . 7 |- ( ( M e. RR /\ N e. RR ) -> ( M x. N ) e. RR )
7	5, 6	jctild 543	. . . . . 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 10833	. . . . . . . . 9 |- ( ( -u M e. NN0 /\ N e. NN0 ) -> ( -u M x. N ) e. NN0 )
9		recn 9580	. . . . . . . . . . 11 |- ( M e. RR -> M e. CC )
10		recn 9580	. . . . . . . . . . 11 |- ( N e. RR -> N e. CC )
11		mulneg1 9994	. . . . . . . . . . 11 |- ( ( M e. CC /\ N e. CC ) -> ( -u M x. N ) = -u ( M x. N ) )
12	9, 10, 11	syl2an 477	. . . . . . . . . 10 |- ( ( M e. RR /\ N e. RR ) -> ( -u M x. N ) = -u ( M x. N ) )
13	12	eleq1d 2510	. . . . . . . . 9 |- ( ( M e. RR /\ N e. RR ) -> ( ( -u M x. N ) e. NN0 <-> -u ( M x. N ) e. NN0 ) )
14	8, 13	syl5ib 219	. . . . . . . 8 |- ( ( M e. RR /\ N e. RR ) -> ( ( -u M e. NN0 /\ N e. NN0 ) -> -u ( M x. N ) e. NN0 ) )
15		olc 384	. . . . . . . 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 543	. . . . . 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 10833	. . . . . . . . 9 |- ( ( M e. NN0 /\ -u N e. NN0 ) -> ( M x. -u N ) e. NN0 )
19		mulneg2 9995	. . . . . . . . . . 11 |- ( ( M e. CC /\ N e. CC ) -> ( M x. -u N ) = -u ( M x. N ) )
20	9, 10, 19	syl2an 477	. . . . . . . . . 10 |- ( ( M e. RR /\ N e. RR ) -> ( M x. -u N ) = -u ( M x. N ) )
21	20	eleq1d 2510	. . . . . . . . 9 |- ( ( M e. RR /\ N e. RR ) -> ( ( M x. -u N ) e. NN0 <-> -u ( M x. N ) e. NN0 ) )
22	18, 21	syl5ib 219	. . . . . . . 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 543	. . . . . 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 10833	. . . . . . . . 9 |- ( ( -u M e. NN0 /\ -u N e. NN0 ) -> ( -u M x. -u N ) e. NN0 )
26		mul2neg 9997	. . . . . . . . . . 11 |- ( ( M e. CC /\ N e. CC ) -> ( -u M x. -u N ) = ( M x. N ) )
27	9, 10, 26	syl2an 477	. . . . . . . . . 10 |- ( ( M e. RR /\ N e. RR ) -> ( -u M x. -u N ) = ( M x. N ) )
28	27	eleq1d 2510	. . . . . . . . 9 |- ( ( M e. RR /\ N e. RR ) -> ( ( -u M x. -u N ) e. NN0 <-> ( M x. N ) e. NN0 ) )
29	25, 28	syl5ib 219	. . . . . . . 8 |- ( ( M e. RR /\ N e. RR ) -> ( ( -u M e. NN0 /\ -u N e. NN0 ) -> ( M x. N ) e. NN0 ) )
30		orc 385	. . . . . . . 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 543	. . . . . 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 945	. . . . 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 10880	. . . . 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	syl6ibr 227	. . . 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 429	. . 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 824	. 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 479	1 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ )

Syntax hints:   -> wi 4   \/ wo 368   /\ wa 369   = wceq 1381   e. wcel 1802  (class class class)co 6277   CCcc 9488   RRcr 9489   x. cmul 9495   -ucneg 9806   NN0cn0 10796   ZZcz 10865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-iun 4313  df-br 4434  df-opab 4492  df-mpt 4493  df-tr 4527  df-eprel 4777  df-id 4781  df-po 4786  df-so 4787  df-fr 4824  df-we 4826  df-ord 4867  df-on 4868  df-lim 4869  df-suc 4870  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-riota 6238  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-om 6682  df-recs 7040  df-rdg 7074  df-er 7309  df-en 7515  df-dom 7516  df-sdom 7517  df-pnf 9628  df-mnf 9629  df-ltxr 9631  df-sub 9807  df-neg 9808  df-nn 10538  df-n0 10797  df-z 10866

This theorem is referenced by:  zdivmul  10936  msqznn  10945  zmulcld  10975  uz2mulcl  11163  qaddcl  11202  qmulcl  11204  qreccl  11206  fzctr  11790  flmulnn0  11934  zexpcl  12155  iexpcyc  12246  zesq  12263  cshweqrep  12763  dvdsmul1  13877  dvdsmul2  13878  muldvds1  13880  muldvds2  13881  dvdscmul  13882  dvdsmulc  13883  dvdscmulr  13884  dvdsmulcr  13885  dvds2ln  13886  dvdstr  13890  dvdsmultr1  13891  dvdsmultr2  13893  oexpneg  13921  divalglem0  13923  divalglem2  13925  divalglem4  13926  divalglem8  13930  divalgb  13934  divalgmod  13936  ndvdsi  13940  gcdaddmlem  14038  absmulgcd  14057  gcdmultiple  14060  gcdmultiplez  14061  dvdsmulgcd  14064  rpmulgcd  14065  coprmdvds  14115  rpmul  14136  eulerthlem2  14184  modprminv  14198  modprminveq  14199  modprm0  14202  pythagtriplem4  14215  pcpremul  14239  pcmul  14247  gzmulcl  14328  pgpfac1lem2  16994  zsubrg  18339  dvdsrzring  18374  dvdsrz  18375  mulgrhm  18399  mulgrhmOLD  18402  domnchr  18436  znfld  18466  znunit  18469  mbfi1fseqlem5  21992  dvexp3  22245  basellem2  23220  basellem5  23223  dvdsflf1o  23328  chtub  23352  bposlem1  23424  bposlem5  23428  bposlem6  23429  lgslem3  23438  lgsval4a  23458  lgsneg  23459  lgsdir2  23468  lgsdchr  23488  lgseisenlem1  23489  lgseisenlem2  23490  lgseisenlem3  23491  lgsquadlem1  23494  lgsquad2lem2  23499  chebbnd1lem1  23519  chebbnd1lem3  23521  gxnn0mul  25144  fprodzcl  29054  zrisefaccl  29110  zfallfaccl  29111  fzmul  30201  mzpclall  30627  mzpindd  30646  acongrep  30886  acongeq  30889  jm2.18  30898  jm2.21  30904  jm2.26a  30910  jm2.26  30912  jm2.16nn0  30914  jm2.27a  30915  jm2.27c  30917  jm3.1lem3  30929  lcmcllem  31171  fourierswlem  31898  2zrngmmgm  32452  zlmodzxzequa  32807  zlmodzxzequap  32810