Theorem nnex 12199

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 11156	. 2 ⊢ ℂ ∈ V
2		nnsscn 12198	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5280	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3450  ℂcc 11073  ℕcn 12193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-1cn 11133  ax-addcl 11135

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-nn 12194

This theorem is referenced by:  dfnn2  12206  nn0ex  12455  nn0ennn  13951  facmapnn  14257  isercolllem2  15639  supcvg  15829  trireciplem  15835  expcnv  15837  geo2lim  15848  qnnen  16188  rpnnen2lem1  16189  rpnnen2lem2  16190  rpnnen  16202  rucALT  16205  prmex  16654  unbenlem  16886  vdwapfval  16949  vdwapf  16950  vdwlem6  16964  vdwlem7  16965  vdwlem8  16966  vdwlem11  16969  prmgaplcm  17038  prmgapprmo  17040  ndxarg  17173  odfval  19469  odval  19471  gexval  19515  pnrmopn  23237  1stcfb  23339  hausmapdom  23394  met1stc  24416  met2ndci  24417  rectbntr0  24728  metcld2  25214  elovolmlem  25382  ovolctb  25398  ovol0  25401  mbfimaopnlem  25563  itg1climres  25622  mbfi1fseqlem6  25628  mbfi1flimlem  25630  mbfmullem2  25632  itg2monolem1  25658  itg2addlem  25666  plyeq0lem  26122  leibpi  26859  dfef2  26888  emcllem4  26916  emcllem6  26918  emcllem7  26919  lgamgulmlem6  26951  lgamcvg2  26972  basellem6  27003  basellem7  27004  basellem8  27005  basellem9  27006  dchrisumlem3  27409  dirith2  27446  nmounbseqiALT  30714  nmobndseqiALT  30716  h2hcau  30915  h2hlm  30916  hcau  31120  hlimi  31124  hlimadd  31129  hhcms  31139  isch2  31159  chlimi  31170  hlim0  31171  hhsscms  31214  padct  32650  smatfval  33792  lmdvg  33950  esumfsup  34067  esumpcvgval  34075  esumcvg  34083  sigapildsys  34159  measiun  34215  voliune  34226  omssubadd  34298  carsggect  34316  carsgclctunlem2  34317  eulerpartlems  34358  eulerpartleme  34361  eulerpartlem1  34365  eulerpartlemb  34366  eulerpartlemt  34369  eulerpartgbij  34370  eulerpartlemr  34372  eulerpartlemmf  34373  eulerpartlemgvv  34374  eulerpartlemgf  34377  eulerpartlemgs2  34378  eulerpartlemn  34379  reprval  34608  repr0  34609  reprsuc  34613  reprss  34615  reprinrn  34616  reprlt  34617  hashreprin  34618  reprinfz1  34620  reprpmtf1o  34624  reprdifc  34625  breprexplemb  34629  breprexpnat  34632  vtsval  34635  circlemethnat  34639  circlevma  34640  circlemethhgt  34641  sinccvglem  35666  circum  35668  divcnvlin  35727  faclimlem2  35738  faclim2  35742  colinearex  36055  bj-ndxarg  37072  poimirlem32  37653  voliunnfl  37665  volsupnfl  37666  lmclim2  37759  geomcau  37760  rrncmslem  37833  fisdomnn  42239  eldioph3b  42760  lzenom  42765  diophin  42767  diophun  42768  pellexlem3  42826  pellexlem4  42827  pellexlem5  42828  eltrclrec  43676  brtrclrec  43692  iunrelexpmin1  43704  trclrelexplem  43707  dftrcl3  43716  fvtrcllb1d  43718  trclfvcom  43719  cnvtrclfv  43720  cotrcltrcl  43721  trclimalb2  43722  trclfvdecomr  43724  dfrtrcl4  43734  corcltrcl  43735  cotrclrcl  43738  hashnzfzclim  44318  dvradcnv2  44343  binomcxplemcvg  44350  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  ssnnf1octb  45195  clim1fr1  45606  divcnvg  45632  limsup10ex  45778  liminf10ex  45779  wallispilem5  46074  wallispi  46075  stirlinglem1  46079  stirlinglem8  46086  stirlinglem14  46092  stirlinglem15  46093  fourierdlem103  46214  fourierdlem104  46215  fourierdlem112  46223  subsaliuncllem  46362  subsaliuncl  46363  nnfoctbdjlem  46460  nnfoctbdj  46461  ismeannd  46472  voliunsge0lem  46477  caratheodorylem2  46532  isomenndlem  46535  hoicvrrex  46561  ovnsupge0  46562  ovnlecvr  46563  ovn0lem  46570  ovnsubaddlem1  46575  ovnsubadd  46577  sge0hsphoire  46594  hoidmv1lelem1  46596  hoidmv1lelem2  46597  hoidmv1lelem3  46598  hoidmv1le  46599  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem4  46603  hoidmvlelem5  46604  hoidmvle  46605  ovnhoilem1  46606  ovnhoilem2  46607  ovnlecvr2  46615  hspmbllem2  46632  ovolval2lem  46648  ovnsubadd2lem  46650  ovolval4lem2  46655  ovolval5lem1  46657  ovolval5lem2  46658  ovnovollem1  46661  ovnovollem2  46662  vonioolem1  46685  smflimlem6  46781  smfresal  46793  fsupdm  46847  smfsupdmmbllem  46849  finfdm  46851  smfinfdmmbllem  46853  nnsgrpmgm  48168  nnsgrp  48169  nnsgrpnmnd  48170