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

Theorem nn0cnd 10895
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 10894 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9652 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1842   CCcc 9520   NN0cn0 10836
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574  ax-resscn 9579  ax-1cn 9580  ax-icn 9581  ax-addcl 9582  ax-addrcl 9583  ax-mulcl 9584  ax-mulrcl 9585  ax-i2m1 9590  ax-1ne0 9591  ax-rnegex 9593  ax-rrecex 9594  ax-cnre 9595
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-reu 2761  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-pss 3430  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-uni 4192  df-iun 4273  df-br 4396  df-opab 4454  df-mpt 4455  df-tr 4490  df-eprel 4734  df-id 4738  df-po 4744  df-so 4745  df-fr 4782  df-we 4784  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-pred 5367  df-ord 5413  df-on 5414  df-lim 5415  df-suc 5416  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-ov 6281  df-om 6684  df-wrecs 7013  df-recs 7075  df-rdg 7113  df-nn 10577  df-n0 10837
This theorem is referenced by:  quoremnn0ALT  12022  expaddzlem  12253  expaddz  12254  expmulz  12256  facdiv  12409  faclbnd4lem3  12417  bcp1n  12438  bcn2m1  12446  bcn2p1  12447  hashgadd  12493  hashdom  12495  hashun3  12500  hashssdif  12524  hashxplem  12540  hashmap  12542  hashbclem  12550  hashf1lem2  12554  hashf1  12555  ccatval3  12651  ccatlid  12657  ccatrid  12658  ccatass  12659  ccatrn  12660  lswccatn0lsw  12661  wrdlenccats1lenm1  12681  ccats1val2  12685  ccatws1lenrev  12689  swrd0f  12708  swrdid  12709  addlenswrd  12719  swrdtrcfvl  12731  swrdccat2  12739  ccatopth2  12752  wrdeqcats1OLD  12755  cats1un  12757  swrdccat3b  12777  spllen  12786  splfv2a  12788  revccat  12796  cshwlen  12826  cshwidxmod  12830  repswcshw  12836  2cshwid  12838  cshweqdif2  12843  relexpaddg  13035  rtrclreclem3  13042  isercoll2  13640  iseraltlem3  13655  binomlem  13792  bcxmas  13798  incexclem  13799  incexc  13800  incexc2  13801  climcndslem1  13812  climcndslem2  13813  arisum  13823  arisum2  13824  geomulcvg  13837  mertens  13847  risefacval2  13955  fallfacval2  13956  fallfacval3  13957  risefallfac  13969  risefacp1  13974  fallfacp1  13975  fallfacfwd  13981  binomfallfaclem1  13984  binomfallfaclem2  13985  binomrisefac  13987  bpolycl  13997  bpolysum  13998  bpolydiflem  13999  fsumkthpow  14001  bpoly4  14004  effsumlt  14055  dvdsexp  14251  divalgmod  14273  bitsinv1lem  14300  sadcp1  14314  sadcaddlem  14316  sadadd2lem  14318  sadadd3  14320  sadaddlem  14325  sadasslem  14329  smupp1  14339  smumullem  14351  mulgcd  14393  absmulgcd  14394  mulgcdr  14395  gcddiv  14396  mulgcddvds  14454  qredeu  14457  odzdvds  14531  powm2modprm  14537  coprimeprodsq  14542  pceulem  14578  pczpre  14580  pcqmul  14586  pcaddlem  14616  pcmpt  14620  pcmpt2  14621  sumhash  14624  mul4sq  14681  4sqlem12  14683  vdwapun  14701  vdwlem2  14709  vdwlem3  14710  vdwlem6  14713  vdwlem8  14715  vdwlem9  14716  ramub1lem2  14754  ramcl  14756  mulgnn0dir  16489  mulgnn0ass  16495  lagsubg2  16586  psgnunilem2  16844  odmodnn0  16888  odmulg  16902  odmulgeq  16903  odinv  16907  sylow1lem1  16942  sylow2a  16963  sylow2blem3  16966  sylow3lem3  16973  sylow3lem4  16974  efginvrel2  17069  efgsval2  17075  efgsp1  17079  efgredlemg  17084  efgredleme  17085  efgcpbllemb  17097  odadd2  17179  odadd  17180  torsubg  17184  frgpnabllem1  17201  pgpfaclem1  17452  srgbinomlem3  17513  srgbinomlem4  17514  mplcoe5  18451  mplcoe2OLD  18453  coe1tmmul2  18637  coe1tmmul2fv  18639  coe1pwmulfv  18641  nn0srg  18806  mbfi1fseqlem3  22416  dvn2bss  22625  tdeglem4  22750  tdeglem2  22751  mdegmullem  22770  coe1mul3  22792  ply1divex  22829  fta1glem1  22858  plyaddlem1  22902  plymullem1  22903  coeeulem  22913  coemulc  22944  dgrmulc  22960  dgrcolem2  22963  dgrco  22964  dvply1  22972  dvply2g  22973  plydivlem4  22984  fta1lem  22995  vieta1lem1  22998  aareccl  23014  aaliou3lem8  23033  taylply2  23055  dvtaylp  23057  dvntaylp  23058  dvntaylp0  23059  dvradcnv  23108  pserdvlem2  23115  advlogexp  23330  cxpeq  23427  atantayl3  23595  birthdaylem2  23608  harmonicbnd4  23666  dmgmaddnn0  23682  lgamucov  23693  wilthlem2  23724  basellem2  23736  basellem3  23737  basellem5  23739  0sgm  23799  sgmppw  23853  chtublem  23867  chpval2  23874  sumdchr2  23926  bcp1ctr  23935  lgslem1  23952  lgseisenlem2  24006  lgseisenlem3  24007  lgsquadlem1  24010  lgsquadlem2  24011  lgsquad2lem2  24015  m1lgs  24018  2sqlem8  24028  dchrisumlem1  24055  dchrisum0flblem2  24075  rpvmasum2  24078  mulogsumlem  24097  selberg2lem  24116  pntrsumo1  24131  pntrlog2bndlem4  24146  cusgrasizeinds  24893  wlklniswwlkn2  25117  wwlknred  25140  wwlknext  25141  wwlknextbi  25142  wwlknredwwlkn  25143  wwlkextproplem2  25159  clwlkisclwwlk  25206  vdgrfiun  25319  nbhashuvtx1  25332  eupath2lem3  25396  frghash2spot  25480  usgreghash2spotv  25483  frgregordn0  25487  numclwwlk3  25526  ex-ind-dvds  25587  divnumden2  28060  2sqmod  28088  omndmul2  28154  omndmul3  28155  archiabllem1a  28187  oddpwdc  28799  eulerpartlemsv2  28803  eulerpartlems  28805  eulerpartlemsv3  28806  eulerpartlemv  28809  eulerpartlemb  28813  iwrdsplit  28832  ballotlemgun  28969  ccatmulgnn0dir  29002  ofcccat  29004  signsplypnf  29013  signslema  29025  signstfvn  29032  signstfveq0  29040  signsvtp  29046  signsvtn  29047  signlem0  29050  signshf  29051  subfacp1lem6  29482  subfacval2  29484  subfaclim  29485  cvmliftlem7  29588  elmrsubrn  29732  bcprod  29947  bccolsum  29948  faclimlem1  29952  faclim2  29957  fwddifnp1  30503  rmxyneg  35217  rmxyadd  35218  rmyp1  35230  rmxm1  35231  rmym1  35232  rmxluc  35233  rmyluc  35234  rmxdbl  35236  rmydbl  35237  jm2.18  35292  jm2.19lem1  35293  jm2.19lem2  35294  jm2.22  35299  jm2.23  35300  jm2.25  35303  jm2.27c  35311  rmxdiophlem  35319  expdioph  35327  hbtlem4  35439  itgpowd  35546  relexpmulg  35689  radcnvrat  36043  lcmgcd  36061  lcmid  36063  nzprmdif  36072  bcc0  36093  bccp1k  36094  bccbc  36098  binomcxplemnn0  36102  binomcxplemrat  36103  binomcxplemfrat  36104  binomcxplemnotnn0  36109  fzisoeu  36869  mccllem  36973  dvxpaek  37105  dvnxpaek  37107  dvnmul  37108  dvnprodlem1  37111  dvnprodlem2  37112  stoweidlem24  37174  stirlinglem3  37226  stirlinglem7  37230  fourierdlem36  37293  fourierdlem47  37304  etransclem23  37408  etransclem32  37417  etransclem48  37433  addlenpfx  37885  pfxfv  37886  pfxtrcfvl  37892  pfxpfx  37902  ccats1pfxeq  37908  fz0addcom  37965  altgsumbc  38452  altgsumbcALT  38453  nn0ob  38650  nnpw2pmod  38714  dignn0ehalf  38748  nn0sumshdiglemA  38750  nn0sumshdiglemB  38751  nn0sumshdiglem2  38753  nn0mullong  38756  aacllem  38860
  Copyright terms: Public domain W3C validator