Theorem nn0cnd 12562

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℂcc 11093  ℕ₀cn0 12499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-i2m1 11163  ax-1ne0 11164  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-nn 12229  df-n0 12500

This theorem is referenced by:  quoremnn0ALT  13886  expaddzlem  14137  expaddz  14138  expmulz  14140  facdiv  14319  faclbnd4lem3  14327  bcp1n  14348  bcn2m1  14356  bcn2p1  14357  hashgadd  14409  hashdom  14411  hashun3  14416  hashssdif  14445  hashdifpr  14448  hashxplem  14466  hashmap  14468  hashreshashfun  14472  hashbclem  14485  hashf1lem2  14489  hashf1  14490  ccatval3  14612  ccatval21sw  14619  ccatlid  14620  ccatrid  14621  ccatass  14622  ccatrn  14623  lswccatn0lsw  14625  ccatalpha  14627  ccatws1lenp1b  14655  wrdlenccats1lenm1  14656  ccats1val2  14661  swrdccat2  14703  pfxfv  14716  addlenpfx  14724  pfxtrcfvl  14730  pfxpfx  14741  lenrevpfxcctswrd  14745  ccats1pfxeq  14747  ccatopth2  14750  cats1un  14754  swrdccat3b  14773  spllen  14787  splfv2a  14789  revccat  14799  cshwlen  14832  cshwidxmod  14836  repswcshw  14845  2cshwid  14847  cshweqdif2  14852  relexpaddg  15086  rtrclreclem3  15093  isercoll2  15716  iseraltlem3  15731  fsumconst1  15838  hash2iun1dif1  15872  binomlem  15879  bcxmas  15885  incexclem  15886  incexc  15887  incexc2  15888  climcndslem1  15899  climcndslem2  15900  arisum  15910  arisum2  15911  pwdif  15918  geomulcvg  15926  mertens  15936  risefacval2  16060  fallfacval2  16061  fallfacval3  16062  risefallfac  16074  risefacp1  16078  fallfacp1  16079  fallfacfwd  16085  binomfallfaclem1  16088  binomfallfaclem2  16089  binomrisefac  16091  bpolycl  16101  bpolysum  16102  bpolydiflem  16103  fsumkthpow  16105  bpoly4  16108  effsumlt  16162  dvdsexp  16381  nn0ob  16437  divalgmod  16459  bitsinv1lem  16494  sadcp1  16508  sadcaddlem  16510  sadadd2lem  16512  sadadd3  16514  sadaddlem  16519  sadasslem  16523  smupp1  16533  smumullem  16545  mulgcd  16601  absmulgcd  16602  mulgcdr  16603  gcddiv  16604  lcmgcd  16660  lcmid  16662  lcm1  16663  3lcm2e6woprm  16668  6lcm4e12  16669  mulgcddvds  16708  qredeu  16711  divgcdcoprm0  16718  divgcdcoprmex  16719  cncongr1  16720  cncongr2  16721  odzdvds  16850  powm2modprm  16858  coprimeprodsq  16863  pceulem  16900  pczpre  16902  pcqmul  16908  pcaddlem  16943  pcmpt  16947  pcmpt2  16948  sumhash  16951  oddprmdvds  16958  mul4sq  17009  4sqlem12  17011  vdwapun  17029  vdwlem2  17037  vdwlem3  17038  vdwlem6  17041  vdwlem8  17043  vdwlem9  17044  ramub1lem2  17082  ramcl  17084  chnrev  18678  mulgnn0dir  19165  mulgnn0ass  19171  lagsubg2  19260  psgnunilem2  19560  odmodnn0  19605  odmulg  19621  odmulgeq  19622  odinv  19626  sylow1lem1  19663  sylow2a  19684  sylow2blem3  19687  sylow3lem3  19694  sylow3lem4  19695  efginvrel2  19792  efgsval2  19798  efgsp1  19802  efgredlemg  19807  efgredleme  19808  efgcpbllemb  19820  odadd2  19914  odadd  19915  torsubg  19919  frgpnabllem1  19938  pgpfaclem1  20148  fincygsubgodd  20179  omndmul2  20198  omndmul3  20199  srgbinomlem3  20305  srgbinomlem4  20306  nn0srg  21587  freshmansdream  21724  mplcoe5  22191  mhpmulcl  22312  mhppwdeg  22313  psdmplcl  22325  psdmul  22329  coe1tmmul2  22437  coe1tmmul2fv  22439  coe1pwmulfv  22441  mbfi1fseqlem3  25876  dvn2bss  26089  itgpowd  26209  tdeglem4  26217  tdeglem2  26218  mdegmullem  26235  coe1mul3  26256  ply1divex  26294  fta1glem1  26325  plyaddlem1  26370  plymullem1  26371  coeeulem  26381  coemulc  26412  dgrmulc  26428  dgrcolem2  26431  dgrco  26432  dvply1  26445  dvply2g  26446  plydivlem4  26457  fta1lem  26468  vieta1lem1  26471  aareccl  26489  aaliou3lem8  26508  taylply2  26531  dvtaylp  26533  dvntaylp  26534  dvntaylp0  26535  dvradcnv  26584  pserdvlem2  26591  advlogexp  26820  cxpeq  26922  atantayl3  27104  birthdaylem2  27117  harmonicbnd4  27175  dmgmaddnn0  27191  lgamucov  27202  wilthlem2  27233  basellem2  27246  basellem3  27247  basellem5  27249  0sgm  27308  sgmppw  27361  chtublem  27375  chpval2  27382  sumdchr2  27434  bcp1ctr  27443  lgslem1  27461  gausslemma2dlem6  27536  gausslemma2d  27538  lgseisenlem2  27540  lgseisenlem3  27541  lgsquadlem1  27544  lgsquadlem2  27545  lgsquad2lem2  27549  m1lgs  27552  2lgslem1c  27557  2lgslem3a  27560  2lgslem3b  27561  2lgslem3c  27562  2lgslem3d  27563  2sqlem8  27590  2sq2  27597  2sqmod  27600  dchrisumlem1  27653  dchrisum0flblem2  27673  rpvmasum2  27676  mulogsumlem  27695  selberg2lem  27714  pntrsumo1  27729  pntrlog2bndlem4  27744  finsumvtxdg2ssteplem4  29898  vtxdgoddnumeven  29903  wlklenvm1  29971  wlklenvclwlk  30003  crctcshlem4  30169  crctcsh  30173  wlklnwwlkln2lem  30231  wlknwwlksnbij  30237  wwlksnred  30241  wwlksnext  30242  wwlksnextbi  30243  wwlksnredwwlkn  30244  wwlksnextproplem2  30259  rusgrnumwwlks  30326  rusgrnumwwlk  30327  clwwlkccatlem  30340  clwlkclwwlk  30353  clwwlkwwlksb  30405  eupth2lem3lem3  30581  eupth2lem3lem6  30584  fusgreghash2wsp  30689  frrusgrord0lem  30690  numclwwlk1  30712  numclwwlk3  30736  ex-lcm  30809  ex-ind-dvds  30812  nnmulge  33084  elq2  33156  divnumden2  33160  ccatf1  33269  pfxlsw2ccat  33270  ccatws1f1o  33271  wrdt2ind  33273  gsummptrev  33376  gsummptp1  33377  gsummulsubdishift1  33388  cycpmco2lem2  33447  cycpmco2lem3  33448  cycpmco2lem4  33449  cycpmco2lem5  33450  cycpmco2lem6  33451  cycpmco2lem7  33452  cycpmco2  33453  archiabllem1a  33511  gsumind  33665  deg1prod  33873  ply1dg3rt0irred  33874  esplyind  33965  esplyindfv  33966  esplyfvn  33967  vietadeg1  33968  vietalem  33969  vieta  33970  iconstr  34156  cos9thpiminplylem1  34172  oddpwdc  34744  eulerpartlemsv2  34748  eulerpartlems  34750  eulerpartlemsv3  34751  eulerpartlemv  34754  eulerpartlemb  34758  iwrdsplit  34777  ballotlemgun  34915  ccatmulgnn0dir  34932  ofcccat  34933  signsplypnf  34937  signslema  34949  signstfvn  34956  signstfveq0  34964  signsvtp  34970  signsvtn  34971  signlem0  34974  signshf  34975  fsum2dsub  34994  hashreprin  35007  breprexp  35020  circlemeth  35027  lpadlem2  35070  lpadlen2  35071  revpfxsfxrev  35607  revwlk  35617  subfacp1lem6  35677  subfacval2  35679  subfaclim  35680  cvmliftlem7  35783  elmrsubrn  36012  bcprod  36230  bccolsum  36231  faclimlem1  36235  faclim2  36240  fwddifnp1  36657  knoppndvlem6  37126  knoppndvlem14  37134  poimirlem4  38295  poimirlem5  38296  poimirlem6  38297  poimirlem7  38298  poimirlem10  38301  poimirlem11  38302  poimirlem12  38303  poimirlem16  38307  poimirlem17  38308  poimirlem19  38310  poimirlem20  38311  poimirlem22  38313  poimirlem24  38315  poimirlem25  38316  poimirlem29  38320  poimirlem31  38322  lcmineqlem1  42816  lcmineqlem2  42817  lcmineqlem12  42827  lcmineqlem17  42832  primrootscoprmpow  42886  aks6d1c2p2  42906  deg1gprod  42927  deg1pow  42928  2np3bcnp1  42931  2ap1caineq  42932  sticksstones7  42939  sticksstones9  42941  sticksstones10  42942  sticksstones11  42943  sticksstones12a  42944  sticksstones12  42945  sticksstones22  42955  aks6d1c6lem1  42957  aks6d1c6lem3  42959  bcled  42965  bcle2d  42966  aks6d1c7lem1  42967  unitscyglem2  42983  unitscyglem4  42985  ccatcan2d  43039  fz1sump1  43091  sumcubes  43094  zaddcomlem  43257  frlmvscadiccat  43300  fltnltalem  43414  3cubeslem3l  43437  3cubeslem3r  43438  rmxyneg  43667  rmxyadd  43668  rmyp1  43680  rmxm1  43681  rmym1  43682  rmxluc  43683  rmyluc  43684  rmxdbl  43686  rmydbl  43687  jm2.18  43735  jm2.19lem1  43736  jm2.19lem2  43737  jm2.22  43742  jm2.23  43743  jm2.25  43746  jm2.27c  43754  rmxdiophlem  43762  expdioph  43770  hbtlem4  43873  relexpmulg  44456  radcnvrat  45044  nzprmdif  45049  bcc0  45070  bccp1k  45071  bccbc  45075  binomcxplemnn0  45079  binomcxplemrat  45080  binomcxplemfrat  45081  binomcxplemnotnn0  45086  fzisoeu  46039  mccllem  46333  dvxpaek  46674  dvnxpaek  46676  dvnmul  46677  dvnprodlem1  46680  dvnprodlem2  46681  stoweidlem24  46758  stirlinglem3  46810  stirlinglem7  46814  fourierdlem36  46877  fourierdlem47  46887  etransclem23  46991  etransclem32  47000  etransclem48  47016  fz0addcom  48074  fmtnom1nn  48304  fmtnof1  48307  fmtnorec1  48309  sqrtpwpw2p  48310  fmtnorec2lem  48314  fmtnorec3  48320  fmtnofac2lem  48340  fmtnofac2  48341  fmtnofac1  48342  lighneallem3  48379  lighneallem4b  48381  altgsumbc  49152  altgsumbcALT  49153  nnpw2pmod  49383  dignn0ehalf  49417  nn0sumshdiglemA  49419  nn0sumshdiglemB  49420  nn0sumshdiglem2  49422  nn0mullong  49425  itcovalpclem2  49471  itcovalt2lem2lem2  49474  itcovalt2lem1  49475  aacllem  50641