Theorem nnex 12381

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 11320	. 2 ⊢ ℂ ∈ V
2		nnsscn 12380	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5291	1 ⊢ ℕ ∈ V

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  ℂcc 11237  ℕcn 12375

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783  ax-cnex 11295  ax-1cn 11297  ax-addcl 11299

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-om 7912  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-nn 12376

This theorem is used by:  dfnn2  12388  nn0ex  12652  nn0ennn  14162  facmapnn  14470  isercolllem2  15877  supcvg  16069  trireciplem  16075  expcnv  16077  geo2lim  16088  qnnen  16425  rpnnen2lem1  16426  rpnnen2lem2  16427  rpnnen  16439  rucALT  16442  prmex  16896  unbenlem  17130  vdwapfval  17193  vdwapf  17194  vdwlem6  17208  vdwlem7  17209  vdwlem8  17210  vdwlem11  17213  prmgaplcm  17282  prmgapprmo  17284  ndxarg  17418  ex-chn2  18862  odfval  19797  odval  19799  gexval  19843  pnrmopn  23716  1stcfb  23818  hausmapdom  23874  met1stc  24895  met2ndci  24896  rectbntr0  25207  metcld2  25683  elovolmlem  25850  ovolctb  25866  ovol0  25869  mbfimaopnlem  26031  itg1climres  26090  mbfi1fseqlem6  26096  mbfi1flimlem  26098  mbfmullem2  26100  itg2monolem1  26126  itg2addlem  26134  plyeq0lem  26584  leibpi  27327  dfef2  27355  emcllem4  27383  emcllem6  27385  emcllem7  27386  lgamgulmlem6  27418  lgamcvg2  27439  basellem6  27470  basellem7  27471  basellem8  27472  basellem9  27473  dchrisumlem3  27875  dirith2  27912  nmounbseqiALT  31437  nmobndseqiALT  31439  h2hcau  31638  h2hlm  31639  hcau  31843  hlimi  31847  hlimadd  31852  hhcms  31862  isch2  31882  chlimi  31893  hlim0  31894  hhsscms  31937  padct  33407  smatfval  34538  lmdvg  34696  esumfsup  34813  esumpcvgval  34821  esumcvg  34829  sigapildsys  34906  measiun  34962  voliune  34973  omssubadd  35043  carsggect  35061  carsgclctunlem2  35062  eulerpartlems  35103  eulerpartleme  35106  eulerpartlem1  35110  eulerpartlemb  35111  eulerpartlemt  35114  eulerpartgbij  35115  eulerpartlemr  35117  eulerpartlemmf  35118  eulerpartlemgvv  35119  eulerpartlemgf  35122  eulerpartlemgs2  35123  eulerpartlemn  35124  reprval  35350  repr0  35351  reprsuc  35355  reprss  35357  reprinrn  35358  reprlt  35359  hashreprin  35360  reprinfz1  35362  reprpmtf1o  35366  reprdifc  35367  breprexplemb  35371  breprexpnat  35374  vtsval  35377  circlemethnat  35381  circlevma  35382  circlemethhgt  35383  sinccvglem  36645  circum  36647  divcnvlin  36713  faclimlem2  36724  faclim2  36728  colinearex  37040  bj-ndxarg  38268  poimirlem32  38838  voliunnfl  38850  volsupnfl  38851  dfproplem  38909  lmclim2  38958  geomcau  38959  rrncmslem  39032  fisdomnn  43562  eldioph3b  44042  lzenom  44047  diophin  44049  diophun  44050  pellexlem3  44104  pellexlem4  44105  pellexlem5  44106  eltrclrec  44941  brtrclrec  44957  iunrelexpmin1  44969  trclrelexplem  44972  dftrcl3  44981  fvtrcllb1d  44983  trclfvcom  44984  cnvtrclfv  44985  cotrcltrcl  44986  trclimalb2  44987  trclfvdecomr  44989  dfrtrcl4  44999  corcltrcl  45000  cotrclrcl  45003  hashnzfzclim  45567  dvradcnv2  45592  binomcxplemcvg  45599  binomcxplemdvsum  45600  binomcxplemnotnn0  45601  ssnnf1octb  46482  clim1fr1  46886  divcnvg  46912  limsup10ex  47056  liminf10ex  47057  wallispilem5  47352  wallispi  47353  stirlinglem1  47357  stirlinglem8  47364  stirlinglem14  47370  stirlinglem15  47371  fourierdlem103  47492  fourierdlem104  47493  fourierdlem112  47501  subsaliuncllem  47640  nnfoctbdjlem  47738  nnfoctbdj  47739  ismeannd  47750  voliunsge0lem  47755  caratheodorylem2  47810  isomenndlem  47813  hoicvrrex  47839  ovnsupge0  47840  ovnlecvr  47841  ovn0lem  47848  ovnsubaddlem1  47853  ovnsubadd  47855  sge0hsphoire  47872  hoidmv1lelem1  47874  hoidmv1lelem2  47875  hoidmv1lelem3  47876  hoidmv1le  47877  hoidmvlelem1  47878  hoidmvlelem2  47879  hoidmvlelem3  47880  hoidmvlelem4  47881  hoidmvlelem5  47882  hoidmvle  47883  ovnhoilem1  47884  ovnhoilem2  47885  ovnlecvr2  47893  hspmbllem2  47910  ovolval2lem  47926  ovnsubadd2lem  47928  ovolval4lem2  47933  ovolval5lem1  47935  ovolval5lem2  47936  ovnovollem1  47939  ovnovollem2  47940  vonioolem1  47963  smfresal  48071  fsupdm  48125  smfsupdmmbllem  48127  finfdm  48129  smfinfdmmbllem  48131  numtowerdt  48189  nnsgrpmgm  49546  nnsgrp  49547  nnsgrpnmnd  49548