Theorem nn0cnd 12464

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 12463	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 11160	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11024  ℕ₀cn0 12401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-i2m1 11094  ax-1ne0 11095  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-nn 12146  df-n0 12402

This theorem is referenced by:  quoremnn0ALT  13777  expaddzlem  14028  expaddz  14029  expmulz  14031  facdiv  14210  faclbnd4lem3  14218  bcp1n  14239  bcn2m1  14247  bcn2p1  14248  hashgadd  14300  hashdom  14302  hashun3  14307  hashssdif  14335  hashdifpr  14338  hashxplem  14356  hashmap  14358  hashreshashfun  14362  hashbclem  14375  hashf1lem2  14379  hashf1  14380  ccatval3  14502  ccatval21sw  14509  ccatlid  14510  ccatrid  14511  ccatass  14512  ccatrn  14513  lswccatn0lsw  14515  ccatalpha  14517  ccatws1lenp1b  14545  wrdlenccats1lenm1  14546  ccats1val2  14551  swrdccat2  14593  pfxfv  14606  addlenpfx  14614  pfxtrcfvl  14620  pfxpfx  14631  lenrevpfxcctswrd  14635  ccats1pfxeq  14637  ccatopth2  14640  cats1un  14644  swrdccat3b  14663  spllen  14677  splfv2a  14679  revccat  14689  cshwlen  14722  cshwidxmod  14726  repswcshw  14735  2cshwid  14737  cshweqdif2  14742  relexpaddg  14976  rtrclreclem3  14983  isercoll2  15592  iseraltlem3  15607  hash2iun1dif1  15747  binomlem  15752  bcxmas  15758  incexclem  15759  incexc  15760  incexc2  15761  climcndslem1  15772  climcndslem2  15773  arisum  15783  arisum2  15784  pwdif  15791  geomulcvg  15799  mertens  15809  risefacval2  15933  fallfacval2  15934  fallfacval3  15935  risefallfac  15947  risefacp1  15952  fallfacp1  15953  fallfacfwd  15959  binomfallfaclem1  15962  binomfallfaclem2  15963  binomrisefac  15965  bpolycl  15975  bpolysum  15976  bpolydiflem  15977  fsumkthpow  15979  bpoly4  15982  effsumlt  16036  dvdsexp  16255  nn0ob  16311  divalgmod  16333  bitsinv1lem  16368  sadcp1  16382  sadcaddlem  16384  sadadd2lem  16386  sadadd3  16388  sadaddlem  16393  sadasslem  16397  smupp1  16407  smumullem  16419  mulgcd  16475  absmulgcd  16476  mulgcdr  16477  gcddiv  16478  lcmgcd  16534  lcmid  16536  lcm1  16537  3lcm2e6woprm  16542  6lcm4e12  16543  mulgcddvds  16582  qredeu  16585  divgcdcoprm0  16592  divgcdcoprmex  16593  cncongr1  16594  cncongr2  16595  odzdvds  16723  powm2modprm  16731  coprimeprodsq  16736  pceulem  16773  pczpre  16775  pcqmul  16781  pcaddlem  16816  pcmpt  16820  pcmpt2  16821  sumhash  16824  oddprmdvds  16831  mul4sq  16882  4sqlem12  16884  vdwapun  16902  vdwlem2  16910  vdwlem3  16911  vdwlem6  16914  vdwlem8  16916  vdwlem9  16917  ramub1lem2  16955  ramcl  16957  chnrev  18550  mulgnn0dir  19034  mulgnn0ass  19040  lagsubg2  19123  psgnunilem2  19424  odmodnn0  19469  odmulg  19485  odmulgeq  19486  odinv  19490  sylow1lem1  19527  sylow2a  19548  sylow2blem3  19551  sylow3lem3  19558  sylow3lem4  19559  efginvrel2  19656  efgsval2  19662  efgsp1  19666  efgredlemg  19671  efgredleme  19672  efgcpbllemb  19684  odadd2  19778  odadd  19779  torsubg  19783  frgpnabllem1  19802  pgpfaclem1  20012  fincygsubgodd  20043  omndmul2  20062  omndmul3  20063  srgbinomlem3  20163  srgbinomlem4  20164  nn0srg  21392  freshmansdream  21529  mplcoe5  21995  mhpmulcl  22092  mhppwdeg  22093  psdmplcl  22105  psdmul  22109  coe1tmmul2  22218  coe1tmmul2fv  22220  coe1pwmulfv  22222  mbfi1fseqlem3  25674  dvn2bss  25888  itgpowd  26013  tdeglem4  26021  tdeglem2  26022  mdegmullem  26039  coe1mul3  26060  ply1divex  26098  fta1glem1  26129  plyaddlem1  26174  plymullem1  26175  coeeulem  26185  coemulc  26216  dgrmulc  26233  dgrcolem2  26236  dgrco  26237  dvply1  26247  dvply2g  26248  dvply2gOLD  26249  plydivlem4  26260  fta1lem  26271  vieta1lem1  26274  aareccl  26290  aaliou3lem8  26309  taylply2  26331  taylply2OLD  26332  dvtaylp  26334  dvntaylp  26335  dvntaylp0  26336  dvradcnv  26386  pserdvlem2  26394  advlogexp  26620  cxpeq  26723  atantayl3  26905  birthdaylem2  26918  harmonicbnd4  26977  dmgmaddnn0  26993  lgamucov  27004  wilthlem2  27035  basellem2  27048  basellem3  27049  basellem5  27051  0sgm  27110  sgmppw  27164  chtublem  27178  chpval2  27185  sumdchr2  27237  bcp1ctr  27246  lgslem1  27264  gausslemma2dlem6  27339  gausslemma2d  27341  lgseisenlem2  27343  lgseisenlem3  27344  lgsquadlem1  27347  lgsquadlem2  27348  lgsquad2lem2  27352  m1lgs  27355  2lgslem1c  27360  2lgslem3a  27363  2lgslem3b  27364  2lgslem3c  27365  2lgslem3d  27366  2sqlem8  27393  2sq2  27400  2sqmod  27403  dchrisumlem1  27456  dchrisum0flblem2  27476  rpvmasum2  27479  mulogsumlem  27498  selberg2lem  27517  pntrsumo1  27532  pntrlog2bndlem4  27547  finsumvtxdg2ssteplem4  29622  vtxdgoddnumeven  29627  wlklenvm1  29695  wlklenvclwlk  29727  crctcshlem4  29893  crctcsh  29897  wlklnwwlkln2lem  29955  wlknwwlksnbij  29961  wwlksnred  29965  wwlksnext  29966  wwlksnextbi  29967  wwlksnredwwlkn  29968  wwlksnextproplem2  29983  rusgrnumwwlks  30050  rusgrnumwwlk  30051  clwwlkccatlem  30064  clwlkclwwlk  30077  clwwlkwwlksb  30129  eupth2lem3lem3  30305  eupth2lem3lem6  30308  fusgreghash2wsp  30413  frrusgrord0lem  30414  numclwwlk1  30436  numclwwlk3  30460  ex-lcm  30533  ex-ind-dvds  30536  nnmulge  32818  elq2  32892  divnumden2  32896  ccatf1  33031  pfxlsw2ccat  33032  ccatws1f1o  33033  wrdt2ind  33035  gsummptrev  33139  gsummptp1  33140  gsummulsubdishift1  33151  cycpmco2lem2  33209  cycpmco2lem3  33210  cycpmco2lem4  33211  cycpmco2lem5  33212  cycpmco2lem6  33213  cycpmco2lem7  33214  cycpmco2  33215  archiabllem1a  33273  gsumind  33426  deg1prod  33664  ply1dg3rt0irred  33665  esplyind  33731  esplyindfv  33732  esplyfvn  33733  vietadeg1  33734  vietalem  33735  vieta  33736  iconstr  33923  cos9thpiminplylem1  33939  oddpwdc  34511  eulerpartlemsv2  34515  eulerpartlems  34517  eulerpartlemsv3  34518  eulerpartlemv  34521  eulerpartlemb  34525  iwrdsplit  34544  ballotlemgun  34682  ccatmulgnn0dir  34699  ofcccat  34700  signsplypnf  34707  signslema  34719  signstfvn  34726  signstfveq0  34734  signsvtp  34740  signsvtn  34741  signlem0  34744  signshf  34745  fsum2dsub  34764  hashreprin  34777  breprexp  34790  circlemeth  34797  lpadlem2  34837  lpadlen2  34838  revpfxsfxrev  35310  revwlk  35319  subfacp1lem6  35379  subfacval2  35381  subfaclim  35382  cvmliftlem7  35485  elmrsubrn  35714  bcprod  35932  bccolsum  35933  faclimlem1  35937  faclim2  35942  fwddifnp1  36359  knoppndvlem6  36717  knoppndvlem14  36725  poimirlem4  37825  poimirlem5  37826  poimirlem6  37827  poimirlem7  37828  poimirlem10  37831  poimirlem11  37832  poimirlem12  37833  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem22  37843  poimirlem24  37845  poimirlem25  37846  poimirlem29  37850  poimirlem31  37852  lcmineqlem1  42293  lcmineqlem2  42294  lcmineqlem12  42304  lcmineqlem17  42309  primrootscoprmpow  42363  aks6d1c2p2  42383  deg1gprod  42404  deg1pow  42405  2np3bcnp1  42408  2ap1caineq  42409  sticksstones7  42416  sticksstones9  42418  sticksstones10  42419  sticksstones11  42420  sticksstones12a  42421  sticksstones12  42422  sticksstones22  42432  aks6d1c6lem1  42434  aks6d1c6lem3  42436  bcled  42442  bcle2d  42443  aks6d1c7lem1  42444  unitscyglem2  42460  unitscyglem4  42462  ccatcan2d  42516  fz1sump1  42575  sumcubes  42578  zaddcomlem  42728  frlmvscadiccat  42771  fltnltalem  42915  3cubeslem3l  42938  3cubeslem3r  42939  rmxyneg  43172  rmxyadd  43173  rmyp1  43185  rmxm1  43186  rmym1  43187  rmxluc  43188  rmyluc  43189  rmxdbl  43191  rmydbl  43192  jm2.18  43240  jm2.19lem1  43241  jm2.19lem2  43242  jm2.22  43247  jm2.23  43248  jm2.25  43251  jm2.27c  43259  rmxdiophlem  43267  expdioph  43275  hbtlem4  43378  relexpmulg  43961  radcnvrat  44565  nzprmdif  44570  bcc0  44591  bccp1k  44592  bccbc  44596  binomcxplemnn0  44600  binomcxplemrat  44601  binomcxplemfrat  44602  binomcxplemnotnn0  44607  fzisoeu  45558  mccllem  45853  dvxpaek  46194  dvnxpaek  46196  dvnmul  46197  dvnprodlem1  46200  dvnprodlem2  46201  stoweidlem24  46278  stirlinglem3  46330  stirlinglem7  46334  fourierdlem36  46397  fourierdlem47  46407  etransclem23  46511  etransclem32  46520  etransclem48  46536  fz0addcom  47573  fmtnom1nn  47788  fmtnof1  47791  fmtnorec1  47793  sqrtpwpw2p  47794  fmtnorec2lem  47798  fmtnorec3  47804  fmtnofac2lem  47824  fmtnofac2  47825  fmtnofac1  47826  lighneallem3  47863  lighneallem4b  47865  altgsumbc  48608  altgsumbcALT  48609  nnpw2pmod  48839  dignn0ehalf  48873  nn0sumshdiglemA  48875  nn0sumshdiglemB  48876  nn0sumshdiglem2  48878  nn0mullong  48881  itcovalpclem2  48927  itcovalt2lem2lem2  48930  itcovalt2lem1  48931  aacllem  50056