Theorem nnex 11442

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 10412	. 2 ⊢ ℂ ∈ V
2		nnsscn 11440	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5080	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2048  Vcvv 3412  ℂcc 10329  ℕcn 11435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-sep 5058  ax-nul 5065  ax-pow 5117  ax-pr 5184  ax-un 7277  ax-cnex 10387  ax-1cn 10389  ax-addcl 10391

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ne 2965  df-ral 3090  df-rex 3091  df-reu 3092  df-rab 3094  df-v 3414  df-sbc 3681  df-csb 3786  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-pss 3844  df-nul 4178  df-if 4349  df-pw 4422  df-sn 4440  df-pr 4442  df-tp 4444  df-op 4446  df-uni 4711  df-iun 4792  df-br 4928  df-opab 4990  df-mpt 5007  df-tr 5029  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-ov 6977  df-om 7395  df-wrecs 7747  df-recs 7809  df-rdg 7847  df-nn 11436

This theorem is referenced by:  dfnn2  11450  nn0ex  11711  nn0ennn  13159  facmapnn  13457  isercolllem2  14877  supcvg  15065  trireciplem  15071  expcnv  15073  geo2lim  15085  qnnen  15420  rpnnen2lem1  15421  rpnnen2lem2  15422  rpnnen  15434  rucALT  15437  prmex  15871  unbenlem  16094  vdwapfval  16157  vdwapf  16158  vdwlem6  16172  vdwlem7  16173  vdwlem8  16174  vdwlem11  16177  prmgaplcm  16246  prmgapprmo  16248  ndxarg  16358  odfval  18416  odval  18418  gexval  18458  pnrmopn  21649  1stcfb  21751  hausmapdom  21806  met1stc  22828  met2ndci  22829  rectbntr0  23137  metcld2  23607  elovolmlem  23772  ovolctb  23788  ovol0  23791  mbfimaopnlem  23953  itg1climres  24012  mbfi1fseqlem6  24018  mbfi1flimlem  24020  mbfmullem2  24022  itg2monolem1  24048  itg2addlem  24056  plyeq0lem  24497  leibpi  25216  dfef2  25244  emcllem4  25272  emcllem6  25274  emcllem7  25275  lgamgulmlem6  25307  lgamcvg2  25328  basellem6  25359  basellem7  25360  basellem8  25361  basellem9  25362  dchrisumlem3  25763  dirith2  25800  nmounbseqiALT  28326  nmobndseqiALT  28328  h2hcau  28529  h2hlm  28530  hcau  28734  hlimi  28738  hlimadd  28743  hhcms  28753  isch2  28773  chlimi  28784  hlim0  28785  hhsscms  28829  padct  30201  smatfval  30693  lmdvg  30831  esumfsup  30964  esumpcvgval  30972  esumcvg  30980  sigapildsys  31057  measiun  31113  voliune  31124  omssubadd  31194  carsggect  31212  carsgclctunlem2  31213  eulerpartlems  31254  eulerpartleme  31257  eulerpartlem1  31261  eulerpartlemb  31262  eulerpartlemt  31265  eulerpartgbij  31266  eulerpartlemr  31268  eulerpartlemmf  31269  eulerpartlemgvv  31270  eulerpartlemgf  31273  eulerpartlemgs2  31274  eulerpartlemn  31275  reprval  31520  repr0  31521  reprsuc  31525  reprss  31527  reprinrn  31528  reprlt  31529  hashreprin  31530  reprinfz1  31532  reprpmtf1o  31536  reprdifc  31537  breprexplemb  31541  breprexpnat  31544  vtsval  31547  circlemethnat  31551  circlevma  31552  circlemethhgt  31553  sinccvglem  32405  circum  32407  divcnvlin  32454  faclimlem2  32466  faclim2  32470  colinearex  33012  bj-ndxarg  33842  poimirlem32  34343  voliunnfl  34355  volsupnfl  34356  lmclim2  34453  geomcau  34454  rrncmslem  34530  eldioph3b  38735  lzenom  38740  diophin  38743  diophun  38744  pellexlem3  38802  pellexlem4  38803  pellexlem5  38804  eltrclrec  39366  brtrclrec  39382  iunrelexpmin1  39394  trclrelexplem  39397  dftrcl3  39406  fvtrcllb1d  39408  trclfvcom  39409  cnvtrclfv  39410  cotrcltrcl  39411  trclimalb2  39412  trclfvdecomr  39414  dfrtrcl4  39424  corcltrcl  39425  cotrclrcl  39428  hashnzfzclim  40047  dvradcnv2  40072  binomcxplemcvg  40079  binomcxplemdvsum  40080  binomcxplemnotnn0  40081  ssnnf1octb  40859  clim1fr1  41292  divcnvg  41318  limsup10ex  41464  liminf10ex  41465  wallispilem5  41764  wallispi  41765  stirlinglem1  41769  stirlinglem8  41776  stirlinglem14  41782  stirlinglem15  41783  fourierdlem103  41904  fourierdlem104  41905  fourierdlem112  41913  subsaliuncllem  42050  subsaliuncl  42051  nnfoctbdjlem  42147  nnfoctbdj  42148  ismeannd  42159  voliunsge0lem  42164  caratheodorylem2  42219  isomenndlem  42222  hoicvrrex  42248  ovnsupge0  42249  ovnlecvr  42250  ovn0lem  42257  ovnsubaddlem1  42262  ovnsubadd  42264  sge0hsphoire  42281  hoidmv1lelem1  42283  hoidmv1lelem2  42284  hoidmv1lelem3  42285  hoidmv1le  42286  hoidmvlelem1  42287  hoidmvlelem2  42288  hoidmvlelem3  42289  hoidmvlelem4  42290  hoidmvlelem5  42291  hoidmvle  42292  ovnhoilem1  42293  ovnhoilem2  42294  ovnlecvr2  42302  hspmbllem2  42319  ovolval2lem  42335  ovnsubadd2lem  42337  ovolval4lem2  42342  ovolval5lem1  42344  ovolval5lem2  42345  ovnovollem1  42348  ovnovollem2  42349  vonioolem1  42372  smflimlem6  42462  smfresal  42473  nnsgrpmgm  43425  nnsgrp  43426  nnsgrpnmnd  43427