Theorem nnex 12272

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 11236	. 2 ⊢ ℂ ∈ V
2		nnsscn 12271	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5322	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3480  ℂcc 11153  ℕcn 12266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-1cn 11213  ax-addcl 11215

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-nn 12267

This theorem is referenced by:  dfnn2  12279  nn0ex  12532  nn0ennn  14020  facmapnn  14324  isercolllem2  15702  supcvg  15892  trireciplem  15898  expcnv  15900  geo2lim  15911  qnnen  16249  rpnnen2lem1  16250  rpnnen2lem2  16251  rpnnen  16263  rucALT  16266  prmex  16714  unbenlem  16946  vdwapfval  17009  vdwapf  17010  vdwlem6  17024  vdwlem7  17025  vdwlem8  17026  vdwlem11  17029  prmgaplcm  17098  prmgapprmo  17100  ndxarg  17233  odfval  19550  odval  19552  gexval  19596  pnrmopn  23351  1stcfb  23453  hausmapdom  23508  met1stc  24534  met2ndci  24535  rectbntr0  24854  metcld2  25341  elovolmlem  25509  ovolctb  25525  ovol0  25528  mbfimaopnlem  25690  itg1climres  25749  mbfi1fseqlem6  25755  mbfi1flimlem  25757  mbfmullem2  25759  itg2monolem1  25785  itg2addlem  25793  plyeq0lem  26249  leibpi  26985  dfef2  27014  emcllem4  27042  emcllem6  27044  emcllem7  27045  lgamgulmlem6  27077  lgamcvg2  27098  basellem6  27129  basellem7  27130  basellem8  27131  basellem9  27132  dchrisumlem3  27535  dirith2  27572  nmounbseqiALT  30797  nmobndseqiALT  30799  h2hcau  30998  h2hlm  30999  hcau  31203  hlimi  31207  hlimadd  31212  hhcms  31222  isch2  31242  chlimi  31253  hlim0  31254  hhsscms  31297  padct  32731  smatfval  33794  lmdvg  33952  esumfsup  34071  esumpcvgval  34079  esumcvg  34087  sigapildsys  34163  measiun  34219  voliune  34230  omssubadd  34302  carsggect  34320  carsgclctunlem2  34321  eulerpartlems  34362  eulerpartleme  34365  eulerpartlem1  34369  eulerpartlemb  34370  eulerpartlemt  34373  eulerpartgbij  34374  eulerpartlemr  34376  eulerpartlemmf  34377  eulerpartlemgvv  34378  eulerpartlemgf  34381  eulerpartlemgs2  34382  eulerpartlemn  34383  reprval  34625  repr0  34626  reprsuc  34630  reprss  34632  reprinrn  34633  reprlt  34634  hashreprin  34635  reprinfz1  34637  reprpmtf1o  34641  reprdifc  34642  breprexplemb  34646  breprexpnat  34649  vtsval  34652  circlemethnat  34656  circlevma  34657  circlemethhgt  34658  sinccvglem  35677  circum  35679  divcnvlin  35733  faclimlem2  35744  faclim2  35748  colinearex  36061  bj-ndxarg  37078  poimirlem32  37659  voliunnfl  37671  volsupnfl  37672  lmclim2  37765  geomcau  37766  rrncmslem  37839  fisdomnn  42285  eldioph3b  42776  lzenom  42781  diophin  42783  diophun  42784  pellexlem3  42842  pellexlem4  42843  pellexlem5  42844  eltrclrec  43693  brtrclrec  43709  iunrelexpmin1  43721  trclrelexplem  43724  dftrcl3  43733  fvtrcllb1d  43735  trclfvcom  43736  cnvtrclfv  43737  cotrcltrcl  43738  trclimalb2  43739  trclfvdecomr  43741  dfrtrcl4  43751  corcltrcl  43752  cotrclrcl  43755  hashnzfzclim  44341  dvradcnv2  44366  binomcxplemcvg  44373  binomcxplemdvsum  44374  binomcxplemnotnn0  44375  ssnnf1octb  45199  clim1fr1  45616  divcnvg  45642  limsup10ex  45788  liminf10ex  45789  wallispilem5  46084  wallispi  46085  stirlinglem1  46089  stirlinglem8  46096  stirlinglem14  46102  stirlinglem15  46103  fourierdlem103  46224  fourierdlem104  46225  fourierdlem112  46233  subsaliuncllem  46372  subsaliuncl  46373  nnfoctbdjlem  46470  nnfoctbdj  46471  ismeannd  46482  voliunsge0lem  46487  caratheodorylem2  46542  isomenndlem  46545  hoicvrrex  46571  ovnsupge0  46572  ovnlecvr  46573  ovn0lem  46580  ovnsubaddlem1  46585  ovnsubadd  46587  sge0hsphoire  46604  hoidmv1lelem1  46606  hoidmv1lelem2  46607  hoidmv1lelem3  46608  hoidmv1le  46609  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  hoidmvlelem5  46614  hoidmvle  46615  ovnhoilem1  46616  ovnhoilem2  46617  ovnlecvr2  46625  hspmbllem2  46642  ovolval2lem  46658  ovnsubadd2lem  46660  ovolval4lem2  46665  ovolval5lem1  46667  ovolval5lem2  46668  ovnovollem1  46671  ovnovollem2  46672  vonioolem1  46695  smflimlem6  46791  smfresal  46803  fsupdm  46857  smfsupdmmbllem  46859  finfdm  46861  smfinfdmmbllem  46863  nnsgrpmgm  48092  nnsgrp  48093  nnsgrpnmnd  48094