Theorem nn0cnd 12512

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11073  ℕ₀cn0 12449

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-i2m1 11143  ax-1ne0 11144  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-nn 12194  df-n0 12450

This theorem is referenced by:  quoremnn0ALT  13826  expaddzlem  14077  expaddz  14078  expmulz  14080  facdiv  14259  faclbnd4lem3  14267  bcp1n  14288  bcn2m1  14296  bcn2p1  14297  hashgadd  14349  hashdom  14351  hashun3  14356  hashssdif  14384  hashdifpr  14387  hashxplem  14405  hashmap  14407  hashreshashfun  14411  hashbclem  14424  hashf1lem2  14428  hashf1  14429  ccatval3  14551  ccatval21sw  14557  ccatlid  14558  ccatrid  14559  ccatass  14560  ccatrn  14561  lswccatn0lsw  14563  ccatalpha  14565  ccatws1lenp1b  14593  wrdlenccats1lenm1  14594  ccats1val2  14599  swrdccat2  14641  pfxfv  14654  addlenpfx  14663  pfxtrcfvl  14669  pfxpfx  14680  ccats1pfxeq  14686  ccatopth2  14689  cats1un  14693  swrdccat3b  14712  spllen  14726  splfv2a  14728  revccat  14738  cshwlen  14771  cshwidxmod  14775  repswcshw  14784  2cshwid  14786  cshweqdif2  14791  relexpaddg  15026  rtrclreclem3  15033  isercoll2  15642  iseraltlem3  15657  hash2iun1dif1  15797  binomlem  15802  bcxmas  15808  incexclem  15809  incexc  15810  incexc2  15811  climcndslem1  15822  climcndslem2  15823  arisum  15833  arisum2  15834  pwdif  15841  geomulcvg  15849  mertens  15859  risefacval2  15983  fallfacval2  15984  fallfacval3  15985  risefallfac  15997  risefacp1  16002  fallfacp1  16003  fallfacfwd  16009  binomfallfaclem1  16012  binomfallfaclem2  16013  binomrisefac  16015  bpolycl  16025  bpolysum  16026  bpolydiflem  16027  fsumkthpow  16029  bpoly4  16032  effsumlt  16086  dvdsexp  16305  nn0ob  16361  divalgmod  16383  bitsinv1lem  16418  sadcp1  16432  sadcaddlem  16434  sadadd2lem  16436  sadadd3  16438  sadaddlem  16443  sadasslem  16447  smupp1  16457  smumullem  16469  mulgcd  16525  absmulgcd  16526  mulgcdr  16527  gcddiv  16528  lcmgcd  16584  lcmid  16586  lcm1  16587  3lcm2e6woprm  16592  6lcm4e12  16593  mulgcddvds  16632  qredeu  16635  divgcdcoprm0  16642  divgcdcoprmex  16643  cncongr1  16644  cncongr2  16645  odzdvds  16773  powm2modprm  16781  coprimeprodsq  16786  pceulem  16823  pczpre  16825  pcqmul  16831  pcaddlem  16866  pcmpt  16870  pcmpt2  16871  sumhash  16874  oddprmdvds  16881  mul4sq  16932  4sqlem12  16934  vdwapun  16952  vdwlem2  16960  vdwlem3  16961  vdwlem6  16964  vdwlem8  16966  vdwlem9  16967  ramub1lem2  17005  ramcl  17007  mulgnn0dir  19043  mulgnn0ass  19049  lagsubg2  19133  psgnunilem2  19432  odmodnn0  19477  odmulg  19493  odmulgeq  19494  odinv  19498  sylow1lem1  19535  sylow2a  19556  sylow2blem3  19559  sylow3lem3  19566  sylow3lem4  19567  efginvrel2  19664  efgsval2  19670  efgsp1  19674  efgredlemg  19679  efgredleme  19680  efgcpbllemb  19692  odadd2  19786  odadd  19787  torsubg  19791  frgpnabllem1  19810  pgpfaclem1  20020  fincygsubgodd  20051  srgbinomlem3  20144  srgbinomlem4  20145  nn0srg  21361  freshmansdream  21491  mplcoe5  21954  mhpmulcl  22043  mhppwdeg  22044  psdmplcl  22056  psdmul  22060  coe1tmmul2  22169  coe1tmmul2fv  22171  coe1pwmulfv  22173  mbfi1fseqlem3  25625  dvn2bss  25839  itgpowd  25964  tdeglem4  25972  tdeglem2  25973  mdegmullem  25990  coe1mul3  26011  ply1divex  26049  fta1glem1  26080  plyaddlem1  26125  plymullem1  26126  coeeulem  26136  coemulc  26167  dgrmulc  26184  dgrcolem2  26187  dgrco  26188  dvply1  26198  dvply2g  26199  dvply2gOLD  26200  plydivlem4  26211  fta1lem  26222  vieta1lem1  26225  aareccl  26241  aaliou3lem8  26260  taylply2  26282  taylply2OLD  26283  dvtaylp  26285  dvntaylp  26286  dvntaylp0  26287  dvradcnv  26337  pserdvlem2  26345  advlogexp  26571  cxpeq  26674  atantayl3  26856  birthdaylem2  26869  harmonicbnd4  26928  dmgmaddnn0  26944  lgamucov  26955  wilthlem2  26986  basellem2  26999  basellem3  27000  basellem5  27002  0sgm  27061  sgmppw  27115  chtublem  27129  chpval2  27136  sumdchr2  27188  bcp1ctr  27197  lgslem1  27215  gausslemma2dlem6  27290  gausslemma2d  27292  lgseisenlem2  27294  lgseisenlem3  27295  lgsquadlem1  27298  lgsquadlem2  27299  lgsquad2lem2  27303  m1lgs  27306  2lgslem1c  27311  2lgslem3a  27314  2lgslem3b  27315  2lgslem3c  27316  2lgslem3d  27317  2sqlem8  27344  2sq2  27351  2sqmod  27354  dchrisumlem1  27407  dchrisum0flblem2  27427  rpvmasum2  27430  mulogsumlem  27449  selberg2lem  27468  pntrsumo1  27483  pntrlog2bndlem4  27498  finsumvtxdg2ssteplem4  29483  vtxdgoddnumeven  29488  wlklenvm1  29557  wlklenvclwlk  29590  crctcshlem4  29757  crctcsh  29761  wlklnwwlkln2lem  29819  wlknwwlksnbij  29825  wwlksnred  29829  wwlksnext  29830  wwlksnextbi  29831  wwlksnredwwlkn  29832  wwlksnextproplem2  29847  rusgrnumwwlks  29911  rusgrnumwwlk  29912  clwwlkccatlem  29925  clwlkclwwlk  29938  clwwlkwwlksb  29990  eupth2lem3lem3  30166  eupth2lem3lem6  30169  fusgreghash2wsp  30274  frrusgrord0lem  30275  numclwwlk1  30297  numclwwlk3  30321  ex-lcm  30394  ex-ind-dvds  30397  nnmulge  32669  elq2  32743  divnumden2  32747  ccatf1  32877  pfxlsw2ccat  32879  ccatws1f1o  32880  wrdt2ind  32882  omndmul2  33033  omndmul3  33034  cycpmco2lem2  33091  cycpmco2lem3  33092  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2lem7  33096  cycpmco2  33097  archiabllem1a  33152  ply1dg3rt0irred  33558  iconstr  33763  cos9thpiminplylem1  33779  oddpwdc  34352  eulerpartlemsv2  34356  eulerpartlems  34358  eulerpartlemsv3  34359  eulerpartlemv  34362  eulerpartlemb  34366  iwrdsplit  34385  ballotlemgun  34523  ccatmulgnn0dir  34540  ofcccat  34541  signsplypnf  34548  signslema  34560  signstfvn  34567  signstfveq0  34575  signsvtp  34581  signsvtn  34582  signlem0  34585  signshf  34586  fsum2dsub  34605  hashreprin  34618  breprexp  34631  circlemeth  34638  lpadlem2  34678  lpadlen2  34679  revpfxsfxrev  35110  revwlk  35119  subfacp1lem6  35179  subfacval2  35181  subfaclim  35182  cvmliftlem7  35285  elmrsubrn  35514  bcprod  35732  bccolsum  35733  faclimlem1  35737  faclim2  35742  fwddifnp1  36160  knoppndvlem6  36512  knoppndvlem14  36520  poimirlem4  37625  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem22  37643  poimirlem24  37645  poimirlem25  37646  poimirlem29  37650  poimirlem31  37652  lcmineqlem1  42024  lcmineqlem2  42025  lcmineqlem12  42035  lcmineqlem17  42040  primrootscoprmpow  42094  aks6d1c2p2  42114  deg1gprod  42135  deg1pow  42136  2np3bcnp1  42139  2ap1caineq  42140  sticksstones7  42147  sticksstones9  42149  sticksstones10  42150  sticksstones11  42151  sticksstones12a  42152  sticksstones12  42153  sticksstones22  42163  aks6d1c6lem1  42165  aks6d1c6lem3  42167  bcled  42173  bcle2d  42174  aks6d1c7lem1  42175  unitscyglem2  42191  unitscyglem4  42193  ccatcan2d  42246  fz1sump1  42305  sumcubes  42308  zaddcomlem  42458  frlmvscadiccat  42501  fltnltalem  42657  3cubeslem3l  42681  3cubeslem3r  42682  rmxyneg  42916  rmxyadd  42917  rmyp1  42929  rmxm1  42930  rmym1  42931  rmxluc  42932  rmyluc  42933  rmxdbl  42935  rmydbl  42936  jm2.18  42984  jm2.19lem1  42985  jm2.19lem2  42986  jm2.22  42991  jm2.23  42992  jm2.25  42995  jm2.27c  43003  rmxdiophlem  43011  expdioph  43019  hbtlem4  43122  relexpmulg  43706  radcnvrat  44310  nzprmdif  44315  bcc0  44336  bccp1k  44337  bccbc  44341  binomcxplemnn0  44345  binomcxplemrat  44346  binomcxplemfrat  44347  binomcxplemnotnn0  44352  fzisoeu  45305  mccllem  45602  dvxpaek  45945  dvnxpaek  45947  dvnmul  45948  dvnprodlem1  45951  dvnprodlem2  45952  stoweidlem24  46029  stirlinglem3  46081  stirlinglem7  46085  fourierdlem36  46148  fourierdlem47  46158  etransclem23  46262  etransclem32  46271  etransclem48  46287  fz0addcom  47322  fmtnom1nn  47537  fmtnof1  47540  fmtnorec1  47542  sqrtpwpw2p  47543  fmtnorec2lem  47547  fmtnorec3  47553  fmtnofac2lem  47573  fmtnofac2  47574  fmtnofac1  47575  lighneallem3  47612  lighneallem4b  47614  altgsumbc  48344  altgsumbcALT  48345  nnpw2pmod  48576  dignn0ehalf  48610  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613  nn0sumshdiglem2  48615  nn0mullong  48618  itcovalpclem2  48664  itcovalt2lem2lem2  48667  itcovalt2lem1  48668  aacllem  49794