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

Theorem nn0uz 11719
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 11403 . 2 0 = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘}
2 0z 11385 . . 3 0 ∈ ℤ
3 uzval 11686 . . 3 (0 ∈ ℤ → (ℤ‘0) = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘})
42, 3ax-mp 5 . 2 (ℤ‘0) = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘}
51, 4eqtr4i 2646 1 0 = (ℤ‘0)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1482  wcel 1989  {crab 2915   class class class wbr 4651  cfv 5886  0cc0 9933  cle 10072  0cn0 11289  cz 11374  cuz 11684
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-cnex 9989  ax-resscn 9990  ax-1cn 9991  ax-icn 9992  ax-addcl 9993  ax-addrcl 9994  ax-mulcl 9995  ax-mulrcl 9996  ax-mulcom 9997  ax-addass 9998  ax-mulass 9999  ax-distr 10000  ax-i2m1 10001  ax-1ne0 10002  ax-1rid 10003  ax-rnegex 10004  ax-rrecex 10005  ax-cnre 10006  ax-pre-lttri 10007  ax-pre-lttrn 10008  ax-pre-ltadd 10009  ax-pre-mulgt0 10010
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-nel 2897  df-ral 2916  df-rex 2917  df-reu 2918  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-om 7063  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-er 7739  df-en 7953  df-dom 7954  df-sdom 7955  df-pnf 10073  df-mnf 10074  df-xr 10075  df-ltxr 10076  df-le 10077  df-sub 10265  df-neg 10266  df-nn 11018  df-n0 11290  df-z 11375  df-uz 11685
This theorem is referenced by:  elnn0uz  11722  2eluzge0  11730  eluznn0  11754  nn0inf  11767  fseq1p1m1  12410  fznn0sub2  12442  nn0split  12450  prednn0  12459  fzossnn0  12495  fzennn  12762  hashgf1o  12765  exple1  12915  faclbnd4lem1  13075  bcval5  13100  bcpasc  13103  hashfzo0  13212  hashf1  13236  ccatval2  13357  ccatass  13366  ccatrn  13367  swrdccat1  13451  swrdccat2  13452  wrdeqs1cat  13468  cats1un  13469  splfv2a  13501  splval2  13502  revccat  13509  cats1fv  13598  binom1dif  14559  isumnn0nn  14568  climcndslem1  14575  climcnds  14577  harmonic  14585  arisum2  14587  explecnv  14591  geoser  14593  geolim  14595  geolim2  14596  geomulcvg  14601  geoisum  14602  geoisumr  14603  mertenslem1  14610  mertenslem2  14611  mertens  14612  fallfacfwd  14761  0fallfac  14762  binomfallfaclem2  14765  bpolylem  14773  bpolysum  14778  bpolydiflem  14779  fsumkthpow  14781  bpoly2  14782  bpoly3  14783  bpoly4  14784  efcllem  14802  ef0lem  14803  eff  14806  efcvg  14809  efcvgfsum  14810  reefcl  14811  ege2le3  14814  efcj  14816  eftlcvg  14830  eftlub  14833  effsumlt  14835  ef4p  14837  efgt1p2  14838  efgt1p  14839  eflegeo  14845  eirrlem  14926  ruclem6  14958  ruclem7  14959  divalglem2  15112  divalglem5  15114  bitsfzolem  15150  bitsfzo  15151  bitsfi  15153  bitsinv1lem  15157  bitsinv1  15158  bitsinvp1  15165  sadcf  15169  sadcp1  15171  sadadd  15183  sadass  15187  bitsres  15189  smupf  15194  smupp1  15196  smuval2  15198  smupval  15204  smueqlem  15206  smumul  15209  alginv  15282  algcvg  15283  algcvga  15286  algfx  15287  eucalgcvga  15293  eucalg  15294  phiprmpw  15475  prmdiv  15484  iserodd  15534  pcfac  15597  prmreclem2  15615  prmreclem4  15617  vdwapun  15672  vdwlem1  15679  ramcl2lem  15707  ramtcl  15708  ramtub  15710  gsumwsubmcl  17369  gsumws1  17370  gsumccat  17372  gsumwmhm  17376  psgnunilem2  17909  psgnunilem4  17911  sylow1lem1  18007  efginvrel2  18134  efgredleme  18150  efgredlemc  18152  efgcpbllemb  18162  frgpuplem  18179  telgsumfz0s  18382  telgsums  18384  pgpfaclem1  18474  psrbaglefi  19366  ltbwe  19466  pmatcollpw3fi1lem1  20585  chfacfisf  20653  chfacfisfcpmat  20654  iscmet3lem3  23082  dyadmax  23360  mbfi1fseqlem3  23478  itgcnlem  23550  dvnff  23680  dvnp1  23682  dvn2bss  23687  cpncn  23693  dveflem  23736  ig1peu  23925  ig1pdvds  23930  ply1termlem  23953  plyeq0lem  23960  plyaddlem1  23963  plymullem1  23964  coeeulem  23974  dgrcl  23983  dgrub  23984  dgrlb  23986  coeid3  23990  plyco  23991  coeeq2  23992  coefv0  23998  coemulhi  24004  coemulc  24005  dvply1  24033  vieta1lem2  24060  vieta1  24061  elqaalem2  24069  elqaalem3  24070  geolim3  24088  dvntaylp  24119  taylthlem1  24121  radcnvlem1  24161  radcnvlem2  24162  radcnvlem3  24163  radcnv0  24164  radcnvlt2  24167  dvradcnv  24169  pserulm  24170  psercn2  24171  pserdvlem2  24176  pserdv2  24178  abelthlem4  24182  abelthlem5  24183  abelthlem6  24184  abelthlem7  24186  abelthlem8  24187  abelthlem9  24188  advlogexp  24395  logtayllem  24399  logtayl  24400  cxpeq  24492  leibpi  24663  leibpisum  24664  log2cnv  24665  log2tlbnd  24666  log2ublem2  24668  birthdaylem3  24674  wilthlem2  24789  ftalem1  24793  ftalem5  24797  basellem2  24802  basellem3  24803  basellem5  24805  musum  24911  0sgmppw  24917  1sgmprm  24918  chtublem  24930  logexprlim  24944  lgseisenlem1  25094  lgsquadlem2  25100  dchrisumlem1  25172  dchrisumlem2  25173  dchrisum0flblem1  25191  ostth2lem3  25318  tgcgr4  25420  eupth2lems  27091  fz2ssnn0  29532  oddpwdc  30401  eulerpartlemb  30415  sseqfn  30437  sseqf  30439  signsplypnf  30612  signstcl  30627  signstf  30628  signstfvn  30631  signstfvneq0  30634  fsum2dsub  30670  reprsuc  30678  breprexplema  30693  breprexplemc  30695  subfacval2  31154  subfaclim  31155  cvmliftlem7  31258  fwddifnp1  32256  knoppcnlem6  32472  knoppcnlem8  32474  knoppcnlem9  32475  knoppcnlem11  32477  knoppcn  32478  knoppndvlem4  32490  knoppndvlem6  32492  knoppf  32510  poimirlem3  33392  poimirlem4  33393  poimirlem18  33407  poimirlem21  33410  poimirlem22  33411  poimirlem25  33414  poimirlem26  33415  poimirlem27  33416  heiborlem4  33593  heiborlem6  33595  mapfzcons  37105  irrapxlem1  37212  ltrmynn0  37341  ltrmxnn0  37342  acongeq  37376  jm2.23  37389  jm2.26lem3  37394  dfrtrcl3  37851  radcnvrat  38339  bcc0  38365  dvradcnv2  38372  binomcxplemnn0  38374  binomcxplemrat  38375  binomcxplemradcnv  38377  binomcxplemnotnn0  38381  fzssnn0  39352  expfac  39695  dvnmptdivc  39922  dvnmul  39927  dvnprodlem3  39932  stoweidlem17  40003  stoweidlem34  40020  stirlinglem5  40064  stirlinglem7  40066  fourierdlem15  40108  fourierdlem25  40118  fourierdlem48  40140  fourierdlem49  40141  fourierdlem50  40142  fourierdlem52  40144  fourierdlem54  40146  fourierdlem64  40156  fourierdlem65  40157  fourierdlem81  40173  fourierdlem92  40184  fourierdlem102  40194  fourierdlem103  40195  fourierdlem104  40196  fourierdlem113  40205  fourierdlem114  40206  elaa2lem  40219  etransclem4  40224  etransclem10  40230  etransclem14  40234  etransclem15  40235  etransclem23  40243  etransclem24  40244  etransclem31  40251  etransclem32  40252  etransclem35  40255  etransclem44  40264  etransclem46  40266  etransclem48  40268  pwdif  41272  ssnn0ssfz  41898  aacllem  42318
  Copyright terms: Public domain W3C validator