Theorem nnex 10903

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 9896	. 2 ⊢ ℂ ∈ V
2		nnsscn 10902	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 4731	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 1977  Vcvv 3173  ℂcc 9813  ℕcn 10897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rrecex 9887  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-nn 10898

This theorem is referenced by:  dfnn2  10910  nn0ex  11175  rpnnen1lem1OLD  11697  rpnnen1lem3OLD  11698  rpnnen1lem4OLD  11699  rpnnen1lem5OLD  11700  nn0ennn  12640  facmapnn  12934  isercolllem2  14244  supcvg  14427  trireciplem  14433  expcnv  14435  geo2lim  14445  qnnen  14781  rpnnen2lem1  14782  rpnnen2lem2  14783  rpnnen  14795  rucALT  14798  prmex  15229  unbenlem  15450  vdwapfval  15513  vdwapf  15514  vdwlem6  15528  vdwlem7  15529  vdwlem8  15530  vdwlem11  15533  prmgaplcm  15602  prmgapprmo  15604  ndxarg  15715  odval  17776  gexval  17816  ablfac1b  18292  pnrmopn  20957  1stcfb  21058  hausmapdom  21113  met1stc  22136  met2ndci  22137  rectbntr0  22443  metcld2  22913  elovolm  23050  elovolmr  23051  ovolmge0  23052  ovolgelb  23055  ovolctb  23065  ovol0  23068  ovolunlem1a  23071  ovolunlem1  23072  ovoliunlem1  23077  ovoliunlem2  23078  ovolshftlem2  23085  ovolicc2  23097  ioombl1  23137  mbfimaopnlem  23228  itg1climres  23287  mbfi1fseqlem6  23293  mbfi1flimlem  23295  mbfmullem2  23297  itg2monolem1  23323  itg2addlem  23331  plyeq0lem  23770  leibpi  24469  dfef2  24497  emcllem4  24525  emcllem6  24527  emcllem7  24528  lgamgulmlem6  24560  lgamcvg2  24581  basellem6  24612  basellem7  24613  basellem8  24614  basellem9  24615  vmaval  24639  sqff1o  24708  0sgmppw  24723  dchrisumlem3  24980  dirith2  25017  iseupa  26492  nmounbseqiALT  27017  nmobndseqiALT  27019  h2hcau  27220  h2hlm  27221  hcau  27425  hlimi  27429  hlimadd  27434  hhcms  27444  isch2  27464  chlimi  27475  hlim0  27476  hhsscms  27520  padct  28885  smatfval  29189  lmdvg  29327  esumfsup  29459  esumpcvgval  29467  esumcvg  29475  sigapildsys  29552  measiun  29608  voliune  29619  omssubadd  29689  carsggect  29707  carsgclctunlem2  29708  eulerpartlems  29749  eulerpartleme  29752  eulerpartlem1  29756  eulerpartlemb  29757  eulerpartlemt  29760  eulerpartgbij  29761  eulerpartlemr  29763  eulerpartlemmf  29764  eulerpartlemgvv  29765  eulerpartlemgf  29768  eulerpartlemgs2  29769  eulerpartlemn  29770  sinccvglem  30820  circum  30822  divcnvlin  30871  faclimlem2  30883  faclim2  30887  colinearex  31337  poimirlem32  32611  voliunnfl  32623  volsupnfl  32624  lmclim2  32724  geomcau  32725  rrncmslem  32801  eldioph3b  36346  lzenom  36351  diophin  36354  diophun  36355  pellexlem3  36413  pellexlem4  36414  pellexlem5  36415  eltrclrec  36991  brtrclrec  37007  iunrelexpmin1  37019  trclrelexplem  37022  dftrcl3  37031  fvtrcllb1d  37033  trclfvcom  37034  cnvtrclfv  37035  cotrcltrcl  37036  trclimalb2  37037  trclfvdecomr  37039  dfrtrcl4  37049  corcltrcl  37050  cotrclrcl  37053  hashnzfzclim  37543  dvradcnv2  37568  binomcxplemcvg  37575  binomcxplemdvsum  37576  binomcxplemnotnn0  37577  ssnnf1octb  38377  clim1fr1  38668  divcnvg  38694  wallispilem5  38962  wallispi  38963  stirlinglem1  38967  stirlinglem8  38974  stirlinglem14  38980  stirlinglem15  38981  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  subsaliuncllem  39251  subsaliuncl  39252  nnfoctbdjlem  39348  nnfoctbdj  39349  ismeannd  39360  voliunsge0lem  39365  caratheodorylem2  39417  isomenndlem  39420  hoicvrrex  39446  ovnsupge0  39447  ovnlecvr  39448  ovn0lem  39455  ovnsubaddlem1  39460  ovnsubadd  39462  sge0hsphoire  39479  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmv1lelem3  39483  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  hoidmvlelem5  39489  hoidmvle  39490  ovnhoilem1  39491  ovnhoilem2  39492  ovnlecvr2  39500  hspmbllem2  39517  ovolval2lem  39533  ovnsubadd2lem  39535  ovolval4lem2  39540  ovolval5lem1  39542  ovolval5lem2  39543  ovnovollem1  39546  ovnovollem2  39547  vonioolem1  39571  smflimlem6  39662  smfresal  39673  nnsgrpmgm  41606  nnsgrp  41607  nnsgrpnmnd  41608