Theorem nn0cnd 12492

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℂcc 11028  ℕ₀cn0 12429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5219  ax-nul 5229  ax-pr 5363  ax-un 7679  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-i2m1 11098  ax-1ne0 11099  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4263  df-if 4456  df-pw 4532  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-iun 4924  df-br 5074  df-opab 5136  df-mpt 5155  df-tr 5181  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7360  df-om 7808  df-2nd 7933  df-frecs 8222  df-wrecs 8253  df-recs 8302  df-rdg 8340  df-nn 12167  df-n0 12430

This theorem is referenced by:  quoremnn0ALT  13808  expaddzlem  14059  expaddz  14060  expmulz  14062  facdiv  14241  faclbnd4lem3  14249  bcp1n  14270  bcn2m1  14278  bcn2p1  14279  hashgadd  14331  hashdom  14333  hashun3  14338  hashssdif  14366  hashdifpr  14369  hashxplem  14387  hashmap  14389  hashreshashfun  14393  hashbclem  14406  hashf1lem2  14410  hashf1  14411  ccatval3  14533  ccatval21sw  14540  ccatlid  14541  ccatrid  14542  ccatass  14543  ccatrn  14544  lswccatn0lsw  14546  ccatalpha  14548  ccatws1lenp1b  14576  wrdlenccats1lenm1  14577  ccats1val2  14582  swrdccat2  14624  pfxfv  14637  addlenpfx  14645  pfxtrcfvl  14651  pfxpfx  14662  lenrevpfxcctswrd  14666  ccats1pfxeq  14668  ccatopth2  14671  cats1un  14675  swrdccat3b  14694  spllen  14708  splfv2a  14710  revccat  14720  cshwlen  14753  cshwidxmod  14757  repswcshw  14766  2cshwid  14768  cshweqdif2  14773  relexpaddg  15007  rtrclreclem3  15014  isercoll2  15623  iseraltlem3  15638  fsumconst1  15745  hash2iun1dif1  15779  binomlem  15786  bcxmas  15792  incexclem  15793  incexc  15794  incexc2  15795  climcndslem1  15806  climcndslem2  15807  arisum  15817  arisum2  15818  pwdif  15825  geomulcvg  15833  mertens  15843  risefacval2  15967  fallfacval2  15968  fallfacval3  15969  risefallfac  15981  risefacp1  15986  fallfacp1  15987  fallfacfwd  15993  binomfallfaclem1  15996  binomfallfaclem2  15997  binomrisefac  15999  bpolycl  16009  bpolysum  16010  bpolydiflem  16011  fsumkthpow  16013  bpoly4  16016  effsumlt  16070  dvdsexp  16289  nn0ob  16345  divalgmod  16367  bitsinv1lem  16402  sadcp1  16416  sadcaddlem  16418  sadadd2lem  16420  sadadd3  16422  sadaddlem  16427  sadasslem  16431  smupp1  16441  smumullem  16453  mulgcd  16509  absmulgcd  16510  mulgcdr  16511  gcddiv  16512  lcmgcd  16568  lcmid  16570  lcm1  16571  3lcm2e6woprm  16576  6lcm4e12  16577  mulgcddvds  16616  qredeu  16619  divgcdcoprm0  16626  divgcdcoprmex  16627  cncongr1  16628  cncongr2  16629  odzdvds  16758  powm2modprm  16766  coprimeprodsq  16771  pceulem  16808  pczpre  16810  pcqmul  16816  pcaddlem  16851  pcmpt  16855  pcmpt2  16856  sumhash  16859  oddprmdvds  16866  mul4sq  16917  4sqlem12  16919  vdwapun  16937  vdwlem2  16945  vdwlem3  16946  vdwlem6  16949  vdwlem8  16951  vdwlem9  16952  ramub1lem2  16990  ramcl  16992  chnrev  18585  mulgnn0dir  19072  mulgnn0ass  19078  lagsubg2  19161  psgnunilem2  19462  odmodnn0  19507  odmulg  19523  odmulgeq  19524  odinv  19528  sylow1lem1  19565  sylow2a  19586  sylow2blem3  19589  sylow3lem3  19596  sylow3lem4  19597  efginvrel2  19694  efgsval2  19700  efgsp1  19704  efgredlemg  19709  efgredleme  19710  efgcpbllemb  19722  odadd2  19816  odadd  19817  torsubg  19821  frgpnabllem1  19840  pgpfaclem1  20050  fincygsubgodd  20081  omndmul2  20100  omndmul3  20101  srgbinomlem3  20201  srgbinomlem4  20202  nn0srg  21413  freshmansdream  21550  mplcoe5  22017  mhpmulcl  22138  mhppwdeg  22139  psdmplcl  22151  psdmul  22155  coe1tmmul2  22263  coe1tmmul2fv  22265  coe1pwmulfv  22267  mbfi1fseqlem3  25703  dvn2bss  25916  itgpowd  26036  tdeglem4  26044  tdeglem2  26045  mdegmullem  26062  coe1mul3  26083  ply1divex  26121  fta1glem1  26152  plyaddlem1  26197  plymullem1  26198  coeeulem  26208  coemulc  26239  dgrmulc  26255  dgrcolem2  26258  dgrco  26259  dvply1  26269  dvply2g  26270  plydivlem4  26281  fta1lem  26292  vieta1lem1  26295  aareccl  26311  aaliou3lem8  26330  taylply2  26352  dvtaylp  26354  dvntaylp  26355  dvntaylp0  26356  dvradcnv  26405  pserdvlem2  26412  advlogexp  26638  cxpeq  26740  atantayl3  26922  birthdaylem2  26935  harmonicbnd4  26993  dmgmaddnn0  27009  lgamucov  27020  wilthlem2  27051  basellem2  27064  basellem3  27065  basellem5  27067  0sgm  27126  sgmppw  27179  chtublem  27193  chpval2  27200  sumdchr2  27252  bcp1ctr  27261  lgslem1  27279  gausslemma2dlem6  27354  gausslemma2d  27356  lgseisenlem2  27358  lgseisenlem3  27359  lgsquadlem1  27362  lgsquadlem2  27363  lgsquad2lem2  27367  m1lgs  27370  2lgslem1c  27375  2lgslem3a  27378  2lgslem3b  27379  2lgslem3c  27380  2lgslem3d  27381  2sqlem8  27408  2sq2  27415  2sqmod  27418  dchrisumlem1  27471  dchrisum0flblem2  27491  rpvmasum2  27494  mulogsumlem  27513  selberg2lem  27532  pntrsumo1  27547  pntrlog2bndlem4  27562  finsumvtxdg2ssteplem4  29636  vtxdgoddnumeven  29641  wlklenvm1  29709  wlklenvclwlk  29741  crctcshlem4  29907  crctcsh  29911  wlklnwwlkln2lem  29969  wlknwwlksnbij  29975  wwlksnred  29979  wwlksnext  29980  wwlksnextbi  29981  wwlksnredwwlkn  29982  wwlksnextproplem2  29997  rusgrnumwwlks  30064  rusgrnumwwlk  30065  clwwlkccatlem  30078  clwlkclwwlk  30091  clwwlkwwlksb  30143  eupth2lem3lem3  30319  eupth2lem3lem6  30322  fusgreghash2wsp  30427  frrusgrord0lem  30428  numclwwlk1  30450  numclwwlk3  30474  ex-lcm  30547  ex-ind-dvds  30550  nnmulge  32832  elq2  32905  divnumden2  32909  ccatf1  33029  pfxlsw2ccat  33030  ccatws1f1o  33031  wrdt2ind  33033  gsummptrev  33138  gsummptp1  33139  gsummulsubdishift1  33150  cycpmco2lem2  33209  cycpmco2lem3  33210  cycpmco2lem4  33211  cycpmco2lem5  33212  cycpmco2lem6  33213  cycpmco2lem7  33214  cycpmco2  33215  archiabllem1a  33273  gsumind  33429  deg1prod  33675  ply1dg3rt0irred  33676  esplyind  33768  esplyindfv  33769  esplyfvn  33770  vietadeg1  33771  vietalem  33772  vieta  33773  iconstr  33959  cos9thpiminplylem1  33975  oddpwdc  34547  eulerpartlemsv2  34551  eulerpartlems  34553  eulerpartlemsv3  34554  eulerpartlemv  34557  eulerpartlemb  34561  iwrdsplit  34580  ballotlemgun  34718  ccatmulgnn0dir  34735  ofcccat  34736  signsplypnf  34743  signslema  34755  signstfvn  34762  signstfveq0  34770  signsvtp  34776  signsvtn  34777  signlem0  34780  signshf  34781  fsum2dsub  34800  hashreprin  34813  breprexp  34826  circlemeth  34833  lpadlem2  34873  lpadlen2  34874  revpfxsfxrev  35353  revwlk  35362  subfacp1lem6  35422  subfacval2  35424  subfaclim  35425  cvmliftlem7  35528  elmrsubrn  35757  bcprod  35975  bccolsum  35976  faclimlem1  35980  faclim2  35985  fwddifnp1  36402  knoppndvlem6  36832  knoppndvlem14  36840  poimirlem4  38000  poimirlem5  38001  poimirlem6  38002  poimirlem7  38003  poimirlem10  38006  poimirlem11  38007  poimirlem12  38008  poimirlem16  38012  poimirlem17  38013  poimirlem19  38015  poimirlem20  38016  poimirlem22  38018  poimirlem24  38020  poimirlem25  38021  poimirlem29  38025  poimirlem31  38027  lcmineqlem1  42523  lcmineqlem2  42524  lcmineqlem12  42534  lcmineqlem17  42539  primrootscoprmpow  42593  aks6d1c2p2  42613  deg1gprod  42634  deg1pow  42635  2np3bcnp1  42638  2ap1caineq  42639  sticksstones7  42646  sticksstones9  42648  sticksstones10  42649  sticksstones11  42650  sticksstones12a  42651  sticksstones12  42652  sticksstones22  42662  aks6d1c6lem1  42664  aks6d1c6lem3  42666  bcled  42672  bcle2d  42673  aks6d1c7lem1  42674  unitscyglem2  42690  unitscyglem4  42692  ccatcan2d  42744  fz1sump1  42796  sumcubes  42799  zaddcomlem  42962  frlmvscadiccat  43005  fltnltalem  43121  3cubeslem3l  43144  3cubeslem3r  43145  rmxyneg  43374  rmxyadd  43375  rmyp1  43387  rmxm1  43388  rmym1  43389  rmxluc  43390  rmyluc  43391  rmxdbl  43393  rmydbl  43394  jm2.18  43442  jm2.19lem1  43443  jm2.19lem2  43444  jm2.22  43449  jm2.23  43450  jm2.25  43453  jm2.27c  43461  rmxdiophlem  43469  expdioph  43477  hbtlem4  43580  relexpmulg  44163  radcnvrat  44767  nzprmdif  44772  bcc0  44793  bccp1k  44794  bccbc  44798  binomcxplemnn0  44802  binomcxplemrat  44803  binomcxplemfrat  44804  binomcxplemnotnn0  44809  fzisoeu  45756  mccllem  46050  dvxpaek  46391  dvnxpaek  46393  dvnmul  46394  dvnprodlem1  46397  dvnprodlem2  46398  stoweidlem24  46475  stirlinglem3  46527  stirlinglem7  46531  fourierdlem36  46594  fourierdlem47  46604  etransclem23  46708  etransclem32  46717  etransclem48  46733  fz0addcom  47788  fmtnom1nn  48018  fmtnof1  48021  fmtnorec1  48023  sqrtpwpw2p  48024  fmtnorec2lem  48028  fmtnorec3  48034  fmtnofac2lem  48054  fmtnofac2  48055  fmtnofac1  48056  lighneallem3  48093  lighneallem4b  48095  altgsumbc  48851  altgsumbcALT  48852  nnpw2pmod  49082  dignn0ehalf  49116  nn0sumshdiglemA  49118  nn0sumshdiglemB  49119  nn0sumshdiglem2  49121  nn0mullong  49124  itcovalpclem2  49170  itcovalt2lem2lem2  49173  itcovalt2lem1  49174  aacllem  50299