Theorem nnex 12220

Description: The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.)

Assertion

Ref	Expression
nnex	⊢ ℕ ∈ V

Proof of Theorem nnex

Step	Hyp	Ref	Expression
1		cnex 11193	. 2 ⊢ ℂ ∈ V
2		nnsscn 12219	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5322	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3474  ℂcc 11110  ℕcn 12214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-1cn 11170  ax-addcl 11172

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7414  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-nn 12215

This theorem is referenced by:  dfnn2  12227  nn0ex  12480  nn0ennn  13946  facmapnn  14247  isercolllem2  15614  supcvg  15804  trireciplem  15810  expcnv  15812  geo2lim  15823  qnnen  16158  rpnnen2lem1  16159  rpnnen2lem2  16160  rpnnen  16172  rucALT  16175  prmex  16616  unbenlem  16843  vdwapfval  16906  vdwapf  16907  vdwlem6  16921  vdwlem7  16922  vdwlem8  16923  vdwlem11  16926  prmgaplcm  16995  prmgapprmo  16997  ndxarg  17131  odfval  19402  odval  19404  gexval  19448  pnrmopn  22854  1stcfb  22956  hausmapdom  23011  met1stc  24037  met2ndci  24038  rectbntr0  24355  metcld2  24831  elovolmlem  24998  ovolctb  25014  ovol0  25017  mbfimaopnlem  25179  itg1climres  25239  mbfi1fseqlem6  25245  mbfi1flimlem  25247  mbfmullem2  25249  itg2monolem1  25275  itg2addlem  25283  plyeq0lem  25731  leibpi  26454  dfef2  26482  emcllem4  26510  emcllem6  26512  emcllem7  26513  lgamgulmlem6  26545  lgamcvg2  26566  basellem6  26597  basellem7  26598  basellem8  26599  basellem9  26600  dchrisumlem3  27001  dirith2  27038  nmounbseqiALT  30069  nmobndseqiALT  30071  h2hcau  30270  h2hlm  30271  hcau  30475  hlimi  30479  hlimadd  30484  hhcms  30494  isch2  30514  chlimi  30525  hlim0  30526  hhsscms  30569  padct  31982  smatfval  32844  lmdvg  33002  esumfsup  33137  esumpcvgval  33145  esumcvg  33153  sigapildsys  33229  measiun  33285  voliune  33296  omssubadd  33368  carsggect  33386  carsgclctunlem2  33387  eulerpartlems  33428  eulerpartleme  33431  eulerpartlem1  33435  eulerpartlemb  33436  eulerpartlemt  33439  eulerpartgbij  33440  eulerpartlemr  33442  eulerpartlemmf  33443  eulerpartlemgvv  33444  eulerpartlemgf  33447  eulerpartlemgs2  33448  eulerpartlemn  33449  reprval  33691  repr0  33692  reprsuc  33696  reprss  33698  reprinrn  33699  reprlt  33700  hashreprin  33701  reprinfz1  33703  reprpmtf1o  33707  reprdifc  33708  breprexplemb  33712  breprexpnat  33715  vtsval  33718  circlemethnat  33722  circlevma  33723  circlemethhgt  33724  sinccvglem  34726  circum  34728  divcnvlin  34777  faclimlem2  34789  faclim2  34793  colinearex  35107  bj-ndxarg  36050  poimirlem32  36612  voliunnfl  36624  volsupnfl  36625  lmclim2  36718  geomcau  36719  rrncmslem  36792  eldioph3b  41591  lzenom  41596  diophin  41598  diophun  41599  pellexlem3  41657  pellexlem4  41658  pellexlem5  41659  eltrclrec  42519  brtrclrec  42535  iunrelexpmin1  42547  trclrelexplem  42550  dftrcl3  42559  fvtrcllb1d  42561  trclfvcom  42562  cnvtrclfv  42563  cotrcltrcl  42564  trclimalb2  42565  trclfvdecomr  42567  dfrtrcl4  42577  corcltrcl  42578  cotrclrcl  42581  hashnzfzclim  43169  dvradcnv2  43194  binomcxplemcvg  43201  binomcxplemdvsum  43202  binomcxplemnotnn0  43203  ssnnf1octb  43978  clim1fr1  44402  divcnvg  44428  limsup10ex  44574  liminf10ex  44575  wallispilem5  44870  wallispi  44871  stirlinglem1  44875  stirlinglem8  44882  stirlinglem14  44888  stirlinglem15  44889  fourierdlem103  45010  fourierdlem104  45011  fourierdlem112  45019  subsaliuncllem  45158  subsaliuncl  45159  nnfoctbdjlem  45256  nnfoctbdj  45257  ismeannd  45268  voliunsge0lem  45273  caratheodorylem2  45328  isomenndlem  45331  hoicvrrex  45357  ovnsupge0  45358  ovnlecvr  45359  ovn0lem  45366  ovnsubaddlem1  45371  ovnsubadd  45373  sge0hsphoire  45390  hoidmv1lelem1  45392  hoidmv1lelem2  45393  hoidmv1lelem3  45394  hoidmv1le  45395  hoidmvlelem1  45396  hoidmvlelem2  45397  hoidmvlelem3  45398  hoidmvlelem4  45399  hoidmvlelem5  45400  hoidmvle  45401  ovnhoilem1  45402  ovnhoilem2  45403  ovnlecvr2  45411  hspmbllem2  45428  ovolval2lem  45444  ovnsubadd2lem  45446  ovolval4lem2  45451  ovolval5lem1  45453  ovolval5lem2  45454  ovnovollem1  45457  ovnovollem2  45458  vonioolem1  45481  smflimlem6  45577  smfresal  45589  fsupdm  45643  smfsupdmmbllem  45645  finfdm  45647  smfinfdmmbllem  45649  nnsgrpmgm  46671  nnsgrp  46672  nnsgrpnmnd  46673