Theorem nnex 12168

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 11125	. 2 ⊢ ℂ ∈ V
2		nnsscn 12167	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5272	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3444  ℂcc 11042  ℕcn 12162

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 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-1cn 11102  ax-addcl 11104

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 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-nn 12163

This theorem is referenced by:  dfnn2  12175  nn0ex  12424  nn0ennn  13920  facmapnn  14226  isercolllem2  15608  supcvg  15798  trireciplem  15804  expcnv  15806  geo2lim  15817  qnnen  16157  rpnnen2lem1  16158  rpnnen2lem2  16159  rpnnen  16171  rucALT  16174  prmex  16623  unbenlem  16855  vdwapfval  16918  vdwapf  16919  vdwlem6  16933  vdwlem7  16934  vdwlem8  16935  vdwlem11  16938  prmgaplcm  17007  prmgapprmo  17009  ndxarg  17142  odfval  19438  odval  19440  gexval  19484  pnrmopn  23206  1stcfb  23308  hausmapdom  23363  met1stc  24385  met2ndci  24386  rectbntr0  24697  metcld2  25183  elovolmlem  25351  ovolctb  25367  ovol0  25370  mbfimaopnlem  25532  itg1climres  25591  mbfi1fseqlem6  25597  mbfi1flimlem  25599  mbfmullem2  25601  itg2monolem1  25627  itg2addlem  25635  plyeq0lem  26091  leibpi  26828  dfef2  26857  emcllem4  26885  emcllem6  26887  emcllem7  26888  lgamgulmlem6  26920  lgamcvg2  26941  basellem6  26972  basellem7  26973  basellem8  26974  basellem9  26975  dchrisumlem3  27378  dirith2  27415  nmounbseqiALT  30680  nmobndseqiALT  30682  h2hcau  30881  h2hlm  30882  hcau  31086  hlimi  31090  hlimadd  31095  hhcms  31105  isch2  31125  chlimi  31136  hlim0  31137  hhsscms  31180  padct  32616  smatfval  33758  lmdvg  33916  esumfsup  34033  esumpcvgval  34041  esumcvg  34049  sigapildsys  34125  measiun  34181  voliune  34192  omssubadd  34264  carsggect  34282  carsgclctunlem2  34283  eulerpartlems  34324  eulerpartleme  34327  eulerpartlem1  34331  eulerpartlemb  34332  eulerpartlemt  34335  eulerpartgbij  34336  eulerpartlemr  34338  eulerpartlemmf  34339  eulerpartlemgvv  34340  eulerpartlemgf  34343  eulerpartlemgs2  34344  eulerpartlemn  34345  reprval  34574  repr0  34575  reprsuc  34579  reprss  34581  reprinrn  34582  reprlt  34583  hashreprin  34584  reprinfz1  34586  reprpmtf1o  34590  reprdifc  34591  breprexplemb  34595  breprexpnat  34598  vtsval  34601  circlemethnat  34605  circlevma  34606  circlemethhgt  34607  sinccvglem  35632  circum  35634  divcnvlin  35693  faclimlem2  35704  faclim2  35708  colinearex  36021  bj-ndxarg  37038  poimirlem32  37619  voliunnfl  37631  volsupnfl  37632  lmclim2  37725  geomcau  37726  rrncmslem  37799  fisdomnn  42205  eldioph3b  42726  lzenom  42731  diophin  42733  diophun  42734  pellexlem3  42792  pellexlem4  42793  pellexlem5  42794  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  44284  dvradcnv2  44309  binomcxplemcvg  44316  binomcxplemdvsum  44317  binomcxplemnotnn0  44318  ssnnf1octb  45161  clim1fr1  45572  divcnvg  45598  limsup10ex  45744  liminf10ex  45745  wallispilem5  46040  wallispi  46041  stirlinglem1  46045  stirlinglem8  46052  stirlinglem14  46058  stirlinglem15  46059  fourierdlem103  46180  fourierdlem104  46181  fourierdlem112  46189  subsaliuncllem  46328  subsaliuncl  46329  nnfoctbdjlem  46426  nnfoctbdj  46427  ismeannd  46438  voliunsge0lem  46443  caratheodorylem2  46498  isomenndlem  46501  hoicvrrex  46527  ovnsupge0  46528  ovnlecvr  46529  ovn0lem  46536  ovnsubaddlem1  46541  ovnsubadd  46543  sge0hsphoire  46560  hoidmv1lelem1  46562  hoidmv1lelem2  46563  hoidmv1lelem3  46564  hoidmv1le  46565  hoidmvlelem1  46566  hoidmvlelem2  46567  hoidmvlelem3  46568  hoidmvlelem4  46569  hoidmvlelem5  46570  hoidmvle  46571  ovnhoilem1  46572  ovnhoilem2  46573  ovnlecvr2  46581  hspmbllem2  46598  ovolval2lem  46614  ovnsubadd2lem  46616  ovolval4lem2  46621  ovolval5lem1  46623  ovolval5lem2  46624  ovnovollem1  46627  ovnovollem2  46628  vonioolem1  46651  smflimlem6  46747  smfresal  46759  fsupdm  46813  smfsupdmmbllem  46815  finfdm  46817  smfinfdmmbllem  46819  nnsgrpmgm  48137  nnsgrp  48138  nnsgrpnmnd  48139