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

Theorem nncnd 10559
Description: A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nnred.1  |-  ( ph  ->  A  e.  NN )
Assertion
Ref Expression
nncnd  |-  ( ph  ->  A  e.  CC )

Proof of Theorem nncnd
StepHypRef Expression
1 nnsscn 10548 . 2  |-  NN  C_  CC
2 nnred.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3487 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   CCcc 9493   NNcn 10543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-i2m1 9563  ax-1ne0 9564  ax-rrecex 9567  ax-cnre 9568
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-ov 6284  df-om 6686  df-recs 7044  df-rdg 7078  df-nn 10544
This theorem is referenced by:  facdiv  12346  facndiv  12347  faclbnd  12349  faclbnd5  12357  faclbnd6  12358  facubnd  12359  facavg  12360  bccmpl  12368  bcn0  12369  bcn1  12372  bcm1k  12374  bcp1n  12375  bcp1nk  12376  bcval5  12377  bcpasc  12380  permnn  12385  hashf1  12487  hashfac  12488  wrdeqcats1  12680  binom11  13625  binom1dif  13626  climcndslem2  13643  arisum2  13653  trireciplem  13654  trirecip  13655  geo2sum  13663  geo2lim  13665  fprodfac  13758  eftcl  13790  eftabs  13792  efcllem  13794  ege2le3  13806  efcj  13808  efaddlem  13809  eftlub  13825  eirrlem  13918  sqr2irrlem  13962  oexpneg  14030  bitsp1  14062  bitsfzolem  14065  bitsfzo  14066  bitsmod  14067  bitscmp  14069  bitsinv1lem  14072  bitsinv1  14073  2ebits  14078  bitsinvp1  14080  sadcaddlem  14088  sadadd3  14092  bitsres  14104  bitsuz  14105  bitsshft  14106  mulgcd  14165  rplpwr  14175  sqgcd  14177  prmind2  14209  isprm5  14234  prmdvdsexpr  14238  divgcdodd  14241  qmuldeneqnum  14261  divnumden  14262  qnumgt0  14264  numdensq  14268  hashdvds  14286  phiprmpw  14287  prmdiv  14296  prmdivdiv  14298  modprm0  14311  pythagtriplem4  14324  pythagtriplem6  14326  pythagtriplem7  14327  pythagtriplem14  14333  pythagtriplem15  14334  pythagtriplem19  14338  pythagtrip  14339  pcprendvds2  14346  pcpre1  14347  pcpremul  14348  pceulem  14350  pcdiv  14357  pcqmul  14358  pcelnn  14374  pcid  14377  pc2dvds  14383  pcaddlem  14388  pcadd  14389  pcfaclem  14398  qexpz  14401  expnprm  14402  prmpwdvds  14403  pockthlem  14404  pockthg  14405  infpnlem1  14409  prmreclem1  14415  prmreclem2  14416  prmreclem3  14417  prmreclem4  14418  prmreclem6  14420  4sqlem6  14442  4sqlem7  14443  4sqlem10  14446  mul4sqlem  14452  4sqlem11  14454  4sqlem12  14455  4sqlem14  14457  4sqlem17  14460  4sqlem18  14461  vdwlem1  14480  vdwlem2  14481  vdwlem3  14482  vdwlem5  14484  vdwlem6  14485  vdwlem8  14487  vdwlem9  14488  vdwlem10  14489  vdwlem12  14491  ramub1lem2  14526  ramcl  14528  gsumccat  15987  mulgnndir  16142  mulgnnass  16148  psgnunilem5  16497  odf1o2  16571  pgp0  16594  sylow1lem1  16596  odcau  16602  sylow2blem3  16620  sylow3lem3  16627  sylow3lem4  16628  gexexlem  16836  ablfacrp2  17096  ablfac1lem  17097  ablfac1eu  17102  pgpfac1lem3a  17105  pgpfac1lem3  17106  zringlpirlem3  18488  zlpirlem3  18493  znrrg  18581  cpmadugsumlemF  19354  lebnumlem3  21440  ovollb2lem  21876  ovolunlem1a  21884  ovolunlem1  21885  uniioombllem3  21971  uniioombllem4  21972  dyaddisjlem  21981  mbfi1fseqlem3  22101  mbfi1fseqlem4  22102  dgrcolem1  22646  vieta1lem1  22682  vieta1lem2  22683  elqaalem2  22692  elqaalem3  22693  aalioulem1  22704  aaliou3lem2  22715  aaliou3lem8  22717  aaliou3lem6  22720  aaliou3lem9  22722  taylfvallem1  22728  tayl0  22733  taylply2  22739  taylply  22740  dvtaylp  22741  taylthlem1  22744  taylthlem2  22745  pserdvlem2  22799  advlogexp  23012  cxpmul2  23046  cxpeq  23107  atantayl3  23246  leibpi  23249  log2cnv  23251  log2tlbnd  23252  birthdaylem2  23258  birthdaylem3  23259  amgmlem  23295  amgm  23296  emcllem5  23305  fsumharmonic  23317  wilthlem1  23318  wilthlem2  23319  wilthlem3  23320  basellem1  23330  basellem2  23331  basellem3  23332  basellem4  23333  basellem5  23334  basellem8  23337  vmaprm  23367  sgmval2  23393  0sgm  23394  sgmf  23395  vma1  23416  dvdsdivcl  23433  fsumdvdsdiaglem  23435  dvdsflf1o  23439  muinv  23445  dvdsmulf1o  23446  sgmppw  23448  1sgmprm  23450  1sgm2ppw  23451  sgmmul  23452  chtublem  23462  fsumvma2  23465  chpchtsum  23470  logfaclbnd  23473  logexprlim  23476  mersenne  23478  perfect1  23479  perfectlem1  23480  perfectlem2  23481  perfect  23482  dchrsum2  23519  dchrhash  23522  bcmono  23528  bcp1ctr  23530  bclbnd  23531  bposlem1  23535  bposlem2  23536  bposlem3  23537  bposlem5  23539  bposlem6  23540  lgsval2lem  23557  lgsqrlem2  23593  lgseisenlem1  23600  lgseisenlem4  23603  lgsquadlem1  23605  lgsquadlem2  23606  lgsquadlem3  23607  lgsquad2  23611  m1lgs  23613  2sqlem3  23617  2sqlem4  23618  chebbnd1lem1  23630  chebbnd1  23633  rplogsumlem1  23645  rplogsumlem2  23646  rpvmasumlem  23648  dchrisumlem1  23650  dchrmusum2  23655  dchrvmasumlem1  23656  dchrvmasum2lem  23657  dchrvmasum2if  23658  dchrvmasumlem2  23659  dchrvmasumlem3  23660  dchrvmasumiflem1  23662  dchrisum0flblem1  23669  dchrisum0flblem2  23670  dchrisum0fno1  23672  rpvmasum2  23673  rplogsum  23688  mulogsumlem  23692  mulogsum  23693  mulog2sumlem2  23696  vmalogdivsum2  23699  vmalogdivsum  23700  2vmadivsumlem  23701  logsqvma  23703  selberglem2  23707  selberglem3  23708  selberg  23709  selberg2lem  23711  logdivbnd  23717  selberg3lem1  23718  selberg4lem1  23721  pntrsumo1  23726  pntrsumbnd2  23728  selberg3r  23730  selberg4r  23731  selberg34r  23732  pntsval2  23737  pntrlog2bndlem2  23739  pntrlog2bndlem4  23741  pntrlog2bndlem6  23744  pntpbnd1  23747  pntpbnd2  23748  pntlemg  23759  pntlemn  23761  pntlemf  23766  pnt  23775  padicabvf  23792  ostth2lem2  23795  ostth3  23799  hashclwwlkn  24812  eupares  24951  numdenneg  27584  ltesubnnd  27589  qqhnm  27948  oddpwdc  28270  eulerpartlemsv2  28274  eulerpartlems  28276  eulerpartlemsv3  28277  eulerpartlemgc  28278  eulerpartlemv  28280  eulerpartlemgs2  28296  fibp1  28317  ballotlemfc0  28408  ballotlemfcc  28409  signsvtn0  28504  zetacvg  28534  dmgmdivn0  28547  lgamgulmlem3  28550  lgamgulmlem4  28551  lgamgulmlem5  28552  lgamgulmlem6  28553  lgamgulm2  28555  lgamcvg2  28574  gamcvg  28575  gamcvg2lem  28578  facgam  28585  subfacp1lem1  28600  subfacp1lem5  28605  subfacval2  28608  subfaclim  28609  cvmliftlem2  28708  cvmliftlem7  28713  cvmliftlem10  28716  cvmliftlem11  28717  cvmliftlem13  28718  iprodgam  29100  risefacfac  29132  fallfacfwd  29133  fallfacval4  29140  bcfallfac  29141  fallfacfac  29142  faclimlem1  29143  faclimlem2  29144  faclim2  29148  bpolycl  29789  bpolysum  29790  bpolydiflem  29791  fsumkthpow  29793  nn0prpwlem  30115  nn0prpw  30116  irrapxlem4  30736  irrapxlem5  30737  pellexlem2  30741  pellexlem6  30745  pell1234qrne0  30764  pell1234qrreccl  30765  pell1234qrmulcl  30766  pell1234qrdich  30772  pell14qrdich  30780  pell1qrge1  30781  pell1qr1  30782  pell14qrgapw  30787  rmxyneg  30831  rmxm1  30845  rmxluc  30847  rmxdbl  30850  jm2.19lem1  30906  jm2.27c  30924  phisum  31135  itgpowd  31158  lcmgcdlem  31188  hashnzfzclim  31203  clim1fr1  31515  sumnnodd  31544  dvsinexp  31609  itgsinexplem1  31642  itgsinexp  31643  stoweidlem1  31672  stoweidlem11  31682  stoweidlem25  31696  stoweidlem26  31697  stoweidlem34  31705  stoweidlem37  31708  stoweidlem38  31709  stoweidlem42  31713  wallispi2lem1  31742  wallispi2  31744  stirlinglem4  31748  stirlinglem5  31749  stirlinglem10  31754  stirlinglem15  31759  dirkertrigeqlem3  31771  dirkertrigeq  31772  dirkercncflem2  31775  dirkercncflem4  31777  fourierdlem11  31789  fourierdlem15  31793  fourierdlem79  31857  fourierdlem83  31861  sqwvfourb  31901  inductionexd  37637
  Copyright terms: Public domain W3C validator