Theorem nnex 12249

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 11220	. 2 ⊢ ℂ ∈ V
2		nnsscn 12248	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5322	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2099  Vcvv 3471  ℂcc 11137  ℕcn 12243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pr 5429  ax-un 7740  ax-cnex 11195  ax-1cn 11197  ax-addcl 11199

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-ov 7423  df-om 7871  df-2nd 7994  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-nn 12244

This theorem is referenced by:  dfnn2  12256  nn0ex  12509  nn0ennn  13977  facmapnn  14277  isercolllem2  15645  supcvg  15835  trireciplem  15841  expcnv  15843  geo2lim  15854  qnnen  16190  rpnnen2lem1  16191  rpnnen2lem2  16192  rpnnen  16204  rucALT  16207  prmex  16648  unbenlem  16877  vdwapfval  16940  vdwapf  16941  vdwlem6  16955  vdwlem7  16956  vdwlem8  16957  vdwlem11  16960  prmgaplcm  17029  prmgapprmo  17031  ndxarg  17165  odfval  19487  odval  19489  gexval  19533  pnrmopn  23260  1stcfb  23362  hausmapdom  23417  met1stc  24443  met2ndci  24444  rectbntr0  24761  metcld2  25248  elovolmlem  25416  ovolctb  25432  ovol0  25435  mbfimaopnlem  25597  itg1climres  25657  mbfi1fseqlem6  25663  mbfi1flimlem  25665  mbfmullem2  25667  itg2monolem1  25693  itg2addlem  25701  plyeq0lem  26157  leibpi  26887  dfef2  26916  emcllem4  26944  emcllem6  26946  emcllem7  26947  lgamgulmlem6  26979  lgamcvg2  27000  basellem6  27031  basellem7  27032  basellem8  27033  basellem9  27034  dchrisumlem3  27437  dirith2  27474  nmounbseqiALT  30601  nmobndseqiALT  30603  h2hcau  30802  h2hlm  30803  hcau  31007  hlimi  31011  hlimadd  31016  hhcms  31026  isch2  31046  chlimi  31057  hlim0  31058  hhsscms  31101  padct  32514  smatfval  33396  lmdvg  33554  esumfsup  33689  esumpcvgval  33697  esumcvg  33705  sigapildsys  33781  measiun  33837  voliune  33848  omssubadd  33920  carsggect  33938  carsgclctunlem2  33939  eulerpartlems  33980  eulerpartleme  33983  eulerpartlem1  33987  eulerpartlemb  33988  eulerpartlemt  33991  eulerpartgbij  33992  eulerpartlemr  33994  eulerpartlemmf  33995  eulerpartlemgvv  33996  eulerpartlemgf  33999  eulerpartlemgs2  34000  eulerpartlemn  34001  reprval  34242  repr0  34243  reprsuc  34247  reprss  34249  reprinrn  34250  reprlt  34251  hashreprin  34252  reprinfz1  34254  reprpmtf1o  34258  reprdifc  34259  breprexplemb  34263  breprexpnat  34266  vtsval  34269  circlemethnat  34273  circlevma  34274  circlemethhgt  34275  sinccvglem  35276  circum  35278  divcnvlin  35327  faclimlem2  35338  faclim2  35342  colinearex  35656  bj-ndxarg  36556  poimirlem32  37125  voliunnfl  37137  volsupnfl  37138  lmclim2  37231  geomcau  37232  rrncmslem  37305  eldioph3b  42185  lzenom  42190  diophin  42192  diophun  42193  pellexlem3  42251  pellexlem4  42252  pellexlem5  42253  eltrclrec  43110  brtrclrec  43126  iunrelexpmin1  43138  trclrelexplem  43141  dftrcl3  43150  fvtrcllb1d  43152  trclfvcom  43153  cnvtrclfv  43154  cotrcltrcl  43155  trclimalb2  43156  trclfvdecomr  43158  dfrtrcl4  43168  corcltrcl  43169  cotrclrcl  43172  hashnzfzclim  43759  dvradcnv2  43784  binomcxplemcvg  43791  binomcxplemdvsum  43792  binomcxplemnotnn0  43793  ssnnf1octb  44567  clim1fr1  44989  divcnvg  45015  limsup10ex  45161  liminf10ex  45162  wallispilem5  45457  wallispi  45458  stirlinglem1  45462  stirlinglem8  45469  stirlinglem14  45475  stirlinglem15  45476  fourierdlem103  45597  fourierdlem104  45598  fourierdlem112  45606  subsaliuncllem  45745  subsaliuncl  45746  nnfoctbdjlem  45843  nnfoctbdj  45844  ismeannd  45855  voliunsge0lem  45860  caratheodorylem2  45915  isomenndlem  45918  hoicvrrex  45944  ovnsupge0  45945  ovnlecvr  45946  ovn0lem  45953  ovnsubaddlem1  45958  ovnsubadd  45960  sge0hsphoire  45977  hoidmv1lelem1  45979  hoidmv1lelem2  45980  hoidmv1lelem3  45981  hoidmv1le  45982  hoidmvlelem1  45983  hoidmvlelem2  45984  hoidmvlelem3  45985  hoidmvlelem4  45986  hoidmvlelem5  45987  hoidmvle  45988  ovnhoilem1  45989  ovnhoilem2  45990  ovnlecvr2  45998  hspmbllem2  46015  ovolval2lem  46031  ovnsubadd2lem  46033  ovolval4lem2  46038  ovolval5lem1  46040  ovolval5lem2  46041  ovnovollem1  46044  ovnovollem2  46045  vonioolem1  46068  smflimlem6  46164  smfresal  46176  fsupdm  46230  smfsupdmmbllem  46232  finfdm  46234  smfinfdmmbllem  46236  nnsgrpmgm  47238  nnsgrp  47239  nnsgrpnmnd  47240