Theorem nn0cnd 12586

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

Syntax hints:   → wi 4   ∈ wcel 2099  ℂcc 11156  ℕ₀cn0 12524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433  ax-un 7746  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-i2m1 11226  ax-1ne0 11227  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-iun 5003  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-ov 7427  df-om 7877  df-2nd 8004  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-nn 12265  df-n0 12525

This theorem is referenced by:  quoremnn0ALT  13877  expaddzlem  14125  expaddz  14126  expmulz  14128  facdiv  14304  faclbnd4lem3  14312  bcp1n  14333  bcn2m1  14341  bcn2p1  14342  hashgadd  14394  hashdom  14396  hashun3  14401  hashssdif  14429  hashdifpr  14432  hashxplem  14450  hashmap  14452  hashreshashfun  14456  hashbclem  14469  hashf1lem2  14475  hashf1  14476  ccatval3  14587  ccatval21sw  14593  ccatlid  14594  ccatrid  14595  ccatass  14596  ccatrn  14597  lswccatn0lsw  14599  ccatalpha  14601  ccatws1lenp1b  14629  wrdlenccats1lenm1  14630  ccats1val2  14635  swrdccat2  14677  pfxfv  14690  addlenpfx  14699  pfxtrcfvl  14705  pfxpfx  14716  ccats1pfxeq  14722  ccatopth2  14725  cats1un  14729  swrdccat3b  14748  spllen  14762  splfv2a  14764  revccat  14774  cshwlen  14807  cshwidxmod  14811  repswcshw  14820  2cshwid  14822  cshweqdif2  14827  relexpaddg  15058  rtrclreclem3  15065  isercoll2  15673  iseraltlem3  15688  hash2iun1dif1  15828  binomlem  15833  bcxmas  15839  incexclem  15840  incexc  15841  incexc2  15842  climcndslem1  15853  climcndslem2  15854  arisum  15864  arisum2  15865  pwdif  15872  geomulcvg  15880  mertens  15890  risefacval2  16012  fallfacval2  16013  fallfacval3  16014  risefallfac  16026  risefacp1  16031  fallfacp1  16032  fallfacfwd  16038  binomfallfaclem1  16041  binomfallfaclem2  16042  binomrisefac  16044  bpolycl  16054  bpolysum  16055  bpolydiflem  16056  fsumkthpow  16058  bpoly4  16061  effsumlt  16113  dvdsexp  16330  nn0ob  16386  divalgmod  16408  bitsinv1lem  16441  sadcp1  16455  sadcaddlem  16457  sadadd2lem  16459  sadadd3  16461  sadaddlem  16466  sadasslem  16470  smupp1  16480  smumullem  16492  mulgcd  16549  absmulgcd  16550  mulgcdr  16551  gcddiv  16552  lcmgcd  16608  lcmid  16610  lcm1  16611  3lcm2e6woprm  16616  6lcm4e12  16617  mulgcddvds  16656  qredeu  16659  divgcdcoprm0  16666  divgcdcoprmex  16667  cncongr1  16668  cncongr2  16669  odzdvds  16797  powm2modprm  16805  coprimeprodsq  16810  pceulem  16847  pczpre  16849  pcqmul  16855  pcaddlem  16890  pcmpt  16894  pcmpt2  16895  sumhash  16898  oddprmdvds  16905  mul4sq  16956  4sqlem12  16958  vdwapun  16976  vdwlem2  16984  vdwlem3  16985  vdwlem6  16988  vdwlem8  16990  vdwlem9  16991  ramub1lem2  17029  ramcl  17031  mulgnn0dir  19098  mulgnn0ass  19104  lagsubg2  19188  psgnunilem2  19493  odmodnn0  19538  odmulg  19554  odmulgeq  19555  odinv  19559  sylow1lem1  19596  sylow2a  19617  sylow2blem3  19620  sylow3lem3  19627  sylow3lem4  19628  efginvrel2  19725  efgsval2  19731  efgsp1  19735  efgredlemg  19740  efgredleme  19741  efgcpbllemb  19753  odadd2  19847  odadd  19848  torsubg  19852  frgpnabllem1  19871  pgpfaclem1  20081  fincygsubgodd  20112  srgbinomlem3  20211  srgbinomlem4  20212  nn0srg  21434  freshmansdream  21572  mplcoe5  22047  mhpmulcl  22143  mhppwdeg  22144  psdmplcl  22156  psdmul  22160  coe1tmmul2  22267  coe1tmmul2fv  22269  coe1pwmulfv  22271  mbfi1fseqlem3  25738  dvn2bss  25951  itgpowd  26076  tdeglem4  26086  tdeglem4OLD  26087  tdeglem2  26088  mdegmullem  26105  coe1mul3  26126  ply1divex  26164  fta1glem1  26195  plyaddlem1  26240  plymullem1  26241  coeeulem  26251  coemulc  26282  dgrmulc  26299  dgrcolem2  26302  dgrco  26303  dvply1  26311  dvply2g  26312  dvply2gOLD  26313  plydivlem4  26324  fta1lem  26335  vieta1lem1  26338  aareccl  26354  aaliou3lem8  26373  taylply2  26395  taylply2OLD  26396  dvtaylp  26398  dvntaylp  26399  dvntaylp0  26400  dvradcnv  26450  pserdvlem2  26458  advlogexp  26682  cxpeq  26785  atantayl3  26967  birthdaylem2  26980  harmonicbnd4  27039  dmgmaddnn0  27055  lgamucov  27066  wilthlem2  27097  basellem2  27110  basellem3  27111  basellem5  27113  0sgm  27172  sgmppw  27226  chtublem  27240  chpval2  27247  sumdchr2  27299  bcp1ctr  27308  lgslem1  27326  gausslemma2dlem6  27401  gausslemma2d  27403  lgseisenlem2  27405  lgseisenlem3  27406  lgsquadlem1  27409  lgsquadlem2  27410  lgsquad2lem2  27414  m1lgs  27417  2lgslem1c  27422  2lgslem3a  27425  2lgslem3b  27426  2lgslem3c  27427  2lgslem3d  27428  2sqlem8  27455  2sq2  27462  2sqmod  27465  dchrisumlem1  27518  dchrisum0flblem2  27538  rpvmasum2  27541  mulogsumlem  27560  selberg2lem  27579  pntrsumo1  27594  pntrlog2bndlem4  27609  finsumvtxdg2ssteplem4  29485  vtxdgoddnumeven  29490  wlklenvm1  29559  wlklenvclwlk  29592  crctcshlem4  29754  crctcsh  29758  wlklnwwlkln2lem  29816  wlknwwlksnbij  29822  wwlksnred  29826  wwlksnext  29827  wwlksnextbi  29828  wwlksnredwwlkn  29829  wwlksnextproplem2  29844  rusgrnumwwlks  29908  rusgrnumwwlk  29909  clwwlkccatlem  29922  clwlkclwwlk  29935  clwwlkwwlksb  29987  eupth2lem3lem3  30163  eupth2lem3lem6  30166  fusgreghash2wsp  30271  frrusgrord0lem  30272  numclwwlk1  30294  numclwwlk3  30318  ex-lcm  30391  ex-ind-dvds  30394  nnmulge  32652  divnumden2  32716  ccatf1  32812  pfxlsw2ccat  32814  ccatws1f1o  32815  wrdt2ind  32817  omndmul2  32947  omndmul3  32948  cycpmco2lem2  33005  cycpmco2lem3  33006  cycpmco2lem4  33007  cycpmco2lem5  33008  cycpmco2lem6  33009  cycpmco2lem7  33010  cycpmco2  33011  archiabllem1a  33056  ply1dg3rt0irred  33454  oddpwdc  34188  eulerpartlemsv2  34192  eulerpartlems  34194  eulerpartlemsv3  34195  eulerpartlemv  34198  eulerpartlemb  34202  iwrdsplit  34221  ballotlemgun  34358  ccatmulgnn0dir  34388  ofcccat  34389  signsplypnf  34396  signslema  34408  signstfvn  34415  signstfveq0  34423  signsvtp  34429  signsvtn  34430  signlem0  34433  signshf  34434  fsum2dsub  34453  hashreprin  34466  breprexp  34479  circlemeth  34486  lpadlem2  34526  lpadlen2  34527  revpfxsfxrev  34943  revwlk  34952  subfacp1lem6  35013  subfacval2  35015  subfaclim  35016  cvmliftlem7  35119  elmrsubrn  35348  bcprod  35560  bccolsum  35561  faclimlem1  35565  faclim2  35570  fwddifnp1  35989  knoppndvlem6  36220  knoppndvlem14  36228  poimirlem4  37325  poimirlem5  37326  poimirlem6  37327  poimirlem7  37328  poimirlem10  37331  poimirlem11  37332  poimirlem12  37333  poimirlem16  37337  poimirlem17  37338  poimirlem19  37340  poimirlem20  37341  poimirlem22  37343  poimirlem24  37345  poimirlem25  37346  poimirlem29  37350  poimirlem31  37352  lcmineqlem1  41728  lcmineqlem2  41729  lcmineqlem12  41739  lcmineqlem17  41744  primrootscoprmpow  41797  aks6d1c2p2  41817  deg1gprod  41838  deg1pow  41839  2np3bcnp1  41842  2ap1caineq  41843  sticksstones7  41850  sticksstones9  41852  sticksstones10  41853  sticksstones11  41854  sticksstones12a  41855  sticksstones12  41856  sticksstones22  41866  aks6d1c6lem1  41868  aks6d1c6lem3  41870  bcled  41876  bcle2d  41877  aks6d1c7lem1  41878  ccatcan2d  41974  frlmvscadiccat  41985  fz1sump1  42109  sumcubes  42112  zaddcomlem  42231  fltnltalem  42316  3cubeslem3l  42343  3cubeslem3r  42344  rmxyneg  42578  rmxyadd  42579  rmyp1  42591  rmxm1  42592  rmym1  42593  rmxluc  42594  rmyluc  42595  rmxdbl  42597  rmydbl  42598  jm2.18  42646  jm2.19lem1  42647  jm2.19lem2  42648  jm2.22  42653  jm2.23  42654  jm2.25  42657  jm2.27c  42665  rmxdiophlem  42673  expdioph  42681  hbtlem4  42787  relexpmulg  43377  radcnvrat  43988  nzprmdif  43993  bcc0  44014  bccp1k  44015  bccbc  44019  binomcxplemnn0  44023  binomcxplemrat  44024  binomcxplemfrat  44025  binomcxplemnotnn0  44030  fzisoeu  44915  mccllem  45218  dvxpaek  45561  dvnxpaek  45563  dvnmul  45564  dvnprodlem1  45567  dvnprodlem2  45568  stoweidlem24  45645  stirlinglem3  45697  stirlinglem7  45701  fourierdlem36  45764  fourierdlem47  45774  etransclem23  45878  etransclem32  45887  etransclem48  45903  fz0addcom  46930  fmtnom1nn  47104  fmtnof1  47107  fmtnorec1  47109  sqrtpwpw2p  47110  fmtnorec2lem  47114  fmtnorec3  47120  fmtnofac2lem  47140  fmtnofac2  47141  fmtnofac1  47142  lighneallem3  47179  lighneallem4b  47181  altgsumbc  47731  altgsumbcALT  47732  nnpw2pmod  47971  dignn0ehalf  48005  nn0sumshdiglemA  48007  nn0sumshdiglemB  48008  nn0sumshdiglem2  48010  nn0mullong  48013  itcovalpclem2  48059  itcovalt2lem2lem2  48062  itcovalt2lem1  48063  aacllem  48549