Theorem nnex 12131

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 11087	. 2 ⊢ ℂ ∈ V
2		nnsscn 12130	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5258	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2111  Vcvv 3436  ℂcc 11004  ℕcn 12125

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7668  ax-cnex 11062  ax-1cn 11064  ax-addcl 11066

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-om 7797  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-nn 12126

This theorem is referenced by:  dfnn2  12138  nn0ex  12387  nn0ennn  13886  facmapnn  14192  isercolllem2  15573  supcvg  15763  trireciplem  15769  expcnv  15771  geo2lim  15782  qnnen  16122  rpnnen2lem1  16123  rpnnen2lem2  16124  rpnnen  16136  rucALT  16139  prmex  16588  unbenlem  16820  vdwapfval  16883  vdwapf  16884  vdwlem6  16898  vdwlem7  16899  vdwlem8  16900  vdwlem11  16903  prmgaplcm  16972  prmgapprmo  16974  ndxarg  17107  ex-chn2  18544  odfval  19444  odval  19446  gexval  19490  pnrmopn  23258  1stcfb  23360  hausmapdom  23415  met1stc  24436  met2ndci  24437  rectbntr0  24748  metcld2  25234  elovolmlem  25402  ovolctb  25418  ovol0  25421  mbfimaopnlem  25583  itg1climres  25642  mbfi1fseqlem6  25648  mbfi1flimlem  25650  mbfmullem2  25652  itg2monolem1  25678  itg2addlem  25686  plyeq0lem  26142  leibpi  26879  dfef2  26908  emcllem4  26936  emcllem6  26938  emcllem7  26939  lgamgulmlem6  26971  lgamcvg2  26992  basellem6  27023  basellem7  27024  basellem8  27025  basellem9  27026  dchrisumlem3  27429  dirith2  27466  nmounbseqiALT  30758  nmobndseqiALT  30760  h2hcau  30959  h2hlm  30960  hcau  31164  hlimi  31168  hlimadd  31173  hhcms  31183  isch2  31203  chlimi  31214  hlim0  31215  hhsscms  31258  padct  32701  smatfval  33808  lmdvg  33966  esumfsup  34083  esumpcvgval  34091  esumcvg  34099  sigapildsys  34175  measiun  34231  voliune  34242  omssubadd  34313  carsggect  34331  carsgclctunlem2  34332  eulerpartlems  34373  eulerpartleme  34376  eulerpartlem1  34380  eulerpartlemb  34381  eulerpartlemt  34384  eulerpartgbij  34385  eulerpartlemr  34387  eulerpartlemmf  34388  eulerpartlemgvv  34389  eulerpartlemgf  34392  eulerpartlemgs2  34393  eulerpartlemn  34394  reprval  34623  repr0  34624  reprsuc  34628  reprss  34630  reprinrn  34631  reprlt  34632  hashreprin  34633  reprinfz1  34635  reprpmtf1o  34639  reprdifc  34640  breprexplemb  34644  breprexpnat  34647  vtsval  34650  circlemethnat  34654  circlevma  34655  circlemethhgt  34656  sinccvglem  35716  circum  35718  divcnvlin  35777  faclimlem2  35788  faclim2  35792  colinearex  36102  bj-ndxarg  37119  poimirlem32  37700  voliunnfl  37712  volsupnfl  37713  lmclim2  37806  geomcau  37807  rrncmslem  37880  fisdomnn  42285  eldioph3b  42806  lzenom  42811  diophin  42813  diophun  42814  pellexlem3  42872  pellexlem4  42873  pellexlem5  42874  eltrclrec  43721  brtrclrec  43737  iunrelexpmin1  43749  trclrelexplem  43752  dftrcl3  43761  fvtrcllb1d  43763  trclfvcom  43764  cnvtrclfv  43765  cotrcltrcl  43766  trclimalb2  43767  trclfvdecomr  43769  dfrtrcl4  43779  corcltrcl  43780  cotrclrcl  43783  hashnzfzclim  44363  dvradcnv2  44388  binomcxplemcvg  44395  binomcxplemdvsum  44396  binomcxplemnotnn0  44397  ssnnf1octb  45239  clim1fr1  45649  divcnvg  45675  limsup10ex  45819  liminf10ex  45820  wallispilem5  46115  wallispi  46116  stirlinglem1  46120  stirlinglem8  46127  stirlinglem14  46133  stirlinglem15  46134  fourierdlem103  46255  fourierdlem104  46256  fourierdlem112  46264  subsaliuncllem  46403  subsaliuncl  46404  nnfoctbdjlem  46501  nnfoctbdj  46502  ismeannd  46513  voliunsge0lem  46518  caratheodorylem2  46573  isomenndlem  46576  hoicvrrex  46602  ovnsupge0  46603  ovnlecvr  46604  ovn0lem  46611  ovnsubaddlem1  46616  ovnsubadd  46618  sge0hsphoire  46635  hoidmv1lelem1  46637  hoidmv1lelem2  46638  hoidmv1lelem3  46639  hoidmv1le  46640  hoidmvlelem1  46641  hoidmvlelem2  46642  hoidmvlelem3  46643  hoidmvlelem4  46644  hoidmvlelem5  46645  hoidmvle  46646  ovnhoilem1  46647  ovnhoilem2  46648  ovnlecvr2  46656  hspmbllem2  46673  ovolval2lem  46689  ovnsubadd2lem  46691  ovolval4lem2  46696  ovolval5lem1  46698  ovolval5lem2  46699  ovnovollem1  46702  ovnovollem2  46703  vonioolem1  46726  smflimlem6  46822  smfresal  46834  fsupdm  46888  smfsupdmmbllem  46890  finfdm  46892  smfinfdmmbllem  46894  nnsgrpmgm  48215  nnsgrp  48216  nnsgrpnmnd  48217