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

Theorem nn0cnd 10626
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 10625 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9400 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   CCcc 9268   NN0cn0 10567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-i2m1 9338  ax-1ne0 9339  ax-rnegex 9341  ax-rrecex 9342  ax-cnre 9343
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-ov 6083  df-om 6466  df-recs 6818  df-rdg 6852  df-nn 10311  df-n0 10568
This theorem is referenced by:  expaddzlem  11891  expaddz  11892  expmulz  11894  facdiv  12047  faclbnd4lem3  12055  bcp1n  12076  bcn2m1  12084  bcn2p1  12085  hashgadd  12124  hashdom  12126  hashun3  12131  hashssdif  12151  hashxplem  12179  hashmap  12181  hashbclem  12189  hashf1lem2  12193  hashf1  12194  ccatcl  12258  ccatval3  12262  ccatlid  12268  ccatrid  12269  ccatass  12270  wrdlenccats1lenm1  12289  ccats1val2  12291  ccatws1lenrev  12293  swrdid  12305  addlenswrd  12315  swrdtrcfvl  12328  swrdccat2  12336  ccatopth2  12349  cats1un  12354  swrdccat3b  12371  spllen  12380  splfv2a  12382  revccat  12390  cshwlen  12420  cshwidxmod  12424  repswcshw  12430  2cshwid  12432  cshweqdif2  12437  isercoll2  13130  iseraltlem3  13145  binomlem  13275  bcxmas  13281  incexclem  13282  incexc  13283  incexc2  13284  climcndslem1  13295  climcndslem2  13296  arisum  13305  arisum2  13306  geomulcvg  13319  mertens  13329  effsumlt  13378  dvdsexp  13572  divalgmod  13593  bitsinv1lem  13620  sadcp1  13634  sadcaddlem  13636  sadadd2lem  13638  sadadd3  13640  sadaddlem  13645  sadasslem  13649  smupp1  13659  smumullem  13671  mulgcd  13713  absmulgcd  13714  mulgcdr  13715  gcddiv  13716  mulgcddvds  13773  qredeu  13776  odzdvds  13850  coprimeprodsq  13859  pceulem  13895  pczpre  13897  pcqmul  13903  pcaddlem  13933  pcmpt  13937  pcmpt2  13938  sumhash  13941  mul4sq  13998  4sqlem12  14000  vdwapun  14018  vdwlem2  14026  vdwlem3  14027  vdwlem6  14030  vdwlem8  14032  vdwlem9  14033  ramub1lem2  14071  ramcl  14073  mulgnn0dir  15630  mulgnn0ass  15636  lagsubg2  15722  psgnunilem2  15981  odmodnn0  16023  odmulg  16037  odmulgeq  16038  odinv  16042  sylow1lem1  16077  sylow2a  16098  sylow2blem3  16101  sylow3lem3  16108  sylow3lem4  16109  efginvrel2  16204  efgsval2  16210  efgsp1  16214  efgredlemg  16219  efgredleme  16220  efgcpbllemb  16232  odadd2  16311  odadd  16312  torsubg  16316  frgpnabllem1  16331  pgpfaclem1  16556  mplcoe2  17481  mplcoe2OLD  17482  coe1tmmul2  17627  coe1tmmul2fv  17629  coe1pwmulfv  17631  mbfi1fseqlem3  21037  dvn2bss  21246  tdeglem4  21414  tdeglem2  21415  mdegmullem  21434  coe1mul3  21456  ply1divex  21493  fta1glem1  21522  plyaddlem1  21566  plymullem1  21567  coeeulem  21577  coemulc  21607  dgrmulc  21623  dgrcolem2  21626  dgrco  21627  dvply1  21635  dvply2g  21636  plydivlem4  21647  fta1lem  21658  vieta1lem1  21661  aareccl  21677  aaliou3lem8  21696  taylply2  21718  dvtaylp  21720  dvntaylp  21721  dvntaylp0  21722  dvradcnv  21771  pserdvlem2  21778  advlogexp  21985  cxpeq  22080  atantayl3  22219  birthdaylem2  22231  harmonicbnd4  22289  wilthlem2  22292  basellem2  22304  basellem3  22305  basellem5  22307  0sgm  22367  sgmppw  22421  chtublem  22435  chpval2  22442  sumdchr2  22494  bcp1ctr  22503  lgslem1  22520  lgseisenlem2  22574  lgseisenlem3  22575  lgsquadlem1  22578  lgsquadlem2  22579  lgsquad2lem2  22583  m1lgs  22586  2sqlem8  22596  dchrisumlem1  22623  dchrisum0flblem2  22643  rpvmasum2  22646  mulogsumlem  22665  selberg2lem  22684  pntrsumo1  22699  pntrlog2bndlem4  22714  cusgrasizeinds  23207  vdgrfiun  23395  eupath2lem3  23423  divnumden2  25910  omndmul2  25999  omndmul3  26000  archiabllem1a  26032  oddpwdc  26585  eulerpartlemsv2  26589  eulerpartlems  26591  eulerpartlemsv3  26592  eulerpartlemv  26595  eulerpartlemb  26599  iwrdsplit  26618  ballotlemgun  26755  ccatmulgnn0dir  26788  ofcccat  26790  signsplypnf  26799  signslema  26811  signstfvn  26818  signstfveq0  26826  signsvtp  26832  signsvtn  26833  signlem0  26836  signshf  26837  dmgmaddnn0  26861  lgamucov  26872  subfacp1lem6  26921  subfacval2  26923  subfaclim  26924  cvmliftlem7  27028  relexpadd  27187  rtrclreclem.trans  27195  risefacval2  27360  fallfacval2  27361  fallfacval3  27362  risefallfac  27374  risefacp1  27379  fallfacp1  27380  fallfacfwd  27386  binomfallfaclem1  27389  binomfallfaclem2  27390  binomrisefac  27392  faclimlem1  27396  faclim2  27401  bpolycl  28042  bpolysum  28043  bpolydiflem  28044  fsumkthpow  28046  bpoly4  28049  rmxyneg  29106  rmxyadd  29107  rmyp1  29119  rmxm1  29120  rmym1  29121  rmxluc  29122  rmyluc  29123  rmxdbl  29125  rmydbl  29126  jm2.18  29182  jm2.19lem1  29183  jm2.19lem2  29184  jm2.22  29189  jm2.23  29190  jm2.25  29193  jm2.27c  29201  rmxdiophlem  29209  expdioph  29217  hbtlem4  29327  itgpowd  29435  stoweidlem24  29665  stirlinglem3  29717  stirlinglem7  29721  fz0addcom  30046  powm2modprm  30094  ccatw2s1p1  30115  wwlknext  30202  wwlknextbi  30203  wwlknredwwlkn  30204  clwlkisclwwlk  30297  nbhashuvtx1  30379  wwlkextproplem2  30407  frghash2spot  30502  usgreghash2spotv  30505  frgregordn0  30509  numclwwlk3  30548
  Copyright terms: Public domain W3C validator