Theorem nn0cnd 12434

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 11008  ℕ₀cn0 12372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-sep 5255  ax-nul 5262  ax-pr 5383  ax-un 7665  ax-resscn 11067  ax-1cn 11068  ax-icn 11069  ax-addcl 11070  ax-addrcl 11071  ax-mulcl 11072  ax-mulrcl 11073  ax-i2m1 11078  ax-1ne0 11079  ax-rnegex 11081  ax-rrecex 11082  ax-cnre 11083

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-ral 3064  df-rex 3073  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-iun 4955  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5530  df-eprel 5536  df-po 5544  df-so 5545  df-fr 5587  df-we 5589  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6252  df-ord 6319  df-on 6320  df-lim 6321  df-suc 6322  df-iota 6446  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-ov 7355  df-om 7796  df-2nd 7915  df-frecs 8205  df-wrecs 8236  df-recs 8310  df-rdg 8349  df-nn 12113  df-n0 12373

This theorem is referenced by:  quoremnn0ALT  13717  expaddzlem  13966  expaddz  13967  expmulz  13969  facdiv  14141  faclbnd4lem3  14149  bcp1n  14170  bcn2m1  14178  bcn2p1  14179  hashgadd  14231  hashdom  14233  hashun3  14238  hashssdif  14266  hashdifpr  14269  hashxplem  14287  hashmap  14289  hashreshashfun  14293  hashbclem  14303  hashf1lem2  14309  hashf1  14310  ccatval3  14421  ccatval21sw  14427  ccatlid  14428  ccatrid  14429  ccatass  14430  ccatrn  14431  lswccatn0lsw  14433  ccatalpha  14435  ccatws1lenp1b  14463  wrdlenccats1lenm1  14464  ccats1val2  14469  swrdccat2  14515  pfxfv  14528  addlenpfx  14537  pfxtrcfvl  14543  pfxpfx  14554  ccats1pfxeq  14560  ccatopth2  14563  cats1un  14567  swrdccat3b  14586  spllen  14600  splfv2a  14602  revccat  14612  cshwlen  14645  cshwidxmod  14649  repswcshw  14658  2cshwid  14660  cshweqdif2  14665  relexpaddg  14898  rtrclreclem3  14905  isercoll2  15513  iseraltlem3  15528  hash2iun1dif1  15669  binomlem  15674  bcxmas  15680  incexclem  15681  incexc  15682  incexc2  15683  climcndslem1  15694  climcndslem2  15695  arisum  15705  arisum2  15706  pwdif  15713  geomulcvg  15721  mertens  15731  risefacval2  15853  fallfacval2  15854  fallfacval3  15855  risefallfac  15867  risefacp1  15872  fallfacp1  15873  fallfacfwd  15879  binomfallfaclem1  15882  binomfallfaclem2  15883  binomrisefac  15885  bpolycl  15895  bpolysum  15896  bpolydiflem  15897  fsumkthpow  15899  bpoly4  15902  effsumlt  15953  dvdsexp  16170  nn0ob  16226  divalgmod  16248  bitsinv1lem  16281  sadcp1  16295  sadcaddlem  16297  sadadd2lem  16299  sadadd3  16301  sadaddlem  16306  sadasslem  16310  smupp1  16320  smumullem  16332  mulgcd  16389  absmulgcd  16390  mulgcdr  16391  gcddiv  16392  lcmgcd  16443  lcmid  16445  lcm1  16446  3lcm2e6woprm  16451  6lcm4e12  16452  mulgcddvds  16491  qredeu  16494  divgcdcoprm0  16501  divgcdcoprmex  16502  cncongr1  16503  cncongr2  16504  odzdvds  16627  powm2modprm  16635  coprimeprodsq  16640  pceulem  16677  pczpre  16679  pcqmul  16685  pcaddlem  16720  pcmpt  16724  pcmpt2  16725  sumhash  16728  oddprmdvds  16735  mul4sq  16786  4sqlem12  16788  vdwapun  16806  vdwlem2  16814  vdwlem3  16815  vdwlem6  16818  vdwlem8  16820  vdwlem9  16821  ramub1lem2  16859  ramcl  16861  mulgnn0dir  18865  mulgnn0ass  18871  lagsubg2  18950  psgnunilem2  19236  odmodnn0  19281  odmulg  19297  odmulgeq  19298  odinv  19302  sylow1lem1  19339  sylow2a  19360  sylow2blem3  19363  sylow3lem3  19370  sylow3lem4  19371  efginvrel2  19468  efgsval2  19474  efgsp1  19478  efgredlemg  19483  efgredleme  19484  efgcpbllemb  19496  odadd2  19586  odadd  19587  torsubg  19591  frgpnabllem1  19610  pgpfaclem1  19819  fincygsubgodd  19850  srgbinomlem3  19913  srgbinomlem4  19914  nn0srg  20820  mplcoe5  21393  mhpmulcl  21491  mhppwdeg  21492  coe1tmmul2  21599  coe1tmmul2fv  21601  coe1pwmulfv  21603  mbfi1fseqlem3  25034  dvn2bss  25246  itgpowd  25366  tdeglem4  25376  tdeglem4OLD  25377  tdeglem2  25378  mdegmullem  25395  coe1mul3  25416  ply1divex  25453  fta1glem1  25482  plyaddlem1  25526  plymullem1  25527  coeeulem  25537  coemulc  25568  dgrmulc  25584  dgrcolem2  25587  dgrco  25588  dvply1  25596  dvply2g  25597  plydivlem4  25608  fta1lem  25619  vieta1lem1  25622  aareccl  25638  aaliou3lem8  25657  taylply2  25679  dvtaylp  25681  dvntaylp  25682  dvntaylp0  25683  dvradcnv  25732  pserdvlem2  25739  advlogexp  25962  cxpeq  26062  atantayl3  26241  birthdaylem2  26254  harmonicbnd4  26312  dmgmaddnn0  26328  lgamucov  26339  wilthlem2  26370  basellem2  26383  basellem3  26384  basellem5  26386  0sgm  26445  sgmppw  26497  chtublem  26511  chpval2  26518  sumdchr2  26570  bcp1ctr  26579  lgslem1  26597  gausslemma2dlem6  26672  gausslemma2d  26674  lgseisenlem2  26676  lgseisenlem3  26677  lgsquadlem1  26680  lgsquadlem2  26681  lgsquad2lem2  26685  m1lgs  26688  2lgslem1c  26693  2lgslem3a  26696  2lgslem3b  26697  2lgslem3c  26698  2lgslem3d  26699  2sqlem8  26726  2sq2  26733  2sqmod  26736  dchrisumlem1  26789  dchrisum0flblem2  26809  rpvmasum2  26812  mulogsumlem  26831  selberg2lem  26850  pntrsumo1  26865  pntrlog2bndlem4  26880  finsumvtxdg2ssteplem4  28325  vtxdgoddnumeven  28330  wlklenvm1  28399  wlklenvclwlk  28432  crctcshlem4  28594  crctcsh  28598  wlklnwwlkln2lem  28656  wlknwwlksnbij  28662  wwlksnred  28666  wwlksnext  28667  wwlksnextbi  28668  wwlksnredwwlkn  28669  wwlksnextproplem2  28684  rusgrnumwwlks  28748  rusgrnumwwlk  28749  clwwlkccatlem  28762  clwlkclwwlk  28775  clwwlkwwlksb  28827  eupth2lem3lem3  29003  eupth2lem3lem6  29006  fusgreghash2wsp  29111  frrusgrord0lem  29112  numclwwlk1  29134  numclwwlk3  29158  ex-lcm  29231  ex-ind-dvds  29234  nnmulge  31480  divnumden2  31539  ccatf1  31630  pfxlsw2ccat  31631  wrdt2ind  31632  omndmul2  31745  omndmul3  31746  cycpmco2lem2  31801  cycpmco2lem3  31802  cycpmco2lem4  31803  cycpmco2lem5  31804  cycpmco2lem6  31805  cycpmco2lem7  31806  cycpmco2  31807  archiabllem1a  31852  freshmansdream  31891  oddpwdc  32758  eulerpartlemsv2  32762  eulerpartlems  32764  eulerpartlemsv3  32765  eulerpartlemv  32768  eulerpartlemb  32772  iwrdsplit  32791  ballotlemgun  32928  ccatmulgnn0dir  32958  ofcccat  32959  signsplypnf  32966  signslema  32978  signstfvn  32985  signstfveq0  32993  signsvtp  32999  signsvtn  33000  signlem0  33003  signshf  33004  fsum2dsub  33024  hashreprin  33037  breprexp  33050  circlemeth  33057  lpadlem2  33097  lpadlen2  33098  revpfxsfxrev  33513  revwlk  33522  subfacp1lem6  33583  subfacval2  33585  subfaclim  33586  cvmliftlem7  33689  elmrsubrn  33918  bcprod  34121  bccolsum  34122  faclimlem1  34126  faclim2  34131  fwddifnp1  34682  knoppndvlem6  34912  knoppndvlem14  34920  poimirlem4  36014  poimirlem5  36015  poimirlem6  36016  poimirlem7  36017  poimirlem10  36020  poimirlem11  36021  poimirlem12  36022  poimirlem16  36026  poimirlem17  36027  poimirlem19  36029  poimirlem20  36030  poimirlem22  36032  poimirlem24  36034  poimirlem25  36035  poimirlem29  36039  poimirlem31  36041  lcmineqlem1  40418  lcmineqlem2  40419  lcmineqlem12  40429  lcmineqlem17  40434  aks6d1c2p2  40481  2np3bcnp1  40484  2ap1caineq  40485  sticksstones7  40492  sticksstones9  40494  sticksstones10  40495  sticksstones11  40496  sticksstones12a  40497  sticksstones12  40498  sticksstones22  40508  ccatcan2d  40598  frlmvscadiccat  40618  zaddcomlem  40823  fltnltalem  40903  3cubeslem3l  40912  3cubeslem3r  40913  rmxyneg  41147  rmxyadd  41148  rmyp1  41160  rmxm1  41161  rmym1  41162  rmxluc  41163  rmyluc  41164  rmxdbl  41166  rmydbl  41167  jm2.18  41215  jm2.19lem1  41216  jm2.19lem2  41217  jm2.22  41222  jm2.23  41223  jm2.25  41226  jm2.27c  41234  rmxdiophlem  41242  expdioph  41250  hbtlem4  41356  relexpmulg  41887  radcnvrat  42499  nzprmdif  42504  bcc0  42525  bccp1k  42526  bccbc  42530  binomcxplemnn0  42534  binomcxplemrat  42535  binomcxplemfrat  42536  binomcxplemnotnn0  42541  fzisoeu  43433  mccllem  43733  dvxpaek  44076  dvnxpaek  44078  dvnmul  44079  dvnprodlem1  44082  dvnprodlem2  44083  stoweidlem24  44160  stirlinglem3  44212  stirlinglem7  44216  fourierdlem36  44279  fourierdlem47  44289  etransclem23  44393  etransclem32  44402  etransclem48  44418  fz0addcom  45444  fmtnom1nn  45619  fmtnof1  45622  fmtnorec1  45624  sqrtpwpw2p  45625  fmtnorec2lem  45629  fmtnorec3  45635  fmtnofac2lem  45655  fmtnofac2  45656  fmtnofac1  45657  lighneallem3  45694  lighneallem4b  45696  altgsumbc  46323  altgsumbcALT  46324  nnpw2pmod  46564  dignn0ehalf  46598  nn0sumshdiglemA  46600  nn0sumshdiglemB  46601  nn0sumshdiglem2  46603  nn0mullong  46606  itcovalpclem2  46652  itcovalt2lem2lem2  46655  itcovalt2lem1  46656  aacllem  47143