Theorem nn0cnd 12481

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11042  ℕ₀cn0 12418

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-i2m1 11112  ax-1ne0 11113  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-nn 12163  df-n0 12419

This theorem is referenced by:  quoremnn0ALT  13795  expaddzlem  14046  expaddz  14047  expmulz  14049  facdiv  14228  faclbnd4lem3  14236  bcp1n  14257  bcn2m1  14265  bcn2p1  14266  hashgadd  14318  hashdom  14320  hashun3  14325  hashssdif  14353  hashdifpr  14356  hashxplem  14374  hashmap  14376  hashreshashfun  14380  hashbclem  14393  hashf1lem2  14397  hashf1  14398  ccatval3  14520  ccatval21sw  14526  ccatlid  14527  ccatrid  14528  ccatass  14529  ccatrn  14530  lswccatn0lsw  14532  ccatalpha  14534  ccatws1lenp1b  14562  wrdlenccats1lenm1  14563  ccats1val2  14568  swrdccat2  14610  pfxfv  14623  addlenpfx  14632  pfxtrcfvl  14638  pfxpfx  14649  ccats1pfxeq  14655  ccatopth2  14658  cats1un  14662  swrdccat3b  14681  spllen  14695  splfv2a  14697  revccat  14707  cshwlen  14740  cshwidxmod  14744  repswcshw  14753  2cshwid  14755  cshweqdif2  14760  relexpaddg  14995  rtrclreclem3  15002  isercoll2  15611  iseraltlem3  15626  hash2iun1dif1  15766  binomlem  15771  bcxmas  15777  incexclem  15778  incexc  15779  incexc2  15780  climcndslem1  15791  climcndslem2  15792  arisum  15802  arisum2  15803  pwdif  15810  geomulcvg  15818  mertens  15828  risefacval2  15952  fallfacval2  15953  fallfacval3  15954  risefallfac  15966  risefacp1  15971  fallfacp1  15972  fallfacfwd  15978  binomfallfaclem1  15981  binomfallfaclem2  15982  binomrisefac  15984  bpolycl  15994  bpolysum  15995  bpolydiflem  15996  fsumkthpow  15998  bpoly4  16001  effsumlt  16055  dvdsexp  16274  nn0ob  16330  divalgmod  16352  bitsinv1lem  16387  sadcp1  16401  sadcaddlem  16403  sadadd2lem  16405  sadadd3  16407  sadaddlem  16412  sadasslem  16416  smupp1  16426  smumullem  16438  mulgcd  16494  absmulgcd  16495  mulgcdr  16496  gcddiv  16497  lcmgcd  16553  lcmid  16555  lcm1  16556  3lcm2e6woprm  16561  6lcm4e12  16562  mulgcddvds  16601  qredeu  16604  divgcdcoprm0  16611  divgcdcoprmex  16612  cncongr1  16613  cncongr2  16614  odzdvds  16742  powm2modprm  16750  coprimeprodsq  16755  pceulem  16792  pczpre  16794  pcqmul  16800  pcaddlem  16835  pcmpt  16839  pcmpt2  16840  sumhash  16843  oddprmdvds  16850  mul4sq  16901  4sqlem12  16903  vdwapun  16921  vdwlem2  16929  vdwlem3  16930  vdwlem6  16933  vdwlem8  16935  vdwlem9  16936  ramub1lem2  16974  ramcl  16976  mulgnn0dir  19018  mulgnn0ass  19024  lagsubg2  19108  psgnunilem2  19409  odmodnn0  19454  odmulg  19470  odmulgeq  19471  odinv  19475  sylow1lem1  19512  sylow2a  19533  sylow2blem3  19536  sylow3lem3  19543  sylow3lem4  19544  efginvrel2  19641  efgsval2  19647  efgsp1  19651  efgredlemg  19656  efgredleme  19657  efgcpbllemb  19669  odadd2  19763  odadd  19764  torsubg  19768  frgpnabllem1  19787  pgpfaclem1  19997  fincygsubgodd  20028  omndmul2  20047  omndmul3  20048  srgbinomlem3  20148  srgbinomlem4  20149  nn0srg  21379  freshmansdream  21516  mplcoe5  21980  mhpmulcl  22069  mhppwdeg  22070  psdmplcl  22082  psdmul  22086  coe1tmmul2  22195  coe1tmmul2fv  22197  coe1pwmulfv  22199  mbfi1fseqlem3  25651  dvn2bss  25865  itgpowd  25990  tdeglem4  25998  tdeglem2  25999  mdegmullem  26016  coe1mul3  26037  ply1divex  26075  fta1glem1  26106  plyaddlem1  26151  plymullem1  26152  coeeulem  26162  coemulc  26193  dgrmulc  26210  dgrcolem2  26213  dgrco  26214  dvply1  26224  dvply2g  26225  dvply2gOLD  26226  plydivlem4  26237  fta1lem  26248  vieta1lem1  26251  aareccl  26267  aaliou3lem8  26286  taylply2  26308  taylply2OLD  26309  dvtaylp  26311  dvntaylp  26312  dvntaylp0  26313  dvradcnv  26363  pserdvlem2  26371  advlogexp  26597  cxpeq  26700  atantayl3  26882  birthdaylem2  26895  harmonicbnd4  26954  dmgmaddnn0  26970  lgamucov  26981  wilthlem2  27012  basellem2  27025  basellem3  27026  basellem5  27028  0sgm  27087  sgmppw  27141  chtublem  27155  chpval2  27162  sumdchr2  27214  bcp1ctr  27223  lgslem1  27241  gausslemma2dlem6  27316  gausslemma2d  27318  lgseisenlem2  27320  lgseisenlem3  27321  lgsquadlem1  27324  lgsquadlem2  27325  lgsquad2lem2  27329  m1lgs  27332  2lgslem1c  27337  2lgslem3a  27340  2lgslem3b  27341  2lgslem3c  27342  2lgslem3d  27343  2sqlem8  27370  2sq2  27377  2sqmod  27380  dchrisumlem1  27433  dchrisum0flblem2  27453  rpvmasum2  27456  mulogsumlem  27475  selberg2lem  27494  pntrsumo1  27509  pntrlog2bndlem4  27524  finsumvtxdg2ssteplem4  29529  vtxdgoddnumeven  29534  wlklenvm1  29602  wlklenvclwlk  29634  crctcshlem4  29800  crctcsh  29804  wlklnwwlkln2lem  29862  wlknwwlksnbij  29868  wwlksnred  29872  wwlksnext  29873  wwlksnextbi  29874  wwlksnredwwlkn  29875  wwlksnextproplem2  29890  rusgrnumwwlks  29954  rusgrnumwwlk  29955  clwwlkccatlem  29968  clwlkclwwlk  29981  clwwlkwwlksb  30033  eupth2lem3lem3  30209  eupth2lem3lem6  30212  fusgreghash2wsp  30317  frrusgrord0lem  30318  numclwwlk1  30340  numclwwlk3  30364  ex-lcm  30437  ex-ind-dvds  30440  nnmulge  32712  elq2  32786  divnumden2  32790  ccatf1  32920  pfxlsw2ccat  32922  ccatws1f1o  32923  wrdt2ind  32925  cycpmco2lem2  33099  cycpmco2lem3  33100  cycpmco2lem4  33101  cycpmco2lem5  33102  cycpmco2lem6  33103  cycpmco2lem7  33104  cycpmco2  33105  archiabllem1a  33160  ply1dg3rt0irred  33544  iconstr  33749  cos9thpiminplylem1  33765  oddpwdc  34338  eulerpartlemsv2  34342  eulerpartlems  34344  eulerpartlemsv3  34345  eulerpartlemv  34348  eulerpartlemb  34352  iwrdsplit  34371  ballotlemgun  34509  ccatmulgnn0dir  34526  ofcccat  34527  signsplypnf  34534  signslema  34546  signstfvn  34553  signstfveq0  34561  signsvtp  34567  signsvtn  34568  signlem0  34571  signshf  34572  fsum2dsub  34591  hashreprin  34604  breprexp  34617  circlemeth  34624  lpadlem2  34664  lpadlen2  34665  revpfxsfxrev  35096  revwlk  35105  subfacp1lem6  35165  subfacval2  35167  subfaclim  35168  cvmliftlem7  35271  elmrsubrn  35500  bcprod  35718  bccolsum  35719  faclimlem1  35723  faclim2  35728  fwddifnp1  36146  knoppndvlem6  36498  knoppndvlem14  36506  poimirlem4  37611  poimirlem5  37612  poimirlem6  37613  poimirlem7  37614  poimirlem10  37617  poimirlem11  37618  poimirlem12  37619  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem22  37629  poimirlem24  37631  poimirlem25  37632  poimirlem29  37636  poimirlem31  37638  lcmineqlem1  42010  lcmineqlem2  42011  lcmineqlem12  42021  lcmineqlem17  42026  primrootscoprmpow  42080  aks6d1c2p2  42100  deg1gprod  42121  deg1pow  42122  2np3bcnp1  42125  2ap1caineq  42126  sticksstones7  42133  sticksstones9  42135  sticksstones10  42136  sticksstones11  42137  sticksstones12a  42138  sticksstones12  42139  sticksstones22  42149  aks6d1c6lem1  42151  aks6d1c6lem3  42153  bcled  42159  bcle2d  42160  aks6d1c7lem1  42161  unitscyglem2  42177  unitscyglem4  42179  ccatcan2d  42232  fz1sump1  42291  sumcubes  42294  zaddcomlem  42444  frlmvscadiccat  42487  fltnltalem  42643  3cubeslem3l  42667  3cubeslem3r  42668  rmxyneg  42902  rmxyadd  42903  rmyp1  42915  rmxm1  42916  rmym1  42917  rmxluc  42918  rmyluc  42919  rmxdbl  42921  rmydbl  42922  jm2.18  42970  jm2.19lem1  42971  jm2.19lem2  42972  jm2.22  42977  jm2.23  42978  jm2.25  42981  jm2.27c  42989  rmxdiophlem  42997  expdioph  43005  hbtlem4  43108  relexpmulg  43692  radcnvrat  44296  nzprmdif  44301  bcc0  44322  bccp1k  44323  bccbc  44327  binomcxplemnn0  44331  binomcxplemrat  44332  binomcxplemfrat  44333  binomcxplemnotnn0  44338  fzisoeu  45291  mccllem  45588  dvxpaek  45931  dvnxpaek  45933  dvnmul  45934  dvnprodlem1  45937  dvnprodlem2  45938  stoweidlem24  46015  stirlinglem3  46067  stirlinglem7  46071  fourierdlem36  46134  fourierdlem47  46144  etransclem23  46248  etransclem32  46257  etransclem48  46273  fz0addcom  47311  fmtnom1nn  47526  fmtnof1  47529  fmtnorec1  47531  sqrtpwpw2p  47532  fmtnorec2lem  47536  fmtnorec3  47542  fmtnofac2lem  47562  fmtnofac2  47563  fmtnofac1  47564  lighneallem3  47601  lighneallem4b  47603  altgsumbc  48333  altgsumbcALT  48334  nnpw2pmod  48565  dignn0ehalf  48599  nn0sumshdiglemA  48601  nn0sumshdiglemB  48602  nn0sumshdiglem2  48604  nn0mullong  48607  itcovalpclem2  48653  itcovalt2lem2lem2  48656  itcovalt2lem1  48657  aacllem  49783