Theorem nnex 11644

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 10618	. 2 ⊢ ℂ ∈ V
2		nnsscn 11643	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5226	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3494  ℂcc 10535  ℕcn 11638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-1cn 10595  ax-addcl 10597

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-nn 11639

This theorem is referenced by:  dfnn2  11651  nn0ex  11904  nn0ennn  13348  facmapnn  13646  isercolllem2  15022  supcvg  15211  trireciplem  15217  expcnv  15219  geo2lim  15231  qnnen  15566  rpnnen2lem1  15567  rpnnen2lem2  15568  rpnnen  15580  rucALT  15583  prmex  16021  unbenlem  16244  vdwapfval  16307  vdwapf  16308  vdwlem6  16322  vdwlem7  16323  vdwlem8  16324  vdwlem11  16327  prmgaplcm  16396  prmgapprmo  16398  ndxarg  16508  odfval  18660  odval  18662  gexval  18703  pnrmopn  21951  1stcfb  22053  hausmapdom  22108  met1stc  23131  met2ndci  23132  rectbntr0  23440  metcld2  23910  elovolmlem  24075  ovolctb  24091  ovol0  24094  mbfimaopnlem  24256  itg1climres  24315  mbfi1fseqlem6  24321  mbfi1flimlem  24323  mbfmullem2  24325  itg2monolem1  24351  itg2addlem  24359  plyeq0lem  24800  leibpi  25520  dfef2  25548  emcllem4  25576  emcllem6  25578  emcllem7  25579  lgamgulmlem6  25611  lgamcvg2  25632  basellem6  25663  basellem7  25664  basellem8  25665  basellem9  25666  dchrisumlem3  26067  dirith2  26104  nmounbseqiALT  28555  nmobndseqiALT  28557  h2hcau  28756  h2hlm  28757  hcau  28961  hlimi  28965  hlimadd  28970  hhcms  28980  isch2  29000  chlimi  29011  hlim0  29012  hhsscms  29055  padct  30455  smatfval  31060  lmdvg  31196  esumfsup  31329  esumpcvgval  31337  esumcvg  31345  sigapildsys  31421  measiun  31477  voliune  31488  omssubadd  31558  carsggect  31576  carsgclctunlem2  31577  eulerpartlems  31618  eulerpartleme  31621  eulerpartlem1  31625  eulerpartlemb  31626  eulerpartlemt  31629  eulerpartgbij  31630  eulerpartlemr  31632  eulerpartlemmf  31633  eulerpartlemgvv  31634  eulerpartlemgf  31637  eulerpartlemgs2  31638  eulerpartlemn  31639  reprval  31881  repr0  31882  reprsuc  31886  reprss  31888  reprinrn  31889  reprlt  31890  hashreprin  31891  reprinfz1  31893  reprpmtf1o  31897  reprdifc  31898  breprexplemb  31902  breprexpnat  31905  vtsval  31908  circlemethnat  31912  circlevma  31913  circlemethhgt  31914  sinccvglem  32915  circum  32917  divcnvlin  32964  faclimlem2  32976  faclim2  32980  colinearex  33521  bj-ndxarg  34371  poimirlem32  34939  voliunnfl  34951  volsupnfl  34952  lmclim2  35048  geomcau  35049  rrncmslem  35125  eldioph3b  39382  lzenom  39387  diophin  39389  diophun  39390  pellexlem3  39448  pellexlem4  39449  pellexlem5  39450  eltrclrec  40045  brtrclrec  40061  iunrelexpmin1  40073  trclrelexplem  40076  dftrcl3  40085  fvtrcllb1d  40087  trclfvcom  40088  cnvtrclfv  40089  cotrcltrcl  40090  trclimalb2  40091  trclfvdecomr  40093  dfrtrcl4  40103  corcltrcl  40104  cotrclrcl  40107  hashnzfzclim  40674  dvradcnv2  40699  binomcxplemcvg  40706  binomcxplemdvsum  40707  binomcxplemnotnn0  40708  ssnnf1octb  41476  clim1fr1  41902  divcnvg  41928  limsup10ex  42074  liminf10ex  42075  wallispilem5  42374  wallispi  42375  stirlinglem1  42379  stirlinglem8  42386  stirlinglem14  42392  stirlinglem15  42393  fourierdlem103  42514  fourierdlem104  42515  fourierdlem112  42523  subsaliuncllem  42660  subsaliuncl  42661  nnfoctbdjlem  42757  nnfoctbdj  42758  ismeannd  42769  voliunsge0lem  42774  caratheodorylem2  42829  isomenndlem  42832  hoicvrrex  42858  ovnsupge0  42859  ovnlecvr  42860  ovn0lem  42867  ovnsubaddlem1  42872  ovnsubadd  42874  sge0hsphoire  42891  hoidmv1lelem1  42893  hoidmv1lelem2  42894  hoidmv1lelem3  42895  hoidmv1le  42896  hoidmvlelem1  42897  hoidmvlelem2  42898  hoidmvlelem3  42899  hoidmvlelem4  42900  hoidmvlelem5  42901  hoidmvle  42902  ovnhoilem1  42903  ovnhoilem2  42904  ovnlecvr2  42912  hspmbllem2  42929  ovolval2lem  42945  ovnsubadd2lem  42947  ovolval4lem2  42952  ovolval5lem1  42954  ovolval5lem2  42955  ovnovollem1  42958  ovnovollem2  42959  vonioolem1  42982  smflimlem6  43072  smfresal  43083  nnsgrpmgm  44103  nnsgrp  44104  nnsgrpnmnd  44105