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

Theorem nn0uz 11915
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
StepHypRef Expression
1 nn0zrab 11598 . 2 0 = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘}
2 0z 11580 . . 3 0 ∈ ℤ
3 uzval 11881 . . 3 (0 ∈ ℤ → (ℤ‘0) = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘})
42, 3ax-mp 5 . 2 (ℤ‘0) = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘}
51, 4eqtr4i 2785 1 0 = (ℤ‘0)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  wcel 2139  {crab 3054   class class class wbr 4804  cfv 6049  0cc0 10128  cle 10267  0cn0 11484  cz 11569  cuz 11879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-nn 11213  df-n0 11485  df-z 11570  df-uz 11880
This theorem is referenced by:  elnn0uz  11918  2eluzge0  11926  eluznn0  11950  nn0inf  11963  fseq1p1m1  12607  fznn0sub2  12640  nn0split  12648  prednn0  12657  fzossnn0  12693  fzennn  12961  hashgf1o  12964  exple1  13114  faclbnd4lem1  13274  bcval5  13299  bcpasc  13302  hashfzo0  13409  hashf1  13433  ccatval2  13550  ccatass  13560  ccatrn  13561  swrdccat1  13657  swrdccat2  13658  wrdeqs1cat  13674  cats1un  13675  splfv2a  13707  splval2  13708  revccat  13715  cats1fv  13804  binom1dif  14764  isumnn0nn  14773  climcndslem1  14780  climcnds  14782  harmonic  14790  arisum2  14792  explecnv  14796  geoser  14798  geolim  14800  geolim2  14801  geomulcvg  14806  geoisum  14807  geoisumr  14808  mertenslem1  14815  mertenslem2  14816  mertens  14817  fallfacfwd  14966  0fallfac  14967  binomfallfaclem2  14970  bpolylem  14978  bpolysum  14983  bpolydiflem  14984  fsumkthpow  14986  bpoly2  14987  bpoly3  14988  bpoly4  14989  efcllem  15007  ef0lem  15008  eff  15011  efcvg  15014  efcvgfsum  15015  reefcl  15016  ege2le3  15019  efcj  15021  eftlcvg  15035  eftlub  15038  effsumlt  15040  ef4p  15042  efgt1p2  15043  efgt1p  15044  eflegeo  15050  eirrlem  15131  ruclem6  15163  ruclem7  15164  divalglem2  15320  divalglem5  15322  bitsfzolem  15358  bitsfzo  15359  bitsfi  15361  bitsinv1lem  15365  bitsinv1  15366  bitsinvp1  15373  sadcf  15377  sadcp1  15379  sadadd  15391  sadass  15395  bitsres  15397  smupf  15402  smupp1  15404  smuval2  15406  smupval  15412  smueqlem  15414  smumul  15417  alginv  15490  algcvg  15491  algcvga  15494  algfx  15495  eucalgcvga  15501  eucalg  15502  phiprmpw  15683  prmdiv  15692  iserodd  15742  pcfac  15805  prmreclem2  15823  prmreclem4  15825  vdwapun  15880  vdwlem1  15887  ramcl2lem  15915  ramtcl  15916  ramtub  15918  gsumwsubmcl  17576  gsumws1  17577  gsumccat  17579  gsumwmhm  17583  psgnunilem2  18115  psgnunilem4  18117  sylow1lem1  18213  efginvrel2  18340  efgredleme  18356  efgredlemc  18358  efgcpbllemb  18368  frgpuplem  18385  telgsumfz0s  18588  telgsums  18590  pgpfaclem1  18680  psrbaglefi  19574  ltbwe  19674  pmatcollpw3fi1lem1  20793  chfacfisf  20861  chfacfisfcpmat  20862  iscmet3lem3  23288  dyadmax  23566  mbfi1fseqlem3  23683  itgcnlem  23755  dvnff  23885  dvnp1  23887  dvn2bss  23892  cpncn  23898  dveflem  23941  ig1peu  24130  ig1pdvds  24135  ply1termlem  24158  plyeq0lem  24165  plyaddlem1  24168  plymullem1  24169  coeeulem  24179  dgrcl  24188  dgrub  24189  dgrlb  24191  coeid3  24195  plyco  24196  coeeq2  24197  coefv0  24203  coemulhi  24209  coemulc  24210  dvply1  24238  vieta1lem2  24265  vieta1  24266  elqaalem2  24274  elqaalem3  24275  geolim3  24293  dvntaylp  24324  taylthlem1  24326  radcnvlem1  24366  radcnvlem2  24367  radcnvlem3  24368  radcnv0  24369  radcnvlt2  24372  dvradcnv  24374  pserulm  24375  psercn2  24376  pserdvlem2  24381  pserdv2  24383  abelthlem4  24387  abelthlem5  24388  abelthlem6  24389  abelthlem7  24391  abelthlem8  24392  abelthlem9  24393  advlogexp  24600  logtayllem  24604  logtayl  24605  cxpeq  24697  leibpi  24868  leibpisum  24869  log2cnv  24870  log2tlbnd  24871  log2ublem2  24873  birthdaylem3  24879  wilthlem2  24994  ftalem1  24998  ftalem5  25002  basellem2  25007  basellem3  25008  basellem5  25010  musum  25116  0sgmppw  25122  1sgmprm  25123  chtublem  25135  logexprlim  25149  lgseisenlem1  25299  lgsquadlem2  25305  dchrisumlem1  25377  dchrisumlem2  25378  dchrisum0flblem1  25396  ostth2lem3  25523  tgcgr4  25625  clwwlknonex2lem1  27256  eupth2lems  27390  fz2ssnn0  29856  oddpwdc  30725  eulerpartlemb  30739  sseqfn  30761  sseqf  30763  signsplypnf  30936  signstcl  30951  signstf  30952  signstfvn  30955  signstfvneq0  30958  fsum2dsub  30994  reprsuc  31002  breprexplema  31017  breprexplemc  31019  subfacval2  31476  subfaclim  31477  cvmliftlem7  31580  fwddifnp1  32578  knoppcnlem6  32794  knoppcnlem8  32796  knoppcnlem9  32797  knoppcnlem11  32799  knoppcn  32800  knoppndvlem4  32812  knoppndvlem6  32814  knoppf  32832  poimirlem3  33725  poimirlem4  33726  poimirlem18  33740  poimirlem21  33743  poimirlem22  33744  poimirlem25  33747  poimirlem26  33748  poimirlem27  33749  heiborlem4  33926  heiborlem6  33928  mapfzcons  37781  irrapxlem1  37888  ltrmynn0  38017  ltrmxnn0  38018  acongeq  38052  jm2.23  38065  jm2.26lem3  38070  dfrtrcl3  38527  radcnvrat  39015  bcc0  39041  dvradcnv2  39048  binomcxplemnn0  39050  binomcxplemrat  39051  binomcxplemradcnv  39053  binomcxplemnotnn0  39057  fzssnn0  40031  expfac  40392  dvnmptdivc  40656  dvnmul  40661  dvnprodlem3  40666  stoweidlem17  40737  stoweidlem34  40754  stirlinglem5  40798  stirlinglem7  40800  fourierdlem15  40842  fourierdlem25  40852  fourierdlem48  40874  fourierdlem49  40875  fourierdlem50  40876  fourierdlem52  40878  fourierdlem54  40880  fourierdlem64  40890  fourierdlem65  40891  fourierdlem81  40907  fourierdlem92  40918  fourierdlem102  40928  fourierdlem103  40929  fourierdlem104  40930  fourierdlem113  40939  fourierdlem114  40940  elaa2lem  40953  etransclem4  40958  etransclem10  40964  etransclem14  40968  etransclem15  40969  etransclem23  40977  etransclem24  40978  etransclem31  40985  etransclem32  40986  etransclem35  40989  etransclem44  40998  etransclem46  41000  etransclem48  41002  pwdif  42011  ssnn0ssfz  42637  aacllem  43060
  Copyright terms: Public domain W3C validator