Theorem nnuz 9792

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 9503	. 2 ⊢ ℕ = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘}
2		1z 9505	. . 3 ⊢ 1 ∈ ℤ
3		uzval 9757	. . 3 ⊢ (1 ∈ ℤ → (ℤ≥‘1) = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘})
4	2, 3	ax-mp 5	. 2 ⊢ (ℤ≥‘1) = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘}
5	1, 4	eqtr4i 2255	1 ⊢ ℕ = (ℤ≥‘1)

Syntax hints:   = wceq 1397   ∈ wcel 2202  {crab 2514   class class class wbr 4088  ‘cfv 5326  1c1 8033   ≤ cle 8215  ℕcn 9143  ℤcz 9479  ℤ_≥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  11560  resqrexlemf  11572  climuni  11858  climrecvg1n  11913  climcvg1nlem  11914  summodclem3  11946  summodclem2a  11947  fsum3  11953  sum0  11954  isumz  11955  fsumcl2lem  11964  fsumadd  11972  fsummulc2  12014  isumnn0nn  12059  divcnv  12063  trireciplem  12066  trirecip  12067  expcnvap0  12068  expcnv  12070  geo2lim  12082  geoisum1  12085  geoisum1c  12086  cvgratnnlemnexp  12090  cvgratnnlemseq  12092  cvgratnnlemrate  12096  cvgratnn  12097  mertenslem2  12102  prodmodclem3  12141  prodmodclem2a  12142  fprodseq  12149  prod0  12151  prod1dc  12152  fprodssdc  12156  fprodmul  12157  ege2le3  12237  gcdsupex  12533  gcdsupcl  12534  nnmindc  12610  nnminle  12611  lcmval  12640  lcmcllem  12644  lcmledvds  12647  isprm3  12695  phicl2  12791  phibndlem  12793  odzcllem  12820  odzdvds  12823  pcmptcl  12920  pcmpt  12921  pockthlem  12934  pockthg  12935  1arith  12945  4sqlem13m  12981  4sqlem14  12982  4sqlem17  12985  4sqlem18  12986  ennnfonelemjn  13028  ssnnctlemct  13072  nninfdclemf  13075  nninfdclemp1  13076  mulgval  13714  mulgfng  13716  mulgnnp1  13722  mulgnnsubcl  13726  mulgnn0z  13741  mulgnndir  13743  mulgpropdg  13756  lmtopcnp  14980  lgsval  15739  lgscllem  15742  lgsval2lem  15745  lgsval4a  15757  lgsneg  15759  lgsdir  15770  lgsdilem2  15771  lgsdi  15772  lgsne0  15773  gausslemma2dlem3  15798  lgseisenlem4  15808  lgsquadlem2  15813  cvgcmp2nlemabs  16662  cvgcmp2n  16663  trilpolemcl  16667  trilpolemisumle  16668  trilpolemgt1  16669  trilpolemeq1  16670  trilpolemlt1  16671  nconstwlpolem0  16694  nconstwlpolemgt0  16695  gfsump1  16713