Theorem nnex 12168

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 11125	. 2 ⊢ ℂ ∈ V
2		nnsscn 12167	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5272	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3444  ℂcc 11042  ℕcn 12162

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 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-1cn 11102  ax-addcl 11104

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-nn 12163

This theorem is referenced by:  dfnn2  12175  nn0ex  12424  nn0ennn  13920  facmapnn  14226  isercolllem2  15608  supcvg  15798  trireciplem  15804  expcnv  15806  geo2lim  15817  qnnen  16157  rpnnen2lem1  16158  rpnnen2lem2  16159  rpnnen  16171  rucALT  16174  prmex  16623  unbenlem  16855  vdwapfval  16918  vdwapf  16919  vdwlem6  16933  vdwlem7  16934  vdwlem8  16935  vdwlem11  16938  prmgaplcm  17007  prmgapprmo  17009  ndxarg  17142  odfval  19446  odval  19448  gexval  19492  pnrmopn  23263  1stcfb  23365  hausmapdom  23420  met1stc  24442  met2ndci  24443  rectbntr0  24754  metcld2  25240  elovolmlem  25408  ovolctb  25424  ovol0  25427  mbfimaopnlem  25589  itg1climres  25648  mbfi1fseqlem6  25654  mbfi1flimlem  25656  mbfmullem2  25658  itg2monolem1  25684  itg2addlem  25692  plyeq0lem  26148  leibpi  26885  dfef2  26914  emcllem4  26942  emcllem6  26944  emcllem7  26945  lgamgulmlem6  26977  lgamcvg2  26998  basellem6  27029  basellem7  27030  basellem8  27031  basellem9  27032  dchrisumlem3  27435  dirith2  27472  nmounbseqiALT  30757  nmobndseqiALT  30759  h2hcau  30958  h2hlm  30959  hcau  31163  hlimi  31167  hlimadd  31172  hhcms  31182  isch2  31202  chlimi  31213  hlim0  31214  hhsscms  31257  padct  32693  smatfval  33778  lmdvg  33936  esumfsup  34053  esumpcvgval  34061  esumcvg  34069  sigapildsys  34145  measiun  34201  voliune  34212  omssubadd  34284  carsggect  34302  carsgclctunlem2  34303  eulerpartlems  34344  eulerpartleme  34347  eulerpartlem1  34351  eulerpartlemb  34352  eulerpartlemt  34355  eulerpartgbij  34356  eulerpartlemr  34358  eulerpartlemmf  34359  eulerpartlemgvv  34360  eulerpartlemgf  34363  eulerpartlemgs2  34364  eulerpartlemn  34365  reprval  34594  repr0  34595  reprsuc  34599  reprss  34601  reprinrn  34602  reprlt  34603  hashreprin  34604  reprinfz1  34606  reprpmtf1o  34610  reprdifc  34611  breprexplemb  34615  breprexpnat  34618  vtsval  34621  circlemethnat  34625  circlevma  34626  circlemethhgt  34627  sinccvglem  35652  circum  35654  divcnvlin  35713  faclimlem2  35724  faclim2  35728  colinearex  36041  bj-ndxarg  37058  poimirlem32  37639  voliunnfl  37651  volsupnfl  37652  lmclim2  37745  geomcau  37746  rrncmslem  37819  fisdomnn  42225  eldioph3b  42746  lzenom  42751  diophin  42753  diophun  42754  pellexlem3  42812  pellexlem4  42813  pellexlem5  42814  eltrclrec  43662  brtrclrec  43678  iunrelexpmin1  43690  trclrelexplem  43693  dftrcl3  43702  fvtrcllb1d  43704  trclfvcom  43705  cnvtrclfv  43706  cotrcltrcl  43707  trclimalb2  43708  trclfvdecomr  43710  dfrtrcl4  43720  corcltrcl  43721  cotrclrcl  43724  hashnzfzclim  44304  dvradcnv2  44329  binomcxplemcvg  44336  binomcxplemdvsum  44337  binomcxplemnotnn0  44338  ssnnf1octb  45181  clim1fr1  45592  divcnvg  45618  limsup10ex  45764  liminf10ex  45765  wallispilem5  46060  wallispi  46061  stirlinglem1  46065  stirlinglem8  46072  stirlinglem14  46078  stirlinglem15  46079  fourierdlem103  46200  fourierdlem104  46201  fourierdlem112  46209  subsaliuncllem  46348  subsaliuncl  46349  nnfoctbdjlem  46446  nnfoctbdj  46447  ismeannd  46458  voliunsge0lem  46463  caratheodorylem2  46518  isomenndlem  46521  hoicvrrex  46547  ovnsupge0  46548  ovnlecvr  46549  ovn0lem  46556  ovnsubaddlem1  46561  ovnsubadd  46563  sge0hsphoire  46580  hoidmv1lelem1  46582  hoidmv1lelem2  46583  hoidmv1lelem3  46584  hoidmv1le  46585  hoidmvlelem1  46586  hoidmvlelem2  46587  hoidmvlelem3  46588  hoidmvlelem4  46589  hoidmvlelem5  46590  hoidmvle  46591  ovnhoilem1  46592  ovnhoilem2  46593  ovnlecvr2  46601  hspmbllem2  46618  ovolval2lem  46634  ovnsubadd2lem  46636  ovolval4lem2  46641  ovolval5lem1  46643  ovolval5lem2  46644  ovnovollem1  46647  ovnovollem2  46648  vonioolem1  46671  smflimlem6  46767  smfresal  46779  fsupdm  46833  smfsupdmmbllem  46835  finfdm  46837  smfinfdmmbllem  46839  nnsgrpmgm  48157  nnsgrp  48158  nnsgrpnmnd  48159