Theorem nnex 12174

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 11113	. 2 ⊢ ℂ ∈ V
2		nnsscn 12173	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5260	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3430  ℂcc 11030  ℕcn 12168

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-1cn 11090  ax-addcl 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7364  df-om 7812  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-nn 12169

This theorem is referenced by:  dfnn2  12181  nn0ex  12437  nn0ennn  13935  facmapnn  14241  isercolllem2  15622  supcvg  15815  trireciplem  15821  expcnv  15823  geo2lim  15834  qnnen  16174  rpnnen2lem1  16175  rpnnen2lem2  16176  rpnnen  16188  rucALT  16191  prmex  16640  unbenlem  16873  vdwapfval  16936  vdwapf  16937  vdwlem6  16951  vdwlem7  16952  vdwlem8  16953  vdwlem11  16956  prmgaplcm  17025  prmgapprmo  17027  ndxarg  17160  ex-chn2  18598  odfval  19501  odval  19503  gexval  19547  pnrmopn  23321  1stcfb  23423  hausmapdom  23478  met1stc  24499  met2ndci  24500  rectbntr0  24811  metcld2  25287  elovolmlem  25454  ovolctb  25470  ovol0  25473  mbfimaopnlem  25635  itg1climres  25694  mbfi1fseqlem6  25700  mbfi1flimlem  25702  mbfmullem2  25704  itg2monolem1  25730  itg2addlem  25738  plyeq0lem  26188  leibpi  26922  dfef2  26951  emcllem4  26979  emcllem6  26981  emcllem7  26982  lgamgulmlem6  27014  lgamcvg2  27035  basellem6  27066  basellem7  27067  basellem8  27068  basellem9  27069  dchrisumlem3  27471  dirith2  27508  nmounbseqiALT  30867  nmobndseqiALT  30869  h2hcau  31068  h2hlm  31069  hcau  31273  hlimi  31277  hlimadd  31282  hhcms  31292  isch2  31312  chlimi  31323  hlim0  31324  hhsscms  31367  padct  32809  smatfval  33958  lmdvg  34116  esumfsup  34233  esumpcvgval  34241  esumcvg  34249  sigapildsys  34325  measiun  34381  voliune  34392  omssubadd  34463  carsggect  34481  carsgclctunlem2  34482  eulerpartlems  34523  eulerpartleme  34526  eulerpartlem1  34530  eulerpartlemb  34531  eulerpartlemt  34534  eulerpartgbij  34535  eulerpartlemr  34537  eulerpartlemmf  34538  eulerpartlemgvv  34539  eulerpartlemgf  34542  eulerpartlemgs2  34543  eulerpartlemn  34544  reprval  34773  repr0  34774  reprsuc  34778  reprss  34780  reprinrn  34781  reprlt  34782  hashreprin  34783  reprinfz1  34785  reprpmtf1o  34789  reprdifc  34790  breprexplemb  34794  breprexpnat  34797  vtsval  34800  circlemethnat  34804  circlevma  34805  circlemethhgt  34806  sinccvglem  35873  circum  35875  divcnvlin  35934  faclimlem2  35945  faclim2  35949  colinearex  36261  bj-ndxarg  37408  poimirlem32  37990  voliunnfl  38002  volsupnfl  38003  lmclim2  38096  geomcau  38097  rrncmslem  38170  fisdomnn  42700  eldioph3b  43214  lzenom  43219  diophin  43221  diophun  43222  pellexlem3  43280  pellexlem4  43281  pellexlem5  43282  eltrclrec  44128  brtrclrec  44144  iunrelexpmin1  44156  trclrelexplem  44159  dftrcl3  44168  fvtrcllb1d  44170  trclfvcom  44171  cnvtrclfv  44172  cotrcltrcl  44173  trclimalb2  44174  trclfvdecomr  44176  dfrtrcl4  44186  corcltrcl  44187  cotrclrcl  44190  hashnzfzclim  44770  dvradcnv2  44795  binomcxplemcvg  44802  binomcxplemdvsum  44803  binomcxplemnotnn0  44804  ssnnf1octb  45645  clim1fr1  46052  divcnvg  46078  limsup10ex  46222  liminf10ex  46223  wallispilem5  46518  wallispi  46519  stirlinglem1  46523  stirlinglem8  46530  stirlinglem14  46536  stirlinglem15  46537  fourierdlem103  46658  fourierdlem104  46659  fourierdlem112  46667  subsaliuncllem  46806  subsaliuncl  46807  nnfoctbdjlem  46904  nnfoctbdj  46905  ismeannd  46916  voliunsge0lem  46921  caratheodorylem2  46976  isomenndlem  46979  hoicvrrex  47005  ovnsupge0  47006  ovnlecvr  47007  ovn0lem  47014  ovnsubaddlem1  47019  ovnsubadd  47021  sge0hsphoire  47038  hoidmv1lelem1  47040  hoidmv1lelem2  47041  hoidmv1lelem3  47042  hoidmv1le  47043  hoidmvlelem1  47044  hoidmvlelem2  47045  hoidmvlelem3  47046  hoidmvlelem4  47047  hoidmvlelem5  47048  hoidmvle  47049  ovnhoilem1  47050  ovnhoilem2  47051  ovnlecvr2  47059  hspmbllem2  47076  ovolval2lem  47092  ovnsubadd2lem  47094  ovolval4lem2  47099  ovolval5lem1  47101  ovolval5lem2  47102  ovnovollem1  47105  ovnovollem2  47106  vonioolem1  47129  smflimlem6  47225  smfresal  47237  fsupdm  47291  smfsupdmmbllem  47293  finfdm  47295  smfinfdmmbllem  47297  nthrucw  47335  nnsgrpmgm  48667  nnsgrp  48668  nnsgrpnmnd  48669