Theorem nnex 11638

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 10612	. 2 ⊢ ℂ ∈ V
2		nnsscn 11637	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5218	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2110  Vcvv 3494  ℂcc 10529  ℕcn 11632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-cnex 10587  ax-1cn 10589  ax-addcl 10591

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7153  df-om 7575  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-nn 11633

This theorem is referenced by:  dfnn2  11645  nn0ex  11897  nn0ennn  13341  facmapnn  13639  isercolllem2  15016  supcvg  15205  trireciplem  15211  expcnv  15213  geo2lim  15225  qnnen  15560  rpnnen2lem1  15561  rpnnen2lem2  15562  rpnnen  15574  rucALT  15577  prmex  16015  unbenlem  16238  vdwapfval  16301  vdwapf  16302  vdwlem6  16316  vdwlem7  16317  vdwlem8  16318  vdwlem11  16321  prmgaplcm  16390  prmgapprmo  16392  ndxarg  16502  odfval  18654  odval  18656  gexval  18697  pnrmopn  21945  1stcfb  22047  hausmapdom  22102  met1stc  23125  met2ndci  23126  rectbntr0  23434  metcld2  23904  elovolmlem  24069  ovolctb  24085  ovol0  24088  mbfimaopnlem  24250  itg1climres  24309  mbfi1fseqlem6  24315  mbfi1flimlem  24317  mbfmullem2  24319  itg2monolem1  24345  itg2addlem  24353  plyeq0lem  24794  leibpi  25514  dfef2  25542  emcllem4  25570  emcllem6  25572  emcllem7  25573  lgamgulmlem6  25605  lgamcvg2  25626  basellem6  25657  basellem7  25658  basellem8  25659  basellem9  25660  dchrisumlem3  26061  dirith2  26098  nmounbseqiALT  28549  nmobndseqiALT  28551  h2hcau  28750  h2hlm  28751  hcau  28955  hlimi  28959  hlimadd  28964  hhcms  28974  isch2  28994  chlimi  29005  hlim0  29006  hhsscms  29049  padct  30449  smatfval  31055  lmdvg  31191  esumfsup  31324  esumpcvgval  31332  esumcvg  31340  sigapildsys  31416  measiun  31472  voliune  31483  omssubadd  31553  carsggect  31571  carsgclctunlem2  31572  eulerpartlems  31613  eulerpartleme  31616  eulerpartlem1  31620  eulerpartlemb  31621  eulerpartlemt  31624  eulerpartgbij  31625  eulerpartlemr  31627  eulerpartlemmf  31628  eulerpartlemgvv  31629  eulerpartlemgf  31632  eulerpartlemgs2  31633  eulerpartlemn  31634  reprval  31876  repr0  31877  reprsuc  31881  reprss  31883  reprinrn  31884  reprlt  31885  hashreprin  31886  reprinfz1  31888  reprpmtf1o  31892  reprdifc  31893  breprexplemb  31897  breprexpnat  31900  vtsval  31903  circlemethnat  31907  circlevma  31908  circlemethhgt  31909  sinccvglem  32910  circum  32912  divcnvlin  32959  faclimlem2  32971  faclim2  32975  colinearex  33516  bj-ndxarg  34362  poimirlem32  34918  voliunnfl  34930  volsupnfl  34931  lmclim2  35027  geomcau  35028  rrncmslem  35104  eldioph3b  39355  lzenom  39360  diophin  39362  diophun  39363  pellexlem3  39421  pellexlem4  39422  pellexlem5  39423  eltrclrec  40018  brtrclrec  40034  iunrelexpmin1  40046  trclrelexplem  40049  dftrcl3  40058  fvtrcllb1d  40060  trclfvcom  40061  cnvtrclfv  40062  cotrcltrcl  40063  trclimalb2  40064  trclfvdecomr  40066  dfrtrcl4  40076  corcltrcl  40077  cotrclrcl  40080  hashnzfzclim  40647  dvradcnv2  40672  binomcxplemcvg  40679  binomcxplemdvsum  40680  binomcxplemnotnn0  40681  ssnnf1octb  41449  clim1fr1  41875  divcnvg  41901  limsup10ex  42047  liminf10ex  42048  wallispilem5  42348  wallispi  42349  stirlinglem1  42353  stirlinglem8  42360  stirlinglem14  42366  stirlinglem15  42367  fourierdlem103  42488  fourierdlem104  42489  fourierdlem112  42497  subsaliuncllem  42634  subsaliuncl  42635  nnfoctbdjlem  42731  nnfoctbdj  42732  ismeannd  42743  voliunsge0lem  42748  caratheodorylem2  42803  isomenndlem  42806  hoicvrrex  42832  ovnsupge0  42833  ovnlecvr  42834  ovn0lem  42841  ovnsubaddlem1  42846  ovnsubadd  42848  sge0hsphoire  42865  hoidmv1lelem1  42867  hoidmv1lelem2  42868  hoidmv1lelem3  42869  hoidmv1le  42870  hoidmvlelem1  42871  hoidmvlelem2  42872  hoidmvlelem3  42873  hoidmvlelem4  42874  hoidmvlelem5  42875  hoidmvle  42876  ovnhoilem1  42877  ovnhoilem2  42878  ovnlecvr2  42886  hspmbllem2  42903  ovolval2lem  42919  ovnsubadd2lem  42921  ovolval4lem2  42926  ovolval5lem1  42928  ovolval5lem2  42929  ovnovollem1  42932  ovnovollem2  42933  vonioolem1  42956  smflimlem6  43046  smfresal  43057  nnsgrpmgm  44077  nnsgrp  44078  nnsgrpnmnd  44079