Theorem nnex 12334

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 11274	. 2 ⊢ ℂ ∈ V
2		nnsscn 12333	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5284	1 ⊢ ℕ ∈ V

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  ℂcc 11191  ℕcn 12328

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7749  ax-cnex 11249  ax-1cn 11251  ax-addcl 11253

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7421  df-om 7876  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-nn 12329

This theorem is used by:  dfnn2  12341  nn0ex  12605  nn0ennn  14115  facmapnn  14422  isercolllem2  15826  supcvg  16018  trireciplem  16024  expcnv  16026  geo2lim  16037  qnnen  16374  rpnnen2lem1  16375  rpnnen2lem2  16376  rpnnen  16388  rucALT  16391  prmex  16845  unbenlem  17079  vdwapfval  17142  vdwapf  17143  vdwlem6  17157  vdwlem7  17158  vdwlem8  17159  vdwlem11  17162  prmgaplcm  17231  prmgapprmo  17233  ndxarg  17367  ex-chn2  18805  odfval  19739  odval  19741  gexval  19785  pnrmopn  23654  1stcfb  23756  hausmapdom  23812  met1stc  24833  met2ndci  24834  rectbntr0  25145  metcld2  25621  elovolmlem  25788  ovolctb  25804  ovol0  25807  mbfimaopnlem  25969  itg1climres  26028  mbfi1fseqlem6  26034  mbfi1flimlem  26036  mbfmullem2  26038  itg2monolem1  26064  itg2addlem  26072  plyeq0lem  26522  leibpi  27263  dfef2  27291  emcllem4  27319  emcllem6  27321  emcllem7  27322  lgamgulmlem6  27354  lgamcvg2  27375  basellem6  27406  basellem7  27407  basellem8  27408  basellem9  27409  dchrisumlem3  27811  dirith2  27848  nmounbseqiALT  31373  nmobndseqiALT  31375  h2hcau  31574  h2hlm  31575  hcau  31779  hlimi  31783  hlimadd  31788  hhcms  31798  isch2  31818  chlimi  31829  hlim0  31830  hhsscms  31873  padct  33303  smatfval  34420  lmdvg  34578  esumfsup  34695  esumpcvgval  34703  esumcvg  34711  sigapildsys  34788  measiun  34844  voliune  34855  omssubadd  34925  carsggect  34943  carsgclctunlem2  34944  eulerpartlems  34985  eulerpartleme  34988  eulerpartlem1  34992  eulerpartlemb  34993  eulerpartlemt  34996  eulerpartgbij  34997  eulerpartlemr  34999  eulerpartlemmf  35000  eulerpartlemgvv  35001  eulerpartlemgf  35004  eulerpartlemgs2  35005  eulerpartlemn  35006  reprval  35232  repr0  35233  reprsuc  35237  reprss  35239  reprinrn  35240  reprlt  35241  hashreprin  35242  reprinfz1  35244  reprpmtf1o  35248  reprdifc  35249  breprexplemb  35253  breprexpnat  35256  vtsval  35259  circlemethnat  35263  circlevma  35264  circlemethhgt  35265  sinccvglem  36416  circum  36418  divcnvlin  36477  faclimlem2  36488  faclim2  36492  colinearex  36805  bj-ndxarg  37978  poimirlem32  38550  voliunnfl  38562  volsupnfl  38563  dfproplem  38621  lmclim2  38672  geomcau  38673  rrncmslem  38746  fisdomnn  43275  eldioph3b  43755  lzenom  43760  diophin  43762  diophun  43763  pellexlem3  43817  pellexlem4  43818  pellexlem5  43819  eltrclrec  44665  brtrclrec  44681  iunrelexpmin1  44693  trclrelexplem  44696  dftrcl3  44705  fvtrcllb1d  44707  trclfvcom  44708  cnvtrclfv  44709  cotrcltrcl  44710  trclimalb2  44711  trclfvdecomr  44713  dfrtrcl4  44723  corcltrcl  44724  cotrclrcl  44727  hashnzfzclim  45291  dvradcnv2  45316  binomcxplemcvg  45323  binomcxplemdvsum  45324  binomcxplemnotnn0  45325  ssnnf1octb  46178  clim1fr1  46582  divcnvg  46608  limsup10ex  46752  liminf10ex  46753  wallispilem5  47048  wallispi  47049  stirlinglem1  47053  stirlinglem8  47060  stirlinglem14  47066  stirlinglem15  47067  fourierdlem103  47188  fourierdlem104  47189  fourierdlem112  47197  subsaliuncllem  47336  nnfoctbdjlem  47434  nnfoctbdj  47435  ismeannd  47446  voliunsge0lem  47451  caratheodorylem2  47506  isomenndlem  47509  hoicvrrex  47535  ovnsupge0  47536  ovnlecvr  47537  ovn0lem  47544  ovnsubaddlem1  47549  ovnsubadd  47551  sge0hsphoire  47568  hoidmv1lelem1  47570  hoidmv1lelem2  47571  hoidmv1lelem3  47572  hoidmv1le  47573  hoidmvlelem1  47574  hoidmvlelem2  47575  hoidmvlelem3  47576  hoidmvlelem4  47577  hoidmvlelem5  47578  hoidmvle  47579  ovnhoilem1  47580  ovnhoilem2  47581  ovnlecvr2  47589  hspmbllem2  47606  ovolval2lem  47622  ovnsubadd2lem  47624  ovolval4lem2  47629  ovolval5lem1  47631  ovolval5lem2  47632  ovnovollem1  47635  ovnovollem2  47636  vonioolem1  47659  smfresal  47767  fsupdm  47821  smfsupdmmbllem  47823  finfdm  47825  smfinfdmmbllem  47827  numtowerdt  47885  nnsgrpmgm  49242  nnsgrp  49243  nnsgrpnmnd  49244