Theorem nnex 12299

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 11265	. 2 ⊢ ℂ ∈ V
2		nnsscn 12298	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5340	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3488  ℂcc 11182  ℕcn 12293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-1cn 11242  ax-addcl 11244

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-nn 12294

This theorem is referenced by:  dfnn2  12306  nn0ex  12559  nn0ennn  14030  facmapnn  14334  isercolllem2  15714  supcvg  15904  trireciplem  15910  expcnv  15912  geo2lim  15923  qnnen  16261  rpnnen2lem1  16262  rpnnen2lem2  16263  rpnnen  16275  rucALT  16278  prmex  16724  unbenlem  16955  vdwapfval  17018  vdwapf  17019  vdwlem6  17033  vdwlem7  17034  vdwlem8  17035  vdwlem11  17038  prmgaplcm  17107  prmgapprmo  17109  ndxarg  17243  odfval  19574  odval  19576  gexval  19620  pnrmopn  23372  1stcfb  23474  hausmapdom  23529  met1stc  24555  met2ndci  24556  rectbntr0  24873  metcld2  25360  elovolmlem  25528  ovolctb  25544  ovol0  25547  mbfimaopnlem  25709  itg1climres  25769  mbfi1fseqlem6  25775  mbfi1flimlem  25777  mbfmullem2  25779  itg2monolem1  25805  itg2addlem  25813  plyeq0lem  26269  leibpi  27003  dfef2  27032  emcllem4  27060  emcllem6  27062  emcllem7  27063  lgamgulmlem6  27095  lgamcvg2  27116  basellem6  27147  basellem7  27148  basellem8  27149  basellem9  27150  dchrisumlem3  27553  dirith2  27590  nmounbseqiALT  30810  nmobndseqiALT  30812  h2hcau  31011  h2hlm  31012  hcau  31216  hlimi  31220  hlimadd  31225  hhcms  31235  isch2  31255  chlimi  31266  hlim0  31267  hhsscms  31310  padct  32733  smatfval  33741  lmdvg  33899  esumfsup  34034  esumpcvgval  34042  esumcvg  34050  sigapildsys  34126  measiun  34182  voliune  34193  omssubadd  34265  carsggect  34283  carsgclctunlem2  34284  eulerpartlems  34325  eulerpartleme  34328  eulerpartlem1  34332  eulerpartlemb  34333  eulerpartlemt  34336  eulerpartgbij  34337  eulerpartlemr  34339  eulerpartlemmf  34340  eulerpartlemgvv  34341  eulerpartlemgf  34344  eulerpartlemgs2  34345  eulerpartlemn  34346  reprval  34587  repr0  34588  reprsuc  34592  reprss  34594  reprinrn  34595  reprlt  34596  hashreprin  34597  reprinfz1  34599  reprpmtf1o  34603  reprdifc  34604  breprexplemb  34608  breprexpnat  34611  vtsval  34614  circlemethnat  34618  circlevma  34619  circlemethhgt  34620  sinccvglem  35640  circum  35642  divcnvlin  35695  faclimlem2  35706  faclim2  35710  colinearex  36024  bj-ndxarg  37043  poimirlem32  37612  voliunnfl  37624  volsupnfl  37625  lmclim2  37718  geomcau  37719  rrncmslem  37792  fisdomnn  42239  eldioph3b  42721  lzenom  42726  diophin  42728  diophun  42729  pellexlem3  42787  pellexlem4  42788  pellexlem5  42789  eltrclrec  43642  brtrclrec  43658  iunrelexpmin1  43670  trclrelexplem  43673  dftrcl3  43682  fvtrcllb1d  43684  trclfvcom  43685  cnvtrclfv  43686  cotrcltrcl  43687  trclimalb2  43688  trclfvdecomr  43690  dfrtrcl4  43700  corcltrcl  43701  cotrclrcl  43704  hashnzfzclim  44291  dvradcnv2  44316  binomcxplemcvg  44323  binomcxplemdvsum  44324  binomcxplemnotnn0  44325  ssnnf1octb  45101  clim1fr1  45522  divcnvg  45548  limsup10ex  45694  liminf10ex  45695  wallispilem5  45990  wallispi  45991  stirlinglem1  45995  stirlinglem8  46002  stirlinglem14  46008  stirlinglem15  46009  fourierdlem103  46130  fourierdlem104  46131  fourierdlem112  46139  subsaliuncllem  46278  subsaliuncl  46279  nnfoctbdjlem  46376  nnfoctbdj  46377  ismeannd  46388  voliunsge0lem  46393  caratheodorylem2  46448  isomenndlem  46451  hoicvrrex  46477  ovnsupge0  46478  ovnlecvr  46479  ovn0lem  46486  ovnsubaddlem1  46491  ovnsubadd  46493  sge0hsphoire  46510  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmv1lelem3  46514  hoidmv1le  46515  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  hoidmvlelem5  46520  hoidmvle  46521  ovnhoilem1  46522  ovnhoilem2  46523  ovnlecvr2  46531  hspmbllem2  46548  ovolval2lem  46564  ovnsubadd2lem  46566  ovolval4lem2  46571  ovolval5lem1  46573  ovolval5lem2  46574  ovnovollem1  46577  ovnovollem2  46578  vonioolem1  46601  smflimlem6  46697  smfresal  46709  fsupdm  46763  smfsupdmmbllem  46765  finfdm  46767  smfinfdmmbllem  46769  nnsgrpmgm  47899  nnsgrp  47900  nnsgrpnmnd  47901