Theorem nn0cnd 12567

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

Step	Hyp	Ref	Expression
1		nn0red.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
2	1	nn0red 12566	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 11237	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2149  ℂcc 11098  ℕ₀cn0 12504

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-un 7733  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-addrcl 11161  ax-mulcl 11162  ax-mulrcl 11163  ax-i2m1 11168  ax-1ne0 11169  ax-rnegex 11171  ax-rrecex 11172  ax-cnre 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-om 7863  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-nn 12234  df-n0 12505

This theorem is referenced by:  quoremnn0ALT  13890  expaddzlem  14141  expaddz  14142  expmulz  14144  facdiv  14323  faclbnd4lem3  14331  bcp1n  14352  bcn2m1  14360  bcn2p1  14361  hashgadd  14413  hashdom  14415  hashun3  14420  hashssdif  14449  hashdifpr  14452  hashxplem  14470  hashmap  14472  hashreshashfun  14476  hashbclem  14489  hashf1lem2  14493  hashf1  14494  ccatval3  14616  ccatval21sw  14623  ccatlid  14624  ccatrid  14625  ccatass  14626  ccatrn  14627  lswccatn0lsw  14629  ccatalpha  14631  ccatws1lenp1b  14659  wrdlenccats1lenm1  14660  ccats1val2  14665  swrdccat2  14707  pfxfv  14720  addlenpfx  14728  pfxtrcfvl  14734  pfxpfx  14745  lenrevpfxcctswrd  14749  ccats1pfxeq  14751  ccatopth2  14754  cats1un  14758  swrdccat3b  14777  spllen  14791  splfv2a  14793  revccat  14803  cshwlen  14836  cshwidxmod  14840  repswcshw  14849  2cshwid  14851  cshweqdif2  14856  relexpaddg  15090  rtrclreclem3  15097  isercoll2  15720  iseraltlem3  15735  fsumconst1  15842  hash2iun1dif1  15876  binomlem  15883  bcxmas  15889  incexclem  15890  incexc  15891  incexc2  15892  climcndslem1  15903  climcndslem2  15904  arisum  15914  arisum2  15915  pwdif  15922  geomulcvg  15930  mertens  15940  risefacval2  16064  fallfacval2  16065  fallfacval3  16066  risefallfac  16078  risefacp1  16083  fallfacp1  16084  fallfacfwd  16090  binomfallfaclem1  16093  binomfallfaclem2  16094  binomrisefac  16096  bpolycl  16106  bpolysum  16107  bpolydiflem  16108  fsumkthpow  16110  bpoly4  16113  effsumlt  16167  dvdsexp  16386  nn0ob  16442  divalgmod  16464  bitsinv1lem  16499  sadcp1  16513  sadcaddlem  16515  sadadd2lem  16517  sadadd3  16519  sadaddlem  16524  sadasslem  16528  smupp1  16538  smumullem  16550  mulgcd  16606  absmulgcd  16607  mulgcdr  16608  gcddiv  16609  lcmgcd  16665  lcmid  16667  lcm1  16668  3lcm2e6woprm  16673  6lcm4e12  16674  mulgcddvds  16713  qredeu  16716  divgcdcoprm0  16723  divgcdcoprmex  16724  cncongr1  16725  cncongr2  16726  odzdvds  16855  powm2modprm  16863  coprimeprodsq  16868  pceulem  16905  pczpre  16907  pcqmul  16913  pcaddlem  16948  pcmpt  16952  pcmpt2  16953  sumhash  16956  oddprmdvds  16963  mul4sq  17014  4sqlem12  17016  vdwapun  17034  vdwlem2  17042  vdwlem3  17043  vdwlem6  17046  vdwlem8  17048  vdwlem9  17049  ramub1lem2  17087  ramcl  17089  chnrev  18683  mulgnn0dir  19170  mulgnn0ass  19176  lagsubg2  19265  psgnunilem2  19565  odmodnn0  19610  odmulg  19626  odmulgeq  19627  odinv  19631  sylow1lem1  19668  sylow2a  19689  sylow2blem3  19692  sylow3lem3  19699  sylow3lem4  19700  efginvrel2  19797  efgsval2  19803  efgsp1  19807  efgredlemg  19812  efgredleme  19813  efgcpbllemb  19825  odadd2  19919  odadd  19920  torsubg  19924  frgpnabllem1  19943  pgpfaclem1  20153  fincygsubgodd  20184  omndmul2  20203  omndmul3  20204  srgbinomlem3  20310  srgbinomlem4  20311  nn0srg  21556  freshmansdream  21693  mplcoe5  22160  mhpmulcl  22281  mhppwdeg  22282  psdmplcl  22294  psdmul  22298  coe1tmmul2  22406  coe1tmmul2fv  22408  coe1pwmulfv  22410  mbfi1fseqlem3  25845  dvn2bss  26058  itgpowd  26178  tdeglem4  26186  tdeglem2  26187  mdegmullem  26204  coe1mul3  26225  ply1divex  26263  fta1glem1  26294  plyaddlem1  26339  plymullem1  26340  coeeulem  26350  coemulc  26381  dgrmulc  26397  dgrcolem2  26400  dgrco  26401  dvply1  26414  dvply2g  26415  plydivlem4  26426  fta1lem  26437  vieta1lem1  26440  aareccl  26456  aaliou3lem8  26475  taylply2  26497  dvtaylp  26499  dvntaylp  26500  dvntaylp0  26501  dvradcnv  26550  pserdvlem2  26557  advlogexp  26786  cxpeq  26888  atantayl3  27070  birthdaylem2  27083  harmonicbnd4  27141  dmgmaddnn0  27157  lgamucov  27168  wilthlem2  27199  basellem2  27212  basellem3  27213  basellem5  27215  0sgm  27274  sgmppw  27327  chtublem  27341  chpval2  27348  sumdchr2  27400  bcp1ctr  27409  lgslem1  27427  gausslemma2dlem6  27502  gausslemma2d  27504  lgseisenlem2  27506  lgseisenlem3  27507  lgsquadlem1  27510  lgsquadlem2  27511  lgsquad2lem2  27515  m1lgs  27518  2lgslem1c  27523  2lgslem3a  27526  2lgslem3b  27527  2lgslem3c  27528  2lgslem3d  27529  2sqlem8  27556  2sq2  27563  2sqmod  27566  dchrisumlem1  27619  dchrisum0flblem2  27639  rpvmasum2  27642  mulogsumlem  27661  selberg2lem  27680  pntrsumo1  27695  pntrlog2bndlem4  27710  finsumvtxdg2ssteplem4  29839  vtxdgoddnumeven  29844  wlklenvm1  29912  wlklenvclwlk  29944  crctcshlem4  30110  crctcsh  30114  wlklnwwlkln2lem  30172  wlknwwlksnbij  30178  wwlksnred  30182  wwlksnext  30183  wwlksnextbi  30184  wwlksnredwwlkn  30185  wwlksnextproplem2  30200  rusgrnumwwlks  30267  rusgrnumwwlk  30268  clwwlkccatlem  30281  clwlkclwwlk  30294  clwwlkwwlksb  30346  eupth2lem3lem3  30522  eupth2lem3lem6  30525  fusgreghash2wsp  30630  frrusgrord0lem  30631  numclwwlk1  30653  numclwwlk3  30677  ex-lcm  30750  ex-ind-dvds  30753  nnmulge  33025  elq2  33097  divnumden2  33101  ccatf1  33210  pfxlsw2ccat  33211  ccatws1f1o  33212  wrdt2ind  33214  gsummptrev  33317  gsummptp1  33318  gsummulsubdishift1  33329  cycpmco2lem2  33388  cycpmco2lem3  33389  cycpmco2lem4  33390  cycpmco2lem5  33391  cycpmco2lem6  33392  cycpmco2lem7  33393  cycpmco2  33394  archiabllem1a  33452  gsumind  33608  deg1prod  33818  ply1dg3rt0irred  33819  esplyind  33910  esplyindfv  33911  esplyfvn  33912  vietadeg1  33913  vietalem  33914  vieta  33915  iconstr  34101  cos9thpiminplylem1  34117  oddpwdc  34689  eulerpartlemsv2  34693  eulerpartlems  34695  eulerpartlemsv3  34696  eulerpartlemv  34699  eulerpartlemb  34703  iwrdsplit  34722  ballotlemgun  34860  ccatmulgnn0dir  34877  ofcccat  34878  signsplypnf  34882  signslema  34894  signstfvn  34901  signstfveq0  34909  signsvtp  34915  signsvtn  34916  signlem0  34919  signshf  34920  fsum2dsub  34939  hashreprin  34952  breprexp  34965  circlemeth  34972  lpadlem2  35015  lpadlen2  35016  revpfxsfxrev  35540  revwlk  35550  subfacp1lem6  35610  subfacval2  35612  subfaclim  35613  cvmliftlem7  35716  elmrsubrn  35945  bcprod  36163  bccolsum  36164  faclimlem1  36168  faclim2  36173  fwddifnp1  36590  knoppndvlem6  37029  knoppndvlem14  37037  poimirlem4  38197  poimirlem5  38198  poimirlem6  38199  poimirlem7  38200  poimirlem10  38203  poimirlem11  38204  poimirlem12  38205  poimirlem16  38209  poimirlem17  38210  poimirlem19  38212  poimirlem20  38213  poimirlem22  38215  poimirlem24  38217  poimirlem25  38218  poimirlem29  38222  poimirlem31  38224  lcmineqlem1  42720  lcmineqlem2  42721  lcmineqlem12  42731  lcmineqlem17  42736  primrootscoprmpow  42790  aks6d1c2p2  42810  deg1gprod  42831  deg1pow  42832  2np3bcnp1  42835  2ap1caineq  42836  sticksstones7  42843  sticksstones9  42845  sticksstones10  42846  sticksstones11  42847  sticksstones12a  42848  sticksstones12  42849  sticksstones22  42859  aks6d1c6lem1  42861  aks6d1c6lem3  42863  bcled  42869  bcle2d  42870  aks6d1c7lem1  42871  unitscyglem2  42887  unitscyglem4  42889  ccatcan2d  42943  fz1sump1  42995  sumcubes  42998  zaddcomlem  43161  frlmvscadiccat  43204  fltnltalem  43320  3cubeslem3l  43343  3cubeslem3r  43344  rmxyneg  43573  rmxyadd  43574  rmyp1  43586  rmxm1  43587  rmym1  43588  rmxluc  43589  rmyluc  43590  rmxdbl  43592  rmydbl  43593  jm2.18  43641  jm2.19lem1  43642  jm2.19lem2  43643  jm2.22  43648  jm2.23  43649  jm2.25  43652  jm2.27c  43660  rmxdiophlem  43668  expdioph  43676  hbtlem4  43779  relexpmulg  44362  radcnvrat  44950  nzprmdif  44955  bcc0  44976  bccp1k  44977  bccbc  44981  binomcxplemnn0  44985  binomcxplemrat  44986  binomcxplemfrat  44987  binomcxplemnotnn0  44992  fzisoeu  45945  mccllem  46239  dvxpaek  46580  dvnxpaek  46582  dvnmul  46583  dvnprodlem1  46586  dvnprodlem2  46587  stoweidlem24  46664  stirlinglem3  46716  stirlinglem7  46720  fourierdlem36  46783  fourierdlem47  46793  etransclem23  46897  etransclem32  46906  etransclem48  46922  fz0addcom  47977  fmtnom1nn  48207  fmtnof1  48210  fmtnorec1  48212  sqrtpwpw2p  48213  fmtnorec2lem  48217  fmtnorec3  48223  fmtnofac2lem  48243  fmtnofac2  48244  fmtnofac1  48245  lighneallem3  48282  lighneallem4b  48284  altgsumbc  49051  altgsumbcALT  49052  nnpw2pmod  49282  dignn0ehalf  49316  nn0sumshdiglemA  49318  nn0sumshdiglemB  49319  nn0sumshdiglem2  49321  nn0mullong  49324  itcovalpclem2  49370  itcovalt2lem2lem2  49373  itcovalt2lem1  49374  aacllem  50509