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 11286	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2105  ℂcc 11150  ℕ₀cn0 12523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-i2m1 11220  ax-1ne0 11221  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-nn 12264  df-n0 12524

This theorem is referenced by:  quoremnn0ALT  13893  expaddzlem  14142  expaddz  14143  expmulz  14145  facdiv  14322  faclbnd4lem3  14330  bcp1n  14351  bcn2m1  14359  bcn2p1  14360  hashgadd  14412  hashdom  14414  hashun3  14419  hashssdif  14447  hashdifpr  14450  hashxplem  14468  hashmap  14470  hashreshashfun  14474  hashbclem  14487  hashf1lem2  14491  hashf1  14492  ccatval3  14613  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  14725  pfxtrcfvl  14731  pfxpfx  14742  ccats1pfxeq  14748  ccatopth2  14751  cats1un  14755  swrdccat3b  14774  spllen  14788  splfv2a  14790  revccat  14800  cshwlen  14833  cshwidxmod  14837  repswcshw  14846  2cshwid  14848  cshweqdif2  14853  relexpaddg  15088  rtrclreclem3  15095  isercoll2  15701  iseraltlem3  15716  hash2iun1dif1  15856  binomlem  15861  bcxmas  15867  incexclem  15868  incexc  15869  incexc2  15870  climcndslem1  15881  climcndslem2  15882  arisum  15892  arisum2  15893  pwdif  15900  geomulcvg  15908  mertens  15918  risefacval2  16042  fallfacval2  16043  fallfacval3  16044  risefallfac  16056  risefacp1  16061  fallfacp1  16062  fallfacfwd  16068  binomfallfaclem1  16071  binomfallfaclem2  16072  binomrisefac  16074  bpolycl  16084  bpolysum  16085  bpolydiflem  16086  fsumkthpow  16088  bpoly4  16091  effsumlt  16143  dvdsexp  16361  nn0ob  16417  divalgmod  16439  bitsinv1lem  16474  sadcp1  16488  sadcaddlem  16490  sadadd2lem  16492  sadadd3  16494  sadaddlem  16499  sadasslem  16503  smupp1  16513  smumullem  16525  mulgcd  16581  absmulgcd  16582  mulgcdr  16583  gcddiv  16584  lcmgcd  16640  lcmid  16642  lcm1  16643  3lcm2e6woprm  16648  6lcm4e12  16649  mulgcddvds  16688  qredeu  16691  divgcdcoprm0  16698  divgcdcoprmex  16699  cncongr1  16700  cncongr2  16701  odzdvds  16828  powm2modprm  16836  coprimeprodsq  16841  pceulem  16878  pczpre  16880  pcqmul  16886  pcaddlem  16921  pcmpt  16925  pcmpt2  16926  sumhash  16929  oddprmdvds  16936  mul4sq  16987  4sqlem12  16989  vdwapun  17007  vdwlem2  17015  vdwlem3  17016  vdwlem6  17019  vdwlem8  17021  vdwlem9  17022  ramub1lem2  17060  ramcl  17062  mulgnn0dir  19134  mulgnn0ass  19140  lagsubg2  19224  psgnunilem2  19527  odmodnn0  19572  odmulg  19588  odmulgeq  19589  odinv  19593  sylow1lem1  19630  sylow2a  19651  sylow2blem3  19654  sylow3lem3  19661  sylow3lem4  19662  efginvrel2  19759  efgsval2  19765  efgsp1  19769  efgredlemg  19774  efgredleme  19775  efgcpbllemb  19787  odadd2  19881  odadd  19882  torsubg  19886  frgpnabllem1  19905  pgpfaclem1  20115  fincygsubgodd  20146  srgbinomlem3  20245  srgbinomlem4  20246  nn0srg  21472  freshmansdream  21610  mplcoe5  22075  mhpmulcl  22170  mhppwdeg  22171  psdmplcl  22183  psdmul  22187  coe1tmmul2  22294  coe1tmmul2fv  22296  coe1pwmulfv  22298  mbfi1fseqlem3  25766  dvn2bss  25980  itgpowd  26105  tdeglem4  26113  tdeglem2  26114  mdegmullem  26131  coe1mul3  26152  ply1divex  26190  fta1glem1  26221  plyaddlem1  26266  plymullem1  26267  coeeulem  26277  coemulc  26308  dgrmulc  26325  dgrcolem2  26328  dgrco  26329  dvply1  26339  dvply2g  26340  dvply2gOLD  26341  plydivlem4  26352  fta1lem  26363  vieta1lem1  26366  aareccl  26382  aaliou3lem8  26401  taylply2  26423  taylply2OLD  26424  dvtaylp  26426  dvntaylp  26427  dvntaylp0  26428  dvradcnv  26478  pserdvlem2  26486  advlogexp  26711  cxpeq  26814  atantayl3  26996  birthdaylem2  27009  harmonicbnd4  27068  dmgmaddnn0  27084  lgamucov  27095  wilthlem2  27126  basellem2  27139  basellem3  27140  basellem5  27142  0sgm  27201  sgmppw  27255  chtublem  27269  chpval2  27276  sumdchr2  27328  bcp1ctr  27337  lgslem1  27355  gausslemma2dlem6  27430  gausslemma2d  27432  lgseisenlem2  27434  lgseisenlem3  27435  lgsquadlem1  27438  lgsquadlem2  27439  lgsquad2lem2  27443  m1lgs  27446  2lgslem1c  27451  2lgslem3a  27454  2lgslem3b  27455  2lgslem3c  27456  2lgslem3d  27457  2sqlem8  27484  2sq2  27491  2sqmod  27494  dchrisumlem1  27547  dchrisum0flblem2  27567  rpvmasum2  27570  mulogsumlem  27589  selberg2lem  27608  pntrsumo1  27623  pntrlog2bndlem4  27638  finsumvtxdg2ssteplem4  29580  vtxdgoddnumeven  29585  wlklenvm1  29654  wlklenvclwlk  29687  crctcshlem4  29849  crctcsh  29853  wlklnwwlkln2lem  29911  wlknwwlksnbij  29917  wwlksnred  29921  wwlksnext  29922  wwlksnextbi  29923  wwlksnredwwlkn  29924  wwlksnextproplem2  29939  rusgrnumwwlks  30003  rusgrnumwwlk  30004  clwwlkccatlem  30017  clwlkclwwlk  30030  clwwlkwwlksb  30082  eupth2lem3lem3  30258  eupth2lem3lem6  30261  fusgreghash2wsp  30366  frrusgrord0lem  30367  numclwwlk1  30389  numclwwlk3  30413  ex-lcm  30486  ex-ind-dvds  30489  nnmulge  32755  divnumden2  32821  ccatf1  32917  pfxlsw2ccat  32919  ccatws1f1o  32920  wrdt2ind  32922  omndmul2  33071  omndmul3  33072  cycpmco2lem2  33129  cycpmco2lem3  33130  cycpmco2lem4  33131  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2lem7  33134  cycpmco2  33135  archiabllem1a  33180  ply1dg3rt0irred  33586  oddpwdc  34335  eulerpartlemsv2  34339  eulerpartlems  34341  eulerpartlemsv3  34342  eulerpartlemv  34345  eulerpartlemb  34349  iwrdsplit  34368  ballotlemgun  34505  ccatmulgnn0dir  34535  ofcccat  34536  signsplypnf  34543  signslema  34555  signstfvn  34562  signstfveq0  34570  signsvtp  34576  signsvtn  34577  signlem0  34580  signshf  34581  fsum2dsub  34600  hashreprin  34613  breprexp  34626  circlemeth  34633  lpadlem2  34673  lpadlen2  34674  revpfxsfxrev  35099  revwlk  35108  subfacp1lem6  35169  subfacval2  35171  subfaclim  35172  cvmliftlem7  35275  elmrsubrn  35504  bcprod  35717  bccolsum  35718  faclimlem1  35722  faclim2  35727  fwddifnp1  36146  knoppndvlem6  36499  knoppndvlem14  36507  poimirlem4  37610  poimirlem5  37611  poimirlem6  37612  poimirlem7  37613  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem22  37628  poimirlem24  37630  poimirlem25  37631  poimirlem29  37635  poimirlem31  37637  lcmineqlem1  42010  lcmineqlem2  42011  lcmineqlem12  42021  lcmineqlem17  42026  primrootscoprmpow  42080  aks6d1c2p2  42100  deg1gprod  42121  deg1pow  42122  2np3bcnp1  42125  2ap1caineq  42126  sticksstones7  42133  sticksstones9  42135  sticksstones10  42136  sticksstones11  42137  sticksstones12a  42138  sticksstones12  42139  sticksstones22  42149  aks6d1c6lem1  42151  aks6d1c6lem3  42153  bcled  42159  bcle2d  42160  aks6d1c7lem1  42161  unitscyglem2  42177  unitscyglem4  42179  ccatcan2d  42270  fz1sump1  42322  sumcubes  42325  zaddcomlem  42457  frlmvscadiccat  42492  fltnltalem  42648  3cubeslem3l  42673  3cubeslem3r  42674  rmxyneg  42908  rmxyadd  42909  rmyp1  42921  rmxm1  42922  rmym1  42923  rmxluc  42924  rmyluc  42925  rmxdbl  42927  rmydbl  42928  jm2.18  42976  jm2.19lem1  42977  jm2.19lem2  42978  jm2.22  42983  jm2.23  42984  jm2.25  42987  jm2.27c  42995  rmxdiophlem  43003  expdioph  43011  hbtlem4  43114  relexpmulg  43699  radcnvrat  44309  nzprmdif  44314  bcc0  44335  bccp1k  44336  bccbc  44340  binomcxplemnn0  44344  binomcxplemrat  44345  binomcxplemfrat  44346  binomcxplemnotnn0  44351  fzisoeu  45250  mccllem  45552  dvxpaek  45895  dvnxpaek  45897  dvnmul  45898  dvnprodlem1  45901  dvnprodlem2  45902  stoweidlem24  45979  stirlinglem3  46031  stirlinglem7  46035  fourierdlem36  46098  fourierdlem47  46108  etransclem23  46212  etransclem32  46221  etransclem48  46237  fz0addcom  47266  fmtnom1nn  47456  fmtnof1  47459  fmtnorec1  47461  sqrtpwpw2p  47462  fmtnorec2lem  47466  fmtnorec3  47472  fmtnofac2lem  47492  fmtnofac2  47493  fmtnofac1  47494  lighneallem3  47531  lighneallem4b  47533  altgsumbc  48196  altgsumbcALT  48197  nnpw2pmod  48432  dignn0ehalf  48466  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  nn0sumshdiglem2  48471  nn0mullong  48474  itcovalpclem2  48520  itcovalt2lem2lem2  48523  itcovalt2lem1  48524  aacllem  49031