Theorem nnex 12216

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 11154	. 2 ⊢ ℂ ∈ V
2		nnsscn 12215	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5278	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2142  Vcvv 3454  ℂcc 11071  ℕcn 12210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-un 7718  ax-cnex 11129  ax-1cn 11131  ax-addcl 11133

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-ov 7399  df-om 7847  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-nn 12211

This theorem is referenced by:  dfnn2  12223  nn0ex  12487  nn0ennn  13992  facmapnn  14298  isercolllem2  15693  supcvg  15886  trireciplem  15892  expcnv  15894  geo2lim  15905  qnnen  16245  rpnnen2lem1  16246  rpnnen2lem2  16247  rpnnen  16259  rucALT  16262  prmex  16711  unbenlem  16944  vdwapfval  17007  vdwapf  17008  vdwlem6  17022  vdwlem7  17023  vdwlem8  17024  vdwlem11  17027  prmgaplcm  17096  prmgapprmo  17098  ndxarg  17232  ex-chn2  18670  odfval  19572  odval  19574  gexval  19618  pnrmopn  23400  1stcfb  23502  hausmapdom  23557  met1stc  24578  met2ndci  24579  rectbntr0  24890  metcld2  25366  elovolmlem  25533  ovolctb  25549  ovol0  25552  mbfimaopnlem  25714  itg1climres  25773  mbfi1fseqlem6  25779  mbfi1flimlem  25781  mbfmullem2  25783  itg2monolem1  25809  itg2addlem  25817  plyeq0lem  26267  leibpi  27004  dfef2  27032  emcllem4  27060  emcllem6  27062  emcllem7  27063  lgamgulmlem6  27095  lgamcvg2  27116  basellem6  27147  basellem7  27148  basellem8  27149  basellem9  27150  dchrisumlem3  27552  dirith2  27589  nmounbseqiALT  30978  nmobndseqiALT  30980  h2hcau  31179  h2hlm  31180  hcau  31384  hlimi  31388  hlimadd  31393  hhcms  31403  isch2  31423  chlimi  31434  hlim0  31435  hhsscms  31478  padct  32917  smatfval  34089  lmdvg  34247  esumfsup  34364  esumpcvgval  34372  esumcvg  34380  sigapildsys  34456  measiun  34512  voliune  34523  omssubadd  34594  carsggect  34612  carsgclctunlem2  34613  eulerpartlems  34654  eulerpartleme  34657  eulerpartlem1  34661  eulerpartlemb  34662  eulerpartlemt  34665  eulerpartgbij  34666  eulerpartlemr  34668  eulerpartlemmf  34669  eulerpartlemgvv  34670  eulerpartlemgf  34673  eulerpartlemgs2  34674  eulerpartlemn  34675  reprval  34901  repr0  34902  reprsuc  34906  reprss  34908  reprinrn  34909  reprlt  34910  hashreprin  34911  reprinfz1  34913  reprpmtf1o  34917  reprdifc  34918  breprexplemb  34922  breprexpnat  34925  vtsval  34928  circlemethnat  34932  circlevma  34933  circlemethhgt  34934  sinccvglem  36019  circum  36021  divcnvlin  36080  faclimlem2  36091  faclim2  36095  colinearex  36407  bj-ndxarg  37564  poimirlem32  38148  voliunnfl  38160  volsupnfl  38161  lmclim2  38254  geomcau  38255  rrncmslem  38328  fisdomnn  42857  eldioph3b  43343  lzenom  43348  diophin  43350  diophun  43351  pellexlem3  43405  pellexlem4  43406  pellexlem5  43407  eltrclrec  44253  brtrclrec  44269  iunrelexpmin1  44281  trclrelexplem  44284  dftrcl3  44293  fvtrcllb1d  44295  trclfvcom  44296  cnvtrclfv  44297  cotrcltrcl  44298  trclimalb2  44299  trclfvdecomr  44301  dfrtrcl4  44311  corcltrcl  44312  cotrclrcl  44315  hashnzfzclim  44895  dvradcnv2  44920  binomcxplemcvg  44927  binomcxplemdvsum  44928  binomcxplemnotnn0  44929  ssnnf1octb  45769  clim1fr1  46174  divcnvg  46200  limsup10ex  46344  liminf10ex  46345  wallispilem5  46640  wallispi  46641  stirlinglem1  46645  stirlinglem8  46652  stirlinglem14  46658  stirlinglem15  46659  fourierdlem103  46780  fourierdlem104  46781  fourierdlem112  46789  subsaliuncllem  46928  subsaliuncl  46929  nnfoctbdjlem  47026  nnfoctbdj  47027  ismeannd  47038  voliunsge0lem  47043  caratheodorylem2  47098  isomenndlem  47101  hoicvrrex  47127  ovnsupge0  47128  ovnlecvr  47129  ovn0lem  47136  ovnsubaddlem1  47141  ovnsubadd  47143  sge0hsphoire  47160  hoidmv1lelem1  47162  hoidmv1lelem2  47163  hoidmv1lelem3  47164  hoidmv1le  47165  hoidmvlelem1  47166  hoidmvlelem2  47167  hoidmvlelem3  47168  hoidmvlelem4  47169  hoidmvlelem5  47170  hoidmvle  47171  ovnhoilem1  47172  ovnhoilem2  47173  ovnlecvr2  47181  hspmbllem2  47198  ovolval2lem  47214  ovnsubadd2lem  47216  ovolval4lem2  47221  ovolval5lem1  47223  ovolval5lem2  47224  ovnovollem1  47227  ovnovollem2  47228  vonioolem1  47251  smflimlem6  47347  smfresal  47359  fsupdm  47413  smfsupdmmbllem  47415  finfdm  47417  smfinfdmmbllem  47419  nthrucw  47459  nnsgrpmgm  48795  nnsgrp  48796  nnsgrpnmnd  48797