Theorem nn0cnd 12476

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  ℕ₀cn0 12413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  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 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-nn 12158  df-n0 12414

This theorem is referenced by:  quoremnn0ALT  13789  expaddzlem  14040  expaddz  14041  expmulz  14043  facdiv  14222  faclbnd4lem3  14230  bcp1n  14251  bcn2m1  14259  bcn2p1  14260  hashgadd  14312  hashdom  14314  hashun3  14319  hashssdif  14347  hashdifpr  14350  hashxplem  14368  hashmap  14370  hashreshashfun  14374  hashbclem  14387  hashf1lem2  14391  hashf1  14392  ccatval3  14514  ccatval21sw  14521  ccatlid  14522  ccatrid  14523  ccatass  14524  ccatrn  14525  lswccatn0lsw  14527  ccatalpha  14529  ccatws1lenp1b  14557  wrdlenccats1lenm1  14558  ccats1val2  14563  swrdccat2  14605  pfxfv  14618  addlenpfx  14626  pfxtrcfvl  14632  pfxpfx  14643  lenrevpfxcctswrd  14647  ccats1pfxeq  14649  ccatopth2  14652  cats1un  14656  swrdccat3b  14675  spllen  14689  splfv2a  14691  revccat  14701  cshwlen  14734  cshwidxmod  14738  repswcshw  14747  2cshwid  14749  cshweqdif2  14754  relexpaddg  14988  rtrclreclem3  14995  isercoll2  15604  iseraltlem3  15619  hash2iun1dif1  15759  binomlem  15764  bcxmas  15770  incexclem  15771  incexc  15772  incexc2  15773  climcndslem1  15784  climcndslem2  15785  arisum  15795  arisum2  15796  pwdif  15803  geomulcvg  15811  mertens  15821  risefacval2  15945  fallfacval2  15946  fallfacval3  15947  risefallfac  15959  risefacp1  15964  fallfacp1  15965  fallfacfwd  15971  binomfallfaclem1  15974  binomfallfaclem2  15975  binomrisefac  15977  bpolycl  15987  bpolysum  15988  bpolydiflem  15989  fsumkthpow  15991  bpoly4  15994  effsumlt  16048  dvdsexp  16267  nn0ob  16323  divalgmod  16345  bitsinv1lem  16380  sadcp1  16394  sadcaddlem  16396  sadadd2lem  16398  sadadd3  16400  sadaddlem  16405  sadasslem  16409  smupp1  16419  smumullem  16431  mulgcd  16487  absmulgcd  16488  mulgcdr  16489  gcddiv  16490  lcmgcd  16546  lcmid  16548  lcm1  16549  3lcm2e6woprm  16554  6lcm4e12  16555  mulgcddvds  16594  qredeu  16597  divgcdcoprm0  16604  divgcdcoprmex  16605  cncongr1  16606  cncongr2  16607  odzdvds  16735  powm2modprm  16743  coprimeprodsq  16748  pceulem  16785  pczpre  16787  pcqmul  16793  pcaddlem  16828  pcmpt  16832  pcmpt2  16833  sumhash  16836  oddprmdvds  16843  mul4sq  16894  4sqlem12  16896  vdwapun  16914  vdwlem2  16922  vdwlem3  16923  vdwlem6  16926  vdwlem8  16928  vdwlem9  16929  ramub1lem2  16967  ramcl  16969  chnrev  18562  mulgnn0dir  19046  mulgnn0ass  19052  lagsubg2  19135  psgnunilem2  19436  odmodnn0  19481  odmulg  19497  odmulgeq  19498  odinv  19502  sylow1lem1  19539  sylow2a  19560  sylow2blem3  19563  sylow3lem3  19570  sylow3lem4  19571  efginvrel2  19668  efgsval2  19674  efgsp1  19678  efgredlemg  19683  efgredleme  19684  efgcpbllemb  19696  odadd2  19790  odadd  19791  torsubg  19795  frgpnabllem1  19814  pgpfaclem1  20024  fincygsubgodd  20055  omndmul2  20074  omndmul3  20075  srgbinomlem3  20175  srgbinomlem4  20176  nn0srg  21404  freshmansdream  21541  mplcoe5  22007  mhpmulcl  22104  mhppwdeg  22105  psdmplcl  22117  psdmul  22121  coe1tmmul2  22230  coe1tmmul2fv  22232  coe1pwmulfv  22234  mbfi1fseqlem3  25686  dvn2bss  25900  itgpowd  26025  tdeglem4  26033  tdeglem2  26034  mdegmullem  26051  coe1mul3  26072  ply1divex  26110  fta1glem1  26141  plyaddlem1  26186  plymullem1  26187  coeeulem  26197  coemulc  26228  dgrmulc  26245  dgrcolem2  26248  dgrco  26249  dvply1  26259  dvply2g  26260  dvply2gOLD  26261  plydivlem4  26272  fta1lem  26283  vieta1lem1  26286  aareccl  26302  aaliou3lem8  26321  taylply2  26343  taylply2OLD  26344  dvtaylp  26346  dvntaylp  26347  dvntaylp0  26348  dvradcnv  26398  pserdvlem2  26406  advlogexp  26632  cxpeq  26735  atantayl3  26917  birthdaylem2  26930  harmonicbnd4  26989  dmgmaddnn0  27005  lgamucov  27016  wilthlem2  27047  basellem2  27060  basellem3  27061  basellem5  27063  0sgm  27122  sgmppw  27176  chtublem  27190  chpval2  27197  sumdchr2  27249  bcp1ctr  27258  lgslem1  27276  gausslemma2dlem6  27351  gausslemma2d  27353  lgseisenlem2  27355  lgseisenlem3  27356  lgsquadlem1  27359  lgsquadlem2  27360  lgsquad2lem2  27364  m1lgs  27367  2lgslem1c  27372  2lgslem3a  27375  2lgslem3b  27376  2lgslem3c  27377  2lgslem3d  27378  2sqlem8  27405  2sq2  27412  2sqmod  27415  dchrisumlem1  27468  dchrisum0flblem2  27488  rpvmasum2  27491  mulogsumlem  27510  selberg2lem  27529  pntrsumo1  27544  pntrlog2bndlem4  27559  finsumvtxdg2ssteplem4  29634  vtxdgoddnumeven  29639  wlklenvm1  29707  wlklenvclwlk  29739  crctcshlem4  29905  crctcsh  29909  wlklnwwlkln2lem  29967  wlknwwlksnbij  29973  wwlksnred  29977  wwlksnext  29978  wwlksnextbi  29979  wwlksnredwwlkn  29980  wwlksnextproplem2  29995  rusgrnumwwlks  30062  rusgrnumwwlk  30063  clwwlkccatlem  30076  clwlkclwwlk  30089  clwwlkwwlksb  30141  eupth2lem3lem3  30317  eupth2lem3lem6  30320  fusgreghash2wsp  30425  frrusgrord0lem  30426  numclwwlk1  30448  numclwwlk3  30472  ex-lcm  30545  ex-ind-dvds  30548  nnmulge  32829  elq2  32903  divnumden2  32907  ccatf1  33042  pfxlsw2ccat  33043  ccatws1f1o  33044  wrdt2ind  33046  gsummptrev  33150  gsummptp1  33151  gsummulsubdishift1  33162  cycpmco2lem2  33221  cycpmco2lem3  33222  cycpmco2lem4  33223  cycpmco2lem5  33224  cycpmco2lem6  33225  cycpmco2lem7  33226  cycpmco2  33227  archiabllem1a  33285  gsumind  33438  deg1prod  33676  ply1dg3rt0irred  33677  esplyind  33752  esplyindfv  33753  esplyfvn  33754  vietadeg1  33755  vietalem  33756  vieta  33757  iconstr  33944  cos9thpiminplylem1  33960  oddpwdc  34532  eulerpartlemsv2  34536  eulerpartlems  34538  eulerpartlemsv3  34539  eulerpartlemv  34542  eulerpartlemb  34546  iwrdsplit  34565  ballotlemgun  34703  ccatmulgnn0dir  34720  ofcccat  34721  signsplypnf  34728  signslema  34740  signstfvn  34747  signstfveq0  34755  signsvtp  34761  signsvtn  34762  signlem0  34765  signshf  34766  fsum2dsub  34785  hashreprin  34798  breprexp  34811  circlemeth  34818  lpadlem2  34858  lpadlen2  34859  revpfxsfxrev  35332  revwlk  35341  subfacp1lem6  35401  subfacval2  35403  subfaclim  35404  cvmliftlem7  35507  elmrsubrn  35736  bcprod  35954  bccolsum  35955  faclimlem1  35959  faclim2  35964  fwddifnp1  36381  knoppndvlem6  36739  knoppndvlem14  36747  poimirlem4  37875  poimirlem5  37876  poimirlem6  37877  poimirlem7  37878  poimirlem10  37881  poimirlem11  37882  poimirlem12  37883  poimirlem16  37887  poimirlem17  37888  poimirlem19  37890  poimirlem20  37891  poimirlem22  37893  poimirlem24  37895  poimirlem25  37896  poimirlem29  37900  poimirlem31  37902  lcmineqlem1  42399  lcmineqlem2  42400  lcmineqlem12  42410  lcmineqlem17  42415  primrootscoprmpow  42469  aks6d1c2p2  42489  deg1gprod  42510  deg1pow  42511  2np3bcnp1  42514  2ap1caineq  42515  sticksstones7  42522  sticksstones9  42524  sticksstones10  42525  sticksstones11  42526  sticksstones12a  42527  sticksstones12  42528  sticksstones22  42538  aks6d1c6lem1  42540  aks6d1c6lem3  42542  bcled  42548  bcle2d  42549  aks6d1c7lem1  42550  unitscyglem2  42566  unitscyglem4  42568  ccatcan2d  42621  fz1sump1  42680  sumcubes  42683  zaddcomlem  42833  frlmvscadiccat  42876  fltnltalem  43020  3cubeslem3l  43043  3cubeslem3r  43044  rmxyneg  43277  rmxyadd  43278  rmyp1  43290  rmxm1  43291  rmym1  43292  rmxluc  43293  rmyluc  43294  rmxdbl  43296  rmydbl  43297  jm2.18  43345  jm2.19lem1  43346  jm2.19lem2  43347  jm2.22  43352  jm2.23  43353  jm2.25  43356  jm2.27c  43364  rmxdiophlem  43372  expdioph  43380  hbtlem4  43483  relexpmulg  44066  radcnvrat  44670  nzprmdif  44675  bcc0  44696  bccp1k  44697  bccbc  44701  binomcxplemnn0  44705  binomcxplemrat  44706  binomcxplemfrat  44707  binomcxplemnotnn0  44712  fzisoeu  45662  mccllem  45957  dvxpaek  46298  dvnxpaek  46300  dvnmul  46301  dvnprodlem1  46304  dvnprodlem2  46305  stoweidlem24  46382  stirlinglem3  46434  stirlinglem7  46438  fourierdlem36  46501  fourierdlem47  46511  etransclem23  46615  etransclem32  46624  etransclem48  46640  fz0addcom  47677  fmtnom1nn  47892  fmtnof1  47895  fmtnorec1  47897  sqrtpwpw2p  47898  fmtnorec2lem  47902  fmtnorec3  47908  fmtnofac2lem  47928  fmtnofac2  47929  fmtnofac1  47930  lighneallem3  47967  lighneallem4b  47969  altgsumbc  48712  altgsumbcALT  48713  nnpw2pmod  48943  dignn0ehalf  48977  nn0sumshdiglemA  48979  nn0sumshdiglemB  48980  nn0sumshdiglem2  48982  nn0mullong  48985  itcovalpclem2  49031  itcovalt2lem2lem2  49034  itcovalt2lem1  49035  aacllem  50160