Theorem nnex 12244

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 11208	. 2 ⊢ ℂ ∈ V
2		nnsscn 12243	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5292	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3459  ℂcc 11125  ℕcn 12238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-1cn 11185  ax-addcl 11187

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-ov 7406  df-om 7860  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-nn 12239

This theorem is referenced by:  dfnn2  12251  nn0ex  12505  nn0ennn  13995  facmapnn  14301  isercolllem2  15680  supcvg  15870  trireciplem  15876  expcnv  15878  geo2lim  15889  qnnen  16229  rpnnen2lem1  16230  rpnnen2lem2  16231  rpnnen  16243  rucALT  16246  prmex  16694  unbenlem  16926  vdwapfval  16989  vdwapf  16990  vdwlem6  17004  vdwlem7  17005  vdwlem8  17006  vdwlem11  17009  prmgaplcm  17078  prmgapprmo  17080  ndxarg  17213  odfval  19511  odval  19513  gexval  19557  pnrmopn  23279  1stcfb  23381  hausmapdom  23436  met1stc  24458  met2ndci  24459  rectbntr0  24770  metcld2  25257  elovolmlem  25425  ovolctb  25441  ovol0  25444  mbfimaopnlem  25606  itg1climres  25665  mbfi1fseqlem6  25671  mbfi1flimlem  25673  mbfmullem2  25675  itg2monolem1  25701  itg2addlem  25709  plyeq0lem  26165  leibpi  26902  dfef2  26931  emcllem4  26959  emcllem6  26961  emcllem7  26962  lgamgulmlem6  26994  lgamcvg2  27015  basellem6  27046  basellem7  27047  basellem8  27048  basellem9  27049  dchrisumlem3  27452  dirith2  27489  nmounbseqiALT  30705  nmobndseqiALT  30707  h2hcau  30906  h2hlm  30907  hcau  31111  hlimi  31115  hlimadd  31120  hhcms  31130  isch2  31150  chlimi  31161  hlim0  31162  hhsscms  31205  padct  32643  smatfval  33772  lmdvg  33930  esumfsup  34047  esumpcvgval  34055  esumcvg  34063  sigapildsys  34139  measiun  34195  voliune  34206  omssubadd  34278  carsggect  34296  carsgclctunlem2  34297  eulerpartlems  34338  eulerpartleme  34341  eulerpartlem1  34345  eulerpartlemb  34346  eulerpartlemt  34349  eulerpartgbij  34350  eulerpartlemr  34352  eulerpartlemmf  34353  eulerpartlemgvv  34354  eulerpartlemgf  34357  eulerpartlemgs2  34358  eulerpartlemn  34359  reprval  34588  repr0  34589  reprsuc  34593  reprss  34595  reprinrn  34596  reprlt  34597  hashreprin  34598  reprinfz1  34600  reprpmtf1o  34604  reprdifc  34605  breprexplemb  34609  breprexpnat  34612  vtsval  34615  circlemethnat  34619  circlevma  34620  circlemethhgt  34621  sinccvglem  35640  circum  35642  divcnvlin  35696  faclimlem2  35707  faclim2  35711  colinearex  36024  bj-ndxarg  37041  poimirlem32  37622  voliunnfl  37634  volsupnfl  37635  lmclim2  37728  geomcau  37729  rrncmslem  37802  fisdomnn  42242  eldioph3b  42735  lzenom  42740  diophin  42742  diophun  42743  pellexlem3  42801  pellexlem4  42802  pellexlem5  42803  eltrclrec  43651  brtrclrec  43667  iunrelexpmin1  43679  trclrelexplem  43682  dftrcl3  43691  fvtrcllb1d  43693  trclfvcom  43694  cnvtrclfv  43695  cotrcltrcl  43696  trclimalb2  43697  trclfvdecomr  43699  dfrtrcl4  43709  corcltrcl  43710  cotrclrcl  43713  hashnzfzclim  44294  dvradcnv2  44319  binomcxplemcvg  44326  binomcxplemdvsum  44327  binomcxplemnotnn0  44328  ssnnf1octb  45166  clim1fr1  45578  divcnvg  45604  limsup10ex  45750  liminf10ex  45751  wallispilem5  46046  wallispi  46047  stirlinglem1  46051  stirlinglem8  46058  stirlinglem14  46064  stirlinglem15  46065  fourierdlem103  46186  fourierdlem104  46187  fourierdlem112  46195  subsaliuncllem  46334  subsaliuncl  46335  nnfoctbdjlem  46432  nnfoctbdj  46433  ismeannd  46444  voliunsge0lem  46449  caratheodorylem2  46504  isomenndlem  46507  hoicvrrex  46533  ovnsupge0  46534  ovnlecvr  46535  ovn0lem  46542  ovnsubaddlem1  46547  ovnsubadd  46549  sge0hsphoire  46566  hoidmv1lelem1  46568  hoidmv1lelem2  46569  hoidmv1lelem3  46570  hoidmv1le  46571  hoidmvlelem1  46572  hoidmvlelem2  46573  hoidmvlelem3  46574  hoidmvlelem4  46575  hoidmvlelem5  46576  hoidmvle  46577  ovnhoilem1  46578  ovnhoilem2  46579  ovnlecvr2  46587  hspmbllem2  46604  ovolval2lem  46620  ovnsubadd2lem  46622  ovolval4lem2  46627  ovolval5lem1  46629  ovolval5lem2  46630  ovnovollem1  46633  ovnovollem2  46634  vonioolem1  46657  smflimlem6  46753  smfresal  46765  fsupdm  46819  smfsupdmmbllem  46821  finfdm  46823  smfinfdmmbllem  46825  nnsgrpmgm  48099  nnsgrp  48100  nnsgrpnmnd  48101