Theorem nnex 12151

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 11107	. 2 ⊢ ℂ ∈ V
2		nnsscn 12150	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5267	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2113  Vcvv 3440  ℂcc 11024  ℕcn 12145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-1cn 11084  ax-addcl 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-nn 12146

This theorem is referenced by:  dfnn2  12158  nn0ex  12407  nn0ennn  13902  facmapnn  14208  isercolllem2  15589  supcvg  15779  trireciplem  15785  expcnv  15787  geo2lim  15798  qnnen  16138  rpnnen2lem1  16139  rpnnen2lem2  16140  rpnnen  16152  rucALT  16155  prmex  16604  unbenlem  16836  vdwapfval  16899  vdwapf  16900  vdwlem6  16914  vdwlem7  16915  vdwlem8  16916  vdwlem11  16919  prmgaplcm  16988  prmgapprmo  16990  ndxarg  17123  ex-chn2  18561  odfval  19461  odval  19463  gexval  19507  pnrmopn  23287  1stcfb  23389  hausmapdom  23444  met1stc  24465  met2ndci  24466  rectbntr0  24777  metcld2  25263  elovolmlem  25431  ovolctb  25447  ovol0  25450  mbfimaopnlem  25612  itg1climres  25671  mbfi1fseqlem6  25677  mbfi1flimlem  25679  mbfmullem2  25681  itg2monolem1  25707  itg2addlem  25715  plyeq0lem  26171  leibpi  26908  dfef2  26937  emcllem4  26965  emcllem6  26967  emcllem7  26968  lgamgulmlem6  27000  lgamcvg2  27021  basellem6  27052  basellem7  27053  basellem8  27054  basellem9  27055  dchrisumlem3  27458  dirith2  27495  nmounbseqiALT  30853  nmobndseqiALT  30855  h2hcau  31054  h2hlm  31055  hcau  31259  hlimi  31263  hlimadd  31268  hhcms  31278  isch2  31298  chlimi  31309  hlim0  31310  hhsscms  31353  padct  32797  smatfval  33952  lmdvg  34110  esumfsup  34227  esumpcvgval  34235  esumcvg  34243  sigapildsys  34319  measiun  34375  voliune  34386  omssubadd  34457  carsggect  34475  carsgclctunlem2  34476  eulerpartlems  34517  eulerpartleme  34520  eulerpartlem1  34524  eulerpartlemb  34525  eulerpartlemt  34528  eulerpartgbij  34529  eulerpartlemr  34531  eulerpartlemmf  34532  eulerpartlemgvv  34533  eulerpartlemgf  34536  eulerpartlemgs2  34537  eulerpartlemn  34538  reprval  34767  repr0  34768  reprsuc  34772  reprss  34774  reprinrn  34775  reprlt  34776  hashreprin  34777  reprinfz1  34779  reprpmtf1o  34783  reprdifc  34784  breprexplemb  34788  breprexpnat  34791  vtsval  34794  circlemethnat  34798  circlevma  34799  circlemethhgt  34800  sinccvglem  35866  circum  35868  divcnvlin  35927  faclimlem2  35938  faclim2  35942  colinearex  36254  bj-ndxarg  37282  poimirlem32  37853  voliunnfl  37865  volsupnfl  37866  lmclim2  37959  geomcau  37960  rrncmslem  38033  fisdomnn  42499  eldioph3b  43007  lzenom  43012  diophin  43014  diophun  43015  pellexlem3  43073  pellexlem4  43074  pellexlem5  43075  eltrclrec  43921  brtrclrec  43937  iunrelexpmin1  43949  trclrelexplem  43952  dftrcl3  43961  fvtrcllb1d  43963  trclfvcom  43964  cnvtrclfv  43965  cotrcltrcl  43966  trclimalb2  43967  trclfvdecomr  43969  dfrtrcl4  43979  corcltrcl  43980  cotrclrcl  43983  hashnzfzclim  44563  dvradcnv2  44588  binomcxplemcvg  44595  binomcxplemdvsum  44596  binomcxplemnotnn0  44597  ssnnf1octb  45438  clim1fr1  45847  divcnvg  45873  limsup10ex  46017  liminf10ex  46018  wallispilem5  46313  wallispi  46314  stirlinglem1  46318  stirlinglem8  46325  stirlinglem14  46331  stirlinglem15  46332  fourierdlem103  46453  fourierdlem104  46454  fourierdlem112  46462  subsaliuncllem  46601  subsaliuncl  46602  nnfoctbdjlem  46699  nnfoctbdj  46700  ismeannd  46711  voliunsge0lem  46716  caratheodorylem2  46771  isomenndlem  46774  hoicvrrex  46800  ovnsupge0  46801  ovnlecvr  46802  ovn0lem  46809  ovnsubaddlem1  46814  ovnsubadd  46816  sge0hsphoire  46833  hoidmv1lelem1  46835  hoidmv1lelem2  46836  hoidmv1lelem3  46837  hoidmv1le  46838  hoidmvlelem1  46839  hoidmvlelem2  46840  hoidmvlelem3  46841  hoidmvlelem4  46842  hoidmvlelem5  46843  hoidmvle  46844  ovnhoilem1  46845  ovnhoilem2  46846  ovnlecvr2  46854  hspmbllem2  46871  ovolval2lem  46887  ovnsubadd2lem  46889  ovolval4lem2  46894  ovolval5lem1  46896  ovolval5lem2  46897  ovnovollem1  46900  ovnovollem2  46901  vonioolem1  46924  smflimlem6  47020  smfresal  47032  fsupdm  47086  smfsupdmmbllem  47088  finfdm  47090  smfinfdmmbllem  47092  nthrucw  47130  nnsgrpmgm  48422  nnsgrp  48423  nnsgrpnmnd  48424