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

Theorem nn0cnd 10956
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 10955 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9695 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1898   CCcc 9563   NN0cn0 10898
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-i2m1 9633  ax-1ne0 9634  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6318  df-om 6720  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-nn 10638  df-n0 10899
This theorem is referenced by:  quoremnn0ALT  12116  expaddzlem  12347  expaddz  12348  expmulz  12350  facdiv  12504  faclbnd4lem3  12512  bcp1n  12533  bcn2m1  12541  bcn2p1  12542  hashgadd  12588  hashdom  12590  hashun3  12595  hashssdif  12621  hashdifpr  12624  hashxplem  12638  hashmap  12640  hashbclem  12648  hashf1lem2  12652  hashf1  12653  ccatval3  12760  ccatlid  12766  ccatrid  12767  ccatass  12768  ccatrn  12769  lswccatn0lsw  12770  wrdlenccats1lenm1  12793  ccats1val2  12797  ccatws1lenrev  12801  swrd0f  12820  swrdid  12821  addlenswrd  12831  swrdtrcfvl  12843  swrdccat2  12851  ccatopth2  12864  wrdeqcats1OLD  12867  cats1un  12869  swrdccat3b  12889  spllen  12898  splfv2a  12900  revccat  12908  cshwlen  12938  cshwidxmod  12942  repswcshw  12948  2cshwid  12950  cshweqdif2  12955  relexpaddg  13165  rtrclreclem3  13172  isercoll2  13781  iseraltlem3  13799  binomlem  13936  bcxmas  13942  incexclem  13943  incexc  13944  incexc2  13945  climcndslem1  13956  climcndslem2  13957  arisum  13967  arisum2  13968  geomulcvg  13981  mertens  13991  risefacval2  14112  fallfacval2  14113  fallfacval3  14114  risefallfac  14126  risefacp1  14131  fallfacp1  14132  fallfacfwd  14138  binomfallfaclem1  14141  binomfallfaclem2  14142  binomrisefac  14144  bpolycl  14154  bpolysum  14155  bpolydiflem  14156  fsumkthpow  14158  bpoly4  14161  effsumlt  14214  dvdsexp  14410  divalgmod  14436  bitsinv1lem  14464  sadcp1  14478  sadcaddlem  14480  sadadd2lem  14482  sadadd3  14484  sadaddlem  14489  sadasslem  14493  smupp1  14503  smumullem  14515  mulgcd  14563  absmulgcd  14564  mulgcdr  14565  gcddiv  14566  lcmgcd  14621  lcmid  14623  lcm1  14624  3lcm2e6woprm  14629  6lcm4e12  14630  mulgcddvds  14710  qredeu  14713  odzdvds  14789  odzdvdsOLD  14795  powm2modprm  14803  coprimeprodsq  14808  pceulem  14844  pczpre  14846  pcqmul  14852  pcaddlem  14882  pcmpt  14886  pcmpt2  14887  sumhash  14890  mul4sq  14947  4sqlem12  14949  vdwapun  14973  vdwlem2  14981  vdwlem3  14982  vdwlem6  14985  vdwlem8  14987  vdwlem9  14988  ramub1lem2  15034  ramcl  15036  mulgnn0dir  16830  mulgnn0ass  16836  lagsubg2  16927  psgnunilem2  17185  odmodnn0  17238  odmulg  17256  odmulgeq  17257  odinv  17261  sylow1lem1  17299  sylow2a  17320  sylow2blem3  17323  sylow3lem3  17330  sylow3lem4  17331  efginvrel2  17426  efgsval2  17432  efgsp1  17436  efgredlemg  17441  efgredleme  17442  efgcpbllemb  17454  odadd2  17536  odadd  17537  torsubg  17541  frgpnabllem1  17558  pgpfaclem1  17763  srgbinomlem3  17824  srgbinomlem4  17825  mplcoe5  18741  coe1tmmul2  18918  coe1tmmul2fv  18920  coe1pwmulfv  18922  nn0srg  19086  mbfi1fseqlem3  22724  dvn2bss  22933  tdeglem4  23058  tdeglem2  23059  mdegmullem  23076  coe1mul3  23097  ply1divex  23136  fta1glem1  23165  plyaddlem1  23216  plymullem1  23217  coeeulem  23227  coemulc  23258  dgrmulc  23274  dgrcolem2  23277  dgrco  23278  dvply1  23286  dvply2g  23287  plydivlem4  23298  fta1lem  23309  vieta1lem1  23312  aareccl  23331  aaliou3lem8  23350  taylply2  23372  dvtaylp  23374  dvntaylp  23375  dvntaylp0  23376  dvradcnv  23425  pserdvlem2  23432  advlogexp  23649  cxpeq  23746  atantayl3  23914  birthdaylem2  23927  harmonicbnd4  23985  dmgmaddnn0  24001  lgamucov  24012  wilthlem2  24043  basellem2  24057  basellem3  24058  basellem5  24060  0sgm  24120  sgmppw  24174  chtublem  24188  chpval2  24195  sumdchr2  24247  bcp1ctr  24256  lgslem1  24273  lgseisenlem2  24327  lgseisenlem3  24328  lgsquadlem1  24331  lgsquadlem2  24332  lgsquad2lem2  24336  m1lgs  24339  2sqlem8  24349  dchrisumlem1  24376  dchrisum0flblem2  24396  rpvmasum2  24399  mulogsumlem  24418  selberg2lem  24437  pntrsumo1  24452  pntrlog2bndlem4  24467  cusgrasizeinds  25253  wlklniswwlkn2  25477  wwlknred  25500  wwlknext  25501  wwlknextbi  25502  wwlknredwwlkn  25503  wwlkextproplem2  25519  clwlkisclwwlk  25566  vdgrfiun  25679  nbhashuvtx1  25692  eupath2lem3  25756  frghash2spot  25840  usgreghash2spotv  25843  frgregordn0  25847  numclwwlk3  25886  ex-ind-dvds  25948  divnumden2  28430  2sqmod  28458  omndmul2  28524  omndmul3  28525  archiabllem1a  28557  oddpwdc  29236  eulerpartlemsv2  29240  eulerpartlems  29242  eulerpartlemsv3  29243  eulerpartlemv  29246  eulerpartlemb  29250  iwrdsplit  29269  ballotlemgun  29406  ballotlemgunOLD  29444  ccatmulgnn0dir  29477  ofcccat  29479  signsplypnf  29488  signslema  29500  signstfvn  29507  signstfveq0  29515  signsvtp  29521  signsvtn  29522  signlem0  29525  signshf  29526  subfacp1lem6  29957  subfacval2  29959  subfaclim  29960  cvmliftlem7  30063  elmrsubrn  30207  bcprod  30423  bccolsum  30424  faclimlem1  30428  faclim2  30433  fwddifnp1  30981  poimirlem4  31989  poimirlem5  31990  poimirlem6  31991  poimirlem7  31992  poimirlem10  31995  poimirlem11  31996  poimirlem12  31997  poimirlem16  32001  poimirlem17  32002  poimirlem19  32004  poimirlem20  32005  poimirlem22  32007  poimirlem24  32009  poimirlem25  32010  poimirlem29  32014  poimirlem31  32016  rmxyneg  35813  rmxyadd  35814  rmyp1  35826  rmxm1  35827  rmym1  35828  rmxluc  35829  rmyluc  35830  rmxdbl  35832  rmydbl  35833  jm2.18  35888  jm2.19lem1  35889  jm2.19lem2  35890  jm2.22  35895  jm2.23  35896  jm2.25  35899  jm2.27c  35907  rmxdiophlem  35915  expdioph  35923  hbtlem4  36030  itgpowd  36144  relexpmulg  36347  radcnvrat  36707  nzprmdif  36712  bcc0  36733  bccp1k  36734  bccbc  36738  binomcxplemnn0  36742  binomcxplemrat  36743  binomcxplemfrat  36744  binomcxplemnotnn0  36749  fzisoeu  37556  mccllem  37715  dvxpaek  37853  dvnxpaek  37855  dvnmul  37856  dvnprodlem1  37859  dvnprodlem2  37860  stoweidlem24  37922  stirlinglem3  37976  stirlinglem7  37980  fourierdlem36  38044  fourierdlem47  38055  etransclem23  38160  etransclem32  38169  etransclem48OLD  38185  etransclem48  38186  addlenpfx  38979  pfxfv  38980  pfxtrcfvl  38986  pfxpfx  38996  ccats1pfxeq  39002  fz0addcom  39099  wlkOnwlk1l  39713  altgsumbc  40406  altgsumbcALT  40407  nn0ob  40603  nnpw2pmod  40667  dignn0ehalf  40701  nn0sumshdiglemA  40703  nn0sumshdiglemB  40704  nn0sumshdiglem2  40706  nn0mullong  40709  aacllem  40813
  Copyright terms: Public domain W3C validator