Theorem nn0cnd 12545

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℂcc 11072  ℕ₀cn0 12482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pr 5391  ax-un 7719  ax-resscn 11131  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-addrcl 11135  ax-mulcl 11136  ax-mulrcl 11137  ax-i2m1 11142  ax-1ne0 11143  ax-rnegex 11145  ax-rrecex 11146  ax-cnre 11147

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-reu 3369  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5102  df-opab 5164  df-mpt 5183  df-tr 5209  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-pred 6289  df-ord 6350  df-on 6351  df-lim 6352  df-suc 6353  df-iota 6478  df-fun 6524  df-fn 6525  df-f 6526  df-f1 6527  df-fo 6528  df-f1o 6529  df-fv 6530  df-ov 7400  df-om 7848  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8382  df-nn 12212  df-n0 12483

This theorem is referenced by:  quoremnn0ALT  13868  expaddzlem  14119  expaddz  14120  expmulz  14122  facdiv  14301  faclbnd4lem3  14309  bcp1n  14330  bcn2m1  14338  bcn2p1  14339  hashgadd  14391  hashdom  14393  hashun3  14398  hashssdif  14426  hashdifpr  14429  hashxplem  14447  hashmap  14449  hashreshashfun  14453  hashbclem  14466  hashf1lem2  14470  hashf1  14471  ccatval3  14593  ccatval21sw  14600  ccatlid  14601  ccatrid  14602  ccatass  14603  ccatrn  14604  lswccatn0lsw  14606  ccatalpha  14608  ccatws1lenp1b  14636  wrdlenccats1lenm1  14637  ccats1val2  14642  swrdccat2  14684  pfxfv  14697  addlenpfx  14705  pfxtrcfvl  14711  pfxpfx  14722  lenrevpfxcctswrd  14726  ccats1pfxeq  14728  ccatopth2  14731  cats1un  14735  swrdccat3b  14754  spllen  14768  splfv2a  14770  revccat  14780  cshwlen  14813  cshwidxmod  14817  repswcshw  14826  2cshwid  14828  cshweqdif2  14833  relexpaddg  15067  rtrclreclem3  15074  isercoll2  15697  iseraltlem3  15712  fsumconst1  15819  hash2iun1dif1  15853  binomlem  15860  bcxmas  15866  incexclem  15867  incexc  15868  incexc2  15869  climcndslem1  15880  climcndslem2  15881  arisum  15891  arisum2  15892  pwdif  15899  geomulcvg  15907  mertens  15917  risefacval2  16041  fallfacval2  16042  fallfacval3  16043  risefallfac  16055  risefacp1  16060  fallfacp1  16061  fallfacfwd  16067  binomfallfaclem1  16070  binomfallfaclem2  16071  binomrisefac  16073  bpolycl  16083  bpolysum  16084  bpolydiflem  16085  fsumkthpow  16087  bpoly4  16090  effsumlt  16144  dvdsexp  16363  nn0ob  16419  divalgmod  16441  bitsinv1lem  16476  sadcp1  16490  sadcaddlem  16492  sadadd2lem  16494  sadadd3  16496  sadaddlem  16501  sadasslem  16505  smupp1  16515  smumullem  16527  mulgcd  16583  absmulgcd  16584  mulgcdr  16585  gcddiv  16586  lcmgcd  16642  lcmid  16644  lcm1  16645  3lcm2e6woprm  16650  6lcm4e12  16651  mulgcddvds  16690  qredeu  16693  divgcdcoprm0  16700  divgcdcoprmex  16701  cncongr1  16702  cncongr2  16703  odzdvds  16832  powm2modprm  16840  coprimeprodsq  16845  pceulem  16882  pczpre  16884  pcqmul  16890  pcaddlem  16925  pcmpt  16929  pcmpt2  16930  sumhash  16933  oddprmdvds  16940  mul4sq  16991  4sqlem12  16993  vdwapun  17011  vdwlem2  17019  vdwlem3  17020  vdwlem6  17023  vdwlem8  17025  vdwlem9  17026  ramub1lem2  17064  ramcl  17066  chnrev  18660  mulgnn0dir  19147  mulgnn0ass  19153  lagsubg2  19236  psgnunilem2  19536  odmodnn0  19581  odmulg  19597  odmulgeq  19598  odinv  19602  sylow1lem1  19639  sylow2a  19660  sylow2blem3  19663  sylow3lem3  19670  sylow3lem4  19671  efginvrel2  19768  efgsval2  19774  efgsp1  19778  efgredlemg  19783  efgredleme  19784  efgcpbllemb  19796  odadd2  19890  odadd  19891  torsubg  19895  frgpnabllem1  19914  pgpfaclem1  20124  fincygsubgodd  20155  omndmul2  20174  omndmul3  20175  srgbinomlem3  20279  srgbinomlem4  20280  nn0srg  21490  freshmansdream  21627  mplcoe5  22094  mhpmulcl  22215  mhppwdeg  22216  psdmplcl  22228  psdmul  22232  coe1tmmul2  22340  coe1tmmul2fv  22342  coe1pwmulfv  22344  mbfi1fseqlem3  25780  dvn2bss  25993  itgpowd  26113  tdeglem4  26121  tdeglem2  26122  mdegmullem  26139  coe1mul3  26160  ply1divex  26198  fta1glem1  26229  plyaddlem1  26274  plymullem1  26275  coeeulem  26285  coemulc  26316  dgrmulc  26332  dgrcolem2  26335  dgrco  26336  dvply1  26349  dvply2g  26350  plydivlem4  26361  fta1lem  26372  vieta1lem1  26375  aareccl  26391  aaliou3lem8  26410  taylply2  26432  dvtaylp  26434  dvntaylp  26435  dvntaylp0  26436  dvradcnv  26485  pserdvlem2  26492  advlogexp  26721  cxpeq  26823  atantayl3  27005  birthdaylem2  27018  harmonicbnd4  27076  dmgmaddnn0  27092  lgamucov  27103  wilthlem2  27134  basellem2  27147  basellem3  27148  basellem5  27150  0sgm  27209  sgmppw  27262  chtublem  27276  chpval2  27283  sumdchr2  27335  bcp1ctr  27344  lgslem1  27362  gausslemma2dlem6  27437  gausslemma2d  27439  lgseisenlem2  27441  lgseisenlem3  27442  lgsquadlem1  27445  lgsquadlem2  27446  lgsquad2lem2  27450  m1lgs  27453  2lgslem1c  27458  2lgslem3a  27461  2lgslem3b  27462  2lgslem3c  27463  2lgslem3d  27464  2sqlem8  27491  2sq2  27498  2sqmod  27501  dchrisumlem1  27554  dchrisum0flblem2  27574  rpvmasum2  27577  mulogsumlem  27596  selberg2lem  27615  pntrsumo1  27630  pntrlog2bndlem4  27645  finsumvtxdg2ssteplem4  29750  vtxdgoddnumeven  29755  wlklenvm1  29823  wlklenvclwlk  29855  crctcshlem4  30021  crctcsh  30025  wlklnwwlkln2lem  30083  wlknwwlksnbij  30089  wwlksnred  30093  wwlksnext  30094  wwlksnextbi  30095  wwlksnredwwlkn  30096  wwlksnextproplem2  30111  rusgrnumwwlks  30178  rusgrnumwwlk  30179  clwwlkccatlem  30192  clwlkclwwlk  30205  clwwlkwwlksb  30257  eupth2lem3lem3  30433  eupth2lem3lem6  30436  fusgreghash2wsp  30541  frrusgrord0lem  30542  numclwwlk1  30564  numclwwlk3  30588  ex-lcm  30661  ex-ind-dvds  30664  nnmulge  32942  elq2  33015  divnumden2  33019  ccatf1  33128  pfxlsw2ccat  33129  ccatws1f1o  33130  wrdt2ind  33132  gsummptrev  33237  gsummptp1  33238  gsummulsubdishift1  33249  cycpmco2lem2  33308  cycpmco2lem3  33309  cycpmco2lem4  33310  cycpmco2lem5  33311  cycpmco2lem6  33312  cycpmco2lem7  33313  cycpmco2  33314  archiabllem1a  33372  gsumind  33532  deg1prod  33780  ply1dg3rt0irred  33781  esplyind  33873  esplyindfv  33874  esplyfvn  33875  vietadeg1  33876  vietalem  33877  vieta  33878  iconstr  34064  cos9thpiminplylem1  34080  oddpwdc  34652  eulerpartlemsv2  34656  eulerpartlems  34658  eulerpartlemsv3  34659  eulerpartlemv  34662  eulerpartlemb  34666  iwrdsplit  34685  ballotlemgun  34823  ccatmulgnn0dir  34840  ofcccat  34841  signsplypnf  34845  signslema  34857  signstfvn  34864  signstfveq0  34872  signsvtp  34878  signsvtn  34879  signlem0  34882  signshf  34883  fsum2dsub  34902  hashreprin  34915  breprexp  34928  circlemeth  34935  lpadlem2  34978  lpadlen2  34979  revpfxsfxrev  35467  revwlk  35476  subfacp1lem6  35536  subfacval2  35538  subfaclim  35539  cvmliftlem7  35642  elmrsubrn  35871  bcprod  36089  bccolsum  36090  faclimlem1  36094  faclim2  36099  fwddifnp1  36516  knoppndvlem6  36956  knoppndvlem14  36964  poimirlem4  38124  poimirlem5  38125  poimirlem6  38126  poimirlem7  38127  poimirlem10  38130  poimirlem11  38131  poimirlem12  38132  poimirlem16  38136  poimirlem17  38137  poimirlem19  38139  poimirlem20  38140  poimirlem22  38142  poimirlem24  38144  poimirlem25  38145  poimirlem29  38149  poimirlem31  38151  lcmineqlem1  42647  lcmineqlem2  42648  lcmineqlem12  42658  lcmineqlem17  42663  primrootscoprmpow  42717  aks6d1c2p2  42737  deg1gprod  42758  deg1pow  42759  2np3bcnp1  42762  2ap1caineq  42763  sticksstones7  42770  sticksstones9  42772  sticksstones10  42773  sticksstones11  42774  sticksstones12a  42775  sticksstones12  42776  sticksstones22  42786  aks6d1c6lem1  42788  aks6d1c6lem3  42790  bcled  42796  bcle2d  42797  aks6d1c7lem1  42798  unitscyglem2  42814  unitscyglem4  42816  ccatcan2d  42868  fz1sump1  42920  sumcubes  42923  zaddcomlem  43086  frlmvscadiccat  43129  fltnltalem  43245  3cubeslem3l  43268  3cubeslem3r  43269  rmxyneg  43498  rmxyadd  43499  rmyp1  43511  rmxm1  43512  rmym1  43513  rmxluc  43514  rmyluc  43515  rmxdbl  43517  rmydbl  43518  jm2.18  43566  jm2.19lem1  43567  jm2.19lem2  43568  jm2.22  43573  jm2.23  43574  jm2.25  43577  jm2.27c  43585  rmxdiophlem  43593  expdioph  43601  hbtlem4  43704  relexpmulg  44287  radcnvrat  44891  nzprmdif  44896  bcc0  44917  bccp1k  44918  bccbc  44922  binomcxplemnn0  44926  binomcxplemrat  44927  binomcxplemfrat  44928  binomcxplemnotnn0  44933  fzisoeu  45880  mccllem  46174  dvxpaek  46515  dvnxpaek  46517  dvnmul  46518  dvnprodlem1  46521  dvnprodlem2  46522  stoweidlem24  46599  stirlinglem3  46651  stirlinglem7  46655  fourierdlem36  46718  fourierdlem47  46728  etransclem23  46832  etransclem32  46841  etransclem48  46857  fz0addcom  47912  fmtnom1nn  48142  fmtnof1  48145  fmtnorec1  48147  sqrtpwpw2p  48148  fmtnorec2lem  48152  fmtnorec3  48158  fmtnofac2lem  48178  fmtnofac2  48179  fmtnofac1  48180  lighneallem3  48217  lighneallem4b  48219  altgsumbc  48975  altgsumbcALT  48976  nnpw2pmod  49206  dignn0ehalf  49240  nn0sumshdiglemA  49242  nn0sumshdiglemB  49243  nn0sumshdiglem2  49245  nn0mullong  49248  itcovalpclem2  49294  itcovalt2lem2lem2  49297  itcovalt2lem1  49298  aacllem  50423