Theorem nn0cnd 12594

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11125  ℕ₀cn0 12531

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7737  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-i2m1 11195  ax-1ne0 11196  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7417  df-om 7864  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-nn 12261  df-n0 12532

This theorem is used by:  quoremnn0ALT  13921  expaddzlem  14172  expaddz  14173  expmulz  14175  facdiv  14354  faclbnd4lem3  14362  bcp1n  14383  bcn2m1  14391  bcn2p1  14392  hashgadd  14444  hashdom  14446  hashun3  14451  hashssdif  14480  hashdifpr  14483  hashxplem  14501  hashmap  14503  hashreshashfun  14507  hashbclem  14520  hashf1lem2  14524  hashf1  14525  ccatval3  14647  ccatval21sw  14654  ccatlid  14655  ccatrid  14656  ccatass  14657  ccatrn  14658  ccatf1  14659  lswccatn0lsw  14661  ccatalpha  14663  ccatws1lenp1b  14692  wrdlenccats1lenm1  14693  ccats1val2  14698  swrdccat2  14742  pfxfv  14755  addlenpfx  14763  pfxtrcfvl  14769  pfxpfx  14780  lenrevpfxcctswrd  14784  ccats1pfxeq  14786  ccatopth2  14789  cats1un  14793  swrdccat3b  14812  spllen  14826  splfv2a  14828  revccat  14838  revpfxsfxrev  14840  cshwlen  14873  cshwidxmod  14877  repswcshw  14886  2cshwid  14888  cshweqdif2  14893  relexpaddg  15129  rtrclreclem3  15136  isercoll2  15759  iseraltlem3  15774  fsumconst1  15880  hash2iun1dif1  15914  binomlem  15921  bcxmas  15927  incexclem  15928  incexc  15929  incexc2  15930  climcndslem1  15941  climcndslem2  15942  arisum  15952  arisum2  15953  pwdif  15960  geomulcvg  15968  mertens  15978  risefacval2  16100  fallfacval2  16101  fallfacval3  16102  risefallfac  16114  risefacp1  16118  fallfacp1  16119  fallfacfwd  16125  binomfallfaclem1  16128  binomfallfaclem2  16129  binomrisefac  16131  bpolycl  16141  bpolysum  16142  bpolydiflem  16143  fsumkthpow  16145  bpoly4  16148  effsumlt  16202  dvdsexp  16421  nn0ob  16477  divalgmod  16499  bitsinv1lem  16534  sadcp1  16548  sadcaddlem  16550  sadadd2lem  16552  sadadd3  16554  sadaddlem  16559  sadasslem  16563  smupp1  16573  smumullem  16585  mulgcd  16641  absmulgcd  16642  mulgcdr  16643  gcddiv  16644  lcmgcd  16700  lcmid  16702  lcm1  16703  3lcm2e6woprm  16708  6lcm4e12  16709  mulgcddvds  16748  qredeu  16751  divgcdcoprm0  16758  divgcdcoprmex  16759  cncongr1  16760  cncongr2  16761  odzdvds  16890  powm2modprm  16898  coprimeprodsq  16903  pceulem  16940  pczpre  16942  pcqmul  16948  pcaddlem  16983  pcmpt  16987  pcmpt2  16988  sumhash  16991  oddprmdvds  16998  mul4sq  17049  4sqlem12  17051  vdwapun  17069  vdwlem2  17077  vdwlem3  17078  vdwlem6  17081  vdwlem8  17083  vdwlem9  17084  ramub1lem2  17122  ramcl  17124  chnrev  18718  mulgnn0dir  19230  mulgnn0ass  19236  lagsubg2  19325  psgnunilem2  19625  odmodnn0  19670  odmulg  19686  odmulgeq  19687  odinv  19691  sylow1lem1  19728  sylow2a  19749  sylow2blem3  19752  sylow3lem3  19759  sylow3lem4  19760  efginvrel2  19857  efgsval2  19863  efgsp1  19867  efgredlemg  19872  efgredleme  19873  efgcpbllemb  19885  odadd2  19979  odadd  19980  torsubg  19984  frgpnabllem1  20003  pgpfaclem1  20213  fincygsubgodd  20244  omndmul2  20263  omndmul3  20264  srgbinomlem3  20370  srgbinomlem4  20371  nn0srg  21653  freshmansdream  21790  mplcoe5  22259  mhpmulcl  22380  mhppwdeg  22381  psdmplcl  22393  psdmul  22397  coe1tmmul2  22505  coe1tmmul2fv  22507  coe1pwmulfv  22509  mbfi1fseqlem3  25948  dvn2bss  26160  itgpowd  26280  tdeglem4  26288  tdeglem2  26289  mdegmullem  26306  coe1mul3  26327  ply1divex  26365  fta1glem1  26396  plyaddlem1  26442  plymullem1  26443  coeeulem  26453  coemulc  26484  dgrmulc  26500  dgrcolem2  26503  dgrco  26504  dvply1  26517  dvply2g  26518  plydivlem4  26529  fta1lem  26540  vieta1lem1  26545  aareccl  26565  aaliou3lem8  26584  taylply2  26607  dvtaylp  26609  dvntaylp  26610  dvntaylp0  26611  dvradcnv  26660  pserdvlem2  26667  advlogexp  26895  cxpeq  26997  atantayl3  27179  birthdaylem2  27192  harmonicbnd4  27250  dmgmaddnn0  27266  lgamucov  27277  wilthlem2  27308  basellem2  27321  basellem3  27322  basellem5  27324  0sgm  27383  sgmppw  27436  chtublem  27450  chpval2  27457  sumdchr2  27509  bcp1ctr  27518  lgslem1  27536  gausslemma2dlem6  27611  gausslemma2d  27613  lgseisenlem2  27615  lgseisenlem3  27616  lgsquadlem1  27619  lgsquadlem2  27620  lgsquad2lem2  27624  m1lgs  27627  2lgslem1c  27632  2lgslem3a  27635  2lgslem3b  27636  2lgslem3c  27637  2lgslem3d  27638  2sqlem8  27665  2sq2  27672  2sqmod  27675  dchrisumlem1  27728  dchrisum0flblem2  27748  rpvmasum2  27751  mulogsumlem  27770  selberg2lem  27789  pntrsumo1  27804  pntrlog2bndlem4  27819  finsumvtxdg2ssteplem4  30011  vtxdgoddnumeven  30016  wlklenvm1  30084  wlklenvclwlk  30116  revwlk  30149  crctcshlem4  30291  crctcsh  30295  wlklnwwlkln2lem  30353  wlknwwlksnbij  30359  wwlksnred  30363  wwlksnext  30364  wwlksnextbi  30365  wwlksnredwwlkn  30366  wwlksnextproplem2  30381  rusgrnumwwlks  30448  rusgrnumwwlk  30449  clwwlkccatlem  30462  clwlkclwwlk  30475  clwwlkwwlksb  30527  eupth2lem3lem3  30713  eupth2lem3lem6  30716  fusgreghash2wsp  30821  frrusgrord0lem  30822  numclwwlk1  30844  numclwwlk3  30868  ex-lcm  30941  ex-ind-dvds  30944  nnmulge  33213  elq2  33285  divnumden2  33289  pfxlsw2ccat  33395  ccatws1f1o  33396  wrdt2ind  33398  gsummptrev  33499  gsummptp1  33500  gsummulsubdishift1  33511  cycpmco2lem2  33570  cycpmco2lem3  33571  cycpmco2lem4  33572  cycpmco2lem5  33573  cycpmco2lem6  33574  cycpmco2lem7  33575  cycpmco2  33576  archiabllem1a  33634  gsumind  33788  deg1prod  33996  ply1dg3rt0irred  33997  esplyind  34088  esplyindfv  34089  esplyfvn  34090  vietadeg1  34091  vietalem  34092  vieta  34093  iconstr  34279  cos9thpiminplylem1  34295  oddpwdc  34868  eulerpartlemsv2  34872  eulerpartlems  34874  eulerpartlemsv3  34875  eulerpartlemv  34878  eulerpartlemb  34882  iwrdsplit  34901  ballotlemgun  35039  ccatmulgnn0dir  35056  ofcccat  35057  signsplypnf  35061  signslema  35073  signstfvn  35080  signstfveq0  35088  signsvtp  35094  signsvtn  35095  signlem0  35098  signshf  35099  fsum2dsub  35118  hashreprin  35131  breprexp  35144  circlemeth  35151  lpadlem2  35194  lpadlen2  35195  subfacp1lem6  35767  subfacval2  35769  subfaclim  35770  cvmliftlem7  35873  elmrsubrn  36102  bcprod  36320  bccolsum  36321  faclimlem1  36325  faclim2  36330  fwddifnp1  36748  knoppndvlem6  37217  knoppndvlem14  37225  poimirlem4  38376  poimirlem5  38377  poimirlem6  38378  poimirlem7  38379  poimirlem10  38382  poimirlem11  38383  poimirlem12  38384  poimirlem16  38388  poimirlem17  38389  poimirlem19  38391  poimirlem20  38392  poimirlem22  38394  poimirlem24  38396  poimirlem25  38397  poimirlem29  38401  poimirlem31  38403  lcmineqlem1  42898  lcmineqlem2  42899  lcmineqlem12  42909  lcmineqlem17  42914  primrootscoprmpow  42968  aks6d1c2p2  42988  deg1gprod  43009  deg1pow  43010  2np3bcnp1  43013  2ap1caineq  43014  sticksstones7  43021  sticksstones9  43023  sticksstones10  43024  sticksstones11  43025  sticksstones12a  43026  sticksstones12  43027  sticksstones22  43037  aks6d1c6lem1  43039  aks6d1c6lem3  43041  bcled  43047  bcle2d  43048  aks6d1c7lem1  43049  unitscyglem2  43065  unitscyglem4  43067  ccatcan2d  43121  fz1sump1  43188  sumcubes  43191  zaddcomlem  43354  frlmvscadiccat  43397  fltnltalem  43511  3cubeslem3l  43534  3cubeslem3r  43535  rmxyneg  43764  rmxyadd  43765  rmyp1  43777  rmxm1  43778  rmym1  43779  rmxluc  43780  rmyluc  43781  rmxdbl  43783  rmydbl  43784  jm2.18  43832  jm2.19lem1  43833  jm2.19lem2  43834  jm2.22  43839  jm2.23  43840  jm2.25  43843  jm2.27c  43851  rmxdiophlem  43859  expdioph  43867  hbtlem4  43970  relexpmulg  44553  radcnvrat  45141  nzprmdif  45146  bcc0  45167  bccp1k  45168  bccbc  45172  binomcxplemnn0  45176  binomcxplemrat  45177  binomcxplemfrat  45178  binomcxplemnotnn0  45183  fzisoeu  46136  mccllem  46430  dvxpaek  46771  dvnxpaek  46773  dvnmul  46774  dvnprodlem1  46777  dvnprodlem2  46778  stoweidlem24  46855  stirlinglem3  46907  stirlinglem7  46911  fourierdlem36  46974  fourierdlem47  46984  etransclem23  47088  etransclem32  47097  etransclem48  47113  fz0addcom  48208  fmtnom1nn  48438  fmtnof1  48441  fmtnorec1  48443  sqrtpwpw2p  48444  fmtnorec2lem  48448  fmtnorec3  48454  fmtnofac2lem  48474  fmtnofac2  48475  fmtnofac1  48476  lighneallem3  48513  lighneallem4b  48515  altgsumbc  49285  altgsumbcALT  49286  nnpw2pmod  49516  dignn0ehalf  49550  nn0sumshdiglemA  49552  nn0sumshdiglemB  49553  nn0sumshdiglem2  49555  nn0mullong  49558  itcovalpclem2  49604  itcovalt2lem2lem2  49607  itcovalt2lem1  49608  aacllem  50775