Theorem nnex 12238

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 11202	. 2 ⊢ ℂ ∈ V
2		nnsscn 12237	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5289	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2107  Vcvv 3457  ℂcc 11119  ℕcn 12232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5263  ax-nul 5273  ax-pr 5399  ax-un 7723  ax-cnex 11177  ax-1cn 11179  ax-addcl 11181

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-reu 3358  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-pss 3944  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-iun 4966  df-br 5117  df-opab 5179  df-mpt 5199  df-tr 5227  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6287  df-ord 6352  df-on 6353  df-lim 6354  df-suc 6355  df-iota 6480  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-ov 7402  df-om 7856  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8379  df-rdg 8418  df-nn 12233

This theorem is referenced by:  dfnn2  12245  nn0ex  12499  nn0ennn  13986  facmapnn  14291  isercolllem2  15669  supcvg  15859  trireciplem  15865  expcnv  15867  geo2lim  15878  qnnen  16216  rpnnen2lem1  16217  rpnnen2lem2  16218  rpnnen  16230  rucALT  16233  prmex  16681  unbenlem  16913  vdwapfval  16976  vdwapf  16977  vdwlem6  16991  vdwlem7  16992  vdwlem8  16993  vdwlem11  16996  prmgaplcm  17065  prmgapprmo  17067  ndxarg  17200  odfval  19498  odval  19500  gexval  19544  pnrmopn  23266  1stcfb  23368  hausmapdom  23423  met1stc  24445  met2ndci  24446  rectbntr0  24757  metcld2  25244  elovolmlem  25412  ovolctb  25428  ovol0  25431  mbfimaopnlem  25593  itg1climres  25652  mbfi1fseqlem6  25658  mbfi1flimlem  25660  mbfmullem2  25662  itg2monolem1  25688  itg2addlem  25696  plyeq0lem  26152  leibpi  26888  dfef2  26917  emcllem4  26945  emcllem6  26947  emcllem7  26948  lgamgulmlem6  26980  lgamcvg2  27001  basellem6  27032  basellem7  27033  basellem8  27034  basellem9  27035  dchrisumlem3  27438  dirith2  27475  nmounbseqiALT  30691  nmobndseqiALT  30693  h2hcau  30892  h2hlm  30893  hcau  31097  hlimi  31101  hlimadd  31106  hhcms  31116  isch2  31136  chlimi  31147  hlim0  31148  hhsscms  31191  padct  32632  smatfval  33734  lmdvg  33892  esumfsup  34009  esumpcvgval  34017  esumcvg  34025  sigapildsys  34101  measiun  34157  voliune  34168  omssubadd  34240  carsggect  34258  carsgclctunlem2  34259  eulerpartlems  34300  eulerpartleme  34303  eulerpartlem1  34307  eulerpartlemb  34308  eulerpartlemt  34311  eulerpartgbij  34312  eulerpartlemr  34314  eulerpartlemmf  34315  eulerpartlemgvv  34316  eulerpartlemgf  34319  eulerpartlemgs2  34320  eulerpartlemn  34321  reprval  34563  repr0  34564  reprsuc  34568  reprss  34570  reprinrn  34571  reprlt  34572  hashreprin  34573  reprinfz1  34575  reprpmtf1o  34579  reprdifc  34580  breprexplemb  34584  breprexpnat  34587  vtsval  34590  circlemethnat  34594  circlevma  34595  circlemethhgt  34596  sinccvglem  35615  circum  35617  divcnvlin  35671  faclimlem2  35682  faclim2  35686  colinearex  35999  bj-ndxarg  37016  poimirlem32  37597  voliunnfl  37609  volsupnfl  37610  lmclim2  37703  geomcau  37704  rrncmslem  37777  fisdomnn  42218  eldioph3b  42713  lzenom  42718  diophin  42720  diophun  42721  pellexlem3  42779  pellexlem4  42780  pellexlem5  42781  eltrclrec  43629  brtrclrec  43645  iunrelexpmin1  43657  trclrelexplem  43660  dftrcl3  43669  fvtrcllb1d  43671  trclfvcom  43672  cnvtrclfv  43673  cotrcltrcl  43674  trclimalb2  43675  trclfvdecomr  43677  dfrtrcl4  43687  corcltrcl  43688  cotrclrcl  43691  hashnzfzclim  44272  dvradcnv2  44297  binomcxplemcvg  44304  binomcxplemdvsum  44305  binomcxplemnotnn0  44306  ssnnf1octb  45145  clim1fr1  45560  divcnvg  45586  limsup10ex  45732  liminf10ex  45733  wallispilem5  46028  wallispi  46029  stirlinglem1  46033  stirlinglem8  46040  stirlinglem14  46046  stirlinglem15  46047  fourierdlem103  46168  fourierdlem104  46169  fourierdlem112  46177  subsaliuncllem  46316  subsaliuncl  46317  nnfoctbdjlem  46414  nnfoctbdj  46415  ismeannd  46426  voliunsge0lem  46431  caratheodorylem2  46486  isomenndlem  46489  hoicvrrex  46515  ovnsupge0  46516  ovnlecvr  46517  ovn0lem  46524  ovnsubaddlem1  46529  ovnsubadd  46531  sge0hsphoire  46548  hoidmv1lelem1  46550  hoidmv1lelem2  46551  hoidmv1lelem3  46552  hoidmv1le  46553  hoidmvlelem1  46554  hoidmvlelem2  46555  hoidmvlelem3  46556  hoidmvlelem4  46557  hoidmvlelem5  46558  hoidmvle  46559  ovnhoilem1  46560  ovnhoilem2  46561  ovnlecvr2  46569  hspmbllem2  46586  ovolval2lem  46602  ovnsubadd2lem  46604  ovolval4lem2  46609  ovolval5lem1  46611  ovolval5lem2  46612  ovnovollem1  46615  ovnovollem2  46616  vonioolem1  46639  smflimlem6  46735  smfresal  46747  fsupdm  46801  smfsupdmmbllem  46803  finfdm  46805  smfinfdmmbllem  46807  nnsgrpmgm  48037  nnsgrp  48038  nnsgrpnmnd  48039