Theorem nn0cnd 12505

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11066  ℕ₀cn0 12442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-nn 12187  df-n0 12443

This theorem is referenced by:  quoremnn0ALT  13819  expaddzlem  14070  expaddz  14071  expmulz  14073  facdiv  14252  faclbnd4lem3  14260  bcp1n  14281  bcn2m1  14289  bcn2p1  14290  hashgadd  14342  hashdom  14344  hashun3  14349  hashssdif  14377  hashdifpr  14380  hashxplem  14398  hashmap  14400  hashreshashfun  14404  hashbclem  14417  hashf1lem2  14421  hashf1  14422  ccatval3  14544  ccatval21sw  14550  ccatlid  14551  ccatrid  14552  ccatass  14553  ccatrn  14554  lswccatn0lsw  14556  ccatalpha  14558  ccatws1lenp1b  14586  wrdlenccats1lenm1  14587  ccats1val2  14592  swrdccat2  14634  pfxfv  14647  addlenpfx  14656  pfxtrcfvl  14662  pfxpfx  14673  ccats1pfxeq  14679  ccatopth2  14682  cats1un  14686  swrdccat3b  14705  spllen  14719  splfv2a  14721  revccat  14731  cshwlen  14764  cshwidxmod  14768  repswcshw  14777  2cshwid  14779  cshweqdif2  14784  relexpaddg  15019  rtrclreclem3  15026  isercoll2  15635  iseraltlem3  15650  hash2iun1dif1  15790  binomlem  15795  bcxmas  15801  incexclem  15802  incexc  15803  incexc2  15804  climcndslem1  15815  climcndslem2  15816  arisum  15826  arisum2  15827  pwdif  15834  geomulcvg  15842  mertens  15852  risefacval2  15976  fallfacval2  15977  fallfacval3  15978  risefallfac  15990  risefacp1  15995  fallfacp1  15996  fallfacfwd  16002  binomfallfaclem1  16005  binomfallfaclem2  16006  binomrisefac  16008  bpolycl  16018  bpolysum  16019  bpolydiflem  16020  fsumkthpow  16022  bpoly4  16025  effsumlt  16079  dvdsexp  16298  nn0ob  16354  divalgmod  16376  bitsinv1lem  16411  sadcp1  16425  sadcaddlem  16427  sadadd2lem  16429  sadadd3  16431  sadaddlem  16436  sadasslem  16440  smupp1  16450  smumullem  16462  mulgcd  16518  absmulgcd  16519  mulgcdr  16520  gcddiv  16521  lcmgcd  16577  lcmid  16579  lcm1  16580  3lcm2e6woprm  16585  6lcm4e12  16586  mulgcddvds  16625  qredeu  16628  divgcdcoprm0  16635  divgcdcoprmex  16636  cncongr1  16637  cncongr2  16638  odzdvds  16766  powm2modprm  16774  coprimeprodsq  16779  pceulem  16816  pczpre  16818  pcqmul  16824  pcaddlem  16859  pcmpt  16863  pcmpt2  16864  sumhash  16867  oddprmdvds  16874  mul4sq  16925  4sqlem12  16927  vdwapun  16945  vdwlem2  16953  vdwlem3  16954  vdwlem6  16957  vdwlem8  16959  vdwlem9  16960  ramub1lem2  16998  ramcl  17000  mulgnn0dir  19036  mulgnn0ass  19042  lagsubg2  19126  psgnunilem2  19425  odmodnn0  19470  odmulg  19486  odmulgeq  19487  odinv  19491  sylow1lem1  19528  sylow2a  19549  sylow2blem3  19552  sylow3lem3  19559  sylow3lem4  19560  efginvrel2  19657  efgsval2  19663  efgsp1  19667  efgredlemg  19672  efgredleme  19673  efgcpbllemb  19685  odadd2  19779  odadd  19780  torsubg  19784  frgpnabllem1  19803  pgpfaclem1  20013  fincygsubgodd  20044  srgbinomlem3  20137  srgbinomlem4  20138  nn0srg  21354  freshmansdream  21484  mplcoe5  21947  mhpmulcl  22036  mhppwdeg  22037  psdmplcl  22049  psdmul  22053  coe1tmmul2  22162  coe1tmmul2fv  22164  coe1pwmulfv  22166  mbfi1fseqlem3  25618  dvn2bss  25832  itgpowd  25957  tdeglem4  25965  tdeglem2  25966  mdegmullem  25983  coe1mul3  26004  ply1divex  26042  fta1glem1  26073  plyaddlem1  26118  plymullem1  26119  coeeulem  26129  coemulc  26160  dgrmulc  26177  dgrcolem2  26180  dgrco  26181  dvply1  26191  dvply2g  26192  dvply2gOLD  26193  plydivlem4  26204  fta1lem  26215  vieta1lem1  26218  aareccl  26234  aaliou3lem8  26253  taylply2  26275  taylply2OLD  26276  dvtaylp  26278  dvntaylp  26279  dvntaylp0  26280  dvradcnv  26330  pserdvlem2  26338  advlogexp  26564  cxpeq  26667  atantayl3  26849  birthdaylem2  26862  harmonicbnd4  26921  dmgmaddnn0  26937  lgamucov  26948  wilthlem2  26979  basellem2  26992  basellem3  26993  basellem5  26995  0sgm  27054  sgmppw  27108  chtublem  27122  chpval2  27129  sumdchr2  27181  bcp1ctr  27190  lgslem1  27208  gausslemma2dlem6  27283  gausslemma2d  27285  lgseisenlem2  27287  lgseisenlem3  27288  lgsquadlem1  27291  lgsquadlem2  27292  lgsquad2lem2  27296  m1lgs  27299  2lgslem1c  27304  2lgslem3a  27307  2lgslem3b  27308  2lgslem3c  27309  2lgslem3d  27310  2sqlem8  27337  2sq2  27344  2sqmod  27347  dchrisumlem1  27400  dchrisum0flblem2  27420  rpvmasum2  27423  mulogsumlem  27442  selberg2lem  27461  pntrsumo1  27476  pntrlog2bndlem4  27491  finsumvtxdg2ssteplem4  29476  vtxdgoddnumeven  29481  wlklenvm1  29550  wlklenvclwlk  29583  crctcshlem4  29750  crctcsh  29754  wlklnwwlkln2lem  29812  wlknwwlksnbij  29818  wwlksnred  29822  wwlksnext  29823  wwlksnextbi  29824  wwlksnredwwlkn  29825  wwlksnextproplem2  29840  rusgrnumwwlks  29904  rusgrnumwwlk  29905  clwwlkccatlem  29918  clwlkclwwlk  29931  clwwlkwwlksb  29983  eupth2lem3lem3  30159  eupth2lem3lem6  30162  fusgreghash2wsp  30267  frrusgrord0lem  30268  numclwwlk1  30290  numclwwlk3  30314  ex-lcm  30387  ex-ind-dvds  30390  nnmulge  32662  elq2  32736  divnumden2  32740  ccatf1  32870  pfxlsw2ccat  32872  ccatws1f1o  32873  wrdt2ind  32875  omndmul2  33026  omndmul3  33027  cycpmco2lem2  33084  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmco2  33090  archiabllem1a  33145  ply1dg3rt0irred  33551  iconstr  33756  cos9thpiminplylem1  33772  oddpwdc  34345  eulerpartlemsv2  34349  eulerpartlems  34351  eulerpartlemsv3  34352  eulerpartlemv  34355  eulerpartlemb  34359  iwrdsplit  34378  ballotlemgun  34516  ccatmulgnn0dir  34533  ofcccat  34534  signsplypnf  34541  signslema  34553  signstfvn  34560  signstfveq0  34568  signsvtp  34574  signsvtn  34575  signlem0  34578  signshf  34579  fsum2dsub  34598  hashreprin  34611  breprexp  34624  circlemeth  34631  lpadlem2  34671  lpadlen2  34672  revpfxsfxrev  35103  revwlk  35112  subfacp1lem6  35172  subfacval2  35174  subfaclim  35175  cvmliftlem7  35278  elmrsubrn  35507  bcprod  35725  bccolsum  35726  faclimlem1  35730  faclim2  35735  fwddifnp1  36153  knoppndvlem6  36505  knoppndvlem14  36513  poimirlem4  37618  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem22  37636  poimirlem24  37638  poimirlem25  37639  poimirlem29  37643  poimirlem31  37645  lcmineqlem1  42017  lcmineqlem2  42018  lcmineqlem12  42028  lcmineqlem17  42033  primrootscoprmpow  42087  aks6d1c2p2  42107  deg1gprod  42128  deg1pow  42129  2np3bcnp1  42132  2ap1caineq  42133  sticksstones7  42140  sticksstones9  42142  sticksstones10  42143  sticksstones11  42144  sticksstones12a  42145  sticksstones12  42146  sticksstones22  42156  aks6d1c6lem1  42158  aks6d1c6lem3  42160  bcled  42166  bcle2d  42167  aks6d1c7lem1  42168  unitscyglem2  42184  unitscyglem4  42186  ccatcan2d  42239  fz1sump1  42298  sumcubes  42301  zaddcomlem  42451  frlmvscadiccat  42494  fltnltalem  42650  3cubeslem3l  42674  3cubeslem3r  42675  rmxyneg  42909  rmxyadd  42910  rmyp1  42922  rmxm1  42923  rmym1  42924  rmxluc  42925  rmyluc  42926  rmxdbl  42928  rmydbl  42929  jm2.18  42977  jm2.19lem1  42978  jm2.19lem2  42979  jm2.22  42984  jm2.23  42985  jm2.25  42988  jm2.27c  42996  rmxdiophlem  43004  expdioph  43012  hbtlem4  43115  relexpmulg  43699  radcnvrat  44303  nzprmdif  44308  bcc0  44329  bccp1k  44330  bccbc  44334  binomcxplemnn0  44338  binomcxplemrat  44339  binomcxplemfrat  44340  binomcxplemnotnn0  44345  fzisoeu  45298  mccllem  45595  dvxpaek  45938  dvnxpaek  45940  dvnmul  45941  dvnprodlem1  45944  dvnprodlem2  45945  stoweidlem24  46022  stirlinglem3  46074  stirlinglem7  46078  fourierdlem36  46141  fourierdlem47  46151  etransclem23  46255  etransclem32  46264  etransclem48  46280  fz0addcom  47318  fmtnom1nn  47533  fmtnof1  47536  fmtnorec1  47538  sqrtpwpw2p  47539  fmtnorec2lem  47543  fmtnorec3  47549  fmtnofac2lem  47569  fmtnofac2  47570  fmtnofac1  47571  lighneallem3  47608  lighneallem4b  47610  altgsumbc  48340  altgsumbcALT  48341  nnpw2pmod  48572  dignn0ehalf  48606  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  nn0sumshdiglem2  48611  nn0mullong  48614  itcovalpclem2  48660  itcovalt2lem2lem2  48663  itcovalt2lem1  48664  aacllem  49790