MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnex Structured version   Visualization version   GIF version

Theorem nnex 11643
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
StepHypRef Expression
1 cnex 10617 . 2 ℂ ∈ V
2 nnsscn 11642 . 2 ℕ ⊆ ℂ
31, 2ssexi 5213 1 ℕ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2115  Vcvv 3481  cc 10534  cn 11637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7456  ax-cnex 10592  ax-1cn 10594  ax-addcl 10596
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3483  df-sbc 3760  df-csb 3868  df-dif 3923  df-un 3925  df-in 3927  df-ss 3937  df-pss 3939  df-nul 4278  df-if 4452  df-pw 4525  df-sn 4552  df-pr 4554  df-tp 4556  df-op 4558  df-uni 4826  df-iun 4908  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6136  df-ord 6182  df-on 6183  df-lim 6184  df-suc 6185  df-iota 6303  df-fun 6346  df-fn 6347  df-f 6348  df-f1 6349  df-fo 6350  df-f1o 6351  df-fv 6352  df-ov 7153  df-om 7576  df-wrecs 7944  df-recs 8005  df-rdg 8043  df-nn 11638
This theorem is referenced by:  dfnn2  11650  nn0ex  11903  nn0ennn  13354  facmapnn  13653  isercolllem2  15025  supcvg  15214  trireciplem  15220  expcnv  15222  geo2lim  15234  qnnen  15569  rpnnen2lem1  15570  rpnnen2lem2  15571  rpnnen  15583  rucALT  15586  prmex  16022  unbenlem  16245  vdwapfval  16308  vdwapf  16309  vdwlem6  16323  vdwlem7  16324  vdwlem8  16325  vdwlem11  16328  prmgaplcm  16397  prmgapprmo  16399  ndxarg  16511  odfval  18663  odval  18665  gexval  18706  pnrmopn  21954  1stcfb  22056  hausmapdom  22111  met1stc  23134  met2ndci  23135  rectbntr0  23443  metcld2  23917  elovolmlem  24084  ovolctb  24100  ovol0  24103  mbfimaopnlem  24265  itg1climres  24324  mbfi1fseqlem6  24330  mbfi1flimlem  24332  mbfmullem2  24334  itg2monolem1  24360  itg2addlem  24368  plyeq0lem  24813  leibpi  25534  dfef2  25562  emcllem4  25590  emcllem6  25592  emcllem7  25593  lgamgulmlem6  25625  lgamcvg2  25646  basellem6  25677  basellem7  25678  basellem8  25679  basellem9  25680  dchrisumlem3  26081  dirith2  26118  nmounbseqiALT  28567  nmobndseqiALT  28569  h2hcau  28768  h2hlm  28769  hcau  28973  hlimi  28977  hlimadd  28982  hhcms  28992  isch2  29012  chlimi  29023  hlim0  29024  hhsscms  29067  padct  30469  smatfval  31123  lmdvg  31256  esumfsup  31389  esumpcvgval  31397  esumcvg  31405  sigapildsys  31481  measiun  31537  voliune  31548  omssubadd  31618  carsggect  31636  carsgclctunlem2  31637  eulerpartlems  31678  eulerpartleme  31681  eulerpartlem1  31685  eulerpartlemb  31686  eulerpartlemt  31689  eulerpartgbij  31690  eulerpartlemr  31692  eulerpartlemmf  31693  eulerpartlemgvv  31694  eulerpartlemgf  31697  eulerpartlemgs2  31698  eulerpartlemn  31699  reprval  31941  repr0  31942  reprsuc  31946  reprss  31948  reprinrn  31949  reprlt  31950  hashreprin  31951  reprinfz1  31953  reprpmtf1o  31957  reprdifc  31958  breprexplemb  31962  breprexpnat  31965  vtsval  31968  circlemethnat  31972  circlevma  31973  circlemethhgt  31974  sinccvglem  32975  circum  32977  divcnvlin  33024  faclimlem2  33036  faclim2  33040  colinearex  33581  bj-ndxarg  34439  poimirlem32  35035  voliunnfl  35047  volsupnfl  35048  lmclim2  35142  geomcau  35143  rrncmslem  35216  eldioph3b  39623  lzenom  39628  diophin  39630  diophun  39631  pellexlem3  39689  pellexlem4  39690  pellexlem5  39691  eltrclrec  40298  brtrclrec  40314  iunrelexpmin1  40326  trclrelexplem  40329  dftrcl3  40338  fvtrcllb1d  40340  trclfvcom  40341  cnvtrclfv  40342  cotrcltrcl  40343  trclimalb2  40344  trclfvdecomr  40346  dfrtrcl4  40356  corcltrcl  40357  cotrclrcl  40360  hashnzfzclim  40947  dvradcnv2  40972  binomcxplemcvg  40979  binomcxplemdvsum  40980  binomcxplemnotnn0  40981  ssnnf1octb  41748  clim1fr1  42170  divcnvg  42196  limsup10ex  42342  liminf10ex  42343  wallispilem5  42638  wallispi  42639  stirlinglem1  42643  stirlinglem8  42650  stirlinglem14  42656  stirlinglem15  42657  fourierdlem103  42778  fourierdlem104  42779  fourierdlem112  42787  subsaliuncllem  42924  subsaliuncl  42925  nnfoctbdjlem  43021  nnfoctbdj  43022  ismeannd  43033  voliunsge0lem  43038  caratheodorylem2  43093  isomenndlem  43096  hoicvrrex  43122  ovnsupge0  43123  ovnlecvr  43124  ovn0lem  43131  ovnsubaddlem1  43136  ovnsubadd  43138  sge0hsphoire  43155  hoidmv1lelem1  43157  hoidmv1lelem2  43158  hoidmv1lelem3  43159  hoidmv1le  43160  hoidmvlelem1  43161  hoidmvlelem2  43162  hoidmvlelem3  43163  hoidmvlelem4  43164  hoidmvlelem5  43165  hoidmvle  43166  ovnhoilem1  43167  ovnhoilem2  43168  ovnlecvr2  43176  hspmbllem2  43193  ovolval2lem  43209  ovnsubadd2lem  43211  ovolval4lem2  43216  ovolval5lem1  43218  ovolval5lem2  43219  ovnovollem1  43222  ovnovollem2  43223  vonioolem1  43246  smflimlem6  43336  smfresal  43347  nnsgrpmgm  44363  nnsgrp  44364  nnsgrpnmnd  44365
  Copyright terms: Public domain W3C validator