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

Theorem nn0cnd 10928
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 10927 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9670 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1868   CCcc 9538   NN0cn0 10870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594  ax-resscn 9597  ax-1cn 9598  ax-icn 9599  ax-addcl 9600  ax-addrcl 9601  ax-mulcl 9602  ax-mulrcl 9603  ax-i2m1 9608  ax-1ne0 9609  ax-rnegex 9611  ax-rrecex 9612  ax-cnre 9613
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4761  df-id 4765  df-po 4771  df-so 4772  df-fr 4809  df-we 4811  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-pred 5396  df-ord 5442  df-on 5443  df-lim 5444  df-suc 5445  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-ov 6305  df-om 6704  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-nn 10611  df-n0 10871
This theorem is referenced by:  quoremnn0ALT  12084  expaddzlem  12315  expaddz  12316  expmulz  12318  facdiv  12472  faclbnd4lem3  12480  bcp1n  12501  bcn2m1  12509  bcn2p1  12510  hashgadd  12556  hashdom  12558  hashun3  12563  hashssdif  12587  hashxplem  12603  hashmap  12605  hashbclem  12613  hashf1lem2  12617  hashf1  12618  ccatval3  12717  ccatlid  12723  ccatrid  12724  ccatass  12725  ccatrn  12726  lswccatn0lsw  12727  wrdlenccats1lenm1  12747  ccats1val2  12751  ccatws1lenrev  12755  swrd0f  12774  swrdid  12775  addlenswrd  12785  swrdtrcfvl  12797  swrdccat2  12805  ccatopth2  12818  wrdeqcats1OLD  12821  cats1un  12823  swrdccat3b  12843  spllen  12852  splfv2a  12854  revccat  12862  cshwlen  12892  cshwidxmod  12896  repswcshw  12902  2cshwid  12904  cshweqdif2  12909  relexpaddg  13105  rtrclreclem3  13112  isercoll2  13720  iseraltlem3  13738  binomlem  13875  bcxmas  13881  incexclem  13882  incexc  13883  incexc2  13884  climcndslem1  13895  climcndslem2  13896  arisum  13906  arisum2  13907  geomulcvg  13920  mertens  13930  risefacval2  14051  fallfacval2  14052  fallfacval3  14053  risefallfac  14065  risefacp1  14070  fallfacp1  14071  fallfacfwd  14077  binomfallfaclem1  14080  binomfallfaclem2  14081  binomrisefac  14083  bpolycl  14093  bpolysum  14094  bpolydiflem  14095  fsumkthpow  14097  bpoly4  14100  effsumlt  14153  dvdsexp  14349  divalgmod  14375  bitsinv1lem  14403  sadcp1  14417  sadcaddlem  14419  sadadd2lem  14421  sadadd3  14423  sadaddlem  14428  sadasslem  14432  smupp1  14442  smumullem  14454  mulgcd  14502  absmulgcd  14503  mulgcdr  14504  gcddiv  14505  lcmgcd  14560  lcmid  14562  lcm1  14563  3lcm2e6woprm  14568  6lcm4e12  14569  mulgcddvds  14649  qredeu  14652  odzdvds  14728  odzdvdsOLD  14734  powm2modprm  14742  coprimeprodsq  14747  pceulem  14783  pczpre  14785  pcqmul  14791  pcaddlem  14821  pcmpt  14825  pcmpt2  14826  sumhash  14829  mul4sq  14886  4sqlem12  14888  vdwapun  14912  vdwlem2  14920  vdwlem3  14921  vdwlem6  14924  vdwlem8  14926  vdwlem9  14927  ramub1lem2  14973  ramcl  14975  mulgnn0dir  16769  mulgnn0ass  16775  lagsubg2  16866  psgnunilem2  17124  odmodnn0  17177  odmulg  17195  odmulgeq  17196  odinv  17200  sylow1lem1  17238  sylow2a  17259  sylow2blem3  17262  sylow3lem3  17269  sylow3lem4  17270  efginvrel2  17365  efgsval2  17371  efgsp1  17375  efgredlemg  17380  efgredleme  17381  efgcpbllemb  17393  odadd2  17475  odadd  17476  torsubg  17480  frgpnabllem1  17497  pgpfaclem1  17702  srgbinomlem3  17763  srgbinomlem4  17764  mplcoe5  18680  coe1tmmul2  18857  coe1tmmul2fv  18859  coe1pwmulfv  18861  nn0srg  19024  mbfi1fseqlem3  22662  dvn2bss  22871  tdeglem4  22996  tdeglem2  22997  mdegmullem  23014  coe1mul3  23035  ply1divex  23074  fta1glem1  23103  plyaddlem1  23154  plymullem1  23155  coeeulem  23165  coemulc  23196  dgrmulc  23212  dgrcolem2  23215  dgrco  23216  dvply1  23224  dvply2g  23225  plydivlem4  23236  fta1lem  23247  vieta1lem1  23250  aareccl  23269  aaliou3lem8  23288  taylply2  23310  dvtaylp  23312  dvntaylp  23313  dvntaylp0  23314  dvradcnv  23363  pserdvlem2  23370  advlogexp  23587  cxpeq  23684  atantayl3  23852  birthdaylem2  23865  harmonicbnd4  23923  dmgmaddnn0  23939  lgamucov  23950  wilthlem2  23981  basellem2  23995  basellem3  23996  basellem5  23998  0sgm  24058  sgmppw  24112  chtublem  24126  chpval2  24133  sumdchr2  24185  bcp1ctr  24194  lgslem1  24211  lgseisenlem2  24265  lgseisenlem3  24266  lgsquadlem1  24269  lgsquadlem2  24270  lgsquad2lem2  24274  m1lgs  24277  2sqlem8  24287  dchrisumlem1  24314  dchrisum0flblem2  24334  rpvmasum2  24337  mulogsumlem  24356  selberg2lem  24375  pntrsumo1  24390  pntrlog2bndlem4  24405  cusgrasizeinds  25190  wlklniswwlkn2  25414  wwlknred  25437  wwlknext  25438  wwlknextbi  25439  wwlknredwwlkn  25440  wwlkextproplem2  25456  clwlkisclwwlk  25503  vdgrfiun  25616  nbhashuvtx1  25629  eupath2lem3  25693  frghash2spot  25777  usgreghash2spotv  25780  frgregordn0  25784  numclwwlk3  25823  ex-ind-dvds  25885  divnumden2  28376  2sqmod  28404  omndmul2  28470  omndmul3  28471  archiabllem1a  28503  oddpwdc  29183  eulerpartlemsv2  29187  eulerpartlems  29189  eulerpartlemsv3  29190  eulerpartlemv  29193  eulerpartlemb  29197  iwrdsplit  29216  ballotlemgun  29353  ballotlemgunOLD  29391  ccatmulgnn0dir  29424  ofcccat  29426  signsplypnf  29435  signslema  29447  signstfvn  29454  signstfveq0  29462  signsvtp  29468  signsvtn  29469  signlem0  29472  signshf  29473  subfacp1lem6  29904  subfacval2  29906  subfaclim  29907  cvmliftlem7  30010  elmrsubrn  30154  bcprod  30369  bccolsum  30370  faclimlem1  30374  faclim2  30379  fwddifnp1  30925  poimirlem4  31858  poimirlem5  31859  poimirlem6  31860  poimirlem7  31861  poimirlem10  31864  poimirlem11  31865  poimirlem12  31866  poimirlem16  31870  poimirlem17  31871  poimirlem19  31873  poimirlem20  31874  poimirlem22  31876  poimirlem24  31878  poimirlem25  31879  poimirlem29  31883  poimirlem31  31885  rmxyneg  35688  rmxyadd  35689  rmyp1  35701  rmxm1  35702  rmym1  35703  rmxluc  35704  rmyluc  35705  rmxdbl  35707  rmydbl  35708  jm2.18  35763  jm2.19lem1  35764  jm2.19lem2  35765  jm2.22  35770  jm2.23  35771  jm2.25  35774  jm2.27c  35782  rmxdiophlem  35790  expdioph  35798  hbtlem4  35905  itgpowd  36019  relexpmulg  36162  radcnvrat  36521  nzprmdif  36526  bcc0  36547  bccp1k  36548  bccbc  36552  binomcxplemnn0  36556  binomcxplemrat  36557  binomcxplemfrat  36558  binomcxplemnotnn0  36563  fzisoeu  37360  mccllem  37497  dvxpaek  37635  dvnxpaek  37637  dvnmul  37638  dvnprodlem1  37641  dvnprodlem2  37642  stoweidlem24  37704  stirlinglem3  37758  stirlinglem7  37762  fourierdlem36  37826  fourierdlem47  37837  etransclem23  37942  etransclem32  37951  etransclem48OLD  37967  etransclem48  37968  addlenpfx  38651  pfxfv  38652  pfxtrcfvl  38658  pfxpfx  38668  ccats1pfxeq  38674  fz0addcom  38746  altgsumbc  39407  altgsumbcALT  39408  nn0ob  39604  nnpw2pmod  39668  dignn0ehalf  39702  nn0sumshdiglemA  39704  nn0sumshdiglemB  39705  nn0sumshdiglem2  39707  nn0mullong  39710  aacllem  39814
  Copyright terms: Public domain W3C validator