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

Theorem nnex 11064
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 10055 . 2 ℂ ∈ V
2 nnsscn 11063 . 2 ℕ ⊆ ℂ
31, 2ssexi 4836 1 ℕ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  Vcvv 3231  cc 9972  cn 11058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-i2m1 10042  ax-1ne0 10043  ax-rrecex 10046  ax-cnre 10047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-om 7108  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-nn 11059
This theorem is referenced by:  dfnn2  11071  nn0ex  11336  rpnnen1lem1OLD  11859  rpnnen1lem3OLD  11860  rpnnen1lem4OLD  11861  rpnnen1lem5OLD  11862  nn0ennn  12818  facmapnn  13112  isercolllem2  14440  supcvg  14632  trireciplem  14638  expcnv  14640  geo2lim  14650  qnnen  14986  rpnnen2lem1  14987  rpnnen2lem2  14988  rpnnen  15000  rucALT  15003  prmex  15438  unbenlem  15659  vdwapfval  15722  vdwapf  15723  vdwlem6  15737  vdwlem7  15738  vdwlem8  15739  vdwlem11  15742  prmgaplcm  15811  prmgapprmo  15813  ndxarg  15929  odval  17999  gexval  18039  ablfac1b  18515  pnrmopn  21195  1stcfb  21296  hausmapdom  21351  met1stc  22373  met2ndci  22374  rectbntr0  22682  metcld2  23151  elovolm  23289  elovolmr  23290  ovolmge0  23291  ovolgelb  23294  ovolctb  23304  ovol0  23307  ovolunlem1a  23310  ovolunlem1  23311  ovoliunlem1  23316  ovoliunlem2  23317  ovolshftlem2  23324  ovolicc2  23336  ioombl1  23376  mbfimaopnlem  23467  itg1climres  23526  mbfi1fseqlem6  23532  mbfi1flimlem  23534  mbfmullem2  23536  itg2monolem1  23562  itg2addlem  23570  plyeq0lem  24011  leibpi  24714  dfef2  24742  emcllem4  24770  emcllem6  24772  emcllem7  24773  lgamgulmlem6  24805  lgamcvg2  24826  basellem6  24857  basellem7  24858  basellem8  24859  basellem9  24860  vmaval  24884  sqff1o  24953  0sgmppw  24968  dchrisumlem3  25225  dirith2  25262  nmounbseqiALT  27761  nmobndseqiALT  27763  h2hcau  27964  h2hlm  27965  hcau  28169  hlimi  28173  hlimadd  28178  hhcms  28188  isch2  28208  chlimi  28219  hlim0  28220  hhsscms  28264  padct  29625  smatfval  29989  lmdvg  30127  esumfsup  30260  esumpcvgval  30268  esumcvg  30276  sigapildsys  30353  measiun  30409  voliune  30420  omssubadd  30490  carsggect  30508  carsgclctunlem2  30509  eulerpartlems  30550  eulerpartleme  30553  eulerpartlem1  30557  eulerpartlemb  30558  eulerpartlemt  30561  eulerpartgbij  30562  eulerpartlemr  30564  eulerpartlemmf  30565  eulerpartlemgvv  30566  eulerpartlemgf  30569  eulerpartlemgs2  30570  eulerpartlemn  30571  reprval  30816  repr0  30817  reprsuc  30821  reprss  30823  reprinrn  30824  reprlt  30825  hashreprin  30826  reprinfz1  30828  reprpmtf1o  30832  reprdifc  30833  breprexplemb  30837  breprexpnat  30840  vtsval  30843  circlemethnat  30847  circlevma  30848  circlemethhgt  30849  sinccvglem  31692  circum  31694  divcnvlin  31744  faclimlem2  31756  faclim2  31760  colinearex  32292  bj-ndxarg  33154  poimirlem32  33571  voliunnfl  33583  volsupnfl  33584  lmclim2  33684  geomcau  33685  rrncmslem  33761  eldioph3b  37645  lzenom  37650  diophin  37653  diophun  37654  pellexlem3  37712  pellexlem4  37713  pellexlem5  37714  eltrclrec  38289  brtrclrec  38305  iunrelexpmin1  38317  trclrelexplem  38320  dftrcl3  38329  fvtrcllb1d  38331  trclfvcom  38332  cnvtrclfv  38333  cotrcltrcl  38334  trclimalb2  38335  trclfvdecomr  38337  dfrtrcl4  38347  corcltrcl  38348  cotrclrcl  38351  hashnzfzclim  38838  dvradcnv2  38863  binomcxplemcvg  38870  binomcxplemdvsum  38871  binomcxplemnotnn0  38872  ssnnf1octb  39696  clim1fr1  40151  divcnvg  40177  limsup10ex  40323  liminf10ex  40324  wallispilem5  40604  wallispi  40605  stirlinglem1  40609  stirlinglem8  40616  stirlinglem14  40622  stirlinglem15  40623  fourierdlem103  40744  fourierdlem104  40745  fourierdlem112  40753  subsaliuncllem  40893  subsaliuncl  40894  nnfoctbdjlem  40990  nnfoctbdj  40991  ismeannd  41002  voliunsge0lem  41007  caratheodorylem2  41062  isomenndlem  41065  hoicvrrex  41091  ovnsupge0  41092  ovnlecvr  41093  ovn0lem  41100  ovnsubaddlem1  41105  ovnsubadd  41107  sge0hsphoire  41124  hoidmv1lelem1  41126  hoidmv1lelem2  41127  hoidmv1lelem3  41128  hoidmv1le  41129  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem4  41133  hoidmvlelem5  41134  hoidmvle  41135  ovnhoilem1  41136  ovnhoilem2  41137  ovnlecvr2  41145  hspmbllem2  41162  ovolval2lem  41178  ovnsubadd2lem  41180  ovolval4lem2  41185  ovolval5lem1  41187  ovolval5lem2  41188  ovnovollem1  41191  ovnovollem2  41192  vonioolem1  41215  smflimlem6  41305  smfresal  41316  nnsgrpmgm  42141  nnsgrp  42142  nnsgrpnmnd  42143
  Copyright terms: Public domain W3C validator