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

Theorem nn0cnd 10750
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 10749 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9524 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   CCcc 9392   NN0cn0 10691
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4522  ax-nul 4530  ax-pow 4579  ax-pr 4640  ax-un 6483  ax-resscn 9451  ax-1cn 9452  ax-icn 9453  ax-addcl 9454  ax-addrcl 9455  ax-mulcl 9456  ax-mulrcl 9457  ax-i2m1 9462  ax-1ne0 9463  ax-rnegex 9465  ax-rrecex 9466  ax-cnre 9467
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-reu 2806  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3747  df-if 3901  df-pw 3971  df-sn 3987  df-pr 3989  df-tp 3991  df-op 3993  df-uni 4201  df-iun 4282  df-br 4402  df-opab 4460  df-mpt 4461  df-tr 4495  df-eprel 4741  df-id 4745  df-po 4750  df-so 4751  df-fr 4788  df-we 4790  df-ord 4831  df-on 4832  df-lim 4833  df-suc 4834  df-xp 4955  df-rel 4956  df-cnv 4957  df-co 4958  df-dm 4959  df-rn 4960  df-res 4961  df-ima 4962  df-iota 5490  df-fun 5529  df-fn 5530  df-f 5531  df-f1 5532  df-fo 5533  df-f1o 5534  df-fv 5535  df-ov 6204  df-om 6588  df-recs 6943  df-rdg 6977  df-nn 10435  df-n0 10692
This theorem is referenced by:  quoremnn0ALT  11814  expaddzlem  12025  expaddz  12026  expmulz  12028  facdiv  12181  faclbnd4lem3  12189  bcp1n  12210  bcn2m1  12218  bcn2p1  12219  hashgadd  12259  hashdom  12261  hashun3  12266  hashssdif  12286  hashxplem  12314  hashmap  12316  hashbclem  12324  hashf1lem2  12328  hashf1  12329  ccatcl  12393  ccatval3  12397  ccatlid  12403  ccatrid  12404  ccatass  12405  wrdlenccats1lenm1  12424  ccats1val2  12426  ccatws1lenrev  12428  swrdid  12440  addlenswrd  12450  swrdtrcfvl  12463  swrdccat2  12471  ccatopth2  12484  cats1un  12489  swrdccat3b  12506  spllen  12515  splfv2a  12517  revccat  12525  cshwlen  12555  cshwidxmod  12559  repswcshw  12565  2cshwid  12567  cshweqdif2  12572  isercoll2  13265  iseraltlem3  13280  binomlem  13411  bcxmas  13417  incexclem  13418  incexc  13419  incexc2  13420  climcndslem1  13431  climcndslem2  13432  arisum  13441  arisum2  13442  geomulcvg  13455  mertens  13465  effsumlt  13514  dvdsexp  13708  divalgmod  13729  bitsinv1lem  13756  sadcp1  13770  sadcaddlem  13772  sadadd2lem  13774  sadadd3  13776  sadaddlem  13781  sadasslem  13785  smupp1  13795  smumullem  13807  mulgcd  13849  absmulgcd  13850  mulgcdr  13851  gcddiv  13852  mulgcddvds  13909  qredeu  13912  odzdvds  13986  coprimeprodsq  13995  pceulem  14031  pczpre  14033  pcqmul  14039  pcaddlem  14069  pcmpt  14073  pcmpt2  14074  sumhash  14077  mul4sq  14134  4sqlem12  14136  vdwapun  14154  vdwlem2  14162  vdwlem3  14163  vdwlem6  14166  vdwlem8  14168  vdwlem9  14169  ramub1lem2  14207  ramcl  14209  mulgnn0dir  15770  mulgnn0ass  15776  lagsubg2  15862  psgnunilem2  16121  odmodnn0  16165  odmulg  16179  odmulgeq  16180  odinv  16184  sylow1lem1  16219  sylow2a  16240  sylow2blem3  16243  sylow3lem3  16250  sylow3lem4  16251  efginvrel2  16346  efgsval2  16352  efgsp1  16356  efgredlemg  16361  efgredleme  16362  efgcpbllemb  16374  odadd2  16453  odadd  16454  torsubg  16458  frgpnabllem1  16473  pgpfaclem1  16705  srgbinomlem3  16764  srgbinomlem4  16765  mplcoe5  17673  mplcoe2OLD  17675  coe1tmmul2  17854  coe1tmmul2fv  17856  coe1pwmulfv  17858  mbfi1fseqlem3  21329  dvn2bss  21538  tdeglem4  21663  tdeglem2  21664  mdegmullem  21683  coe1mul3  21705  ply1divex  21742  fta1glem1  21771  plyaddlem1  21815  plymullem1  21816  coeeulem  21826  coemulc  21856  dgrmulc  21872  dgrcolem2  21875  dgrco  21876  dvply1  21884  dvply2g  21885  plydivlem4  21896  fta1lem  21907  vieta1lem1  21910  aareccl  21926  aaliou3lem8  21945  taylply2  21967  dvtaylp  21969  dvntaylp  21970  dvntaylp0  21971  dvradcnv  22020  pserdvlem2  22027  advlogexp  22234  cxpeq  22329  atantayl3  22468  birthdaylem2  22480  harmonicbnd4  22538  wilthlem2  22541  basellem2  22553  basellem3  22554  basellem5  22556  0sgm  22616  sgmppw  22670  chtublem  22684  chpval2  22691  sumdchr2  22743  bcp1ctr  22752  lgslem1  22769  lgseisenlem2  22823  lgseisenlem3  22824  lgsquadlem1  22827  lgsquadlem2  22828  lgsquad2lem2  22832  m1lgs  22835  2sqlem8  22845  dchrisumlem1  22872  dchrisum0flblem2  22892  rpvmasum2  22895  mulogsumlem  22914  selberg2lem  22933  pntrsumo1  22948  pntrlog2bndlem4  22963  cusgrasizeinds  23537  vdgrfiun  23725  eupath2lem3  23753  divnumden2  26233  omndmul2  26321  omndmul3  26322  archiabllem1a  26354  oddpwdc  26882  eulerpartlemsv2  26886  eulerpartlems  26888  eulerpartlemsv3  26889  eulerpartlemv  26892  eulerpartlemb  26896  iwrdsplit  26915  ballotlemgun  27052  ccatmulgnn0dir  27085  ofcccat  27087  signsplypnf  27096  signslema  27108  signstfvn  27115  signstfveq0  27123  signsvtp  27129  signsvtn  27130  signlem0  27133  signshf  27134  dmgmaddnn0  27158  lgamucov  27169  subfacp1lem6  27218  subfacval2  27220  subfaclim  27221  cvmliftlem7  27325  relexpadd  27485  rtrclreclem.trans  27493  risefacval2  27658  fallfacval2  27659  fallfacval3  27660  risefallfac  27672  risefacp1  27677  fallfacp1  27678  fallfacfwd  27684  binomfallfaclem1  27687  binomfallfaclem2  27688  binomrisefac  27690  faclimlem1  27694  faclim2  27699  bpolycl  28340  bpolysum  28341  bpolydiflem  28342  fsumkthpow  28344  bpoly4  28347  rmxyneg  29410  rmxyadd  29411  rmyp1  29423  rmxm1  29424  rmym1  29425  rmxluc  29426  rmyluc  29427  rmxdbl  29429  rmydbl  29430  jm2.18  29486  jm2.19lem1  29487  jm2.19lem2  29488  jm2.22  29493  jm2.23  29494  jm2.25  29497  jm2.27c  29505  rmxdiophlem  29513  expdioph  29521  hbtlem4  29631  itgpowd  29739  stoweidlem24  29968  stirlinglem3  30020  stirlinglem7  30024  fz0addcom  30349  powm2modprm  30397  ccatw2s1p1  30418  wwlknext  30505  wwlknextbi  30506  wwlknredwwlkn  30507  clwlkisclwwlk  30600  nbhashuvtx1  30682  wwlkextproplem2  30710  frghash2spot  30805  usgreghash2spotv  30808  frgregordn0  30812  numclwwlk3  30851  altgsumbc  30898  altgsumbcALT  30899
  Copyright terms: Public domain W3C validator