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

Theorem nn0cnd 10861
Description: A nonnegative integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nn0red.1  |-  ( ph  ->  A  e.  NN0 )
Assertion
Ref Expression
nn0cnd  |-  ( ph  ->  A  e.  CC )

Proof of Theorem nn0cnd
StepHypRef Expression
1 nn0red.1 . . 3  |-  ( ph  ->  A  e.  NN0 )
21nn0red 10860 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9625 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   CCcc 9493   NN0cn0 10802
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-rnegex 9566  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  df-n0 10803
This theorem is referenced by:  quoremnn0ALT  11966  expaddzlem  12191  expaddz  12192  expmulz  12194  facdiv  12347  faclbnd4lem3  12355  bcp1n  12376  bcn2m1  12384  bcn2p1  12385  hashgadd  12427  hashdom  12429  hashun3  12434  hashssdif  12457  hashxplem  12473  hashmap  12475  hashbclem  12483  hashf1lem2  12487  hashf1  12488  ccatcl  12575  ccatval3  12579  ccatlid  12585  ccatrid  12586  ccatass  12587  ccatrn  12588  lswccat0lsw  12590  wrdlenccats1lenm1  12609  ccats1val2  12613  ccatws1lenrev  12617  ccatw2s1p1  12622  swrdid  12634  addlenswrd  12644  swrdtrcfvl  12657  swrdccat2  12665  ccatopth2  12678  cats1un  12683  swrdccat3b  12703  spllen  12712  splfv2a  12714  revccat  12722  cshwlen  12752  cshwidxmod  12756  repswcshw  12762  2cshwid  12764  cshweqdif2  12769  isercoll2  13473  iseraltlem3  13488  binomlem  13623  bcxmas  13629  incexclem  13630  incexc  13631  incexc2  13632  climcndslem1  13643  climcndslem2  13644  arisum  13653  arisum2  13654  geomulcvg  13667  mertens  13677  effsumlt  13828  dvdsexp  14024  divalgmod  14046  bitsinv1lem  14073  sadcp1  14087  sadcaddlem  14089  sadadd2lem  14091  sadadd3  14093  sadaddlem  14098  sadasslem  14102  smupp1  14112  smumullem  14124  mulgcd  14166  absmulgcd  14167  mulgcdr  14168  gcddiv  14169  mulgcddvds  14227  qredeu  14230  odzdvds  14304  powm2modprm  14310  coprimeprodsq  14315  pceulem  14351  pczpre  14353  pcqmul  14359  pcaddlem  14389  pcmpt  14393  pcmpt2  14394  sumhash  14397  mul4sq  14454  4sqlem12  14456  vdwapun  14474  vdwlem2  14482  vdwlem3  14483  vdwlem6  14486  vdwlem8  14488  vdwlem9  14489  ramub1lem2  14527  ramcl  14529  mulgnn0dir  16144  mulgnn0ass  16150  lagsubg2  16241  psgnunilem2  16499  odmodnn0  16543  odmulg  16557  odmulgeq  16558  odinv  16562  sylow1lem1  16597  sylow2a  16618  sylow2blem3  16621  sylow3lem3  16628  sylow3lem4  16629  efginvrel2  16724  efgsval2  16730  efgsp1  16734  efgredlemg  16739  efgredleme  16740  efgcpbllemb  16752  odadd2  16834  odadd  16835  torsubg  16839  frgpnabllem1  16856  pgpfaclem1  17111  srgbinomlem3  17172  srgbinomlem4  17173  mplcoe5  18110  mplcoe2OLD  18112  coe1tmmul2  18296  coe1tmmul2fv  18298  coe1pwmulfv  18300  nn0srg  18465  mbfi1fseqlem3  22102  dvn2bss  22311  tdeglem4  22436  tdeglem2  22437  mdegmullem  22456  coe1mul3  22478  ply1divex  22515  fta1glem1  22544  plyaddlem1  22588  plymullem1  22589  coeeulem  22599  coemulc  22630  dgrmulc  22646  dgrcolem2  22649  dgrco  22650  dvply1  22658  dvply2g  22659  plydivlem4  22670  fta1lem  22681  vieta1lem1  22684  aareccl  22700  aaliou3lem8  22719  taylply2  22741  dvtaylp  22743  dvntaylp  22744  dvntaylp0  22745  dvradcnv  22794  pserdvlem2  22801  advlogexp  23014  cxpeq  23109  atantayl3  23248  birthdaylem2  23260  harmonicbnd4  23318  wilthlem2  23321  basellem2  23333  basellem3  23334  basellem5  23336  0sgm  23396  sgmppw  23450  chtublem  23464  chpval2  23471  sumdchr2  23523  bcp1ctr  23532  lgslem1  23549  lgseisenlem2  23603  lgseisenlem3  23604  lgsquadlem1  23607  lgsquadlem2  23608  lgsquad2lem2  23612  m1lgs  23615  2sqlem8  23625  dchrisumlem1  23652  dchrisum0flblem2  23672  rpvmasum2  23675  mulogsumlem  23694  selberg2lem  23713  pntrsumo1  23728  pntrlog2bndlem4  23743  cusgrasizeinds  24454  wlklniswwlkn2  24678  wwlknred  24701  wwlknext  24702  wwlknextbi  24703  wwlknredwwlkn  24704  wwlkextproplem2  24720  clwlkisclwwlk  24767  vdgrfiun  24880  nbhashuvtx1  24893  eupath2lem3  24957  frghash2spot  25041  usgreghash2spotv  25044  frgregordn0  25048  numclwwlk3  25087  ex-ind-dvds  25148  divnumden2  27587  2sqmod  27614  omndmul2  27680  omndmul3  27681  archiabllem1a  27713  oddpwdc  28271  eulerpartlemsv2  28275  eulerpartlems  28277  eulerpartlemsv3  28278  eulerpartlemv  28281  eulerpartlemb  28285  iwrdsplit  28304  ballotlemgun  28441  ccatmulgnn0dir  28474  ofcccat  28476  signsplypnf  28485  signslema  28497  signstfvn  28504  signstfveq0  28512  signsvtp  28518  signsvtn  28519  signlem0  28522  signshf  28523  dmgmaddnn0  28547  lgamucov  28558  subfacp1lem6  28607  subfacval2  28609  subfaclim  28610  cvmliftlem7  28714  elmrsubrn  28858  relexpadd  29039  rtrclreclem.trans  29047  risefacval2  29108  fallfacval2  29109  fallfacval3  29110  risefallfac  29122  risefacp1  29127  fallfacp1  29128  fallfacfwd  29134  binomfallfaclem1  29137  binomfallfaclem2  29138  binomrisefac  29140  faclimlem1  29144  faclim2  29149  bpolycl  29790  bpolysum  29791  bpolydiflem  29792  fsumkthpow  29794  bpoly4  29797  rmxyneg  30832  rmxyadd  30833  rmyp1  30845  rmxm1  30846  rmym1  30847  rmxluc  30848  rmyluc  30849  rmxdbl  30851  rmydbl  30852  jm2.18  30906  jm2.19lem1  30907  jm2.19lem2  30908  jm2.22  30913  jm2.23  30914  jm2.25  30917  jm2.27c  30925  rmxdiophlem  30933  expdioph  30941  hbtlem4  31051  itgpowd  31158  radcnvrat  31171  lcmgcd  31189  lcmid  31191  nzprmdif  31200  fzisoeu  31454  mccllem  31559  dvxpaek  31691  dvnxpaek  31693  dvnmul  31694  dvnprodlem1  31697  dvnprodlem2  31698  stoweidlem24  31760  stirlinglem3  31812  stirlinglem7  31816  fourierdlem36  31879  fourierdlem47  31890  etransclem23  31994  etransclem32  32003  etransclem48  32019  fz0addcom  32287  altgsumbc  32809  altgsumbcALT  32810
  Copyright terms: Public domain W3C validator