Theorem nn0cnd 11769

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

Syntax hints:   → wi 4   ∈ wcel 2050  ℂcc 10333  ℕ₀cn0 11707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-resscn 10392  ax-1cn 10393  ax-icn 10394  ax-addcl 10395  ax-addrcl 10396  ax-mulcl 10397  ax-mulrcl 10398  ax-i2m1 10403  ax-1ne0 10404  ax-rnegex 10406  ax-rrecex 10407  ax-cnre 10408

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-reu 3095  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-pss 3845  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-ov 6979  df-om 7397  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-nn 11440  df-n0 11708

This theorem is referenced by:  quoremnn0ALT  13040  expaddzlem  13287  expaddz  13288  expmulz  13290  facdiv  13462  faclbnd4lem3  13470  bcp1n  13491  bcn2m1  13499  bcn2p1  13500  hashgadd  13551  hashdom  13553  hashun3  13558  hashssdif  13586  hashdifpr  13589  hashxplem  13607  hashmap  13609  hashreshashfun  13613  hashbclem  13623  hashf1lem2  13627  hashf1  13628  ccatval3  13742  ccatval21sw  13748  ccatlid  13749  ccatrid  13750  ccatass  13751  ccatrn  13752  lswccatn0lsw  13754  ccatalpha  13756  ccatws1lenp1b  13784  wrdlenccats1lenm1  13785  ccats1val2  13790  swrd0fOLD  13817  swrdidOLD  13818  addlenswrdOLD  13830  swrdtrcfvlOLD  13843  swrdccat2  13851  pfxfv  13864  addlenpfx  13873  pfxtrcfvl  13879  pfxpfx  13893  ccats1pfxeq  13904  ccatopth2  13909  cats1un  13914  swrdccat3b  13945  swrdccat3bOLD  13946  spllen  13969  spllenOLD  13970  splfv2a  13973  splfv2aOLD  13974  revccat  13985  cshwlen  14023  cshwidxmod  14027  repswcshw  14036  2cshwid  14038  cshweqdif2  14043  relexpaddg  14273  rtrclreclem3  14280  isercoll2  14886  iseraltlem3  14901  hash2iun1dif1  15039  binomlem  15044  bcxmas  15050  incexclem  15051  incexc  15052  incexc2  15053  climcndslem1  15064  climcndslem2  15065  arisum  15075  arisum2  15076  pwdif  15083  geomulcvg  15092  mertens  15102  risefacval2  15224  fallfacval2  15225  fallfacval3  15226  risefallfac  15238  risefacp1  15243  fallfacp1  15244  fallfacfwd  15250  binomfallfaclem1  15253  binomfallfaclem2  15254  binomrisefac  15256  bpolycl  15266  bpolysum  15267  bpolydiflem  15268  fsumkthpow  15270  bpoly4  15273  effsumlt  15324  dvdsexp  15537  nn0ob  15595  divalgmod  15617  bitsinv1lem  15650  sadcp1  15664  sadcaddlem  15666  sadadd2lem  15668  sadadd3  15670  sadaddlem  15675  sadasslem  15679  smupp1  15689  smumullem  15701  mulgcd  15752  absmulgcd  15753  mulgcdr  15754  gcddiv  15755  lcmgcd  15807  lcmid  15809  lcm1  15810  3lcm2e6woprm  15815  6lcm4e12  15816  mulgcddvds  15855  qredeu  15858  divgcdcoprm0  15865  divgcdcoprmex  15866  cncongr1  15867  cncongr2  15868  odzdvds  15988  powm2modprm  15996  coprimeprodsq  16001  pceulem  16038  pczpre  16040  pcqmul  16046  pcaddlem  16080  pcmpt  16084  pcmpt2  16085  sumhash  16088  oddprmdvds  16095  mul4sq  16146  4sqlem12  16148  vdwapun  16166  vdwlem2  16174  vdwlem3  16175  vdwlem6  16178  vdwlem8  16180  vdwlem9  16181  ramub1lem2  16219  ramcl  16221  mulgnn0dir  18041  mulgnn0ass  18047  lagsubg2  18124  psgnunilem2  18385  odmodnn0  18430  odmulg  18444  odmulgeq  18445  odinv  18449  sylow1lem1  18484  sylow2a  18505  sylow2blem3  18508  sylow3lem3  18515  sylow3lem4  18516  efginvrel2  18611  efgsval2  18617  efgsp1  18621  efgredlemg  18627  efgredleme  18628  efgcpbllemb  18641  odadd2  18725  odadd  18726  torsubg  18730  frgpnabllem1  18749  pgpfaclem1  18953  srgbinomlem3  19015  srgbinomlem4  19016  mplcoe5  19962  coe1tmmul2  20147  coe1tmmul2fv  20149  coe1pwmulfv  20151  nn0srg  20317  mbfi1fseqlem3  24021  dvn2bss  24230  tdeglem4  24357  tdeglem2  24358  mdegmullem  24375  coe1mul3  24396  ply1divex  24433  fta1glem1  24462  plyaddlem1  24506  plymullem1  24507  coeeulem  24517  coemulc  24548  dgrmulc  24564  dgrcolem2  24567  dgrco  24568  dvply1  24576  dvply2g  24577  plydivlem4  24588  fta1lem  24599  vieta1lem1  24602  aareccl  24618  aaliou3lem8  24637  taylply2  24659  dvtaylp  24661  dvntaylp  24662  dvntaylp0  24663  dvradcnv  24712  pserdvlem2  24719  advlogexp  24939  cxpeq  25039  atantayl3  25218  birthdaylem2  25232  harmonicbnd4  25290  dmgmaddnn0  25306  lgamucov  25317  wilthlem2  25348  basellem2  25361  basellem3  25362  basellem5  25364  0sgm  25423  sgmppw  25475  chtublem  25489  chpval2  25496  sumdchr2  25548  bcp1ctr  25557  lgslem1  25575  gausslemma2dlem6  25650  gausslemma2d  25652  lgseisenlem2  25654  lgseisenlem3  25655  lgsquadlem1  25658  lgsquadlem2  25659  lgsquad2lem2  25663  m1lgs  25666  2lgslem1c  25671  2lgslem3a  25674  2lgslem3b  25675  2lgslem3c  25676  2lgslem3d  25677  2sqlem8  25704  2sq2  25711  2sqmod  25714  dchrisumlem1  25767  dchrisum0flblem2  25787  rpvmasum2  25790  mulogsumlem  25809  selberg2lem  25828  pntrsumo1  25843  pntrlog2bndlem4  25858  finsumvtxdg2ssteplem4  27033  vtxdgoddnumeven  27038  wlklenvm1  27106  crctcshlem4  27306  crctcsh  27310  wlklnwwlkln2lem  27369  wlknwwlksnbij  27375  wwlksnred  27379  wwlksnredOLD  27380  wwlksnext  27381  wwlksnextbi  27382  wwlksnextbiOLD  27383  wwlksnredwwlkn  27384  wwlksnredwwlknOLD  27385  wwlksnextproplem2  27411  wwlksnextproplem2OLD  27412  rusgrnumwwlks  27480  rusgrnumwwlksOLD  27481  rusgrnumwwlk  27482  clwwlkccatlem  27495  clwlkclwwlk  27508  clwlkclwwlkOLD  27509  clwwlkwwlksb  27577  eupth2lem3lem3  27760  eupth2lem3lem6  27763  fusgreghash2wsp  27872  frrusgrord0lem  27873  numclwwlk1  27909  numclwwlk3  27942  ex-lcm  28015  ex-ind-dvds  28018  nnmulge  30233  divnumden2  30287  omndmul2  30437  omndmul3  30438  archiabllem1a  30492  freshmansdream  30544  oddpwdc  31263  eulerpartlemsv2  31267  eulerpartlems  31269  eulerpartlemsv3  31270  eulerpartlemv  31273  eulerpartlemb  31277  iwrdsplit  31296  iwrdsplitOLD  31297  ballotlemgun  31434  ccatmulgnn0dir  31464  ofcccat  31465  signsplypnf  31472  signslema  31484  signstfvn  31491  signstfveq0  31500  signstfveq0OLD  31501  signsvtp  31507  signsvtn  31508  signlem0  31511  signshf  31512  fsum2dsub  31532  hashreprin  31545  breprexp  31558  circlemeth  31565  lpadlem2  31605  lpadlen2  31606  subfacp1lem6  32023  subfacval2  32025  subfaclim  32026  cvmliftlem7  32129  elmrsubrn  32293  bcprod  32496  bccolsum  32497  faclimlem1  32501  faclim2  32506  fwddifnp1  33153  knoppndvlem6  33382  knoppndvlem14  33390  poimirlem4  34343  poimirlem5  34344  poimirlem6  34345  poimirlem7  34346  poimirlem10  34349  poimirlem11  34350  poimirlem12  34351  poimirlem16  34355  poimirlem17  34356  poimirlem19  34358  poimirlem20  34359  poimirlem22  34361  poimirlem24  34363  poimirlem25  34364  poimirlem29  34368  poimirlem31  34370  ccatcan2d  38578  frlmvscadiccat  38588  fltnltalem  38687  rmxyneg  38919  rmxyadd  38920  rmyp1  38932  rmxm1  38933  rmym1  38934  rmxluc  38935  rmyluc  38936  rmxdbl  38938  rmydbl  38939  jm2.18  38987  jm2.19lem1  38988  jm2.19lem2  38989  jm2.22  38994  jm2.23  38995  jm2.25  38998  jm2.27c  39006  rmxdiophlem  39014  expdioph  39022  hbtlem4  39128  itgpowd  39223  relexpmulg  39424  fincygsubgodd  40053  radcnvrat  40068  nzprmdif  40073  bcc0  40094  bccp1k  40095  bccbc  40099  binomcxplemnn0  40103  binomcxplemrat  40104  binomcxplemfrat  40105  binomcxplemnotnn0  40110  fzisoeu  41002  mccllem  41315  dvxpaek  41661  dvnxpaek  41663  dvnmul  41664  dvnprodlem1  41667  dvnprodlem2  41668  stoweidlem24  41746  stirlinglem3  41798  stirlinglem7  41802  fourierdlem36  41865  fourierdlem47  41875  etransclem23  41979  etransclem32  41988  etransclem48  42004  fz0addcom  42929  fmtnom1nn  43068  fmtnof1  43071  fmtnorec1  43073  sqrtpwpw2p  43074  fmtnorec2lem  43078  fmtnorec3  43084  fmtnofac2lem  43104  fmtnofac2  43105  fmtnofac1  43106  lighneallem3  43146  lighneallem4b  43148  altgsumbc  43770  altgsumbcALT  43771  nnpw2pmod  44017  dignn0ehalf  44051  nn0sumshdiglemA  44053  nn0sumshdiglemB  44054  nn0sumshdiglem2  44056  nn0mullong  44059  aacllem  44275