Theorem nnuz 9974

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

Assertion

Ref	Expression
nnuz	⊢ ℕ = (ℤ≥‘1)

Proof of Theorem nnuz

Step	Hyp	Ref	Expression
1		nnzrab 9679	. 2 ⊢ ℕ = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘}
2		1z 9681	. . 3 ⊢ 1 ∈ ℤ
3		uzval 9939	. . 3 ⊢ (1 ∈ ℤ → (ℤ≥‘1) = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘})
4	2, 3	ax-mp 5	. 2 ⊢ (ℤ≥‘1) = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘}
5	1, 4	eqtr4i 2262	1 ⊢ ℕ = (ℤ≥‘1)

This proof depends on syntax axioms:   = wceq 1402   ∈ wcel 2209  {crab 2532   class class class wbr 4131  ‘cfv 5380  1c1 8186   ≤ cle 8367  ℕcn 9313  ℤcz 9655  ℤ_≥cuz 9937

This proof depends on 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 4251  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-setind 4686  ax-cnex 8276  ax-resscn 8277  ax-1cn 8278  ax-1re 8279  ax-icn 8280  ax-addcl 8281  ax-addrcl 8282  ax-mulcl 8283  ax-addcom 8285  ax-addass 8287  ax-distr 8289  ax-i2m1 8290  ax-0lt1 8291  ax-0id 8293  ax-rnegex 8294  ax-cnre 8296  ax-pre-ltirr 8297  ax-pre-ltwlin 8298  ax-pre-lttrn 8299  ax-pre-ltadd 8301

This proof 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 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-br 4132  df-opab 4194  df-mpt 4195  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-iota 5340  df-fun 5382  df-fv 5388  df-riota 6041  df-ov 6091  df-oprab 6092  df-mpo 6093  df-pnf 8368  df-mnf 8369  df-xr 8370  df-ltxr 8371  df-le 8372  df-sub 8506  df-neg 8507  df-inn 9314  df-z 9656  df-uz 9938

This theorem is used by:  elnnuz  9975  eluz2nn  9982  uznnssnn  9993  eluznn  10016  fzssnn  10491  fseq1p1m1  10518  fz01or  10535  nnsplit  10561  elfzo1  10620  nninfdcex  10689  exp3vallem  10998  exp3val  10999  facnn  11187  fac0  11188  bcm1k  11220  bcval5  11223  bcpasc  11226  seq3coll  11316  recvguniq  11783  resqrexlemf  11795  climuni  12084  climrecvg1n  12139  climcvg1nlem  12140  summodclem3  12172  summodclem2a  12173  fsum3  12179  sum0  12180  isumz  12181  fsumcl2lem  12190  fsumadd  12198  fsummulc2  12240  isumnn0nn  12285  divcnv  12289  trireciplem  12292  trirecip  12293  expcnvap0  12294  expcnv  12296  geo2lim  12308  geoisum1  12311  geoisum1c  12312  cvgratnnlemnexp  12316  cvgratnnlemseq  12318  cvgratnnlemrate  12322  cvgratnn  12323  mertenslem2  12328  prodmodclem3  12367  prodmodclem2a  12368  fprodseq  12375  prod0  12377  prod1dc  12378  fprodssdc  12382  fprodmul  12383  ege2le3  12463  gcdsupex  12759  gcdsupcl  12760  nnmindc  12836  nnminle  12837  lcmval  12866  lcmcllem  12870  lcmledvds  12873  isprm3  12921  phicl2  13021  phibndlem  13023  odzcllem  13050  odzdvds  13053  pcmptcl  13150  pcmpt  13151  pockthlem  13164  pockthg  13165  1arith  13175  4sqlem13m  13211  4sqlem14  13212  4sqlem17  13215  4sqlem18  13216  prmlem1a  13250  ballotfilem2  13286  ballotfilem1ri  13336  ennnfonelemjn  13351  ssnnctlemct  13395  nninfdclemf  13398  nninfdclemp1  13399  mulgval  13984  mulgfng  13986  mulgnnp1  13992  mulgnnsubcl  13996  mulgnn0z  14011  mulgnndir  14013  mulgpropdg  14026  gsump1  14247  lmtopcnp  15476  birthdaylem2  16226  ppiprm  16259  ppinprm  16260  chtprm  16261  chtnprm  16262  bposlem5  16315  lgsval  16328  lgscllem  16331  lgsval2lem  16334  lgsval4a  16346  lgsneg  16348  lgsdir  16359  lgsdilem2  16360  lgsdi  16361  lgsne0  16362  gausslemma2dlem3  16387  lgseisenlem4  16397  lgsquadlem2  16402  cvgcmp2nlemabs  17287  cvgcmp2n  17288  trilpolemcl  17293  trilpolemisumle  17294  trilpolemgt1  17295  trilpolemeq1  17296  trilpolemlt1  17297  nconstwlpolem0  17320  nconstwlpolemgt0  17321