Theorem nnex 12134

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 11090	. 2 ⊢ ℂ ∈ V
2		nnsscn 12133	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5261	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3436  ℂcc 11007  ℕcn 12128

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-1cn 11067  ax-addcl 11069

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-om 7800  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-nn 12129

This theorem is referenced by:  dfnn2  12141  nn0ex  12390  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  odfval  19411  odval  19413  gexval  19457  pnrmopn  23228  1stcfb  23330  hausmapdom  23385  met1stc  24407  met2ndci  24408  rectbntr0  24719  metcld2  25205  elovolmlem  25373  ovolctb  25389  ovol0  25392  mbfimaopnlem  25554  itg1climres  25613  mbfi1fseqlem6  25619  mbfi1flimlem  25621  mbfmullem2  25623  itg2monolem1  25649  itg2addlem  25657  plyeq0lem  26113  leibpi  26850  dfef2  26879  emcllem4  26907  emcllem6  26909  emcllem7  26910  lgamgulmlem6  26942  lgamcvg2  26963  basellem6  26994  basellem7  26995  basellem8  26996  basellem9  26997  dchrisumlem3  27400  dirith2  27437  nmounbseqiALT  30722  nmobndseqiALT  30724  h2hcau  30923  h2hlm  30924  hcau  31128  hlimi  31132  hlimadd  31137  hhcms  31147  isch2  31167  chlimi  31178  hlim0  31179  hhsscms  31222  padct  32662  smatfval  33762  lmdvg  33920  esumfsup  34037  esumpcvgval  34045  esumcvg  34053  sigapildsys  34129  measiun  34185  voliune  34196  omssubadd  34268  carsggect  34286  carsgclctunlem2  34287  eulerpartlems  34328  eulerpartleme  34331  eulerpartlem1  34335  eulerpartlemb  34336  eulerpartlemt  34339  eulerpartgbij  34340  eulerpartlemr  34342  eulerpartlemmf  34343  eulerpartlemgvv  34344  eulerpartlemgf  34347  eulerpartlemgs2  34348  eulerpartlemn  34349  reprval  34578  repr0  34579  reprsuc  34583  reprss  34585  reprinrn  34586  reprlt  34587  hashreprin  34588  reprinfz1  34590  reprpmtf1o  34594  reprdifc  34595  breprexplemb  34599  breprexpnat  34602  vtsval  34605  circlemethnat  34609  circlevma  34610  circlemethhgt  34611  sinccvglem  35645  circum  35647  divcnvlin  35706  faclimlem2  35717  faclim2  35721  colinearex  36034  bj-ndxarg  37051  poimirlem32  37632  voliunnfl  37644  volsupnfl  37645  lmclim2  37738  geomcau  37739  rrncmslem  37812  fisdomnn  42217  eldioph3b  42738  lzenom  42743  diophin  42745  diophun  42746  pellexlem3  42804  pellexlem4  42805  pellexlem5  42806  eltrclrec  43653  brtrclrec  43669  iunrelexpmin1  43681  trclrelexplem  43684  dftrcl3  43693  fvtrcllb1d  43695  trclfvcom  43696  cnvtrclfv  43697  cotrcltrcl  43698  trclimalb2  43699  trclfvdecomr  43701  dfrtrcl4  43711  corcltrcl  43712  cotrclrcl  43715  hashnzfzclim  44295  dvradcnv2  44320  binomcxplemcvg  44327  binomcxplemdvsum  44328  binomcxplemnotnn0  44329  ssnnf1octb  45172  clim1fr1  45582  divcnvg  45608  limsup10ex  45754  liminf10ex  45755  wallispilem5  46050  wallispi  46051  stirlinglem1  46055  stirlinglem8  46062  stirlinglem14  46068  stirlinglem15  46069  fourierdlem103  46190  fourierdlem104  46191  fourierdlem112  46199  subsaliuncllem  46338  subsaliuncl  46339  nnfoctbdjlem  46436  nnfoctbdj  46437  ismeannd  46448  voliunsge0lem  46453  caratheodorylem2  46508  isomenndlem  46511  hoicvrrex  46537  ovnsupge0  46538  ovnlecvr  46539  ovn0lem  46546  ovnsubaddlem1  46551  ovnsubadd  46553  sge0hsphoire  46570  hoidmv1lelem1  46572  hoidmv1lelem2  46573  hoidmv1lelem3  46574  hoidmv1le  46575  hoidmvlelem1  46576  hoidmvlelem2  46577  hoidmvlelem3  46578  hoidmvlelem4  46579  hoidmvlelem5  46580  hoidmvle  46581  ovnhoilem1  46582  ovnhoilem2  46583  ovnlecvr2  46591  hspmbllem2  46608  ovolval2lem  46624  ovnsubadd2lem  46626  ovolval4lem2  46631  ovolval5lem1  46633  ovolval5lem2  46634  ovnovollem1  46637  ovnovollem2  46638  vonioolem1  46661  smflimlem6  46757  smfresal  46769  fsupdm  46823  smfsupdmmbllem  46825  finfdm  46827  smfinfdmmbllem  46829  nnsgrpmgm  48160  nnsgrp  48161  nnsgrpnmnd  48162