Theorem nn0cnd 12562

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11125  ℕ₀cn0 12499

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 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7727  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 theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-ov 7406  df-om 7860  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-nn 12239  df-n0 12500

This theorem is referenced by:  quoremnn0ALT  13872  expaddzlem  14121  expaddz  14122  expmulz  14124  facdiv  14303  faclbnd4lem3  14311  bcp1n  14332  bcn2m1  14340  bcn2p1  14341  hashgadd  14393  hashdom  14395  hashun3  14400  hashssdif  14428  hashdifpr  14431  hashxplem  14449  hashmap  14451  hashreshashfun  14455  hashbclem  14468  hashf1lem2  14472  hashf1  14473  ccatval3  14595  ccatval21sw  14601  ccatlid  14602  ccatrid  14603  ccatass  14604  ccatrn  14605  lswccatn0lsw  14607  ccatalpha  14609  ccatws1lenp1b  14637  wrdlenccats1lenm1  14638  ccats1val2  14643  swrdccat2  14685  pfxfv  14698  addlenpfx  14707  pfxtrcfvl  14713  pfxpfx  14724  ccats1pfxeq  14730  ccatopth2  14733  cats1un  14737  swrdccat3b  14756  spllen  14770  splfv2a  14772  revccat  14782  cshwlen  14815  cshwidxmod  14819  repswcshw  14828  2cshwid  14830  cshweqdif2  14835  relexpaddg  15070  rtrclreclem3  15077  isercoll2  15683  iseraltlem3  15698  hash2iun1dif1  15838  binomlem  15843  bcxmas  15849  incexclem  15850  incexc  15851  incexc2  15852  climcndslem1  15863  climcndslem2  15864  arisum  15874  arisum2  15875  pwdif  15882  geomulcvg  15890  mertens  15900  risefacval2  16024  fallfacval2  16025  fallfacval3  16026  risefallfac  16038  risefacp1  16043  fallfacp1  16044  fallfacfwd  16050  binomfallfaclem1  16053  binomfallfaclem2  16054  binomrisefac  16056  bpolycl  16066  bpolysum  16067  bpolydiflem  16068  fsumkthpow  16070  bpoly4  16073  effsumlt  16127  dvdsexp  16345  nn0ob  16401  divalgmod  16423  bitsinv1lem  16458  sadcp1  16472  sadcaddlem  16474  sadadd2lem  16476  sadadd3  16478  sadaddlem  16483  sadasslem  16487  smupp1  16497  smumullem  16509  mulgcd  16565  absmulgcd  16566  mulgcdr  16567  gcddiv  16568  lcmgcd  16624  lcmid  16626  lcm1  16627  3lcm2e6woprm  16632  6lcm4e12  16633  mulgcddvds  16672  qredeu  16675  divgcdcoprm0  16682  divgcdcoprmex  16683  cncongr1  16684  cncongr2  16685  odzdvds  16813  powm2modprm  16821  coprimeprodsq  16826  pceulem  16863  pczpre  16865  pcqmul  16871  pcaddlem  16906  pcmpt  16910  pcmpt2  16911  sumhash  16914  oddprmdvds  16921  mul4sq  16972  4sqlem12  16974  vdwapun  16992  vdwlem2  17000  vdwlem3  17001  vdwlem6  17004  vdwlem8  17006  vdwlem9  17007  ramub1lem2  17045  ramcl  17047  mulgnn0dir  19085  mulgnn0ass  19091  lagsubg2  19175  psgnunilem2  19474  odmodnn0  19519  odmulg  19535  odmulgeq  19536  odinv  19540  sylow1lem1  19577  sylow2a  19598  sylow2blem3  19601  sylow3lem3  19608  sylow3lem4  19609  efginvrel2  19706  efgsval2  19712  efgsp1  19716  efgredlemg  19721  efgredleme  19722  efgcpbllemb  19734  odadd2  19828  odadd  19829  torsubg  19833  frgpnabllem1  19852  pgpfaclem1  20062  fincygsubgodd  20093  srgbinomlem3  20186  srgbinomlem4  20187  nn0srg  21403  freshmansdream  21533  mplcoe5  21996  mhpmulcl  22085  mhppwdeg  22086  psdmplcl  22098  psdmul  22102  coe1tmmul2  22211  coe1tmmul2fv  22213  coe1pwmulfv  22215  mbfi1fseqlem3  25668  dvn2bss  25882  itgpowd  26007  tdeglem4  26015  tdeglem2  26016  mdegmullem  26033  coe1mul3  26054  ply1divex  26092  fta1glem1  26123  plyaddlem1  26168  plymullem1  26169  coeeulem  26179  coemulc  26210  dgrmulc  26227  dgrcolem2  26230  dgrco  26231  dvply1  26241  dvply2g  26242  dvply2gOLD  26243  plydivlem4  26254  fta1lem  26265  vieta1lem1  26268  aareccl  26284  aaliou3lem8  26303  taylply2  26325  taylply2OLD  26326  dvtaylp  26328  dvntaylp  26329  dvntaylp0  26330  dvradcnv  26380  pserdvlem2  26388  advlogexp  26614  cxpeq  26717  atantayl3  26899  birthdaylem2  26912  harmonicbnd4  26971  dmgmaddnn0  26987  lgamucov  26998  wilthlem2  27029  basellem2  27042  basellem3  27043  basellem5  27045  0sgm  27104  sgmppw  27158  chtublem  27172  chpval2  27179  sumdchr2  27231  bcp1ctr  27240  lgslem1  27258  gausslemma2dlem6  27333  gausslemma2d  27335  lgseisenlem2  27337  lgseisenlem3  27338  lgsquadlem1  27341  lgsquadlem2  27342  lgsquad2lem2  27346  m1lgs  27349  2lgslem1c  27354  2lgslem3a  27357  2lgslem3b  27358  2lgslem3c  27359  2lgslem3d  27360  2sqlem8  27387  2sq2  27394  2sqmod  27397  dchrisumlem1  27450  dchrisum0flblem2  27470  rpvmasum2  27473  mulogsumlem  27492  selberg2lem  27511  pntrsumo1  27526  pntrlog2bndlem4  27541  finsumvtxdg2ssteplem4  29474  vtxdgoddnumeven  29479  wlklenvm1  29548  wlklenvclwlk  29581  crctcshlem4  29748  crctcsh  29752  wlklnwwlkln2lem  29810  wlknwwlksnbij  29816  wwlksnred  29820  wwlksnext  29821  wwlksnextbi  29822  wwlksnredwwlkn  29823  wwlksnextproplem2  29838  rusgrnumwwlks  29902  rusgrnumwwlk  29903  clwwlkccatlem  29916  clwlkclwwlk  29929  clwwlkwwlksb  29981  eupth2lem3lem3  30157  eupth2lem3lem6  30160  fusgreghash2wsp  30265  frrusgrord0lem  30266  numclwwlk1  30288  numclwwlk3  30312  ex-lcm  30385  ex-ind-dvds  30388  nnmulge  32662  elq2  32736  divnumden2  32740  ccatf1  32870  pfxlsw2ccat  32872  ccatws1f1o  32873  wrdt2ind  32875  omndmul2  33026  omndmul3  33027  cycpmco2lem2  33084  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmco2  33090  archiabllem1a  33135  ply1dg3rt0irred  33541  iconstr  33746  cos9thpiminplylem1  33762  oddpwdc  34332  eulerpartlemsv2  34336  eulerpartlems  34338  eulerpartlemsv3  34339  eulerpartlemv  34342  eulerpartlemb  34346  iwrdsplit  34365  ballotlemgun  34503  ccatmulgnn0dir  34520  ofcccat  34521  signsplypnf  34528  signslema  34540  signstfvn  34547  signstfveq0  34555  signsvtp  34561  signsvtn  34562  signlem0  34565  signshf  34566  fsum2dsub  34585  hashreprin  34598  breprexp  34611  circlemeth  34618  lpadlem2  34658  lpadlen2  34659  revpfxsfxrev  35084  revwlk  35093  subfacp1lem6  35153  subfacval2  35155  subfaclim  35156  cvmliftlem7  35259  elmrsubrn  35488  bcprod  35701  bccolsum  35702  faclimlem1  35706  faclim2  35711  fwddifnp1  36129  knoppndvlem6  36481  knoppndvlem14  36489  poimirlem4  37594  poimirlem5  37595  poimirlem6  37596  poimirlem7  37597  poimirlem10  37600  poimirlem11  37601  poimirlem12  37602  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem22  37612  poimirlem24  37614  poimirlem25  37615  poimirlem29  37619  poimirlem31  37621  lcmineqlem1  41988  lcmineqlem2  41989  lcmineqlem12  41999  lcmineqlem17  42004  primrootscoprmpow  42058  aks6d1c2p2  42078  deg1gprod  42099  deg1pow  42100  2np3bcnp1  42103  2ap1caineq  42104  sticksstones7  42111  sticksstones9  42113  sticksstones10  42114  sticksstones11  42115  sticksstones12a  42116  sticksstones12  42117  sticksstones22  42127  aks6d1c6lem1  42129  aks6d1c6lem3  42131  bcled  42137  bcle2d  42138  aks6d1c7lem1  42139  unitscyglem2  42155  unitscyglem4  42157  ccatcan2d  42249  fz1sump1  42306  sumcubes  42309  zaddcomlem  42441  frlmvscadiccat  42476  fltnltalem  42632  3cubeslem3l  42656  3cubeslem3r  42657  rmxyneg  42891  rmxyadd  42892  rmyp1  42904  rmxm1  42905  rmym1  42906  rmxluc  42907  rmyluc  42908  rmxdbl  42910  rmydbl  42911  jm2.18  42959  jm2.19lem1  42960  jm2.19lem2  42961  jm2.22  42966  jm2.23  42967  jm2.25  42970  jm2.27c  42978  rmxdiophlem  42986  expdioph  42994  hbtlem4  43097  relexpmulg  43681  radcnvrat  44286  nzprmdif  44291  bcc0  44312  bccp1k  44313  bccbc  44317  binomcxplemnn0  44321  binomcxplemrat  44322  binomcxplemfrat  44323  binomcxplemnotnn0  44328  fzisoeu  45277  mccllem  45574  dvxpaek  45917  dvnxpaek  45919  dvnmul  45920  dvnprodlem1  45923  dvnprodlem2  45924  stoweidlem24  46001  stirlinglem3  46053  stirlinglem7  46057  fourierdlem36  46120  fourierdlem47  46130  etransclem23  46234  etransclem32  46243  etransclem48  46259  fz0addcom  47294  fmtnom1nn  47494  fmtnof1  47497  fmtnorec1  47499  sqrtpwpw2p  47500  fmtnorec2lem  47504  fmtnorec3  47510  fmtnofac2lem  47530  fmtnofac2  47531  fmtnofac1  47532  lighneallem3  47569  lighneallem4b  47571  altgsumbc  48275  altgsumbcALT  48276  nnpw2pmod  48511  dignn0ehalf  48545  nn0sumshdiglemA  48547  nn0sumshdiglemB  48548  nn0sumshdiglem2  48550  nn0mullong  48553  itcovalpclem2  48599  itcovalt2lem2lem2  48602  itcovalt2lem1  48603  aacllem  49613