Theorem nnex 12163

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 11119	. 2 ⊢ ℂ ∈ V
2		nnsscn 12162	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5269	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3442  ℂcc 11036  ℕcn 12157

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-nn 12158

This theorem is referenced by:  dfnn2  12170  nn0ex  12419  nn0ennn  13914  facmapnn  14220  isercolllem2  15601  supcvg  15791  trireciplem  15797  expcnv  15799  geo2lim  15810  qnnen  16150  rpnnen2lem1  16151  rpnnen2lem2  16152  rpnnen  16164  rucALT  16167  prmex  16616  unbenlem  16848  vdwapfval  16911  vdwapf  16912  vdwlem6  16926  vdwlem7  16927  vdwlem8  16928  vdwlem11  16931  prmgaplcm  17000  prmgapprmo  17002  ndxarg  17135  ex-chn2  18573  odfval  19473  odval  19475  gexval  19519  pnrmopn  23299  1stcfb  23401  hausmapdom  23456  met1stc  24477  met2ndci  24478  rectbntr0  24789  metcld2  25275  elovolmlem  25443  ovolctb  25459  ovol0  25462  mbfimaopnlem  25624  itg1climres  25683  mbfi1fseqlem6  25689  mbfi1flimlem  25691  mbfmullem2  25693  itg2monolem1  25719  itg2addlem  25727  plyeq0lem  26183  leibpi  26920  dfef2  26949  emcllem4  26977  emcllem6  26979  emcllem7  26980  lgamgulmlem6  27012  lgamcvg2  27033  basellem6  27064  basellem7  27065  basellem8  27066  basellem9  27067  dchrisumlem3  27470  dirith2  27507  nmounbseqiALT  30866  nmobndseqiALT  30868  h2hcau  31067  h2hlm  31068  hcau  31272  hlimi  31276  hlimadd  31281  hhcms  31291  isch2  31311  chlimi  31322  hlim0  31323  hhsscms  31366  padct  32808  smatfval  33973  lmdvg  34131  esumfsup  34248  esumpcvgval  34256  esumcvg  34264  sigapildsys  34340  measiun  34396  voliune  34407  omssubadd  34478  carsggect  34496  carsgclctunlem2  34497  eulerpartlems  34538  eulerpartleme  34541  eulerpartlem1  34545  eulerpartlemb  34546  eulerpartlemt  34549  eulerpartgbij  34550  eulerpartlemr  34552  eulerpartlemmf  34553  eulerpartlemgvv  34554  eulerpartlemgf  34557  eulerpartlemgs2  34558  eulerpartlemn  34559  reprval  34788  repr0  34789  reprsuc  34793  reprss  34795  reprinrn  34796  reprlt  34797  hashreprin  34798  reprinfz1  34800  reprpmtf1o  34804  reprdifc  34805  breprexplemb  34809  breprexpnat  34812  vtsval  34815  circlemethnat  34819  circlevma  34820  circlemethhgt  34821  sinccvglem  35888  circum  35890  divcnvlin  35949  faclimlem2  35960  faclim2  35964  colinearex  36276  bj-ndxarg  37330  poimirlem32  37903  voliunnfl  37915  volsupnfl  37916  lmclim2  38009  geomcau  38010  rrncmslem  38083  fisdomnn  42614  eldioph3b  43122  lzenom  43127  diophin  43129  diophun  43130  pellexlem3  43188  pellexlem4  43189  pellexlem5  43190  eltrclrec  44036  brtrclrec  44052  iunrelexpmin1  44064  trclrelexplem  44067  dftrcl3  44076  fvtrcllb1d  44078  trclfvcom  44079  cnvtrclfv  44080  cotrcltrcl  44081  trclimalb2  44082  trclfvdecomr  44084  dfrtrcl4  44094  corcltrcl  44095  cotrclrcl  44098  hashnzfzclim  44678  dvradcnv2  44703  binomcxplemcvg  44710  binomcxplemdvsum  44711  binomcxplemnotnn0  44712  ssnnf1octb  45553  clim1fr1  45961  divcnvg  45987  limsup10ex  46131  liminf10ex  46132  wallispilem5  46427  wallispi  46428  stirlinglem1  46432  stirlinglem8  46439  stirlinglem14  46445  stirlinglem15  46446  fourierdlem103  46567  fourierdlem104  46568  fourierdlem112  46576  subsaliuncllem  46715  subsaliuncl  46716  nnfoctbdjlem  46813  nnfoctbdj  46814  ismeannd  46825  voliunsge0lem  46830  caratheodorylem2  46885  isomenndlem  46888  hoicvrrex  46914  ovnsupge0  46915  ovnlecvr  46916  ovn0lem  46923  ovnsubaddlem1  46928  ovnsubadd  46930  sge0hsphoire  46947  hoidmv1lelem1  46949  hoidmv1lelem2  46950  hoidmv1lelem3  46951  hoidmv1le  46952  hoidmvlelem1  46953  hoidmvlelem2  46954  hoidmvlelem3  46955  hoidmvlelem4  46956  hoidmvlelem5  46957  hoidmvle  46958  ovnhoilem1  46959  ovnhoilem2  46960  ovnlecvr2  46968  hspmbllem2  46985  ovolval2lem  47001  ovnsubadd2lem  47003  ovolval4lem2  47008  ovolval5lem1  47010  ovolval5lem2  47011  ovnovollem1  47014  ovnovollem2  47015  vonioolem1  47038  smflimlem6  47134  smfresal  47146  fsupdm  47200  smfsupdmmbllem  47202  finfdm  47204  smfinfdmmbllem  47206  nthrucw  47244  nnsgrpmgm  48536  nnsgrp  48537  nnsgrpnmnd  48538