Theorem nn0cnd 12500

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  ℕ₀cn0 12437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-nn 12175  df-n0 12438

This theorem is referenced by:  quoremnn0ALT  13816  expaddzlem  14067  expaddz  14068  expmulz  14070  facdiv  14249  faclbnd4lem3  14257  bcp1n  14278  bcn2m1  14286  bcn2p1  14287  hashgadd  14339  hashdom  14341  hashun3  14346  hashssdif  14374  hashdifpr  14377  hashxplem  14395  hashmap  14397  hashreshashfun  14401  hashbclem  14414  hashf1lem2  14418  hashf1  14419  ccatval3  14541  ccatval21sw  14548  ccatlid  14549  ccatrid  14550  ccatass  14551  ccatrn  14552  lswccatn0lsw  14554  ccatalpha  14556  ccatws1lenp1b  14584  wrdlenccats1lenm1  14585  ccats1val2  14590  swrdccat2  14632  pfxfv  14645  addlenpfx  14653  pfxtrcfvl  14659  pfxpfx  14670  lenrevpfxcctswrd  14674  ccats1pfxeq  14676  ccatopth2  14679  cats1un  14683  swrdccat3b  14702  spllen  14716  splfv2a  14718  revccat  14728  cshwlen  14761  cshwidxmod  14765  repswcshw  14774  2cshwid  14776  cshweqdif2  14781  relexpaddg  15015  rtrclreclem3  15022  isercoll2  15631  iseraltlem3  15646  fsumconst1  15753  hash2iun1dif1  15787  binomlem  15794  bcxmas  15800  incexclem  15801  incexc  15802  incexc2  15803  climcndslem1  15814  climcndslem2  15815  arisum  15825  arisum2  15826  pwdif  15833  geomulcvg  15841  mertens  15851  risefacval2  15975  fallfacval2  15976  fallfacval3  15977  risefallfac  15989  risefacp1  15994  fallfacp1  15995  fallfacfwd  16001  binomfallfaclem1  16004  binomfallfaclem2  16005  binomrisefac  16007  bpolycl  16017  bpolysum  16018  bpolydiflem  16019  fsumkthpow  16021  bpoly4  16024  effsumlt  16078  dvdsexp  16297  nn0ob  16353  divalgmod  16375  bitsinv1lem  16410  sadcp1  16424  sadcaddlem  16426  sadadd2lem  16428  sadadd3  16430  sadaddlem  16435  sadasslem  16439  smupp1  16449  smumullem  16461  mulgcd  16517  absmulgcd  16518  mulgcdr  16519  gcddiv  16520  lcmgcd  16576  lcmid  16578  lcm1  16579  3lcm2e6woprm  16584  6lcm4e12  16585  mulgcddvds  16624  qredeu  16627  divgcdcoprm0  16634  divgcdcoprmex  16635  cncongr1  16636  cncongr2  16637  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  chnrev  18593  mulgnn0dir  19080  mulgnn0ass  19086  lagsubg2  19169  psgnunilem2  19470  odmodnn0  19515  odmulg  19531  odmulgeq  19532  odinv  19536  sylow1lem1  19573  sylow2a  19594  sylow2blem3  19597  sylow3lem3  19604  sylow3lem4  19605  efginvrel2  19702  efgsval2  19708  efgsp1  19712  efgredlemg  19717  efgredleme  19718  efgcpbllemb  19730  odadd2  19824  odadd  19825  torsubg  19829  frgpnabllem1  19848  pgpfaclem1  20058  fincygsubgodd  20089  omndmul2  20108  omndmul3  20109  srgbinomlem3  20209  srgbinomlem4  20210  nn0srg  21417  freshmansdream  21554  mplcoe5  22018  mhpmulcl  22115  mhppwdeg  22116  psdmplcl  22128  psdmul  22132  coe1tmmul2  22241  coe1tmmul2fv  22243  coe1pwmulfv  22245  mbfi1fseqlem3  25684  dvn2bss  25897  itgpowd  26017  tdeglem4  26025  tdeglem2  26026  mdegmullem  26043  coe1mul3  26064  ply1divex  26102  fta1glem1  26133  plyaddlem1  26178  plymullem1  26179  coeeulem  26189  coemulc  26220  dgrmulc  26236  dgrcolem2  26239  dgrco  26240  dvply1  26250  dvply2g  26251  plydivlem4  26262  fta1lem  26273  vieta1lem1  26276  aareccl  26292  aaliou3lem8  26311  taylply2  26333  dvtaylp  26335  dvntaylp  26336  dvntaylp0  26337  dvradcnv  26386  pserdvlem2  26393  advlogexp  26619  cxpeq  26721  atantayl3  26903  birthdaylem2  26916  harmonicbnd4  26974  dmgmaddnn0  26990  lgamucov  27001  wilthlem2  27032  basellem2  27045  basellem3  27046  basellem5  27048  0sgm  27107  sgmppw  27160  chtublem  27174  chpval2  27181  sumdchr2  27233  bcp1ctr  27242  lgslem1  27260  gausslemma2dlem6  27335  gausslemma2d  27337  lgseisenlem2  27339  lgseisenlem3  27340  lgsquadlem1  27343  lgsquadlem2  27344  lgsquad2lem2  27348  m1lgs  27351  2lgslem1c  27356  2lgslem3a  27359  2lgslem3b  27360  2lgslem3c  27361  2lgslem3d  27362  2sqlem8  27389  2sq2  27396  2sqmod  27399  dchrisumlem1  27452  dchrisum0flblem2  27472  rpvmasum2  27475  mulogsumlem  27494  selberg2lem  27513  pntrsumo1  27528  pntrlog2bndlem4  27543  finsumvtxdg2ssteplem4  29617  vtxdgoddnumeven  29622  wlklenvm1  29690  wlklenvclwlk  29722  crctcshlem4  29888  crctcsh  29892  wlklnwwlkln2lem  29950  wlknwwlksnbij  29956  wwlksnred  29960  wwlksnext  29961  wwlksnextbi  29962  wwlksnredwwlkn  29963  wwlksnextproplem2  29978  rusgrnumwwlks  30045  rusgrnumwwlk  30046  clwwlkccatlem  30059  clwlkclwwlk  30072  clwwlkwwlksb  30124  eupth2lem3lem3  30300  eupth2lem3lem6  30303  fusgreghash2wsp  30408  frrusgrord0lem  30409  numclwwlk1  30431  numclwwlk3  30455  ex-lcm  30528  ex-ind-dvds  30531  nnmulge  32812  elq2  32885  divnumden2  32889  ccatf1  33009  pfxlsw2ccat  33010  ccatws1f1o  33011  wrdt2ind  33013  gsummptrev  33117  gsummptp1  33118  gsummulsubdishift1  33129  cycpmco2lem2  33188  cycpmco2lem3  33189  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2lem7  33193  cycpmco2  33194  archiabllem1a  33252  gsumind  33405  deg1prod  33643  ply1dg3rt0irred  33644  esplyind  33719  esplyindfv  33720  esplyfvn  33721  vietadeg1  33722  vietalem  33723  vieta  33724  iconstr  33910  cos9thpiminplylem1  33926  oddpwdc  34498  eulerpartlemsv2  34502  eulerpartlems  34504  eulerpartlemsv3  34505  eulerpartlemv  34508  eulerpartlemb  34512  iwrdsplit  34531  ballotlemgun  34669  ccatmulgnn0dir  34686  ofcccat  34687  signsplypnf  34694  signslema  34706  signstfvn  34713  signstfveq0  34721  signsvtp  34727  signsvtn  34728  signlem0  34731  signshf  34732  fsum2dsub  34751  hashreprin  34764  breprexp  34777  circlemeth  34784  lpadlem2  34824  lpadlen2  34825  revpfxsfxrev  35298  revwlk  35307  subfacp1lem6  35367  subfacval2  35369  subfaclim  35370  cvmliftlem7  35473  elmrsubrn  35702  bcprod  35920  bccolsum  35921  faclimlem1  35925  faclim2  35930  fwddifnp1  36347  knoppndvlem6  36777  knoppndvlem14  36785  poimirlem4  37945  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem22  37963  poimirlem24  37965  poimirlem25  37966  poimirlem29  37970  poimirlem31  37972  lcmineqlem1  42468  lcmineqlem2  42469  lcmineqlem12  42479  lcmineqlem17  42484  primrootscoprmpow  42538  aks6d1c2p2  42558  deg1gprod  42579  deg1pow  42580  2np3bcnp1  42583  2ap1caineq  42584  sticksstones7  42591  sticksstones9  42593  sticksstones10  42594  sticksstones11  42595  sticksstones12a  42596  sticksstones12  42597  sticksstones22  42607  aks6d1c6lem1  42609  aks6d1c6lem3  42611  bcled  42617  bcle2d  42618  aks6d1c7lem1  42619  unitscyglem2  42635  unitscyglem4  42637  ccatcan2d  42690  fz1sump1  42742  sumcubes  42745  zaddcomlem  42908  frlmvscadiccat  42951  fltnltalem  43095  3cubeslem3l  43118  3cubeslem3r  43119  rmxyneg  43348  rmxyadd  43349  rmyp1  43361  rmxm1  43362  rmym1  43363  rmxluc  43364  rmyluc  43365  rmxdbl  43367  rmydbl  43368  jm2.18  43416  jm2.19lem1  43417  jm2.19lem2  43418  jm2.22  43423  jm2.23  43424  jm2.25  43427  jm2.27c  43435  rmxdiophlem  43443  expdioph  43451  hbtlem4  43554  relexpmulg  44137  radcnvrat  44741  nzprmdif  44746  bcc0  44767  bccp1k  44768  bccbc  44772  binomcxplemnn0  44776  binomcxplemrat  44777  binomcxplemfrat  44778  binomcxplemnotnn0  44783  fzisoeu  45733  mccllem  46027  dvxpaek  46368  dvnxpaek  46370  dvnmul  46371  dvnprodlem1  46374  dvnprodlem2  46375  stoweidlem24  46452  stirlinglem3  46504  stirlinglem7  46508  fourierdlem36  46571  fourierdlem47  46581  etransclem23  46685  etransclem32  46694  etransclem48  46710  fz0addcom  47765  fmtnom1nn  47995  fmtnof1  47998  fmtnorec1  48000  sqrtpwpw2p  48001  fmtnorec2lem  48005  fmtnorec3  48011  fmtnofac2lem  48031  fmtnofac2  48032  fmtnofac1  48033  lighneallem3  48070  lighneallem4b  48072  altgsumbc  48828  altgsumbcALT  48829  nnpw2pmod  49059  dignn0ehalf  49093  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096  nn0sumshdiglem2  49098  nn0mullong  49101  itcovalpclem2  49147  itcovalt2lem2lem2  49150  itcovalt2lem1  49151  aacllem  50276