Theorem nnex 12169

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 11108	. 2 ⊢ ℂ ∈ V
2		nnsscn 12168	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5257	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3430  ℂcc 11025  ℕcn 12163

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5368  ax-un 7680  ax-cnex 11083  ax-1cn 11085  ax-addcl 11087

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8222  df-wrecs 8253  df-recs 8302  df-rdg 8340  df-nn 12164

This theorem is referenced by:  dfnn2  12176  nn0ex  12432  nn0ennn  13930  facmapnn  14236  isercolllem2  15617  supcvg  15810  trireciplem  15816  expcnv  15818  geo2lim  15829  qnnen  16169  rpnnen2lem1  16170  rpnnen2lem2  16171  rpnnen  16183  rucALT  16186  prmex  16635  unbenlem  16868  vdwapfval  16931  vdwapf  16932  vdwlem6  16946  vdwlem7  16947  vdwlem8  16948  vdwlem11  16951  prmgaplcm  17020  prmgapprmo  17022  ndxarg  17155  ex-chn2  18593  odfval  19496  odval  19498  gexval  19542  pnrmopn  23317  1stcfb  23419  hausmapdom  23474  met1stc  24495  met2ndci  24496  rectbntr0  24807  metcld2  25283  elovolmlem  25450  ovolctb  25466  ovol0  25469  mbfimaopnlem  25631  itg1climres  25690  mbfi1fseqlem6  25696  mbfi1flimlem  25698  mbfmullem2  25700  itg2monolem1  25726  itg2addlem  25734  plyeq0lem  26187  leibpi  26923  dfef2  26952  emcllem4  26980  emcllem6  26982  emcllem7  26983  lgamgulmlem6  27015  lgamcvg2  27036  basellem6  27067  basellem7  27068  basellem8  27069  basellem9  27070  dchrisumlem3  27473  dirith2  27510  nmounbseqiALT  30869  nmobndseqiALT  30871  h2hcau  31070  h2hlm  31071  hcau  31275  hlimi  31279  hlimadd  31284  hhcms  31294  isch2  31314  chlimi  31325  hlim0  31326  hhsscms  31369  padct  32811  smatfval  33960  lmdvg  34118  esumfsup  34235  esumpcvgval  34243  esumcvg  34251  sigapildsys  34327  measiun  34383  voliune  34394  omssubadd  34465  carsggect  34483  carsgclctunlem2  34484  eulerpartlems  34525  eulerpartleme  34528  eulerpartlem1  34532  eulerpartlemb  34533  eulerpartlemt  34536  eulerpartgbij  34537  eulerpartlemr  34539  eulerpartlemmf  34540  eulerpartlemgvv  34541  eulerpartlemgf  34544  eulerpartlemgs2  34545  eulerpartlemn  34546  reprval  34775  repr0  34776  reprsuc  34780  reprss  34782  reprinrn  34783  reprlt  34784  hashreprin  34785  reprinfz1  34787  reprpmtf1o  34791  reprdifc  34792  breprexplemb  34796  breprexpnat  34799  vtsval  34802  circlemethnat  34806  circlevma  34807  circlemethhgt  34808  sinccvglem  35875  circum  35877  divcnvlin  35936  faclimlem2  35947  faclim2  35951  colinearex  36263  bj-ndxarg  37402  poimirlem32  37984  voliunnfl  37996  volsupnfl  37997  lmclim2  38090  geomcau  38091  rrncmslem  38164  fisdomnn  42694  eldioph3b  43208  lzenom  43213  diophin  43215  diophun  43216  pellexlem3  43274  pellexlem4  43275  pellexlem5  43276  eltrclrec  44122  brtrclrec  44138  iunrelexpmin1  44150  trclrelexplem  44153  dftrcl3  44162  fvtrcllb1d  44164  trclfvcom  44165  cnvtrclfv  44166  cotrcltrcl  44167  trclimalb2  44168  trclfvdecomr  44170  dfrtrcl4  44180  corcltrcl  44181  cotrclrcl  44184  hashnzfzclim  44764  dvradcnv2  44789  binomcxplemcvg  44796  binomcxplemdvsum  44797  binomcxplemnotnn0  44798  ssnnf1octb  45639  clim1fr1  46046  divcnvg  46072  limsup10ex  46216  liminf10ex  46217  wallispilem5  46512  wallispi  46513  stirlinglem1  46517  stirlinglem8  46524  stirlinglem14  46530  stirlinglem15  46531  fourierdlem103  46652  fourierdlem104  46653  fourierdlem112  46661  subsaliuncllem  46800  subsaliuncl  46801  nnfoctbdjlem  46898  nnfoctbdj  46899  ismeannd  46910  voliunsge0lem  46915  caratheodorylem2  46970  isomenndlem  46973  hoicvrrex  46999  ovnsupge0  47000  ovnlecvr  47001  ovn0lem  47008  ovnsubaddlem1  47013  ovnsubadd  47015  sge0hsphoire  47032  hoidmv1lelem1  47034  hoidmv1lelem2  47035  hoidmv1lelem3  47036  hoidmv1le  47037  hoidmvlelem1  47038  hoidmvlelem2  47039  hoidmvlelem3  47040  hoidmvlelem4  47041  hoidmvlelem5  47042  hoidmvle  47043  ovnhoilem1  47044  ovnhoilem2  47045  ovnlecvr2  47053  hspmbllem2  47070  ovolval2lem  47086  ovnsubadd2lem  47088  ovolval4lem2  47093  ovolval5lem1  47095  ovolval5lem2  47096  ovnovollem1  47099  ovnovollem2  47100  vonioolem1  47123  smflimlem6  47219  smfresal  47231  fsupdm  47285  smfsupdmmbllem  47287  finfdm  47289  smfinfdmmbllem  47291  nthrucw  47329  nnsgrpmgm  48649  nnsgrp  48650  nnsgrpnmnd  48651