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

Theorem nn0cnd 11203
Description: A nonnegative integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nn0red.1 (𝜑𝐴 ∈ ℕ0)
Assertion
Ref Expression
nn0cnd (𝜑𝐴 ∈ ℂ)

Proof of Theorem nn0cnd
StepHypRef Expression
1 nn0red.1 . . 3 (𝜑𝐴 ∈ ℕ0)
21nn0red 11202 . 2 (𝜑𝐴 ∈ ℝ)
32recnd 9925 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  cc 9791  0cn0 11142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-i2m1 9861  ax-1ne0 9862  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-ov 6530  df-om 6936  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-nn 10871  df-n0 11143
This theorem is referenced by:  quoremnn0ALT  12476  expaddzlem  12723  expaddz  12724  expmulz  12726  facdiv  12894  faclbnd4lem3  12902  bcp1n  12923  bcn2m1  12931  bcn2p1  12932  hashgadd  12982  hashdom  12984  hashun3  12989  hashssdif  13016  hashdifpr  13019  hashxplem  13035  hashmap  13037  hashbclem  13048  hashf1lem2  13052  hashf1  13053  ccatval3  13165  ccatlid  13171  ccatrid  13172  ccatass  13173  ccatrn  13174  lswccatn0lsw  13175  ccatalpha  13177  wrdlenccats1lenm1  13201  ccats1val2  13205  ccatws1lenrev  13209  swrd0f  13228  swrdid  13229  addlenswrd  13239  swrdtrcfvl  13251  swrdccat2  13259  ccatopth2  13272  cats1un  13276  swrdccat3b  13296  spllen  13305  splfv2a  13307  revccat  13315  cshwlen  13345  cshwidxmod  13349  repswcshw  13358  2cshwid  13360  cshweqdif2  13365  relexpaddg  13590  rtrclreclem3  13597  isercoll2  14196  iseraltlem3  14211  binomlem  14349  bcxmas  14355  incexclem  14356  incexc  14357  incexc2  14358  climcndslem1  14369  climcndslem2  14370  arisum  14380  arisum2  14381  geomulcvg  14395  mertens  14406  risefacval2  14529  fallfacval2  14530  fallfacval3  14531  risefallfac  14543  risefacp1  14548  fallfacp1  14549  fallfacfwd  14555  binomfallfaclem1  14558  binomfallfaclem2  14559  binomrisefac  14561  bpolycl  14571  bpolysum  14572  bpolydiflem  14573  fsumkthpow  14575  bpoly4  14578  effsumlt  14629  dvdsexp  14836  nn0ob  14887  divalgmod  14916  divalgmodOLD  14917  bitsinv1lem  14950  sadcp1  14964  sadcaddlem  14966  sadadd2lem  14968  sadadd3  14970  sadaddlem  14975  sadasslem  14979  smupp1  14989  smumullem  15001  mulgcd  15052  absmulgcd  15053  mulgcdr  15054  gcddiv  15055  lcmgcd  15107  lcmid  15109  lcm1  15110  3lcm2e6woprm  15115  6lcm4e12  15116  mulgcddvds  15156  qredeu  15159  divgcdcoprm0  15166  divgcdcoprmex  15167  cncongr1  15168  cncongr2  15169  odzdvds  15287  powm2modprm  15295  coprimeprodsq  15300  pceulem  15337  pczpre  15339  pcqmul  15345  pcaddlem  15379  pcmpt  15383  pcmpt2  15384  sumhash  15387  oddprmdvds  15394  mul4sq  15445  4sqlem12  15447  vdwapun  15465  vdwlem2  15473  vdwlem3  15474  vdwlem6  15477  vdwlem8  15479  vdwlem9  15480  ramub1lem2  15518  ramcl  15520  mulgnn0dir  17343  mulgnn0ass  17350  lagsubg2  17427  psgnunilem2  17687  odmodnn0  17731  odmulg  17745  odmulgeq  17746  odinv  17750  sylow1lem1  17785  sylow2a  17806  sylow2blem3  17809  sylow3lem3  17816  sylow3lem4  17817  efginvrel2  17912  efgsval2  17918  efgsp1  17922  efgredlemg  17927  efgredleme  17928  efgcpbllemb  17940  odadd2  18024  odadd  18025  torsubg  18029  frgpnabllem1  18048  pgpfaclem1  18252  srgbinomlem3  18314  srgbinomlem4  18315  mplcoe5  19238  coe1tmmul2  19416  coe1tmmul2fv  19418  coe1pwmulfv  19420  nn0srg  19584  mbfi1fseqlem3  23235  dvn2bss  23444  tdeglem4  23569  tdeglem2  23570  mdegmullem  23587  coe1mul3  23608  ply1divex  23645  fta1glem1  23674  plyaddlem1  23718  plymullem1  23719  coeeulem  23729  coemulc  23760  dgrmulc  23776  dgrcolem2  23779  dgrco  23780  dvply1  23788  dvply2g  23789  plydivlem4  23800  fta1lem  23811  vieta1lem1  23814  aareccl  23830  aaliou3lem8  23849  taylply2  23871  dvtaylp  23873  dvntaylp  23874  dvntaylp0  23875  dvradcnv  23924  pserdvlem2  23931  advlogexp  24146  cxpeq  24243  atantayl3  24411  birthdaylem2  24424  harmonicbnd4  24482  dmgmaddnn0  24498  lgamucov  24509  wilthlem2  24540  basellem2  24553  basellem3  24554  basellem5  24556  0sgm  24615  sgmppw  24667  chtublem  24681  chpval2  24688  sumdchr2  24740  bcp1ctr  24749  lgslem1  24767  gausslemma2dlem6  24842  gausslemma2d  24844  lgseisenlem2  24846  lgseisenlem3  24847  lgsquadlem1  24850  lgsquadlem2  24851  lgsquad2lem2  24855  m1lgs  24858  2lgslem1c  24863  2lgslem3a  24866  2lgslem3b  24867  2lgslem3c  24868  2lgslem3d  24869  2sqlem8  24896  dchrisumlem1  24923  dchrisum0flblem2  24943  rpvmasum2  24946  mulogsumlem  24965  selberg2lem  24984  pntrsumo1  24999  pntrlog2bndlem4  25014  cusgrasizeinds  25798  wlklniswwlkn2  26022  wwlknred  26045  wwlknext  26046  wwlknextbi  26047  wwlknredwwlkn  26048  wwlkextproplem2  26064  clwlkisclwwlk  26111  vdgrfiun  26223  nbhashuvtx1  26236  eupath2lem3  26300  frghash2spot  26384  usgreghash2spotv  26387  frgregordn0  26391  numclwwlk3  26430  ex-lcm  26501  ex-ind-dvds  26504  divnumden2  28785  2sqmod  28813  omndmul2  28877  omndmul3  28878  archiabllem1a  28910  oddpwdc  29577  eulerpartlemsv2  29581  eulerpartlems  29583  eulerpartlemsv3  29584  eulerpartlemv  29587  eulerpartlemb  29591  iwrdsplit  29610  ballotlemgun  29747  ccatmulgnn0dir  29779  ofcccat  29780  signsplypnf  29787  signslema  29799  signstfvn  29806  signstfveq0  29814  signsvtp  29820  signsvtn  29821  signlem0  29824  signshf  29825  subfacp1lem6  30255  subfacval2  30257  subfaclim  30258  cvmliftlem7  30361  elmrsubrn  30505  bcprod  30711  bccolsum  30712  faclimlem1  30716  faclim2  30721  fwddifnp1  31276  knoppndvlem6  31512  knoppndvlem14  31520  poimirlem4  32407  poimirlem5  32408  poimirlem6  32409  poimirlem7  32410  poimirlem10  32413  poimirlem11  32414  poimirlem12  32415  poimirlem16  32419  poimirlem17  32420  poimirlem19  32422  poimirlem20  32423  poimirlem22  32425  poimirlem24  32427  poimirlem25  32428  poimirlem29  32432  poimirlem31  32434  rmxyneg  36327  rmxyadd  36328  rmyp1  36340  rmxm1  36341  rmym1  36342  rmxluc  36343  rmyluc  36344  rmxdbl  36346  rmydbl  36347  jm2.18  36397  jm2.19lem1  36398  jm2.19lem2  36399  jm2.22  36404  jm2.23  36405  jm2.25  36408  jm2.27c  36416  rmxdiophlem  36424  expdioph  36432  hbtlem4  36539  itgpowd  36643  relexpmulg  36845  radcnvrat  37359  nzprmdif  37364  bcc0  37385  bccp1k  37386  bccbc  37390  binomcxplemnn0  37394  binomcxplemrat  37395  binomcxplemfrat  37396  binomcxplemnotnn0  37401  fzisoeu  38279  mccllem  38488  dvxpaek  38654  dvnxpaek  38656  dvnmul  38657  dvnprodlem1  38660  dvnprodlem2  38661  stoweidlem24  38741  stirlinglem3  38793  stirlinglem7  38797  fourierdlem36  38860  fourierdlem47  38870  etransclem23  38974  etransclem32  38983  etransclem48  38999  fmtnom1nn  39807  fmtnof1  39810  fmtnorec1  39812  sqrtpwpw2p  39813  fmtnorec2lem  39817  fmtnorec3  39823  fmtnofac2lem  39843  fmtnofac2  39844  fmtnofac1  39845  pwdif  39864  lighneallem3  39887  lighneallem4b  39889  addlenpfx  40086  pfxfv  40087  pfxtrcfvl  40093  pfxpfx  40103  ccats1pfxeq  40109  fz0addcom  40201  1wlklenvm1  40848  crctcshlem4  41045  crctcsh  41049  1wlklnwwlkln2lem  41101  wwlksnred  41120  wwlksnext  41121  wwlksnextbi  41122  wwlksnredwwlkn  41123  wwlksnextproplem2  41138  rusgrnumwwlks  41199  rusgrnumwwlk  41200  clwlkclwwlk  41233  eupth2lem3lem3  41420  eupth2lem3lem6  41423  frgrhash2wsp  41519  fusgreghash2wspv  41521  frrusgrord0  41525  av-numclwwlk1  41550  av-numclwwlk3  41561  altgsumbc  41945  altgsumbcALT  41946  nnpw2pmod  42197  dignn0ehalf  42231  nn0sumshdiglemA  42233  nn0sumshdiglemB  42234  nn0sumshdiglem2  42236  nn0mullong  42239  aacllem  42339
  Copyright terms: Public domain W3C validator