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

Theorem nncnd 11319
Description: A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nnred.1 (𝜑𝐴 ∈ ℕ)
Assertion
Ref Expression
nncnd (𝜑𝐴 ∈ ℂ)

Proof of Theorem nncnd
StepHypRef Expression
1 nnsscn 11308 . 2 ℕ ⊆ ℂ
2 nnred.1 . 2 (𝜑𝐴 ∈ ℕ)
31, 2sseldi 3794 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2156  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-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:  facdiv  13292  facndiv  13293  faclbnd  13295  faclbnd5  13303  faclbnd6  13304  facubnd  13305  facavg  13306  bccmpl  13314  bcn0  13315  bcn1  13318  bcm1k  13320  bcp1n  13321  bcp1nk  13322  bcval5  13323  bcpasc  13326  permnn  13331  hashf1  13456  hashfac  13457  relexpaddnn  14012  binom11  14784  binom1dif  14785  climcndslem2  14802  arisum2  14813  trireciplem  14814  trirecip  14815  geo2sum  14824  geo2lim  14826  fprodfac  14922  risefacfac  14984  fallfacfwd  14985  fallfacval4  14992  bcfallfac  14993  fallfacfac  14994  bpolycl  15001  bpolysum  15002  bpolydiflem  15003  fsumkthpow  15005  eftcl  15022  eftabs  15024  efcllem  15026  ege2le3  15038  efcj  15040  efaddlem  15041  eftlub  15057  eirrlem  15150  sqrt2irrlem  15195  sqrt2irrlemOLD  15196  oexpneg  15287  pwp1fsum  15332  bitsp1  15370  bitsfzolem  15373  bitsfzo  15374  bitsmod  15375  bitscmp  15377  bitsinv1lem  15380  bitsinv1  15381  2ebits  15386  bitsinvp1  15388  sadcaddlem  15396  sadadd3  15400  bitsres  15412  bitsuz  15413  bitsshft  15414  mulgcd  15482  rplpwr  15493  sqgcd  15495  lcmgcdlem  15536  3lcm2e6woprm  15545  coprmprod  15591  coprmproddvdslem  15592  cncongr1  15597  cncongr2  15598  prmind2  15614  isprm5  15634  divgcdodd  15637  prmdvdsexpr  15644  qmuldeneqnum  15670  divnumden  15671  qnumgt0  15673  numdensq  15677  hashdvds  15695  phiprmpw  15696  prmdiv  15705  prmdivdiv  15707  phisum  15710  modprm0  15725  pythagtriplem4  15739  pythagtriplem6  15741  pythagtriplem7  15742  pythagtriplem14  15748  pythagtriplem15  15749  pythagtriplem19  15753  pythagtrip  15754  pcprendvds2  15761  pcpre1  15762  pcpremul  15763  pceulem  15765  pcdiv  15772  pcqmul  15773  pcelnn  15789  pcid  15792  pc2dvds  15798  dvdsprmpweqnn  15804  dvdsprmpweqle  15805  pcaddlem  15807  pcadd  15808  pcfaclem  15817  qexpz  15820  expnprm  15821  oddprmdvds  15822  prmpwdvds  15823  pockthlem  15824  pockthg  15825  infpnlem1  15829  prmreclem1  15835  prmreclem2  15836  prmreclem3  15837  prmreclem4  15838  prmreclem6  15840  4sqlem6  15862  4sqlem7  15863  4sqlem10  15866  mul4sqlem  15872  4sqlem11  15874  4sqlem12  15875  4sqlem14  15877  4sqlem17  15880  4sqlem18  15881  vdwlem1  15900  vdwlem2  15901  vdwlem3  15902  vdwlem5  15904  vdwlem6  15905  vdwlem8  15907  vdwlem9  15908  vdwlem10  15909  vdwlem12  15911  ramub1lem2  15946  ramcl  15948  prmop1  15957  prmdvdsprmo  15961  prmgaplem7  15976  prmgaplem8  15977  gsumccat  17581  mulgnndir  17771  mulgnnass  17777  psgnunilem5  18113  odf1o2  18187  pgp0  18210  sylow1lem1  18212  odcau  18218  sylow2blem3  18236  sylow3lem3  18243  sylow3lem4  18244  gexexlem  18454  ablfacrp2  18666  ablfac1lem  18667  ablfac1eu  18672  pgpfac1lem3a  18675  pgpfac1lem3  18676  zringlpirlem3  20040  znrrg  20119  cpmadugsumlemF  20892  lebnumlem3  22973  ovollb2lem  23467  ovolunlem1a  23475  ovolunlem1  23476  uniioombllem3  23564  uniioombllem4  23565  dyaddisjlem  23574  mbfi1fseqlem3  23696  mbfi1fseqlem4  23697  dgrcolem1  24241  vieta1lem1  24277  vieta1lem2  24278  elqaalem2  24287  elqaalem3  24288  aalioulem1  24299  aaliou3lem2  24310  aaliou3lem8  24312  aaliou3lem6  24315  aaliou3lem9  24317  taylfvallem1  24323  tayl0  24328  taylply2  24334  taylply  24335  dvtaylp  24336  taylthlem1  24339  taylthlem2  24340  pserdvlem2  24394  advlogexp  24613  cxpmul2  24647  cxpeq  24710  atantayl3  24878  leibpi  24881  log2cnv  24883  log2tlbnd  24884  birthdaylem2  24891  birthdaylem3  24892  amgmlem  24928  amgm  24929  emcllem5  24938  fsumharmonic  24950  zetacvg  24953  dmgmdivn0  24966  lgamgulmlem3  24969  lgamgulmlem4  24970  lgamgulmlem5  24971  lgamgulmlem6  24972  lgamgulm2  24974  lgamcvg2  24993  gamcvg  24994  gamcvg2lem  24997  facgam  25004  wilthlem1  25006  wilthlem2  25007  wilthlem3  25008  wilthimp  25010  basellem1  25019  basellem2  25020  basellem3  25021  basellem4  25022  basellem5  25023  basellem8  25026  vmaprm  25055  sgmval2  25081  0sgm  25082  sgmf  25083  vma1  25104  fsumdvdsdiaglem  25121  dvdsflf1o  25125  muinv  25131  dvdsmulf1o  25132  sgmppw  25134  1sgmprm  25136  1sgm2ppw  25137  sgmmul  25138  chtublem  25148  fsumvma2  25151  chpchtsum  25156  logfaclbnd  25159  logexprlim  25162  mersenne  25164  perfect1  25165  perfectlem1  25166  perfectlem2  25167  perfect  25168  dchrsum2  25205  dchrhash  25208  bcmono  25214  bcp1ctr  25216  bclbnd  25217  bposlem1  25221  bposlem2  25222  bposlem3  25223  bposlem5  25225  bposlem6  25226  lgsval2lem  25244  lgsqrlem2  25284  gausslemma2dlem6  25309  gausslemma2dlem7  25310  gausslemma2d  25311  lgseisenlem1  25312  lgseisenlem4  25315  lgsquadlem1  25317  lgsquadlem2  25318  lgsquadlem3  25319  lgsquad2  25323  m1lgs  25325  2sqlem3  25357  2sqlem4  25358  chebbnd1lem1  25370  chebbnd1  25373  rplogsumlem1  25385  rplogsumlem2  25386  rpvmasumlem  25388  dchrisumlem1  25390  dchrmusum2  25395  dchrvmasumlem1  25396  dchrvmasum2lem  25397  dchrvmasum2if  25398  dchrvmasumlem2  25399  dchrvmasumlem3  25400  dchrvmasumiflem1  25402  dchrisum0flblem1  25409  dchrisum0flblem2  25410  dchrisum0fno1  25412  rpvmasum2  25413  rplogsum  25428  mulogsumlem  25432  mulogsum  25433  mulog2sumlem2  25436  vmalogdivsum2  25439  vmalogdivsum  25440  2vmadivsumlem  25441  logsqvma  25443  selberglem2  25447  selberglem3  25448  selberg  25449  selberg2lem  25451  logdivbnd  25457  selberg3lem1  25458  selberg4lem1  25461  pntrsumo1  25466  pntrsumbnd2  25468  selberg3r  25470  selberg4r  25471  selberg34r  25472  pntsval2  25477  pntrlog2bndlem2  25479  pntrlog2bndlem4  25481  pntrlog2bndlem6  25484  pntpbnd1  25487  pntpbnd2  25488  pntlemg  25499  pntlemn  25501  pntlemf  25506  pnt  25515  padicabvf  25532  ostth2lem2  25535  ostth3  25539  fusgrhashclwwlkn  27228  eucrct2eupth  27416  numdenneg  29888  ltesubnnd  29893  1smat1  30193  madjusmdetlem2  30217  madjusmdetlem4  30219  qqhnm  30357  oddpwdc  30739  eulerpartlemsv2  30743  eulerpartlems  30745  eulerpartlemsv3  30746  eulerpartlemgc  30747  eulerpartlemv  30749  eulerpartlemgs2  30765  fibp1  30786  ballotlemfc0  30877  ballotlemfcc  30878  signsvtn0  30970  reprpmtf1o  31027  vtscl  31039  hgt750lemb  31057  tgoldbachgt  31064  subfacp1lem1  31482  subfacp1lem5  31487  subfacval2  31490  subfaclim  31491  cvmliftlem2  31589  cvmliftlem7  31594  cvmliftlem10  31597  cvmliftlem11  31598  cvmliftlem13  31599  bcm1nt  31943  bcprod  31944  iprodgam  31948  faclimlem1  31949  faclimlem2  31950  faclim2  31954  nn0prpwlem  32636  nn0prpw  32637  knoppndvlem16  32833  poimirlem1  33721  poimirlem2  33722  poimirlem6  33726  poimirlem7  33727  poimirlem8  33728  poimirlem9  33729  poimirlem10  33730  poimirlem11  33731  poimirlem12  33732  poimirlem13  33733  poimirlem15  33735  poimirlem16  33736  poimirlem17  33737  poimirlem18  33738  poimirlem19  33739  poimirlem20  33740  poimirlem21  33741  poimirlem22  33742  poimirlem23  33743  poimirlem24  33744  poimirlem25  33745  poimirlem26  33746  poimirlem27  33747  poimirlem31  33751  irrapxlem4  37889  irrapxlem5  37890  pellexlem2  37894  pellexlem6  37898  pell1234qrne0  37917  pell1234qrreccl  37918  pell1234qrmulcl  37919  pell1234qrdich  37925  pell14qrdich  37933  pell1qrge1  37934  pell1qr1  37935  pell14qrgapw  37940  rmxyneg  37984  rmxm1  37998  rmxluc  38000  rmxdbl  38003  jm2.19lem1  38055  jm2.27c  38073  itgpowd  38298  relexpmulnn  38499  relexpmulg  38500  inductionexd  38951  hashnzfzclim  39019  bcccl  39036  bcc0  39037  bccp1k  39038  bccm1k  39039  binomcxplemwb  39045  fsumnncl  40281  mccllem  40307  clim1fr1  40311  sumnnodd  40340  dvsinexp  40603  dvxpaek  40633  dvnxpaek  40635  dvnprodlem2  40640  itgsinexplem1  40647  itgsinexp  40648  stoweidlem1  40695  stoweidlem11  40705  stoweidlem25  40719  stoweidlem26  40720  stoweidlem34  40728  stoweidlem37  40731  stoweidlem38  40732  stoweidlem42  40736  wallispi2lem1  40765  wallispi2  40767  stirlinglem4  40771  stirlinglem5  40772  stirlinglem10  40777  stirlinglem15  40782  dirkertrigeqlem3  40794  dirkertrigeq  40795  dirkercncflem2  40798  dirkercncflem4  40800  fourierdlem11  40812  fourierdlem15  40816  fourierdlem79  40879  fourierdlem83  40883  sqwvfourb  40923  etransclem14  40942  etransclem15  40943  etransclem20  40948  etransclem21  40949  etransclem22  40950  etransclem23  40951  etransclem24  40952  etransclem25  40953  etransclem28  40956  etransclem31  40959  etransclem32  40960  etransclem33  40961  etransclem34  40962  etransclem35  40963  etransclem38  40966  etransclem41  40969  etransclem44  40972  etransclem45  40973  etransclem47  40975  etransclem48  40976  nnfoctbdjlem  41149  deccarry  41894  iccpartgtprec  41929  fmtnoodd  42018  fmtnorec2lem  42027  fmtnorec2  42028  fmtnodvds  42029  goldbachthlem2  42031  fmtnorec3  42033  fmtnorec4  42034  fmtnoprmfac1lem  42049  fmtnoprmfac1  42050  fmtnoprmfac2lem1  42051  fmtnoprmfac2  42052  2pwp1prm  42076  sfprmdvdsmersenne  42093  lighneallem4b  42099  lighneal  42101  proththdlem  42103  proththd  42104  oexpnegALTV  42161  perfectALTVlem1  42203  perfectALTVlem2  42204  perfectALTV  42205  nnpw2pmod  42943  nnolog2flm1  42950  blennn0em1  42951  blengt1fldiv2p1  42953  nn0sumshdiglemB  42980  amgmlemALT  43118
  Copyright terms: Public domain W3C validator