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

Theorem zmulcl 12617
Description: Closure of multiplication of integers. (Contributed by NM, 30-Jul-2004.)
Assertion
Ref Expression
zmulcl ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„ค)

Proof of Theorem zmulcl
StepHypRef Expression
1 elznn0 12579 . 2 (๐‘€ โˆˆ โ„ค โ†” (๐‘€ โˆˆ โ„ โˆง (๐‘€ โˆˆ โ„•0 โˆจ -๐‘€ โˆˆ โ„•0)))
2 elznn0 12579 . 2 (๐‘ โˆˆ โ„ค โ†” (๐‘ โˆˆ โ„ โˆง (๐‘ โˆˆ โ„•0 โˆจ -๐‘ โˆˆ โ„•0)))
3 nn0mulcl 12514 . . . . . . . . 9 ((๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„•0)
43orcd 869 . . . . . . . 8 ((๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0) โ†’ ((๐‘€ ยท ๐‘) โˆˆ โ„•0 โˆจ -(๐‘€ ยท ๐‘) โˆˆ โ„•0))
54a1i 11 . . . . . . 7 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ((๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0) โ†’ ((๐‘€ ยท ๐‘) โˆˆ โ„•0 โˆจ -(๐‘€ ยท ๐‘) โˆˆ โ„•0)))
6 remulcl 11199 . . . . . . 7 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„)
75, 6jctild 524 . . . . . 6 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ((๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0) โ†’ ((๐‘€ ยท ๐‘) โˆˆ โ„ โˆง ((๐‘€ ยท ๐‘) โˆˆ โ„•0 โˆจ -(๐‘€ ยท ๐‘) โˆˆ โ„•0))))
8 nn0mulcl 12514 . . . . . . . . 9 ((-๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0) โ†’ (-๐‘€ ยท ๐‘) โˆˆ โ„•0)
9 recn 11204 . . . . . . . . . . 11 (๐‘€ โˆˆ โ„ โ†’ ๐‘€ โˆˆ โ„‚)
10 recn 11204 . . . . . . . . . . 11 (๐‘ โˆˆ โ„ โ†’ ๐‘ โˆˆ โ„‚)
11 mulneg1 11656 . . . . . . . . . . 11 ((๐‘€ โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ (-๐‘€ ยท ๐‘) = -(๐‘€ ยท ๐‘))
129, 10, 11syl2an 594 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (-๐‘€ ยท ๐‘) = -(๐‘€ ยท ๐‘))
1312eleq1d 2816 . . . . . . . . 9 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ((-๐‘€ ยท ๐‘) โˆˆ โ„•0 โ†” -(๐‘€ ยท ๐‘) โˆˆ โ„•0))
148, 13imbitrid 243 . . . . . . . 8 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ((-๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0) โ†’ -(๐‘€ ยท ๐‘) โˆˆ โ„•0))
15 olc 864 . . . . . . . 8 (-(๐‘€ ยท ๐‘) โˆˆ โ„•0 โ†’ ((๐‘€ ยท ๐‘) โˆˆ โ„•0 โˆจ -(๐‘€ ยท ๐‘) โˆˆ โ„•0))
1614, 15syl6 35 . . . . . . 7 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ((-๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0) โ†’ ((๐‘€ ยท ๐‘) โˆˆ โ„•0 โˆจ -(๐‘€ ยท ๐‘) โˆˆ โ„•0)))
1716, 6jctild 524 . . . . . 6 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ((-๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0) โ†’ ((๐‘€ ยท ๐‘) โˆˆ โ„ โˆง ((๐‘€ ยท ๐‘) โˆˆ โ„•0 โˆจ -(๐‘€ ยท ๐‘) โˆˆ โ„•0))))
18 nn0mulcl 12514 . . . . . . . . 9 ((๐‘€ โˆˆ โ„•0 โˆง -๐‘ โˆˆ โ„•0) โ†’ (๐‘€ ยท -๐‘) โˆˆ โ„•0)
19 mulneg2 11657 . . . . . . . . . . 11 ((๐‘€ โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ (๐‘€ ยท -๐‘) = -(๐‘€ ยท ๐‘))
209, 10, 19syl2an 594 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (๐‘€ ยท -๐‘) = -(๐‘€ ยท ๐‘))
2120eleq1d 2816 . . . . . . . . 9 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ((๐‘€ ยท -๐‘) โˆˆ โ„•0 โ†” -(๐‘€ ยท ๐‘) โˆˆ โ„•0))
2218, 21imbitrid 243 . . . . . . . 8 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ((๐‘€ โˆˆ โ„•0 โˆง -๐‘ โˆˆ โ„•0) โ†’ -(๐‘€ ยท ๐‘) โˆˆ โ„•0))
2322, 15syl6 35 . . . . . . 7 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ((๐‘€ โˆˆ โ„•0 โˆง -๐‘ โˆˆ โ„•0) โ†’ ((๐‘€ ยท ๐‘) โˆˆ โ„•0 โˆจ -(๐‘€ ยท ๐‘) โˆˆ โ„•0)))
2423, 6jctild 524 . . . . . 6 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ((๐‘€ โˆˆ โ„•0 โˆง -๐‘ โˆˆ โ„•0) โ†’ ((๐‘€ ยท ๐‘) โˆˆ โ„ โˆง ((๐‘€ ยท ๐‘) โˆˆ โ„•0 โˆจ -(๐‘€ ยท ๐‘) โˆˆ โ„•0))))
25 nn0mulcl 12514 . . . . . . . . 9 ((-๐‘€ โˆˆ โ„•0 โˆง -๐‘ โˆˆ โ„•0) โ†’ (-๐‘€ ยท -๐‘) โˆˆ โ„•0)
26 mul2neg 11659 . . . . . . . . . . 11 ((๐‘€ โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ (-๐‘€ ยท -๐‘) = (๐‘€ ยท ๐‘))
279, 10, 26syl2an 594 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (-๐‘€ ยท -๐‘) = (๐‘€ ยท ๐‘))
2827eleq1d 2816 . . . . . . . . 9 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ((-๐‘€ ยท -๐‘) โˆˆ โ„•0 โ†” (๐‘€ ยท ๐‘) โˆˆ โ„•0))
2925, 28imbitrid 243 . . . . . . . 8 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ((-๐‘€ โˆˆ โ„•0 โˆง -๐‘ โˆˆ โ„•0) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„•0))
30 orc 863 . . . . . . . 8 ((๐‘€ ยท ๐‘) โˆˆ โ„•0 โ†’ ((๐‘€ ยท ๐‘) โˆˆ โ„•0 โˆจ -(๐‘€ ยท ๐‘) โˆˆ โ„•0))
3129, 30syl6 35 . . . . . . 7 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ((-๐‘€ โˆˆ โ„•0 โˆง -๐‘ โˆˆ โ„•0) โ†’ ((๐‘€ ยท ๐‘) โˆˆ โ„•0 โˆจ -(๐‘€ ยท ๐‘) โˆˆ โ„•0)))
3231, 6jctild 524 . . . . . 6 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ((-๐‘€ โˆˆ โ„•0 โˆง -๐‘ โˆˆ โ„•0) โ†’ ((๐‘€ ยท ๐‘) โˆˆ โ„ โˆง ((๐‘€ ยท ๐‘) โˆˆ โ„•0 โˆจ -(๐‘€ ยท ๐‘) โˆˆ โ„•0))))
337, 17, 24, 32ccased 1035 . . . . 5 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (((๐‘€ โˆˆ โ„•0 โˆจ -๐‘€ โˆˆ โ„•0) โˆง (๐‘ โˆˆ โ„•0 โˆจ -๐‘ โˆˆ โ„•0)) โ†’ ((๐‘€ ยท ๐‘) โˆˆ โ„ โˆง ((๐‘€ ยท ๐‘) โˆˆ โ„•0 โˆจ -(๐‘€ ยท ๐‘) โˆˆ โ„•0))))
34 elznn0 12579 . . . . 5 ((๐‘€ ยท ๐‘) โˆˆ โ„ค โ†” ((๐‘€ ยท ๐‘) โˆˆ โ„ โˆง ((๐‘€ ยท ๐‘) โˆˆ โ„•0 โˆจ -(๐‘€ ยท ๐‘) โˆˆ โ„•0)))
3533, 34imbitrrdi 251 . . . 4 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (((๐‘€ โˆˆ โ„•0 โˆจ -๐‘€ โˆˆ โ„•0) โˆง (๐‘ โˆˆ โ„•0 โˆจ -๐‘ โˆˆ โ„•0)) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„ค))
3635imp 405 . . 3 (((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โˆง ((๐‘€ โˆˆ โ„•0 โˆจ -๐‘€ โˆˆ โ„•0) โˆง (๐‘ โˆˆ โ„•0 โˆจ -๐‘ โˆˆ โ„•0))) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„ค)
3736an4s 656 . 2 (((๐‘€ โˆˆ โ„ โˆง (๐‘€ โˆˆ โ„•0 โˆจ -๐‘€ โˆˆ โ„•0)) โˆง (๐‘ โˆˆ โ„ โˆง (๐‘ โˆˆ โ„•0 โˆจ -๐‘ โˆˆ โ„•0))) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„ค)
381, 2, 37syl2anb 596 1 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„ค)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 394   โˆจ wo 843   = wceq 1539   โˆˆ wcel 2104  (class class class)co 7413  โ„‚cc 11112  โ„cr 11113   ยท cmul 11119  -cneg 11451  โ„•0cn0 12478  โ„คcz 12564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7729  ax-resscn 11171  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-mulcom 11178  ax-addass 11179  ax-mulass 11180  ax-distr 11181  ax-i2m1 11182  ax-1ne0 11183  ax-1rid 11184  ax-rnegex 11185  ax-rrecex 11186  ax-cnre 11187  ax-pre-lttri 11188  ax-pre-lttrn 11189  ax-pre-ltadd 11190
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7860  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-er 8707  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11256  df-mnf 11257  df-ltxr 11259  df-sub 11452  df-neg 11453  df-nn 12219  df-n0 12479  df-z 12565
This theorem is referenced by:  zdivmul  12640  msqznn  12650  zmulcld  12678  uz2mulcl  12916  qaddcl  12955  qmulcl  12957  qreccl  12959  fzctr  13619  flmulnn0  13798  zexpcl  14048  iexpcyc  14177  zesq  14195  cshweqrep  14777  fprodzcl  15904  zrisefaccl  15970  zfallfaccl  15971  dvdsmul1  16227  dvdsmul2  16228  muldvds1  16230  muldvds2  16231  dvdscmul  16232  dvdsmulc  16233  dvdscmulr  16234  dvdsmulcr  16235  dvds2ln  16238  dvdstr  16243  dvdsmultr1  16245  dvdsmultr2  16247  3dvdsdec  16281  3dvds2dec  16282  oexpneg  16294  mulsucdiv2z  16302  divalglem0  16342  divalglem2  16344  divalglem4  16345  divalglem8  16349  divalgb  16353  divalgmod  16355  ndvdsi  16361  gcdaddmlem  16471  absmulgcd  16497  dvdsmulgcd  16503  rpmulgcd  16504  lcmcllem  16539  rpmul  16602  cncongr1  16610  cncongr2  16611  eulerthlem2  16721  modprminv  16738  modprminveq  16739  modprm0  16744  pythagtriplem4  16758  pcpremul  16782  pcmul  16790  gzmulcl  16877  pgpfac1lem2  19988  zsubrg  21200  dvdsrzring  21234  mulgrhm  21250  pzriprnglem5  21256  pzriprng1ALT  21267  domnchr  21305  znfld  21337  znunit  21340  mbfi1fseqlem5  25471  dvexp3  25729  basellem2  26820  basellem5  26823  dvdsflf1o  26925  chtub  26949  bposlem1  27021  bposlem5  27025  bposlem6  27026  lgslem3  27036  lgsval4a  27056  lgsneg  27058  lgsdir2  27067  lgsdchr  27092  lgseisenlem1  27112  lgseisenlem2  27113  lgseisenlem3  27114  lgsquadlem1  27117  lgsquad2lem2  27122  2lgsoddprmlem2  27146  chebbnd1lem1  27206  chebbnd1lem3  27208  knoppndvlem2  35694  fzmul  36914  mzpclall  41769  mzpindd  41788  acongrep  42023  acongeq  42026  jm2.18  42031  jm2.21  42037  jm2.26a  42043  jm2.26  42045  jm2.16nn0  42047  jm2.27a  42048  jm2.27c  42050  jm3.1lem3  42062  fourierswlem  45246  oexpnegALTV  46645  oexpnegnz  46646  tgblthelfgott  46783  2zrngmmgm  46934  zlmodzxzequa  47266  zlmodzxzequap  47269
  Copyright terms: Public domain W3C validator