Theorem nnex 12269

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 11233	. 2 ⊢ ℂ ∈ V
2		nnsscn 12268	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5327	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2105  Vcvv 3477  ℂcc 11150  ℕcn 12263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-1cn 11210  ax-addcl 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-nn 12264

This theorem is referenced by:  dfnn2  12276  nn0ex  12529  nn0ennn  14016  facmapnn  14320  isercolllem2  15698  supcvg  15888  trireciplem  15894  expcnv  15896  geo2lim  15907  qnnen  16245  rpnnen2lem1  16246  rpnnen2lem2  16247  rpnnen  16259  rucALT  16262  prmex  16710  unbenlem  16941  vdwapfval  17004  vdwapf  17005  vdwlem6  17019  vdwlem7  17020  vdwlem8  17021  vdwlem11  17024  prmgaplcm  17093  prmgapprmo  17095  ndxarg  17229  odfval  19564  odval  19566  gexval  19610  pnrmopn  23366  1stcfb  23468  hausmapdom  23523  met1stc  24549  met2ndci  24550  rectbntr0  24867  metcld2  25354  elovolmlem  25522  ovolctb  25538  ovol0  25541  mbfimaopnlem  25703  itg1climres  25763  mbfi1fseqlem6  25769  mbfi1flimlem  25771  mbfmullem2  25773  itg2monolem1  25799  itg2addlem  25807  plyeq0lem  26263  leibpi  26999  dfef2  27028  emcllem4  27056  emcllem6  27058  emcllem7  27059  lgamgulmlem6  27091  lgamcvg2  27112  basellem6  27143  basellem7  27144  basellem8  27145  basellem9  27146  dchrisumlem3  27549  dirith2  27586  nmounbseqiALT  30806  nmobndseqiALT  30808  h2hcau  31007  h2hlm  31008  hcau  31212  hlimi  31216  hlimadd  31221  hhcms  31231  isch2  31251  chlimi  31262  hlim0  31263  hhsscms  31306  padct  32736  smatfval  33755  lmdvg  33913  esumfsup  34050  esumpcvgval  34058  esumcvg  34066  sigapildsys  34142  measiun  34198  voliune  34209  omssubadd  34281  carsggect  34299  carsgclctunlem2  34300  eulerpartlems  34341  eulerpartleme  34344  eulerpartlem1  34348  eulerpartlemb  34349  eulerpartlemt  34352  eulerpartgbij  34353  eulerpartlemr  34355  eulerpartlemmf  34356  eulerpartlemgvv  34357  eulerpartlemgf  34360  eulerpartlemgs2  34361  eulerpartlemn  34362  reprval  34603  repr0  34604  reprsuc  34608  reprss  34610  reprinrn  34611  reprlt  34612  hashreprin  34613  reprinfz1  34615  reprpmtf1o  34619  reprdifc  34620  breprexplemb  34624  breprexpnat  34627  vtsval  34630  circlemethnat  34634  circlevma  34635  circlemethhgt  34636  sinccvglem  35656  circum  35658  divcnvlin  35712  faclimlem2  35723  faclim2  35727  colinearex  36041  bj-ndxarg  37059  poimirlem32  37638  voliunnfl  37650  volsupnfl  37651  lmclim2  37744  geomcau  37745  rrncmslem  37818  fisdomnn  42263  eldioph3b  42752  lzenom  42757  diophin  42759  diophun  42760  pellexlem3  42818  pellexlem4  42819  pellexlem5  42820  eltrclrec  43669  brtrclrec  43685  iunrelexpmin1  43697  trclrelexplem  43700  dftrcl3  43709  fvtrcllb1d  43711  trclfvcom  43712  cnvtrclfv  43713  cotrcltrcl  43714  trclimalb2  43715  trclfvdecomr  43717  dfrtrcl4  43727  corcltrcl  43728  cotrclrcl  43731  hashnzfzclim  44317  dvradcnv2  44342  binomcxplemcvg  44349  binomcxplemdvsum  44350  binomcxplemnotnn0  44351  ssnnf1octb  45136  clim1fr1  45556  divcnvg  45582  limsup10ex  45728  liminf10ex  45729  wallispilem5  46024  wallispi  46025  stirlinglem1  46029  stirlinglem8  46036  stirlinglem14  46042  stirlinglem15  46043  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  subsaliuncllem  46312  subsaliuncl  46313  nnfoctbdjlem  46410  nnfoctbdj  46411  ismeannd  46422  voliunsge0lem  46427  caratheodorylem2  46482  isomenndlem  46485  hoicvrrex  46511  ovnsupge0  46512  ovnlecvr  46513  ovn0lem  46520  ovnsubaddlem1  46525  ovnsubadd  46527  sge0hsphoire  46544  hoidmv1lelem1  46546  hoidmv1lelem2  46547  hoidmv1lelem3  46548  hoidmv1le  46549  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem4  46553  hoidmvlelem5  46554  hoidmvle  46555  ovnhoilem1  46556  ovnhoilem2  46557  ovnlecvr2  46565  hspmbllem2  46582  ovolval2lem  46598  ovnsubadd2lem  46600  ovolval4lem2  46605  ovolval5lem1  46607  ovolval5lem2  46608  ovnovollem1  46611  ovnovollem2  46612  vonioolem1  46635  smflimlem6  46731  smfresal  46743  fsupdm  46797  smfsupdmmbllem  46799  finfdm  46801  smfinfdmmbllem  46803  nnsgrpmgm  48019  nnsgrp  48020  nnsgrpnmnd  48021