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

Theorem nnex 11309
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 10300 . 2 ℂ ∈ V
2 nnsscn 11308 . 2 ℕ ⊆ ℂ
31, 2ssexi 4996 1 ℕ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2156  Vcvv 3389  cc 10217  cn 11303
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2782  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5094  ax-un 7177  ax-cnex 10275  ax-resscn 10276  ax-1cn 10277  ax-icn 10278  ax-addcl 10279  ax-addrcl 10280  ax-mulcl 10281  ax-mulrcl 10282  ax-i2m1 10287  ax-1ne0 10288  ax-rrecex 10291  ax-cnre 10292
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2791  df-cleq 2797  df-clel 2800  df-nfc 2935  df-ne 2977  df-ral 3099  df-rex 3100  df-reu 3101  df-rab 3103  df-v 3391  df-sbc 3632  df-csb 3727  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-pss 3783  df-nul 4115  df-if 4278  df-pw 4351  df-sn 4369  df-pr 4371  df-tp 4373  df-op 4375  df-uni 4629  df-iun 4712  df-br 4843  df-opab 4905  df-mpt 4922  df-tr 4945  df-id 5217  df-eprel 5222  df-po 5230  df-so 5231  df-fr 5268  df-we 5270  df-xp 5315  df-rel 5316  df-cnv 5317  df-co 5318  df-dm 5319  df-rn 5320  df-res 5321  df-ima 5322  df-pred 5891  df-ord 5937  df-on 5938  df-lim 5939  df-suc 5940  df-iota 6062  df-fun 6101  df-fn 6102  df-f 6103  df-f1 6104  df-fo 6105  df-f1o 6106  df-fv 6107  df-ov 6875  df-om 7294  df-wrecs 7640  df-recs 7702  df-rdg 7740  df-nn 11304
This theorem is referenced by:  dfnn2  11316  nn0ex  11563  nn0ennn  13000  facmapnn  13290  isercolllem2  14617  supcvg  14808  trireciplem  14814  expcnv  14816  geo2lim  14826  qnnen  15160  rpnnen2lem1  15161  rpnnen2lem2  15162  rpnnen  15174  rucALT  15177  prmex  15607  unbenlem  15827  vdwapfval  15890  vdwapf  15891  vdwlem6  15905  vdwlem7  15906  vdwlem8  15907  vdwlem11  15910  prmgaplcm  15979  prmgapprmo  15981  ndxarg  16091  odval  18152  gexval  18192  ablfac1b  18669  pnrmopn  21359  1stcfb  21460  hausmapdom  21515  met1stc  22537  met2ndci  22538  rectbntr0  22846  metcld2  23315  elovolmlem  23453  ovolctb  23469  ovol0  23472  mbfimaopnlem  23634  itg1climres  23693  mbfi1fseqlem6  23699  mbfi1flimlem  23701  mbfmullem2  23703  itg2monolem1  23729  itg2addlem  23737  plyeq0lem  24178  leibpi  24881  dfef2  24909  emcllem4  24937  emcllem6  24939  emcllem7  24940  lgamgulmlem6  24972  lgamcvg2  24993  basellem6  25024  basellem7  25025  basellem8  25026  basellem9  25027  vmaval  25051  sqff1o  25120  0sgmppw  25135  dchrisumlem3  25392  dirith2  25429  nmounbseqiALT  27959  nmobndseqiALT  27961  h2hcau  28162  h2hlm  28163  hcau  28367  hlimi  28371  hlimadd  28376  hhcms  28386  isch2  28406  chlimi  28417  hlim0  28418  hhsscms  28462  padct  29822  smatfval  30184  lmdvg  30322  esumfsup  30455  esumpcvgval  30463  esumcvg  30471  sigapildsys  30548  measiun  30604  voliune  30615  omssubadd  30685  carsggect  30703  carsgclctunlem2  30704  eulerpartlems  30745  eulerpartleme  30748  eulerpartlem1  30752  eulerpartlemb  30753  eulerpartlemt  30756  eulerpartgbij  30757  eulerpartlemr  30759  eulerpartlemmf  30760  eulerpartlemgvv  30761  eulerpartlemgf  30764  eulerpartlemgs2  30765  eulerpartlemn  30766  reprval  31011  repr0  31012  reprsuc  31016  reprss  31018  reprinrn  31019  reprlt  31020  hashreprin  31021  reprinfz1  31023  reprpmtf1o  31027  reprdifc  31028  breprexplemb  31032  breprexpnat  31035  vtsval  31038  circlemethnat  31042  circlevma  31043  circlemethhgt  31044  sinccvglem  31886  circum  31888  divcnvlin  31938  faclimlem2  31950  faclim2  31954  colinearex  32486  bj-ndxarg  33338  poimirlem32  33752  voliunnfl  33764  volsupnfl  33765  lmclim2  33863  geomcau  33864  rrncmslem  33940  eldioph3b  37828  lzenom  37833  diophin  37836  diophun  37837  pellexlem3  37895  pellexlem4  37896  pellexlem5  37897  eltrclrec  38470  brtrclrec  38486  iunrelexpmin1  38498  trclrelexplem  38501  dftrcl3  38510  fvtrcllb1d  38512  trclfvcom  38513  cnvtrclfv  38514  cotrcltrcl  38515  trclimalb2  38516  trclfvdecomr  38518  dfrtrcl4  38528  corcltrcl  38529  cotrclrcl  38532  hashnzfzclim  39019  dvradcnv2  39044  binomcxplemcvg  39051  binomcxplemdvsum  39052  binomcxplemnotnn0  39053  ssnnf1octb  39869  clim1fr1  40311  divcnvg  40337  limsup10ex  40483  liminf10ex  40484  wallispilem5  40763  wallispi  40764  stirlinglem1  40768  stirlinglem8  40775  stirlinglem14  40781  stirlinglem15  40782  fourierdlem103  40903  fourierdlem104  40904  fourierdlem112  40912  subsaliuncllem  41052  subsaliuncl  41053  nnfoctbdjlem  41149  nnfoctbdj  41150  ismeannd  41161  voliunsge0lem  41166  caratheodorylem2  41221  isomenndlem  41224  hoicvrrex  41250  ovnsupge0  41251  ovnlecvr  41252  ovn0lem  41259  ovnsubaddlem1  41264  ovnsubadd  41266  sge0hsphoire  41283  hoidmv1lelem1  41285  hoidmv1lelem2  41286  hoidmv1lelem3  41287  hoidmv1le  41288  hoidmvlelem1  41289  hoidmvlelem2  41290  hoidmvlelem3  41291  hoidmvlelem4  41292  hoidmvlelem5  41293  hoidmvle  41294  ovnhoilem1  41295  ovnhoilem2  41296  ovnlecvr2  41304  hspmbllem2  41321  ovolval2lem  41337  ovnsubadd2lem  41339  ovolval4lem2  41344  ovolval5lem1  41346  ovolval5lem2  41347  ovnovollem1  41350  ovnovollem2  41351  vonioolem1  41374  smflimlem6  41464  smfresal  41475  nnsgrpmgm  42382  nnsgrp  42383  nnsgrpnmnd  42384
  Copyright terms: Public domain W3C validator