Theorem nnex 11631

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 10607	. 2 ⊢ ℂ ∈ V
2		nnsscn 11630	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5190	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2111  Vcvv 3441  ℂcc 10524  ℕcn 11625

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-1cn 10584  ax-addcl 10586

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-om 7561  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-nn 11626

This theorem is referenced by:  dfnn2  11638  nn0ex  11891  nn0ennn  13342  facmapnn  13641  isercolllem2  15014  supcvg  15203  trireciplem  15209  expcnv  15211  geo2lim  15223  qnnen  15558  rpnnen2lem1  15559  rpnnen2lem2  15560  rpnnen  15572  rucALT  15575  prmex  16011  unbenlem  16234  vdwapfval  16297  vdwapf  16298  vdwlem6  16312  vdwlem7  16313  vdwlem8  16314  vdwlem11  16317  prmgaplcm  16386  prmgapprmo  16388  ndxarg  16500  odfval  18652  odval  18654  gexval  18695  pnrmopn  21948  1stcfb  22050  hausmapdom  22105  met1stc  23128  met2ndci  23129  rectbntr0  23437  metcld2  23911  elovolmlem  24078  ovolctb  24094  ovol0  24097  mbfimaopnlem  24259  itg1climres  24318  mbfi1fseqlem6  24324  mbfi1flimlem  24326  mbfmullem2  24328  itg2monolem1  24354  itg2addlem  24362  plyeq0lem  24807  leibpi  25528  dfef2  25556  emcllem4  25584  emcllem6  25586  emcllem7  25587  lgamgulmlem6  25619  lgamcvg2  25640  basellem6  25671  basellem7  25672  basellem8  25673  basellem9  25674  dchrisumlem3  26075  dirith2  26112  nmounbseqiALT  28561  nmobndseqiALT  28563  h2hcau  28762  h2hlm  28763  hcau  28967  hlimi  28971  hlimadd  28976  hhcms  28986  isch2  29006  chlimi  29017  hlim0  29018  hhsscms  29061  padct  30481  smatfval  31148  lmdvg  31306  esumfsup  31439  esumpcvgval  31447  esumcvg  31455  sigapildsys  31531  measiun  31587  voliune  31598  omssubadd  31668  carsggect  31686  carsgclctunlem2  31687  eulerpartlems  31728  eulerpartleme  31731  eulerpartlem1  31735  eulerpartlemb  31736  eulerpartlemt  31739  eulerpartgbij  31740  eulerpartlemr  31742  eulerpartlemmf  31743  eulerpartlemgvv  31744  eulerpartlemgf  31747  eulerpartlemgs2  31748  eulerpartlemn  31749  reprval  31991  repr0  31992  reprsuc  31996  reprss  31998  reprinrn  31999  reprlt  32000  hashreprin  32001  reprinfz1  32003  reprpmtf1o  32007  reprdifc  32008  breprexplemb  32012  breprexpnat  32015  vtsval  32018  circlemethnat  32022  circlevma  32023  circlemethhgt  32024  sinccvglem  33028  circum  33030  divcnvlin  33077  faclimlem2  33089  faclim2  33093  colinearex  33634  bj-ndxarg  34492  poimirlem32  35089  voliunnfl  35101  volsupnfl  35102  lmclim2  35196  geomcau  35197  rrncmslem  35270  eldioph3b  39706  lzenom  39711  diophin  39713  diophun  39714  pellexlem3  39772  pellexlem4  39773  pellexlem5  39774  eltrclrec  40381  brtrclrec  40397  iunrelexpmin1  40409  trclrelexplem  40412  dftrcl3  40421  fvtrcllb1d  40423  trclfvcom  40424  cnvtrclfv  40425  cotrcltrcl  40426  trclimalb2  40427  trclfvdecomr  40429  dfrtrcl4  40439  corcltrcl  40440  cotrclrcl  40443  hashnzfzclim  41026  dvradcnv2  41051  binomcxplemcvg  41058  binomcxplemdvsum  41059  binomcxplemnotnn0  41060  ssnnf1octb  41822  clim1fr1  42243  divcnvg  42269  limsup10ex  42415  liminf10ex  42416  wallispilem5  42711  wallispi  42712  stirlinglem1  42716  stirlinglem8  42723  stirlinglem14  42729  stirlinglem15  42730  fourierdlem103  42851  fourierdlem104  42852  fourierdlem112  42860  subsaliuncllem  42997  subsaliuncl  42998  nnfoctbdjlem  43094  nnfoctbdj  43095  ismeannd  43106  voliunsge0lem  43111  caratheodorylem2  43166  isomenndlem  43169  hoicvrrex  43195  ovnsupge0  43196  ovnlecvr  43197  ovn0lem  43204  ovnsubaddlem1  43209  ovnsubadd  43211  sge0hsphoire  43228  hoidmv1lelem1  43230  hoidmv1lelem2  43231  hoidmv1lelem3  43232  hoidmv1le  43233  hoidmvlelem1  43234  hoidmvlelem2  43235  hoidmvlelem3  43236  hoidmvlelem4  43237  hoidmvlelem5  43238  hoidmvle  43239  ovnhoilem1  43240  ovnhoilem2  43241  ovnlecvr2  43249  hspmbllem2  43266  ovolval2lem  43282  ovnsubadd2lem  43284  ovolval4lem2  43289  ovolval5lem1  43291  ovolval5lem2  43292  ovnovollem1  43295  ovnovollem2  43296  vonioolem1  43319  smflimlem6  43409  smfresal  43420  nnsgrpmgm  44436  nnsgrp  44437  nnsgrpnmnd  44438