Theorem nnex 11979

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 10952	. 2 ⊢ ℂ ∈ V
2		nnsscn 11978	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5246	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3432  ℂcc 10869  ℕcn 11973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-1cn 10929  ax-addcl 10931

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-om 7713  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-nn 11974

This theorem is referenced by:  dfnn2  11986  nn0ex  12239  nn0ennn  13699  facmapnn  13999  isercolllem2  15377  supcvg  15568  trireciplem  15574  expcnv  15576  geo2lim  15587  qnnen  15922  rpnnen2lem1  15923  rpnnen2lem2  15924  rpnnen  15936  rucALT  15939  prmex  16382  unbenlem  16609  vdwapfval  16672  vdwapf  16673  vdwlem6  16687  vdwlem7  16688  vdwlem8  16689  vdwlem11  16692  prmgaplcm  16761  prmgapprmo  16763  ndxarg  16897  odfval  19140  odval  19142  gexval  19183  pnrmopn  22494  1stcfb  22596  hausmapdom  22651  met1stc  23677  met2ndci  23678  rectbntr0  23995  metcld2  24471  elovolmlem  24638  ovolctb  24654  ovol0  24657  mbfimaopnlem  24819  itg1climres  24879  mbfi1fseqlem6  24885  mbfi1flimlem  24887  mbfmullem2  24889  itg2monolem1  24915  itg2addlem  24923  plyeq0lem  25371  leibpi  26092  dfef2  26120  emcllem4  26148  emcllem6  26150  emcllem7  26151  lgamgulmlem6  26183  lgamcvg2  26204  basellem6  26235  basellem7  26236  basellem8  26237  basellem9  26238  dchrisumlem3  26639  dirith2  26676  nmounbseqiALT  29140  nmobndseqiALT  29142  h2hcau  29341  h2hlm  29342  hcau  29546  hlimi  29550  hlimadd  29555  hhcms  29565  isch2  29585  chlimi  29596  hlim0  29597  hhsscms  29640  padct  31054  smatfval  31745  lmdvg  31903  esumfsup  32038  esumpcvgval  32046  esumcvg  32054  sigapildsys  32130  measiun  32186  voliune  32197  omssubadd  32267  carsggect  32285  carsgclctunlem2  32286  eulerpartlems  32327  eulerpartleme  32330  eulerpartlem1  32334  eulerpartlemb  32335  eulerpartlemt  32338  eulerpartgbij  32339  eulerpartlemr  32341  eulerpartlemmf  32342  eulerpartlemgvv  32343  eulerpartlemgf  32346  eulerpartlemgs2  32347  eulerpartlemn  32348  reprval  32590  repr0  32591  reprsuc  32595  reprss  32597  reprinrn  32598  reprlt  32599  hashreprin  32600  reprinfz1  32602  reprpmtf1o  32606  reprdifc  32607  breprexplemb  32611  breprexpnat  32614  vtsval  32617  circlemethnat  32621  circlevma  32622  circlemethhgt  32623  sinccvglem  33630  circum  33632  divcnvlin  33698  faclimlem2  33710  faclim2  33714  colinearex  34362  bj-ndxarg  35248  poimirlem32  35809  voliunnfl  35821  volsupnfl  35822  lmclim2  35916  geomcau  35917  rrncmslem  35990  eldioph3b  40587  lzenom  40592  diophin  40594  diophun  40595  pellexlem3  40653  pellexlem4  40654  pellexlem5  40655  eltrclrec  41288  brtrclrec  41304  iunrelexpmin1  41316  trclrelexplem  41319  dftrcl3  41328  fvtrcllb1d  41330  trclfvcom  41331  cnvtrclfv  41332  cotrcltrcl  41333  trclimalb2  41334  trclfvdecomr  41336  dfrtrcl4  41346  corcltrcl  41347  cotrclrcl  41350  hashnzfzclim  41940  dvradcnv2  41965  binomcxplemcvg  41972  binomcxplemdvsum  41973  binomcxplemnotnn0  41974  ssnnf1octb  42733  clim1fr1  43142  divcnvg  43168  limsup10ex  43314  liminf10ex  43315  wallispilem5  43610  wallispi  43611  stirlinglem1  43615  stirlinglem8  43622  stirlinglem14  43628  stirlinglem15  43629  fourierdlem103  43750  fourierdlem104  43751  fourierdlem112  43759  subsaliuncllem  43896  subsaliuncl  43897  nnfoctbdjlem  43993  nnfoctbdj  43994  ismeannd  44005  voliunsge0lem  44010  caratheodorylem2  44065  isomenndlem  44068  hoicvrrex  44094  ovnsupge0  44095  ovnlecvr  44096  ovn0lem  44103  ovnsubaddlem1  44108  ovnsubadd  44110  sge0hsphoire  44127  hoidmv1lelem1  44129  hoidmv1lelem2  44130  hoidmv1lelem3  44131  hoidmv1le  44132  hoidmvlelem1  44133  hoidmvlelem2  44134  hoidmvlelem3  44135  hoidmvlelem4  44136  hoidmvlelem5  44137  hoidmvle  44138  ovnhoilem1  44139  ovnhoilem2  44140  ovnlecvr2  44148  hspmbllem2  44165  ovolval2lem  44181  ovnsubadd2lem  44183  ovolval4lem2  44188  ovolval5lem1  44190  ovolval5lem2  44191  ovnovollem1  44194  ovnovollem2  44195  vonioolem1  44218  smflimlem6  44311  smfresal  44322  nnsgrpmgm  45370  nnsgrp  45371  nnsgrpnmnd  45372