Theorem nn0cnd 12494

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11030  ℕ₀cn0 12431

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 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-i2m1 11100  ax-1ne0 11101  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7364  df-om 7812  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-nn 12169  df-n0 12432

This theorem is referenced by:  quoremnn0ALT  13810  expaddzlem  14061  expaddz  14062  expmulz  14064  facdiv  14243  faclbnd4lem3  14251  bcp1n  14272  bcn2m1  14280  bcn2p1  14281  hashgadd  14333  hashdom  14335  hashun3  14340  hashssdif  14368  hashdifpr  14371  hashxplem  14389  hashmap  14391  hashreshashfun  14395  hashbclem  14408  hashf1lem2  14412  hashf1  14413  ccatval3  14535  ccatval21sw  14542  ccatlid  14543  ccatrid  14544  ccatass  14545  ccatrn  14546  lswccatn0lsw  14548  ccatalpha  14550  ccatws1lenp1b  14578  wrdlenccats1lenm1  14579  ccats1val2  14584  swrdccat2  14626  pfxfv  14639  addlenpfx  14647  pfxtrcfvl  14653  pfxpfx  14664  lenrevpfxcctswrd  14668  ccats1pfxeq  14670  ccatopth2  14673  cats1un  14677  swrdccat3b  14696  spllen  14710  splfv2a  14712  revccat  14722  cshwlen  14755  cshwidxmod  14759  repswcshw  14768  2cshwid  14770  cshweqdif2  14775  relexpaddg  15009  rtrclreclem3  15016  isercoll2  15625  iseraltlem3  15640  fsumconst1  15747  hash2iun1dif1  15781  binomlem  15788  bcxmas  15794  incexclem  15795  incexc  15796  incexc2  15797  climcndslem1  15808  climcndslem2  15809  arisum  15819  arisum2  15820  pwdif  15827  geomulcvg  15835  mertens  15845  risefacval2  15969  fallfacval2  15970  fallfacval3  15971  risefallfac  15983  risefacp1  15988  fallfacp1  15989  fallfacfwd  15995  binomfallfaclem1  15998  binomfallfaclem2  15999  binomrisefac  16001  bpolycl  16011  bpolysum  16012  bpolydiflem  16013  fsumkthpow  16015  bpoly4  16018  effsumlt  16072  dvdsexp  16291  nn0ob  16347  divalgmod  16369  bitsinv1lem  16404  sadcp1  16418  sadcaddlem  16420  sadadd2lem  16422  sadadd3  16424  sadaddlem  16429  sadasslem  16433  smupp1  16443  smumullem  16455  mulgcd  16511  absmulgcd  16512  mulgcdr  16513  gcddiv  16514  lcmgcd  16570  lcmid  16572  lcm1  16573  3lcm2e6woprm  16578  6lcm4e12  16579  mulgcddvds  16618  qredeu  16621  divgcdcoprm0  16628  divgcdcoprmex  16629  cncongr1  16630  cncongr2  16631  odzdvds  16760  powm2modprm  16768  coprimeprodsq  16773  pceulem  16810  pczpre  16812  pcqmul  16818  pcaddlem  16853  pcmpt  16857  pcmpt2  16858  sumhash  16861  oddprmdvds  16868  mul4sq  16919  4sqlem12  16921  vdwapun  16939  vdwlem2  16947  vdwlem3  16948  vdwlem6  16951  vdwlem8  16953  vdwlem9  16954  ramub1lem2  16992  ramcl  16994  chnrev  18587  mulgnn0dir  19074  mulgnn0ass  19080  lagsubg2  19163  psgnunilem2  19464  odmodnn0  19509  odmulg  19525  odmulgeq  19526  odinv  19530  sylow1lem1  19567  sylow2a  19588  sylow2blem3  19591  sylow3lem3  19598  sylow3lem4  19599  efginvrel2  19696  efgsval2  19702  efgsp1  19706  efgredlemg  19711  efgredleme  19712  efgcpbllemb  19724  odadd2  19818  odadd  19819  torsubg  19823  frgpnabllem1  19842  pgpfaclem1  20052  fincygsubgodd  20083  omndmul2  20102  omndmul3  20103  srgbinomlem3  20203  srgbinomlem4  20204  nn0srg  21430  freshmansdream  21567  mplcoe5  22031  mhpmulcl  22128  mhppwdeg  22129  psdmplcl  22141  psdmul  22145  coe1tmmul2  22254  coe1tmmul2fv  22256  coe1pwmulfv  22258  mbfi1fseqlem3  25697  dvn2bss  25910  itgpowd  26030  tdeglem4  26038  tdeglem2  26039  mdegmullem  26056  coe1mul3  26077  ply1divex  26115  fta1glem1  26146  plyaddlem1  26191  plymullem1  26192  coeeulem  26202  coemulc  26233  dgrmulc  26249  dgrcolem2  26252  dgrco  26253  dvply1  26263  dvply2g  26264  dvply2gOLD  26265  plydivlem4  26276  fta1lem  26287  vieta1lem1  26290  aareccl  26306  aaliou3lem8  26325  taylply2  26347  taylply2OLD  26348  dvtaylp  26350  dvntaylp  26351  dvntaylp0  26352  dvradcnv  26402  pserdvlem2  26409  advlogexp  26635  cxpeq  26737  atantayl3  26919  birthdaylem2  26932  harmonicbnd4  26991  dmgmaddnn0  27007  lgamucov  27018  wilthlem2  27049  basellem2  27062  basellem3  27063  basellem5  27065  0sgm  27124  sgmppw  27177  chtublem  27191  chpval2  27198  sumdchr2  27250  bcp1ctr  27259  lgslem1  27277  gausslemma2dlem6  27352  gausslemma2d  27354  lgseisenlem2  27356  lgseisenlem3  27357  lgsquadlem1  27360  lgsquadlem2  27361  lgsquad2lem2  27365  m1lgs  27368  2lgslem1c  27373  2lgslem3a  27376  2lgslem3b  27377  2lgslem3c  27378  2lgslem3d  27379  2sqlem8  27406  2sq2  27413  2sqmod  27416  dchrisumlem1  27469  dchrisum0flblem2  27489  rpvmasum2  27492  mulogsumlem  27511  selberg2lem  27530  pntrsumo1  27545  pntrlog2bndlem4  27560  finsumvtxdg2ssteplem4  29635  vtxdgoddnumeven  29640  wlklenvm1  29708  wlklenvclwlk  29740  crctcshlem4  29906  crctcsh  29910  wlklnwwlkln2lem  29968  wlknwwlksnbij  29974  wwlksnred  29978  wwlksnext  29979  wwlksnextbi  29980  wwlksnredwwlkn  29981  wwlksnextproplem2  29996  rusgrnumwwlks  30063  rusgrnumwwlk  30064  clwwlkccatlem  30077  clwlkclwwlk  30090  clwwlkwwlksb  30142  eupth2lem3lem3  30318  eupth2lem3lem6  30321  fusgreghash2wsp  30426  frrusgrord0lem  30427  numclwwlk1  30449  numclwwlk3  30473  ex-lcm  30546  ex-ind-dvds  30549  nnmulge  32830  elq2  32903  divnumden2  32907  ccatf1  33027  pfxlsw2ccat  33028  ccatws1f1o  33029  wrdt2ind  33031  gsummptrev  33135  gsummptp1  33136  gsummulsubdishift1  33147  cycpmco2lem2  33206  cycpmco2lem3  33207  cycpmco2lem4  33208  cycpmco2lem5  33209  cycpmco2lem6  33210  cycpmco2lem7  33211  cycpmco2  33212  archiabllem1a  33270  gsumind  33423  deg1prod  33661  ply1dg3rt0irred  33662  esplyind  33737  esplyindfv  33738  esplyfvn  33739  vietadeg1  33740  vietalem  33741  vieta  33742  iconstr  33929  cos9thpiminplylem1  33945  oddpwdc  34517  eulerpartlemsv2  34521  eulerpartlems  34523  eulerpartlemsv3  34524  eulerpartlemv  34527  eulerpartlemb  34531  iwrdsplit  34550  ballotlemgun  34688  ccatmulgnn0dir  34705  ofcccat  34706  signsplypnf  34713  signslema  34725  signstfvn  34732  signstfveq0  34740  signsvtp  34746  signsvtn  34747  signlem0  34750  signshf  34751  fsum2dsub  34770  hashreprin  34783  breprexp  34796  circlemeth  34803  lpadlem2  34843  lpadlen2  34844  revpfxsfxrev  35317  revwlk  35326  subfacp1lem6  35386  subfacval2  35388  subfaclim  35389  cvmliftlem7  35492  elmrsubrn  35721  bcprod  35939  bccolsum  35940  faclimlem1  35944  faclim2  35949  fwddifnp1  36366  knoppndvlem6  36796  knoppndvlem14  36804  poimirlem4  37962  poimirlem5  37963  poimirlem6  37964  poimirlem7  37965  poimirlem10  37968  poimirlem11  37969  poimirlem12  37970  poimirlem16  37974  poimirlem17  37975  poimirlem19  37977  poimirlem20  37978  poimirlem22  37980  poimirlem24  37982  poimirlem25  37983  poimirlem29  37987  poimirlem31  37989  lcmineqlem1  42485  lcmineqlem2  42486  lcmineqlem12  42496  lcmineqlem17  42501  primrootscoprmpow  42555  aks6d1c2p2  42575  deg1gprod  42596  deg1pow  42597  2np3bcnp1  42600  2ap1caineq  42601  sticksstones7  42608  sticksstones9  42610  sticksstones10  42611  sticksstones11  42612  sticksstones12a  42613  sticksstones12  42614  sticksstones22  42624  aks6d1c6lem1  42626  aks6d1c6lem3  42628  bcled  42634  bcle2d  42635  aks6d1c7lem1  42636  unitscyglem2  42652  unitscyglem4  42654  ccatcan2d  42707  fz1sump1  42759  sumcubes  42762  zaddcomlem  42925  frlmvscadiccat  42968  fltnltalem  43112  3cubeslem3l  43135  3cubeslem3r  43136  rmxyneg  43369  rmxyadd  43370  rmyp1  43382  rmxm1  43383  rmym1  43384  rmxluc  43385  rmyluc  43386  rmxdbl  43388  rmydbl  43389  jm2.18  43437  jm2.19lem1  43438  jm2.19lem2  43439  jm2.22  43444  jm2.23  43445  jm2.25  43448  jm2.27c  43456  rmxdiophlem  43464  expdioph  43472  hbtlem4  43575  relexpmulg  44158  radcnvrat  44762  nzprmdif  44767  bcc0  44788  bccp1k  44789  bccbc  44793  binomcxplemnn0  44797  binomcxplemrat  44798  binomcxplemfrat  44799  binomcxplemnotnn0  44804  fzisoeu  45754  mccllem  46048  dvxpaek  46389  dvnxpaek  46391  dvnmul  46392  dvnprodlem1  46395  dvnprodlem2  46396  stoweidlem24  46473  stirlinglem3  46525  stirlinglem7  46529  fourierdlem36  46592  fourierdlem47  46602  etransclem23  46706  etransclem32  46715  etransclem48  46731  fz0addcom  47780  fmtnom1nn  48010  fmtnof1  48013  fmtnorec1  48015  sqrtpwpw2p  48016  fmtnorec2lem  48020  fmtnorec3  48026  fmtnofac2lem  48046  fmtnofac2  48047  fmtnofac1  48048  lighneallem3  48085  lighneallem4b  48087  altgsumbc  48843  altgsumbcALT  48844  nnpw2pmod  49074  dignn0ehalf  49108  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  nn0sumshdiglem2  49113  nn0mullong  49116  itcovalpclem2  49162  itcovalt2lem2lem2  49165  itcovalt2lem1  49166  aacllem  50291