Theorem nnex 12254

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 11196	. 2 ⊢ ℂ ∈ V
2		nnsscn 12253	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5295	1 ⊢ ℕ ∈ V

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457  ℂcc 11113  ℕcn 12248

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7742  ax-cnex 11171  ax-1cn 11173  ax-addcl 11175

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7422  df-om 7869  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-nn 12249

This theorem is used by:  dfnn2  12261  nn0ex  12525  nn0ennn  14033  facmapnn  14339  isercolllem2  15741  supcvg  15933  trireciplem  15939  expcnv  15941  geo2lim  15952  qnnen  16291  rpnnen2lem1  16292  rpnnen2lem2  16293  rpnnen  16305  rucALT  16308  prmex  16757  unbenlem  16990  vdwapfval  17053  vdwapf  17054  vdwlem6  17068  vdwlem7  17069  vdwlem8  17070  vdwlem11  17073  prmgaplcm  17142  prmgapprmo  17144  ndxarg  17278  ex-chn2  18716  odfval  19646  odval  19648  gexval  19692  pnrmopn  23550  1stcfb  23652  hausmapdom  23708  met1stc  24729  met2ndci  24730  rectbntr0  25041  metcld2  25517  elovolmlem  25684  ovolctb  25700  ovol0  25703  mbfimaopnlem  25865  itg1climres  25924  mbfi1fseqlem6  25930  mbfi1flimlem  25932  mbfmullem2  25934  itg2monolem1  25960  itg2addlem  25968  plyeq0lem  26418  leibpi  27158  dfef2  27186  emcllem4  27214  emcllem6  27216  emcllem7  27217  lgamgulmlem6  27249  lgamcvg2  27270  basellem6  27301  basellem7  27302  basellem8  27303  basellem9  27304  dchrisumlem3  27706  dirith2  27743  nmounbseqiALT  31201  nmobndseqiALT  31203  h2hcau  31402  h2hlm  31403  hcau  31607  hlimi  31611  hlimadd  31616  hhcms  31626  isch2  31646  chlimi  31657  hlim0  31658  hhsscms  31701  padct  33133  smatfval  34249  lmdvg  34407  esumfsup  34524  esumpcvgval  34532  esumcvg  34540  sigapildsys  34617  measiun  34673  voliune  34684  omssubadd  34755  carsggect  34773  carsgclctunlem2  34774  eulerpartlems  34815  eulerpartleme  34818  eulerpartlem1  34822  eulerpartlemb  34823  eulerpartlemt  34826  eulerpartgbij  34827  eulerpartlemr  34829  eulerpartlemmf  34830  eulerpartlemgvv  34831  eulerpartlemgf  34834  eulerpartlemgs2  34835  eulerpartlemn  34836  reprval  35062  repr0  35063  reprsuc  35067  reprss  35069  reprinrn  35070  reprlt  35071  hashreprin  35072  reprinfz1  35074  reprpmtf1o  35078  reprdifc  35079  breprexplemb  35083  breprexpnat  35086  vtsval  35089  circlemethnat  35093  circlevma  35094  circlemethhgt  35095  sinccvglem  36201  circum  36203  divcnvlin  36262  faclimlem2  36273  faclim2  36277  colinearex  36589  bj-ndxarg  37776  poimirlem32  38360  voliunnfl  38372  volsupnfl  38373  lmclim2  38467  geomcau  38468  rrncmslem  38541  fisdomnn  43070  eldioph3b  43554  lzenom  43559  diophin  43561  diophun  43562  pellexlem3  43616  pellexlem4  43617  pellexlem5  43618  eltrclrec  44464  brtrclrec  44480  iunrelexpmin1  44492  trclrelexplem  44495  dftrcl3  44504  fvtrcllb1d  44506  trclfvcom  44507  cnvtrclfv  44508  cotrcltrcl  44509  trclimalb2  44510  trclfvdecomr  44512  dfrtrcl4  44522  corcltrcl  44523  cotrclrcl  44526  hashnzfzclim  45090  dvradcnv2  45115  binomcxplemcvg  45122  binomcxplemdvsum  45123  binomcxplemnotnn0  45124  ssnnf1octb  45970  clim1fr1  46375  divcnvg  46401  limsup10ex  46545  liminf10ex  46546  wallispilem5  46841  wallispi  46842  stirlinglem1  46846  stirlinglem8  46853  stirlinglem14  46859  stirlinglem15  46860  fourierdlem103  46981  fourierdlem104  46982  fourierdlem112  46990  subsaliuncllem  47129  subsaliuncl  47130  nnfoctbdjlem  47227  nnfoctbdj  47228  ismeannd  47239  voliunsge0lem  47244  caratheodorylem2  47299  isomenndlem  47302  hoicvrrex  47328  ovnsupge0  47329  ovnlecvr  47330  ovn0lem  47337  ovnsubaddlem1  47342  ovnsubadd  47344  sge0hsphoire  47361  hoidmv1lelem1  47363  hoidmv1lelem2  47364  hoidmv1lelem3  47365  hoidmv1le  47366  hoidmvlelem1  47367  hoidmvlelem2  47368  hoidmvlelem3  47369  hoidmvlelem4  47370  hoidmvlelem5  47371  hoidmvle  47372  ovnhoilem1  47373  ovnhoilem2  47374  ovnlecvr2  47382  hspmbllem2  47399  ovolval2lem  47415  ovnsubadd2lem  47417  ovolval4lem2  47422  ovolval5lem1  47424  ovolval5lem2  47425  ovnovollem1  47428  ovnovollem2  47429  vonioolem1  47452  smflimlem6  47548  smfresal  47560  fsupdm  47614  smfsupdmmbllem  47616  finfdm  47618  smfinfdmmbllem  47620  nthrucw  47665  nnsgrpmgm  48998  nnsgrp  48999  nnsgrpnmnd  49000