Theorem nnuz 11723

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

Assertion

Ref	Expression
nnuz	|- NN = ( ZZ>= ` 1 )

Proof of Theorem nnuz

Step	Hyp	Ref	Expression
1		nnzrab 11405	. 2 |- NN = { k e. ZZ | 1 <_ k }
2		1z 11407	. . 3 |- 1 e. ZZ
3		uzval 11689	. . 3 |- ( 1 e. ZZ -> ( ZZ>= ` 1 ) = { k e. ZZ | 1 <_ k } )
4	2, 3	ax-mp 5	. 2 |- ( ZZ>= ` 1 ) = { k e. ZZ | 1 <_ k }
5	1, 4	eqtr4i 2647	1 |- NN = ( ZZ>= ` 1 )

Syntax hints:   = wceq 1483   e. wcel 1990   {crab 2916   class class class wbr 4653   ` cfv 5888   1c1 9937   <_ cle 10075   NNcn 11020   ZZcz 11377   ZZ>=cuz 11687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-z 11378  df-uz 11688

This theorem is referenced by:  elnnuz  11724  eluz2nn  11726  uznnssnn  11735  nnwo  11753  eluznn  11758  nninf  11769  fzssnn  12385  fseq1p1m1  12414  prednn  12462  elfzo1  12517  ltwenn  12761  nnnfi  12765  ser1const  12857  expp1  12867  digit1  12998  facnn  13062  fac0  13063  facp1  13065  faclbnd4lem1  13080  bcm1k  13102  bcval5  13105  bcpasc  13108  fz1isolem  13245  seqcoll  13248  seqcoll2  13249  climuni  14283  isercolllem2  14396  isercoll  14398  sumeq2ii  14423  summolem3  14445  summolem2a  14446  fsum  14451  sum0  14452  sumz  14453  fsumcl2lem  14462  fsumadd  14470  fsummulc2  14516  fsumrelem  14539  isumnn0nn  14574  climcndslem1  14581  climcndslem2  14582  climcnds  14583  divcnv  14585  divcnvshft  14587  supcvg  14588  trireciplem  14594  trirecip  14595  expcnv  14596  geo2lim  14606  geoisum1  14610  geoisum1c  14611  mertenslem2  14617  prodeq2ii  14643  prodmolem3  14663  prodmolem2a  14664  fprod  14671  prod0  14673  prod1  14674  fprodss  14678  fprodser  14679  fprodcl2lem  14680  fprodmul  14690  fproddiv  14691  fprodn0  14709  fallfacval4  14774  bpoly4  14790  ege2le3  14820  rpnnen2lem3  14945  rpnnen2lem5  14947  rpnnen2lem8  14950  rpnnen2lem12  14954  ruclem6  14964  pwp1fsum  15114  bezoutlem2  15257  bezoutlem3  15258  lcmcllem  15309  lcmledvds  15312  lcmfval  15334  lcmfcllem  15338  lcmfledvds  15345  isprm3  15396  phicl2  15473  phibndlem  15475  eulerthlem2  15487  odzcllem  15497  odzdvds  15500  iserodd  15540  pcmptcl  15595  pcmpt  15596  pockthlem  15609  pockthg  15610  unbenlem  15612  prmreclem3  15622  prmreclem5  15624  prmreclem6  15625  prmrec  15626  1arith  15631  4sqlem13  15661  4sqlem14  15662  4sqlem17  15665  4sqlem18  15666  vdwlem1  15685  vdwlem2  15686  vdwlem3  15687  vdwlem6  15690  vdwlem8  15692  vdwlem10  15694  vdw  15698  vdwnnlem1  15699  vdwnnlem3  15701  prmlem1a  15813  mulgnnp1  17549  mulgnnsubcl  17553  mulgnn0z  17567  mulgnndir  17569  mulgnndirOLD  17570  mulgpropd  17584  odlem1  17954  odlem2  17958  gexlem1  17994  gexlem2  17997  gexcl3  18002  sylow1lem1  18013  efgsdmi  18145  efgsrel  18147  efgs1b  18149  efgsp1  18150  mulgnn0di  18231  lt6abl  18296  gsumval3eu  18305  gsumval3  18308  gsumzcl2  18311  gsumzaddlem  18321  gsumconst  18334  gsumzmhm  18337  gsumzoppg  18344  zringlpirlem2  19833  zringlpirlem3  19834  lmcnp  21108  lmmo  21184  1stcelcls  21264  1stccnp  21265  1stckgenlem  21356  1stckgen  21357  imasdsf1olem  22178  cphipval  23042  lmnn  23061  cmetcaulem  23086  iscmet2  23092  causs  23096  nglmle  23100  caubl  23106  iscmet3i  23110  bcthlem5  23125  ovolsf  23241  ovollb2lem  23256  ovolctb  23258  ovolunlem1a  23264  ovolunlem1  23265  ovoliunlem1  23270  ovoliun  23273  ovoliun2  23274  ovoliunnul  23275  ovolscalem1  23281  ovolicc1  23284  ovolicc2lem2  23286  ovolicc2lem3  23287  ovolicc2lem4  23288  iundisj  23316  iundisj2  23317  voliunlem1  23318  voliunlem2  23319  voliunlem3  23320  volsup  23324  ioombl1lem4  23329  uniioovol  23347  uniioombllem2  23351  uniioombllem3  23353  uniioombllem4  23354  uniioombllem6  23356  vitalilem4  23380  vitalilem5  23381  itg1climres  23481  mbfi1fseqlem6  23487  mbfi1flimlem  23489  mbfmullem2  23491  itg2monolem1  23517  itg2i1fseqle  23521  itg2i1fseq  23522  itg2i1fseq2  23523  itg2addlem  23525  plyeq0lem  23966  vieta1lem2  24066  elqaalem1  24074  elqaalem3  24076  aaliou3lem4  24101  aaliou3lem7  24104  dvtaylp  24124  taylthlem2  24128  pserdvlem2  24182  pserdv2  24184  abelthlem6  24190  abelthlem9  24194  logtayl  24406  logtaylsum  24407  logtayl2  24408  atantayl  24664  leibpilem2  24668  leibpi  24669  birthdaylem2  24679  dfef2  24697  divsqrtsumlem  24706  emcllem2  24723  emcllem4  24725  emcllem5  24726  emcllem6  24727  emcllem7  24728  harmonicbnd4  24737  fsumharmonic  24738  zetacvg  24741  lgamgulmlem4  24758  lgamgulmlem6  24760  lgamgulm2  24762  lgamcvglem  24766  lgamcvg2  24781  gamcvg  24782  gamcvg2lem  24785  regamcl  24787  relgamcl  24788  lgam1  24790  wilthlem3  24796  ftalem2  24800  ftalem4  24802  ftalem5  24803  basellem5  24811  basellem6  24812  basellem7  24813  basellem8  24814  basellem9  24815  ppiprm  24877  ppinprm  24878  chtprm  24879  chtnprm  24880  chpp1  24881  vma1  24892  ppiltx  24903  fsumvma2  24939  chpchtsum  24944  logfacbnd3  24948  logexprlim  24950  bposlem5  25013  lgscllem  25029  lgsval2lem  25032  lgsval4a  25044  lgsneg  25046  lgsdir  25057  lgsdilem2  25058  lgsdi  25059  lgsne0  25060  gausslemma2dlem3  25093  lgsquadlem2  25106  chebbnd1lem1  25158  chtppilimlem1  25162  rplogsumlem1  25173  rplogsumlem2  25174  rpvmasumlem  25176  dchrisumlema  25177  dchrisumlem2  25179  dchrisumlem3  25180  dchrmusum2  25183  dchrvmasum2lem  25185  dchrvmasumiflem1  25190  dchrvmaeq0  25193  dchrisum0flblem2  25198  dchrisum0flb  25199  dchrisum0re  25202  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0lem2a  25206  dchrisum0lem2  25207  dchrisum0lem3  25208  mudivsum  25219  mulogsum  25221  logdivsum  25222  mulog2sumlem2  25224  log2sumbnd  25233  selberg2lem  25239  logdivbnd  25245  pntrsumo1  25254  pntrsumbnd2  25256  pntrlog2bndlem2  25267  pntrlog2bndlem4  25269  pntrlog2bndlem6a  25271  pntlemf  25294  eedimeq  25778  axlowdimlem6  25827  axlowdimlem16  25837  axlowdimlem17  25838  ipval2  27562  minvecolem3  27732  minvecolem4b  27734  minvecolem4  27736  h2hcau  27836  h2hlm  27837  hlimadd  28050  hlim0  28092  hhsscms  28136  occllem  28162  nlelchi  28920  opsqrlem4  29002  hmopidmchi  29010  iundisjf  29402  iundisj2f  29403  ssnnssfz  29549  iundisjfi  29555  iundisj2fi  29556  1smat1  29870  submat1n  29871  submatres  29872  submateqlem2  29874  lmatfval  29880  madjusmdetlem1  29893  madjusmdetlem2  29894  madjusmdetlem3  29895  madjusmdetlem4  29896  lmlim  29993  rge0scvg  29995  lmxrge0  29998  lmdvg  29999  esumfzf  30131  esumfsup  30132  esumpcvgval  30140  esumpmono  30141  esumcvg  30148  esumcvgsum  30150  esumsup  30151  fiunelros  30237  eulerpartlemsv2  30420  eulerpartlems  30422  eulerpartlemsv3  30423  eulerpartlemv  30426  eulerpartlemb  30430  fiblem  30460  fibp1  30463  rrvsum  30516  dstfrvclim1  30539  ballotlem1ri  30596  signsvfn  30659  chtvalz  30707  circlemethhgt  30721  subfacp1lem1  31161  subfacp1lem5  31166  subfacp1lem6  31167  erdszelem7  31179  cvmliftlem5  31271  cvmliftlem7  31273  cvmliftlem10  31276  cvmliftlem13  31278  sinccvg  31567  circum  31568  divcnvlin  31618  iprodgam  31628  faclimlem1  31629  faclimlem2  31630  faclim  31632  iprodfac  31633  faclim2  31634  poimirlem3  33412  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem12  33421  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem22  33431  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem27  33436  poimirlem28  33437  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  mblfinlem2  33447  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  lmclim2  33554  geomcau  33555  heibor1lem  33608  heibor1  33609  bfplem1  33621  bfplem2  33622  rrncmslem  33631  rrncms  33632  eldioph3b  37328  diophin  37336  diophun  37337  diophren  37377  jm3.1lem2  37585  dgraalem  37715  dgraaub  37718  dftrcl3  38012  trclfvdecomr  38020  hashnzfz2  38520  hashnzfzclim  38521  dvradcnv2  38546  binomcxplemnotnn0  38555  nnsplit  39574  clim1fr1  39833  sumnnodd  39862  limsup10exlem  40004  fprodsubrecnncnvlem  40121  fprodaddrecnncnvlem  40123  stoweidlem7  40224  stoweidlem14  40231  stoweidlem20  40237  stoweidlem34  40251  wallispilem5  40286  wallispi  40287  stirlinglem1  40291  stirlinglem5  40295  stirlinglem7  40297  stirlinglem8  40298  stirlinglem10  40300  stirlinglem11  40301  stirlinglem12  40302  stirlinglem13  40303  stirlinglem14  40304  stirlinglem15  40305  stirlingr  40307  dirkertrigeqlem2  40316  dirkertrigeqlem3  40317  fourierdlem11  40335  fourierdlem31  40355  fourierdlem48  40371  fourierdlem49  40372  fourierdlem69  40392  fourierdlem73  40396  fourierdlem81  40404  fourierdlem93  40416  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  fouriersw  40448  sge0ad2en  40648  voliunsge0lem  40689  caragenunicl  40738  caratheodorylem2  40741  hoidmvlelem3  40811  ovolval2lem  40857  ovolval2  40858  vonioolem2  40895  vonicclem2  40898  fmtno4prmfac  41484