Theorem nn0uz 12871

Description: Nonnegative integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.)

Assertion

Ref	Expression
nn0uz	⊢ ℕ0 = (ℤ≥‘0)

Proof of Theorem nn0uz

Step	Hyp	Ref	Expression
1		nn0zrab 12594	. 2 ⊢ ℕ0 = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘}
2		0z 12573	. . 3 ⊢ 0 ∈ ℤ
3		uzval 12835	. . 3 ⊢ (0 ∈ ℤ → (ℤ≥‘0) = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘})
4	2, 3	ax-mp 5	. 2 ⊢ (ℤ≥‘0) = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘}
5	1, 4	eqtr4i 2787	1 ⊢ ℕ0 = (ℤ≥‘0)

Syntax hints:   = wceq 1559   ∈ wcel 2141  {crab 3413   class class class wbr 5097  ‘cfv 6516  0cc0 11067   ≤ cle 11211  ℕ₀cn0 12475  ℤcz 12562  ℤ_≥cuz 12833

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-cnex 11123  ax-resscn 11124  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-addrcl 11128  ax-mulcl 11129  ax-mulrcl 11130  ax-mulcom 11131  ax-addass 11132  ax-mulass 11133  ax-distr 11134  ax-i2m1 11135  ax-1ne0 11136  ax-1rid 11137  ax-rnegex 11138  ax-rrecex 11139  ax-cnre 11140  ax-pre-lttri 11141  ax-pre-lttrn 11142  ax-pre-ltadd 11143  ax-pre-mulgt0 11144

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-riota 7348  df-ov 7394  df-oprab 7395  df-mpo 7396  df-om 7842  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11212  df-mnf 11213  df-xr 11214  df-ltxr 11215  df-le 11216  df-sub 11410  df-neg 11411  df-nn 12205  df-n0 12476  df-z 12563  df-uz 12834

This theorem is referenced by:  elnn0uz  12874  2eluzge0  12876  eluznn0  12912  nn0inf  12925  fseq1p1m1  13597  fznn0sub2  13634  nn0split  13642  prednn0  13651  fzossnn0  13690  fzennn  13975  hashgf1o  13978  exple1  14184  faclbnd4lem1  14300  bcval5  14325  bcpasc  14328  hashfzo0  14437  hashf1  14464  ccatval2  14585  ccatass  14596  ccatrn  14597  swrdccat2  14677  wrdeqs1cat  14727  cats1un  14728  splfv2a  14763  splval2  14764  revccat  14773  cats1fv  14866  binom1dif  15854  isumnn0nn  15863  climcndslem1  15870  climcnds  15872  harmonic  15880  arisum2  15882  explecnv  15886  geoser  15888  pwdif  15889  geolim  15891  geolim2  15892  geomulcvg  15897  geoisum  15898  geoisumr  15899  mertenslem1  15905  mertenslem2  15906  mertens  15907  fallfacfwd  16057  0fallfac  16058  binomfallfaclem2  16061  bpolylem  16069  bpolysum  16074  bpolydiflem  16075  fsumkthpow  16077  bpoly2  16078  bpoly3  16079  bpoly4  16080  efcllem  16098  ef0lem  16099  eff  16102  efcvg  16106  efcvgfsum  16107  reefcl  16108  ege2le3  16111  efcj  16113  eftlcvg  16129  eftlub  16132  effsumlt  16134  ef4p  16136  efgt1p2  16137  efgt1p  16138  eflegeo  16144  eirrlem  16227  ruclem6  16258  ruclem7  16259  divalglem2  16420  divalglem5  16422  bitsfzolem  16459  bitsfzo  16460  bitsfi  16462  bitsinv1lem  16466  bitsinv1  16467  bitsinvp1  16474  sadcf  16478  sadcp1  16480  sadadd  16492  sadass  16496  bitsres  16498  smupf  16503  smupp1  16505  smuval2  16507  smupval  16513  smueqlem  16515  smumul  16518  alginv  16600  algcvg  16601  algcvga  16604  algfx  16605  eucalgcvga  16611  eucalg  16612  phiprmpw  16802  prmdiv  16811  iserodd  16862  pcfac  16926  prmreclem2  16944  prmreclem4  16946  vdwapun  17001  vdwlem1  17008  ramcl2lem  17036  ramtcl  17037  ramtub  17039  chnccats1  18648  gsumwsubmcl  18862  gsumws1  18863  gsumsgrpccat  18865  gsumwmhm  18870  psgnunilem2  19526  psgnunilem4  19528  sylow1lem1  19629  efginvrel2  19758  efgredleme  19774  efgredlemc  19776  efgcpbllemb  19786  frgpuplem  19803  telgsumfz0s  20022  telgsums  20024  pgpfaclem1  20114  psrbaglefi  21966  ltbwe  22085  pmatcollpw3fi1lem1  22834  chfacfisf  22902  chfacfisfcpmat  22903  iscmet3lem3  25340  dyadmax  25648  mbfi1fseqlem3  25767  itgcnlem  25840  dvnff  25973  dvnp1  25975  dvn2bss  25980  cpncn  25986  dveflem  26029  ig1peu  26223  ig1pdvds  26228  ply1termlem  26251  plyeq0lem  26258  plyaddlem1  26261  plymullem1  26262  coeeulem  26272  dgrcl  26281  dgrub  26282  dgrlb  26284  coeid3  26288  plyco  26289  coeeq2  26290  coefv0  26296  coemulhi  26302  coemulc  26303  dvply1  26336  vieta1lem2  26363  vieta1  26364  elqaalem2  26372  elqaalem3  26373  geolim3  26391  dvntaylp  26422  taylthlem1  26424  radcnvlem1  26464  radcnvlem2  26465  radcnvlem3  26466  radcnv0  26467  radcnvlt2  26470  dvradcnv  26472  pserulm  26473  psercn2  26474  pserdvlem2  26479  pserdv2  26481  abelthlem4  26485  abelthlem5  26486  abelthlem6  26487  abelthlem7  26489  abelthlem8  26490  abelthlem9  26491  advlogexp  26708  logtayllem  26712  logtayl  26713  cxpeq  26810  leibpi  26995  leibpisum  26996  log2cnv  26997  log2tlbnd  26998  log2ublem2  27000  birthdaylem3  27006  wilthlem2  27121  ftalem1  27125  ftalem5  27129  basellem2  27134  basellem3  27135  basellem5  27137  musum  27243  0sgmppw  27250  1sgmprm  27251  chtublem  27263  logexprlim  27277  lgseisenlem1  27427  lgsquadlem2  27433  dchrisumlem1  27541  dchrisumlem2  27542  dchrisum0flblem1  27560  ostth2lem3  27687  tgcgr4  28688  clwwlknonex2lem1  30266  eupth2lems  30397  fz2ssnn0  32948  nn0diffz0  32957  nn0split01  32981  ccatws1f1o  33090  gsummulsubdishift1  33209  gsumwrd2dccat  33219  cycpmco2rn  33266  cycpmco2lem6  33272  evl1deg1  33733  evl1deg2  33734  evl1deg3  33735  ig1pmindeg  33759  vietalem  33837  exsslsb  33855  oddpwdc  34612  eulerpartlemb  34626  sseqfn  34648  sseqf  34650  signsplypnf  34805  signstcl  34820  signstf  34821  signstfvn  34824  signstfvneq0  34827  fsum2dsub  34862  reprsuc  34870  breprexplema  34885  breprexplemc  34887  subfacval2  35498  subfaclim  35499  cvmliftlem7  35602  fwddifnp1  36476  knoppcnlem6  36897  knoppcnlem8  36899  knoppcnlem9  36900  knoppcnlem11  36902  knoppcn  36903  knoppndvlem4  36914  knoppndvlem6  36916  knoppf  36934  poimirlem3  38083  poimirlem4  38084  poimirlem18  38098  poimirlem21  38101  poimirlem22  38102  poimirlem25  38105  poimirlem26  38106  poimirlem27  38107  heiborlem4  38274  heiborlem6  38276  lcmfunnnd  42590  mapfzcons  43258  irrapxlem1  43360  ltrmynn0  43486  ltrmxnn0  43487  acongeq  43521  jm2.23  43534  jm2.26lem3  43539  dfrtrcl3  44270  radcnvrat  44851  bcc0  44877  dvradcnv2  44884  binomcxplemnn0  44886  binomcxplemrat  44887  binomcxplemradcnv  44889  binomcxplemnotnn0  44893  fzssnn0  45856  rexanuz2nf  46027  expfac  46192  dvnmptdivc  46473  dvnmul  46478  dvnprodlem3  46483  stoweidlem17  46552  stoweidlem34  46569  stirlinglem5  46613  stirlinglem7  46615  fourierdlem15  46657  fourierdlem25  46667  fourierdlem48  46689  fourierdlem49  46690  fourierdlem50  46691  fourierdlem52  46693  fourierdlem54  46695  fourierdlem64  46705  fourierdlem65  46706  fourierdlem81  46722  fourierdlem92  46733  fourierdlem102  46743  fourierdlem103  46744  fourierdlem104  46745  fourierdlem113  46754  fourierdlem114  46755  elaa2lem  46768  etransclem4  46773  etransclem10  46779  etransclem14  46783  etransclem15  46784  etransclem23  46792  etransclem24  46793  etransclem31  46800  etransclem32  46801  etransclem35  46804  etransclem44  46813  etransclem46  46815  etransclem48  46817  chnerlem1  47419  chnerlem2  47420  ssnn0ssfz  48932  itcoval1  49246  itcoval2  49247  itcoval3  49248  itcovalsuc  49250  ackvalsuc1mpt  49261  aacllem  50383