MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zmulcl Unicode version

Theorem zmulcl 10257
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
StepHypRef Expression
1 elznn0 10229 . 2  |-  ( M  e.  ZZ  <->  ( M  e.  RR  /\  ( M  e.  NN0  \/  -u M  e.  NN0 ) ) )
2 elznn0 10229 . 2  |-  ( N  e.  ZZ  <->  ( N  e.  RR  /\  ( N  e.  NN0  \/  -u N  e.  NN0 ) ) )
3 nn0mulcl 10189 . . . . . . . . 9  |-  ( ( M  e.  NN0  /\  N  e.  NN0 )  -> 
( M  x.  N
)  e.  NN0 )
43orcd 382 . . . . . . . 8  |-  ( ( M  e.  NN0  /\  N  e.  NN0 )  -> 
( ( M  x.  N )  e.  NN0  \/  -u ( M  x.  N
)  e.  NN0 )
)
54a1i 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 9009 . . . . . . 7  |-  ( ( M  e.  RR  /\  N  e.  RR )  ->  ( M  x.  N
)  e.  RR )
75, 6jctild 528 . . . . . 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 10189 . . . . . . . . 9  |-  ( (
-u M  e.  NN0  /\  N  e.  NN0 )  ->  ( -u M  x.  N )  e.  NN0 )
9 recn 9014 . . . . . . . . . . 11  |-  ( M  e.  RR  ->  M  e.  CC )
10 recn 9014 . . . . . . . . . . 11  |-  ( N  e.  RR  ->  N  e.  CC )
11 mulneg1 9403 . . . . . . . . . . 11  |-  ( ( M  e.  CC  /\  N  e.  CC )  ->  ( -u M  x.  N )  =  -u ( M  x.  N
) )
129, 10, 11syl2an 464 . . . . . . . . . 10  |-  ( ( M  e.  RR  /\  N  e.  RR )  ->  ( -u M  x.  N )  =  -u ( M  x.  N
) )
1312eleq1d 2454 . . . . . . . . 9  |-  ( ( M  e.  RR  /\  N  e.  RR )  ->  ( ( -u M  x.  N )  e.  NN0  <->  -u ( M  x.  N )  e.  NN0 ) )
148, 13syl5ib 211 . . . . . . . 8  |-  ( ( M  e.  RR  /\  N  e.  RR )  ->  ( ( -u M  e.  NN0  /\  N  e. 
NN0 )  ->  -u ( M  x.  N )  e.  NN0 ) )
15 olc 374 . . . . . . . 8  |-  ( -u ( M  x.  N
)  e.  NN0  ->  ( ( M  x.  N
)  e.  NN0  \/  -u ( M  x.  N
)  e.  NN0 )
)
1614, 15syl6 31 . . . . . . 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 )
) )
1716, 6jctild 528 . . . . . 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 10189 . . . . . . . . 9  |-  ( ( M  e.  NN0  /\  -u N  e.  NN0 )  ->  ( M  x.  -u N
)  e.  NN0 )
19 mulneg2 9404 . . . . . . . . . . 11  |-  ( ( M  e.  CC  /\  N  e.  CC )  ->  ( M  x.  -u N
)  =  -u ( M  x.  N )
)
209, 10, 19syl2an 464 . . . . . . . . . 10  |-  ( ( M  e.  RR  /\  N  e.  RR )  ->  ( M  x.  -u N
)  =  -u ( M  x.  N )
)
2120eleq1d 2454 . . . . . . . . 9  |-  ( ( M  e.  RR  /\  N  e.  RR )  ->  ( ( M  x.  -u N )  e.  NN0  <->  -u ( M  x.  N )  e.  NN0 ) )
2218, 21syl5ib 211 . . . . . . . 8  |-  ( ( M  e.  RR  /\  N  e.  RR )  ->  ( ( M  e. 
NN0  /\  -u N  e. 
NN0 )  ->  -u ( M  x.  N )  e.  NN0 ) )
2322, 15syl6 31 . . . . . . 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 )
) )
2423, 6jctild 528 . . . . . 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 10189 . . . . . . . . 9  |-  ( (
-u M  e.  NN0  /\  -u N  e.  NN0 )  ->  ( -u M  x.  -u N )  e. 
NN0 )
26 mul2neg 9406 . . . . . . . . . . 11  |-  ( ( M  e.  CC  /\  N  e.  CC )  ->  ( -u M  x.  -u N )  =  ( M  x.  N ) )
279, 10, 26syl2an 464 . . . . . . . . . 10  |-  ( ( M  e.  RR  /\  N  e.  RR )  ->  ( -u M  x.  -u N )  =  ( M  x.  N ) )
2827eleq1d 2454 . . . . . . . . 9  |-  ( ( M  e.  RR  /\  N  e.  RR )  ->  ( ( -u M  x.  -u N )  e. 
NN0 
<->  ( M  x.  N
)  e.  NN0 )
)
2925, 28syl5ib 211 . . . . . . . 8  |-  ( ( M  e.  RR  /\  N  e.  RR )  ->  ( ( -u M  e.  NN0  /\  -u N  e.  NN0 )  ->  ( M  x.  N )  e.  NN0 ) )
30 orc 375 . . . . . . . 8  |-  ( ( M  x.  N )  e.  NN0  ->  ( ( M  x.  N )  e.  NN0  \/  -u ( M  x.  N )  e.  NN0 ) )
3129, 30syl6 31 . . . . . . 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 )
) )
3231, 6jctild 528 . . . . . 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 )
) ) )
337, 17, 24, 32ccased 914 . . . . 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 10229 . . . . 5  |-  ( ( M  x.  N )  e.  ZZ  <->  ( ( M  x.  N )  e.  RR  /\  ( ( M  x.  N )  e.  NN0  \/  -u ( M  x.  N )  e.  NN0 ) ) )
3533, 34syl6ibr 219 . . . 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 ) )
3635imp 419 . . 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 )
3736an4s 800 . 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 )
381, 2, 37syl2anb 466 1  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  x.  N
)  e.  ZZ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358    /\ wa 359    = wceq 1649    e. wcel 1717  (class class class)co 6021   CCcc 8922   RRcr 8923    x. cmul 8929   -ucneg 9225   NN0cn0 10154   ZZcz 10215
This theorem is referenced by:  zdivmul  10275  msqznn  10284  zmulcld  10314  uz2mulcl  10486  qaddcl  10523  qmulcl  10525  qreccl  10527  fzctr  11048  flmulnn0  11157  zexpcl  11324  iexpcyc  11413  zesq  11430  dvdsmul1  12799  dvdsmul2  12800  muldvds1  12802  muldvds2  12803  dvdscmul  12804  dvdsmulc  12805  dvdscmulr  12806  dvdsmulcr  12807  dvds2ln  12808  dvdstr  12811  dvdsmultr1  12812  dvdsmultr2  12813  oexpneg  12839  divalglem0  12841  divalglem2  12843  divalglem4  12844  divalglem8  12848  divalgb  12852  divalgmod  12854  ndvdsi  12858  gcdaddmlem  12956  absmulgcd  12975  gcdmultiple  12978  gcdmultiplez  12979  dvdsmulgcd  12982  rpmulgcd  12983  coprmdvds  13030  rpmul  13051  eulerthlem2  13099  pythagtriplem4  13121  pcpremul  13145  pcmul  13153  gzmulcl  13234  pgpfac1lem2  15561  zsubrg  16676  dvdsrz  16691  mulgrhm  16711  domnchr  16737  znfld  16765  znunit  16768  mbfi1fseqlem5  19479  dvexp3  19730  basellem2  20732  basellem5  20735  dvdsflf1o  20840  chtub  20864  bposlem1  20936  bposlem5  20940  bposlem6  20941  lgslem3  20950  lgsval4a  20970  lgsneg  20971  lgsdir2  20980  lgsdchr  21000  lgseisenlem1  21001  lgseisenlem2  21002  lgseisenlem3  21003  lgsquadlem1  21006  lgsquad2lem2  21011  chebbnd1lem1  21031  chebbnd1lem3  21033  gxnn0mul  21714  fprodzcl  25060  zrisefaccl  25105  zfallfaccl  25106  fzmul  26136  mzpclall  26476  mzpindd  26495  acongrep  26737  acongeq  26740  jm2.18  26751  jm2.21  26757  jm2.26a  26763  jm2.26  26765  jm2.16nn0  26767  jm2.27a  26768  jm2.27c  26770  jm3.1lem3  26782
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-sep 4272  ax-nul 4280  ax-pow 4319  ax-pr 4345  ax-un 4642  ax-resscn 8981  ax-1cn 8982  ax-icn 8983  ax-addcl 8984  ax-addrcl 8985  ax-mulcl 8986  ax-mulrcl 8987  ax-mulcom 8988  ax-addass 8989  ax-mulass 8990  ax-distr 8991  ax-i2m1 8992  ax-1ne0 8993  ax-1rid 8994  ax-rnegex 8995  ax-rrecex 8996  ax-cnre 8997  ax-pre-lttri 8998  ax-pre-lttrn 8999  ax-pre-ltadd 9000
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2243  df-mo 2244  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-nel 2554  df-ral 2655  df-rex 2656  df-reu 2657  df-rab 2659  df-v 2902  df-sbc 3106  df-csb 3196  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-pss 3280  df-nul 3573  df-if 3684  df-pw 3745  df-sn 3764  df-pr 3765  df-tp 3766  df-op 3767  df-uni 3959  df-iun 4038  df-br 4155  df-opab 4209  df-mpt 4210  df-tr 4245  df-eprel 4436  df-id 4440  df-po 4445  df-so 4446  df-fr 4483  df-we 4485  df-ord 4526  df-on 4527  df-lim 4528  df-suc 4529  df-om 4787  df-xp 4825  df-rel 4826  df-cnv 4827  df-co 4828  df-dm 4829  df-rn 4830  df-res 4831  df-ima 4832  df-iota 5359  df-fun 5397  df-fn 5398  df-f 5399  df-f1 5400  df-fo 5401  df-f1o 5402  df-fv 5403  df-ov 6024  df-oprab 6025  df-mpt2 6026  df-riota 6486  df-recs 6570  df-rdg 6605  df-er 6842  df-en 7047  df-dom 7048  df-sdom 7049  df-pnf 9056  df-mnf 9057  df-ltxr 9059  df-sub 9226  df-neg 9227  df-nn 9934  df-n0 10155  df-z 10216
  Copyright terms: Public domain W3C validator