Theorem nn0cnd 12589

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11153  ℕ₀cn0 12526

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-i2m1 11223  ax-1ne0 11224  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-nn 12267  df-n0 12527

This theorem is referenced by:  quoremnn0ALT  13897  expaddzlem  14146  expaddz  14147  expmulz  14149  facdiv  14326  faclbnd4lem3  14334  bcp1n  14355  bcn2m1  14363  bcn2p1  14364  hashgadd  14416  hashdom  14418  hashun3  14423  hashssdif  14451  hashdifpr  14454  hashxplem  14472  hashmap  14474  hashreshashfun  14478  hashbclem  14491  hashf1lem2  14495  hashf1  14496  ccatval3  14617  ccatval21sw  14623  ccatlid  14624  ccatrid  14625  ccatass  14626  ccatrn  14627  lswccatn0lsw  14629  ccatalpha  14631  ccatws1lenp1b  14659  wrdlenccats1lenm1  14660  ccats1val2  14665  swrdccat2  14707  pfxfv  14720  addlenpfx  14729  pfxtrcfvl  14735  pfxpfx  14746  ccats1pfxeq  14752  ccatopth2  14755  cats1un  14759  swrdccat3b  14778  spllen  14792  splfv2a  14794  revccat  14804  cshwlen  14837  cshwidxmod  14841  repswcshw  14850  2cshwid  14852  cshweqdif2  14857  relexpaddg  15092  rtrclreclem3  15099  isercoll2  15705  iseraltlem3  15720  hash2iun1dif1  15860  binomlem  15865  bcxmas  15871  incexclem  15872  incexc  15873  incexc2  15874  climcndslem1  15885  climcndslem2  15886  arisum  15896  arisum2  15897  pwdif  15904  geomulcvg  15912  mertens  15922  risefacval2  16046  fallfacval2  16047  fallfacval3  16048  risefallfac  16060  risefacp1  16065  fallfacp1  16066  fallfacfwd  16072  binomfallfaclem1  16075  binomfallfaclem2  16076  binomrisefac  16078  bpolycl  16088  bpolysum  16089  bpolydiflem  16090  fsumkthpow  16092  bpoly4  16095  effsumlt  16147  dvdsexp  16365  nn0ob  16421  divalgmod  16443  bitsinv1lem  16478  sadcp1  16492  sadcaddlem  16494  sadadd2lem  16496  sadadd3  16498  sadaddlem  16503  sadasslem  16507  smupp1  16517  smumullem  16529  mulgcd  16585  absmulgcd  16586  mulgcdr  16587  gcddiv  16588  lcmgcd  16644  lcmid  16646  lcm1  16647  3lcm2e6woprm  16652  6lcm4e12  16653  mulgcddvds  16692  qredeu  16695  divgcdcoprm0  16702  divgcdcoprmex  16703  cncongr1  16704  cncongr2  16705  odzdvds  16833  powm2modprm  16841  coprimeprodsq  16846  pceulem  16883  pczpre  16885  pcqmul  16891  pcaddlem  16926  pcmpt  16930  pcmpt2  16931  sumhash  16934  oddprmdvds  16941  mul4sq  16992  4sqlem12  16994  vdwapun  17012  vdwlem2  17020  vdwlem3  17021  vdwlem6  17024  vdwlem8  17026  vdwlem9  17027  ramub1lem2  17065  ramcl  17067  mulgnn0dir  19122  mulgnn0ass  19128  lagsubg2  19212  psgnunilem2  19513  odmodnn0  19558  odmulg  19574  odmulgeq  19575  odinv  19579  sylow1lem1  19616  sylow2a  19637  sylow2blem3  19640  sylow3lem3  19647  sylow3lem4  19648  efginvrel2  19745  efgsval2  19751  efgsp1  19755  efgredlemg  19760  efgredleme  19761  efgcpbllemb  19773  odadd2  19867  odadd  19868  torsubg  19872  frgpnabllem1  19891  pgpfaclem1  20101  fincygsubgodd  20132  srgbinomlem3  20225  srgbinomlem4  20226  nn0srg  21455  freshmansdream  21593  mplcoe5  22058  mhpmulcl  22153  mhppwdeg  22154  psdmplcl  22166  psdmul  22170  coe1tmmul2  22279  coe1tmmul2fv  22281  coe1pwmulfv  22283  mbfi1fseqlem3  25752  dvn2bss  25966  itgpowd  26091  tdeglem4  26099  tdeglem2  26100  mdegmullem  26117  coe1mul3  26138  ply1divex  26176  fta1glem1  26207  plyaddlem1  26252  plymullem1  26253  coeeulem  26263  coemulc  26294  dgrmulc  26311  dgrcolem2  26314  dgrco  26315  dvply1  26325  dvply2g  26326  dvply2gOLD  26327  plydivlem4  26338  fta1lem  26349  vieta1lem1  26352  aareccl  26368  aaliou3lem8  26387  taylply2  26409  taylply2OLD  26410  dvtaylp  26412  dvntaylp  26413  dvntaylp0  26414  dvradcnv  26464  pserdvlem2  26472  advlogexp  26697  cxpeq  26800  atantayl3  26982  birthdaylem2  26995  harmonicbnd4  27054  dmgmaddnn0  27070  lgamucov  27081  wilthlem2  27112  basellem2  27125  basellem3  27126  basellem5  27128  0sgm  27187  sgmppw  27241  chtublem  27255  chpval2  27262  sumdchr2  27314  bcp1ctr  27323  lgslem1  27341  gausslemma2dlem6  27416  gausslemma2d  27418  lgseisenlem2  27420  lgseisenlem3  27421  lgsquadlem1  27424  lgsquadlem2  27425  lgsquad2lem2  27429  m1lgs  27432  2lgslem1c  27437  2lgslem3a  27440  2lgslem3b  27441  2lgslem3c  27442  2lgslem3d  27443  2sqlem8  27470  2sq2  27477  2sqmod  27480  dchrisumlem1  27533  dchrisum0flblem2  27553  rpvmasum2  27556  mulogsumlem  27575  selberg2lem  27594  pntrsumo1  27609  pntrlog2bndlem4  27624  finsumvtxdg2ssteplem4  29566  vtxdgoddnumeven  29571  wlklenvm1  29640  wlklenvclwlk  29673  crctcshlem4  29840  crctcsh  29844  wlklnwwlkln2lem  29902  wlknwwlksnbij  29908  wwlksnred  29912  wwlksnext  29913  wwlksnextbi  29914  wwlksnredwwlkn  29915  wwlksnextproplem2  29930  rusgrnumwwlks  29994  rusgrnumwwlk  29995  clwwlkccatlem  30008  clwlkclwwlk  30021  clwwlkwwlksb  30073  eupth2lem3lem3  30249  eupth2lem3lem6  30252  fusgreghash2wsp  30357  frrusgrord0lem  30358  numclwwlk1  30380  numclwwlk3  30404  ex-lcm  30477  ex-ind-dvds  30480  nnmulge  32749  divnumden2  32817  ccatf1  32933  pfxlsw2ccat  32935  ccatws1f1o  32936  wrdt2ind  32938  omndmul2  33089  omndmul3  33090  cycpmco2lem2  33147  cycpmco2lem3  33148  cycpmco2lem4  33149  cycpmco2lem5  33150  cycpmco2lem6  33151  cycpmco2lem7  33152  cycpmco2  33153  archiabllem1a  33198  ply1dg3rt0irred  33607  oddpwdc  34356  eulerpartlemsv2  34360  eulerpartlems  34362  eulerpartlemsv3  34363  eulerpartlemv  34366  eulerpartlemb  34370  iwrdsplit  34389  ballotlemgun  34527  ccatmulgnn0dir  34557  ofcccat  34558  signsplypnf  34565  signslema  34577  signstfvn  34584  signstfveq0  34592  signsvtp  34598  signsvtn  34599  signlem0  34602  signshf  34603  fsum2dsub  34622  hashreprin  34635  breprexp  34648  circlemeth  34655  lpadlem2  34695  lpadlen2  34696  revpfxsfxrev  35121  revwlk  35130  subfacp1lem6  35190  subfacval2  35192  subfaclim  35193  cvmliftlem7  35296  elmrsubrn  35525  bcprod  35738  bccolsum  35739  faclimlem1  35743  faclim2  35748  fwddifnp1  36166  knoppndvlem6  36518  knoppndvlem14  36526  poimirlem4  37631  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem22  37649  poimirlem24  37651  poimirlem25  37652  poimirlem29  37656  poimirlem31  37658  lcmineqlem1  42030  lcmineqlem2  42031  lcmineqlem12  42041  lcmineqlem17  42046  primrootscoprmpow  42100  aks6d1c2p2  42120  deg1gprod  42141  deg1pow  42142  2np3bcnp1  42145  2ap1caineq  42146  sticksstones7  42153  sticksstones9  42155  sticksstones10  42156  sticksstones11  42157  sticksstones12a  42158  sticksstones12  42159  sticksstones22  42169  aks6d1c6lem1  42171  aks6d1c6lem3  42173  bcled  42179  bcle2d  42180  aks6d1c7lem1  42181  unitscyglem2  42197  unitscyglem4  42199  ccatcan2d  42292  fz1sump1  42344  sumcubes  42347  zaddcomlem  42481  frlmvscadiccat  42516  fltnltalem  42672  3cubeslem3l  42697  3cubeslem3r  42698  rmxyneg  42932  rmxyadd  42933  rmyp1  42945  rmxm1  42946  rmym1  42947  rmxluc  42948  rmyluc  42949  rmxdbl  42951  rmydbl  42952  jm2.18  43000  jm2.19lem1  43001  jm2.19lem2  43002  jm2.22  43007  jm2.23  43008  jm2.25  43011  jm2.27c  43019  rmxdiophlem  43027  expdioph  43035  hbtlem4  43138  relexpmulg  43723  radcnvrat  44333  nzprmdif  44338  bcc0  44359  bccp1k  44360  bccbc  44364  binomcxplemnn0  44368  binomcxplemrat  44369  binomcxplemfrat  44370  binomcxplemnotnn0  44375  fzisoeu  45312  mccllem  45612  dvxpaek  45955  dvnxpaek  45957  dvnmul  45958  dvnprodlem1  45961  dvnprodlem2  45962  stoweidlem24  46039  stirlinglem3  46091  stirlinglem7  46095  fourierdlem36  46158  fourierdlem47  46168  etransclem23  46272  etransclem32  46281  etransclem48  46297  fz0addcom  47329  fmtnom1nn  47519  fmtnof1  47522  fmtnorec1  47524  sqrtpwpw2p  47525  fmtnorec2lem  47529  fmtnorec3  47535  fmtnofac2lem  47555  fmtnofac2  47556  fmtnofac1  47557  lighneallem3  47594  lighneallem4b  47596  altgsumbc  48268  altgsumbcALT  48269  nnpw2pmod  48504  dignn0ehalf  48538  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  nn0sumshdiglem2  48543  nn0mullong  48546  itcovalpclem2  48592  itcovalt2lem2lem2  48595  itcovalt2lem1  48596  aacllem  49320