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

Theorem nnex 10561
Description: The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
nnex  |-  NN  e.  _V

Proof of Theorem nnex
StepHypRef Expression
1 cnex 9566 . 2  |-  CC  e.  _V
2 nnsscn 10560 . 2  |-  NN  C_  CC
31, 2ssexi 4507 1  |-  NN  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1872   _Vcvv 3017   CCcc 9483   NNcn 10555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-i2m1 9553  ax-1ne0 9554  ax-rrecex 9557  ax-cnre 9558
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-reu 2716  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-ov 6247  df-om 6646  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-nn 10556
This theorem is referenced by:  dfnn2  10568  nn0ex  10821  rpnnen1lem1  11236  rpnnen1lem3  11238  rpnnen1lem4  11239  rpnnen1lem5  11240  nn0ennn  12137  facmapnn  12415  isercolllem2  13667  supcvg  13852  trireciplem  13858  expcnv  13860  geo2lim  13869  qnnen  14204  rpnnen2lem1  14205  rpnnen2lem2  14206  rpnnen  14217  rucALT  14220  prmex  14566  unbenlem  14790  vdwapfval  14859  vdwapf  14860  vdwlem6  14874  vdwlem7  14875  vdwlem8  14876  vdwlem11  14879  lcmsmapnnOLD  14949  prmormapnnOLD  14952  prmgaplcm  14969  prmgapprmo  14971  ndxarg  15079  odval  17118  odvalOLD  17121  gexval  17165  gexvalOLD  17167  ablfac1b  17641  pnrmopn  20296  1stcfb  20397  hausmapdom  20452  met1stc  21473  met2ndci  21474  rectbntr0  21787  metcld2  22213  elovolm  22365  elovolmr  22366  ovolmge0  22367  ovolgelb  22370  ovolctb  22380  ovol0  22383  ovolunlem1a  22386  ovolunlem1  22387  ovoliunlem1  22392  ovoliunlem2  22393  ovolshftlem2  22400  ovolicc2  22413  ioombl1  22452  mbfimaopnlem  22548  itg1climres  22609  mbfi1fseqlem6  22615  mbfi1flimlem  22617  mbfmullem2  22619  itg2monolem1  22645  itg2addlem  22653  plyeq0lem  23101  leibpi  23805  dfef2  23833  emcllem4  23861  emcllem6  23863  emcllem7  23864  lgamgulmlem6  23896  lgamcvg2  23917  basellem6  23949  basellem7  23950  basellem8  23951  basellem9  23952  vmaval  23977  sqff1o  24046  0sgmppw  24063  dchrisumlem3  24266  dirith2  24303  iseupa  25630  nmounbseqiALT  26356  nmobndseqiALT  26358  h2hcau  26569  h2hlm  26570  hcau  26774  hlimi  26778  hlimadd  26783  hhcms  26793  isch2  26813  chlimi  26824  hlim0  26825  hhsscms  26867  padct  28252  smatfval  28568  lmdvg  28706  esumfsup  28838  esumpcvgval  28846  esumcvg  28854  sigapildsys  28931  measiun  28987  voliune  28999  omssubadd  29075  omssubaddOLD  29079  carsggect  29097  carsgclctunlem2  29098  eulerpartlems  29140  eulerpartleme  29143  eulerpartlem1  29147  eulerpartlemb  29148  eulerpartlemt  29151  eulerpartgbij  29152  eulerpartlemr  29154  eulerpartlemmf  29155  eulerpartlemgvv  29156  eulerpartlemgf  29159  eulerpartlemgs2  29160  eulerpartlemn  29161  sinccvglem  30263  circum  30265  divcnvlin  30313  faclimlem2  30326  faclim2  30330  colinearex  30771  poimirlem32  31879  voliunnfl  31891  volsupnfl  31892  lmclim2  31994  geomcau  31995  rrncmslem  32071  eldioph3b  35519  lzenom  35524  diophin  35527  diophun  35528  pellexlem3  35588  pellexlem4  35589  pellexlem5  35590  eltrclrec  36185  brtrclrec  36201  iunrelexpmin1  36213  trclrelexplem  36216  dftrcl3  36225  fvtrcllb1d  36227  trclfvcom  36228  cnvtrclfv  36229  cotrcltrcl  36230  trclimalb2  36231  trclfvdecomr  36233  dfrtrcl4  36243  corcltrcl  36244  cotrclrcl  36247  hashnzfzclim  36584  dvradcnv2  36609  binomcxplemcvg  36616  binomcxplemdvsum  36617  binomcxplemnotnn0  36618  ssnnf1octb  37374  clim1fr1  37562  divcnvg  37590  wallispilem5  37814  wallispi  37815  stirlinglem1  37819  stirlinglem8  37826  stirlinglem14  37832  stirlinglem15  37833  fourierdlem103  37956  fourierdlem104  37957  fourierdlem112  37965  nnfoctbdjlem  38144  nnfoctbdj  38145  ismeannd  38156  caratheodorylem2  38199  isomenndlem  38202  hoicvrrex  38225  ovnsupge0  38226  ovnlecvr  38227  ovn0lem  38234  ovnsubaddlem1  38239  ovnsubadd  38241  sge0hsphoire  38258  hoidmv1lelem1  38260  hoidmv1lelem2  38261  hoidmv1lelem3  38262  hoidmv1le  38263  hoidmvlelem1  38264  hoidmvlelem2  38265  hoidmvlelem3  38266  hoidmvlelem4  38267  hoidmvlelem5  38268  hoidmvle  38269  ovnhoilem1  38270  ovnhoilem2  38271  nnsgrpmgm  39407  nnsgrp  39408  nnsgrpnmnd  39409
  Copyright terms: Public domain W3C validator