Theorem nnuz 9792

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 9503	. 2 |- NN = { k e. ZZ | 1 <_ k }
2		1z 9505	. . 3 |- 1 e. ZZ
3		uzval 9757	. . 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 2255	1 |- NN = ( ZZ>= ` 1 )

Syntax hints:   = wceq 1397   e. wcel 2202   {crab 2514   class class class wbr 4088   ` cfv 5326   1c1 8033   <_ cle 8215   NNcn 9143   ZZcz 9479   ZZ>=cuz 9755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-cnex 8123  ax-resscn 8124  ax-1cn 8125  ax-1re 8126  ax-icn 8127  ax-addcl 8128  ax-addrcl 8129  ax-mulcl 8130  ax-addcom 8132  ax-addass 8134  ax-distr 8136  ax-i2m1 8137  ax-0lt1 8138  ax-0id 8140  ax-rnegex 8141  ax-cnre 8143  ax-pre-ltirr 8144  ax-pre-ltwlin 8145  ax-pre-lttrn 8146  ax-pre-ltadd 8148

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-br 4089  df-opab 4151  df-mpt 4152  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-iota 5286  df-fun 5328  df-fv 5334  df-riota 5971  df-ov 6021  df-oprab 6022  df-mpo 6023  df-pnf 8216  df-mnf 8217  df-xr 8218  df-ltxr 8219  df-le 8220  df-sub 8352  df-neg 8353  df-inn 9144  df-z 9480  df-uz 9756

This theorem is referenced by:  elnnuz  9793  eluz2nn  9800  uznnssnn  9811  eluznn  9834  fzssnn  10303  fseq1p1m1  10329  fz01or  10346  nnsplit  10372  elfzo1  10431  nninfdcex  10498  exp3vallem  10803  exp3val  10804  facnn  10990  fac0  10991  bcm1k  11023  bcval5  11026  bcpasc  11029  seq3coll  11107  recvguniq  11573  resqrexlemf  11585  climuni  11871  climrecvg1n  11926  climcvg1nlem  11927  summodclem3  11959  summodclem2a  11960  fsum3  11966  sum0  11967  isumz  11968  fsumcl2lem  11977  fsumadd  11985  fsummulc2  12027  isumnn0nn  12072  divcnv  12076  trireciplem  12079  trirecip  12080  expcnvap0  12081  expcnv  12083  geo2lim  12095  geoisum1  12098  geoisum1c  12099  cvgratnnlemnexp  12103  cvgratnnlemseq  12105  cvgratnnlemrate  12109  cvgratnn  12110  mertenslem2  12115  prodmodclem3  12154  prodmodclem2a  12155  fprodseq  12162  prod0  12164  prod1dc  12165  fprodssdc  12169  fprodmul  12170  ege2le3  12250  gcdsupex  12546  gcdsupcl  12547  nnmindc  12623  nnminle  12624  lcmval  12653  lcmcllem  12657  lcmledvds  12660  isprm3  12708  phicl2  12804  phibndlem  12806  odzcllem  12833  odzdvds  12836  pcmptcl  12933  pcmpt  12934  pockthlem  12947  pockthg  12948  1arith  12958  4sqlem13m  12994  4sqlem14  12995  4sqlem17  12998  4sqlem18  12999  ennnfonelemjn  13041  ssnnctlemct  13085  nninfdclemf  13088  nninfdclemp1  13089  mulgval  13727  mulgfng  13729  mulgnnp1  13735  mulgnnsubcl  13739  mulgnn0z  13754  mulgnndir  13756  mulgpropdg  13769  lmtopcnp  14993  lgsval  15752  lgscllem  15755  lgsval2lem  15758  lgsval4a  15770  lgsneg  15772  lgsdir  15783  lgsdilem2  15784  lgsdi  15785  lgsne0  15786  gausslemma2dlem3  15811  lgseisenlem4  15821  lgsquadlem2  15826  cvgcmp2nlemabs  16687  cvgcmp2n  16688  trilpolemcl  16692  trilpolemisumle  16693  trilpolemgt1  16694  trilpolemeq1  16695  trilpolemlt1  16696  nconstwlpolem0  16719  nconstwlpolemgt0  16720  gfsump1  16738