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

Theorem 2z 10101
Description: Two is an integer. (Contributed by NM, 10-May-2004.)
Assertion
Ref Expression
2z  |-  2  e.  ZZ

Proof of Theorem 2z
StepHypRef Expression
1 2nn 9924 . 2  |-  2  e.  NN
21nnzi 10094 1  |-  2  e.  ZZ
Colors of variables: wff set class
Syntax hints:    e. wcel 1701   2c2 9840   ZZcz 10071
This theorem is referenced by:  eluz2b1  10336  fzctr  10901  flhalf  11001  sq1  11245  expnass  11255  sqrecd  11296  iseraltlem2  12202  iseraltlem3  12203  climcndslem1  12355  climcnds  12357  efgt0  12430  tanval3  12461  cos01bnd  12513  cos01gt0  12518  odd2np1  12634  oddm1even  12635  oddp1even  12636  oexpneg  12637  bits0e  12667  bits0o  12668  bitsp1e  12670  bitsp1o  12671  bitsfzolem  12672  bitsfzo  12673  bitsmod  12674  bitscmp  12676  bitsinv1lem  12679  bitsinv1  12680  isprm3  12814  2prm  12821  3prm  12822  divgcdodd  12845  opoe  12911  omoe  12912  opeo  12913  omeo  12914  oddprm  12915  pythagtriplem4  12919  pythagtriplem11  12925  pythagtriplem13  12927  iserodd  12935  dec2dvds  13125  prmlem0  13154  4001lem1  13186  efgredleme  15101  lt6abl  15230  znidomb  16571  minveclem2  18843  minveclem3  18846  pjthlem1  18854  dyaddisjlem  19003  mbfi1fseqlem5  19127  iblcnlem1  19195  dvexp3  19378  aaliou3lem6  19781  tanregt0  19954  efif1olem4  19960  tanarg  20023  cubic2  20197  asinlem3  20220  atantayl2  20287  cxp2limlem  20323  basellem2  20372  basellem3  20373  basellem4  20374  basellem5  20375  basellem8  20378  basellem9  20379  ppisval  20394  ppiprm  20442  ppinprm  20443  chtprm  20444  chtnprm  20445  chtdif  20449  ppidif  20454  ppi1  20455  cht1  20456  cht3  20464  ppieq0  20467  ppiublem1  20494  ppiublem2  20495  chpeq0  20500  chtub  20504  chpval2  20510  chpub  20512  mersenne  20519  perfect1  20520  perfectlem1  20521  perfectlem2  20522  bposlem1  20576  bposlem2  20577  bposlem3  20578  bposlem5  20580  bposlem6  20581  lgslem1  20588  lgsdir2lem2  20616  lgsdir2lem3  20617  lgsdir2  20620  lgsqr  20638  lgseisenlem1  20641  lgseisenlem2  20642  lgseisenlem3  20643  lgseisenlem4  20644  lgsquadlem1  20646  lgsquadlem2  20647  lgsquad2lem1  20650  lgsquad2lem2  20651  lgsquad2  20652  lgsquad3  20653  m1lgs  20654  2sqblem  20669  chebbnd1lem1  20671  chebbnd1lem3  20673  chebbnd1  20674  dchrisum0lem1a  20688  dchrvmasumiflem1  20703  dchrisum0flblem1  20710  dchrisum0flblem2  20711  dchrisum0lem1b  20717  dchrisum0lem1  20718  dchrisum0lem2a  20719  dchrisum0lem2  20720  dchrisum0lem3  20721  mulog2sumlem2  20737  pntlemd  20796  pntlema  20798  pntlemb  20799  pntlemh  20801  pntlemr  20804  pntlemf  20807  pntlemo  20809  ex-fl  20887  ex-dvds  20888  minvecolem3  21510  pjhthlem1  22025  rnlogblem  23591  dya2ub  23794  dya2icoseg  23801  ballotlem2  23920  ballotlemfc0  23924  ballotlemfcc  23925  eupath2lem3  24187  eupath2  24188  4bc2eq6  24385  axlowdimlem3  24958  axlowdimlem6  24961  axlowdimlem16  24971  axlowdimlem17  24972  axlowdim  24975  bpolydiflem  25175  nn0prpwlem  25387  acongrep  26215  acongeq  26218  jm2.18  26229  jm2.22  26236  jm2.23  26237  jm2.20nn  26238  jm2.26a  26241  jm2.26  26243  jm2.15nn0  26244  jm2.27a  26246  jm2.27c  26248  rmydioph  26255  jm3.1lem1  26258  jm3.1lem3  26260  expdiophlem1  26262  expdiophlem2  26263  psgnunilem4  26568  stoweidlem26  26923  wallispilem4  26965  wallispi2lem1  26968  wallispi2lem2  26969  wallispi2  26970  stirlinglem1  26971  stirlinglem3  26973  stirlinglem7  26977  stirlinglem8  26978  stirlinglem10  26980  stirlinglem11  26981  stirlinglem15  26985  fzo0to2pr  27271  fzo0to42pr  27273  hashtpg  27279  4fvwrd4  27296  usgraexvlem  27360  usgraexmpldifpr  27365  usgraexmpl  27366  wlkntrllem4  27464  2trllem4  27493  constr2trl  27494  2pthonlem2  27496  2pthon  27498  usgrcyclnl2  27525  3v3e3cycl1  27528  constr3lem2  27530  constr3lem4  27531  constr3lem5  27532  constr3trllem1  27534  constr3trllem2  27535  constr3trllem3  27536  constr3trllem5  27538  constr3pthlem1  27539  constr3pthlem2  27540  4cycl4v4e  27550  4cycl4dv4e  27552
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549  ax-resscn 8839  ax-1cn 8840  ax-icn 8841  ax-addcl 8842  ax-addrcl 8843  ax-mulcl 8844  ax-mulrcl 8845  ax-mulcom 8846  ax-addass 8847  ax-mulass 8848  ax-distr 8849  ax-i2m1 8850  ax-1ne0 8851  ax-1rid 8852  ax-rnegex 8853  ax-rrecex 8854  ax-cnre 8855  ax-pre-lttri 8856  ax-pre-lttrn 8857  ax-pre-ltadd 8858  ax-pre-mulgt0 8859
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-nel 2482  df-ral 2582  df-rex 2583  df-reu 2584  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-pss 3202  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-tp 3682  df-op 3683  df-uni 3865  df-iun 3944  df-br 4061  df-opab 4115  df-mpt 4116  df-tr 4151  df-eprel 4342  df-id 4346  df-po 4351  df-so 4352  df-fr 4389  df-we 4391  df-ord 4432  df-on 4433  df-lim 4434  df-suc 4435  df-om 4694  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-riota 6346  df-recs 6430  df-rdg 6465  df-er 6702  df-en 6907  df-dom 6908  df-sdom 6909  df-pnf 8914  df-mnf 8915  df-xr 8916  df-ltxr 8917  df-le 8918  df-sub 9084  df-neg 9085  df-nn 9792  df-2 9849  df-z 10072
  Copyright terms: Public domain W3C validator