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

Theorem nn0uz 10309
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 10099 . 2  |-  NN0  =  { k  e.  ZZ  |  0  <_  k }
2 0z 10082 . . 3  |-  0  e.  ZZ
3 uzval 10279 . . 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 2339 1  |-  NN0  =  ( ZZ>= `  0 )
Colors of variables: wff set class
Syntax hints:    = wceq 1633    e. wcel 1701   {crab 2581   class class class wbr 4060   ` cfv 5292   0cc0 8782    <_ cle 8913   NN0cn0 10012   ZZcz 10071   ZZ>=cuz 10277
This theorem is referenced by:  elnn0uz  10312  eluznn0  10335  nn0infm  10346  fznn0sub2  10872  fseq1p1m1  10904  fzennn  11077  hashgf1o  11080  exple1  11208  faclbnd4lem1  11353  bcn0  11370  bcn1  11372  bcval5  11377  bcpasc  11380  hashfzo0  11431  hashf1  11442  ccatval2  11479  ccatass  11483  swrdid  11505  swrdccat1  11507  swrdccat2  11508  splfv2a  11518  splval2  11519  wrdeqcats1  11521  wrdeqs1cat  11522  cats1un  11523  revccat  11531  cats1fv  11556  binom1dif  12338  isumnn0nn  12348  climcndslem1  12355  climcnds  12357  harmonic  12364  arisum2  12366  explecnv  12370  geoser  12372  geolim  12373  geolim2  12374  geomulcvg  12379  geoisum  12380  geoisumr  12381  mertenslem1  12387  mertenslem2  12388  mertens  12389  efcllem  12406  ef0lem  12407  eff  12410  efcvg  12413  efcvgfsum  12414  reefcl  12415  ege2le3  12418  efcj  12420  eftlcvg  12433  eftlub  12436  effsumlt  12438  ef4p  12440  efgt1p2  12441  efgt1p  12442  eflegeo  12448  eirrlem  12529  ruclem6  12560  ruclem7  12561  divalglem2  12641  divalglem5  12643  bitsfzolem  12672  bitsfzo  12673  bitsfi  12675  bitsinv1lem  12679  bitsinv1  12680  bitsinvp1  12687  sadcf  12691  sadcp1  12693  sadadd  12705  sadass  12709  bitsres  12711  smupf  12716  smupp1  12718  smuval2  12720  smupval  12726  smueqlem  12728  smumul  12731  alginv  12792  algcvg  12793  algcvga  12796  algfx  12797  eucalgcvga  12803  eucalg  12804  dfphi2  12889  phiprmpw  12891  prmdiv  12900  iserodd  12935  pcfac  12994  prmreclem2  13011  prmreclem4  13013  vdwapun  13068  vdwlem1  13075  ramcl2lem  13103  ramtcl  13104  ramtub  13106  gsumwsubmcl  14510  gsumws1  14511  gsumccat  14513  gsumwmhm  14516  sylow1lem1  14958  efginvrel2  15085  efgsp1  15095  efgsres  15096  efgredleme  15101  efgredlemd  15102  efgredlemc  15103  efgredlem  15105  efgcpbllemb  15113  frgpuplem  15130  pgpfaclem1  15365  psrbaglefi  16167  ltbwe  16263  iscmet3lem3  18769  dyadmax  19006  mbfi1fseqlem3  19125  iblcnlem1  19195  itgcnlem  19197  dvnff  19325  dvnp1  19327  dvn2bss  19332  cpncn  19338  dveflem  19379  c1lip2  19398  ig1peu  19610  ig1pdvds  19615  ply1termlem  19638  plyeq0lem  19645  plyaddlem1  19648  plymullem1  19649  coeeulem  19659  dgrcl  19668  dgrub  19669  dgrlb  19671  coeid3  19675  plyco  19676  coeeq2  19677  coefv0  19682  coemulhi  19688  coemulc  19689  dvply1  19717  vieta1lem2  19744  vieta1  19745  elqaalem2  19753  elqaalem3  19754  geolim3  19772  dvtaylp  19802  dvntaylp  19803  taylthlem1  19805  taylthlem2  19806  radcnvlem1  19842  radcnvlem2  19843  radcnvlem3  19844  radcnv0  19845  radcnvlt2  19848  dvradcnv  19850  pserulm  19851  psercn2  19852  pserdvlem2  19857  pserdv2  19859  abelthlem4  19863  abelthlem5  19864  abelthlem6  19865  abelthlem7  19867  abelthlem8  19868  abelthlem9  19869  advlogexp  20055  logtayllem  20059  logtayl  20060  cxpeq  20150  leibpilem2  20290  leibpi  20291  leibpisum  20292  log2cnv  20293  log2tlbnd  20294  log2ublem2  20296  birthdaylem3  20301  wilthlem2  20360  ftalem1  20363  ftalem5  20367  basellem2  20372  basellem3  20373  basellem5  20375  musum  20484  0sgmppw  20490  1sgmprm  20491  chtublem  20503  logexprlim  20517  lgseisenlem1  20641  lgsquadlem2  20647  dchrisumlem1  20691  dchrisumlem2  20692  dchrisum0flblem1  20710  ostth2lem3  20837  ballotlemfrci  23959  ballotlemfrceq  23960  dmgmseqn0  23980  subfacval2  24002  subfaclim  24003  cvmliftlem7  24106  eupares  24183  eupap1  24184  eupath2lem3  24187  eupath2  24188  konigsberg  24195  relexpsucr  24310  prednn0  24587  bpolylem  25169  bpolysum  25174  bpolydiflem  25175  fsumkthpow  25177  bpoly2  25178  bpoly3  25179  bpoly4  25180  heiborlem4  25686  heiborlem6  25688  mapfzcons  25941  irrapxlem1  26055  ltrmynn0  26183  ltrmxnn0  26184  acongeq  26218  jm2.23  26237  jm2.26lem3  26242  psgnunilem2  26566  psgnunilem4  26568  stoweidlem17  26914  stoweidlem34  26931  stirlinglem5  26975  stirlinglem7  26977
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-cnex 8838  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-n0 10013  df-z 10072  df-uz 10278
  Copyright terms: Public domain W3C validator