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

Theorem nn0uz 10521
Description: Nonnegative integers expressed as a set of upper integers. (Contributed by NM, 2-Sep-2005.)
Assertion
Ref Expression
nn0uz  |-  NN0  =  ( ZZ>= `  0 )

Proof of Theorem nn0uz
StepHypRef Expression
1 nn0zrab 10311 . 2  |-  NN0  =  { k  e.  ZZ  |  0  <_  k }
2 0z 10294 . . 3  |-  0  e.  ZZ
3 uzval 10491 . . 3  |-  ( 0  e.  ZZ  ->  ( ZZ>=
`  0 )  =  { k  e.  ZZ  |  0  <_  k } )
42, 3ax-mp 8 . 2  |-  ( ZZ>= ` 
0 )  =  {
k  e.  ZZ  | 
0  <_  k }
51, 4eqtr4i 2460 1  |-  NN0  =  ( ZZ>= `  0 )
Colors of variables: wff set class
Syntax hints:    = wceq 1653    e. wcel 1726   {crab 2710   class class class wbr 4213   ` cfv 5455   0cc0 8991    <_ cle 9122   NN0cn0 10222   ZZcz 10283   ZZ>=cuz 10489
This theorem is referenced by:  elnn0uz  10524  eluznn0  10547  nn0infm  10558  fznn0sub2  11087  fseq1p1m1  11123  fzennn  11308  hashgf1o  11311  exple1  11440  faclbnd4lem1  11585  bcn0  11602  bcn1  11605  bcval5  11610  bcpasc  11613  hashfzo0  11696  hashf1  11707  ccatval2  11747  ccatass  11751  swrdid  11773  swrdccat1  11775  swrdccat2  11776  splfv2a  11786  splval2  11787  wrdeqcats1  11789  wrdeqs1cat  11790  cats1un  11791  revccat  11799  cats1fv  11824  binom1dif  12613  isumnn0nn  12623  climcndslem1  12630  climcnds  12632  harmonic  12639  arisum2  12641  explecnv  12645  geoser  12647  geolim  12648  geolim2  12649  geomulcvg  12654  geoisum  12655  geoisumr  12656  mertenslem1  12662  mertenslem2  12663  mertens  12664  efcllem  12681  ef0lem  12682  eff  12685  efcvg  12688  efcvgfsum  12689  reefcl  12690  ege2le3  12693  efcj  12695  eftlcvg  12708  eftlub  12711  effsumlt  12713  ef4p  12715  efgt1p2  12716  efgt1p  12717  eflegeo  12723  eirrlem  12804  ruclem6  12835  ruclem7  12836  divalglem2  12916  divalglem5  12918  bitsfzolem  12947  bitsfzo  12948  bitsfi  12950  bitsinv1lem  12954  bitsinv1  12955  bitsinvp1  12962  sadcf  12966  sadcp1  12968  sadadd  12980  sadass  12984  bitsres  12986  smupf  12991  smupp1  12993  smuval2  12995  smupval  13001  smueqlem  13003  smumul  13006  alginv  13067  algcvg  13068  algcvga  13071  algfx  13072  eucalgcvga  13078  eucalg  13079  dfphi2  13164  phiprmpw  13166  prmdiv  13175  iserodd  13210  pcfac  13269  prmreclem2  13286  prmreclem4  13288  vdwapun  13343  vdwlem1  13350  ramcl2lem  13378  ramtcl  13379  ramtub  13381  gsumwsubmcl  14785  gsumws1  14786  gsumccat  14788  gsumwmhm  14791  sylow1lem1  15233  efginvrel2  15360  efgsp1  15370  efgsres  15371  efgredleme  15376  efgredlemd  15377  efgredlemc  15378  efgredlem  15380  efgcpbllemb  15388  frgpuplem  15405  pgpfaclem1  15640  psrbaglefi  16438  ltbwe  16534  iscmet3lem3  19244  dyadmax  19491  mbfi1fseqlem3  19610  iblcnlem1  19680  itgcnlem  19682  dvnff  19810  dvnp1  19812  dvn2bss  19817  cpncn  19823  dveflem  19864  c1lip2  19883  ig1peu  20095  ig1pdvds  20100  ply1termlem  20123  plyeq0lem  20130  plyaddlem1  20133  plymullem1  20134  coeeulem  20144  dgrcl  20153  dgrub  20154  dgrlb  20156  coeid3  20160  plyco  20161  coeeq2  20162  coefv0  20167  coemulhi  20173  coemulc  20174  dvply1  20202  vieta1lem2  20229  vieta1  20230  elqaalem2  20238  elqaalem3  20239  geolim3  20257  dvtaylp  20287  dvntaylp  20288  taylthlem1  20290  taylthlem2  20291  radcnvlem1  20330  radcnvlem2  20331  radcnvlem3  20332  radcnv0  20333  radcnvlt2  20336  dvradcnv  20338  pserulm  20339  psercn2  20340  pserdvlem2  20345  pserdv2  20347  abelthlem4  20351  abelthlem5  20352  abelthlem6  20353  abelthlem7  20355  abelthlem8  20356  abelthlem9  20357  advlogexp  20547  logtayllem  20551  logtayl  20552  cxpeq  20642  leibpilem2  20782  leibpi  20783  leibpisum  20784  log2cnv  20785  log2tlbnd  20786  log2ublem2  20788  birthdaylem3  20793  wilthlem2  20853  ftalem1  20856  ftalem5  20860  basellem2  20865  basellem3  20866  basellem5  20868  musum  20977  0sgmppw  20983  1sgmprm  20984  chtublem  20996  logexprlim  21010  lgseisenlem1  21134  lgsquadlem2  21140  dchrisumlem1  21184  dchrisumlem2  21185  dchrisum0flblem1  21203  ostth2lem3  21330  eupares  21698  eupap1  21699  eupath2lem3  21702  eupath2  21703  konigsberg  21710  ballotlemfrci  24786  ballotlemfrceq  24787  subfacval2  24874  subfaclim  24875  cvmliftlem7  24979  relexpsucr  25131  fallfacfwd  25353  0fallfac  25354  binomfallfaclem2  25357  prednn0  25478  bpolylem  26095  bpolysum  26100  bpolydiflem  26101  fsumkthpow  26103  bpoly2  26104  bpoly3  26105  bpoly4  26106  heiborlem4  26524  heiborlem6  26526  mapfzcons  26773  irrapxlem1  26886  ltrmynn0  27014  ltrmxnn0  27015  acongeq  27049  jm2.23  27068  jm2.26lem3  27073  psgnunilem2  27396  psgnunilem4  27398  stoweidlem17  27743  stoweidlem34  27760  stirlinglem5  27804  stirlinglem7  27806  fzossnn0  28125  swrd0fvls  28265
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-sep 4331  ax-nul 4339  ax-pow 4378  ax-pr 4404  ax-un 4702  ax-cnex 9047  ax-resscn 9048  ax-1cn 9049  ax-icn 9050  ax-addcl 9051  ax-addrcl 9052  ax-mulcl 9053  ax-mulrcl 9054  ax-mulcom 9055  ax-addass 9056  ax-mulass 9057  ax-distr 9058  ax-i2m1 9059  ax-1ne0 9060  ax-1rid 9061  ax-rnegex 9062  ax-rrecex 9063  ax-cnre 9064  ax-pre-lttri 9065  ax-pre-lttrn 9066  ax-pre-ltadd 9067  ax-pre-mulgt0 9068
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2711  df-rex 2712  df-reu 2713  df-rab 2715  df-v 2959  df-sbc 3163  df-csb 3253  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-tp 3823  df-op 3824  df-uni 4017  df-iun 4096  df-br 4214  df-opab 4268  df-mpt 4269  df-tr 4304  df-eprel 4495  df-id 4499  df-po 4504  df-so 4505  df-fr 4542  df-we 4544  df-ord 4585  df-on 4586  df-lim 4587  df-suc 4588  df-om 4847  df-xp 4885  df-rel 4886  df-cnv 4887  df-co 4888  df-dm 4889  df-rn 4890  df-res 4891  df-ima 4892  df-iota 5419  df-fun 5457  df-fn 5458  df-f 5459  df-f1 5460  df-fo 5461  df-f1o 5462  df-fv 5463  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-riota 6550  df-recs 6634  df-rdg 6669  df-er 6906  df-en 7111  df-dom 7112  df-sdom 7113  df-pnf 9123  df-mnf 9124  df-xr 9125  df-ltxr 9126  df-le 9127  df-sub 9294  df-neg 9295  df-nn 10002  df-n0 10223  df-z 10284  df-uz 10490
  Copyright terms: Public domain W3C validator