Theorem nnuz 9940

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 9650	. 2 |- NN = { k e. ZZ | 1 <_ k }
2		1z 9652	. . 3 |- 1 e. ZZ
3		uzval 9905	. . 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 2262	1 |- NN = ( ZZ>= ` 1 )

Syntax hints:   = wceq 1402   e. wcel 2209   {crab 2532   class class class wbr 4128   ` cfv 5375   1c1 8173   <_ cle 8354   NNcn 9286   ZZcz 9626   ZZ>=cuz 9903

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 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4247  ax-pow 4309  ax-pr 4344  ax-un 4576  ax-setind 4682  ax-cnex 8263  ax-resscn 8264  ax-1cn 8265  ax-1re 8266  ax-icn 8267  ax-addcl 8268  ax-addrcl 8269  ax-mulcl 8270  ax-addcom 8272  ax-addass 8274  ax-distr 8276  ax-i2m1 8277  ax-0lt1 8278  ax-0id 8280  ax-rnegex 8281  ax-cnre 8283  ax-pre-ltirr 8284  ax-pre-ltwlin 8285  ax-pre-lttrn 8286  ax-pre-ltadd 8288

This theorem depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-int 3969  df-br 4129  df-opab 4191  df-mpt 4192  df-id 4436  df-xp 4778  df-rel 4779  df-cnv 4780  df-co 4781  df-dm 4782  df-iota 5335  df-fun 5377  df-fv 5383  df-riota 6031  df-ov 6081  df-oprab 6082  df-mpo 6083  df-pnf 8355  df-mnf 8356  df-xr 8357  df-ltxr 8358  df-le 8359  df-sub 8492  df-neg 8493  df-inn 9287  df-z 9627  df-uz 9904

This theorem is referenced by:  elnnuz  9941  eluz2nn  9948  uznnssnn  9959  eluznn  9982  fzssnn  10455  fseq1p1m1  10482  fz01or  10499  nnsplit  10525  elfzo1  10584  nninfdcex  10653  exp3vallem  10958  exp3val  10959  facnn  11146  fac0  11147  bcm1k  11179  bcval5  11182  bcpasc  11185  seq3coll  11275  recvguniq  11742  resqrexlemf  11754  climuni  12040  climrecvg1n  12095  climcvg1nlem  12096  summodclem3  12128  summodclem2a  12129  fsum3  12135  sum0  12136  isumz  12137  fsumcl2lem  12146  fsumadd  12154  fsummulc2  12196  isumnn0nn  12241  divcnv  12245  trireciplem  12248  trirecip  12249  expcnvap0  12250  expcnv  12252  geo2lim  12264  geoisum1  12267  geoisum1c  12268  cvgratnnlemnexp  12272  cvgratnnlemseq  12274  cvgratnnlemrate  12278  cvgratnn  12279  mertenslem2  12284  prodmodclem3  12323  prodmodclem2a  12324  fprodseq  12331  prod0  12333  prod1dc  12334  fprodssdc  12338  fprodmul  12339  ege2le3  12419  gcdsupex  12715  gcdsupcl  12716  nnmindc  12792  nnminle  12793  lcmval  12822  lcmcllem  12826  lcmledvds  12829  isprm3  12877  phicl2  12973  phibndlem  12975  odzcllem  13002  odzdvds  13005  pcmptcl  13102  pcmpt  13103  pockthlem  13116  pockthg  13117  1arith  13127  4sqlem13m  13163  4sqlem14  13164  4sqlem17  13167  4sqlem18  13168  ballotfilem2  13209  ballotfilem1ri  13259  ennnfonelemjn  13274  ssnnctlemct  13318  nninfdclemf  13321  nninfdclemp1  13322  mulgval  13905  mulgfng  13907  mulgnnp1  13913  mulgnnsubcl  13917  mulgnn0z  13932  mulgnndir  13934  mulgpropdg  13947  gsump1  14137  lmtopcnp  15277  lgsval  16040  lgscllem  16043  lgsval2lem  16046  lgsval4a  16058  lgsneg  16060  lgsdir  16071  lgsdilem2  16072  lgsdi  16073  lgsne0  16074  gausslemma2dlem3  16099  lgseisenlem4  16109  lgsquadlem2  16114  cvgcmp2nlemabs  16989  cvgcmp2n  16990  trilpolemcl  16994  trilpolemisumle  16995  trilpolemgt1  16996  trilpolemeq1  16997  trilpolemlt1  16998  nconstwlpolem0  17021  nconstwlpolemgt0  17022