Theorem nnex 12217

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

Syntax hints:   ∈ wcel 2106  Vcvv 3474  ℂcc 11107  ℕcn 12211

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7724  ax-cnex 11165  ax-1cn 11167  ax-addcl 11169

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7411  df-om 7855  df-2nd 7975  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-nn 12212

This theorem is referenced by:  dfnn2  12224  nn0ex  12477  nn0ennn  13943  facmapnn  14244  isercolllem2  15611  supcvg  15801  trireciplem  15807  expcnv  15809  geo2lim  15820  qnnen  16155  rpnnen2lem1  16156  rpnnen2lem2  16157  rpnnen  16169  rucALT  16172  prmex  16613  unbenlem  16840  vdwapfval  16903  vdwapf  16904  vdwlem6  16918  vdwlem7  16919  vdwlem8  16920  vdwlem11  16923  prmgaplcm  16992  prmgapprmo  16994  ndxarg  17128  odfval  19399  odval  19401  gexval  19445  pnrmopn  22846  1stcfb  22948  hausmapdom  23003  met1stc  24029  met2ndci  24030  rectbntr0  24347  metcld2  24823  elovolmlem  24990  ovolctb  25006  ovol0  25009  mbfimaopnlem  25171  itg1climres  25231  mbfi1fseqlem6  25237  mbfi1flimlem  25239  mbfmullem2  25241  itg2monolem1  25267  itg2addlem  25275  plyeq0lem  25723  leibpi  26444  dfef2  26472  emcllem4  26500  emcllem6  26502  emcllem7  26503  lgamgulmlem6  26535  lgamcvg2  26556  basellem6  26587  basellem7  26588  basellem8  26589  basellem9  26590  dchrisumlem3  26991  dirith2  27028  nmounbseqiALT  30026  nmobndseqiALT  30028  h2hcau  30227  h2hlm  30228  hcau  30432  hlimi  30436  hlimadd  30441  hhcms  30451  isch2  30471  chlimi  30482  hlim0  30483  hhsscms  30526  padct  31939  smatfval  32770  lmdvg  32928  esumfsup  33063  esumpcvgval  33071  esumcvg  33079  sigapildsys  33155  measiun  33211  voliune  33222  omssubadd  33294  carsggect  33312  carsgclctunlem2  33313  eulerpartlems  33354  eulerpartleme  33357  eulerpartlem1  33361  eulerpartlemb  33362  eulerpartlemt  33365  eulerpartgbij  33366  eulerpartlemr  33368  eulerpartlemmf  33369  eulerpartlemgvv  33370  eulerpartlemgf  33373  eulerpartlemgs2  33374  eulerpartlemn  33375  reprval  33617  repr0  33618  reprsuc  33622  reprss  33624  reprinrn  33625  reprlt  33626  hashreprin  33627  reprinfz1  33629  reprpmtf1o  33633  reprdifc  33634  breprexplemb  33638  breprexpnat  33641  vtsval  33644  circlemethnat  33648  circlevma  33649  circlemethhgt  33650  sinccvglem  34652  circum  34654  divcnvlin  34697  faclimlem2  34709  faclim2  34713  colinearex  35027  bj-ndxarg  35953  poimirlem32  36515  voliunnfl  36527  volsupnfl  36528  lmclim2  36621  geomcau  36622  rrncmslem  36695  eldioph3b  41493  lzenom  41498  diophin  41500  diophun  41501  pellexlem3  41559  pellexlem4  41560  pellexlem5  41561  eltrclrec  42421  brtrclrec  42437  iunrelexpmin1  42449  trclrelexplem  42452  dftrcl3  42461  fvtrcllb1d  42463  trclfvcom  42464  cnvtrclfv  42465  cotrcltrcl  42466  trclimalb2  42467  trclfvdecomr  42469  dfrtrcl4  42479  corcltrcl  42480  cotrclrcl  42483  hashnzfzclim  43071  dvradcnv2  43096  binomcxplemcvg  43103  binomcxplemdvsum  43104  binomcxplemnotnn0  43105  ssnnf1octb  43883  clim1fr1  44307  divcnvg  44333  limsup10ex  44479  liminf10ex  44480  wallispilem5  44775  wallispi  44776  stirlinglem1  44780  stirlinglem8  44787  stirlinglem14  44793  stirlinglem15  44794  fourierdlem103  44915  fourierdlem104  44916  fourierdlem112  44924  subsaliuncllem  45063  subsaliuncl  45064  nnfoctbdjlem  45161  nnfoctbdj  45162  ismeannd  45173  voliunsge0lem  45178  caratheodorylem2  45233  isomenndlem  45236  hoicvrrex  45262  ovnsupge0  45263  ovnlecvr  45264  ovn0lem  45271  ovnsubaddlem1  45276  ovnsubadd  45278  sge0hsphoire  45295  hoidmv1lelem1  45297  hoidmv1lelem2  45298  hoidmv1lelem3  45299  hoidmv1le  45300  hoidmvlelem1  45301  hoidmvlelem2  45302  hoidmvlelem3  45303  hoidmvlelem4  45304  hoidmvlelem5  45305  hoidmvle  45306  ovnhoilem1  45307  ovnhoilem2  45308  ovnlecvr2  45316  hspmbllem2  45333  ovolval2lem  45349  ovnsubadd2lem  45351  ovolval4lem2  45356  ovolval5lem1  45358  ovolval5lem2  45359  ovnovollem1  45362  ovnovollem2  45363  vonioolem1  45386  smflimlem6  45482  smfresal  45494  fsupdm  45548  smfsupdmmbllem  45550  finfdm  45552  smfinfdmmbllem  45554  nnsgrpmgm  46576  nnsgrp  46577  nnsgrpnmnd  46578