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

Theorem 2z 12006
Description: 2 is an integer. (Contributed by NM, 10-May-2004.)
Assertion
Ref Expression
2z 2 ∈ ℤ

Proof of Theorem 2z
StepHypRef Expression
1 2nn 11702 . 2 2 ∈ ℕ
21nnzi 11998 1 2 ∈ ℤ
Colors of variables: wff setvar class
Syntax hints:  wcel 2112  2c2 11684  cz 11973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-i2m1 10598  ax-1ne0 10599  ax-rrecex 10602  ax-cnre 10603
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-om 7565  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-neg 10866  df-nn 11630  df-2 11692  df-z 11974
This theorem is referenced by:  nn0lt2  12037  nn0le2is012  12038  zadd2cl  12087  eluz4eluz2  12277  uzuzle23  12281  2eluzge1  12286  eluz2b1  12311  nn01to3  12333  nn0ge2m1nnALT  12334  ige2m1fz  12996  fz0to3un2pr  13008  fz0to4untppr  13009  fzctr  13018  fzo0to2pr  13121  fzo0to42pr  13123  2tnp1ge0ge0  13198  flhalf  13199  m1modge3gt1  13285  2txmodxeq0  13298  f13idfv  13367  sqrecd  13514  znsqcld  13526  sq1  13558  expnass  13570  sqoddm1div8  13604  bcn2m1  13684  bcn2p1  13685  4bc2eq6  13689  hashtpg  13843  ccat2s1p2  13981  ccat2s1p2OLD  13983  pfxtrcfv0  14051  pfxtrcfvl  14054  eqwrds3  14320  iseraltlem2  15035  iseraltlem3  15036  climcndslem1  15200  climcnds  15202  bpolydiflem  15404  efgt0  15452  tanval3  15483  cos01bnd  15535  cos01gt0  15540  odd2np1  15686  even2n  15687  oddm1even  15688  oddp1even  15689  oexpneg  15690  mod2eq1n2dvds  15692  2tp1odd  15697  2teven  15700  evend2  15702  oddp1d2  15703  ltoddhalfle  15706  opoe  15708  omoe  15709  opeo  15710  omeo  15711  z0even  15712  z2even  15715  z4even  15717  4dvdseven  15718  m1expo  15720  m1exp1  15721  nn0o  15728  sumeven  15732  flodddiv4  15758  bits0e  15772  bits0o  15773  bitsp1e  15775  bitsp1o  15776  bitsfzo  15778  bitsmod  15779  bitscmp  15781  bitsinv1lem  15784  bitsinv1  15785  6gcd4e2  15880  3lcm2e6woprm  15953  lcmf2a3a4e12  15985  isprm3  16021  dvdsnprmd  16028  2prm  16030  2mulprm  16031  oddprmge3  16038  ge2nprmge4  16039  isprm7  16046  divgcdodd  16048  oddprm  16141  pythagtriplem4  16150  pythagtriplem11  16156  pythagtriplem13  16158  iserodd  16166  prmgaplem3  16383  prmgaplem7  16387  dec2dvds  16393  prmlem0  16435  4001lem1  16470  psgnunilem4  18621  efgredleme  18865  lt6abl  19012  ablsimpgfindlem1  19226  ablsimpgfindlem2  19227  zringndrg  20187  znidomb  20257  chfacfscmulfsupp  21468  chfacfpmmulfsupp  21472  minveclem2  24034  minveclem3  24037  pjthlem1  24045  dyaddisjlem  24203  mbfi1fseqlem5  24327  dvrecg  24580  dvexp3  24585  aaliou3lem6  24948  tanregt0  25135  efif1olem4  25141  tanarg  25214  cxpsqrtth  25324  2irrexpq  25325  2logb9irr  25385  2logb9irrALT  25388  sqrt2cxp2logb9e3  25389  cubic2  25438  asinlem3  25461  atantayl2  25528  cxp2limlem  25565  lgamgulmlem3  25620  lgamgulmlem4  25621  basellem2  25671  basellem3  25672  basellem4  25673  basellem5  25674  basellem8  25677  basellem9  25678  ppisval  25693  ppiprm  25740  ppinprm  25741  chtprm  25742  chtnprm  25743  chtdif  25747  ppidif  25752  ppi1  25753  cht1  25754  cht3  25762  ppieq0  25765  ppiublem1  25790  chpeq0  25796  chtub  25800  chpval2  25806  chpub  25808  mersenne  25815  perfect1  25816  perfectlem1  25817  perfectlem2  25818  bposlem1  25872  bposlem2  25873  bposlem3  25874  bposlem5  25876  bposlem6  25877  lgslem1  25885  lgsdir2lem2  25914  lgsdir2  25918  lgsqr  25939  gausslemma2dlem0i  25952  gausslemma2dlem1a  25953  gausslemma2dlem5a  25958  gausslemma2dlem5  25959  gausslemma2dlem6  25960  gausslemma2dlem7  25961  gausslemma2d  25962  lgseisenlem1  25963  lgseisenlem2  25964  lgseisenlem3  25965  lgseisenlem4  25966  lgsquadlem1  25968  lgsquadlem2  25969  lgsquad2lem1  25972  lgsquad2lem2  25973  lgsquad2  25974  lgsquad3  25975  m1lgs  25976  2lgslem1a1  25977  2lgslem1a2  25978  2lgslem1b  25980  2lgslem3b1  25989  2lgslem3c1  25990  2lgs2  25993  2lgs  25995  2lgsoddprmlem2  25997  2lgsoddprmlem3  26002  2lgsoddprm  26004  2sqblem  26019  2sqmod  26024  chebbnd1lem1  26057  chebbnd1lem3  26059  chebbnd1  26060  dchrisum0lem1a  26074  dchrvmasumiflem1  26089  dchrisum0flblem1  26096  dchrisum0flblem2  26097  dchrisum0lem1b  26103  dchrisum0lem1  26104  dchrisum0lem2a  26105  dchrisum0lem2  26106  dchrisum0lem3  26107  mulog2sumlem2  26123  pntlemd  26182  pntlema  26184  pntlemb  26185  pntlemh  26187  pntlemr  26190  pntlemf  26193  pntlemo  26195  istrkg2ld  26258  istrkg3ld  26259  axlowdimlem3  26742  axlowdimlem6  26745  axlowdimlem16  26755  axlowdimlem17  26756  axlowdim  26759  usgrexmpldifpr  27052  usgrexmplef  27053  cusgrsizeindb1  27244  pthdlem1  27559  clwlkclwwlklem2a1  27781  clwlkclwwlklem2fv1  27784  clwlkclwwlklem2fv2  27785  clwlkclwwlklem2a4  27786  clwlkclwwlklem2a  27787  clwwisshclwwslem  27803  eupth2lem3lem3  28019  konigsberglem5  28045  2clwwlk2  28137  numclwwlk2lem1  28165  numclwlk2lem2f  28166  frgrreggt1  28182  ex-fl  28236  ex-mod  28238  ex-hash  28242  ex-dvds  28245  ex-ind-dvds  28250  minvecolem3  28663  pjhthlem1  29178  wrdt2ind  30657  archirngz  30872  archiabllem2c  30878  lmat22det  31179  dya2ub  31642  dya2icoseg  31649  oddpwdc  31726  eulerpartlemd  31738  eulerpartlemt  31743  ballotlem2  31860  signslema  31946  prodfzo03  31988  hgt750leme  32043  tgoldbachgtde  32045  nn0prpwlem  33784  knoppndvlem2  33966  knoppndvlem8  33972  irrdifflemf  34740  poimirlem25  35081  poimirlem26  35082  poimirlem27  35083  poimirlem28  35084  logblebd  39261  lcm2un  39301  lcm3un  39302  lcmineqlem18  39333  lcmineqlem19  39334  lcmineqlem21  39336  lcmineqlem22  39337  5bc2eq10  39343  2np3bcnp1  39345  2ap1caineq  39346  acongrep  39918  acongeq  39921  jm2.18  39926  jm2.22  39933  jm2.23  39934  jm2.20nn  39935  jm2.26a  39938  jm2.26  39940  jm2.15nn0  39941  jm2.27a  39943  jm2.27c  39945  rmydioph  39952  jm3.1lem1  39955  jm3.1lem3  39957  expdiophlem1  39959  expdiophlem2  39960  hashnzfz2  41022  sumnnodd  42269  coskpi2  42505  cosknegpi  42508  dvdivbd  42562  stoweidlem26  42665  wallispilem4  42707  wallispi2lem1  42710  wallispi2lem2  42711  wallispi2  42712  stirlinglem1  42713  stirlinglem3  42715  stirlinglem7  42719  stirlinglem8  42720  stirlinglem10  42722  stirlinglem11  42723  stirlinglem15  42727  dirkertrigeqlem1  42737  dirkercncflem2  42743  fourierdlem54  42799  fourierdlem56  42801  fourierdlem57  42802  fourierdlem102  42847  fourierdlem114  42859  fourierswlem  42869  fouriersw  42870  smfmullem4  43423  fmtnorec1  44051  goldbachthlem2  44060  odz2prm2pw  44077  fmtnoprmfac1  44079  fmtnoprmfac2lem1  44080  fmtnoprmfac2  44081  fmtno4prmfac  44086  31prm  44111  sfprmdvdsmersenne  44118  lighneallem1  44120  lighneallem4a  44123  lighneallem4b  44124  lighneallem4  44125  proththdlem  44128  proththd  44129  3exp4mod41  44131  41prothprmlem2  44133  m1expevenALTV  44162  dfeven2  44164  m2even  44169  gcd2odd1  44183  oexpnegALTV  44192  oexpnegnz  44193  2evenALTV  44207  2noddALTV  44208  nn0o1gt2ALTV  44209  nnpw2evenALTV  44217  perfectALTVlem1  44236  perfectALTVlem2  44237  fppr2odd  44246  341fppr2  44249  9fppr8  44252  nfermltl2rev  44258  sbgoldbalt  44296  mogoldbb  44300  nnsum4primesodd  44311  nnsum4primesoddALTV  44312  wtgoldbnnsum4prm  44317  bgoldbnnsum3prm  44319  2even  44554  zlmodzxzequa  44902  zlmodzxznm  44903  zlmodzxzequap  44905  zlmodzxzldeplem1  44906  zlmodzxzldeplem3  44908  zlmodzxzldep  44910  ldepsnlinclem1  44911  ldepsnlinc  44914  pw2m1lepw2m1  44926  fldivexpfllog2  44976  nnlog2ge0lt1  44977  logbpw2m1  44978  fllog2  44979  blennnelnn  44987  blenpw2  44989  nnpw2blenfzo  44992  blennnt2  45000  nnolog2flm1  45001  dig2nn0ld  45015  dig2nn1st  45016  0dig2pr01  45021  0dig2nn0o  45024  ackval42  45107  itsclc0xyqsolr  45180
  Copyright terms: Public domain W3C validator